cryptol-2.4.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 | Haskell98

Cryptol.TypeCheck

Description

Synopsis

- tcModule :: 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
  - inpNameSeeds :: NameSeeds
  - inpMonoBinds :: Bool
  - inpSolverConfig :: SolverConfig
  - 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
  }
- data NameSeeds
- nameSeeds :: NameSeeds
- data Error
  - = ErrorMsg Doc
  - | KindMismatch Kind Kind
  - | TooManyTypeParams Int Kind
  - | TooManyTySynParams Name Int
  - | TooFewTySynParams Name Int
  - | RepeatedTyParams [TParam Name]
  - | RepeatedDefinitions Name [Range]
  - | RecursiveTypeDecls [Name]
  - | UndefinedTypeSynonym Name
  - | UndefinedVariable Name
  - | UndefinedTypeParam (Located Ident)
  - | MultipleTypeParamDefs Ident [Range]
  - | TypeMismatch Type Type
  - | RecursiveType Type Type
  - | UnsolvedGoal Bool Goal
  - | UnsolvedDelayedCt DelayedCt
  - | UnexpectedTypeWildCard
  - | TypeVariableEscaped Type [TVar]
  - | NotForAll TVar Type
  - | UnusableFunction Name [Prop]
  - | TooManyPositionalTypeParams
  - | CannotMixPositionalAndNamedTypeParams
  - | AmbiguousType [Name]
- data Warning
  - = DefaultingKind (TParam Name) Kind
  - | DefaultingWildType Kind
  - | DefaultingTo Doc Type
- ppWarning :: (Range, Warning) -> Doc
- ppError :: (Range, Error) -> Doc

# Documentation

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

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

- inpNameSeeds :: NameSeeds

  Private state of type-checker

- inpMonoBinds :: Bool

  Should local bindings without signatures be monomorphized?

- inpSolverConfig :: SolverConfig

  Options for the constraint solver

- inpPrimNames :: !PrimMap

  The mapping from `Ident` to `Name`, for names that the typechecker needs to refer to.

- inpSupply :: !Supply

  The supply for fresh name generation

Instances

Show InferInput Source # |
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 # |
Methods showsPrec :: Int -> InferOutput a -> ShowS # show :: InferOutput a -> String # showList :: [InferOutput a] -> ShowS #

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

Instances

Show SolverConfig Source # |
Methods showsPrec :: Int -> SolverConfig -> ShowS # show :: SolverConfig -> String # showList :: [SolverConfig] -> ShowS #
Generic SolverConfig Source # |
Associated Types type Rep SolverConfig :: * -> * # Methods from :: SolverConfig -> Rep SolverConfig x # to :: Rep SolverConfig x -> SolverConfig #
NFData SolverConfig Source # |
Methods rnf :: SolverConfig -> () #
type Rep SolverConfig Source # |

