Safe Haskell	Safe
Language	Haskell2010

Cryptol.TypeCheck.Type

Synopsis

class FVS t where
- fvs :: t -> Set TVar
type SType = Type
data AbstractType = AbstractType {
- atName :: Name
- atKind :: Kind
- atCtrs :: ([TParam], [Prop])
- atFixitiy :: Maybe Fixity
- atDoc :: Maybe String
}
data Newtype = Newtype {
- ntName :: Name
- ntParams :: [TParam]
- ntConstraints :: [Prop]
- ntFields :: [(Ident, Type)]
- ntDoc :: Maybe String
}
data TySyn = TySyn {
- tsName :: Name
- tsParams :: [TParam]
- tsConstraints :: [Prop]
- tsDef :: Type
- tsDoc :: !(Maybe String)
}
type Prop = Type
data TVarSource
- = TVFromModParam Name
- | TVFromSignature Name
- | TypeWildCard
- | TypeOfRecordField Ident
- | TypeOfTupleField Int
- | TypeOfSeqElement
- | LenOfSeq
- | TypeParamInstNamed Name Ident
- | TypeParamInstPos Name Int
- | DefinitionOf Name
- | LenOfCompGen
- | TypeOfArg (Maybe Int)
- | TypeOfRes
- | TypeErrorPlaceHolder
data TVarInfo = TVarInfo {
- tvarSource :: Range
- tvarDesc :: TVarSource
}
data TVar
- = TVFree !Int Kind (Set TParam) TVarInfo
- | TVBound !TParam
data Type
- = TCon !TCon ![Type]
- | TVar TVar
- | TUser !Name ![Type] !Type
- | TRec !(RecordMap Ident Type)
data TPFlavor
- = TPModParam Name
- | TPOther (Maybe Name)
data TParam = TParam {
- tpUnique :: !Int
- tpKind :: Kind
- tpFlav :: TPFlavor
- tpInfo :: !TVarInfo
}
data Schema = Forall {
- sVars :: [TParam]
- sProps :: [Prop]
- sType :: Type
}
tMono :: Type -> Schema
isMono :: Schema -> Maybe Type
schemaParam :: Name -> TPFlavor
tySynParam :: Name -> TPFlavor
propSynParam :: Name -> TPFlavor
newtypeParam :: Name -> TPFlavor
modTyParam :: Name -> TPFlavor
tpfName :: TPFlavor -> Maybe Name
tpName :: TParam -> Maybe Name
tvInfo :: TVar -> TVarInfo
tvSourceName :: TVarSource -> Maybe Name
quickApply :: Kind -> [a] -> Kind
kindResult :: Kind -> Kind
tpVar :: TParam -> TVar
superclassSet :: Prop -> Set Prop
newtypeConType :: Newtype -> Schema
abstractTypeTC :: AbstractType -> TCon
isFreeTV :: TVar -> Bool
isBoundTV :: TVar -> Bool
tIsError :: Type -> Maybe (TCErrorMessage, Type)
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
tIsTuple :: Type -> Maybe [Type]
tIsRec :: Type -> Maybe (RecordMap Ident Type)
tIsBinFun :: TFun -> Type -> Maybe (Type, Type)
tSplitFun :: TFun -> Type -> [Type]
pIsFin :: 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)
pIsFLiteral :: Prop -> Maybe (Type, Type, Type, Type)
pIsTrue :: Prop -> Bool
pIsWidth :: Prop -> Maybe Type
pIsValidFloat :: Prop -> Maybe (Type, Type)
tNum :: Integral a => a -> Type
tZero :: Type
tOne :: Type
tTwo :: Type
tInf :: Type
tNat' :: Nat' -> Type
tAbstract :: UserTC -> [Type] -> Type
tBit :: Type
tInteger :: Type
tRational :: Type
tFloat :: Type -> Type -> Type
tIntMod :: Type -> Type
tArray :: Type -> Type -> Type
tWord :: Type -> Type
tSeq :: Type -> Type -> Type
tChar :: Type
tString :: Int -> Type
tRec :: RecordMap Ident Type -> Type
tTuple :: [Type] -> Type
newtypeTyCon :: Newtype -> TCon
tFun :: Type -> Type -> Type
tNoUser :: Type -> Type
tError :: Type -> String -> Type
tf1 :: TFun -> Type -> Type
tf2 :: TFun -> Type -> Type -> Type
tf3 :: TFun -> Type -> Type -> Type -> Type
tSub :: Type -> Type -> Type
tMul :: Type -> Type -> Type
tDiv :: Type -> Type -> Type
tMod :: Type -> Type -> Type
tExp :: Type -> Type -> Type
tMin :: Type -> Type -> Type
tCeilDiv :: Type -> Type -> Type
tCeilMod :: Type -> Type -> Type
tLenFromThenTo :: Type -> Type -> Type -> Type
(=#=) :: Type -> Type -> Prop
(=/=) :: Type -> Type -> Prop
pZero :: Type -> Prop
pLogic :: Type -> Prop
pRing :: Type -> Prop
pIntegral :: Type -> Prop
pField :: Type -> Prop
pRound :: Type -> Prop
pEq :: Type -> Prop
pCmp :: Type -> Prop
pSignedCmp :: Type -> Prop
pLiteral :: Type -> Type -> Prop
(>==) :: Type -> Type -> Prop
pHas :: Selector -> Type -> Type -> Prop
pTrue :: Prop
pAnd :: [Prop] -> Prop
pSplitAnd :: Prop -> [Prop]
pFin :: Type -> Prop
pValidFloat :: Type -> Type -> Type
noFreeVariables :: FVS t => t -> Bool
freeParams :: FVS t => t -> Set TParam
addTNames :: [TParam] -> NameMap -> NameMap
ppNewtypeShort :: Newtype -> Doc
pickTVarName :: Kind -> TVarSource -> Int -> Doc
module Cryptol.TypeCheck.TCon

Documentation

class FVS t where Source #

Methods

fvs :: t -> Set TVar Source #

Instances

FVS Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Type -> Set TVar Source #
FVS Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Schema -> 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 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 a => FVS [a] Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: [a] -> 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 b) => FVS (a, b) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: (a, b) -> Set TVar Source #

