Language.Fixpoint.Solver.Interpreter

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.

Documentation

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

Strengthen Constraint Environments via PLE

data ICtx

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

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

Methods

simplify :: Knowledge -> ICtx -> a -> a

Instances

Simplifiable Expr

Defined in Language.Fixpoint.Solver.Interpreter

Methods

simplify :: Knowledge -> ICtx -> Expr -> Expr

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