Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
This module contains types related to typechecking and the output of the
typechecker. In particular, it should contain the types needed by
interface files (see Interface
), which are (kind of)
the output of the typechker.
Synopsis
- data Type
- type Prop = Type
- data TVar
- data ArgDescr = ArgDescr {}
- data Schema = Forall {}
- data TParam = TParam {}
- data TySyn = TySyn {}
- data EnumCon = EnumCon {}
- data ModParam = ModParam {
- mpName :: Ident
- mpQual :: !(Maybe ModName)
- mpIface :: ImpName Name
- mpParameters :: ModParamNames
- data ModParamNames = ModParamNames {}
- class FVS t where
- type FunctorParams = Map Ident ModParam
- data ModTParam = ModTParam {}
- data ModVParam = ModVParam {}
- data TVarInfo = TVarInfo {
- tvarSource :: !Range
- tvarDesc :: !TypeSource
- data TPFlavor
- data NominalType = NominalType {}
- data TypeSource
- = TVFromModParam Name
- | TVFromSignature Name
- | TypeWildCard
- | TypeOfRecordField Ident
- | TypeOfTupleField Int
- | TypeOfSeqElement
- | LenOfSeq
- | TypeParamInstNamed Name Ident
- | TypeParamInstPos Name Int
- | DefinitionOf Name
- | LenOfCompGen
- | TypeOfArg ArgDescr
- | TypeOfRes
- | FunApp
- | TypeOfIfCondExpr
- | TypeFromUserAnnotation
- | GeneratorOfListComp
- | CasedExpression
- | ConPat
- | TypeErrorPlaceHolder
- data TypeWithSource = WithSource {}
- data NominalTypeDef
- data StructCon = StructCon {}
- type SType = Type
- (=/=) :: Type -> Type -> Prop
- tArray :: Type -> Type -> Type
- tSub :: Type -> Type -> Type
- tMul :: Type -> Type -> Type
- tDiv :: Type -> Type -> Type
- tMod :: Type -> Type -> Type
- tExp :: Type -> Type -> Type
- tMin :: Type -> Type -> Type
- tCeilDiv :: Type -> Type -> Type
- tCeilMod :: Type -> Type -> Type
- tLenFromThenTo :: Type -> Type -> Type -> Type
- tpName :: TParam -> Maybe Name
- (=#=) :: Type -> Type -> Prop
- (>==) :: Type -> Type -> Prop
- tFun :: Type -> Type -> Type
- allParamNames :: FunctorParams -> ModParamNames
- mtpParam :: ModTParam -> TParam
- tMono :: Type -> Schema
- isMono :: Schema -> Maybe Type
- schemaParam :: Name -> TPFlavor
- tySynParam :: Name -> TPFlavor
- propSynParam :: Name -> TPFlavor
- nominalParam :: Name -> TPFlavor
- primParam :: Name -> TPFlavor
- modTyParam :: Name -> TPFlavor
- tpfName :: TPFlavor -> Maybe Name
- tvInfo :: TVar -> TVarInfo
- tvUnique :: TVar -> Int
- noArgDescr :: ArgDescr
- tvSourceName :: TypeSource -> Maybe Name
- quickApply :: Kind -> [a] -> Kind
- kindResult :: Kind -> Kind
- tpVar :: TParam -> TVar
- superclassSet :: Prop -> Set Prop
- pFin :: Type -> Prop
- tTwo :: Type
- nominalTypeConTypes :: NominalType -> [(Name, Schema)]
- nominalTypeIsAbstract :: NominalType -> Bool
- isFreeTV :: TVar -> Bool
- isBoundTV :: TVar -> Bool
- tIsError :: Type -> Maybe Type
- tNoUser :: Type -> Type
- tHasErrors :: Type -> Bool
- tIsNat' :: Type -> Maybe Nat'
- tIsNum :: Type -> Maybe Integer
- tIsInf :: Type -> Bool
- tIsVar :: Type -> Maybe TVar
- tIsFun :: Type -> Maybe (Type, Type)
- tIsSeq :: Type -> Maybe (Type, Type)
- tIsBit :: Type -> Bool
- tIsInteger :: Type -> Bool
- tIsIntMod :: Type -> Maybe Type
- tIsRational :: Type -> Bool
- tIsFloat :: Type -> Maybe (Type, Type)
- tIsTuple :: Type -> Maybe [Type]
- tIsRec :: Type -> Maybe (RecordMap Ident Type)
- tIsBinFun :: TFun -> Type -> Maybe (Type, Type)
- tSplitFun :: TFun -> Type -> [Type]
- pIsFin :: Prop -> Maybe Type
- pIsPrime :: Prop -> Maybe Type
- pIsGeq :: Prop -> Maybe (Type, Type)
- pIsEqual :: Prop -> Maybe (Type, Type)
- pIsZero :: Prop -> Maybe Type
- pIsLogic :: Prop -> Maybe Type
- pIsRing :: Prop -> Maybe Type
- pIsField :: Prop -> Maybe Type
- pIsIntegral :: Prop -> Maybe Type
- pIsRound :: Prop -> Maybe Type
- pIsEq :: Prop -> Maybe Type
- pIsCmp :: Prop -> Maybe Type
- pIsSignedCmp :: Prop -> Maybe Type
- pIsLiteral :: Prop -> Maybe (Type, Type)
- pIsLiteralLessThan :: Prop -> Maybe (Type, Type)
- pIsFLiteral :: Prop -> Maybe (Type, Type, Type, Type)
- pIsTrue :: Prop -> Bool
- pIsWidth :: Prop -> Maybe Type
- pIsValidFloat :: Prop -> Maybe (Type, Type)
- tNum :: Integral a => a -> Type
- tZero :: Type
- tOne :: Type
- tInf :: Type
- tNat' :: Nat' -> Type
- tNominal :: NominalType -> [Type] -> Type
- tBit :: Type
- tInteger :: Type
- tRational :: Type
- tFloat :: Type -> Type -> Type
- tIntMod :: Type -> Type
- tWord :: Type -> Type
- tSeq :: Type -> Type -> Type
- tChar :: Type
- tString :: Int -> Type
- tRec :: RecordMap Ident Type -> Type
- tTuple :: [Type] -> Type
- tError :: Type -> Type
- tf1 :: TFun -> Type -> Type
- tf2 :: TFun -> Type -> Type -> Type
- tf3 :: TFun -> Type -> Type -> Type -> Type
- pZero :: Type -> Prop
- pLogic :: Type -> Prop
- pRing :: Type -> Prop
- pIntegral :: Type -> Prop
- pField :: Type -> Prop
- pRound :: Type -> Prop
- pEq :: Type -> Prop
- pCmp :: Type -> Prop
- pSignedCmp :: Type -> Prop
- pLiteral :: Type -> Type -> Prop
- pLiteralLessThan :: Type -> Type -> Prop
- pHas :: Selector -> Type -> Type -> Prop
- pTrue :: Prop
- pAnd :: [Prop] -> Prop
- pSplitAnd :: Prop -> [Prop]
- pValidFloat :: Type -> Type -> Type
- pPrime :: Type -> Prop
- pNegNumeric :: Prop -> [Prop]
- noFreeVariables :: FVS t => t -> Bool
- freeParams :: FVS t => t -> Set TParam
- addTNames :: [TParam] -> NameMap -> NameMap
- ppNominalShort :: NominalType -> Doc
- ppNominalFull :: NominalType -> Doc
- pickTVarName :: Kind -> TypeSource -> Int -> Doc
- module Cryptol.TypeCheck.TCon
Documentation
The internal representation of types. These are assumed to be kind correct.
TCon !TCon ![Type] | Type constant with args |
TVar TVar | Type variable (free or bound) |
TUser !Name ![Type] !Type | This is just a type annotation, for a type that
was written as a type synonym. It is useful so that we
can use it to report nicer errors.
Example: |
TRec !(RecordMap Ident Type) | Record type |
TNominal !NominalType ![Type] | A nominal types |
Instances
Type variables.
TVFree !Int Kind (Set TParam) TVarInfo | Unique, kind, ids of bound type variables that are in scope. The last field gives us some info for nicer warnings/errors. |
TVBound !TParam |
Instances
Instances
Generic ArgDescr Source # | |
Show ArgDescr Source # | |
TraverseNames ArgDescr Source # | |
Defined in Cryptol.IR.TraverseNames traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => ArgDescr -> f ArgDescr Source # | |
PP ArgDescr Source # | |
NFData ArgDescr Source # | |
Defined in Cryptol.TypeCheck.Type | |
type Rep ArgDescr Source # | |
Defined in Cryptol.TypeCheck.Type type Rep ArgDescr = D1 ('MetaData "ArgDescr" "Cryptol.TypeCheck.Type" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "ArgDescr" 'PrefixI 'True) (S1 ('MetaSel ('Just "argDescrFun") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Name)) :*: S1 ('MetaSel ('Just "argDescrNumber") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int)))) |
The types of polymorphic values.
Instances
Type parameters.
Instances
Type synonym.
Instances
Constructor for an enumeration
Instances
A module parameter. Corresponds to a "signature import". A single module parameter can bring multiple things in scope.
ModParam | |
|
Instances
Generic ModParam Source # | |
Show ModParam Source # | |
ModuleInstance ModParam Source # | |
Defined in Cryptol.TypeCheck.ModuleInstance moduleInstance :: ModParam -> ModParam Source # | |
NFData ModParam Source # | |
Defined in Cryptol.TypeCheck.Type | |
type Rep ModParam Source # | |
Defined in Cryptol.TypeCheck.Type type Rep ModParam = D1 ('MetaData "ModParam" "Cryptol.TypeCheck.Type" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "ModParam" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mpName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident) :*: S1 ('MetaSel ('Just "mpQual") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe ModName))) :*: (S1 ('MetaSel ('Just "mpIface") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ImpName Name)) :*: S1 ('MetaSel ('Just "mpParameters") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModParamNames)))) |
data ModParamNames Source #
Information about the names brought in through an "interface import". This is also used to keep information about.
Instances
Instances
FVS Error Source # | |
FVS Warning Source # | |
FVS FFITypeError Source # | |
Defined in Cryptol.TypeCheck.FFI.Error | |
FVS FFITypeErrorReason Source # | |
Defined in Cryptol.TypeCheck.FFI.Error | |
FVS DelayedCt Source # | |
FVS Goal Source # | |
FVS Schema Source # | |
FVS Type Source # | |
FVS a => FVS (Maybe a) Source # | |
FVS a => FVS [a] Source # | |
(FVS a, FVS b) => FVS (a, b) Source # | |
A type parameter of a module.
Instances
Generic ModTParam Source # | |
Show ModTParam Source # | |
TraverseNames ModTParam Source # | |
Defined in Cryptol.IR.TraverseNames traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => ModTParam -> f ModTParam Source # | |
ModuleInstance ModTParam Source # | |
Defined in Cryptol.TypeCheck.ModuleInstance moduleInstance :: ModTParam -> ModTParam Source # | |
PP ModTParam Source # | |
NFData ModTParam Source # | |
Defined in Cryptol.TypeCheck.Type | |
type Rep ModTParam Source # | |
Defined in Cryptol.TypeCheck.Type type Rep ModTParam = D1 ('MetaData "ModTParam" "Cryptol.TypeCheck.Type" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "ModTParam" 'PrefixI 'True) (S1 ('MetaSel ('Just "mtpName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: (S1 ('MetaSel ('Just "mtpKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind) :*: S1 ('MetaSel ('Just "mtpDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text))))) |
A value parameter of a module.
Instances
TVarInfo | |
|
Instances
Generic TVarInfo Source # | |
Show TVarInfo Source # | |
TraverseNames TVarInfo Source # | |
Defined in Cryptol.IR.TraverseNames traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => TVarInfo -> f TVarInfo Source # | |
PP TVarInfo Source # | |
NFData TVarInfo Source # | |
Defined in Cryptol.TypeCheck.Type | |
type Rep TVarInfo Source # | |
Defined in Cryptol.TypeCheck.Type type Rep TVarInfo = D1 ('MetaData "TVarInfo" "Cryptol.TypeCheck.Type" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "TVarInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "tvarSource") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Range) :*: S1 ('MetaSel ('Just "tvarDesc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TypeSource))) |
TPModParam Name | |
TPUnifyVar | |
TPSchemaParam Name | |
TPTySynParam Name | |
TPPropSynParam Name | |
TPNominalParam Name | |
TPPrimParam Name |
Instances
data NominalType Source #
Nominal types
Instances
data TypeSource Source #
Explains how this type came to be, for better error messages.
Instances
data NominalTypeDef Source #
Definition of a nominal type
Instances
Constructor for a struct (aka newtype)
Instances
Generic StructCon Source # | |
Show StructCon Source # | |
FreeVars StructCon Source # | |
TraverseNames StructCon Source # | |
Defined in Cryptol.IR.TraverseNames traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => StructCon -> f StructCon Source # | |
ModuleInstance StructCon Source # | |
Defined in Cryptol.TypeCheck.ModuleInstance moduleInstance :: StructCon -> StructCon Source # | |
NFData StructCon Source # | |
Defined in Cryptol.TypeCheck.Type | |
type Rep StructCon Source # | |
Defined in Cryptol.TypeCheck.Type type Rep StructCon = D1 ('MetaData "StructCon" "Cryptol.TypeCheck.Type" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "StructCon" 'PrefixI 'True) (S1 ('MetaSel ('Just "ntConName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name) :*: S1 ('MetaSel ('Just "ntFields") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RecordMap Ident Type)))) |
allParamNames :: FunctorParams -> ModParamNames Source #
Compute the names from all functor parameters
schemaParam :: Name -> TPFlavor Source #
tySynParam :: Name -> TPFlavor Source #
propSynParam :: Name -> TPFlavor Source #
nominalParam :: Name -> TPFlavor Source #
modTyParam :: Name -> TPFlavor Source #
tvSourceName :: TypeSource -> Maybe Name Source #
Get the names of something that is related to the tvar.
quickApply :: Kind -> [a] -> Kind Source #
kindResult :: Kind -> Kind Source #
superclassSet :: Prop -> Set Prop Source #
Compute the set of all Prop
s that are implied by the
given prop via superclass constraints.
nominalTypeConTypes :: NominalType -> [(Name, Schema)] Source #
tHasErrors :: Type -> Bool Source #
tIsInteger :: Type -> Bool Source #
tIsRational :: Type -> Bool Source #
tSplitFun :: TFun -> Type -> [Type] Source #
Split up repeated occurances of the given binary type-level function.
tError :: Type -> Type Source #
Make an error value of the given type to replace the given malformed type (the argument to the error function)
pSignedCmp :: Type -> Prop Source #
pHas :: Selector -> Type -> Type -> Prop Source #
A Has
constraint, used for tuple and record selection.
pNegNumeric :: Prop -> [Prop] Source #
pNegNumeric
negates a simple (i.e., not And, not prime, etc) prop
over numeric type vars. The result is a conjunction of properties.
noFreeVariables :: FVS t => t -> Bool Source #
ppNominalShort :: NominalType -> Doc Source #
ppNominalFull :: NominalType -> Doc Source #
pickTVarName :: Kind -> TypeSource -> Int -> Doc Source #
module Cryptol.TypeCheck.TCon