| 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 = IntMap (Either Nat' TValue)
- evalType :: TypeEnv -> Type -> Either Nat' TValue
- evalValType :: TypeEnv -> Type -> TValue
- evalNumType :: TypeEnv -> Type -> Nat'
- evalTF :: 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 |
| 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 |