cryptol-3.0.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
  - | TVFloat Integer Integer
  - | TVIntMod Integer
  - | TVRational
  - | TVArray TValue TValue
  - | TVSeq Integer TValue
  - | TVStream TValue
  - | TVTuple [TValue]
  - | TVRec (RecordMap Ident TValue)
  - | TVFun TValue TValue
  - | TVNewtype Newtype [Either Nat' TValue] (RecordMap Ident TValue)
  - | TVAbstract UserTC [Either Nat' TValue]
- tValTy :: TValue -> Type
- tNumTy :: Nat' -> Type
- tNumValTy :: Either Nat' TValue -> Type
- isTBit :: TValue -> Bool
- tvSeq :: Nat' -> TValue -> TValue
- tvFloat64 :: TValue
- finNat' :: Nat' -> Integer
- newtype TypeEnv = TypeEnv {
  - envTypeMap :: IntMap (Either Nat' TValue)
  }
- lookupTypeVar :: TVar -> TypeEnv -> Maybe (Either Nat' TValue)
- bindTypeVar :: TVar -> Either Nat' TValue -> TypeEnv -> TypeEnv
- evalType :: TypeEnv -> Type -> Either Nat' TValue
- evalNewtypeBody :: TypeEnv -> Newtype -> [Either Nat' TValue] -> RecordMap Ident TValue
- evalValType :: TypeEnv -> Type -> TValue
- evalNumType :: TypeEnv -> Type -> Nat'
- evalTF :: 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

TVNewtype Newtype [Either Nat' TValue] (RecordMap Ident TValue) | a named newtype
TVAbstract UserTC [Either Nat' TValue] | an abstract type

#### Instances

Instances details

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 #
Show TValue Source # |
Instance details Defined in Cryptol.Eval.Type Methods showsPrec :: Int -> TValue -> ShowS Source # show :: TValue -> String Source # showList :: [TValue] -> ShowS Source #
NFData TValue Source # |
Instance details Defined in Cryptol.Eval.Type Methods rnf :: TValue -> () Source #
Eq TValue Source # |
Instance details Defined in Cryptol.Eval.Type Methods (==) :: TValue -> TValue -> Bool Source # (/=) :: TValue -> TValue -> Bool Source #
type Rep TValue Source # |

Instance details

Defined in Cryptol.Eval.Type

type Rep TValue = D1 ('MetaData "TValue" "Cryptol.Eval.Type" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" '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 "TVNewtype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Newtype) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Either Nat' TValue]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RecordMap Ident 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

tNumTy :: Nat' -> Type Source #

tNumValTy :: Either Nat' TValue -> Type Source #

isTBit :: TValue -> Bool Source #

True if the evaluated value is `Bit`

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

Produce a sequence type value

tvFloat64 :: TValue Source #

The Cryptol `Float64` type.

finNat' :: Nat' -> Integer Source #

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

newtype TypeEnv Source #

Constructors

TypeEnv |

Fields

- envTypeMap :: IntMap (Either Nat' TValue)

#### Instances

Instances details

Monoid TypeEnv Source # |
Instance details Defined in Cryptol.Eval.Type Methods mempty :: TypeEnv Source # mappend :: TypeEnv -> TypeEnv -> TypeEnv Source # mconcat :: [TypeEnv] -> TypeEnv Source #
Semigroup TypeEnv Source # |
Instance details Defined in Cryptol.Eval.Type Methods (<>) :: TypeEnv -> TypeEnv -> TypeEnv Source # sconcat :: NonEmpty TypeEnv -> TypeEnv Source # stimes :: Integral b => b -> TypeEnv -> TypeEnv Source #
Show TypeEnv Source # |
Instance details Defined in Cryptol.Eval.Type Methods showsPrec :: Int -> TypeEnv -> ShowS Source # show :: TypeEnv -> String Source # showList :: [TypeEnv] -> ShowS Source #

lookupTypeVar :: TVar -> TypeEnv -> Maybe (Either Nat' TValue) Source #

bindTypeVar :: TVar -> Either Nat' TValue -> TypeEnv -> TypeEnv Source #

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

Evaluation for types (kind * or #).

evalNewtypeBody :: TypeEnv -> Newtype -> [Either Nat' TValue] -> RecordMap Ident TValue Source #

Evaluate the body of a newtype, given evaluated arguments

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.