Copyright	(c) 2013-2016 Galois Inc.
License	BSD3
Maintainer	cryptol@galois.com
Stability	provisional
Portability	portable
Safe Haskell	Safe-Inferred
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
- | TVNominal NominalType [Either Nat' TValue] TNominalTypeValue
data TNominalTypeValue
- = TVStruct (RecordMap Ident TValue)
- | TVEnum (Vector (ConInfo TValue))
- | TVAbstract
data ConInfo a = ConInfo {
- conIdent :: Ident
- conFields :: Vector a
}
isNullaryCon :: ConInfo a -> Bool
zipConInfo :: (a -> b -> c) -> ConInfo a -> ConInfo b -> ConInfo c
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
evalNominalTypeBody :: TypeEnv -> NominalType -> [Either Nat' TValue] -> TNominalTypeValue
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
TVNominal NominalType [Either Nat' TValue] TNominalTypeValue	a named newtype

Instances

Instances details

Generic TValue Source #
Instance details Defined in Cryptol.Eval.Type Associated Types type Rep TValue :: Type -> Type # Methods from :: TValue -> Rep TValue x # to :: Rep TValue x -> TValue #
Show TValue Source #
Instance details Defined in Cryptol.Eval.Type Methods showsPrec :: Int -> TValue -> ShowS # show :: TValue -> String # showList :: [TValue] -> ShowS #
NFData TValue Source #
Instance details Defined in Cryptol.Eval.Type Methods rnf :: TValue -> () #
Eq TValue Source #
Instance details Defined in Cryptol.Eval.Type Methods (==) :: TValue -> TValue -> Bool # (/=) :: TValue -> TValue -> Bool #
type Rep TValue Source #
Instance details Defined in Cryptol.Eval.Type type Rep TValue = D1 ('MetaData "TValue" "Cryptol.Eval.Type" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" '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 "TVNominal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NominalType) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Either Nat' TValue]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TNominalTypeValue)))))))

data TNominalTypeValue Source #

Constructors

TVStruct (RecordMap Ident TValue)
TVEnum (Vector (ConInfo TValue))	Indexed by constructor number
TVAbstract

Instances

Instances details

Generic TNominalTypeValue Source #
Instance details Defined in Cryptol.Eval.Type Associated Types type Rep TNominalTypeValue :: Type -> Type # Methods from :: TNominalTypeValue -> Rep TNominalTypeValue x # to :: Rep TNominalTypeValue x -> TNominalTypeValue #
NFData TNominalTypeValue Source #
Instance details Defined in Cryptol.Eval.Type Methods rnf :: TNominalTypeValue -> () #
Eq TNominalTypeValue Source #
Instance details Defined in Cryptol.Eval.Type Methods (==) :: TNominalTypeValue -> TNominalTypeValue -> Bool # (/=) :: TNominalTypeValue -> TNominalTypeValue -> Bool #
type Rep TNominalTypeValue Source #
Instance details Defined in Cryptol.Eval.Type type Rep TNominalTypeValue = D1 ('MetaData "TNominalTypeValue" "Cryptol.Eval.Type" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "TVStruct" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (RecordMap Ident TValue))) :+: (C1 ('MetaCons "TVEnum" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Vector (ConInfo TValue)))) :+: C1 ('MetaCons "TVAbstract" 'PrefixI 'False) (U1 :: Type -> Type)))

data ConInfo a Source #

Constructors

ConInfo
Fields conIdent :: Ident conFields :: Vector a

Instances

Instances details

Foldable ConInfo Source #
Instance details Defined in Cryptol.Eval.Type Methods fold :: Monoid m => ConInfo m -> m # foldMap :: Monoid m => (a -> m) -> ConInfo a -> m # foldMap' :: Monoid m => (a -> m) -> ConInfo a -> m # foldr :: (a -> b -> b) -> b -> ConInfo a -> b # foldr' :: (a -> b -> b) -> b -> ConInfo a -> b # foldl :: (b -> a -> b) -> b -> ConInfo a -> b # foldl' :: (b -> a -> b) -> b -> ConInfo a -> b # foldr1 :: (a -> a -> a) -> ConInfo a -> a # foldl1 :: (a -> a -> a) -> ConInfo a -> a # toList :: ConInfo a -> [a] # null :: ConInfo a -> Bool # length :: ConInfo a -> Int # elem :: Eq a => a -> ConInfo a -> Bool # maximum :: Ord a => ConInfo a -> a # minimum :: Ord a => ConInfo a -> a # sum :: Num a => ConInfo a -> a # product :: Num a => ConInfo a -> a #
Traversable ConInfo Source #
Instance details Defined in Cryptol.Eval.Type Methods traverse :: Applicative f => (a -> f b) -> ConInfo a -> f (ConInfo b) # sequenceA :: Applicative f => ConInfo (f a) -> f (ConInfo a) # mapM :: Monad m => (a -> m b) -> ConInfo a -> m (ConInfo b) # sequence :: Monad m => ConInfo (m a) -> m (ConInfo a) #
Functor ConInfo Source #
Instance details Defined in Cryptol.Eval.Type Methods fmap :: (a -> b) -> ConInfo a -> ConInfo b # (<$) :: a -> ConInfo b -> ConInfo a #
Generic (ConInfo a) Source #
Instance details Defined in Cryptol.Eval.Type Associated Types type Rep (ConInfo a) :: Type -> Type # Methods from :: ConInfo a -> Rep (ConInfo a) x # to :: Rep (ConInfo a) x -> ConInfo a #
NFData a => NFData (ConInfo a) Source #
Instance details Defined in Cryptol.Eval.Type Methods rnf :: ConInfo a -> () #
Eq a => Eq (ConInfo a) Source #
Instance details Defined in Cryptol.Eval.Type Methods (==) :: ConInfo a -> ConInfo a -> Bool # (/=) :: ConInfo a -> ConInfo a -> Bool #
type Rep (ConInfo a) Source #
Instance details Defined in Cryptol.Eval.Type type Rep (ConInfo a) = D1 ('MetaData "ConInfo" "Cryptol.Eval.Type" "cryptol-3.1.0-276efOa9Q2aIFSEzDdp2Mp" 'False) (C1 ('MetaCons "ConInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "conIdent") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident) :*: S1 ('MetaSel ('Just "conFields") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Vector a))))

isNullaryCon :: ConInfo a -> Bool Source #

zipConInfo :: (a -> b -> c) -> ConInfo a -> ConInfo b -> ConInfo c Source #

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

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 #).

evalNominalTypeBody :: TypeEnv -> NominalType -> [Either Nat' TValue] -> TNominalTypeValue 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.