| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | [email protected] |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Cryptol.TypeCheck.Solve
Description
Synopsis
- simplifyAllConstraints :: InferM ()
- proveImplication :: Bool -> Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
- tryProveImplication :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM (Either [Error] [Warning])
- proveModuleTopLevel :: InferM ()
- defaultAndSimplify :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning], [Error])
- defaultReplExpr :: Solver -> Expr -> Schema -> IO (Maybe ([(TParam, Type)], Expr))
Documentation
simplifyAllConstraints :: InferM () Source #
proveImplication :: Bool -> 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.
tryProveImplication :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM (Either [Error] [Warning]) Source #
Tries to prove an implication. If proved, then returns a (possibly-empty) list of warnings raised during proving. If not proved, then returns `Left errs`, which records all errors raised during proving.
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.