Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Cryptol.TypeCheck.TCon
Synopsis
- infixPrimTy :: TCon -> Maybe (Ident, Fixity)
- builtInType :: Name -> Maybe TCon
- data Kind
- class HasKind t where
- data TCon
- data PC
- data TC
- data UserTC = UserTC Name Kind
- data TCErrorMessage = TCErrorMessage {
- tcErrorMessage :: !String
- data TFun
Documentation
infixPrimTy :: TCon -> Maybe (Ident, Fixity) Source #
This is used for pretty prinitng. XXX: it would be nice to just rely in the info from the Prelude.
builtInType :: Name -> Maybe TCon Source #
Kinds, classify types.
Instances
Eq Kind Source # | |
Ord Kind Source # | |
Show Kind Source # | |
Generic Kind Source # | |
NFData Kind Source # | |
Defined in Cryptol.TypeCheck.TCon | |
PP Kind Source # | |
type Rep Kind Source # | |
Defined in Cryptol.TypeCheck.TCon type Rep Kind = D1 ('MetaData "Kind" "Cryptol.TypeCheck.TCon" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) ((C1 ('MetaCons "KType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "KNum" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "KProp" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons ":->" ('InfixI 'RightAssociative 5) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind)))) |
Type constants.
Instances
Eq TCon Source # | |
Ord TCon Source # | |
Show TCon Source # | |
Generic TCon Source # | |
NFData TCon Source # | |
Defined in Cryptol.TypeCheck.TCon | |
PP TCon Source # | |
HasKind TCon Source # | |
FreeVars TCon Source # | |
type Rep TCon Source # | |
Defined in Cryptol.TypeCheck.TCon type Rep TCon = D1 ('MetaData "TCon" "Cryptol.TypeCheck.TCon" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) ((C1 ('MetaCons "TC" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TC)) :+: C1 ('MetaCons "PC" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PC))) :+: (C1 ('MetaCons "TF" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TFun)) :+: C1 ('MetaCons "TError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TCErrorMessage)))) |
Predicate symbols.
If you add additional user-visible constructors, please update primTys
.
Constructors
PEqual | _ == _ |
PNeq | _ /= _ |
PGeq | _ >= _ |
PFin | fin _ |
PHas Selector |
|
PZero | Zero _ |
PLogic | Logic _ |
PArith | Arith _ |
PCmp | Cmp _ |
PSignedCmp | SignedCmp _ |
PLiteral | Literal _ _ |
PAnd | This is useful when simplifying things in place |
PTrue | Ditto |
Instances
Eq PC Source # | |
Ord PC Source # | |
Show PC Source # | |
Generic PC Source # | |
NFData PC Source # | |
Defined in Cryptol.TypeCheck.TCon | |
PP PC Source # | |
HasKind PC Source # | |
type Rep PC Source # | |
Defined in Cryptol.TypeCheck.TCon type Rep PC = D1 ('MetaData "PC" "Cryptol.TypeCheck.TCon" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (((C1 ('MetaCons "PEqual" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PNeq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PGeq" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "PFin" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PHas" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Selector)) :+: C1 ('MetaCons "PZero" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "PLogic" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PArith" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PCmp" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PSignedCmp" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PLiteral" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PAnd" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PTrue" 'PrefixI 'False) (U1 :: Type -> Type))))) |
1-1 constants.
If you add additional user-visible constructors, please update primTys
.
Constructors
TCNum Integer | Numbers |
TCInf | Inf |
TCBit | Bit |
TCInteger | Integer |
TCIntMod | Z _ |
TCSeq | [_] _ |
TCFun | _ -> _ |
TCTuple Int | (_, _, _) |
TCAbstract UserTC | An abstract type |
TCNewtype UserTC | user-defined, |
Instances
Eq TC Source # | |
Ord TC Source # | |
Show TC Source # | |
Generic TC Source # | |
NFData TC Source # | |
Defined in Cryptol.TypeCheck.TCon | |
PP TC Source # | |
HasKind TC Source # | |
type Rep TC Source # | |
Defined in Cryptol.TypeCheck.TCon type Rep TC = D1 ('MetaData "TC" "Cryptol.TypeCheck.TCon" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (((C1 ('MetaCons "TCNum" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)) :+: C1 ('MetaCons "TCInf" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TCBit" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TCInteger" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TCIntMod" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "TCSeq" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TCFun" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TCTuple" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: (C1 ('MetaCons "TCAbstract" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UserTC)) :+: C1 ('MetaCons "TCNewtype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UserTC)))))) |
Instances
Eq UserTC Source # | |
Ord UserTC Source # | |
Show UserTC Source # | |
Generic UserTC Source # | |
NFData UserTC Source # | |
Defined in Cryptol.TypeCheck.TCon | |
PP UserTC Source # | |
HasKind UserTC Source # | |
type Rep UserTC Source # | |
Defined in Cryptol.TypeCheck.TCon type Rep UserTC = D1 ('MetaData "UserTC" "Cryptol.TypeCheck.TCon" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "UserTC" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Name) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Kind))) |
data TCErrorMessage Source #
Constructors
TCErrorMessage | |
Fields
|
Instances
Built-in type functions.
If you add additional user-visible constructors,
please update primTys
in Cryptol.Prims.Types.
Constructors
TCAdd | : Num -> Num -> Num |
TCSub | : Num -> Num -> Num |
TCMul | : Num -> Num -> Num |
TCDiv | : Num -> Num -> Num |
TCMod | : Num -> Num -> Num |
TCExp | : Num -> Num -> Num |
TCWidth | : Num -> Num |
TCMin | : Num -> Num -> Num |
TCMax | : Num -> Num -> Num |
TCCeilDiv | : Num -> Num -> Num |
TCCeilMod | : Num -> Num -> Num |
TCLenFromThenTo |
|
Instances
Bounded TFun Source # | |
Defined in Cryptol.TypeCheck.TCon | |
Enum TFun Source # | |
Eq TFun Source # | |
Ord TFun Source # | |
Show TFun Source # | |
Generic TFun Source # | |
NFData TFun Source # | |
Defined in Cryptol.TypeCheck.TCon | |
PP TFun Source # | |
HasKind TFun Source # | |
type Rep TFun Source # | |
Defined in Cryptol.TypeCheck.TCon type Rep TFun = D1 ('MetaData "TFun" "Cryptol.TypeCheck.TCon" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (((C1 ('MetaCons "TCAdd" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TCSub" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TCMul" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "TCDiv" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TCMod" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TCExp" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "TCWidth" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TCMin" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TCMax" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "TCCeilDiv" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TCCeilMod" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TCLenFromThenTo" 'PrefixI 'False) (U1 :: Type -> Type))))) |