Cryptol.Prims.Syntax

Documentation

data PrimTy

Information about a user visible built-in type.

Constructors

PrimTy

Fields

• primTyCon :: !TCon

  Use this ty-con (renamer)

• primTyIdent :: !Ident

  This is what it's called

• primTyDoc :: !String

  Documentation

• primTyFixity :: !(Maybe Fixity)

  Precedence, for infix ones

Instances

Eq PrimTy

Defined in Cryptol.Prims.Syntax

Methods

(==) :: PrimTy -> PrimTy -> Bool

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

Ord PrimTy

Defined in Cryptol.Prims.Syntax

Methods

compare :: PrimTy -> PrimTy -> Ordering

(<) :: PrimTy -> PrimTy -> Bool

(<=) :: PrimTy -> PrimTy -> Bool

(>) :: PrimTy -> PrimTy -> Bool

(>=) :: PrimTy -> PrimTy -> Bool

max :: PrimTy -> PrimTy -> PrimTy

min :: PrimTy -> PrimTy -> PrimTy

primTyList :: [PrimTy]

This list should contain all user-visible built-in types.

primTyIx :: Ord a => (PrimTy -> Maybe a) -> a -> Maybe PrimTy

Construct an index for quick lookup of primtys.

primTyFromPName :: PName -> Maybe PrimTy

Lookup a prim type by a parser name.

primTyFromTC :: TCon -> Maybe PrimTy

Lookup if a ty con is a primitive.

primTyFromTF :: TFun -> Maybe PrimTy

Lookup a TFun prim type.

primTyFromPC :: PC -> Maybe PrimTy

Lookup a TCon prim type.

data Kind

Kinds, classify types.

Constructors

KType

KNum

KProp

Kind :-> Kind infixr 5

Instances

Eq Kind

Defined in Cryptol.Prims.Syntax

Methods

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

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

Ord Kind

Defined in Cryptol.Prims.Syntax

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

Methods

showsPrec :: Int -> Kind -> ShowS

show :: Kind -> String

showList :: [Kind] -> ShowS

Generic Kind

Defined in Cryptol.Prims.Syntax

Associated Types

type Rep Kind :: Type -> Type

Methods

from :: Kind -> Rep Kind x

to :: Rep Kind x -> Kind

NFData Kind

Defined in Cryptol.Prims.Syntax

Methods

rnf :: Kind -> ()

PP Kind

Defined in Cryptol.Prims.Syntax

Methods

ppPrec :: Int -> Kind -> Doc

type Rep Kind

Defined in Cryptol.Prims.Syntax

