Cryptol.Eval.Type

Documentation

data TValue

An evaluated type of kind *. These types do not contain type variables, type synonyms, or type functions.

Constructors

TVBit

 Bit

TVInteger

 Integer

TVIntMod Integer

 Z n

TVSeq Integer TValue

 [n]a

TVStream TValue

 [inf]t

TVTuple [TValue]

 (a, b, c )

TVRec [(Ident, TValue)]

 { x : a, y : b, z : c }

TVFun TValue TValue

 a -> b

TVAbstract UserTC [Either Nat' TValue]

an abstract type

Instances

Show TValue

Defined in Cryptol.Eval.Type

Methods

showsPrec :: Int -> TValue -> ShowS

show :: TValue -> String

showList :: [TValue] -> ShowS

Generic TValue

Defined in Cryptol.Eval.Type

Associated Types

type Rep TValue :: Type -> Type

Methods

from :: TValue -> Rep TValue x

to :: Rep TValue x -> TValue

NFData TValue

Defined in Cryptol.Eval.Type

Methods

rnf :: TValue -> ()

type Rep TValue

Defined in Cryptol.Eval.Type

type Rep TValue = D1 (MetaData "TValue" "Cryptol.Eval.Type" "cryptol-2.8.0-Jl4xQKR0B4Q8VTNDfmeSo7" False) (((C1 (MetaCons "TVBit" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "TVInteger" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "TVIntMod" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Integer)) :+: C1 (MetaCons "TVSeq" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Integer) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TValue)))) :+: ((C1 (MetaCons "TVStream" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TValue)) :+: C1 (MetaCons "TVTuple" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [TValue]))) :+: (C1 (MetaCons "TVRec" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [(Ident, TValue)])) :+: (C1 (MetaCons "TVFun" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TValue) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TValue)) :+: C1 (MetaCons "TVAbstract" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 UserTC) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [Either Nat' TValue]))))))

tValTy :: TValue -> Type

Convert a type value back into a regular type

isTBit :: TValue -> Bool

True if the evaluated value is Bit

tvSeq :: Nat' -> TValue -> TValue

Produce a sequence type value

finNat' :: Nat' -> Integer

Coerce an extended natural into an integer, for values known to be finite

type TypeEnv = Map TVar (Either Nat' TValue)

evalType :: HasCallStack => TypeEnv -> Type -> Either Nat' TValue

Evaluation for types (kind * or #).

evalValType :: HasCallStack => TypeEnv -> Type -> TValue

Evaluation for value types (kind *).

evalNumType :: HasCallStack => TypeEnv -> Type -> Nat'

Evaluation for number types (kind #).

evalTF :: HasCallStack => TFun -> [Nat'] -> Nat'

Reduce type functions, raising an exception for undefined values.