cryptol-2.6.0: Cryptol: The Language of Cryptography

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
  - 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
  - = InferFailed [(Range, Warning)] [(Range, Error)]
  - | InferOK [(Range, Warning)] NameSeeds Supply 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
  - | TooFewTySynParams Name Int
  - | RecursiveTypeDecls [Name]
  - | TypeMismatch Type Type
  - | RecursiveType Type Type
  - | UnsolvedGoals Bool [Goal]
  - | UnsolvedDelayedCt DelayedCt
  - | UnexpectedTypeWildCard
  - | TypeVariableEscaped Type [TParam]
  - | NotForAll TVar Type
  - | UnusableFunction Name [Prop]
  - | TooManyPositionalTypeParams
  - | CannotMixPositionalAndNamedTypeParams
  - | UndefinedTypeParameter (Located Ident)
  - | RepeatedTypeParameter Ident [Range]
  - | AmbiguousType [Name] [TVar]
- data Warning
  - = DefaultingKind (TParam Name) Kind
  - | DefaultingWildType Kind
  - | DefaultingTo TVarInfo Type
- ppWarning :: (Range, Warning) -> Doc
- ppError :: (Range, Error) -> Doc

# Documentation

tcModule :: Module Name -> InferInput -> IO (InferOutput Module) Source #

tcModuleInst 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

- inpRange :: Range

  Location of program source

- inpVars :: Map Name Schema

  Variables that are in scope

- inpTSyns :: Map Name TySyn

  Type synonyms that are in scope

- inpNewtypes :: Map Name Newtype

  Newtypes in scope

- inpParamTypes :: !(Map Name ModTParam)

  Type parameters

- inpParamConstraints :: ![Located Prop]

  Constraints on parameters

- inpParamFuns :: !(Map Name ModVParam)

  Value parameters

- inpNameSeeds :: NameSeeds

  Private state of type-checker

- inpMonoBinds :: Bool

  Should local bindings without signatures be monomorphized?

- inpSolverConfig :: SolverConfig

  Options for the constraint solver

- inpSearchPath :: [FilePath]

  Where to look for Cryptol theory file.

- inpPrimNames :: !PrimMap

  This is used when the type-checker needs to refer to a predefined identifier (e.g., `number`).

- inpSupply :: !Supply

  The supply for fresh name generation

Instances

Show InferInput Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods showsPrec :: Int -> InferInput -> ShowS Source # show :: InferInput -> String Source # showList :: [InferInput] -> ShowS Source #

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 # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods showsPrec :: Int -> InferOutput a -> ShowS Source # show :: InferOutput a -> String Source # showList :: [InferOutput a] -> ShowS Source #

data SolverConfig Source #

Constructors

SolverConfig |

Fields

- solverPath :: FilePath

  The SMT solver to invoke

- solverArgs :: [String]

  Additional arguments to pass to the solver

- solverVerbose :: Int

  How verbose to be when type-checking

- solverPreludePath :: [FilePath]

  Look for the solver prelude in these locations.

Instances

Show SolverConfig Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods showsPrec :: Int -> SolverConfig -> ShowS Source # show :: SolverConfig -> String Source # showList :: [SolverConfig] -> ShowS Source #
Generic SolverConfig Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Associated Types type Rep SolverConfig :: Type -> Type Source # Methods from :: SolverConfig -> Rep SolverConfig x Source # to :: Rep SolverConfig x -> SolverConfig Source #
NFData SolverConfig Source # |
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods rnf :: SolverConfig -> () Source #
type Rep SolverConfig Source # |

Instance details

Defined in Cryptol.TypeCheck.InferTypes

type Rep SolverConfig = D1 (MetaData "SolverConfig" "Cryptol.TypeCheck.InferTypes" "cryptol-2.6.0-FO78l5UWBYr51eDL1ksQpO" 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]))))

data NameSeeds Source #

This is used for generating various names.

Instances

