cryptol-2.10.0: Cryptol: The Language of Cryptography
Safe HaskellSafe
LanguageHaskell2010

Cryptol.TypeCheck.TCon

Synopsis

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 #

data Kind Source #

Kinds, classify types.

Constructors

KType 
KNum 
KProp 
Kind :-> Kind infixr 5 

Instances

Instances details
Eq Kind Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

(==) :: Kind -> Kind -> Bool #

(/=) :: Kind -> Kind -> Bool #

Ord Kind Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

compare :: Kind -> Kind -> Ordering #

(<) :: Kind -> Kind -> Bool #

(<=) :: Kind -> Kind -> Bool #

(>) :: Kind -> Kind -> Bool #

(>=) :: Kind -> Kind -> Bool #

max :: Kind -> Kind -> Kind #

min :: Kind -> Kind -> Kind #

Show Kind Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

showsPrec :: Int -> Kind -> ShowS #

show :: Kind -> String #

showList :: [Kind] -> ShowS #

Generic Kind Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Associated Types

type Rep Kind :: Type -> Type #

Methods

from :: Kind -> Rep Kind x #

to :: Rep Kind x -> Kind #

NFData Kind Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: Kind -> () #

PP Kind Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

ppPrec :: Int -> Kind -> Doc Source #

type Rep Kind Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

type Rep Kind = D1 ('MetaData "Kind" "Cryptol.TypeCheck.TCon" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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))))

class HasKind t where Source #

Methods

kindOf :: t -> Kind Source #

Instances

Instances details
HasKind TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: TFun -> Kind Source #

HasKind UserTC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: UserTC -> Kind Source #

HasKind TC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: TC -> Kind Source #

HasKind PC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: PC -> Kind Source #

HasKind TCon Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: TCon -> Kind Source #

HasKind Newtype Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: Newtype -> Kind Source #

HasKind TySyn Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: TySyn -> Kind Source #

HasKind TVar Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: TVar -> Kind Source #

HasKind Type Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: Type -> Kind Source #

HasKind TParam Source # 
Instance details

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: TParam -> Kind Source #

data TCon Source #

Type constants.

Constructors

TC TC 
PC PC 
TF TFun 
TError Kind 

Instances

Instances details
Eq TCon Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

(==) :: TCon -> TCon -> Bool #

(/=) :: TCon -> TCon -> Bool #

Ord TCon Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

compare :: TCon -> TCon -> Ordering #

(<) :: TCon -> TCon -> Bool #

(<=) :: TCon -> TCon -> Bool #

(>) :: TCon -> TCon -> Bool #

(>=) :: TCon -> TCon -> Bool #

max :: TCon -> TCon -> TCon #

min :: TCon -> TCon -> TCon #

Show TCon Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

showsPrec :: Int -> TCon -> ShowS #

show :: TCon -> String #

showList :: [TCon] -> ShowS #

Generic TCon Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Associated Types

type Rep TCon :: Type -> Type #

Methods

from :: TCon -> Rep TCon x #

to :: Rep TCon x -> TCon #

NFData TCon Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: TCon -> () #

PP TCon Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

ppPrec :: Int -> TCon -> Doc Source #

HasKind TCon Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: TCon -> Kind Source #

FreeVars TCon Source # 
Instance details

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: TCon -> Deps Source #

type Rep TCon Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

type Rep TCon = D1 ('MetaData "TCon" "Cryptol.TypeCheck.TCon" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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))))

data PC Source #

Predicate symbols. If you add additional user-visible constructors, please update primTys.

Constructors

PEqual
_ == _
PNeq
_ /= _
PGeq
_ >= _
PFin
fin _
PPrime
prime _
PHas Selector

Has sel type field does not appear in schemas

PZero
Zero _
PLogic
Logic _
PRing
Ring _
PIntegral
Integral _
PField
Field _
PRound
Round _
PEq
Eq _
PCmp
Cmp _
PSignedCmp
SignedCmp _
PLiteral
Literal _ _
PFLiteral
FLiteral _ _ _
PValidFloat

ValidFloat _ _ constraints on supported floating point representaitons

PAnd

This is useful when simplifying things in place

PTrue

Ditto

Instances

Instances details
Eq PC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

(==) :: PC -> PC -> Bool #

(/=) :: PC -> PC -> Bool #

Ord PC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

compare :: PC -> PC -> Ordering #

(<) :: PC -> PC -> Bool #

(<=) :: PC -> PC -> Bool #

(>) :: PC -> PC -> Bool #

(>=) :: PC -> PC -> Bool #

max :: PC -> PC -> PC #

min :: PC -> PC -> PC #

Show PC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

showsPrec :: Int -> PC -> ShowS #

show :: PC -> String #

showList :: [PC] -> ShowS #

Generic PC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Associated Types

type Rep PC :: Type -> Type #

Methods

from :: PC -> Rep PC x #

to :: Rep PC x -> PC #

NFData PC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: PC -> () #

PP PC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

ppPrec :: Int -> PC -> Doc Source #

HasKind PC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: PC -> Kind Source #

type Rep PC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

type Rep PC = D1 ('MetaData "PC" "Cryptol.TypeCheck.TCon" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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 "PPrime" '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 "PRing" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PIntegral" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "PField" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PRound" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PEq" '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 "PFLiteral" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PValidFloat" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PAnd" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PTrue" 'PrefixI 'False) (U1 :: Type -> Type))))))

