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.

builtInType :: Name -> Maybe TCon Source #

data Kind Source #

Kinds, classify types.

Constructors

KType 
KNum 
KProp 
Kind :-> Kind infixr 5 
Instances
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-Jl4xQKR0B4Q8VTNDfmeSo7" 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
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 TCErrorMessage 
Instances
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-Jl4xQKR0B4Q8VTNDfmeSo7" 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
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-Jl4xQKR0B4Q8VTNDfmeSo7" 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
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-Jl4xQKR0B4Q8VTNDfmeSo7" 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
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-Jl4xQKR0B4Q8VTNDfmeSo7" 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
Eq TCErrorMessage Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

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

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

Ord TCErrorMessage Source # 
Instance details

Defined in Cryptol.TypeCheck.TCon

Methods

compare :: TCErrorMessage -> TCErrorMessage -> Ordering #

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

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

(>) :: TCErrorMessage -> TCErrorMessage -> Bool #

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

max :: TCErrorMessage -> TCErrorMessage -> TCErrorMessage #

min :: TCErrorMessage -> TCErrorMessage -> TCErrorMessage #

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 #

Methods

from :: TCErrorMessage -> Rep TCErrorMessage x #

to :: Rep TCErrorMessage x -> TCErrorMessage #

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-Jl4xQKR0B4Q8VTNDfmeSo7" 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
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.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" 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)))))