type Rep Kind = D1 (MetaData "Kind" "Cryptol.Prims.Syntax" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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.Prims.Syntax

Methods

kindOf :: TFun -> Kind

HasKind UserTC

Defined in Cryptol.Prims.Syntax

Methods

kindOf :: UserTC -> Kind

HasKind TC

Defined in Cryptol.Prims.Syntax

Methods

kindOf :: TC -> Kind

HasKind PC

Defined in Cryptol.Prims.Syntax

Methods

kindOf :: PC -> Kind

HasKind TCon

Defined in Cryptol.Prims.Syntax

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 TCErrorMessage

Instances

Eq TCon

Defined in Cryptol.Prims.Syntax

Methods

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

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

Ord TCon

Defined in Cryptol.Prims.Syntax

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

Methods

showsPrec :: Int -> TCon -> ShowS

show :: TCon -> String

showList :: [TCon] -> ShowS

Generic TCon

Defined in Cryptol.Prims.Syntax

Associated Types

type Rep TCon :: Type -> Type

Methods

from :: TCon -> Rep TCon x

to :: Rep TCon x -> TCon

NFData TCon

Defined in Cryptol.Prims.Syntax

Methods

rnf :: TCon -> ()

PPName TCon

Defined in Cryptol.Prims.Syntax

Methods

ppNameFixity :: TCon -> Maybe (Assoc, Int)

ppPrefixName :: TCon -> Doc

ppInfixName :: TCon -> Doc

PP TCon

Defined in Cryptol.Prims.Syntax

Methods

ppPrec :: Int -> TCon -> Doc

HasKind TCon

Defined in Cryptol.Prims.Syntax

Methods

kindOf :: TCon -> Kind

FreeVars TCon

Defined in Cryptol.IR.FreeVars

Methods

freeVars :: TCon -> Deps

type Rep TCon

Defined in Cryptol.Prims.Syntax

type Rep TCon = D1 (MetaData "TCon" "Cryptol.Prims.Syntax" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

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

Defined in Cryptol.Prims.Syntax

Methods

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

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

Ord PC

Defined in Cryptol.Prims.Syntax

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

Methods

showsPrec :: Int -> PC -> ShowS

show :: PC -> String

showList :: [PC] -> ShowS

Generic PC

Defined in Cryptol.Prims.Syntax

Associated Types

type Rep PC :: Type -> Type

Methods

from :: PC -> Rep PC x

to :: Rep PC x -> PC

NFData PC

Defined in Cryptol.Prims.Syntax

Methods

rnf :: PC -> ()

PP PC

Defined in Cryptol.Prims.Syntax

Methods

ppPrec :: Int -> PC -> Doc

HasKind PC

Defined in Cryptol.Prims.Syntax

Methods

kindOf :: PC -> Kind

type Rep PC

Defined in Cryptol.Prims.Syntax

type Rep PC = D1 (MetaData "PC" "Cryptol.Prims.Syntax" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

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

(_, _, _)

TCNewtype UserTC

user-defined, T

Instances

Eq TC

Defined in Cryptol.Prims.Syntax

Methods

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

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

Ord TC

Defined in Cryptol.Prims.Syntax

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

Methods

showsPrec :: Int -> TC -> ShowS

show :: TC -> String

showList :: [TC] -> ShowS

Generic TC

Defined in Cryptol.Prims.Syntax

Associated Types

type Rep TC :: Type -> Type

Methods

from :: TC -> Rep TC x

to :: Rep TC x -> TC

NFData TC

Defined in Cryptol.Prims.Syntax

Methods

rnf :: TC -> ()

PP TC

Defined in Cryptol.Prims.Syntax

Methods

ppPrec :: Int -> TC -> Doc

HasKind TC

Defined in Cryptol.Prims.Syntax

Methods

kindOf :: TC -> Kind

type Rep TC

Defined in Cryptol.Prims.Syntax

type Rep TC = D1 (MetaData "TC" "Cryptol.Prims.Syntax" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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 "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.Prims.Syntax

Methods

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

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

Ord UserTC

Defined in Cryptol.Prims.Syntax

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

Methods

showsPrec :: Int -> UserTC -> ShowS

show :: UserTC -> String

showList :: [UserTC] -> ShowS

Generic UserTC

Defined in Cryptol.Prims.Syntax

Associated Types

type Rep UserTC :: Type -> Type

Methods

from :: UserTC -> Rep UserTC x

to :: Rep UserTC x -> UserTC

NFData UserTC

Defined in Cryptol.Prims.Syntax

Methods

rnf :: UserTC -> ()

PP UserTC

Defined in Cryptol.Prims.Syntax

Methods

ppPrec :: Int -> UserTC -> Doc

HasKind UserTC

Defined in Cryptol.Prims.Syntax

Methods

kindOf :: UserTC -> Kind

type Rep UserTC

Defined in Cryptol.Prims.Syntax

type Rep UserTC = D1 (MetaData "UserTC" "Cryptol.Prims.Syntax" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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

Constructors

TCErrorMessage

Fields

• tcErrorMessage :: !String

Instances

Eq TCErrorMessage

Defined in Cryptol.Prims.Syntax

Methods

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

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

Ord TCErrorMessage

Defined in Cryptol.Prims.Syntax

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

Defined in Cryptol.Prims.Syntax

Methods

showsPrec :: Int -> TCErrorMessage -> ShowS

show :: TCErrorMessage -> String

showList :: [TCErrorMessage] -> ShowS

Generic TCErrorMessage

Defined in Cryptol.Prims.Syntax

Associated Types

type Rep TCErrorMessage :: Type -> Type

Methods

from :: TCErrorMessage -> Rep TCErrorMessage x

to :: Rep TCErrorMessage x -> TCErrorMessage

NFData TCErrorMessage

Defined in Cryptol.Prims.Syntax

Methods

rnf :: TCErrorMessage -> ()

PP TCErrorMessage

Defined in Cryptol.Prims.Syntax

Methods

ppPrec :: Int -> TCErrorMessage -> Doc

type Rep TCErrorMessage

Defined in Cryptol.Prims.Syntax

type Rep TCErrorMessage = D1 (MetaData "TCErrorMessage" "Cryptol.Prims.Syntax" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" False) (C1 (MetaCons "TCErrorMessage" PrefixI True) (S1 (MetaSel (Just "tcErrorMessage") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 String)))

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

Methods

minBound :: TFun

maxBound :: TFun

Enum TFun

Defined in Cryptol.Prims.Syntax

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

Methods

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

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

Ord TFun

Defined in Cryptol.Prims.Syntax

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

Methods

showsPrec :: Int -> TFun -> ShowS

show :: TFun -> String

showList :: [TFun] -> ShowS

Generic TFun

Defined in Cryptol.Prims.Syntax

Associated Types

type Rep TFun :: Type -> Type

Methods

from :: TFun -> Rep TFun x

to :: Rep TFun x -> TFun

NFData TFun

Defined in Cryptol.Prims.Syntax

Methods

rnf :: TFun -> ()

PPName TFun

Defined in Cryptol.Prims.Syntax

Methods

ppNameFixity :: TFun -> Maybe (Assoc, Int)

ppPrefixName :: TFun -> Doc

ppInfixName :: TFun -> Doc

PP TFun

Defined in Cryptol.Prims.Syntax

Methods

ppPrec :: Int -> TFun -> Doc

HasKind TFun

Defined in Cryptol.Prims.Syntax

Methods

kindOf :: TFun -> Kind

type Rep TFun

Defined in Cryptol.Prims.Syntax

type Rep TFun = D1 (MetaData "TFun" "Cryptol.Prims.Syntax" "cryptol-2.7.0-6VD9sMh08R1JPrYSq7DH8b" 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)))))