data TC Source #

1-1 constants. If you add additional user-visible constructors, please update primTys.

Constructors

TCNum Integer

Numbers

TCInf

Inf

TCBit

Bit

TCInteger

Integer

TCFloat

Float

TCIntMod
Z _
TCRational
Rational
TCArray
Array _ _
TCSeq
[_] _
TCFun
_ -> _
TCTuple Int
(_, _, _)
TCAbstract UserTC

An abstract type

TCNewtype UserTC

user-defined, T

Instances

Instances details
Eq TC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

(==) :: TC -> TC -> Bool #

(/=) :: TC -> TC -> Bool #

Ord TC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

compare :: TC -> TC -> Ordering #

(<) :: TC -> TC -> Bool #

(<=) :: TC -> TC -> Bool #

(>) :: TC -> TC -> Bool #

(>=) :: TC -> TC -> Bool #

max :: TC -> TC -> TC #

min :: TC -> TC -> TC #

Show TC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

showsPrec :: Int -> TC -> ShowS #

show :: TC -> String #

showList :: [TC] -> ShowS #

Generic TC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Associated Types

type Rep TC :: Type -> Type #

Methods

from :: TC -> Rep TC x #

to :: Rep TC x -> TC #

NFData TC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: TC -> () #

PP TC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

ppPrec :: Int -> TC -> Doc Source #

HasKind TC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: TC -> Kind Source #

type Rep TC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

type Rep TC = D1 ('MetaData "TC" "Cryptol.TypeCheck.TCon" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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 "TCFloat" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TCIntMod" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "TCRational" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TCArray" '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))))))

data UserTC Source #

Constructors

UserTC Name Kind 

Instances

Instances details
Eq UserTC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

(==) :: UserTC -> UserTC -> Bool #

(/=) :: UserTC -> UserTC -> Bool #

Ord UserTC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

compare :: UserTC -> UserTC -> Ordering #

(<) :: UserTC -> UserTC -> Bool #

(<=) :: UserTC -> UserTC -> Bool #

(>) :: UserTC -> UserTC -> Bool #

(>=) :: UserTC -> UserTC -> Bool #

max :: UserTC -> UserTC -> UserTC #

min :: UserTC -> UserTC -> UserTC #

Show UserTC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

showsPrec :: Int -> UserTC -> ShowS #

show :: UserTC -> String #

showList :: [UserTC] -> ShowS #

Generic UserTC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Associated Types

type Rep UserTC :: Type -> Type #

Methods

from :: UserTC -> Rep UserTC x #

to :: Rep UserTC x -> UserTC #

NFData UserTC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: UserTC -> () #

PP UserTC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

ppPrec :: Int -> UserTC -> Doc Source #

HasKind UserTC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: UserTC -> Kind Source #

type Rep UserTC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

type Rep UserTC = D1 ('MetaData "UserTC" "Cryptol.TypeCheck.TCon" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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 TFun Source #

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

: Num -> Num -> Num -> Num Example: [ 1, 5 .. 9 ] :: [lengthFromThenTo 1 5 9][b]

Instances

Instances details
Bounded TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

minBound :: TFun #

maxBound :: TFun #

Enum TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

succ :: TFun -> TFun #

pred :: TFun -> TFun #

toEnum :: Int -> TFun #

fromEnum :: TFun -> Int #

enumFrom :: TFun -> [TFun] #

enumFromThen :: TFun -> TFun -> [TFun] #

enumFromTo :: TFun -> TFun -> [TFun] #

enumFromThenTo :: TFun -> TFun -> TFun -> [TFun] #

Eq TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

(==) :: TFun -> TFun -> Bool #

(/=) :: TFun -> TFun -> Bool #

Ord TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

compare :: TFun -> TFun -> Ordering #

(<) :: TFun -> TFun -> Bool #

(<=) :: TFun -> TFun -> Bool #

(>) :: TFun -> TFun -> Bool #

(>=) :: TFun -> TFun -> Bool #

max :: TFun -> TFun -> TFun #

min :: TFun -> TFun -> TFun #

Show TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

showsPrec :: Int -> TFun -> ShowS #

show :: TFun -> String #

showList :: [TFun] -> ShowS #

Generic TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Associated Types

type Rep TFun :: Type -> Type #

Methods

from :: TFun -> Rep TFun x #

to :: Rep TFun x -> TFun #

NFData TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: TFun -> () #

PP TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

ppPrec :: Int -> TFun -> Doc Source #

HasKind TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: TFun -> Kind Source #

type Rep TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

type Rep TFun = D1 ('MetaData "TFun" "Cryptol.TypeCheck.TCon" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" '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)))))