| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Cryptol.TypeCheck.Type
Synopsis
- class FVS t where
- type SType = Type
- data AbstractType = AbstractType {}
- data Newtype = Newtype {}
- data TySyn = TySyn {}
- type Prop = Type
- data TypeWithSource = WithSource {
- twsType :: Type
- twsSource :: TypeSource
- 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 {}
- 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.
Constructors
| AbstractType | |
Instances
Named records
Constructors
| Newtype | |
Instances
Type synonym.
Constructors
| TySyn | |
Instances
| Show TySyn Source # | |
| Generic TySyn Source # | |
| NFData TySyn Source # | |
Defined in Cryptol.TypeCheck.Type | |
| PP TySyn Source # | |
| HasKind 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.11.0-KBQWpCBm4GD4lGHyVVV39L" '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)))))) | |
data TypeWithSource Source #
A type annotated with information on how it came about.
Constructors
| WithSource | |
Fields
| |
Constructors
| ArgDescr | |
Fields
| |
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.11.0-KBQWpCBm4GD4lGHyVVV39L" '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.
Constructors
Instances
Constructors
| TVarInfo | |
Fields
| |
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.11.0-KBQWpCBm4GD4lGHyVVV39L" '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.
Constructors
| 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.
Constructors
| 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
Constructors
| TPModParam Name | |
| TPUnifyVar | |
| TPSchemaParam Name | |
| TPTySynParam Name | |
| TPPropSynParam Name | |
| TPNewtypeParam Name | |
| TPPrimParam Name |
Instances
Type parameters.
Constructors
| TParam | |
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 Methods showParseable :: TParam -> Doc Source # | |
| PP (WithNames TParam) Source # | |
| type Rep TParam Source # | |
Defined in Cryptol.TypeCheck.Type type Rep TParam = D1 ('MetaData "TParam" "Cryptol.TypeCheck.Type" "cryptol-2.11.0-KBQWpCBm4GD4lGHyVVV39L" '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.11.0-KBQWpCBm4GD4lGHyVVV39L" '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)))) | |
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 Props 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