Copyright	(c) 2013-2016 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	Safe
Language	Haskell2010

Cryptol.TypeCheck.Infer

Description

Assumes that the NoPat pass has been run.

Synopsis

checkE :: Expr Name -> TypeWithSource -> InferM Expr
checkSigB :: Bind Name -> (Schema, [Goal]) -> InferM Decl
inferModule :: Module Name -> InferM Module
inferBinds :: Bool -> Bool -> [Bind Name] -> InferM [Decl]
inferDs :: FromDecl d => [d] -> ([DeclGroup] -> InferM a) -> InferM a

Documentation

checkE :: Expr Name -> TypeWithSource -> InferM Expr Source #

Infer the type of an expression, and translate it to a fully elaborated core term.

checkSigB :: Bind Name -> (Schema, [Goal]) -> InferM Decl Source #

inferModule :: Module Name -> InferM Module Source #

inferBinds :: Bool -> Bool -> [Bind Name] -> InferM [Decl] Source #

inferBinds isTopLevel isRec binds performs inference for a strongly-connected component of Binds. If any of the members of the recursive group are already marked as monomorphic, then we don't do generalization. If isTopLevel is true, any bindings without type signatures will be generalized. If it is false, and the mono-binds flag is enabled, no bindings without type signatures will be generalized, but bindings with signatures will be unaffected.

inferDs :: FromDecl d => [d] -> ([DeclGroup] -> InferM a) -> InferM a Source #