Enable choice of term ordering for REST

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.

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)

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
   }
 

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)
 

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

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

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 = ()