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

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Sort

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

Checking Well-Formedness

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

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

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

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

Unify

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

Unification of Sorts

Apply Substitution

apply :: TVSubst -> Sort -> Sort Source

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