| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe |
| Language | Haskell2010 |
Cryptol.TypeCheck.Solve
Description
Synopsis
- simplifyAllConstraints :: InferM ()
- proveImplication :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
- proveModuleTopLevel :: InferM ()
- wfType :: Type -> [Prop]
- wfTypeFunction :: TFun -> [Type] -> [Prop]
- wfTC :: TC -> [Type] -> [Prop]
- defaultAndSimplify :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning])
- defaultReplExpr :: Solver -> Expr -> Schema -> IO (Maybe ([(TParam, Type)], Expr))
Documentation
simplifyAllConstraints :: InferM () Source #
proveImplication :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst Source #
Prove an implication, and return any improvements that we computed. Records errors, if any of the goals couldn't be solved.
proveModuleTopLevel :: InferM () Source #
Try to clean-up any left-over constraints after we've checked everything in a module. Typically these are either trivial things, or constraints on the module's type parameters.
wfTypeFunction :: TFun -> [Type] -> [Prop] Source #
Add additional constraints that ensure validity of type function. Note that these constraints do not introduce additional malformed types, so the well-formedness constraints are guaranteed to be well-formed. This assumes that the parameters are well-formed.