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.Infer

Description

Assumes that the `NoPat` pass has been run.

Synopsis

- checkE :: Expr Name -> TypeWithSource -> InferM Expr
- checkSigB :: Bind Name -> (Schema, [Goal]) -> InferM Decl
- inferTopModule :: Module Name -> InferM TCTopEntity
- inferBinds :: Bool -> Bool -> [Bind Name] -> InferM [Decl]
- checkTopDecls :: [TopDecl Name] -> InferM ()

# 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 #

inferTopModule :: Module Name -> InferM TCTopEntity Source #

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

`inferBinds isTopLevel isRec binds` performs inference for a strongly-connected component of `Bind`s. 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.

checkTopDecls :: [TopDecl Name] -> InferM () Source #