Allow different ordering constraints

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)

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"
   }
 
 

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