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 -> Type -> Prop
data NominalTypeDef
- = Struct StructCon
- | Enum [EnumCon]
- | Abstract
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
}
tArray :: Type -> Type -> 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)
}
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
class FVS t where
- fvs :: t -> Set TVar
tNum :: Integral a => a -> Type
tInf :: 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
tFun :: Type -> Type -> Type
tNominal :: NominalType -> [Type] -> Type
tMono :: Type -> Schema
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
tpName :: TParam -> Maybe Name
(=#=) :: Type -> Type -> Prop
(>==) :: Type -> Type -> Prop
type FunctorParams = Map Ident ModParam
allParamNames :: FunctorParams -> ModParamNames
data ModTParam = ModTParam {
- mtpName :: Name
- mtpKind :: Kind
- mtpDoc :: Maybe Text
}
data ModVParam = ModVParam {
- mvpName :: Name
- mvpType :: Schema
- mvpDoc :: Maybe Text
- mvpFixity :: Maybe Fixity
}
mtpParam :: ModTParam -> TParam
data TPFlavor
- = TPModParam Name
- | TPUnifyVar
- | TPSchemaParam Name
- | TPTySynParam Name
- | TPPropSynParam Name
- | TPNominalParam Name
- | TPPrimParam Name
data TVarInfo = TVarInfo {
- tvarSource :: !Range
- tvarDesc :: !TypeSource
}
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
data NominalType = NominalType {
- ntName :: Name
- ntParams :: [TParam]
- ntKind :: !Kind
- ntConstraints :: [Prop]
- ntDef :: NominalTypeDef
- ntDeriving :: Map PC [Prop]
- ntFixity :: !(Maybe Fixity)
- ntDoc :: Maybe Text
}
tvInfo :: TVar -> TVarInfo
tvUnique :: TVar -> Int
noArgDescr :: ArgDescr
tvSourceName :: TypeSource -> Maybe Name
data TypeWithSource = WithSource {
- twsType :: Type
- twsSource :: TypeSource
- twsRange :: !(Maybe Range)
}
data StructCon = StructCon {
- ntConName :: !Name
- ntFields :: RecordMap Ident Type
}
quickApply :: Kind -> [a] -> Kind
kindResult :: Kind -> Kind
tpVar :: TParam -> TVar
type SType = Type
superclassSet :: Prop -> Set Prop
pFin :: Type -> Prop
tTwo :: Type
typeSuperclassSet :: PC -> Set PC
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)
tZero :: Type
tOne :: Type
tNat' :: Nat' -> 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 :: PPCfg -> [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

Instance details

Defined in Cryptol.TypeCheck.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 #

ppPrecWithAnnot :: [([Int], PPAnnot)] -> 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 #

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> WithNames Type -> Doc Source #

type Rep Type Source #

Instance details

Defined in Cryptol.TypeCheck.Type

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

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

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep NominalTypeDef = D1 ('MetaData "NominalTypeDef" "Cryptol.TypeCheck.Type" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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)))

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.5.0-HoSGjqdyafy4TMoEJgOBMg" '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)))

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

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep TVar = D1 ('MetaData "TVar" "Cryptol.TypeCheck.Type" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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)))

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 #

ppPrecWithAnnot :: [([Int], PPAnnot)] -> 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 #

ppPrecWithAnnot :: [([Int], PPAnnot)] -> 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.5.0-HoSGjqdyafy4TMoEJgOBMg" '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

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep ArgDescr = D1 ('MetaData "ArgDescr" "Cryptol.TypeCheck.Type" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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))))

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 #

ppPrecWithAnnot :: [([Int], PPAnnot)] -> 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.5.0-HoSGjqdyafy4TMoEJgOBMg" '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

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep Schema = D1 ('MetaData "Schema" "Cryptol.TypeCheck.Type" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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))))

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 #

ppPrecWithAnnot :: [([Int], PPAnnot)] -> 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 #

ppPrecWithAnnot :: [([Int], PPAnnot)] -> 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.5.0-HoSGjqdyafy4TMoEJgOBMg" '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))))

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

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

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep TParam = D1 ('MetaData "TParam" "Cryptol.TypeCheck.Type" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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))))

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 #

ppPrecWithAnnot :: [([Int], PPAnnot)] -> 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 #

ppPrecWithAnnot :: [([Int], PPAnnot)] -> 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.5.0-HoSGjqdyafy4TMoEJgOBMg" '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

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep TySyn = D1 ('MetaData "TySyn" "Cryptol.TypeCheck.Type" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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))))))

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 #

ppPrecWithAnnot :: [([Int], PPAnnot)] -> 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 #

ppPrecWithAnnot :: [([Int], PPAnnot)] -> 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.5.0-HoSGjqdyafy4TMoEJgOBMg" '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

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep EnumCon = D1 ('MetaData "EnumCon" "Cryptol.TypeCheck.Type" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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))))))

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.5.0-HoSGjqdyafy4TMoEJgOBMg" '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

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep ModParam = D1 ('MetaData "ModParam" "Cryptol.TypeCheck.Type" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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))))

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.5.0-HoSGjqdyafy4TMoEJgOBMg" '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

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep ModParamNames = D1 ('MetaData "ModParamNames" "Cryptol.TypeCheck.Type" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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))))))

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 #

ppPrecWithAnnot :: [([Int], PPAnnot)] -> 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.5.0-HoSGjqdyafy4TMoEJgOBMg" '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))))))

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 #

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 #

tNum :: Integral a => a -> Type Source #

tInf :: Type Source #

tBit :: Type Source #

tInteger :: Type Source #

tRational :: Type Source #

tFloat :: Type -> Type -> Type Source #

tIntMod :: Type -> Type Source #

tWord :: Type -> Type Source #

tSeq :: Type -> Type -> Type Source #

tChar :: Type Source #

tString :: Int -> Type Source #

tRec :: RecordMap Ident Type -> Type Source #

tTuple :: [Type] -> Type Source #

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

Make a function type.

tNominal :: NominalType -> [Type] -> Type Source #

tMono :: Type -> Schema Source #

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

Instance details

Defined in Cryptol.TypeCheck.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 #

ppPrecWithAnnot :: [([Int], PPAnnot)] -> 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

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.

type FunctorParams = Map Ident ModParam Source #

allParamNames :: FunctorParams -> ModParamNames Source #

Compute the names from all functor parameters

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

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep ModTParam = D1 ('MetaData "ModTParam" "Cryptol.TypeCheck.Type" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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)))))

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 #

ppPrecWithAnnot :: [([Int], PPAnnot)] -> 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.5.0-HoSGjqdyafy4TMoEJgOBMg" '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

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep ModVParam = D1 ('MetaData "ModVParam" "Cryptol.TypeCheck.Type" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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)))))

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 #

ppPrecWithAnnot :: [([Int], PPAnnot)] -> 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.5.0-HoSGjqdyafy4TMoEJgOBMg" '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)))))

mtpParam :: ModTParam -> TParam Source #

This is how module parameters appear in actual types.

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

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep TPFlavor = D1 ('MetaData "TPFlavor" "Cryptol.TypeCheck.Type" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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)))))

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.5.0-HoSGjqdyafy4TMoEJgOBMg" '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 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

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep TVarInfo = D1 ('MetaData "TVarInfo" "Cryptol.TypeCheck.Type" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "TVarInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "tvarSource") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Range) :*: S1 ('MetaSel ('Just "tvarDesc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TypeSource)))

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 #

ppPrecWithAnnot :: [([Int], PPAnnot)] -> 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.5.0-HoSGjqdyafy4TMoEJgOBMg" 'False) (C1 ('MetaCons "TVarInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "tvarSource") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Range) :*: S1 ('MetaSel ('Just "tvarDesc") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TypeSource)))

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 #

data NominalType Source #

Nominal types

Constructors

NominalType

Fields

ntName :: Name
ntParams :: [TParam]
ntKind :: !Kind
Result kind
ntConstraints :: [Prop]
ntDef :: NominalTypeDef
ntDeriving :: Map PC [Prop]
Derived classes and their conditions (which may contain type variables).
For instance, if we have enum Maybe a = Nothing | Just a deriving (Eq), this map would be {Eq -> [Eq a]}, since the derived instance is instance (Eq a) => Eq (Maybe a).
ntFixity :: !(Maybe Fixity)
ntDoc :: Maybe Text

Instances

Instances details

Generic NominalType Source #

Instance details

Defined in Cryptol.TypeCheck.Type

Associated Types

type Rep NominalType

Instance details

Defined in Cryptol.TypeCheck.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 #

ppPrecWithAnnot :: [([Int], PPAnnot)] -> 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 #

ppPrecWithAnnot :: [([Int], PPAnnot)] -> Int -> WithNames NominalType -> Doc Source #

type Rep NominalType Source #

Instance details

Defined in Cryptol.TypeCheck.Type

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.

data TypeWithSource Source #

A type annotated with information on how it came about.

Constructors

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

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

Instance details

Defined in Cryptol.TypeCheck.Type

type Rep StructCon = D1 ('MetaData "StructCon" "Cryptol.TypeCheck.Type" "cryptol-3.5.0-HoSGjqdyafy4TMoEJgOBMg" '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))))

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.5.0-HoSGjqdyafy4TMoEJgOBMg" '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))))

quickApply :: Kind -> [a] -> Kind Source #

kindResult :: Kind -> Kind Source #

tpVar :: TParam -> TVar Source #

type SType = Type Source #

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

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 #

typeSuperclassSet :: PC -> Set PC Source #

Given a typeclass of kind * -> Prop, compute the set of all transitive superclasses of kind * -> Prop.

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 #