From 54a15674085991bc2fc663a758d61a1e76252579 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Tue, 24 Sep 2024 19:39:02 +0000 Subject: [PATCH 1/7] Export relatedSymbols and make it a bit more general --- src/Language/Fixpoint/Solver/EnvironmentReduction.hs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/Language/Fixpoint/Solver/EnvironmentReduction.hs b/src/Language/Fixpoint/Solver/EnvironmentReduction.hs index 6375eac3e..ebf38d053 100644 --- a/src/Language/Fixpoint/Solver/EnvironmentReduction.hs +++ b/src/Language/Fixpoint/Solver/EnvironmentReduction.hs @@ -11,6 +11,7 @@ module Language.Fixpoint.Solver.EnvironmentReduction ( reduceEnvironments , simplifyBindings , dropLikelyIrrelevantBindings + , relatedSymbols , inlineInExpr , inlineInSortedReft , mergeDuplicatedBindings @@ -744,7 +745,8 @@ dropLikelyIrrelevantBindings -> HashMap Symbol SortedReft dropLikelyIrrelevantBindings ss env = HashMap.filterWithKey relevant env where - relatedSyms = relatedSymbols ss env + directlyUses = HashMap.map (exprSymbolsSet . reftPred . sr_reft) env + relatedSyms = relatedSymbols ss directlyUses relevant s _sr = (not (capitalizedSym s) || prefixOfSym s /= s) && s `HashSet.member` relatedSyms capitalizedSym = Text.all isUpper . Text.take 1 . symbolText @@ -760,10 +762,10 @@ dropLikelyIrrelevantBindings ss env = HashMap.filterWithKey relevant env -- @a@ uses @b@. Because the predicate of @c@ relates @b@ with @d@, -- @d@ can also influence the validity of the predicate of @a@, and therefore -- we include both @b@, @c@, and @d@ in the set of related symbols. -relatedSymbols :: HashSet Symbol -> HashMap Symbol SortedReft -> HashSet Symbol -relatedSymbols ss0 env = go HashSet.empty ss0 +relatedSymbols + :: HashSet Symbol -> HashMap Symbol (HashSet Symbol) -> HashSet Symbol +relatedSymbols ss0 directlyUses = go HashSet.empty ss0 where - directlyUses = HashMap.map (exprSymbolsSet . reftPred . sr_reft) env usedBy = HashMap.fromListWith HashSet.union [ (x, HashSet.singleton s) | (s, xs) <- HashMap.toList directlyUses From e9bed6460f893904afb1aac7020cc495ad47245f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Facundo=20Dom=C3=ADnguez?= Date: Tue, 24 Sep 2024 19:46:33 +0000 Subject: [PATCH 2/7] Update changelog --- CHANGES.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index 696f55750..68eae02f2 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -2,6 +2,10 @@ ## NEXT +- Expose relatedSymbols from EnvironmentReduction. Needed for improving error + 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) ## 0.9.6.3.1 (2024-08-21) From d70d85d8e77d85955e19be0f1e7a7a7d6d0611cc Mon Sep 17 00:00:00 2001 From: Alessio Ferrarini Date: Wed, 25 Sep 2024 10:10:29 +0200 Subject: [PATCH 3/7] WIP: smt=>ple equalities --- src/Language/Fixpoint/Solver/PLE.hs | 141 +++++++++++++++++++++++----- 1 file changed, 120 insertions(+), 21 deletions(-) diff --git a/src/Language/Fixpoint/Solver/PLE.hs b/src/Language/Fixpoint/Solver/PLE.hs index 30a575c66..76ddde02b 100644 --- a/src/Language/Fixpoint/Solver/PLE.hs +++ b/src/Language/Fixpoint/Solver/PLE.hs @@ -54,7 +54,7 @@ import Language.REST.SMT (withZ3, SolverHandle) import Control.Monad (filterM, foldM, forM_, when, replicateM) import Control.Monad.State import Control.Monad.Trans.Maybe -import Data.Bifunctor (second) +import Data.Bifunctor (second, bimap) import qualified Data.HashMap.Strict as M import qualified Data.HashMap.Lazy as HashMap.Lazy import qualified Data.HashSet as S @@ -65,6 +65,9 @@ import qualified Data.Map as Map import qualified Data.Maybe as Mb import qualified Data.Set as Set import Text.PrettyPrint.HughesPJ.Compat +import qualified Data.Text as T + +import Debug.Trace mytracepp :: (PPrint a) => String -> a -> a mytracepp = notracepp @@ -216,12 +219,13 @@ pleTrie t env = loopT env' ctx0 diff0 Nothing res0 t diff0 = [] res0 = M.empty ctx0 = ICtx - { icAssms = mempty - , icCands = mempty - , icEquals = mempty - , icSimpl = mempty - , icSubcId = Nothing - , icANFs = [] + { icAssms = mempty + , icCands = mempty + , icEquals = mempty + , icSimpl = mempty + , icSubcId = Nothing + , icANFs = [] + , icSMTRewrites = mempty } loopT @@ -269,9 +273,82 @@ withAssms :: InstEnv a -> ICtx -> Diff -> Maybe SubcId -> (InstEnv a -> ICtx -> withAssms env@InstEnv{..} ctx delta cidMb act = do let (ctx', env') = updCtx env ctx delta cidMb let assms = icAssms ctx' - SMT.smtBracket ieSMT "PLE.evaluate" $ do - forM_ assms (SMT.smtAssert ieSMT) - act env' ctx' { icAssms = mempty } + + let smtRewrites = concatMap (\i -> extractRewrites $ lookupBindEnv i ieBEnv) delta + + SMT.smtBracket ieSMT "PLE.evaluate" $ do + forM_ assms (SMT.smtAssert ieSMT ) + act env' ctx' { icAssms = mempty, icSMTRewrites = M.union (M.fromList smtRewrites) (icSMTRewrites ctx) } + where + + -- [(is$Something foo); + -- (~((is$SomethingElse foo)); + -- ... + -- ((prop foo) = + -- (Something v₁ ... vₙ)); + -- ((prop foo) = + -- (Something m₁ ... mₙ)); + -- ...] + + -- We some the system v₁ = m₁, v₂ = m₂, ... vₙ = mₙ + -- finding equalities between the free variables + + -- Given ((Something v₁ ... vₙ), (Something m₁ ... mₙ)) + -- obtain the unification + obtainEqualities (e1, e2) + | fst1 : args1 <- flatten $ dropECst e1 + , fst2 : args2 <- flatten $ dropECst e2 + , EVar cons1 <- dropECst fst1 + , EVar cons2 <- dropECst fst2 + , cons1 == cons2 + , Just _ <- M.lookup cons1 (knDataCtors ieKnowl) + , Just unified <- unifyArgumets args1 args2 + = do + traceShowM ("e1" :: String, cons1) + traceShowM ("e2" :: String, pprint unified) + pure unified + obtainEqualities _ = Nothing + + flatten (EApp x xs) = flatten x ++ [ xs ] + flatten x = [x] + + unifyArgumets [] [] = Just [] + unifyArgumets (x:xs) (y:ys) + | EVar xn <- dropECst x + , validVar xn + = fmap ((xn, y) :) (unifyArgumets xs ys) + unifyArgumets (x:xs) (y:ys) + | EVar yn <- dropECst y + , validVar yn + = fmap ((yn, x) :) (unifyArgumets xs ys) + unifyArgumets (x:xs) (y:ys) + | dropECst x == dropECst y + = unifyArgumets xs ys + unifyArgumets _ _ + = Nothing + + extractRewrites (_, sreft, _) + | Reft (_, PAnd ra) <- sr_reft sreft + = concat + $ Mb.mapMaybe obtainEqualities + $ Mb.mapMaybe keepTrans + $ map snd + $ Misc.groupList + $ fmap (bimap unApply unApply) + $ Mb.mapMaybe keepPropEq ra + extractRewrites _ = [] + + keepPropEq (PAtom Eq e1 e2) = Just (e1, e2) + keepPropEq _ = Nothing + + keepTrans [a, b] = Just (a, b) + keepTrans _ = Nothing + + -- Find a way to make this check more roboust + validVar name = (not $ T.elem '.' name') + && (T.elem '#' name' || T.elem '_' name') + && (not $ T.isPrefixOf "lq_anf" name') + where name' = symbolText name -- | @ple1@ performs the PLE at a single "node" in the Trie -- @@ -370,12 +447,13 @@ data InstEnv a = InstEnv ---------------------------------------------------------------------------------------------- data ICtx = ICtx - { icAssms :: S.HashSet Pred -- ^ Equalities converted to SMT format - , icCands :: S.HashSet Expr -- ^ "Candidates" for unfolding - , icEquals :: EvEqualities -- ^ Accumulated equalities - , icSimpl :: !ConstMap -- ^ Map of expressions to constants - , icSubcId :: Maybe SubcId -- ^ Current subconstraint ID - , icANFs :: [[(Symbol, SortedReft)]] -- Hopefully contain only ANF things + { icAssms :: S.HashSet Pred -- ^ Equalities converted to SMT format + , icCands :: S.HashSet Expr -- ^ "Candidates" for unfolding + , icEquals :: EvEqualities -- ^ Accumulated equalities + , icSimpl :: !ConstMap -- ^ Map of expressions to constants + , icSubcId :: Maybe SubcId -- ^ Current subconstraint ID + , icANFs :: [[(Symbol, SortedReft)]] -- Hopefully contain only ANF things + , icSMTRewrites :: M.HashMap Symbol Expr -- ^ Rewrites that have been generated by SMT } ---------------------------------------------------------------------------------------------- @@ -894,6 +972,7 @@ evalApp γ _ctx e0 es _et if not $ any hasTyVar etaArgsType then do performEtaExpansion e0 es nArgsMissing etaArgsType else do + traceShowM ("NO MONO" :: String, pprint f) -- There is at least a non monomorphized type variables -- We cant conclude anything pure (Nothing, noExpand) @@ -959,6 +1038,7 @@ evalApp γ ctx e0 es _et modify $ \st -> st { evNewEqualities = foldr S.insert (evNewEqualities st) eqs' } return (Nothing, noExpand) + evalApp γ ctx e0 es et | ELam (argName, _) body <- dropECst e0 , lambdaArg:remArgs <- es @@ -979,13 +1059,32 @@ evalApp γ ctx e0 es et else do return (Nothing, noExpand) - -evalApp _ _ _e _es _ - = return (Nothing, noExpand) - +evalApp _ ctx e0 es _ + | EVar f <- dropECst e0 + , Just rewrite <- M.lookup f (icSMTRewrites ctx) + = do + modify $ \st -> + st { evNewEqualities = S.insert (eApps e0 es, eApps rewrite es) (evNewEqualities st) } + return (Just $ eApps rewrite es, expand) + +evalApp _γ _ctx _e0 _es _ + -- = pure (Nothing, noExpand) + = do + let deANFed = deANF _ctx _e0 + if dropECst deANFed /= dropECst _e0 then do -- && not (isCoercion deANFed) then do + -- traceShowM ("Replacing" :: String, _e0, deANFed) + -- modify $ \st -> + -- st { evNewEqualities = S.insert (eApps e0 es, eApps deANFed es) (evNewEqualities st) } + return (Just $ eApps deANFed _es, expand) + else do + -- traceShowM ("evalApp: cant expand" :: String, pprint e0) + -- traceShowM ("evalApp: with args" :: String, es) + -- traceShowM ("sel" :: String, pprint (knSels γ)) + -- traceShowM ("ctors" :: String, pprint (knDataCtors γ)) + return (Nothing, noExpand) mkLams :: Expr -> [(Symbol, Sort)] -> Expr -mkLams subject binds = foldr (\bind acc -> ELam bind acc) subject binds +mkLams subject binds = foldr ELam subject binds -- | Evaluates if-then-else statements until they can't be evaluated anymore -- or some other expression is found. From f6ba16264579c8981e67f72a4bedc9cc28e6866d Mon Sep 17 00:00:00 2001 From: Alessio Ferrarini Date: Fri, 27 Sep 2024 09:28:06 +0200 Subject: [PATCH 4/7] WIP: Elaboration on ple-unfolded functions --- src/Language/Fixpoint/Solver/PLE.hs | 268 ++++++++++++++-------------- 1 file changed, 138 insertions(+), 130 deletions(-) diff --git a/src/Language/Fixpoint/Solver/PLE.hs b/src/Language/Fixpoint/Solver/PLE.hs index 76ddde02b..6d3005f90 100644 --- a/src/Language/Fixpoint/Solver/PLE.hs +++ b/src/Language/Fixpoint/Solver/PLE.hs @@ -67,8 +67,6 @@ import qualified Data.Set as Set import Text.PrettyPrint.HughesPJ.Compat import qualified Data.Text as T -import Debug.Trace - mytracepp :: (PPrint a) => String -> a -> a mytracepp = notracepp @@ -302,11 +300,7 @@ withAssms env@InstEnv{..} ctx delta cidMb act = do , EVar cons2 <- dropECst fst2 , cons1 == cons2 , Just _ <- M.lookup cons1 (knDataCtors ieKnowl) - , Just unified <- unifyArgumets args1 args2 - = do - traceShowM ("e1" :: String, cons1) - traceShowM ("e2" :: String, pprint unified) - pure unified + = unifyArgumets args1 args2 obtainEqualities _ = Nothing flatten (EApp x xs) = flatten x ++ [ xs ] @@ -584,7 +578,7 @@ getAutoRws γ ctx = evalOne :: Knowledge -> ICtx -> Int -> Expr -> EvalST [Expr] evalOne γ ctx i e | i > 0 || null (getAutoRws γ ctx) = (:[]) . fst <$> eval γ ctx NoRW False e -evalOne γ ctx _ e = do +evalOne γ ctx _ e | isExprRewritable e = do env <- get let oc :: OCAlgebra OCType RuntimeTerm IO oc = evOCAlgebra env @@ -594,6 +588,7 @@ evalOne γ ctx _ e = do es <- evalREST γ ctx rp modify $ \st -> st { explored = Just emptyET } return es +evalOne _ _ _ _ = return [] -- The FuncNormal and RWNormal evaluation strategies are used for REST -- For example, consider the following function: @@ -730,6 +725,11 @@ evalELam :: Knowledge -> ICtx -> EvalType -> (Symbol, Sort) -> Expr -> EvalST (E evalELam γ ctx et (x, s) e = do oldPendingUnfoldings <- gets evPendingUnfoldings oldEqs <- gets evNewEqualities + + -- We need to declare the variable in the environment + modify $ \st -> st + { evEnv = declareVar x s $ evEnv st } + (e', fe) <- eval (γ { knLams = (x, s) : knLams γ }) ctx et False e let e2' = simplify γ ctx e' elam = ELam (x, s) e @@ -737,15 +737,42 @@ evalELam γ ctx et (x, s) e = do modify $ \st -> st { evPendingUnfoldings = oldPendingUnfoldings , evNewEqualities = S.insert (elam, ELam (x, s) e2') oldEqs + -- Leaving the scope thus we need to get rid of it + , evEnv = deleteVar x $ evEnv st } return (ELam (x, s) e', fe) +declareVar :: Symbol -> Sort -> SymEnv -> SymEnv +declareVar x s env = env { seSort = SE $ M.insert x s (seBinds $ seSort env) } + +deleteVar :: Symbol -> SymEnv -> SymEnv +deleteVar x env = env { seSort = SE $ M.delete x (seBinds $ seSort env) } + data RESTParams oc = RP { oc :: OCAlgebra oc Expr IO , path :: [(Expr, TermOrigin)] , c :: oc } +-- With the support for lambdas in PLE now lambda expression can interact with the +-- rewriting feature. But for the moment we don't support them as we can't convert to +-- REST terms. +isExprRewritable :: Expr -> Bool +isExprRewritable (EIte i t e ) = isExprRewritable i && isExprRewritable t && isExprRewritable e +isExprRewritable (EApp f e) = isExprRewritable f && isExprRewritable e +isExprRewritable (EVar _) = True +isExprRewritable (PNot e) = isExprRewritable e +isExprRewritable (PAnd es) = all isExprRewritable es +isExprRewritable (POr es) = all isExprRewritable es +isExprRewritable (PAtom _ l r) = isExprRewritable l && isExprRewritable r +isExprRewritable (EBin _ l r) = isExprRewritable l && isExprRewritable r +isExprRewritable (ECon _) = True +isExprRewritable (ESym _) = True +isExprRewritable (ECst _ _) = True +isExprRewritable (PIff e0 e1) = isExprRewritable (PAtom Eq e0 e1) +isExprRewritable (PImp e0 e1) = isExprRewritable (POr [PNot e0, e1]) +isExprRewritable _ = False + -- Reverse the ANF transformation deANF :: ICtx -> Expr -> Expr deANF ctx = inlineInExpr (`HashMap.Lazy.lookup` undoANF id bindEnv) @@ -783,47 +810,54 @@ evalRESTWithCache cacheRef _ ctx acc rp evalRESTWithCache cacheRef γ ctx acc rp = do - Just exploredTerms <- gets explored - se <- liftIO (shouldExploreTerm exploredTerms exprs) - if se then do - possibleRWs <- getRWs - rws <- notVisitedFirst exploredTerms <$> filterM (liftIO . allowed) possibleRWs - oldEqualities <- gets evNewEqualities - modify $ \st -> st { evNewEqualities = mempty } - - -- liftIO $ putStrLn $ (show $ length possibleRWs) ++ " rewrites allowed at path length " ++ (show $ (map snd $ path rp)) - (e', FE fe) <- do - r@(ec, _) <- eval γ ctx FuncNormal False exprs - if ec /= exprs - then return r - else eval γ ctx RWNormal False exprs - - let evalIsNewExpr = e' `L.notElem` pathExprs - let exprsToAdd = [e' | evalIsNewExpr] ++ map (\(_, e, _) -> e) rws - acc' = exprsToAdd ++ acc - eqnToAdd = [ (e1, simplify γ ctx e2) | ((e1, e2), _, _) <- rws ] - - newEqualities <- gets evNewEqualities - smtCache <- liftIO $ readIORef cacheRef - modify (\st -> - st { evNewEqualities = foldr S.insert (S.union newEqualities oldEqualities) eqnToAdd - , evSMTCache = smtCache - , explored = Just $ ExploredTerms.insert - (Rewrite.convert exprs) - (c rp) - (S.insert (Rewrite.convert e') $ S.fromList (map (Rewrite.convert . (\(_, e, _) -> e)) possibleRWs)) - (Mb.fromJust $ explored st) - }) - - acc'' <- if evalIsNewExpr - then if fe && any isRW (path rp) - then (:[]) . fst <$> eval γ (addConst (exprs, e')) NoRW False e' - else evalRESTWithCache cacheRef γ (addConst (exprs, e')) acc' (rpEval newEqualities e') - else return acc' - - foldM (\r rw -> evalRESTWithCache cacheRef γ ctx r (rpRW rw)) acc'' rws - else - return acc + mexploredTerms <- gets explored + case mexploredTerms of + Nothing -> return acc + Just exploredTerms -> do + se <- liftIO (shouldExploreTerm exploredTerms exprs) + if se then do + possibleRWs <- getRWs + rws <- notVisitedFirst exploredTerms <$> filterM (liftIO . allowed) possibleRWs + oldEqualities <- gets evNewEqualities + modify $ \st -> st { evNewEqualities = mempty } + + -- liftIO $ putStrLn $ (show $ length possibleRWs) ++ " rewrites allowed at path length " ++ (show $ (map snd $ path rp)) + (e', FE fe) <- do + r@(ec, _) <- eval γ ctx FuncNormal False exprs + if ec /= exprs + then return r + else eval γ ctx RWNormal False exprs + + let evalIsNewExpr = e' `L.notElem` pathExprs + let exprsToAdd = [e' | evalIsNewExpr] ++ map (\(_, e, _) -> e) rws + acc' = exprsToAdd ++ acc + eqnToAdd = [ (e1, simplify γ ctx e2) | ((e1, e2), _, _) <- rws ] + + let explored' st = + if isExprRewritable e' && isExprRewritable exprs + then Just $ ExploredTerms.insert (Rewrite.convert exprs) (c rp) + (S.insert (Rewrite.convert e') + $ S.fromList (map (Rewrite.convert . (\(_, e, _) -> e)) possibleRWs)) + (Mb.fromJust $ explored st) + else Nothing + + newEqualities <- gets evNewEqualities + smtCache <- liftIO $ readIORef cacheRef + modify $ \st -> st + { evNewEqualities = foldr S.insert (S.union newEqualities oldEqualities) eqnToAdd + , evSMTCache = smtCache + , explored = explored' st + } + + acc'' <- if evalIsNewExpr + then if fe && any isRW (path rp) + then (:[]) . fst <$> eval γ (addConst (exprs, e')) NoRW False e' + else evalRESTWithCache cacheRef γ (addConst (exprs, e')) acc' (rpEval newEqualities e') + else return acc' + + foldM (\r rw -> evalRESTWithCache cacheRef γ ctx r (rpRW rw)) acc'' rws + else + return acc where shouldExploreTerm exploredTerms e | Vis.isConc e = case rwTerminationOpts rwArgs of @@ -891,35 +925,31 @@ evalApp γ ctx e0 es et , Just eq <- Map.lookup f (knAms γ) , length (eqArgs eq) <= length es = do - env <- gets (seSort . evEnv) + env <- gets (seSort . evEnv) okFuel <- checkFuel f - if okFuel && et /= FuncNormal - then do - let (es1,es2) = splitAt (length (eqArgs eq)) es - newE = substEq env eq es1 - (e', fe) <- evalIte γ ctx et newE -- TODO:FUEL this is where an "unfolding" happens, CHECK/BUMP counter - let e2' = stripPLEUnfold e' - e3' = simplify γ ctx (eApps e2' es2) -- reduces a bit the equations - undecidedGuards = case e' of - EIte{} -> True - _ -> False - - if undecidedGuards - then do - modify $ \st -> - st { evPendingUnfoldings = M.insert (eApps e0 es) e3' (evPendingUnfoldings st) - , evNewEqualities = S.insert (eApps e0 es, e3') (evNewEqualities st) - } - return (Just $ eApps e2' es2, fe) - else do - useFuel f - modify $ \st -> - st - { evNewEqualities = S.insert (eApps e0 es, e3') (evNewEqualities st) - , evPendingUnfoldings = M.delete (eApps e0 es) (evPendingUnfoldings st) - } - return (Just $ eApps e2' es2, fe) - else return (Nothing, noExpand) + if okFuel && et /= FuncNormal then do + let (es1, es2) = splitAt (length (eqArgs eq)) es + -- Doing elaboration ahead of time would cause too much + -- monomorphization + newE <- elaborateExpr "EvalApp unfold full: " $ substEq env eq es1 + + (e', fe) <- evalIte γ ctx et newE -- TODO:FUEL this is where an "unfolding" happens, CHECK/BUMP counter + let e2' = stripPLEUnfold e' + let e3' = simplify γ ctx (eApps e2' es2) -- reduces a bit the equations + + if isGuardUndecied e' then do + modify $ \st -> st + { evPendingUnfoldings = M.insert (eApps e0 es) e3' (evPendingUnfoldings st) + } + return (Nothing, noExpand) + else do + useFuel f + modify $ \st -> st + { evNewEqualities = S.insert (eApps e0 es, e3') (evNewEqualities st) + , evPendingUnfoldings = M.delete (eApps e0 es) (evPendingUnfoldings st) + } + return (Just $ eApps e2' es2, fe) + else return (Nothing, noExpand) where -- At the time of writing, any function application wrapping an -- if-statement would have the effect of unfolding the invocation. @@ -932,6 +962,9 @@ evalApp γ ctx e0 es et , f == "Language.Haskell.Liquid.ProofCombinators.pleUnfold" = arg | otherwise = e + + isGuardUndecied EIte{} = True + isGuardUndecied _ = False -- **ETA**: PLE before the patch to perform eta expansion was only able to unfold -- fully applied functions, by eta equivalence we mean the property that for all -- functions f the terms f and (\x -> f x) have the same semantics, we leverage @@ -966,52 +999,31 @@ evalApp γ _ctx e0 es _et -- This case is pretty suspicious as we shouldnt generate functions that do not -- have a type annotation Nothing -> do - -- Hack to recover general mono signature, by looking directly - -- at the types in the equation - let etaArgsType = fmap snd $ drop nProvidedArgs $ eqArgs eq - if not $ any hasTyVar etaArgsType then do - performEtaExpansion e0 es nArgsMissing etaArgsType - else do - traceShowM ("NO MONO" :: String, pprint f) - -- There is at least a non monomorphized type variables - -- We cant conclude anything - pure (Nothing, noExpand) + pure (Nothing, noExpand) Just etaArgsType -> do - performEtaExpansion e0 es nArgsMissing etaArgsType + -- Fresh names for the eta expansion + etaNames <- makeFreshEtaNames nArgsMissing + + let etaVars = zipWith (\name ty -> ECst (EVar name) ty) etaNames etaArgsType + let fullBody = eApps e0 (es ++ etaVars) + let etaExpandedTerm = mkLams fullBody (zip etaNames etaArgsType) + + -- Note: we should always add the equality as etaNames is always non empty because the + -- only way for etaNames to be empty is if the function is fully applied, but that case + -- is already handled by the previous case of evalApp + modify $ \st -> st + { evNewEqualities = S.insert (eApps e0 es, etaExpandedTerm) (evNewEqualities st) } + return (Just etaExpandedTerm, expand) else do pure (Nothing, noExpand) where - hasTyVar :: Sort -> Bool - hasTyVar (FObj _) = True - hasTyVar (FApp l r) = hasTyVar l || hasTyVar r - hasTyVar (FFunc l r) = hasTyVar l || hasTyVar r - hasTyVar (FAbs _ i) = hasTyVar i - hasTyVar _ = False - - extractMonoSign :: Expr -> Maybe [Sort] extractMonoSign (ECst _ sort) = Just $ flatten sort extractMonoSign _ = Nothing - flatten :: Sort -> [Sort] flatten (FFunc t ts) = t : flatten ts flatten t = [t] - performEtaExpansion :: Expr -> [Expr] -> Int -> [Sort] -> EvalST (Maybe Expr, FinalExpand) - performEtaExpansion fun actualArgs nArgsMissing etaArgsType = do - -- Fresh names for the eta expansion - etaNames <- makeFreshEtaNames nArgsMissing - - let etaVars = zipWith (\name ty -> ECst (EVar name) ty) etaNames etaArgsType - let fullBody = eApps fun (actualArgs ++ etaVars) - let etaExpandedTerm = mkLams fullBody (zip etaNames etaArgsType) - - -- Note: we should always add the equality as etaNames is always non empty because the - -- only way for etaNames to be empty is if the function is fully applied, but that case - -- is already handled by the previous case of evalApp - modify $ \st -> - st { evNewEqualities = S.insert (eApps fun es, etaExpandedTerm) (evNewEqualities st) } - - return (Just etaExpandedTerm, expand) + mkLams subject binds = foldr ELam subject binds evalApp γ ctx e0 args@(e:es) _ | EVar f <- dropECst e0 @@ -1025,10 +1037,8 @@ evalApp γ ctx e0 args@(e:es) _ = do let newE = eApps (subst (mkSubst $ zip (smArgs rw) as) (smBody rw)) es when (isUserDataSMeasure == NoUserDataSMeasure) $ - modify $ \st -> - st { evNewEqualities = - S.insert (eApps e0 args, simplify γ ctx newE) (evNewEqualities st) - } + modify $ \st -> st + { evNewEqualities = S.insert (eApps e0 args, simplify γ ctx newE) (evNewEqualities st) } return (Just newE, noExpand) evalApp γ ctx e0 es _et @@ -1068,24 +1078,16 @@ evalApp _ ctx e0 es _ return (Just $ eApps rewrite es, expand) evalApp _γ _ctx _e0 _es _ - -- = pure (Nothing, noExpand) = do let deANFed = deANF _ctx _e0 - if dropECst deANFed /= dropECst _e0 then do -- && not (isCoercion deANFed) then do - -- traceShowM ("Replacing" :: String, _e0, deANFed) - -- modify $ \st -> - -- st { evNewEqualities = S.insert (eApps e0 es, eApps deANFed es) (evNewEqualities st) } - return (Just $ eApps deANFed _es, expand) + if dropECst deANFed /= dropECst _e0 then do + -- We need to elaborate the term on the fly as anf-ed terms arent elaborated + -- probably is not needed + deANFed' <- elaborateExpr "EvalApp deANFed elaborate" deANFed + return (Just $ eApps deANFed' _es, expand) else do - -- traceShowM ("evalApp: cant expand" :: String, pprint e0) - -- traceShowM ("evalApp: with args" :: String, es) - -- traceShowM ("sel" :: String, pprint (knSels γ)) - -- traceShowM ("ctors" :: String, pprint (knDataCtors γ)) return (Nothing, noExpand) -mkLams :: Expr -> [(Symbol, Sort)] -> Expr -mkLams subject binds = foldr ELam subject binds - -- | Evaluates if-then-else statements until they can't be evaluated anymore -- or some other expression is found. evalIte :: Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand) @@ -1443,6 +1445,12 @@ makeFreshEtaNames n = replicateM n makeFreshName modify $ \st -> st { freshEtaNames = 1 + freshEtaNames st } pure $ etaExpSymbol ident +elaborateExpr :: String -> Expr -> EvalST Expr +elaborateExpr msg e = do + let elabSpan = atLoc dummySpan msg + symEnv' <- gets evEnv + pure $ unApply $ elaborate elabSpan symEnv' e + -- | Returns False if there is a fuel count in the evaluation environment and -- the fuel count exceeds the maximum. Returns True otherwise. checkFuel :: Symbol -> EvalST Bool From 2f2514c7c7cfc2272b4e1c018dd49c3c0848b430 Mon Sep 17 00:00:00 2001 From: Alessio Ferrarini Date: Fri, 27 Sep 2024 09:32:25 +0200 Subject: [PATCH 5/7] Chore: hlint --- src/Language/Fixpoint/Solver/PLE.hs | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/Language/Fixpoint/Solver/PLE.hs b/src/Language/Fixpoint/Solver/PLE.hs index 6d3005f90..691dc9008 100644 --- a/src/Language/Fixpoint/Solver/PLE.hs +++ b/src/Language/Fixpoint/Solver/PLE.hs @@ -323,13 +323,12 @@ withAssms env@InstEnv{..} ctx delta cidMb act = do extractRewrites (_, sreft, _) | Reft (_, PAnd ra) <- sr_reft sreft - = concat - $ Mb.mapMaybe obtainEqualities - $ Mb.mapMaybe keepTrans - $ map snd - $ Misc.groupList - $ fmap (bimap unApply unApply) - $ Mb.mapMaybe keepPropEq ra + = concat + $ Mb.mapMaybe obtainEqualities + $ Mb.mapMaybe (keepTrans . snd) + $ Misc.groupList + $ bimap unApply unApply + <$> Mb.mapMaybe keepPropEq ra extractRewrites _ = [] keepPropEq (PAtom Eq e1 e2) = Just (e1, e2) @@ -339,9 +338,9 @@ withAssms env@InstEnv{..} ctx delta cidMb act = do keepTrans _ = Nothing -- Find a way to make this check more roboust - validVar name = (not $ T.elem '.' name') + validVar name = not (T.elem '.' name') && (T.elem '#' name' || T.elem '_' name') - && (not $ T.isPrefixOf "lq_anf" name') + && not (T.isPrefixOf "lq_anf" name') where name' = symbolText name -- | @ple1@ performs the PLE at a single "node" in the Trie From ccb6f0272ef82c82ee4dbf785c21b4b79ae8c0b7 Mon Sep 17 00:00:00 2001 From: Alessio Ferrarini Date: Fri, 27 Sep 2024 13:05:16 +0200 Subject: [PATCH 6/7] Fix: evalIte should look inside ECst --- src/Language/Fixpoint/Solver/PLE.hs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Language/Fixpoint/Solver/PLE.hs b/src/Language/Fixpoint/Solver/PLE.hs index 691dc9008..75c5d01d3 100644 --- a/src/Language/Fixpoint/Solver/PLE.hs +++ b/src/Language/Fixpoint/Solver/PLE.hs @@ -1090,6 +1090,9 @@ evalApp _γ _ctx _e0 _es _ -- | Evaluates if-then-else statements until they can't be evaluated anymore -- or some other expression is found. evalIte :: Knowledge -> ICtx -> EvalType -> Expr -> EvalST (Expr, FinalExpand) +evalIte γ ctx et (ECst e t) = do + (e', fe) <- evalIte γ ctx et e + return (ECst e' t, fe) evalIte γ ctx et (EIte i e1 e2) = do (b, _) <- eval γ ctx et False i b' <- mytracepp ("evalEIt POS " ++ showpp (i, b)) <$> isValidCached γ b From 7f3c46e11ba426077e081cbc3c9ceb81c0822b68 Mon Sep 17 00:00:00 2001 From: Alessio Ferrarini Date: Fri, 27 Sep 2024 16:31:20 +0200 Subject: [PATCH 7/7] Fix: coerce bind env --- src/Language/Fixpoint/Solver/PLE.hs | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/Language/Fixpoint/Solver/PLE.hs b/src/Language/Fixpoint/Solver/PLE.hs index 75c5d01d3..55e7f27d7 100644 --- a/src/Language/Fixpoint/Solver/PLE.hs +++ b/src/Language/Fixpoint/Solver/PLE.hs @@ -159,7 +159,7 @@ instEnv cfg info cs restSolver ctx = do return $ InstEnv { ieCfg = cfg , ieSMT = ctx - , ieBEnv = bs info + , ieBEnv = coerceBindEnv $ bs info , ieAenv = ae info , ieCstrs = cs , ieKnowl = knowledge cfg ctx info @@ -1080,10 +1080,7 @@ evalApp _γ _ctx _e0 _es _ = do let deANFed = deANF _ctx _e0 if dropECst deANFed /= dropECst _e0 then do - -- We need to elaborate the term on the fly as anf-ed terms arent elaborated - -- probably is not needed - deANFed' <- elaborateExpr "EvalApp deANFed elaborate" deANFed - return (Just $ eApps deANFed' _es, expand) + return (Just $ eApps deANFed _es, expand) else do return (Nothing, noExpand)