Merge pull request #725 from AlecsFerra/develop

Support for lambdas :)
ucsd-progsys · Dec 16, 2024 · 48ea289 · 48ea289
2 parents 66b710d + 7ee749a
commit 48ea289
Show file tree

Hide file tree

Showing 7 changed files with 97 additions and 7 deletions.
diff --git a/src/Language/Fixpoint/Defunctionalize.hs b/src/Language/Fixpoint/Defunctionalize.hs
@@ -24,6 +24,7 @@ module Language.Fixpoint.Defunctionalize
 
 import qualified Data.HashMap.Strict as M
 import           Data.Hashable
+import           Data.Bifunctor (bimap)
 import           Control.Monad ((>=>))
 import           Control.Monad.State
 import           Language.Fixpoint.Misc            (fM, secondM)
@@ -32,6 +33,8 @@ import           Language.Fixpoint.Types        hiding (GInfo(..), allowHO, fi)
 import qualified Language.Fixpoint.Types           as Types (GInfo(..))
 import           Language.Fixpoint.Types.Config
 import           Language.Fixpoint.Types.Visitor   (mapMExpr)
+
+
 -- import Debug.Trace (trace)
 
 defunctionalize :: (Fixpoint a) => Config -> SInfo a -> SInfo a
@@ -68,11 +71,12 @@ shiftLam i x t e = ELam (x_i, t) (e `subst1` (x, x_i_t))
 -- is surrounded with a cast.
 
 normalizeLams :: Expr -> Expr
-normalizeLams e = snd $ normalizeLamsFromTo 1 e
+normalizeLams = snd . normalizeLamsFromTo 1
 
 normalizeLamsFromTo :: Int -> Expr -> (Int, Expr)
 normalizeLamsFromTo i   = go
   where
