cryptol-2.4.0: Cryptol: The Language of Cryptography

Copyright(c) 2013-2016 Galois, Inc.
Safe HaskellSafe



Assumes that the NoPat pass has been run.



mkPrim :: String -> InferM (Expr Name) Source #

Construct a primitive in the parsed AST.

appTys :: Expr Name -> [Located (Maybe Ident, Type)] -> Type -> InferM Expr Source #

Infer the type of an expression with an explicit instantiation.

inferE :: Doc -> Expr Name -> InferM (Expr, Type) Source #

We use this when we want to ensure that the expr has exactly (syntactically) the given type.

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

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

expectRec :: [Named a] -> Type -> InferM [(Ident, a, Type)] Source #

smallest :: [Type] -> InferM Type Source #

The type the is the smallest of all

inferP :: Doc -> Pattern Name -> InferM (Name, Located Type) Source #

Infer the type of a pattern. Assumes that the pattern will be just a variable.

inferMatch :: Match Name -> InferM (Match, Name, Located Type, Type) Source #

Infer the type of one match in a list comprehension.

inferCArm :: Int -> [Match Name] -> InferM ([Match], Map Name (Located Type), Type) Source #

Infer the type of one arm of a list comprehension.

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

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

guessType :: Map Name Expr -> Bind Name -> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl)) Source #

Come up with a type for recursive calls to a function, and decide how we are going to be checking the binding. Returns: (Name, type or schema, computation to check binding)

The exprMap is a thunk where we can lookup the final expressions and we should be careful not to force it.

simpBind :: Decl -> Decl Source #

Try to evaluate the inferred type in a binding.

generalize :: [Decl] -> [Goal] -> InferM [Decl] Source #

The inputs should be declarations with monomorphic types (i.e., of the form `Forall [] [] t`).

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