liquid-fixpoint- Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone




This module has the functions that perform sort-checking, and related operations on Fixpoint expressions and predicates.


Sort Substitutions

data TVSubst Source #

API for manipulating Sort Substitutions -----------------------------------


Checking Well-Formedness

checkSorted :: Checkable a => SEnv Sort -> a -> Maybe Doc Source #

checkSortedReft :: SEnv SortedReft -> [Symbol] -> SortedReft -> Maybe Doc Source #

Checking Refinements ------------------------------------------------------

checkSortedReftFull :: Checkable a => SEnv SortedReft -> a -> Maybe Doc Source #

checkSortFull :: Checkable a => SEnv SortedReft -> Sort -> a -> Maybe Doc Source #

Sort inference

sortExpr :: SrcSpan -> SEnv Sort -> Expr -> Sort Source #

Sort Inference ------------------------------------------------------------

exprSort :: String -> Expr -> Sort Source #

Expressions sort ---------------------------------------------------------


unifyFast :: Bool -> Env -> Sort -> Sort -> Maybe TVSubst Source #

Fast Unification; `unifyFast True` is just equality

Apply Substitution

apply :: TVSubst -> Sort -> Sort Source #

Applying a Type Substitution ----------------------------------------------

Exported Sorts

boolSort :: Sort Source #

Exported Basic Sorts -----------------------------------------------

strSort :: Sort Source #

Exported Basic Sorts -----------------------------------------------

Sort-Directed Transformations

class Elaborate a where Source #

Elaborate: make polymorphic instantiation explicit via casts, make applications monomorphic for SMTLIB. This deals with polymorphism by elaborate-ing all refinements except for KVars. THIS IS NOW MANDATORY as sort-variables can be instantiated to int and bool.

Minimal complete definition



elaborate :: String -> SymEnv -> a -> a Source #

applySorts :: Visitable t => t -> [Sort] Source #


Because SMTLIB does not support higher-order functions, all _non-theory_ function applications

EApp e1 e2

are represented, in SMTLIB, as

(Eapp (EApp apply e1) e2)

where apply is 'ECst (EVar "apply") t' and t is 'FFunc a b' a,b are the sorts of e2 and 'e1 e2' respectively.

Note that *all polymorphism* goes through this machinery.

Just before sending to the SMT solver, we use the cast t to generate a special apply_at_t symbol.

To let us do the above, we populate SymEnv with the _set_ of all sorts at which apply is used, computed by applySorts.

Predicates on Sorts

isMono :: Sort -> Bool Source #

Predicates on Sorts -------------------------------------------------------