Language.Fixpoint.Solver.Solution

Solutions and Results

type Solution = Sol KBind

Types ----------------------------------------------------------

type Cand a = [(Pred, a)]

data EQual

Expanded or Instantiated Qualifier -----------------------------

Constructors

EQL

Fields

eqQual :: !Qualifier

eqPred :: !Pred

eqArgs :: ![Expr]

Instances

Eq EQual

Ord EQual

Show EQual

PPrint EQual

Solvable EQual

Types with Template/KVars

class Solvable a where

Apply Solution -------------------------------------------------

Methods

apply :: Solution -> a -> Pred

Instances

Solvable SortedReft

Solvable Reft

Solvable Refa

Solvable Pred

Solvable KVar

Solvable EQual

Solvable a => Solvable [a]

Solvable (Symbol, SortedReft)

Solvable (KVar, Subst)

Initial Solution

init :: Config -> FInfo a -> Solution

Initial Solution (from Qualifiers and WF constraints) ---------

Update Solution

update :: Solution -> [KVar] -> [(KVar, EQual)] -> (Bool, Solution)

Update Solution ---------------------------------------------------

Lookup Solution

lookup :: Solution -> KVar -> KBind