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 Source #

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

Ord Kind Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Show Kind Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Generic Kind Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Associated Types

type Rep Kind :: Type -> Type Source #

Methods

from :: Kind -> Rep Kind x Source #

to :: Rep Kind x -> Kind Source #

NFData Kind Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: Kind -> () Source #

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-11Z6ZaBuQbo1UTYpHYMeUg" '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 Source #

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

Ord TCon Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Show TCon Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Generic TCon Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Associated Types

type Rep TCon :: Type -> Type Source #

Methods

from :: TCon -> Rep TCon x Source #

to :: Rep TCon x -> TCon Source #

NFData TCon Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: TCon -> () Source #

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

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 Source #

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

Ord PC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

compare :: PC -> PC -> Ordering Source #

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

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

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

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

max :: PC -> PC -> PC Source #

min :: PC -> PC -> PC Source #

Show PC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Generic PC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Associated Types

type Rep PC :: Type -> Type Source #

Methods

from :: PC -> Rep PC x Source #

to :: Rep PC x -> PC Source #

NFData PC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: PC -> () Source #

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-11Z6ZaBuQbo1UTYpHYMeUg" '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 Source #

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

Ord TC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

compare :: TC -> TC -> Ordering Source #

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

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

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

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

max :: TC -> TC -> TC Source #

min :: TC -> TC -> TC Source #

Show TC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Generic TC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Associated Types

type Rep TC :: Type -> Type Source #

Methods

from :: TC -> Rep TC x Source #

to :: Rep TC x -> TC Source #

NFData TC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: TC -> () Source #

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-11Z6ZaBuQbo1UTYpHYMeUg" '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

Ord UserTC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Show UserTC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Generic UserTC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Associated Types

type Rep UserTC :: Type -> Type Source #

NFData UserTC Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: UserTC -> () Source #

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-11Z6ZaBuQbo1UTYpHYMeUg" '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

Generic TCErrorMessage Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Associated Types

type Rep TCErrorMessage :: Type -> Type Source #

NFData TCErrorMessage Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: TCErrorMessage -> () Source #

PP TCErrorMessage Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

type Rep TCErrorMessage Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

type Rep TCErrorMessage = D1 ('MetaData "TCErrorMessage" "Cryptol.TypeCheck.TCon" "cryptol-2.8.0-11Z6ZaBuQbo1UTYpHYMeUg" '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

Eq TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

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

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

Ord TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Show TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Generic TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Associated Types

type Rep TFun :: Type -> Type Source #

Methods

from :: TFun -> Rep TFun x Source #

to :: Rep TFun x -> TFun Source #

NFData TFun Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: TFun -> () Source #

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-11Z6ZaBuQbo1UTYpHYMeUg" '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)))))