cryptol-2.6.0: Cryptol: The Language of Cryptography

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
  - | TVIntMod Integer
  - | TVSeq Integer TValue
  - | TVStream TValue
  - | TVTuple [TValue]
  - | TVRec [(Ident, TValue)]
  - | TVFun TValue 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

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

Instances

Show TValue Source # |
Instance details Defined in Cryptol.Eval.Type Methods showsPrec :: Int -> TValue -> ShowS Source # show :: TValue -> String Source # showList :: [TValue] -> ShowS Source #
Generic TValue Source # |
Instance details Defined in Cryptol.Eval.Type Associated Types type Rep TValue :: Type -> Type Source # Methods from :: TValue -> Rep TValue x Source # to :: Rep TValue x -> TValue Source #
NFData TValue Source # |
Instance details Defined in Cryptol.Eval.Type Methods rnf :: TValue -> () Source #
type Rep TValue Source # |

Instance details

Defined in Cryptol.Eval.Type

type Rep TValue = D1 (MetaData "TValue" "Cryptol.Eval.Type" "cryptol-2.6.0-FO78l5UWBYr51eDL1ksQpO" 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)))))

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.