Safe Haskell | None |
---|---|
Language | Haskell98 |
This module has the functions that perform sort-checking, and related operations on Fixpoint expressions and predicates.
- data TVSubst
- type Env = Symbol -> SESearch Sort
- checkSorted :: Checkable a => SEnv Sort -> a -> Maybe Doc
- checkSortedReft :: SEnv SortedReft -> [Symbol] -> SortedReft -> Maybe Doc
- checkSortedReftFull :: Checkable a => SEnv SortedReft -> a -> Maybe Doc
- checkSortFull :: Checkable a => SEnv SortedReft -> Sort -> a -> Maybe Doc
- pruneUnsortedReft :: SEnv Sort -> SortedReft -> SortedReft
- sortExpr :: SrcSpan -> SEnv Sort -> Expr -> Sort
- checkSortExpr :: SEnv Sort -> Expr -> Maybe Sort
- exprSort :: String -> Expr -> Sort
- unifyFast :: Bool -> Env -> Sort -> Sort -> Maybe TVSubst
- unifySorts :: Sort -> Sort -> Maybe TVSubst
- apply :: TVSubst -> Sort -> Sort
- boolSort :: Sort
- strSort :: Sort
- class Elaborate a where
- isFirstOrder :: Sort -> Bool
- isMono :: Sort -> Bool
Sort Substitutions
API for manipulating Sort Substitutions -----------------------------------
Checking Well-Formedness
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 ------------------------------------------------------------
exprSort :: String -> Expr -> Sort Source #
Expressions sort ---------------------------------------------------------
Unify
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
Sort-Directed Transformations
Predicates on Sorts
isFirstOrder :: Sort -> Bool Source #