type Rep SolverConfig = D1 (MetaData "SolverConfig" "Cryptol.TypeCheck.InferTypes" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "SolverConfig" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "solverPath") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 FilePath)) ((:*:) (S1 (MetaSel (Just Symbol "solverArgs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [String])) (S1 (MetaSel (Just Symbol "solverVerbose") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)))))

data NameSeeds Source #

This is used for generating various names.

Instances

Show NameSeeds Source # |
Methods showsPrec :: Int -> NameSeeds -> ShowS # show :: NameSeeds -> String # showList :: [NameSeeds] -> ShowS #
Generic NameSeeds Source # |
Associated Types type Rep NameSeeds :: * -> * # Methods from :: NameSeeds -> Rep NameSeeds x # to :: Rep NameSeeds x -> NameSeeds #
NFData NameSeeds Source # |
Methods rnf :: NameSeeds -> () #
type Rep NameSeeds Source # |
type Rep NameSeeds = D1 (MetaData "NameSeeds" "Cryptol.TypeCheck.Monad" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) (C1 (MetaCons "NameSeeds" PrefixI True) ((:*:) (S1 (MetaSel (Just Symbol "seedTVar") NoSourceUnpackedness SourceStrict DecidedUnpack) (Rec0 Int)) (S1 (MetaSel (Just Symbol "seedGoal") NoSourceUnpackedness SourceStrict DecidedUnpack) (Rec0 Int))))

nameSeeds :: NameSeeds Source #

The initial seeds, used when checking a fresh program.

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 `_ -> _`)
TooManyTySynParams Name Int | Type-synonym, number of extra params
TooFewTySynParams Name Int | Type-synonym, number of missing params
RepeatedTyParams [TParam Name] | Type parameters with the same name (in definition)
RepeatedDefinitions Name [Range] | Multiple definitions for the same name
RecursiveTypeDecls [Name] | The type synonym declarations are recursive
UndefinedTypeSynonym Name | Use of a type synonym that was not defined
UndefinedVariable Name | Use of a variable that was not defined
UndefinedTypeParam (Located Ident) | Attempt to explicitly instantiate a non-existent param.
MultipleTypeParamDefs Ident [Range] | Multiple definitions for the same type parameter
TypeMismatch Type Type | Expected type, inferred type
RecursiveType Type Type | Unification results in a recursive type
UnsolvedGoal 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 [TVar] | 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 |
AmbiguousType [Name] |

Instances

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

type Rep Error = D1 (MetaData "Error" "Cryptol.TypeCheck.InferTypes" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "ErrorMsg" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Doc))) (C1 (MetaCons "KindMismatch" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind))))) ((:+:) (C1 (MetaCons "TooManyTypeParams" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind)))) ((:+:) (C1 (MetaCons "TooManyTySynParams" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)))) (C1 (MetaCons "TooFewTySynParams" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int))))))) ((:+:) ((:+:) (C1 (MetaCons "RepeatedTyParams" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [TParam Name]))) ((:+:) (C1 (MetaCons "RepeatedDefinitions" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Range])))) (C1 (MetaCons "RecursiveTypeDecls" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name]))))) ((:+:) (C1 (MetaCons "UndefinedTypeSynonym" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name))) ((:+:) (C1 (MetaCons "UndefinedVariable" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name))) (C1 (MetaCons "UndefinedTypeParam" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Located Ident)))))))) ((:+:) ((:+:) ((:+:) (C1 (MetaCons "MultipleTypeParamDefs" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Ident)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Range])))) ((:+:) (C1 (MetaCons "TypeMismatch" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)))) (C1 (MetaCons "RecursiveType" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)))))) ((:+:) (C1 (MetaCons "UnsolvedGoal" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Bool)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Goal)))) ((:+:) (C1 (MetaCons "UnsolvedDelayedCt" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 DelayedCt))) (C1 (MetaCons "UnexpectedTypeWildCard" PrefixI False) U1)))) ((:+:) ((:+:) (C1 (MetaCons "TypeVariableEscaped" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [TVar])))) ((:+:) (C1 (MetaCons "NotForAll" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TVar)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type)))) (C1 (MetaCons "UnusableFunction" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Prop])))))) ((:+:) (C1 (MetaCons "TooManyPositionalTypeParams" PrefixI False) U1) ((:+:) (C1 (MetaCons "CannotMixPositionalAndNamedTypeParams" PrefixI False) U1) (C1 (MetaCons "AmbiguousType" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Name]))))))))

data Warning Source #

Constructors

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

Instances

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

type Rep Warning = D1 (MetaData "Warning" "Cryptol.TypeCheck.InferTypes" "cryptol-2.4.0-CN28BMG3PUFD1lr9WvB1U9" False) ((:+:) (C1 (MetaCons "DefaultingKind" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (TParam Name))) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind)))) ((:+:) (C1 (MetaCons "DefaultingWildType" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind))) (C1 (MetaCons "DefaultingTo" PrefixI False) ((:*:) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Doc)) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Type))))))

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

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