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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.SortCheck

Contents

Description

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

Synopsis

Sort Substitutions

data TVSubst Source

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

Instances

type Env = Symbol -> SESearch Sort Source

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

pruneUnsortedReft :: SEnv Sort -> SortedReft -> SortedReft Source

Sort inference

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

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

checkSortExpr :: SEnv Sort -> Expr -> Maybe Sort Source

Unify

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

Fast Unification; `unifyFast True` is just equality

unify :: Env -> Sort -> Sort -> Maybe TVSubst Source

Sort Unification

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 -----------------------------------------------

elaborate :: SEnv Sort -> Expr -> Expr Source

Predicates on Sorts

isFirstOrder :: Sort -> Bool Source

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

isMono :: Sort -> Bool Source