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 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.

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: 2833a743c310747eee1accba2a5bf0b5338e7bb6
 
 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 = ()