Safe Haskell	Safe-Inferred
Language	Haskell98

Language.Fixpoint.Solver.PLE

Description

This module implements "Proof by Logical Evaluation" where we unfold function definitions if they *must* be unfolded, to strengthen the environments with function-definition-equalities. The algorithm is discussed at length in:

"Refinement Reflection", POPL 2018, https://arxiv.org/pdf/1711.03842
"Reasoning about Functions", VMCAI 2018, https://ranjitjhala.github.io/static/reasoning-about-functions.pdf

Synopsis

instantiate :: Loc a => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
data FuelCount = FC {
- fcMap :: HashMap Symbol Int
- fcMax :: Maybe Int
}
data ICtx = ICtx {
- icAssms :: HashSet Pred
- icCands :: HashSet Expr
- icEquals :: EvEqualities
- icSimpl :: !ConstMap
- icSubcId :: Maybe SubcId
- icANFs :: [[(Symbol, SortedReft)]]
}
data Knowledge = KN {
- knSims :: Map Symbol [(Rewrite, IsUserDataSMeasure)]
- knAms :: Map Symbol Equation
- knContext :: Context
- knPreds :: Context -> [(Symbol, Sort)] -> Expr -> IO Bool
- knLams :: ![(Symbol, Sort)]
- knSummary :: ![(Symbol, Int)]
- knDCs :: !(HashSet Symbol)
- knDataCtors :: !(HashMap Symbol DataCtor)
- knSels :: !SelectorMap
- knConsts :: !ConstDCMap
- knAutoRWs :: HashMap SubcId [AutoRewrite]
- knRWTerminationOpts :: RWTerminationOpts
}
simplify :: Knowledge -> ICtx -> Expr -> Expr

Documentation

instantiate :: Loc a => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a) Source #

Strengthen Constraint Environments via PLE

data FuelCount Source #

Constructors

FC
Fields fcMap :: HashMap Symbol Int fcMax :: Maybe Int

Instances

Instances details

Show FuelCount Source #
Instance details Defined in Language.Fixpoint.Solver.PLE Methods showsPrec :: Int -> FuelCount -> ShowS # show :: FuelCount -> String # showList :: [FuelCount] -> ShowS #

data ICtx Source #

ICtx is the local information -- at each trie node -- obtained by incremental PLE

Constructors

ICtx
Fields icAssms :: HashSet Pred Equalities converted to SMT format icCands :: 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)]]

data Knowledge Source #

Knowledge (SMT Interaction)

Constructors

KN

Fields

knSims :: Map Symbol [(Rewrite, IsUserDataSMeasure)]
Rewrites rules came from match definitions
They are grouped by the data constructor that they unfold, and are augmented with an attribute that say whether they originate from a user data declaration.
knAms :: Map Symbol Equation
All function definitions
knContext :: Context
knPreds :: Context -> [(Symbol, Sort)] -> Expr -> IO Bool
knLams :: ![(Symbol, Sort)]
knSummary :: ![(Symbol, Int)]
summary of functions to be evaluates (knSims and knAsms) with their arity
knDCs :: !(HashSet Symbol)
data constructors drawn from Rewrite
knDataCtors :: !(HashMap Symbol DataCtor)
data constructors by name
knSels :: !SelectorMap
knConsts :: !ConstDCMap
knAutoRWs :: HashMap SubcId [AutoRewrite]
knRWTerminationOpts :: RWTerminationOpts

simplify :: Knowledge -> ICtx -> Expr -> Expr Source #