| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| 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 Bool
- 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 Bool Source #
Tries to prove an implication. If proved, then returns `Right (m_su ::
InferM Subst)` where m_su is an InferM computation that results in the
solution substitution, and records any warning invoked during proving. If not
proved, then returns `Left (m_err :: InferM ())`, which records all errors
invoked 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.