cryptol-2.2.6: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2015 Galois, Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe
Language | Haskell98

Cryptol.TypeCheck.Infer

Description

Assumes that the `NoPat` pass has been run.

Synopsis

- inferModule :: Module -> InferM Module
- desugarLiteral :: Bool -> Literal -> InferM Expr
- appTys :: Expr -> [Located (Maybe QName, Type)] -> Type -> InferM Expr
- inferTyParam :: TypeInst -> InferM (Located (Maybe QName, Type))
- checkTypeOfKind :: Type -> Kind -> InferM Type
- inferE :: Doc -> Expr -> InferM (Expr, Type)
- checkE :: Expr -> Type -> InferM Expr
- expectSeq :: Type -> InferM (Type, Type)
- expectTuple :: Int -> Type -> InferM [Type]
- expectRec :: [Named a] -> Type -> InferM [(Name, a, Type)]
- expectFin :: Int -> Type -> InferM ()
- expectFun :: Int -> Type -> InferM ([Type], Type)
- checkHasType :: Expr -> Type -> Type -> InferM Expr
- checkFun :: Doc -> [Pattern] -> Expr -> Type -> InferM Expr
- smallest :: [Type] -> InferM Type
- checkP :: Doc -> Pattern -> Type -> InferM (Located QName)
- inferP :: Doc -> Pattern -> InferM (QName, Located Type)
- inferMatch :: Match -> InferM (Match, QName, Located Type, Type)
- inferCArm :: Int -> [Match] -> InferM ([Match], Map QName (Located Type), Type)
- inferBinds :: Bool -> Bool -> [Bind] -> InferM [Decl]
- guessType :: Map QName Expr -> Bind -> InferM ((QName, VarType), Either (InferM Decl) (InferM Decl))
- simpMonoBind :: OrdFacts -> Decl -> Decl
- generalize :: [Decl] -> [Goal] -> InferM [Decl]
- checkMonoB :: Bind -> Type -> InferM Decl
- checkSigB :: Bind -> (Schema, [Goal]) -> InferM Decl
- inferDs :: FromDecl d => [d] -> ([DeclGroup] -> InferM a) -> InferM a
- tcPanic :: String -> [String] -> a

# Documentation

inferModule :: Module -> InferM Module Source

desugarLiteral :: Bool -> Literal -> InferM Expr Source

appTys :: Expr -> [Located (Maybe QName, Type)] -> Type -> InferM Expr Source

Infer the type of an expression with an explicit instantiation.

inferTyParam :: TypeInst -> InferM (Located (Maybe QName, Type)) Source

checkTypeOfKind :: Type -> Kind -> InferM Type Source

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

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

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

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

expectSeq :: Type -> InferM (Type, Type) Source

expectTuple :: Int -> Type -> InferM [Type] Source

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

expectFin :: Int -> Type -> InferM () Source

expectFun :: Int -> Type -> InferM ([Type], Type) Source

checkHasType :: Expr -> Type -> Type -> InferM Expr Source

checkFun :: Doc -> [Pattern] -> Expr -> Type -> InferM Expr Source

smallest :: [Type] -> InferM Type Source

The type the is the smallest of all

checkP :: Doc -> Pattern -> Type -> InferM (Located QName) Source

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

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

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

Infer the type of one match in a list comprehension.

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

Infer the type of one arm of a list comprehension.

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

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

simpMonoBind :: OrdFacts -> Decl -> Decl Source

Try to evaluate the inferred type of a mono-binding

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

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

checkMonoB :: Bind -> Type -> InferM Decl Source

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

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

tcPanic :: String -> [String] -> a Source