Language.Fixpoint.SortCheck

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

Sort Substitutions

data TVSubst

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

Instances

Show TVSubst

Methods

showsPrec :: Int -> TVSubst -> ShowS

show :: TVSubst -> String

showList :: [TVSubst] -> ShowS

type Env = Symbol -> SESearch Sort

Checking Well-Formedness

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

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

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

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

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

pruneUnsortedReft :: SEnv Sort -> SortedReft -> SortedReft

Sort inference

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

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

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

exprSort :: String -> Expr -> Sort

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

Unify

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

Fast Unification; `unifyFast True` is just equality

unifySorts :: Sort -> Sort -> Maybe TVSubst

Apply Substitution

apply :: TVSubst -> Sort -> Sort

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

Exported Sorts

boolSort :: Sort

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

strSort :: Sort

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

Sort-Directed Transformations

class Elaborate a where

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

Methods

elaborate :: String -> SEnv Sort -> a -> a

Instances

Elaborate Sort

Methods

elaborate :: String -> SEnv Sort -> Sort -> Sort

Elaborate SortedReft

Methods

elaborate :: String -> SEnv Sort -> SortedReft -> SortedReft

Elaborate Expr

Methods

elaborate :: String -> SEnv Sort -> Expr -> Expr

Elaborate BindEnv

Methods

elaborate :: String -> SEnv Sort -> BindEnv -> BindEnv

Elaborate a => Elaborate [a]

Methods

elaborate :: String -> SEnv Sort -> [a] -> [a]

Elaborate e => Elaborate (Triggered e)

Methods

elaborate :: String -> SEnv Sort -> Triggered e -> Triggered e

Elaborate (SInfo a)

Methods

elaborate :: String -> SEnv Sort -> SInfo a -> SInfo a

Elaborate (SimpC a)

Methods

elaborate :: String -> SEnv Sort -> SimpC a -> SimpC a

Elaborate (Symbol, Sort)

Methods

elaborate :: String -> SEnv Sort -> (Symbol, Sort) -> (Symbol, Sort)

Predicates on Sorts

isFirstOrder :: Sort -> Bool

isMono :: Sort -> Bool

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