cryptol-3.0.0: Cryptol: The Language of Cryptography

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.

defaultAndSimplify :: [TVar] -> [Goal] -> ([TVar], [Goal], Subst, [Warning], [Error]) Source #

defaultReplExpr :: Solver -> Expr -> Schema -> IO (Maybe ([(TParam, Type)], Expr)) Source #