cryptol-2.4.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 | Haskell98

Cryptol.TypeCheck.Solve

Description

Synopsis

- simplifyAllConstraints :: InferM ()
- proveImplication :: Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
- wfType :: Type -> [Prop]
- wfTypeFunction :: TFun -> [Type] -> [Prop]
- improveByDefaultingWith :: Solver -> [TVar] -> [Goal] -> IO ([TVar], [Goal], Subst, [Warning])
- defaultReplExpr :: Solver -> Expr -> Schema -> IO (Maybe ([(TParam, Type)], Expr))
- simpType :: Type -> Type
- simpTypeMaybe :: Type -> Maybe Type

# Documentation

simplifyAllConstraints :: InferM () Source #

proveImplication :: Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst Source #

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.

improveByDefaultingWith :: Solver -> [TVar] -> [Goal] -> IO ([TVar], [Goal], Subst, [Warning]) Source #

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

Try to pick a reasonable instantiation for an expression, with the given type. This is useful when we do evaluation at the REPL. The resulting types should satisfy the constraints of the schema.

simpType :: Type -> Type Source #

simpTypeMaybe :: Type -> Maybe Type Source #