Safe Haskell	Safe
Language	Haskell2010

Cryptol.TypeCheck.Type

Description

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
- = TCon !TCon ![Type]
- | TVar TVar
- | TUser !Name ![Type] !Type
- | TRec !(RecordMap Ident Type)
- | TNominal !NominalType ![Type]
type Prop = Type
data TVar
- = TVFree !Int Kind (Set TParam) TVarInfo
- | TVBound !TParam
data ArgDescr = ArgDescr {
- argDescrFun :: Maybe Name
- argDescrNumber :: Maybe Int
}
data Schema = Forall {
- sVars :: [TParam]
- sProps :: [Prop]
- sType :: Type
}
data TParam = TParam {
- tpUnique :: !Int
- tpKind :: Kind
- tpFlav :: TPFlavor
- tpInfo :: !TVarInfo
}
data TySyn = TySyn {
- tsName :: Name
- tsParams :: [TParam]
- tsConstraints :: [Prop]
- tsDef :: Type
- tsDoc :: !(Maybe Text)
}
data EnumCon = EnumCon {
- ecName :: Name
- ecNumber :: !Int
- ecFields :: [Type]
- ecPublic :: Bool
- ecDoc :: Maybe Text
}
data ModParam = ModParam {
- mpName :: Ident
- mpQual :: !(Maybe ModName)
- mpIface :: ImpName Name
- mpParameters :: ModParamNames
}
data ModParamNames = ModParamNames {
- mpnTypes :: Map Name ModTParam
- mpnTySyn :: !(Map Name TySyn)
- mpnConstraints :: [Located Prop]
- mpnFuns :: Map Name ModVParam
- mpnDoc :: !(Maybe Text)
}
class FVS t where
- fvs :: t -> Set TVar
type FunctorParams = Map Ident ModParam
data ModTParam = ModTParam {
- mtpName :: Name
- mtpKind :: Kind
- mtpDoc :: Maybe Text
}
data ModVParam = ModVParam {
- mvpName :: Name
- mvpType :: Schema
- mvpDoc :: Maybe Text
- mvpFixity :: Maybe Fixity
}
data TVarInfo = TVarInfo {
- tvarSource :: !Range
- tvarDesc :: !TypeSource
}
data TPFlavor
- = TPModParam Name
- | TPUnifyVar
- | TPSchemaParam Name
- | TPTySynParam Name
- | TPPropSynParam Name
- | TPNominalParam Name
- | TPPrimParam Name
data NominalType = NominalType {
- ntName :: Name
- ntParams :: [TParam]
- ntKind :: !Kind
- ntConstraints :: [Prop]
- ntDef :: NominalTypeDef
- ntFixity :: !(Maybe Fixity)
- ntDoc :: Maybe Text
}
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 {
- twsType :: Type
- twsSource :: TypeSource
- twsRange :: !(Maybe Range)
}
data NominalTypeDef
- = Struct StructCon
- | Enum [EnumCon]
- | Abstract
data StructCon = StructCon {
- ntConName :: !Name
- ntFields :: RecordMap Ident Type
}
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)
tIsNominal :: Type -> Maybe (NominalType, [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

data Type Source #

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: `TUser T ts t` is really just the type `t` that was written as `T ts` by the user.
TRec !(RecordMap Ident Type)	Record type
TNominal !NominalType ![Type]	A nominal types

Instances

Instances details

Generic Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep Type :: Type -> Type # Methods from :: Type -> Rep Type x # to :: Rep Type x -> Type #
Show Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> Type -> ShowS # show :: Type -> String # showList :: [Type] -> ShowS #
FreeVars Type Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: Type -> Deps Source #
TraverseNames Type Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => Type -> f Type Source #
ModuleInstance Type Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: Type -> Type Source #
ShowParseable Type Source #
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Type -> Doc Void Source #
TVars Type Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Type -> Type Source #
HasKind Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: Type -> Kind Source #
FVS Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Type -> Set TVar Source #
PP Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> Type -> Doc Source #
NFData Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: Type -> () #
Eq Type Source #	Syntactic equality, ignoring type synonyms and record order.
Instance details Defined in Cryptol.TypeCheck.Type Methods (==) :: Type -> Type -> Bool # (/=) :: Type -> Type -> Bool #
Ord Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods compare :: Type -> Type -> Ordering # (<) :: Type -> Type -> Bool # (<=) :: Type -> Type -> Bool # (>) :: Type -> Type -> Bool # (>=) :: Type -> Type -> Bool # max :: Type -> Type -> Type # min :: Type -> Type -> Type #
TrieMap TypeMap Type Source #
Instance details Defined in Cryptol.TypeCheck.TypeMap Methods emptyTM :: TypeMap a Source # nullTM :: TypeMap a -> Bool Source # lookupTM :: Type -> TypeMap a -> Maybe a Source # alterTM :: Type -> (Maybe a -> Maybe a) -> TypeMap a -> TypeMap a Source # unionTM :: (a -> a -> a) -> TypeMap a -> TypeMap a -> TypeMap a Source # toListTM :: TypeMap a -> [(Type, a)] Source # mapMaybeWithKeyTM :: (Type -> a -> Maybe b) -> TypeMap a -> TypeMap b Source #
PP (WithNames Type) Source #	The precedence levels used by this pretty-printing instance correspond with parser non-terminals as follows: 0-1: `type` 2: `infix_type` 3: `app_type` 4: `dimensions atype` 5: `atype`
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames Type -> Doc Source #
type Rep Type Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep Type = D1 ('MetaData "Type" "Cryptol.TypeCheck.Type" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" 'False) ((C1 ('MetaCons "TCon" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TCon) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Type])) :+: C1 ('MetaCons "TVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TVar))) :+: (C1 ('MetaCons "TUser" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Name) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Type]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Type))) :+: (C1 ('MetaCons "TRec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (RecordMap Ident Type))) :+: C1 ('MetaCons "TNominal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 NominalType) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Type])))))

type Prop = Type Source #

The type is supposed to be of kind KProp.

data TVar Source #

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

Instances details

Generic TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep TVar :: Type -> Type # Methods from :: TVar -> Rep TVar x # to :: Rep TVar x -> TVar #
Show TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TVar -> ShowS # show :: TVar -> String # showList :: [TVar] -> ShowS #
FreeVars TVar Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: TVar -> Deps Source #
TraverseNames TVar Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => TVar -> f TVar Source #
HasKind TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: TVar -> Kind Source #
PP TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TVar -> Doc Source #
NFData TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TVar -> () #
Eq TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods (==) :: TVar -> TVar -> Bool # (/=) :: TVar -> TVar -> Bool #
Ord TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods compare :: TVar -> TVar -> Ordering # (<) :: TVar -> TVar -> Bool # (<=) :: TVar -> TVar -> Bool # (>) :: TVar -> TVar -> Bool # (>=) :: TVar -> TVar -> Bool # max :: TVar -> TVar -> TVar # min :: TVar -> TVar -> TVar #
PP (WithNames TVar) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames TVar -> Doc Source #
type Rep TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep TVar = D1 ('MetaData "TVar" "Cryptol.TypeCheck.Type" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" 'False) (C1 ('MetaCons "TVFree" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set TParam)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TVarInfo))) :+: C1 ('MetaCons "TVBound" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 TParam)))

data ArgDescr Source #

Constructors

ArgDescr
Fields argDescrFun :: Maybe Name argDescrNumber :: Maybe Int

Instances

Instances details

Generic ArgDescr Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep ArgDescr :: Type -> Type # Methods from :: ArgDescr -> Rep ArgDescr x # to :: Rep ArgDescr x -> ArgDescr #
Show ArgDescr Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> ArgDescr -> ShowS # show :: ArgDescr -> String # showList :: [ArgDescr] -> ShowS #
TraverseNames ArgDescr Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => ArgDescr -> f ArgDescr Source #
PP ArgDescr Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> ArgDescr -> Doc Source #
NFData ArgDescr Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: ArgDescr -> () #
type Rep ArgDescr Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep ArgDescr = D1 ('MetaData "ArgDescr" "Cryptol.TypeCheck.Type" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" '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 Schema Source #

The types of polymorphic values.

Constructors

Forall
Fields sVars :: [TParam] sProps :: [Prop] sType :: Type

Instances

Instances details

Generic Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep Schema :: Type -> Type # Methods from :: Schema -> Rep Schema x # to :: Rep Schema x -> Schema #
Show Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> Schema -> ShowS # show :: Schema -> String # showList :: [Schema] -> ShowS #
FreeVars Schema Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: Schema -> Deps Source #
TraverseNames Schema Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => Schema -> f Schema Source #
ModuleInstance Schema Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: Schema -> Schema Source #
TVars Schema Source #	This instance does not need to worry about bound variable capture, because we rely on the `Subst` datatype invariant to ensure that variable scopes will be properly preserved.
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Schema -> Schema Source #
FVS Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Schema -> Set TVar Source #
PP Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> Schema -> Doc Source #
NFData Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: Schema -> () #
Eq Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods (==) :: Schema -> Schema -> Bool # (/=) :: Schema -> Schema -> Bool #
PP (WithNames Schema) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames Schema -> Doc Source #
type Rep Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep Schema = D1 ('MetaData "Schema" "Cryptol.TypeCheck.Type" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" '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))))

data TParam Source #

Type parameters.

Constructors

TParam
Fields tpUnique :: !Int Parameter identifier tpKind :: Kind Kind of parameter tpFlav :: TPFlavor What sort of type parameter is this tpInfo :: !TVarInfo A description for better messages.

Instances

Instances details

Generic TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep TParam :: Type -> Type # Methods from :: TParam -> Rep TParam x # to :: Rep TParam x -> TParam #
Show TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TParam -> ShowS # show :: TParam -> String # showList :: [TParam] -> ShowS #
TraverseNames TParam Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => TParam -> f TParam Source #
ShowParseable TParam Source #
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: TParam -> Doc Void Source #
HasKind TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: TParam -> Kind Source #
PP TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TParam -> Doc Source #
NFData TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TParam -> () #
Eq TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods (==) :: TParam -> TParam -> Bool # (/=) :: TParam -> TParam -> Bool #
Ord TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods compare :: TParam -> TParam -> Ordering # (<) :: TParam -> TParam -> Bool # (<=) :: TParam -> TParam -> Bool # (>) :: TParam -> TParam -> Bool # (>=) :: TParam -> TParam -> Bool # max :: TParam -> TParam -> TParam # min :: TParam -> TParam -> TParam #
PP (WithNames TParam) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames TParam -> Doc Source #
type Rep TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep TParam = D1 ('MetaData "TParam" "Cryptol.TypeCheck.Type" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" '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))))

