cryptol-2.8.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.

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.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))))

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.

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.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))))

data PC Source #

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

Constructors

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

Has sel type field does not appear in schemas

PZero
Zero _
PLogic
Logic _
PArith
Arith _
PCmp
Cmp _
PSignedCmp
SignedCmp _
PLiteral
Literal _ _
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.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)))))

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

TCIntMod
Z _
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.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))))))

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.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 

Instances

Instances details
Eq TCErrorMessage Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Ord TCErrorMessage Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Show TCErrorMessage Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

showsPrec :: Int -> TCErrorMessage -> ShowS

show :: TCErrorMessage -> String

showList :: [TCErrorMessage] -> ShowS

Generic TCErrorMessage Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Associated Types

type Rep TCErrorMessage :: Type -> Type

NFData TCErrorMessage Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: TCErrorMessage -> ()

PP TCErrorMessage Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

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

type Rep TCErrorMessage Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

type Rep TCErrorMessage = D1 ('MetaData "TCErrorMessage" "Cryptol.TypeCheck.TCon" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" 'False) (C1 ('MetaCons "TCErrorMessage" 'PrefixI 'True) (S1 ('MetaSel ('Just "tcErrorMessage") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 String)))

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

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.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)))))