Cryptol.TypeCheck.TCon

Documentation

infixPrimTy :: TCon -> Maybe (Ident, Fixity)

This is used for pretty prinitng. XXX: it would be nice to just rely in the info from the Prelude.

builtInType :: Name -> Maybe TCon

data Kind

Kinds, classify types.

Constructors

KType

KNum

KProp

Kind :-> Kind infixr 5

Instances

Eq Kind

Defined in Cryptol.TypeCheck.TCon

Methods

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

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

Ord Kind

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

Defined in Cryptol.TypeCheck.TCon

Methods

showsPrec :: Int -> Kind -> ShowS

show :: Kind -> String

showList :: [Kind] -> ShowS

Generic Kind

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

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: Kind -> ()

PP Kind

Defined in Cryptol.TypeCheck.TCon

Methods

ppPrec :: Int -> Kind -> Doc

type Rep Kind

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

Methods

kindOf :: t -> Kind

Instances

HasKind TFun

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: TFun -> Kind

HasKind UserTC

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: UserTC -> Kind

HasKind TC

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: TC -> Kind

HasKind PC

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: PC -> Kind

HasKind TCon

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: TCon -> Kind

HasKind Newtype

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: Newtype -> Kind

HasKind TySyn

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: TySyn -> Kind

HasKind TVar

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: TVar -> Kind

HasKind Type

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: Type -> Kind

HasKind TParam

Defined in Cryptol.TypeCheck.Type

Methods

kindOf :: TParam -> Kind

data TCon

Type constants.

Constructors

TC TC

PC PC

TF TFun

TError Kind

Instances

Eq TCon

Defined in Cryptol.TypeCheck.TCon

Methods

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

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

Ord TCon

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

Defined in Cryptol.TypeCheck.TCon

Methods

showsPrec :: Int -> TCon -> ShowS

show :: TCon -> String

showList :: [TCon] -> ShowS

Generic TCon

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

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: TCon -> ()

PP TCon

Defined in Cryptol.TypeCheck.TCon

Methods

ppPrec :: Int -> TCon -> Doc

HasKind TCon

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: TCon -> Kind

FreeVars TCon

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: TCon -> Deps

type Rep TCon

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

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

Eq PC

Defined in Cryptol.TypeCheck.TCon

Methods

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

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

Ord PC

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

Defined in Cryptol.TypeCheck.TCon

Methods

showsPrec :: Int -> PC -> ShowS

show :: PC -> String

showList :: [PC] -> ShowS

Generic PC

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

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: PC -> ()

PP PC

Defined in Cryptol.TypeCheck.TCon

Methods

ppPrec :: Int -> PC -> Doc

HasKind PC

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: PC -> Kind

type Rep PC

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

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

Eq TC

Defined in Cryptol.TypeCheck.TCon

Methods

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

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

Ord TC

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

Defined in Cryptol.TypeCheck.TCon

Methods

showsPrec :: Int -> TC -> ShowS

show :: TC -> String

showList :: [TC] -> ShowS

Generic TC

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

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: TC -> ()

PP TC

Defined in Cryptol.TypeCheck.TCon

Methods

ppPrec :: Int -> TC -> Doc

HasKind TC

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: TC -> Kind

type Rep TC

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

Constructors

UserTC Name Kind

Instances

Eq UserTC

Defined in Cryptol.TypeCheck.TCon

Methods

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

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

Ord UserTC

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

Defined in Cryptol.TypeCheck.TCon

Methods

showsPrec :: Int -> UserTC -> ShowS

show :: UserTC -> String

showList :: [UserTC] -> ShowS

Generic UserTC

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

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: UserTC -> ()

PP UserTC

Defined in Cryptol.TypeCheck.TCon

Methods

ppPrec :: Int -> UserTC -> Doc

HasKind UserTC

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: UserTC -> Kind

type Rep UserTC

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

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

Defined in Cryptol.TypeCheck.TCon

Methods

minBound :: TFun

maxBound :: TFun

Enum TFun

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

Defined in Cryptol.TypeCheck.TCon

Methods

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

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

Ord TFun

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

Defined in Cryptol.TypeCheck.TCon

Methods

showsPrec :: Int -> TFun -> ShowS

show :: TFun -> String

showList :: [TFun] -> ShowS

Generic TFun

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

Defined in Cryptol.TypeCheck.TCon

Methods

rnf :: TFun -> ()

PP TFun

Defined in Cryptol.TypeCheck.TCon

Methods

ppPrec :: Int -> TFun -> Doc

HasKind TFun

Defined in Cryptol.TypeCheck.TCon

Methods

kindOf :: TFun -> Kind

type Rep TFun

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