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
- 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
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 Source # | |
Generic TValue Source # | |
NFData TValue Source # | |
Defined in Cryptol.Eval.Type | |
type Rep TValue Source # | |
Defined in Cryptol.Eval.Type type Rep TValue = D1 ('MetaData "TValue" "Cryptol.Eval.Type" "cryptol-2.8.0-8MjdO3NUDs4I9u4d2J06AM" '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])))))) |
finNat' :: Nat' -> Integer Source #
Coerce an extended natural into an integer, for values known to be finite
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 #).