From 000c0ab7b3aa41547f5100f314678b6f04cac1c8 Mon Sep 17 00:00:00 2001 From: Zack Grannan Date: Mon, 8 Nov 2021 20:37:23 -0800 Subject: [PATCH 1/9] Allow different ordering constraints --- liquid-fixpoint | 2 +- src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs | 1 + src/Language/Haskell/Liquid/UX/CmdLine.hs | 5 +++++ src/Language/Haskell/Liquid/UX/Config.hs | 1 + 4 files changed, 8 insertions(+), 1 deletion(-) diff --git a/liquid-fixpoint b/liquid-fixpoint index f0f4732d92..f1205b43a0 160000 --- a/liquid-fixpoint +++ b/liquid-fixpoint @@ -1 +1 @@ -Subproject commit f0f4732d921326e9481a7ece0d92387c16e5b8f8 +Subproject commit f1205b43a0480f2ba7f370a178d5a96d935325d3 diff --git a/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs b/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs index f79ed92eab..d3f5929d18 100644 --- a/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs +++ b/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs @@ -61,6 +61,7 @@ fixConfig tgt cfg = def , FC.fuel = fuel cfg , FC.noEnvironmentReduction = not (environmentReduction cfg) , FC.inlineANFBindings = inlineANFBindings cfg + , FC.restOrdering = read (restOrdering cfg) } cgInfoFInfo :: TargetInfo -> CGInfo -> IO (F.FInfo Cinfo) diff --git a/src/Language/Haskell/Liquid/UX/CmdLine.hs b/src/Language/Haskell/Liquid/UX/CmdLine.hs index 9cf7a34c16..c43054d961 100644 --- a/src/Language/Haskell/Liquid/UX/CmdLine.hs +++ b/src/Language/Haskell/Liquid/UX/CmdLine.hs @@ -446,6 +446,10 @@ config = cmdArgsMode $ Config { , "Sometimes improves performance and sometimes worsens it." , "Disabled by --no-environment-reduction" ]) + , restOrdering + = "rpo" + &= name "rest-ordering" + &= help "Ordering Constraints Algebra to use for REST" } &= program "liquid" &= help "Refinement Types for Haskell" &= summary copyright @@ -702,6 +706,7 @@ defConfig = Config , environmentReduction = False , noEnvironmentReduction = False , inlineANFBindings = False + , restOrdering = "rpo" } diff --git a/src/Language/Haskell/Liquid/UX/Config.hs b/src/Language/Haskell/Liquid/UX/Config.hs index d8cc953ef3..8b334d9c64 100644 --- a/src/Language/Haskell/Liquid/UX/Config.hs +++ b/src/Language/Haskell/Liquid/UX/Config.hs @@ -105,6 +105,7 @@ data Config = Config , noEnvironmentReduction :: Bool -- ^ Don't perform environment reduction , inlineANFBindings :: Bool -- ^ Inline ANF bindings. -- Sometimes improves performance and sometimes worsens it. + , restOrdering :: String } deriving (Generic, Data, Typeable, Show, Eq) allowPLE :: Config -> Bool From 03505b4a9c884858a50b37c604fee8e1e73a55c9 Mon Sep 17 00:00:00 2001 From: Zack Grannan Date: Mon, 22 Nov 2021 19:58:58 -0800 Subject: [PATCH 2/9] Update liquid-fixpoint --- liquid-fixpoint | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquid-fixpoint b/liquid-fixpoint index f1205b43a0..efed204f67 160000 --- a/liquid-fixpoint +++ b/liquid-fixpoint @@ -1 +1 @@ -Subproject commit f1205b43a0480f2ba7f370a178d5a96d935325d3 +Subproject commit efed204f673f5fb57ed65bd50722d42f8d7b5c7c From a0e764b5a1aa7a5d2f2c35205862b79645d2338b Mon Sep 17 00:00:00 2001 From: Zack Grannan Date: Tue, 8 Feb 2022 15:58:03 -0800 Subject: [PATCH 3/9] Update Liquid-Fixpoint, REST --- liquid-fixpoint | 2 +- stack.yaml | 4 ++-- stack.yaml.lock | 14 +++++++------- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/liquid-fixpoint b/liquid-fixpoint index 9a01884523..51d005c1b8 160000 --- a/liquid-fixpoint +++ b/liquid-fixpoint @@ -1 +1 @@ -Subproject commit 9a01884523f83e31da12c85099acda262d50aa8b +Subproject commit 51d005c1b81eead710ace359be376cd6c5a005cc diff --git a/stack.yaml b/stack.yaml index 06d7cd3231..f25384cc1c 100644 --- a/stack.yaml +++ b/stack.yaml @@ -19,8 +19,8 @@ packages: - . extra-deps: - hashable-1.3.0.0 -- git: https://github.com/facundominguez/rest - commit: 31e974979c90e910efe5199ee0d3721b791667f6 +- git: https://github.com/zgrannan/rest + commit: 2833a743c310747eee1accba2a5bf0b5338e7bb6 resolver: lts-18.14 compiler: ghc-8.10.7 diff --git a/stack.yaml.lock b/stack.yaml.lock index 6259ea8ff7..25efca8729 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -13,15 +13,15 @@ packages: hackage: hashable-1.3.0.0 - completed: name: rest-rewrite - version: 0.2.0 - git: https://github.com/facundominguez/rest + version: 0.2.1 + git: https://github.com/zgrannan/rest pantry-tree: - size: 4013 - sha256: 2a91674ccab6b0bd43dcc41fa5e2cb60cbfd35ad585df8293c2884466091d0c0 - commit: 31e974979c90e910efe5199ee0d3721b791667f6 + size: 4368 + sha256: 725fad92ed6299d02fb26aec13b6dd383be111f09377532363277228d2c28658 + commit: 2833a743c310747eee1accba2a5bf0b5338e7bb6 original: - git: https://github.com/facundominguez/rest - commit: 31e974979c90e910efe5199ee0d3721b791667f6 + git: https://github.com/zgrannan/rest + commit: 2833a743c310747eee1accba2a5bf0b5338e7bb6 snapshots: - completed: size: 586069 From 809b4e9cee95b16e14f3015c65f72284c0be7de3 Mon Sep 17 00:00:00 2001 From: Zack Grannan Date: Wed, 9 Feb 2022 19:48:23 -0800 Subject: [PATCH 4/9] Update fixpoint --- liquid-fixpoint | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquid-fixpoint b/liquid-fixpoint index 51d005c1b8..d8d276ddbf 160000 --- a/liquid-fixpoint +++ b/liquid-fixpoint @@ -1 +1 @@ -Subproject commit 51d005c1b81eead710ace359be376cd6c5a005cc +Subproject commit d8d276ddbf7affad4c437ce09c6d091d23dde4fe From c1f66d4e853d7e9111254f17fdea3abb42f4a63e Mon Sep 17 00:00:00 2001 From: Zack Grannan Date: Thu, 10 Feb 2022 18:20:29 -0800 Subject: [PATCH 5/9] Update fixpoint, add KBO test --- docs/mkDocs/docs/options.md | 25 +++++++ liquid-fixpoint | 2 +- .../Haskell/Liquid/Constraint/ToFixpoint.hs | 2 +- src/Language/Haskell/Liquid/UX/CmdLine.hs | 6 +- tests/pos/RewriteKBO.hs | 75 +++++++++++++++++++ 5 files changed, 107 insertions(+), 3 deletions(-) create mode 100644 tests/pos/RewriteKBO.hs diff --git a/docs/mkDocs/docs/options.md b/docs/mkDocs/docs/options.md index 51cc7ef6b3..3b87172b61 100644 --- a/docs/mkDocs/docs/options.md +++ b/docs/mkDocs/docs/options.md @@ -446,3 +446,28 @@ verification attempts. It is also possible to generate *slide shows* from the above. See the [slides directory](https://github.com/ucsd-progsys/liquidhaskell/tree/develop/docs/slides) for an example. + +## Rewrite Rules + +Liquid Haskell provdes experimental support for automatic axiom instantiation +via rewriting. Usage examples are contained in the `Rewrite` tests +[here](https://github.com/ucsd-progsys/liquidhaskell/tree/develop/tests/pos). + +Termination checking for rewriting can be enabled with the argument +`--rw-termination-check`. Enabling this setting uses REST to ensure termination, +REST is described [in this +paper](https://s3.us-west-1.wasabisys.com/zg-public/paper.pdf). + +The ordering constraint algebra used by REST can be adjusted by setting the +`--rest-ordering` flag. Available options are: + +- `rpo`: Recursive Path Ordering (default) +- `kbo`: Knuth-Bendix Ordering +- `lpo`: Lexicographic Path Ordering +- `fuelN`: Only apply `N` consecutive rewriting steps in a row (i.e `fuel5`, `fuel10`, etc). + +The default ordering (`rpo`) is expected to work well for most use cases. +Understanding when other rewrite orderings are preferable requires a bit of +knowledge about termination orders for rewriting; [this survey +paper](https://www.cs.tau.ac.il/~nachumd/papers/termination.pdf) may provide a +good starting place. diff --git a/liquid-fixpoint b/liquid-fixpoint index d8d276ddbf..da96d82b3d 160000 --- a/liquid-fixpoint +++ b/liquid-fixpoint @@ -1 +1 @@ -Subproject commit d8d276ddbf7affad4c437ce09c6d091d23dde4fe +Subproject commit da96d82b3d798912479e9dc937c64b7fb4b77d84 diff --git a/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs b/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs index 04d0ee9279..c6570b97e7 100644 --- a/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs +++ b/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs @@ -62,7 +62,7 @@ fixConfig tgt cfg = def , FC.fuel = fuel cfg , FC.noEnvironmentReduction = not (environmentReduction cfg) , FC.inlineANFBindings = inlineANFBindings cfg - , FC.restOrdering = read (restOrdering cfg) + , FC.restOrdering = restOrdering cfg } cgInfoFInfo :: TargetInfo -> CGInfo -> IO (F.FInfo Cinfo) diff --git a/src/Language/Haskell/Liquid/UX/CmdLine.hs b/src/Language/Haskell/Liquid/UX/CmdLine.hs index 2e5f46a7bd..ce66d30352 100644 --- a/src/Language/Haskell/Liquid/UX/CmdLine.hs +++ b/src/Language/Haskell/Liquid/UX/CmdLine.hs @@ -461,7 +461,11 @@ config = cmdArgsMode $ Config { , restOrdering = "rpo" &= name "rest-ordering" - &= help "Ordering Constraints Algebra to use for REST" + &= help (unwords + [ "Ordering Constraints Algebra to use for REST." + , "Available options : rpo|kbo|lpo|fuelN (where N is some positive integer)" + , "rpo is the default option" + ]) , pandocHtml = False &= name "pandoc-html" diff --git a/tests/pos/RewriteKBO.hs b/tests/pos/RewriteKBO.hs new file mode 100644 index 0000000000..fb952000fe --- /dev/null +++ b/tests/pos/RewriteKBO.hs @@ -0,0 +1,75 @@ +module RewriteKBO where + +{-@ LIQUID "--ple" @-} +{-@ LIQUID "--reflection" @-} +{-@ LIQUID "--fast" @-} +{-@ LIQUID "--rw-termination-check" @-} +{-@ LIQUID "--rest-ordering=kbo" @-} + +import Language.Haskell.Liquid.ProofCombinators + +data Set = Empty | Tree Int Set Set + +{-@ infix \/ @-} +{-@ measure \/ :: Set -> Set -> Set @-} +{-@ assume \/ :: a : Set -> b : Set -> { v : Set | v = a \/ b } @-} +(\/) :: Set -> Set -> Set +a \/ b = undefined + + +{-@ infix /\ @-} +{-@ measure /\ :: Set -> Set -> Set @-} +{-@ assume /\ :: a : Set -> b : Set -> { v : Set | v = a /\ b } @-} +(/\) :: Set -> Set -> Set +a /\ b = undefined + +{-@ measure emptySet :: Set @-} +{-@ assume emptySet :: {v : Set | v = emptySet} @-} +emptySet :: Set +emptySet = undefined + +{-@ predicate IsSubset M1 M2 = M1 \/ M2 = M2 @-} +{-@ predicate IsDisjoint M1 M2 = M1 /\ M2 = emptySet @-} + +{-@ rewrite unionIntersect @-} +{-@ assume unionIntersect :: s0 : Set -> s1 : Set -> s2 : Set -> { (s0 \/ s1) /\ s2 = (s0 /\ s2) \/ (s1 /\ s2) } @-} +unionIntersect :: Set -> Set -> Set -> Proof +unionIntersect _ _ _ = () + +{-@ rewrite intersectSelf @-} +{-@ assume intersectSelf :: s0 : Set -> { s0 /\ s0 = s0 } @-} +intersectSelf :: Set -> Proof +intersectSelf _ = () + +{-@ rewrite unionIdemp @-} +{-@ assume unionIdemp :: ma : Set -> {v : () | IsSubset ma ma } @-} +unionIdemp :: Set -> Proof +unionIdemp _ = () + +{-@ rewrite unionAssoc @-} +{-@ assume unionAssoc :: ma : Set -> mb : Set -> mc : Set -> {v : () | (ma \/ mb) \/ mc = ma \/ (mb \/ mc) } @-} +unionAssoc :: Set -> Set -> Set -> Proof +unionAssoc _ _ _ = () + +{-@ rewrite unionComm @-} +{-@ assume unionComm :: ma : Set -> mb : Set -> {v : () | ma \/ mb = mb \/ ma } @-} +unionComm :: Set -> Set -> Proof +unionComm _ _ = () + +{-@ rewrite intersectComm @-} +{-@ assume intersectComm :: ma : Set -> mb : Set -> {v : () | ma /\ mb = mb /\ ma } @-} +intersectComm :: Set -> Set -> Proof +intersectComm _ _ = () + +{-@ rewrite unionEmpty @-} +{-@ assume unionEmpty :: ma : Set -> {v : () | ma \/ emptySet = ma } @-} +unionEmpty :: Set -> Proof +unionEmpty _ = () + +{-====================================================== + Proofs +=======================================================-} + +{-@ unionMono :: s : Set -> s2 : Set -> {s1 : Set | IsSubset s1 s2 } -> { IsSubset (s \/ s1) (s \/ s2)} @-} +unionMono :: Set -> Set -> Set -> Proof +unionMono s s2 s1 = () From 97d716c05e28cdf4676d5f29419951134296b57e Mon Sep 17 00:00:00 2001 From: Zack Grannan Date: Fri, 11 Feb 2022 08:50:16 -0800 Subject: [PATCH 6/9] Update fixpoint --- liquid-fixpoint | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/liquid-fixpoint b/liquid-fixpoint index da96d82b3d..f3d87b78dd 160000 --- a/liquid-fixpoint +++ b/liquid-fixpoint @@ -1 +1 @@ -Subproject commit da96d82b3d798912479e9dc937c64b7fb4b77d84 +Subproject commit f3d87b78dd46bd64efdd7007ac81acf5ad9e71ff From 2c262e415b703a328ce68724174306c8ba25b30c Mon Sep 17 00:00:00 2001 From: Zack Grannan Date: Fri, 11 Feb 2022 11:37:14 -0800 Subject: [PATCH 7/9] Slightly improve help message --- src/Language/Haskell/Liquid/UX/CmdLine.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Language/Haskell/Liquid/UX/CmdLine.hs b/src/Language/Haskell/Liquid/UX/CmdLine.hs index ce66d30352..28afe528b3 100644 --- a/src/Language/Haskell/Liquid/UX/CmdLine.hs +++ b/src/Language/Haskell/Liquid/UX/CmdLine.hs @@ -463,7 +463,7 @@ config = cmdArgsMode $ Config { &= name "rest-ordering" &= help (unwords [ "Ordering Constraints Algebra to use for REST." - , "Available options : rpo|kbo|lpo|fuelN (where N is some positive integer)" + , "Available options are rpo|kbo|lpo|fuelN (where N is some positive integer)." , "rpo is the default option" ]) , pandocHtml From d971c6d7f053983468b7bd4e462c6e39f656de5d Mon Sep 17 00:00:00 2001 From: Zack Grannan Date: Mon, 14 Feb 2022 12:28:47 -0800 Subject: [PATCH 8/9] Update docs/mkDocs/docs/options.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Facundo Domínguez --- docs/mkDocs/docs/options.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/mkDocs/docs/options.md b/docs/mkDocs/docs/options.md index 3b87172b61..1ac9ea013e 100644 --- a/docs/mkDocs/docs/options.md +++ b/docs/mkDocs/docs/options.md @@ -449,7 +449,7 @@ verification attempts. ## Rewrite Rules -Liquid Haskell provdes experimental support for automatic axiom instantiation +Liquid Haskell provides experimental support for automatic axiom instantiation via rewriting. Usage examples are contained in the `Rewrite` tests [here](https://github.com/ucsd-progsys/liquidhaskell/tree/develop/tests/pos). From 406fad0e524fa91c9d5c3c9ac7ce77fc970a5f83 Mon Sep 17 00:00:00 2001 From: Zack Grannan Date: Tue, 15 Feb 2022 10:54:39 -0800 Subject: [PATCH 9/9] Update fixpoint --- liquid-fixpoint | 2 +- stack.yaml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/liquid-fixpoint b/liquid-fixpoint index 93bcaea1fa..2284da8344 160000 --- a/liquid-fixpoint +++ b/liquid-fixpoint @@ -1 +1 @@ -Subproject commit 93bcaea1fa75bf1352fd5f135d1c9637ce8b5ec9 +Subproject commit 2284da83449368adc3cd780567e8a78bfeeda449 diff --git a/stack.yaml b/stack.yaml index f25384cc1c..011dafcf64 100644 --- a/stack.yaml +++ b/stack.yaml @@ -20,7 +20,7 @@ packages: extra-deps: - hashable-1.3.0.0 - git: https://github.com/zgrannan/rest - commit: 2833a743c310747eee1accba2a5bf0b5338e7bb6 + commit: 1cadb23edfbc393245ae964315b07f5c8581ea9f resolver: lts-18.14 compiler: ghc-8.10.7