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 FreeAbstract t where
- freeAbstract :: t -> Set UserTC
- 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 {}
- data ModParamNames = ModParamNames {}
- data ModParam = ModParam {
- mpName :: Ident
- mpQual :: !(Maybe ModName)
- mpIface :: ImpName Name
- mpParameters :: ModParamNames
- type FunctorParams = Map Ident ModParam
- allParamNames :: FunctorParams -> ModParamNames
- 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
- pNegNumeric :: Prop -> [Prop]
- noFreeVariables :: FVS t => t -> Bool
- freeParams :: FVS t => t -> Set TParam
- addTNames :: [TParam] -> NameMap -> NameMap
- ppNewtypeShort :: Newtype -> Doc
- ppNewtypeFull :: Newtype -> Doc
- pickTVarName :: Kind -> TypeSource -> Int -> Doc
- module Cryptol.TypeCheck.TCon
Documentation
class FreeAbstract t where Source #
Find the abstract types mentioned in a type.
freeAbstract :: t -> Set UserTC Source #
Instances
FreeAbstract TCon Source # | |
Defined in Cryptol.TypeCheck.Type | |
FreeAbstract Type Source # | |
Defined in Cryptol.TypeCheck.Type | |
FreeAbstract a => FreeAbstract [a] Source # | |
Defined in Cryptol.TypeCheck.Type freeAbstract :: [a] -> Set UserTC Source # | |
(FreeAbstract a, FreeAbstract b) => FreeAbstract (a, b) Source # | |
Defined in Cryptol.TypeCheck.Type freeAbstract :: (a, b) -> Set UserTC Source # |
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 # | |
data AbstractType Source #
Information about an abstract type.
Instances
Named records
Instances
Type synonym.
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.0.0-CoAB0rhRDtyEduZtDlyHHM" '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
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.0.0-CoAB0rhRDtyEduZtDlyHHM" '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
The types of polymorphic values.
Instances
A value parameter of a module.
Instances
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.0.0-CoAB0rhRDtyEduZtDlyHHM" '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))))) |
data ModParamNames Source #
Information about the names brought in through an "interface import". This is also used to keep information about.
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.0.0-CoAB0rhRDtyEduZtDlyHHM" '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)))) |
allParamNames :: FunctorParams -> ModParamNames Source #
Compute the names from all functor parameters
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.
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 #
ppNewtypeShort :: Newtype -> Doc Source #
ppNewtypeFull :: Newtype -> Doc Source #
pickTVarName :: Kind -> TypeSource -> Int -> Doc Source #
module Cryptol.TypeCheck.TCon