Copyright | (c) 2013-2016 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell2010 |
Cryptol.TypeCheck
Description
Synopsis
- tcModule :: Module Name -> InferInput -> IO (InferOutput Module)
- tcModuleInst :: Module -> Module Name -> InferInput -> IO (InferOutput Module)
- tcExpr :: Expr Name -> InferInput -> IO (InferOutput (Expr, Schema))
- tcDecls :: FromDecl d => [d] -> InferInput -> IO (InferOutput [DeclGroup])
- 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
- inpSolverConfig :: SolverConfig
- inpSearchPath :: [FilePath]
- inpPrimNames :: !PrimMap
- inpSupply :: !Supply
- data InferOutput a
- data SolverConfig = SolverConfig {
- solverPath :: FilePath
- solverArgs :: [String]
- solverVerbose :: Int
- solverPreludePath :: [FilePath]
- data NameSeeds
- nameSeeds :: NameSeeds
- data Error
- = ErrorMsg Doc
- | KindMismatch Kind Kind
- | TooManyTypeParams Int Kind
- | TyVarWithParams
- | TooManyTySynParams Name Int
- | TooFewTyParams Name Int
- | RecursiveTypeDecls [Name]
- | TypeMismatch Type Type
- | RecursiveType Type Type
- | UnsolvedGoals Bool [Goal]
- | UnsolvedDelayedCt DelayedCt
- | UnexpectedTypeWildCard
- | TypeVariableEscaped Type [TParam]
- | NotForAll TVar Type
- | TooManyPositionalTypeParams
- | CannotMixPositionalAndNamedTypeParams
- | UndefinedTypeParameter (Located Ident)
- | RepeatedTypeParameter Ident [Range]
- data Warning
- ppWarning :: (Range, Warning) -> Doc
- ppError :: (Range, Error) -> Doc
Documentation
tcModule :: Module Name -> InferInput -> IO (InferOutput Module) Source #
Arguments
:: Module | functor |
-> Module Name | |
-> InferInput | TC settings |
-> IO (InferOutput Module) | new version of instance |
Check a module instantiation, assuming that the functor has already been checked.
tcExpr :: Expr Name -> InferInput -> IO (InferOutput (Expr, Schema)) Source #
tcDecls :: FromDecl d => [d] -> InferInput -> IO (InferOutput [DeclGroup]) Source #
data InferInput Source #
Information needed for type inference.
Constructors
InferInput | |
Fields
|
Instances
Show InferInput Source # | |
Defined in Cryptol.TypeCheck.Monad Methods showsPrec :: Int -> InferInput -> ShowS show :: InferInput -> String showList :: [InferInput] -> ShowS |
data InferOutput a Source #
The results of type inference.
Constructors
InferFailed [(Range, Warning)] [(Range, Error)] | We found some errors |
InferOK [(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
Show SolverConfig Source # | |
Defined in Cryptol.TypeCheck.InferTypes Methods showsPrec :: Int -> SolverConfig -> ShowS show :: SolverConfig -> String showList :: [SolverConfig] -> ShowS | |
Generic SolverConfig Source # | |
Defined in Cryptol.TypeCheck.InferTypes Associated Types type Rep SolverConfig :: Type -> Type | |
NFData SolverConfig Source # | |
Defined in Cryptol.TypeCheck.InferTypes Methods rnf :: SolverConfig -> () | |
type Rep SolverConfig Source # | |
Defined in Cryptol.TypeCheck.InferTypes type Rep SolverConfig = D1 ('MetaData "SolverConfig" "Cryptol.TypeCheck.InferTypes" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "SolverConfig" 'PrefixI 'True) ((S1 ('MetaSel ('Just "solverPath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FilePath) :*: S1 ('MetaSel ('Just "solverArgs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])) :*: (S1 ('MetaSel ('Just "solverVerbose") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "solverPreludePath") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath])))) |
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.8.0-8MjdO3NUDs4I9u4d2J06AM" '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
ErrorMsg Doc | Just say this |
KindMismatch 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 Type Type | Expected type, inferred type |
RecursiveType Type Type | Unification results in a recursive type |
UnsolvedGoals Bool [Goal] | A constraint that we could not solve The boolean indicates if we know that this constraint is impossible. |
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 Type [TParam] | Unification variable depends on quantified variables that are not in scope. |
NotForAll 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 |
CannotMixPositionalAndNamedTypeParams | |
UndefinedTypeParameter (Located Ident) | |
RepeatedTypeParameter Ident [Range] |
Instances
Show Error Source # | |
Generic Error Source # | |
NFData Error Source # | |
Defined in Cryptol.TypeCheck.Error | |
PP Error Source # | |
FVS Error Source # | |
TVars Error Source # | |
PP (WithNames Error) Source # | |
type Rep Error Source # | |
Defined in Cryptol.TypeCheck.Error type Rep Error = D1 ('MetaData "Error" "Cryptol.TypeCheck.Error" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) ((((C1 ('MetaCons "ErrorMsg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Doc)) :+: C1 ('MetaCons "KindMismatch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind))) :+: (C1 ('MetaCons "TooManyTypeParams" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)) :+: C1 ('MetaCons "TyVarWithParams" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "TooManyTySynParams" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "TooFewTyParams" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))) :+: (C1 ('MetaCons "RecursiveTypeDecls" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name])) :+: (C1 ('MetaCons "TypeMismatch" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: C1 ('MetaCons "RecursiveType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))))) :+: (((C1 ('MetaCons "UnsolvedGoals" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Goal])) :+: C1 ('MetaCons "UnsolvedDelayedCt" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DelayedCt))) :+: (C1 ('MetaCons "UnexpectedTypeWildCard" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TypeVariableEscaped" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam])))) :+: ((C1 ('MetaCons "NotForAll" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TVar) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)) :+: C1 ('MetaCons "TooManyPositionalTypeParams" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CannotMixPositionalAndNamedTypeParams" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "UndefinedTypeParameter" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Located Ident))) :+: C1 ('MetaCons "RepeatedTypeParameter" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Range]))))))) |
Constructors
DefaultingKind (TParam Name) Kind | |
DefaultingWildType Kind | |
DefaultingTo TVarInfo Type |
Instances
Show Warning Source # | |
Generic Warning Source # | |
NFData Warning Source # | |
Defined in Cryptol.TypeCheck.Error | |
PP Warning Source # | |
FVS Warning Source # | |
TVars Warning Source # | |
PP (WithNames Warning) Source # | |
type Rep Warning Source # | |
Defined in Cryptol.TypeCheck.Error type Rep Warning = D1 ('MetaData "Warning" "Cryptol.TypeCheck.Error" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "DefaultingKind" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TParam Name)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)) :+: (C1 ('MetaCons "DefaultingWildType" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)) :+: C1 ('MetaCons "DefaultingTo" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TVarInfo) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))) |