Merge pull request #705 from AlecsFerra/develop

Extensional reasoning on Values

CHANGES.md

@@ -6,6 +6,7 @@
   messages in LH
   [#2346](https://github.com/ucsd-progsys/liquidhaskell/issues/2346).
 - Support extensionality in PLE [#704](https://github.com/ucsd-progsys/liquid-fixpoint/pull/704)
+- Add a new flag `--etabeta` to reason with lambdas in PLE [#705](https://github.com/ucsd-progsys/liquid-fixpoint/pull/705)
 
 ## 0.9.6.3.1 (2024-08-21)
 

src/Language/Fixpoint/Smt/Serialize.hs

@@ -183,7 +183,7 @@ smt2VarAs :: SymEnv -> Symbol -> Sort -> Builder
 smt2VarAs env x t = parenSeqs ["as", smt2 env x, smt2SortMono x env t]
 
 smt2Lam :: SymEnv -> (Symbol, Sort) -> Expr -> Builder
-smt2Lam env (x, xT) (ECst e eT) = parenSeqs [Builder.fromText lambda, x', smt2 env e]
+smt2Lam env (x, xT) full@(ECst _ eT) = parenSeqs [Builder.fromText lambda, x', smt2 env full]
   where
     x'                          = smtLamArg env x xT
     lambda                      = symbolAtName lambdaName env () (FFunc xT eT)

src/Language/Fixpoint/Solver/Common.hs

@@ -16,7 +16,7 @@ askSMT :: Config -> Context -> [(Symbol, Sort)] -> Expr -> IO Bool
 askSMT cfg ctx xs e
 --   | isContraPred e  = return False
   | isTautoPred  e     = return True
-  | null (kvarsExpr e) = checkValidWithContext ctx [] PTrue e'
+  | null (kvarsExpr e) = checkValidWithContext ctx xs PTrue e'
   | otherwise          = return False
   where
     e' = toSMT "askSMT" cfg ctx xs e

src/Language/Fixpoint/Solver/Rewrite.hs

@@ -89,6 +89,8 @@ ordConstraints (RESTFuel m) _      = bimapConstraints Fuel asFuel $ fuelOC m
     asFuel _        = undefined
 
 
+-- Note: if you change the domain of this function, you need to change
+-- also Language.Fixpoint.Solver.PLE.isExprRewritable
 convert :: Expr -> RT.RuntimeTerm
 convert (EIte i t e)   = RT.App "$ite" $ map convert [i,t,e]
 convert e@EApp{}       | (f, terms) <- splitEAppThroughECst e, EVar fName <- dropECst f

src/Language/Fixpoint/Types/Config.hs

@@ -99,6 +99,7 @@ data Config = Config
   , noslice          :: Bool           -- ^ Disable non-concrete KVar slicing
   , rewriteAxioms    :: Bool           -- ^ Allow axiom instantiation via rewriting
   , pleWithUndecidedGuards :: Bool     -- ^ Unfold invocations with undecided guards in PLE
+  , etabeta          :: Bool           -- ^ Eta expand and beta reduce terms to aid PLE
   , interpreter      :: Bool           -- ^ Do not use the interpreter to assist PLE
   , oldPLE           :: Bool           -- ^ Use old version of PLE
   , noIncrPle        :: Bool           -- ^ Use incremental PLE
@@ -259,6 +260,7 @@ defConfig = Config {
         &= name "interpreter"
         &= help "Use the interpreter to assist PLE"
   , oldPLE                   = False &= help "Use old version of PLE"
+  , etabeta                  = False &= help "Use eta expansion and beta reduction to aid PLE"
   , noIncrPle                = False &= help "Don't use incremental PLE"
   , noEnvironmentReduction   =
       False

src/Language/Fixpoint/Types/Names.hs

@@ -127,7 +127,7 @@ module Language.Fixpoint.Types.Names (
 
   , lambdaName
   , lamArgSymbol
-  , isLamArgSymbol
+  , isLamArgSymbol, etaExpSymbol
 
 ) where
 
@@ -611,6 +611,12 @@ lambdaName = "smt_lambda"
 lamArgPrefix :: Symbol
 lamArgPrefix = "lam_arg"
 
+etaExpPrefix :: Symbol
+etaExpPrefix = "eta"
+
+etaExpSymbol :: Int -> Symbol
+etaExpSymbol = intSymbol etaExpPrefix
+
 lamArgSymbol :: Int -> Symbol
 lamArgSymbol = intSymbol lamArgPrefix
 

src/Language/Fixpoint/Types/Theories.hs

@@ -29,6 +29,7 @@ module Language.Fixpoint.Types.Theories (
     , symEnvSort
     , symEnvTheory
     , insertSymEnv
+    , deleteSymEnv
     , insertsSymEnv
     , symbolAtName
     , symbolAtSmtName
@@ -151,6 +152,9 @@ symEnvSort   x env = lookupSEnv x (seSort env)
 insertSymEnv :: Symbol -> Sort -> SymEnv -> SymEnv
 insertSymEnv x t env = env { seSort = insertSEnv x t (seSort env) }
 
+deleteSymEnv :: Symbol -> SymEnv -> SymEnv
+deleteSymEnv x env = env { seSort = deleteSEnv x (seSort env) }
+
 insertsSymEnv :: SymEnv -> [(Symbol, Sort)] -> SymEnv
 insertsSymEnv = L.foldl' (\env (x, s) -> insertSymEnv x s env)
 

tests/pos/eta_cons.fq

@@ -0,0 +1,24 @@
+fixpoint "--rewrite"
+fixpoint "--allowho"
+fixpoint "--etabeta"
+
+constant f : (func(0 , [int; int; int]))
+define f (x : int, y: int) : int = {(x + y)}
+
+constant g : (func(0 , [int; int; int]))
+define g (a : int, b: int) : int = {(b + a)}
+
+
+data Ty 0 = [
+    | Cons {mkCons : func(0 , [int; int; int])}
+]
+
+constant Cons : (func(0 , [func(0 , [int; int; int]); Ty]))
+
+expand [1 : True; 2 : True]
+
+constraint:
+  env []
+  lhs {VV1 : Tuple | true }
+  rhs {VV2 : Tuple | (Cons f = Cons g) }
+  id 2 tag []

tests/tasty/SimplifyPLE.hs

@@ -32,10 +32,10 @@ simplify' = PLE.simplify emptyKnowledge emptyICtx
     emptyICtx :: PLE.ICtx
     emptyICtx =
       ICtx
-        { icAssms = S.empty, -- S.HashSet Pred
-          icCands = S.empty, -- :: S.HashSet Expr
-          icEquals = S.empty, -- :: EvAccum
-          icSimpl = SM.empty, -- :: !ConstMap
-          icSubcId = Nothing, -- :: Maybe SubcId
-          icANFs = []         -- :: [[(Symbol, SortedReft)]]
+        { icAssms = S.empty,      -- S.HashSet Pred
+          icCands = S.empty,      -- :: S.HashSet Expr
+          icEquals = S.empty,     -- :: EvAccum
+          icSimpl = SM.empty,     -- :: !ConstMap
+          icSubcId = Nothing,     -- :: Maybe SubcId
+          icANFs = []             -- :: [[(Symbol, SortedReft)]]
         }