Show NameSeeds Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods showsPrec :: Int -> NameSeeds -> ShowS Source # show :: NameSeeds -> String Source # showList :: [NameSeeds] -> ShowS Source #
Generic NameSeeds Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Associated Types type Rep NameSeeds :: Type -> Type Source # Methods from :: NameSeeds -> Rep NameSeeds x Source # to :: Rep NameSeeds x -> NameSeeds Source #
NFData NameSeeds Source # |
Instance details Defined in Cryptol.TypeCheck.Monad Methods rnf :: NameSeeds -> () Source #
type Rep NameSeeds Source # |
Instance details Defined in Cryptol.TypeCheck.Monad type Rep NameSeeds = D1 (MetaData "NameSeeds" "Cryptol.TypeCheck.Monad" "cryptol-2.6.0-FO78l5UWBYr51eDL1ksQpO" 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?

data Error Source #

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
TooFewTySynParams Name Int | Type-synonym, 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.
UnusableFunction Name [Prop] | The given constraints causes the signature of the function to be not-satisfiable.
TooManyPositionalTypeParams | Too many positional type arguments, in an explicit type instantiation
CannotMixPositionalAndNamedTypeParams |
UndefinedTypeParameter (Located Ident) |
RepeatedTypeParameter Ident [Range] |
AmbiguousType [Name] [TVar] |

Instances

Show Error Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods showsPrec :: Int -> Error -> ShowS Source # show :: Error -> String Source # showList :: [Error] -> ShowS Source #
Generic Error Source # |
Instance details Defined in Cryptol.TypeCheck.Error Associated Types type Rep Error :: Type -> Type Source # Methods from :: Error -> Rep Error x Source # to :: Rep Error x -> Error Source #
NFData Error Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods rnf :: Error -> () Source #
PP Error Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods ppPrec :: Int -> Error -> Doc Source #
FVS Error Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods fvs :: Error -> Set TVar Source #
TVars Error Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods apSubst :: Subst -> Error -> Error Source #
PP (WithNames Error) Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods ppPrec :: Int -> WithNames Error -> Doc Source #
type Rep Error Source # |

Instance details

Defined in Cryptol.TypeCheck.Error

type Rep Error = D1 (MetaData "Error" "Cryptol.TypeCheck.Error" "cryptol-2.6.0-FO78l5UWBYr51eDL1ksQpO" 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 "TooFewTySynParams" 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 "UnusableFunction" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Prop]))))) :+: ((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])) :+: C1 (MetaCons "AmbiguousType" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name]) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [TVar])))))))

data Warning Source #

Constructors

DefaultingKind (TParam Name) Kind |
DefaultingWildType Kind |
DefaultingTo TVarInfo Type |

Instances

Show Warning Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods showsPrec :: Int -> Warning -> ShowS Source # show :: Warning -> String Source # showList :: [Warning] -> ShowS Source #
Generic Warning Source # |
Instance details Defined in Cryptol.TypeCheck.Error Associated Types type Rep Warning :: Type -> Type Source # Methods from :: Warning -> Rep Warning x Source # to :: Rep Warning x -> Warning Source #
NFData Warning Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods rnf :: Warning -> () Source #
PP Warning Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods ppPrec :: Int -> Warning -> Doc Source #
FVS Warning Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods fvs :: Warning -> Set TVar Source #
TVars Warning Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods apSubst :: Subst -> Warning -> Warning Source #
PP (WithNames Warning) Source # |
Instance details Defined in Cryptol.TypeCheck.Error Methods ppPrec :: Int -> WithNames Warning -> Doc Source #
type Rep Warning Source # |

Instance details

Defined in Cryptol.TypeCheck.Error

type Rep Warning = D1 (MetaData "Warning" "Cryptol.TypeCheck.Error" "cryptol-2.6.0-FO78l5UWBYr51eDL1ksQpO" 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))))

ppWarning :: (Range, Warning) -> Doc Source #

ppError :: (Range, Error) -> Doc Source #