Copyright | (c) 2013-2016 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell98 |
Assumes that the NoPat
pass has been run.
- inferModule :: Module Name -> InferM Module
- mkPrim :: String -> InferM (Expr Name)
- desugarLiteral :: Bool -> Literal -> InferM (Expr Name)
- appTys :: Expr Name -> [Located (Maybe Ident, Type)] -> Type -> InferM Expr
- inferTyParam :: TypeInst Name -> InferM (Located (Maybe Ident, Type))
- checkTypeOfKind :: Type Name -> Kind -> InferM Type
- inferE :: Doc -> Expr Name -> InferM (Expr, Type)
- checkE :: Expr Name -> Type -> InferM Expr
- expectSeq :: Type -> InferM (Type, Type)
- expectTuple :: Int -> Type -> InferM [Type]
- expectRec :: [Named a] -> Type -> InferM [(Ident, a, Type)]
- expectFin :: Int -> Type -> InferM ()
- expectFun :: Int -> Type -> InferM ([Type], Type)
- checkHasType :: Type -> Type -> InferM ()
- checkFun :: Doc -> [Pattern Name] -> Expr Name -> Type -> InferM Expr
- smallest :: [Type] -> InferM Type
- checkP :: Doc -> Pattern Name -> Type -> InferM (Located Name)
- inferP :: Doc -> Pattern Name -> InferM (Name, Located Type)
- inferMatch :: Match Name -> InferM (Match, Name, Located Type, Type)
- inferCArm :: Int -> [Match Name] -> InferM ([Match], Map Name (Located Type), Type)
- inferBinds :: Bool -> Bool -> [Bind Name] -> InferM [Decl]
- guessType :: Map Name Expr -> Bind Name -> InferM ((Name, VarType), Either (InferM Decl) (InferM Decl))
- generalize :: [Decl] -> [Goal] -> InferM [Decl]
- checkMonoB :: Bind Name -> Type -> InferM Decl
- checkSigB :: Bind Name -> (Schema, [Goal]) -> InferM Decl
- inferDs :: FromDecl d => [d] -> ([DeclGroup] -> InferM a) -> InferM a
- tcPanic :: String -> [String] -> a
Documentation
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.
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 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 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.