data TySyn Source #

Type synonym.

Constructors

TySyn
Fields tsName :: Name Name tsParams :: [TParam] Parameters tsConstraints :: [Prop] Ensure body is OK tsDef :: Type Definition tsDoc :: !(Maybe Text) Documentation

Instances

Instances details

Generic TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep TySyn :: Type -> Type # Methods from :: TySyn -> Rep TySyn x # to :: Rep TySyn x -> TySyn #
Show TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TySyn -> ShowS # show :: TySyn -> String # showList :: [TySyn] -> ShowS #
TraverseNames TySyn Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => TySyn -> f TySyn Source #
ModuleInstance TySyn Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: TySyn -> TySyn Source #
TVars TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> TySyn -> TySyn Source #
HasKind TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: TySyn -> Kind Source #
PP TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TySyn -> Doc Source #
NFData TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TySyn -> () #
PP (WithNames TySyn) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames TySyn -> Doc Source #
type Rep TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep TySyn = D1 ('MetaData "TySyn" "Cryptol.TypeCheck.Type" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" '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 EnumCon Source #

Constructor for an enumeration

Constructors

EnumCon
Fields ecName :: Name ecNumber :: !Int Number of constructor in the declaration ecFields :: [Type] ecPublic :: Bool ecDoc :: Maybe Text

Instances

Instances details

Generic EnumCon Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep EnumCon :: Type -> Type # Methods from :: EnumCon -> Rep EnumCon x # to :: Rep EnumCon x -> EnumCon #
Show EnumCon Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> EnumCon -> ShowS # show :: EnumCon -> String # showList :: [EnumCon] -> ShowS #
FreeVars EnumCon Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: EnumCon -> Deps Source #
TraverseNames EnumCon Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => EnumCon -> f EnumCon Source #
ModuleInstance EnumCon Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: EnumCon -> EnumCon Source #
NFData EnumCon Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: EnumCon -> () #
type Rep EnumCon Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep EnumCon = D1 ('MetaData "EnumCon" "Cryptol.TypeCheck.Type" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" 'False) (C1 ('MetaCons "EnumCon" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ecName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Just "ecNumber") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)) :: (S1 ('MetaSel ('Just "ecFields") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Type]) :: (S1 ('MetaSel ('Just "ecPublic") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "ecDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text))))))

data ModParam Source #

A module parameter. Corresponds to a "signature import". A single module parameter can bring multiple things in scope.

Constructors

ModParam

Fields

mpName :: Ident
The name of a functor parameter.
mpQual :: !(Maybe ModName)
This is the qualifier for the parameter. We use it to derive parameter names when doing `_` imports.
mpIface :: ImpName Name
The interface corresponding to this parameter. This is thing in `import interface`
mpParameters :: ModParamNames
These are the actual parameters, not the ones in the interface For example if the same interface is used for multiple parameters the ifmpParameters would all be different.

Instances

Instances details

Generic ModParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep ModParam :: Type -> Type # Methods from :: ModParam -> Rep ModParam x # to :: Rep ModParam x -> ModParam #
Show ModParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> ModParam -> ShowS # show :: ModParam -> String # showList :: [ModParam] -> ShowS #
ModuleInstance ModParam Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: ModParam -> ModParam Source #
NFData ModParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: ModParam -> () #
type Rep ModParam Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep ModParam = D1 ('MetaData "ModParam" "Cryptol.TypeCheck.Type" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" '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.

Constructors

ModParamNames
Fields mpnTypes :: Map Name ModTParam Type parameters mpnTySyn :: !(Map Name TySyn) Type synonyms mpnConstraints :: [Located Prop] Constraints on param. types mpnFuns :: Map Name ModVParam Value parameters mpnDoc :: !(Maybe Text) Documentation about the interface.

Instances

Instances details

Generic ModParamNames Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep ModParamNames :: Type -> Type # Methods from :: ModParamNames -> Rep ModParamNames x # to :: Rep ModParamNames x -> ModParamNames #
Show ModParamNames Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> ModParamNames -> ShowS # show :: ModParamNames -> String # showList :: [ModParamNames] -> ShowS #
ModuleInstance ModParamNames Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: ModParamNames -> ModParamNames Source #
PP ModParamNames Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> ModParamNames -> Doc Source #
NFData ModParamNames Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: ModParamNames -> () #
type Rep ModParamNames Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep ModParamNames = D1 ('MetaData "ModParamNames" "Cryptol.TypeCheck.Type" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" 'False) (C1 ('MetaCons "ModParamNames" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mpnTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name ModTParam)) :: S1 ('MetaSel ('Just "mpnTySyn") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Map Name TySyn))) :: (S1 ('MetaSel ('Just "mpnConstraints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Located Prop]) :: (S1 ('MetaSel ('Just "mpnFuns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Name ModVParam)) :: S1 ('MetaSel ('Just "mpnDoc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Text))))))

class FVS t where Source #

Methods

fvs :: t -> Set TVar Source #

Instances

Instances details

FVS Error Source #
Instance details Defined in Cryptol.TypeCheck.Error Methods fvs :: Error -> Set TVar Source #
FVS Warning Source #
Instance details Defined in Cryptol.TypeCheck.Error Methods fvs :: Warning -> Set TVar Source #
FVS FFITypeError Source #
Instance details Defined in Cryptol.TypeCheck.FFI.Error Methods fvs :: FFITypeError -> Set TVar Source #
FVS FFITypeErrorReason Source #
Instance details Defined in Cryptol.TypeCheck.FFI.Error Methods fvs :: FFITypeErrorReason -> Set TVar Source #
FVS DelayedCt Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods fvs :: DelayedCt -> Set TVar Source #
FVS Goal Source #
Instance details Defined in Cryptol.TypeCheck.InferTypes Methods fvs :: Goal -> Set TVar Source #
FVS Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Schema -> Set TVar Source #
FVS Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Type -> Set TVar Source #
FVS a => FVS (Maybe a) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Maybe a -> Set TVar Source #
FVS a => FVS [a] Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: [a] -> Set TVar Source #
(FVS a, FVS b) => FVS (a, b) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: (a, b) -> Set TVar Source #

type FunctorParams = Map Ident ModParam Source #

data ModTParam Source #

A type parameter of a module.

Constructors

ModTParam
Fields mtpName :: Name mtpKind :: Kind mtpDoc :: Maybe Text

Instances

Instances details

Generic ModTParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep ModTParam :: Type -> Type # Methods from :: ModTParam -> Rep ModTParam x # to :: Rep ModTParam x -> ModTParam #
Show ModTParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> ModTParam -> ShowS # show :: ModTParam -> String # showList :: [ModTParam] -> ShowS #
TraverseNames ModTParam Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => ModTParam -> f ModTParam Source #
ModuleInstance ModTParam Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: ModTParam -> ModTParam Source #
PP ModTParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> ModTParam -> Doc Source #
NFData ModTParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: ModTParam -> () #
type Rep ModTParam Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep ModTParam = D1 ('MetaData "ModTParam" "Cryptol.TypeCheck.Type" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" '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 ModVParam Source #

A value parameter of a module.

Constructors

ModVParam
Fields mvpName :: Name mvpType :: Schema mvpDoc :: Maybe Text mvpFixity :: Maybe Fixity

Instances

Instances details

Generic ModVParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep ModVParam :: Type -> Type # Methods from :: ModVParam -> Rep ModVParam x # to :: Rep ModVParam x -> ModVParam #
Show ModVParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> ModVParam -> ShowS # show :: ModVParam -> String # showList :: [ModVParam] -> ShowS #
TraverseNames ModVParam Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => ModVParam -> f ModVParam Source #
ModuleInstance ModVParam Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: ModVParam -> ModVParam Source #
PP ModVParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> ModVParam -> Doc Source #
NFData ModVParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: ModVParam -> () #
type Rep ModVParam Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep ModVParam = D1 ('MetaData "ModVParam" "Cryptol.TypeCheck.Type" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" '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)))))

data TVarInfo Source #

Constructors

TVarInfo
Fields tvarSource :: !Range Source code that gave rise tvarDesc :: !TypeSource Description

Instances

Instances details

Generic TVarInfo Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep TVarInfo :: Type -> Type # Methods from :: TVarInfo -> Rep TVarInfo x # to :: Rep TVarInfo x -> TVarInfo #
Show TVarInfo Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TVarInfo -> ShowS # show :: TVarInfo -> String # showList :: [TVarInfo] -> ShowS #
TraverseNames TVarInfo Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => TVarInfo -> f TVarInfo Source #
PP TVarInfo Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TVarInfo -> Doc Source #
NFData TVarInfo Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TVarInfo -> () #
type Rep TVarInfo Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep TVarInfo = D1 ('MetaData "TVarInfo" "Cryptol.TypeCheck.Type" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" 'False) (C1 ('MetaCons "TVarInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "tvarSource") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Range) :*: S1 ('MetaSel ('Just "tvarDesc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TypeSource)))

data TPFlavor Source #

Constructors

TPModParam Name
TPUnifyVar
TPSchemaParam Name
TPTySynParam Name
TPPropSynParam Name
TPNominalParam Name
TPPrimParam Name

Instances

Instances details

Generic TPFlavor Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep TPFlavor :: Type -> Type # Methods from :: TPFlavor -> Rep TPFlavor x # to :: Rep TPFlavor x -> TPFlavor #
Show TPFlavor Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TPFlavor -> ShowS # show :: TPFlavor -> String # showList :: [TPFlavor] -> ShowS #
TraverseNames TPFlavor Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => TPFlavor -> f TPFlavor Source #
NFData TPFlavor Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TPFlavor -> () #
type Rep TPFlavor Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep TPFlavor = D1 ('MetaData "TPFlavor" "Cryptol.TypeCheck.Type" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" 'False) ((C1 ('MetaCons "TPModParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: (C1 ('MetaCons "TPUnifyVar" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TPSchemaParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)))) :+: ((C1 ('MetaCons "TPTySynParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "TPPropSynParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name))) :+: (C1 ('MetaCons "TPNominalParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "TPPrimParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)))))

data NominalType Source #

Nominal types

Constructors

NominalType
Fields ntName :: Name ntParams :: [TParam] ntKind :: !Kind Result kind ntConstraints :: [Prop] ntDef :: NominalTypeDef ntFixity :: !(Maybe Fixity) ntDoc :: Maybe Text

Instances

Instances details

Generic NominalType Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep NominalType :: Type -> Type # Methods from :: NominalType -> Rep NominalType x # to :: Rep NominalType x -> NominalType #
Show NominalType Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> NominalType -> ShowS # show :: NominalType -> String # showList :: [NominalType] -> ShowS #
FreeVars NominalType Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: NominalType -> Deps Source #
TraverseNames NominalType Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => NominalType -> f NominalType Source #
ModuleInstance NominalType Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: NominalType -> NominalType Source #
HasKind NominalType Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: NominalType -> Kind Source #
PP NominalType Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> NominalType -> Doc Source #
NFData NominalType Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: NominalType -> () #
Eq NominalType Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods (==) :: NominalType -> NominalType -> Bool # (/=) :: NominalType -> NominalType -> Bool #
Ord NominalType Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods compare :: NominalType -> NominalType -> Ordering # (<) :: NominalType -> NominalType -> Bool # (<=) :: NominalType -> NominalType -> Bool # (>) :: NominalType -> NominalType -> Bool # (>=) :: NominalType -> NominalType -> Bool # max :: NominalType -> NominalType -> NominalType # min :: NominalType -> NominalType -> NominalType #
PP (WithNames NominalType) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames NominalType -> Doc Source #
type Rep NominalType Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep NominalType = D1 ('MetaData "NominalType" "Cryptol.TypeCheck.Type" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" 'False) (C1 ('MetaCons "NominalType" 'PrefixI 'True) ((S1 ('MetaSel ('Just "ntName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: (S1 ('MetaSel ('Just "ntParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TParam]) :: S1 ('MetaSel ('Just "ntKind") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Kind))) :: ((S1 ('MetaSel ('Just "ntConstraints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Prop]) :: S1 ('MetaSel ('Just "ntDef") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NominalTypeDef)) :: (S1 ('MetaSel ('Just "ntFixity") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Maybe Fixity)) :: S1 ('MetaSel ('Just "ntDoc") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Text))))))

data TypeSource Source #

Explains how this type came to be, for better error messages.

Constructors

TVFromModParam Name	Name of module parameter
TVFromSignature Name	A variable in a signature
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

Instances

Instances details

Generic TypeSource Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep TypeSource :: Type -> Type # Methods from :: TypeSource -> Rep TypeSource x # to :: Rep TypeSource x -> TypeSource #
Show TypeSource Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TypeSource -> ShowS # show :: TypeSource -> String # showList :: [TypeSource] -> ShowS #
TraverseNames TypeSource Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => TypeSource -> f TypeSource Source #
PP TypeSource Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TypeSource -> Doc Source #
NFData TypeSource Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TypeSource -> () #
type Rep TypeSource Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep TypeSource = D1 ('MetaData "TypeSource" "Cryptol.TypeCheck.Type" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" 'False) ((((C1 ('MetaCons "TVFromModParam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)) :+: C1 ('MetaCons "TVFromSignature" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name))) :+: (C1 ('MetaCons "TypeWildCard" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TypeOfRecordField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident)) :+: C1 ('MetaCons "TypeOfTupleField" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))))) :+: ((C1 ('MetaCons "TypeOfSeqElement" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "LenOfSeq" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TypeParamInstNamed" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident)) :+: (C1 ('MetaCons "TypeParamInstPos" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "DefinitionOf" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name)))))) :+: (((C1 ('MetaCons "LenOfCompGen" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TypeOfArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgDescr))) :+: (C1 ('MetaCons "TypeOfRes" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FunApp" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TypeOfIfCondExpr" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "TypeFromUserAnnotation" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "GeneratorOfListComp" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CasedExpression" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ConPat" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TypeErrorPlaceHolder" 'PrefixI 'False) (U1 :: Type -> Type))))))

data TypeWithSource Source #

A type annotated with information on how it came about.

Constructors

WithSource
Fields twsType :: Type twsSource :: TypeSource twsRange :: !(Maybe Range)

data NominalTypeDef Source #

Definition of a nominal type

Constructors

Struct StructCon
Enum [EnumCon]
Abstract

Instances

Instances details

Generic NominalTypeDef Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep NominalTypeDef :: Type -> Type # Methods from :: NominalTypeDef -> Rep NominalTypeDef x # to :: Rep NominalTypeDef x -> NominalTypeDef #
Show NominalTypeDef Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> NominalTypeDef -> ShowS # show :: NominalTypeDef -> String # showList :: [NominalTypeDef] -> ShowS #
FreeVars NominalTypeDef Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: NominalTypeDef -> Deps Source #
TraverseNames NominalTypeDef Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => NominalTypeDef -> f NominalTypeDef Source #
ModuleInstance NominalTypeDef Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: NominalTypeDef -> NominalTypeDef Source #
NFData NominalTypeDef Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: NominalTypeDef -> () #
type Rep NominalTypeDef Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep NominalTypeDef = D1 ('MetaData "NominalTypeDef" "Cryptol.TypeCheck.Type" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" 'False) (C1 ('MetaCons "Struct" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 StructCon)) :+: (C1 ('MetaCons "Enum" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [EnumCon])) :+: C1 ('MetaCons "Abstract" 'PrefixI 'False) (U1 :: Type -> Type)))

data StructCon Source #

Constructor for a struct (aka newtype)

Constructors

StructCon
Fields ntConName :: !Name ntFields :: RecordMap Ident Type

Instances

Instances details

Generic StructCon Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep StructCon :: Type -> Type # Methods from :: StructCon -> Rep StructCon x # to :: Rep StructCon x -> StructCon #
Show StructCon Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> StructCon -> ShowS # show :: StructCon -> String # showList :: [StructCon] -> ShowS #
FreeVars StructCon Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: StructCon -> Deps Source #
TraverseNames StructCon Source #
Instance details Defined in Cryptol.IR.TraverseNames Methods traverseNamesIP :: (Applicative f, ?name :: Name -> f Name) => StructCon -> f StructCon Source #
ModuleInstance StructCon Source #
Instance details Defined in Cryptol.TypeCheck.ModuleInstance Methods moduleInstance :: StructCon -> StructCon Source #
NFData StructCon Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: StructCon -> () #
type Rep StructCon Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep StructCon = D1 ('MetaData "StructCon" "Cryptol.TypeCheck.Type" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" '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))))

type SType = Type Source #

The type is "simple" (i.e., it contains no type functions).

(=/=) :: Type -> Type -> Prop Source #

tArray :: Type -> Type -> Type Source #

tSub :: Type -> Type -> Type Source #

tMul :: Type -> Type -> Type Source #

tDiv :: Type -> Type -> Type Source #

tMod :: Type -> Type -> Type Source #

tExp :: Type -> Type -> Type Source #

tMin :: Type -> Type -> Type Source #

tCeilDiv :: Type -> Type -> Type Source #

tCeilMod :: Type -> Type -> Type Source #

tLenFromThenTo :: Type -> Type -> Type -> Type Source #

tpName :: TParam -> Maybe Name Source #

(=#=) :: Type -> Type -> Prop infix 4 Source #

Equality for numeric types.

(>==) :: Type -> Type -> Prop infix 4 Source #

Make a greater-than-or-equal-to constraint.

tFun :: Type -> Type -> Type infixr 5 Source #

Make a function type.

allParamNames :: FunctorParams -> ModParamNames Source #

Compute the names from all functor parameters

mtpParam :: ModTParam -> TParam Source #

This is how module parameters appear in actual types.

tMono :: Type -> Schema Source #

isMono :: Schema -> Maybe Type Source #

schemaParam :: Name -> TPFlavor Source #

tySynParam :: Name -> TPFlavor Source #

propSynParam :: Name -> TPFlavor Source #

nominalParam :: Name -> TPFlavor Source #

primParam :: Name -> TPFlavor Source #

modTyParam :: Name -> TPFlavor Source #

tpfName :: TPFlavor -> Maybe Name Source #

tvInfo :: TVar -> TVarInfo Source #

tvUnique :: TVar -> Int Source #

noArgDescr :: ArgDescr 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 #

tpVar :: TParam -> TVar Source #

superclassSet :: Prop -> Set Prop Source #

Compute the set of all Props that are implied by the given prop via superclass constraints.

pFin :: Type -> Prop Source #

tTwo :: Type Source #

nominalTypeConTypes :: NominalType -> [(Name, Schema)] Source #

nominalTypeIsAbstract :: NominalType -> Bool Source #

isFreeTV :: TVar -> Bool Source #

isBoundTV :: TVar -> Bool Source #

tIsError :: Type -> Maybe Type Source #

tNoUser :: Type -> Type Source #

Eliminate outermost type synonyms.

tHasErrors :: Type -> Bool Source #

tIsNat' :: Type -> Maybe Nat' Source #

tIsNum :: Type -> Maybe Integer Source #

tIsInf :: Type -> Bool Source #

tIsVar :: Type -> Maybe TVar Source #

tIsFun :: Type -> Maybe (Type, Type) Source #

tIsSeq :: Type -> Maybe (Type, Type) Source #

tIsBit :: Type -> Bool Source #

tIsInteger :: Type -> Bool Source #

tIsIntMod :: Type -> Maybe Type Source #

tIsRational :: Type -> Bool Source #

tIsFloat :: Type -> Maybe (Type, Type) Source #

tIsTuple :: Type -> Maybe [Type] Source #

tIsRec :: Type -> Maybe (RecordMap Ident Type) Source #

tIsNominal :: Type -> Maybe (NominalType, [Type]) Source #

If the supplied Type is a TNominal type, then return Just (nt, ts), where nt and ts are the underlying NominalType and Type arguments. Otherwise, return Nothing.

tIsBinFun :: TFun -> Type -> Maybe (Type, Type) Source #

tSplitFun :: TFun -> Type -> [Type] Source #

Split up repeated occurances of the given binary type-level function.

pIsFin :: Prop -> Maybe Type Source #

pIsPrime :: Prop -> Maybe Type Source #

pIsGeq :: Prop -> Maybe (Type, Type) Source #

pIsEqual :: Prop -> Maybe (Type, Type) Source #

pIsZero :: Prop -> Maybe Type Source #

pIsLogic :: Prop -> Maybe Type Source #

pIsRing :: Prop -> Maybe Type Source #

pIsField :: Prop -> Maybe Type Source #

pIsIntegral :: Prop -> Maybe Type Source #