| 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 ()
- defaultAndSimplify :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning], [Error])
- 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.