liquid-fixpoint 0.8.10.1 → 0.8.10.2
raw patch · 2 files changed
+20/−9 lines, 2 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- Language.Fixpoint.Defunctionalize: instance (Language.Fixpoint.Defunctionalize.Defunc a, GHC.Classes.Eq k, Data.Hashable.Class.Hashable k) => Language.Fixpoint.Defunctionalize.Defunc (Data.HashMap.Base.HashMap k a)
- Language.Fixpoint.Horn.Transformations: instance GHC.Base.Functor ((,,) a b)
- Language.Fixpoint.Solver.Extensionality: instance Language.Fixpoint.Solver.Extensionality.Extend a => Language.Fixpoint.Solver.Extensionality.Extend (Data.HashMap.Base.HashMap Language.Fixpoint.Types.Constraints.SubcId a)
- Language.Fixpoint.Types.Constraints: instance Language.Fixpoint.Types.PrettyPrint.Fixpoint (Data.HashMap.Base.HashMap Language.Fixpoint.Types.Constraints.SubcId [Language.Fixpoint.Types.Constraints.AutoRewrite])
- Language.Fixpoint.Types.Environments: instance (Data.Hashable.Class.Hashable a, GHC.Classes.Eq a, Data.Binary.Class.Binary a) => Data.Binary.Class.Binary (Data.HashSet.Base.HashSet a)
- Language.Fixpoint.Types.Graduals: instance Language.Fixpoint.Types.Graduals.Gradual v => Language.Fixpoint.Types.Graduals.Gradual (Data.HashMap.Base.HashMap k v)
- Language.Fixpoint.Types.Graduals: instance Language.Fixpoint.Types.Graduals.Unique a => Language.Fixpoint.Types.Graduals.Unique (Data.HashMap.Base.HashMap Language.Fixpoint.Types.Constraints.SubcId a)
- Language.Fixpoint.Types.PrettyPrint: instance (GHC.Classes.Ord a, Data.Hashable.Class.Hashable a, Language.Fixpoint.Types.PrettyPrint.Fixpoint a) => Language.Fixpoint.Types.PrettyPrint.Fixpoint (Data.HashSet.Base.HashSet a)
- Language.Fixpoint.Types.PrettyPrint: instance (Language.Fixpoint.Types.PrettyPrint.PPrint a, Language.Fixpoint.Types.PrettyPrint.PPrint b) => Language.Fixpoint.Types.PrettyPrint.PPrint (Data.HashMap.Base.HashMap a b)
- Language.Fixpoint.Types.PrettyPrint: instance Language.Fixpoint.Types.PrettyPrint.PPrint a => Language.Fixpoint.Types.PrettyPrint.PPrint (Data.HashSet.Base.HashSet a)
- Language.Fixpoint.Types.Refinements: instance (Data.Hashable.Class.Hashable k, GHC.Classes.Eq k, Data.Binary.Class.Binary k, Data.Binary.Class.Binary v) => Data.Binary.Class.Binary (Data.HashMap.Base.HashMap k v)
- Language.Fixpoint.Types.Refinements: pattern EEq :: () => () => Expr -> Expr -> Expr
- Language.Fixpoint.Types.Substitutions: instance Language.Fixpoint.Types.Refinements.Subable a => Language.Fixpoint.Types.Refinements.Subable (Data.HashMap.Base.HashMap k a)
+ Language.Fixpoint.Defunctionalize: instance (Language.Fixpoint.Defunctionalize.Defunc a, GHC.Classes.Eq k, Data.Hashable.Class.Hashable k) => Language.Fixpoint.Defunctionalize.Defunc (Data.HashMap.Internal.HashMap k a)
+ Language.Fixpoint.Solver.Extensionality: instance Language.Fixpoint.Solver.Extensionality.Extend a => Language.Fixpoint.Solver.Extensionality.Extend (Data.HashMap.Internal.HashMap Language.Fixpoint.Types.Constraints.SubcId a)
+ Language.Fixpoint.Types.Constraints: instance Language.Fixpoint.Types.PrettyPrint.Fixpoint (Data.HashMap.Internal.HashMap Language.Fixpoint.Types.Constraints.SubcId [Language.Fixpoint.Types.Constraints.AutoRewrite])
+ Language.Fixpoint.Types.Environments: instance (Data.Hashable.Class.Hashable a, GHC.Classes.Eq a, Data.Binary.Class.Binary a) => Data.Binary.Class.Binary (Data.HashSet.Internal.HashSet a)
+ Language.Fixpoint.Types.Graduals: instance Language.Fixpoint.Types.Graduals.Gradual v => Language.Fixpoint.Types.Graduals.Gradual (Data.HashMap.Internal.HashMap k v)
+ Language.Fixpoint.Types.Graduals: instance Language.Fixpoint.Types.Graduals.Unique a => Language.Fixpoint.Types.Graduals.Unique (Data.HashMap.Internal.HashMap Language.Fixpoint.Types.Constraints.SubcId a)
+ Language.Fixpoint.Types.PrettyPrint: instance (GHC.Classes.Ord a, Data.Hashable.Class.Hashable a, Language.Fixpoint.Types.PrettyPrint.Fixpoint a) => Language.Fixpoint.Types.PrettyPrint.Fixpoint (Data.HashSet.Internal.HashSet a)
+ Language.Fixpoint.Types.PrettyPrint: instance (Language.Fixpoint.Types.PrettyPrint.PPrint a, Language.Fixpoint.Types.PrettyPrint.PPrint b) => Language.Fixpoint.Types.PrettyPrint.PPrint (Data.HashMap.Internal.HashMap a b)
+ Language.Fixpoint.Types.PrettyPrint: instance Language.Fixpoint.Types.PrettyPrint.PPrint a => Language.Fixpoint.Types.PrettyPrint.PPrint (Data.HashSet.Internal.HashSet a)
+ Language.Fixpoint.Types.Refinements: instance (Data.Hashable.Class.Hashable k, GHC.Classes.Eq k, Data.Binary.Class.Binary k, Data.Binary.Class.Binary v) => Data.Binary.Class.Binary (Data.HashMap.Internal.HashMap k v)
+ Language.Fixpoint.Types.Refinements: pattern EBot :: Expr
+ Language.Fixpoint.Types.Refinements: pattern EDiv :: Expr -> Expr -> Expr
+ Language.Fixpoint.Types.Refinements: pattern EEq :: Expr -> Expr -> Expr
+ Language.Fixpoint.Types.Refinements: pattern ERDiv :: Expr -> Expr -> Expr
+ Language.Fixpoint.Types.Refinements: pattern ERTimes :: Expr -> Expr -> Expr
+ Language.Fixpoint.Types.Refinements: pattern ETimes :: Expr -> Expr -> Expr
+ Language.Fixpoint.Types.Refinements: pattern PFalse :: Expr
+ Language.Fixpoint.Types.Refinements: pattern PTop :: Expr
+ Language.Fixpoint.Types.Refinements: pattern PTrue :: Expr
+ Language.Fixpoint.Types.Substitutions: instance Language.Fixpoint.Types.Refinements.Subable a => Language.Fixpoint.Types.Refinements.Subable (Data.HashMap.Internal.HashMap k a)
- Language.Fixpoint.Graph.Types: lookupCMap :: ?callStack :: CallStack => CMap a -> SubcId -> a
+ Language.Fixpoint.Graph.Types: lookupCMap :: (?callStack :: CallStack) => CMap a -> SubcId -> a
- Language.Fixpoint.Misc: errorstar :: ?callStack :: CallStack => String -> a
+ Language.Fixpoint.Misc: errorstar :: (?callStack :: CallStack) => String -> a
- Language.Fixpoint.Misc: mfromJust :: ?callStack :: CallStack => String -> Maybe a -> a
+ Language.Fixpoint.Misc: mfromJust :: (?callStack :: CallStack) => String -> Maybe a -> a
- Language.Fixpoint.Misc: safeHead :: ?callStack :: CallStack => String -> ListNE a -> a
+ Language.Fixpoint.Misc: safeHead :: (?callStack :: CallStack) => String -> ListNE a -> a
- Language.Fixpoint.Misc: safeInit :: ?callStack :: CallStack => String -> ListNE a -> [a]
+ Language.Fixpoint.Misc: safeInit :: (?callStack :: CallStack) => String -> ListNE a -> [a]
- Language.Fixpoint.Misc: safeLast :: ?callStack :: CallStack => String -> ListNE a -> a
+ Language.Fixpoint.Misc: safeLast :: (?callStack :: CallStack) => String -> ListNE a -> a
- Language.Fixpoint.Misc: safeUncons :: ?callStack :: CallStack => String -> ListNE a -> (a, [a])
+ Language.Fixpoint.Misc: safeUncons :: (?callStack :: CallStack) => String -> ListNE a -> (a, [a])
- Language.Fixpoint.Misc: safeUnsnoc :: ?callStack :: CallStack => String -> ListNE a -> ([a], a)
+ Language.Fixpoint.Misc: safeUnsnoc :: (?callStack :: CallStack) => String -> ListNE a -> ([a], a)
- Language.Fixpoint.Misc: safeZip :: ?callStack :: CallStack => String -> [a] -> [b] -> [(a, b)]
+ Language.Fixpoint.Misc: safeZip :: (?callStack :: CallStack) => String -> [a] -> [b] -> [(a, b)]
- Language.Fixpoint.Misc: safeZipWith :: ?callStack :: CallStack => String -> (a -> b -> c) -> [a] -> [b] -> [c]
+ Language.Fixpoint.Misc: safeZipWith :: (?callStack :: CallStack) => String -> (a -> b -> c) -> [a] -> [b] -> [c]
- Text.PrettyPrint.HughesPJ.Compat: fullRender :: () => Mode -> Int -> Float -> (TextDetails -> a -> a) -> a -> Doc -> a
+ Text.PrettyPrint.HughesPJ.Compat: fullRender :: Mode -> Int -> Float -> (TextDetails -> a -> a) -> a -> Doc -> a
Files
liquid-fixpoint.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.4 name: liquid-fixpoint-version: 0.8.10.1+version: 0.8.10.2 synopsis: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver description: This package implements an SMTLIB based Horn-Clause\/Logical Implication constraint@@ -21,7 +21,7 @@ copyright: 2010-17 Ranjit Jhala, University of California, San Diego. author: Ranjit Jhala, Niki Vazou, Eric Seidel maintainer: jhala@cs.ucsd.edu-tested-with: GHC == 7.10.3, GHC == 8.0.1, GHC == 8.4.3, GHC == 8.6.4+tested-with: GHC == 7.10.3, GHC == 8.0.1, GHC == 8.4.3, GHC == 8.6.4, GHC == 8.10.1 category: Language homepage: https://github.com/ucsd-progsys/liquid-fixpoint build-type: Simple
src/Language/Fixpoint/Solver/PLE.hs view
@@ -409,7 +409,7 @@ go (ECoerc s t e) = ECoerc s t <$> go e go e@(EApp _ _) = case splitEApp e of (f, es) -> do (f':es') <- mapM (fastEval γ ctx) (f:es) - evalApp γ (eApps f' es) (f',es')+ evalApp γ ctx (eApps f' es) (f',es') go e@(PAtom r e1 e2) = fromMaybeM (PAtom r <$> go e1 <*> go e2) (evalBool γ e) go (ENeg e) = do e' <- fastEval γ ctx e return $ ENeg e'@@ -479,7 +479,7 @@ es' <- mapM (evalStep γ ctx) es if es /= es' then return (eApps f' es')- else evalApp γ (eApps f' es') (f',es')+ else evalApp γ ctx (eApps f' es') (f',es') evalStep γ ctx e@(PAtom r e1 e2) = fromMaybeM (PAtom r <$> evalStep γ ctx e1 <*> evalStep γ ctx e2) (evalBool γ e) evalStep γ ctx (ENeg e) = ENeg <$> evalStep γ ctx e@@ -510,21 +510,32 @@ -evalApp :: Knowledge -> Expr -> (Expr, [Expr]) -> EvalST Expr-evalApp γ _ (EVar f, es) +evalApp :: Knowledge -> ICtx -> Expr -> (Expr, [Expr]) -> EvalST Expr+evalApp γ ctx _ (EVar f, es) | Just eq <- L.find ((== f) . eqName) (knAms γ) , length (eqArgs eq) <= length es = do env <- seSort <$> gets evEnv let (es1,es2) = splitAt (length (eqArgs eq)) es- return $ eApps (substEq env eq es1) es2 + shortcut (substEq env eq es1) es2+ where+ shortcut (EIte i e1 e2) es2 = do+ b <- fastEval γ ctx i+ b' <- liftIO $ (mytracepp ("evalEIt POS " ++ showpp b) <$> isValid γ b)+ nb' <- liftIO $ (mytracepp ("evalEIt NEG " ++ showpp (PNot b)) <$> isValid γ (PNot b))+ r <- if b' + then shortcut e1 es2+ else if nb' then shortcut e2 es2+ else return $ eApps (EIte b e1 e2) es2+ return r+ shortcut e' es2 = return $ eApps e' es2 -evalApp γ _ (EVar f, e:es) +evalApp γ _ _ (EVar f, e:es) | (EVar dc, as) <- splitEApp e , Just rw <- L.find (\rw -> smName rw == f && smDC rw == dc) (knSims γ) , length as == length (smArgs rw) = return $ eApps (subst (mkSubst $ zip (smArgs rw) as) (smBody rw)) es -evalApp _ e _+evalApp _ _ e _ = return e --------------------------------------------------------------------------------