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
- applySorts :: Visitable t => t -> [Sort]
- unApplyAt :: Expr -> Maybe Sort
- toInt :: SymEnv -> Expr -> Sort -> Expr
- 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
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
.
Elaborate Sort Source # | |
Elaborate SortedReft Source # | |
Elaborate Expr Source # | |
Elaborate BindEnv Source # | |
Elaborate a => Elaborate [a] Source # | |
Elaborate a => Elaborate (Maybe a) Source # | |
Elaborate e => Elaborate (Triggered e) Source # | |
Elaborate (SInfo a) Source # | |
Elaborate (SimpC a) Source # | |
Elaborate (Symbol, Sort) Source # | |
applySorts :: Visitable t => t -> [Sort] Source #
- NOTE:apply-monomorphization
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' andt
is 'FFunc a b'a
,b
are the sorts ofe2
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 specialapply_at_t
symbol.To let us do the above, we populate
SymEnv
with the _set_ of all sorts at whichapply
is used, computed byapplySorts
.
Predicates on Sorts
isFirstOrder :: Sort -> Bool Source #