| Copyright | (c) 2013-2016 Galois Inc. |
|---|---|
| License | BSD3 |
| Maintainer | cryptol@galois.com |
| Stability | provisional |
| Portability | portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Cryptol.TypeCheck
Description
Synopsis
- tcModule :: Module Name -> InferInput -> IO (InferOutput Module)
- tcModuleInst :: IORef NamingEnv -> Module -> Module Name -> InferInput -> IO (InferOutput Module)
- tcExpr :: Expr Name -> InferInput -> IO (InferOutput (Expr, Schema))
- tcDecls :: [TopDecl Name] -> InferInput -> IO (InferOutput ([DeclGroup], Map Name TySyn))
- data InferInput = InferInput {
- inpRange :: Range
- inpVars :: Map Name Schema
- inpTSyns :: Map Name TySyn
- inpNewtypes :: Map Name Newtype
- inpAbstractTypes :: Map Name AbstractType
- inpParamTypes :: !(Map Name ModTParam)
- inpParamConstraints :: ![Located Prop]
- inpParamFuns :: !(Map Name ModVParam)
- inpNameSeeds :: NameSeeds
- inpMonoBinds :: Bool
- inpCallStacks :: Bool
- inpSearchPath :: [FilePath]
- inpPrimNames :: !PrimMap
- inpSupply :: !Supply
- inpSolver :: Solver
- data InferOutput a
- data SolverConfig = SolverConfig {
- solverPath :: FilePath
- solverArgs :: [String]
- solverVerbose :: Int
- solverPreludePath :: [FilePath]
- defaultSolverConfig :: [FilePath] -> SolverConfig
- data NameSeeds
- nameSeeds :: NameSeeds
- data Error
- = KindMismatch (Maybe TypeSource) Kind Kind
- | TooManyTypeParams Int Kind
- | TyVarWithParams
- | TooManyTySynParams Name Int
- | TooFewTyParams Name Int
- | RecursiveTypeDecls [Name]
- | TypeMismatch TypeSource Path Type Type
- | RecursiveType TypeSource Path Type Type
- | UnsolvedGoals [Goal]
- | UnsolvableGoals [Goal]
- | UnsolvedDelayedCt DelayedCt
- | UnexpectedTypeWildCard
- | TypeVariableEscaped TypeSource Path Type [TParam]
- | NotForAll TypeSource Path TVar Type
- | TooManyPositionalTypeParams
- | BadParameterKind TParam Kind
- | CannotMixPositionalAndNamedTypeParams
- | UndefinedTypeParameter (Located Ident)
- | RepeatedTypeParameter Ident [Range]
- | AmbiguousSize TVarInfo (Maybe Type)
- | BareTypeApp
- | UndefinedExistVar Name
- | TypeShadowing String Name String
- | MissingModTParam (Located Ident)
- | MissingModVParam (Located Ident)
- | TemporaryError Doc
- data Warning
- ppWarning :: (Range, Warning) -> Doc
- ppError :: (Range, Error) -> Doc
- data WithNames a = WithNames a NameMap
- type NameMap = IntMap String
- ppNamedWarning :: NameMap -> (Range, Warning) -> Doc
- ppNamedError :: NameMap -> (Range, Error) -> Doc
Documentation
tcModule :: Module Name -> InferInput -> IO (InferOutput Module) Source #
Arguments
| :: IORef NamingEnv | renaming environment of functor |
| -> Module | functor |
| -> Module Name | params |
| -> InferInput | TC settings |
| -> IO (InferOutput Module) | new version of instance |
Check a module instantiation, assuming that the functor has already been checked. XXX: This will change
tcExpr :: Expr Name -> InferInput -> IO (InferOutput (Expr, Schema)) Source #
data InferInput Source #
Information needed for type inference.
Constructors
| InferInput | |
Fields
| |
data InferOutput a Source #
The results of type inference.
Constructors
| InferFailed NameMap [(Range, Warning)] [(Range, Error)] | We found some errors |
| InferOK NameMap [(Range, Warning)] NameSeeds Supply a | Type inference was successful. |
Instances
| Show a => Show (InferOutput a) Source # | |
Defined in Cryptol.TypeCheck.Monad Methods showsPrec :: Int -> InferOutput a -> ShowS # show :: InferOutput a -> String # showList :: [InferOutput a] -> ShowS # | |
data SolverConfig Source #
Constructors
| SolverConfig | |
Fields
| |
Instances
defaultSolverConfig :: [FilePath] -> SolverConfig Source #
A default configuration for using Z3, where the solver prelude is expected to be found in the given search path.
This is used for generating various names.
Instances
| Show NameSeeds Source # | |
| Generic NameSeeds Source # | |
| NFData NameSeeds Source # | |
Defined in Cryptol.TypeCheck.Monad | |
| type Rep NameSeeds Source # | |
Defined in Cryptol.TypeCheck.Monad type Rep NameSeeds = D1 ('MetaData "NameSeeds" "Cryptol.TypeCheck.Monad" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" 'False) (C1 ('MetaCons "NameSeeds" 'PrefixI 'True) (S1 ('MetaSel ('Just "seedTVar") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Just "seedGoal") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int))) | |
nameSeeds :: NameSeeds Source #
The initial seeds, used when checking a fresh program. XXX: why does this start at 10?
Various errors that might happen during type checking/inference
Constructors
| KindMismatch (Maybe TypeSource) Kind Kind | Expected kind, inferred kind |
| TooManyTypeParams Int Kind | Number of extra parameters, kind of result
(which should not be of the form |
| TyVarWithParams | A type variable was applied to some arguments. |
| TooManyTySynParams Name Int | Type-synonym, number of extra params |
| TooFewTyParams Name Int | Who is missing params, number of missing params |
| RecursiveTypeDecls [Name] | The type synonym declarations are recursive |
| TypeMismatch TypeSource Path Type Type | Expected type, inferred type |
| RecursiveType TypeSource Path Type Type | Unification results in a recursive type |
| UnsolvedGoals [Goal] | A constraint that we could not solve, usually because there are some left-over variables that we could not infer. |
| UnsolvableGoals [Goal] | A constraint that we could not solve and we know it is impossible to do it. |
| UnsolvedDelayedCt DelayedCt | A constraint (with context) that we could not solve |
| UnexpectedTypeWildCard | Type wild cards are not allowed in this context (e.g., definitions of type synonyms). |
| TypeVariableEscaped TypeSource Path Type [TParam] | Unification variable depends on quantified variables that are not in scope. |
| NotForAll TypeSource Path TVar Type | Quantified type variables (of kind *) need to match the given type, so it does not work for all types. |
| TooManyPositionalTypeParams | Too many positional type arguments, in an explicit type instantiation |
| BadParameterKind TParam Kind | Kind other than |
| CannotMixPositionalAndNamedTypeParams | |
| UndefinedTypeParameter (Located Ident) | |
| RepeatedTypeParameter Ident [Range] | |
| AmbiguousSize TVarInfo (Maybe Type) | Could not determine the value of a numeric type variable, but we know it must be at least as large as the given type (or unconstrained, if Nothing). |
| BareTypeApp | Bare expression of the form `{_} |
| UndefinedExistVar Name | |
| TypeShadowing String Name String | |
| MissingModTParam (Located Ident) | |
| MissingModVParam (Located Ident) | |
| TemporaryError Doc | This is for errors that don't fit other cateogories. We should not use it much, and is generally to be used for transient errors, which are due to incomplete implementation. |
Instances
Constructors
| DefaultingKind (TParam Name) Kind | |
| DefaultingWildType Kind | |
| DefaultingTo !TVarInfo Type |
Instances
This packages together a type with some names to be used to display the variables. It is used for pretty printing types.
Instances
| PP (WithNames Newtype) Source # | |
| PP (WithNames TySyn) Source # | |
| PP (WithNames TVar) Source # | |
| PP (WithNames Type) Source # | The precedence levels used by this pretty-printing instance correspond with parser non-terminals as follows:
|
| PP (WithNames TParam) Source # | |
| PP (WithNames Schema) Source # | |
| PP (WithNames DeclDef) Source # | |
| PP (WithNames Decl) Source # | |
| PP (WithNames DeclGroup) Source # | |
| PP (WithNames Match) Source # | |
| PP (WithNames Expr) Source # | |
| PP n => PP (WithNames (ModuleG n)) Source # | |
| PP (WithNames Subst) Source # | |
| PP (WithNames DelayedCt) Source # | |
| PP (WithNames Goal) Source # | |
| PP (WithNames Error) Source # | |
| PP (WithNames Warning) Source # | |