+    go :: Expr -> (Int, Expr)
     go (ELam (y, sy) e) = (i' + 1, shiftLam i' y sy e') where (i', e') = go e
                           -- let (i', e') = go e
                           --    y'       = lamArgSymbol i'  -- SHIFTLAM
@@ -81,7 +85,33 @@ normalizeLamsFromTo i   = go
                               (i2, e2') = go e2
                           in (max i1 i2, EApp e1' e2')
     go (ECst e s)       = fmap (`ECst` s) (go e)
+    go (EIte e1 e2 e3)  = let (i1, e1') = go e1
+                              (i2, e2') = go e2
+                              (i3, e3') = go e3
+                          in (maximum [i1, i2, i3], EIte e1' e2' e3')
+    go (ENeg e)         = fmap ENeg (go e)
+    go (EBin op e1 e2)  = let (i1, e1') = go e1
+                              (i2, e2') = go e2
+                          in (max i1 i2, EBin op e1' e2')
+    go (ETApp e s)      = fmap (`ETApp` s) (go e)
+    go (ETAbs e s)      = fmap (`ETAbs` s) (go e)
+    go (PAnd [])        = (i, PAnd [])
+    go (POr [])         = (i, POr  [])
+    go (PAnd es)        = bimap maximum PAnd $ unzip $ fmap go es
+    go (POr es)         = bimap maximum POr  $ unzip $ fmap go es
+    go (PNot e)         = fmap PNot (go e)
+    go (PImp e1 e2)     = let (i1, e1') = go e1
+                              (i2, e2') = go e2
+                          in (max i1 i2, PImp e1' e2')
+    go (PIff e1 e2)     = let (i1, e1') = go e1
+                              (i2, e2') = go e2
+                          in (max i1 i2, PIff e1' e2')
+    go (PAtom r e1 e2)  = let (i1, e1') = go e1
+                              (i2, e2') = go e2
+                          in (max i1 i2, PAtom r e1' e2')
     go (PAll bs e)      = fmap (PAll bs) (go e)
+    go (PExist bs e)    = fmap (PExist bs) (go e)
+    go (ECoerc s1 s2 e) = fmap (ECoerc s1 s2) (go e)
     go e                = (i, e)
 
 
@@ -179,7 +209,7 @@ data DFST = DFST
   , dfLams  :: ![Expr]      -- ^ lambda expressions appearing in the expressions
   , dfRedex :: ![Expr]      -- ^ redexes appearing in the expressions
   , dfBinds :: !(SEnv Sort) -- ^ sorts of new lambda-binders
-  }
+  } deriving Show
 
 makeDFState :: Config -> SymEnv -> IBindEnv -> DFST
 makeDFState cfg env ibind = DFST

diff --git a/src/Language/Fixpoint/Smt/Theories.hs b/src/Language/Fixpoint/Smt/Theories.hs
@@ -589,8 +589,14 @@ bvConcatSort = FAbs 0 $ FAbs 1 $ FAbs 2 $
 interpSym :: Symbol -> Raw -> Sort -> (Symbol, TheorySymbol)
 interpSym x n t = (x, Thy x n t Theory)
 
+-- This variable is uded to generate the lambda names `lam_arg$n` in
+-- `Interface.hs` that will be used during defunctionalization in
+-- `Defunctionalize.hs`, is a pretty gross hack as if the user typees in the
+-- program or ple generates a term that has more than `maxLamArg` lambda binders
+-- one inside the other, the smt will crash complaining that
+-- `lam_arg${maxLamArg}` was not declared.
 maxLamArg :: Int
-maxLamArg = 7
+maxLamArg = 20
 
 axiomLiterals :: [(Symbol, Sort)] -> [Expr]
 axiomLiterals lts = catMaybes [ lenAxiom l <$> litLen l | (l, t) <- lts, isString t ]

diff --git a/src/Language/Fixpoint/Solver/PLE.hs b/src/Language/Fixpoint/Solver/PLE.hs
@@ -653,6 +653,26 @@ eval γ ctx et = go
 -- | 'evalELamb' produces equations that preserve the context of a rewrite
 -- so equations include any necessary lambda bindings.
 evalELam :: Knowledge -> ICtx -> EvalType -> (Symbol, Sort) -> Expr -> EvalST (Expr, FinalExpand)
+evalELam γ ctx et (x, s) e
+  | not $ isEtaSymbol x = do
+    -- We need to refresh it as for some reason names bound by lambdas
+    -- present in the source code are getting declared twice.
+    -- Maybe we should define a new type of identifier for this kind of fresh
+    -- variables and not reuse the etabeta ones.
+    [ xFresh ] <- makeFreshEtaNames 1
+    let newBody = subst (mkSubst [(x, EVar xFresh)]) e
+
+    modify $ \st -> st
+      { evNewEqualities 
+        = S.insert (ELam (x, s) e, ELam (xFresh, s) newBody)
+                   (evNewEqualities st) 
+      }
+
+    evalELam γ ctx et (xFresh, s) newBody
+  where 
+    isEtaSymbol :: Symbol -> Bool
+    isEtaSymbol = isPrefixOfSym "eta"
+
 evalELam γ ctx et (x, s) e = do
     oldPendingUnfoldings <- gets evPendingUnfoldings
     oldEqs <- gets evNewEqualities
@@ -1113,7 +1133,7 @@ substEq env eq es = subst su (substEqCoerce env eq es)
   where su = mkSubst $ zip (eqArgNames eq) es
 
 substEqCoerce :: SEnv Sort -> Equation -> [Expr] -> Expr
-substEqCoerce env eq es = Vis.applyCoSub coSub $ eqBody eq
+substEqCoerce env eq es = Vis.applyCoSubV coSub $ eqBody eq
   where
     ts    = snd    <$> eqArgs eq
     sp    = panicSpan "mkCoSub"
@@ -1125,18 +1145,20 @@ substEqCoerce env eq es = Vis.applyCoSub coSub $ eqBody eq
 --
 -- The variables in the domain of the substitution are those that appear
 -- as @FObj symbol@ in @xTs@.
-mkCoSub :: SEnv Sort -> [Sort] -> [Sort] -> Vis.CoSub
+mkCoSub :: SEnv Sort -> [Sort] -> [Sort] -> Vis.CoSubV
 mkCoSub env eTs xTs = M.fromList [ (x, unite ys) | (x, ys) <- Misc.groupList xys ]
   where
     unite ts    = Mb.fromMaybe (uError ts) (unifyTo1 symToSearch ts)
     symToSearch = mkSearchEnv env
     uError ts   = panic ("mkCoSub: cannot build CoSub for " ++ showpp xys ++ " cannot unify " ++ showpp ts)
+    xys :: [(Sort, Sort)]
     xys         = Misc.sortNub $ concat $ zipWith matchSorts xTs eTs
 
-matchSorts :: Sort -> Sort -> [(Symbol, Sort)]
+matchSorts :: Sort -> Sort -> [(Sort, Sort)]
 matchSorts = go
   where
-    go (FObj x)      {-FObj-} y    = [(x, y)]
+    go x@(FObj _)    {-FObj-} y    = [(x, y)]
+    go x@(FVar _)    {-FObj-} y    = [(x, y)]
     go (FAbs _ t1)   (FAbs _ t2)   = go t1 t2
     go (FFunc s1 t1) (FFunc s2 t2) = go s1 s2 ++ go t1 t2
     go (FApp s1 t1)  (FApp s2 t2)  = go s1 s2 ++ go t1 t2

diff --git a/src/Language/Fixpoint/Types/Environments.hs b/src/Language/Fixpoint/Types/Environments.hs
@@ -178,6 +178,7 @@ lookupSEnvWithDistance x (SE env)
 
 
 data SESearch a = Found a | Alts [Symbol]
+  deriving Show
 
 -- | Functions for Indexed Bind Environment
 

diff --git a/src/Language/Fixpoint/Types/Refinements.hs b/src/Language/Fixpoint/Types/Refinements.hs
@@ -95,6 +95,7 @@ module Language.Fixpoint.Types.Refinements (
   , reftConjuncts
   , sortedReftSymbols
   , substSortInExpr
+  , sortSubstInExpr
 
   -- * Transforming
   , mapPredReft
@@ -428,6 +429,18 @@ substSortInExpr f = onEverySubexpr go
       ECoerc t0 t1 e -> ECoerc (substSort f t0) (substSort f t1) e
       e -> e
 
+
+sortSubstInExpr :: SortSubst -> Expr -> Expr
+sortSubstInExpr f = onEverySubexpr go
+  where
+    go = \case
+      ELam (x, t) e -> ELam (x, sortSubst f t) e
+      PAll xts e -> PAll (second (sortSubst f) <$> xts) e
+      PExist xts e -> PExist (second (sortSubst f) <$> xts) e
+      ECst e t -> ECst e (sortSubst f t)
+      ECoerc t0 t1 e -> ECoerc (sortSubst f t0) (sortSubst f t1) e
+      e -> e
+
 exprKVars :: Expr -> HashMap KVar [Subst]
 exprKVars = go
   where

diff --git a/src/Language/Fixpoint/Types/Sorts.hs b/src/Language/Fixpoint/Types/Sorts.hs
@@ -57,6 +57,7 @@ module Language.Fixpoint.Types.Sorts (
 
   , mkSortSubst
   , sortSubst
+  , SortSubst
   , functionSort
   , mkFFunc
   , bkFFunc

diff --git a/src/Language/Fixpoint/Types/Visitor.hs b/src/Language/Fixpoint/Types/Visitor.hs
@@ -37,6 +37,8 @@ module Language.Fixpoint.Types.Visitor (
   -- * Coercion Substitutions
   , CoSub
   , applyCoSub
+  , CoSubV
+  , applyCoSubV
 
   -- * Predicates on Constraints
   , isConcC , isConc, isKvarC
@@ -395,6 +397,21 @@ applyCoSub coSub = mapExprOnExpr fE
     fS t              = t
     txV a             = M.lookupDefault (FObj a) a coSub
 
+
+type CoSubV = M.HashMap Sort Sort
+
+applyCoSubV :: CoSubV -> Expr -> Expr
+applyCoSubV coSub = mapExprOnExpr fE
+  where
+    fE (ECoerc s t e) = ECoerc  (txS s) (txS t) e
+    fE (ELam (x,t) e) = ELam (x, txS t)         e
+    fE (ECst e t)     = ECst e (txS t)
+    fE e              = e
+
+    txS               = mapSortOnlyOnce fS
+
+    fS t              = M.lookupDefault t t coSub
+
 ---------------------------------------------------------------------------------
 -- | Visitors over @Sort@
 ---------------------------------------------------------------------------------
Original file line number	Diff line number	Diff line change
Expand Up		@@ -178,6 +178,7 @@ lookupSEnvWithDistance x (SE env)


		data SESearch a = Found a \| Alts [Symbol]
		deriving Show

		-- \| Functions for Indexed Bind Environment

Expand Down