cryptol-2.10.0: Cryptol: The Language of Cryptography
Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

Cryptol.Eval.Type

Description

 
Synopsis

Documentation

data TValue Source #

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

Constructors

TVBit
 Bit
TVInteger
 Integer
TVFloat Integer Integer
 Float e p
TVIntMod Integer
 Z n
TVRational
Rational
TVArray TValue TValue
 Array a b
TVSeq Integer TValue
 [n]a
TVStream TValue
 [inf]t
TVTuple [TValue]
 (a, b, c )
TVRec (RecordMap Ident TValue)
 { x : a, y : b, z : c }
TVFun TValue TValue
 a -> b
TVAbstract UserTC [Either Nat' TValue]

an abstract type

Instances

Instances details
Show TValue Source # 
Instance details

Defined in Cryptol.Eval.Type

Generic TValue Source # 
Instance details

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 Source # 
Instance details

Defined in Cryptol.Eval.Type

Methods

rnf :: TValue -> () #

type Rep TValue Source # 
Instance details

Defined in Cryptol.Eval.Type

type Rep TValue = D1 ('MetaData "TValue" "Cryptol.Eval.Type" "cryptol-2.10.0-Bsi6VMfJ6GCFlOdda30jWW" 'False) (((C1 ('MetaCons "TVBit" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "TVInteger" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TVFloat" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))) :+: (C1 ('MetaCons "TVIntMod" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)) :+: (C1 ('MetaCons "TVRational" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TVArray" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TValue) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TValue))))) :+: ((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 (RecordMap 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 Source #

Convert a type value back into a regular type

isTBit :: TValue -> Bool Source #

True if the evaluated value is Bit

tvSeq :: Nat' -> TValue -> TValue Source #

Produce a sequence type value

finNat' :: Nat' -> Integer Source #

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

evalType :: TypeEnv -> Type -> Either Nat' TValue Source #

Evaluation for types (kind * or #).

evalValType :: TypeEnv -> Type -> TValue Source #

Evaluation for value types (kind *).

evalNumType :: TypeEnv -> Type -> Nat' Source #

Evaluation for number types (kind #).

evalTF :: TFun -> [Nat'] -> Nat' Source #

Reduce type functions, raising an exception for undefined values.