Safe Haskell	Safe
Language	Haskell2010

Cryptol.TypeCheck.TCon

Synopsis

infixPrimTy :: TCon -> Maybe (Ident, Fixity)
builtInType :: Name -> Maybe TCon
data Kind
- = KType
- | KNum
- | KProp
- | Kind :-> Kind
class HasKind t where
- kindOf :: t -> Kind
data TCon
- = TC TC
- | PC PC
- | TF TFun
- | TError Kind TCErrorMessage
data PC
- = PEqual
- | PNeq
- | PGeq
- | PFin
- | PHas Selector
- | PZero
- | PLogic
- | PArith
- | PCmp
- | PSignedCmp
- | PLiteral
- | PAnd
- | PTrue
data TC
- = TCNum Integer
- | TCInf
- | TCBit
- | TCInteger
- | TCIntMod
- | TCSeq
- | TCFun
- | TCTuple Int
- | TCAbstract UserTC
- | TCNewtype UserTC
data UserTC = UserTC Name Kind
data TCErrorMessage = TCErrorMessage {
- tcErrorMessage :: !String
}
data TFun
- = TCAdd
- | TCSub
- | TCMul
- | TCDiv
- | TCMod
- | TCExp
- | TCWidth
- | TCMin
- | TCMax
- | TCCeilDiv
- | TCCeilMod
- | TCLenFromThenTo

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.8.0-jyTxkWAqoKLO0ZfM89b4u" '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 TCErrorMessage

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-jyTxkWAqoKLO0ZfM89b4u" '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-jyTxkWAqoKLO0ZfM89b4u" '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-jyTxkWAqoKLO0ZfM89b4u" '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-jyTxkWAqoKLO0ZfM89b4u" '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 tcErrorMessage :: !String

Instances

Instances details

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-jyTxkWAqoKLO0ZfM89b4u" '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 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-jyTxkWAqoKLO0ZfM89b4u" '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)))))