diff --git a/docs/mkDocs/docs/options.md b/docs/mkDocs/docs/options.md index 51cc7ef6b3..1ac9ea013e 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 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). + +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 d6c95d1d53..2284da8344 160000 --- a/liquid-fixpoint +++ b/liquid-fixpoint @@ -1 +1 @@ -Subproject commit d6c95d1d535125f99f382fa503d012d008b0d480 +Subproject commit 2284da83449368adc3cd780567e8a78bfeeda449 diff --git a/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs b/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs index f7d25bff88..c6570b97e7 100644 --- a/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs +++ b/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs @@ -62,6 +62,7 @@ fixConfig tgt cfg = def , FC.fuel = fuel cfg , FC.noEnvironmentReduction = not (environmentReduction cfg) , FC.inlineANFBindings = inlineANFBindings 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 5d724505e2..28afe528b3 100644 --- a/src/Language/Haskell/Liquid/UX/CmdLine.hs +++ b/src/Language/Haskell/Liquid/UX/CmdLine.hs @@ -458,7 +458,15 @@ config = cmdArgsMode $ Config { , "Sometimes improves performance and sometimes worsens it." , "Disabled by --no-environment-reduction" ]) - , pandocHtml + , restOrdering + = "rpo" + &= name "rest-ordering" + &= help (unwords + [ "Ordering Constraints Algebra to use for REST." + , "Available options are rpo|kbo|lpo|fuelN (where N is some positive integer)." + , "rpo is the default option" + ]) + , pandocHtml = False &= name "pandoc-html" &= help "Use pandoc to generate html." @@ -720,6 +728,7 @@ defConfig = Config , environmentReduction = False , noEnvironmentReduction = False , inlineANFBindings = False + , restOrdering = "rpo" , pandocHtml = False } diff --git a/src/Language/Haskell/Liquid/UX/Config.hs b/src/Language/Haskell/Liquid/UX/Config.hs index 1cf54cbff5..478375f667 100644 --- a/src/Language/Haskell/Liquid/UX/Config.hs +++ b/src/Language/Haskell/Liquid/UX/Config.hs @@ -107,6 +107,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 -- ^ The ordering to use for REST , pandocHtml :: Bool -- ^ Use pandoc to generate html } deriving (Generic, Data, Typeable, Show, Eq) diff --git a/stack.yaml b/stack.yaml index 06d7cd3231..011dafcf64 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: 1cadb23edfbc393245ae964315b07f5c8581ea9f 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 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 = ()