type SType = Type Source #

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

data AbstractType Source #

Information about an abstract type.

Constructors

AbstractType
Fields atName :: Name atKind :: Kind atCtrs :: ([TParam], [Prop]) atFixitiy :: Maybe Fixity atDoc :: Maybe String

Instances

Show AbstractType Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> AbstractType -> ShowS # show :: AbstractType -> String # showList :: [AbstractType] -> ShowS #
Generic AbstractType Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep AbstractType :: Type -> Type # Methods from :: AbstractType -> Rep AbstractType x # to :: Rep AbstractType x -> AbstractType #
NFData AbstractType Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: AbstractType -> () #
type Rep AbstractType Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep AbstractType = D1 (MetaData "AbstractType" "Cryptol.TypeCheck.Type" "cryptol-2.9.0-4aSi1YZNBynFQwh9aOpllR" False) (C1 (MetaCons "AbstractType" PrefixI True) ((S1 (MetaSel (Just "atName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :: S1 (MetaSel (Just "atKind") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind)) :: (S1 (MetaSel (Just "atCtrs") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 ([TParam], [Prop])) :: (S1 (MetaSel (Just "atFixitiy") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Fixity)) :: S1 (MetaSel (Just "atDoc") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe String))))))

data Newtype Source #

Named records

Constructors

Newtype
Fields ntName :: Name ntParams :: [TParam] ntConstraints :: [Prop] ntFields :: [(Ident, Type)] ntDoc :: Maybe String

Instances

Show Newtype Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> Newtype -> ShowS # show :: Newtype -> String # showList :: [Newtype] -> ShowS #
Generic Newtype Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep Newtype :: Type -> Type # Methods from :: Newtype -> Rep Newtype x # to :: Rep Newtype x -> Newtype #
NFData Newtype Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: Newtype -> () #
PP Newtype Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> Newtype -> Doc Source #
HasKind Newtype Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: Newtype -> Kind Source #
FreeVars Newtype Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: Newtype -> Deps Source #
PP (WithNames Newtype) Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> WithNames Newtype -> Doc Source #
type Rep Newtype Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep Newtype = D1 (MetaData "Newtype" "Cryptol.TypeCheck.Type" "cryptol-2.9.0-4aSi1YZNBynFQwh9aOpllR" False) (C1 (MetaCons "Newtype" PrefixI True) ((S1 (MetaSel (Just "ntName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :: S1 (MetaSel (Just "ntParams") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [TParam])) :: (S1 (MetaSel (Just "ntConstraints") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Prop]) :: (S1 (MetaSel (Just "ntFields") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Ident, Type)]) :: S1 (MetaSel (Just "ntDoc") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe String))))))

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 String) Documentation

Instances

Show TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TySyn -> ShowS # show :: TySyn -> String # showList :: [TySyn] -> ShowS #
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 #
NFData TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TySyn -> () #
PP TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TySyn -> Doc Source #
HasKind TySyn Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: TySyn -> Kind Source #
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-2.9.0-4aSi1YZNBynFQwh9aOpllR" 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 String))))))

type Prop = Type Source #

The type is supposed to be of kind KProp.

data TVarSource Source #

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 (Maybe Int)
TypeOfRes
TypeErrorPlaceHolder

Instances

Show TVarSource Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TVarSource -> ShowS # show :: TVarSource -> String # showList :: [TVarSource] -> ShowS #
Generic TVarSource Source #
Instance details Defined in Cryptol.TypeCheck.Type Associated Types type Rep TVarSource :: Type -> Type # Methods from :: TVarSource -> Rep TVarSource x # to :: Rep TVarSource x -> TVarSource #
NFData TVarSource Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TVarSource -> () #
PP TVarSource Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TVarSource -> Doc Source #
type Rep TVarSource Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep TVarSource = D1 (MetaData "TVarSource" "Cryptol.TypeCheck.Type" "cryptol-2.9.0-4aSi1YZNBynFQwh9aOpllR" 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 (Maybe Int)))) :+: (C1 (MetaCons "TypeOfRes" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "TypeErrorPlaceHolder" PrefixI False) (U1 :: Type -> Type)))))

data TVarInfo Source #

Constructors

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

Instances

Show TVarInfo Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TVarInfo -> ShowS # show :: TVarInfo -> String # showList :: [TVarInfo] -> ShowS #
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 #
NFData TVarInfo Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TVarInfo -> () #
PP TVarInfo Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TVarInfo -> Doc Source #
type Rep TVarInfo Source #
Instance details Defined in Cryptol.TypeCheck.Type type Rep TVarInfo = D1 (MetaData "TVarInfo" "Cryptol.TypeCheck.Type" "cryptol-2.9.0-4aSi1YZNBynFQwh9aOpllR" False) (C1 (MetaCons "TVarInfo" PrefixI True) (S1 (MetaSel (Just "tvarSource") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Range) :*: S1 (MetaSel (Just "tvarDesc") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TVarSource)))

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 infor for nicer warnings/errors.
TVBound !TParam

Instances

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 #
Show TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TVar -> ShowS # show :: TVar -> String # showList :: [TVar] -> ShowS #
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 #
NFData TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TVar -> () #
PP TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TVar -> Doc Source #
HasKind TVar Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: TVar -> Kind Source #
FreeVars TVar Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: TVar -> Deps Source #
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-2.9.0-4aSi1YZNBynFQwh9aOpllR" 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 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

Instances

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 #
Show Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> Type -> ShowS # show :: Type -> String # showList :: [Type] -> ShowS #
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 #
NFData Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: Type -> () #
PP Type Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> Type -> Doc 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 #
TVars Type Source #
Instance details Defined in Cryptol.TypeCheck.Subst Methods apSubst :: Subst -> Type -> Type Source #
ShowParseable Type Source #
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: Type -> Doc Source #
FreeVars Type Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: Type -> Deps Source #
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: `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-2.9.0-4aSi1YZNBynFQwh9aOpllR" 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)))))

data TPFlavor Source #

Constructors

TPModParam Name
TPOther (Maybe Name)

Instances

Show TPFlavor Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TPFlavor -> ShowS # show :: TPFlavor -> String # showList :: [TPFlavor] -> ShowS #
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 #
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-2.9.0-4aSi1YZNBynFQwh9aOpllR" False) (C1 (MetaCons "TPModParam" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name)) :+: C1 (MetaCons "TPOther" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Maybe Name))))

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

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 #
Show TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> TParam -> ShowS # show :: TParam -> String # showList :: [TParam] -> ShowS #
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 #
NFData TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: TParam -> () #
PP TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> TParam -> Doc Source #
HasKind TParam Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: TParam -> Kind Source #
ShowParseable TParam Source #
Instance details Defined in Cryptol.TypeCheck.Parseable Methods showParseable :: TParam -> Doc Source #
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-2.9.0-4aSi1YZNBynFQwh9aOpllR" 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 Schema Source #

The types of polymorphic values.

Constructors

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

Instances

Eq Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods (==) :: Schema -> Schema -> Bool # (/=) :: Schema -> Schema -> Bool #
Show Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods showsPrec :: Int -> Schema -> ShowS # show :: Schema -> String # showList :: [Schema] -> ShowS #
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 #
NFData Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods rnf :: Schema -> () #
PP Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods ppPrec :: Int -> Schema -> Doc Source #
FVS Schema Source #
Instance details Defined in Cryptol.TypeCheck.Type Methods fvs :: Schema -> Set TVar 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 #
FreeVars Schema Source #
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: Schema -> Deps Source #
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-2.9.0-4aSi1YZNBynFQwh9aOpllR" 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))))