cryptol-2.6.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
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.

wfType :: Type -> [Prop] Source #

Add additional constraints that ensure the validity of a type.

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.

wfTC :: TC -> [Type] -> [Prop] Source #

Add additional constraints that ensure validity of a type constructor application. Note that the constraints do not use any partial type functions, so the new constraints are guaranteed to be well-formed. This assumes that the parameters are well-formed.

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

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