Disable environment reduction by default

ucsd-progsys · Oct 25, 2021 · 1c2ea7e · 1c2ea7e
1 parent 28a6b51
commit 1c2ea7e
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 1 deletion.
diff --git a/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs b/src/Language/Haskell/Liquid/Constraint/ToFixpoint.hs
@@ -60,7 +60,7 @@ fixConfig tgt cfg = def
   , FC.rwTerminationCheck       = rwTerminationCheck cfg
   , FC.noLazyPLE                = noLazyPLE cfg
   , FC.fuel                     = fuel      cfg
-  , FC.noEnvironmentReduction   = noEnvironmentReduction cfg
+  , FC.noEnvironmentReduction   = not (environmentReduction cfg)
   , FC.inlineANFBindings        = inlineANFBindings cfg
   }
 

diff --git a/src/Language/Haskell/Liquid/UX/CmdLine.hs b/src/Language/Haskell/Liquid/UX/CmdLine.hs
@@ -434,6 +434,11 @@ config = cmdArgsMode $ Config {
     = Nothing 
         &= help "Maximum fuel (per-function unfoldings) for PLE"
 
+  , environmentReduction
+    = def
+        &= explicit
+        &= name "environment-reduction"
+        &= help "perform environment reduction (disabled by default)"
   , noEnvironmentReduction
     = def
         &= explicit
@@ -702,6 +707,7 @@ defConfig = Config
   , skipModule               = False
   , noLazyPLE                = False
   , fuel                     = Nothing
+  , environmentReduction     = False
   , noEnvironmentReduction   = False
   , inlineANFBindings        = False
   }

diff --git a/src/Language/Haskell/Liquid/UX/Config.hs b/src/Language/Haskell/Liquid/UX/Config.hs
@@ -102,6 +102,7 @@ data Config = Config
   , skipModule               :: Bool       -- ^ Skip this module entirely (don't even compile any specs in it)
   , noLazyPLE                :: Bool
   , fuel                     :: Maybe Int  -- ^ Maximum PLE "fuel" (unfold depth) (default=infinite) 
+  , environmentReduction     :: Bool       -- ^ Perform environment reduction
   , noEnvironmentReduction   :: Bool       -- ^ Don't perform environment reduction
   , inlineANFBindings        :: Bool       -- ^ Inline ANF bindings.
                                            -- Sometimes improves performance and sometimes worsens it.