Safe Haskell	Safe-Inferred
Language	Haskell98

Language.Fixpoint.Solver.Interpreter

Description

This module is a preliminary part of the implementation of "Proof by Logical Evaluation" where we unfold function definitions if they *must* be unfolded, to strengthen the environments with function-definition-equalities.

In this module, we attempt to verify as many of the PLE constaints as possible without invoking the SMT solver or performing any I/O at all. To this end, we use an interpreter in Haskell to attempt to evaluate down expressions and generate equalities.

Synopsis

instInterpreter :: Loc a => Config -> SInfo a -> Maybe [SubcId] -> IO (SInfo a)
data ICtx = ICtx {
- icCands :: HashSet Expr
- icEquals :: EvAccum
- icSolved :: HashSet Expr
- icSimpl :: !ConstMap
- icSubcId :: Maybe SubcId
}
data Knowledge = KN {
- knSims :: HashMap (Symbol, Symbol) Rewrite
- knAms :: HashMap Symbol Equation
- knLams :: ![(Symbol, Sort)]
- knSummary :: ![(Symbol, Int)]
- knDCs :: !(HashSet Symbol)
- knAllDCs :: !(HashSet Symbol)
- knSels :: !SelectorMap
- knConsts :: !ConstDCMap
}
class Simplifiable a where
- simplify :: Knowledge -> ICtx -> a -> a
interpret :: ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr

Documentation

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

Strengthen Constraint Environments via PLE

data ICtx Source #

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

Constructors

ICtx
Fields icCands :: HashSet Expr Candidates for unfolding icEquals :: EvAccum Accumulated equalities icSolved :: HashSet Expr Terms that we have already expanded icSimpl :: !ConstMap Map of expressions to constants icSubcId :: Maybe SubcId Current subconstraint ID

data Knowledge Source #

Knowledge (SMT Interaction)

Constructors

KN

Fields

knSims :: HashMap (Symbol, Symbol) Rewrite
Rewrite rules came from match and data type definitions
knAms :: HashMap Symbol Equation
All function definitions -- restore ! here?
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
knAllDCs :: !(HashSet Symbol)
knSels :: !SelectorMap
knConsts :: !ConstDCMap

class Simplifiable a where Source #

Methods

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

Instances

Instances details

Simplifiable Expr Source #
Instance details Defined in Language.Fixpoint.Solver.Interpreter Methods simplify :: Knowledge -> ICtx -> Expr -> Expr Source #

interpret :: ConstMap -> Knowledge -> ICtx -> SEnv Sort -> Expr -> Expr Source #