Copyright	(c) 2013-2016 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	Safe
Language	Haskell2010

Cryptol.Eval.Type

Description

Synopsis

data TValue
- = TVBit
- | TVInteger
- | TVFloat Integer Integer
- | TVIntMod Integer
- | TVRational
- | TVArray TValue TValue
- | TVSeq Integer TValue
- | TVStream TValue
- | TVTuple [TValue]
- | TVRec (RecordMap Ident TValue)
- | TVFun TValue TValue
- | TVAbstract UserTC [Either Nat' TValue]
tValTy :: TValue -> Type
isTBit :: TValue -> Bool
tvSeq :: Nat' -> TValue -> TValue
finNat' :: Nat' -> Integer
type TypeEnv = Map TVar (Either Nat' TValue)
evalType :: HasCallStack => TypeEnv -> Type -> Either Nat' TValue
evalValType :: HasCallStack => TypeEnv -> Type -> TValue
evalNumType :: HasCallStack => TypeEnv -> Type -> Nat'
evalTF :: HasCallStack => TFun -> [Nat'] -> Nat'

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

Show TValue Source #
Instance details Defined in Cryptol.Eval.Type Methods showsPrec :: Int -> TValue -> ShowS # show :: TValue -> String # showList :: [TValue] -> ShowS #
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.9.1-EDtcoHURvveHmx5M6ZZjMK" 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

type TypeEnv = Map TVar (Either Nat' TValue) Source #

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

Evaluation for types (kind * or #).

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

Evaluation for value types (kind *).

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

Evaluation for number types (kind #).

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

Reduce type functions, raising an exception for undefined values.