| 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
- 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
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
finNat' :: Nat' -> Integer Source #
Coerce an extended natural into an integer, for values known to be finite