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
- class FVS t where
- type SType = Type
- data AbstractType = AbstractType {}
- data Newtype = Newtype {}
- data TySyn = TySyn {}
- type Prop = Type
- data TypeWithSource = WithSource {}
- data ArgDescr = ArgDescr {}
- 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
- | TypeErrorPlaceHolder
- data TVarInfo = TVarInfo {
- tvarSource :: !Range
- tvarDesc :: !TypeSource
- data TVar
- data Type
- data TPFlavor
- data TParam = TParam {}
- data Schema = Forall {}
- data ModVParam = ModVParam {}
- data ModTParam = ModTParam {}
- mtpParam :: ModTParam -> TParam
- tMono :: Type -> Schema
- isMono :: Schema -> Maybe Type
- schemaParam :: Name -> TPFlavor
- tySynParam :: Name -> TPFlavor
- propSynParam :: Name -> TPFlavor
- newtypeParam :: Name -> TPFlavor
- modTyParam :: Name -> TPFlavor
- tpfName :: TPFlavor -> Maybe Name
- tpName :: TParam -> 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
- newtypeConType :: Newtype -> Schema
- abstractTypeTC :: AbstractType -> TCon
- isFreeTV :: TVar -> Bool
- isBoundTV :: TVar -> Bool
- tIsError :: Type -> Maybe 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
- tTwo :: Type
- tInf :: Type
- tNat' :: Nat' -> Type
- tAbstract :: UserTC -> [Type] -> Type
- tNewtype :: Newtype -> [Type] -> Type
- tBit :: Type
- tInteger :: Type
- tRational :: Type
- tFloat :: Type -> Type -> Type
- tIntMod :: Type -> Type
- tArray :: Type -> Type -> Type
- tWord :: Type -> Type
- tSeq :: Type -> Type -> Type
- tChar :: Type
- tString :: Int -> Type
- tRec :: RecordMap Ident Type -> Type
- tTuple :: [Type] -> Type
- tFun :: Type -> Type -> Type
- tNoUser :: Type -> Type
- tError :: Type -> Type
- tf1 :: TFun -> Type -> Type
- tf2 :: TFun -> Type -> Type -> Type
- tf3 :: TFun -> Type -> 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
- (=#=) :: Type -> Type -> Prop
- (=/=) :: Type -> Type -> Prop
- 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
- (>==) :: Type -> Type -> Prop
- pHas :: Selector -> Type -> Type -> Prop
- pTrue :: Prop
- pAnd :: [Prop] -> Prop
- pSplitAnd :: Prop -> [Prop]
- pFin :: Type -> Prop
- pValidFloat :: Type -> Type -> Type
- pPrime :: Type -> Prop
- noFreeVariables :: FVS t => t -> Bool
- freeParams :: FVS t => t -> Set TParam
- addTNames :: [TParam] -> NameMap -> NameMap
- ppNewtypeShort :: Newtype -> Doc
- pickTVarName :: Kind -> TypeSource -> Int -> Doc
- module Cryptol.TypeCheck.TCon
Documentation
data AbstractType Source #
Information about an abstract type.
Instances
Named records
Instances
Type synonym.
Instances
Show TySyn Source # | |
Generic TySyn Source # | |
NFData TySyn Source # | |
Defined in Cryptol.TypeCheck.Type | |
PP TySyn Source # | |
HasKind TySyn Source # | |
TVars TySyn Source # | |
PP (WithNames TySyn) Source # | |
type Rep TySyn Source # | |
Defined in Cryptol.TypeCheck.Type type Rep TySyn = D1 ('MetaData "TySyn" "Cryptol.TypeCheck.Type" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" 'False) (C1 ('MetaCons "TySyn" 'PrefixI 'True) ((S1 ('MetaSel ('Just "tsName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "tsParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam])) :*: (S1 ('MetaSel ('Just "tsConstraints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Prop]) :*: (S1 ('MetaSel ('Just "tsDef") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type) :*: S1 ('MetaSel ('Just "tsDoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Text)))))) |
Instances
Show ArgDescr Source # | |
Generic ArgDescr Source # | |
NFData ArgDescr Source # | |
Defined in Cryptol.TypeCheck.Type | |
PP ArgDescr Source # | |
type Rep ArgDescr Source # | |
Defined in Cryptol.TypeCheck.Type type Rep ArgDescr = D1 ('MetaData "ArgDescr" "Cryptol.TypeCheck.Type" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" '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)))) |
data TypeSource Source #
Explains how this type came to be, for better error messages.
Instances
TVarInfo | |
|
Instances
Show TVarInfo Source # | |
Generic TVarInfo Source # | |
NFData TVarInfo Source # | |
Defined in Cryptol.TypeCheck.Type | |
PP TVarInfo Source # | |
type Rep TVarInfo Source # | |
Defined in Cryptol.TypeCheck.Type type Rep TVarInfo = D1 ('MetaData "TVarInfo" "Cryptol.TypeCheck.Type" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" 'False) (C1 ('MetaCons "TVarInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "tvarSource") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Range) :*: S1 ('MetaSel ('Just "tvarDesc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TypeSource))) |
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
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 |
TNewtype !Newtype ![Type] | A newtype |
Instances
TPModParam Name | |
TPUnifyVar | |
TPSchemaParam Name | |
TPTySynParam Name | |
TPPropSynParam Name | |
TPNewtypeParam Name | |
TPPrimParam Name |
Instances
Type parameters.
Instances
Eq TParam Source # | |
Ord TParam Source # | |
Show TParam Source # | |
Generic TParam Source # | |
NFData TParam Source # | |
Defined in Cryptol.TypeCheck.Type | |
PP TParam Source # | |
HasKind TParam Source # | |
ShowParseable TParam Source # | |
Defined in Cryptol.TypeCheck.Parseable | |
PP (WithNames TParam) Source # | |
type Rep TParam Source # | |
Defined in Cryptol.TypeCheck.Type type Rep TParam = D1 ('MetaData "TParam" "Cryptol.TypeCheck.Type" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" 'False) (C1 ('MetaCons "TParam" 'PrefixI 'True) ((S1 ('MetaSel ('Just "tpUnique") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Just "tpKind") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)) :*: (S1 ('MetaSel ('Just "tpFlav") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TPFlavor) :*: S1 ('MetaSel ('Just "tpInfo") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TVarInfo)))) |
The types of polymorphic values.
Instances
Eq Schema Source # | |
Show Schema Source # | |
Generic Schema Source # | |
NFData Schema Source # | |
Defined in Cryptol.TypeCheck.Type | |
PP Schema Source # | |
FVS Schema Source # | |
TVars Schema Source # | This instance does not need to worry about bound variable
capture, because we rely on the |
FreeVars Schema Source # | |
PP (WithNames Schema) Source # | |
type Rep Schema Source # | |
Defined in Cryptol.TypeCheck.Type type Rep Schema = D1 ('MetaData "Schema" "Cryptol.TypeCheck.Type" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" 'False) (C1 ('MetaCons "Forall" 'PrefixI 'True) (S1 ('MetaSel ('Just "sVars") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam]) :*: (S1 ('MetaSel ('Just "sProps") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Prop]) :*: S1 ('MetaSel ('Just "sType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Type)))) |
A value parameter of a module.
Instances
Show ModVParam Source # | |
Generic ModVParam Source # | |
NFData ModVParam Source # | |
Defined in Cryptol.TypeCheck.Type | |
type Rep ModVParam Source # | |
Defined in Cryptol.TypeCheck.Type type Rep ModVParam = D1 ('MetaData "ModVParam" "Cryptol.TypeCheck.Type" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" 'False) (C1 ('MetaCons "ModVParam" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mvpName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Just "mvpType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Schema)) :*: (S1 ('MetaSel ('Just "mvpDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text)) :*: S1 ('MetaSel ('Just "mvpFixity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Fixity))))) |
A type parameter of a module.
Instances
Show ModTParam Source # | |
Generic 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-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" '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 "mtpNumber") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Just "mtpDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text))))) |
schemaParam :: Name -> TPFlavor Source #
tySynParam :: Name -> TPFlavor Source #
propSynParam :: Name -> TPFlavor Source #
newtypeParam :: 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.
newtypeConType :: Newtype -> Schema Source #
abstractTypeTC :: AbstractType -> TCon 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.
noFreeVariables :: FVS t => t -> Bool Source #
ppNewtypeShort :: Newtype -> Doc Source #
pickTVarName :: Kind -> TypeSource -> Int -> Doc Source #
module Cryptol.TypeCheck.TCon