Safe Haskell	Safe-Inferred
Language	Haskell2010

Cryptol.Eval.Prims

Synopsis

data Prim sym
- = PFun (SEval sym (GenValue sym) -> Prim sym)
- | PStrict (GenValue sym -> Prim sym)
- | PWordFun (SWord sym -> Prim sym)
- | PFloatFun (SFloat sym -> Prim sym)
- | PTyPoly (TValue -> Prim sym)
- | PNumPoly (Nat' -> Prim sym)
- | PFinPoly (Integer -> Prim sym)
- | PPrim (SEval sym (GenValue sym))
- | PVal (GenValue sym)
evalPrim :: Backend sym => sym -> Name -> Prim sym -> SEval sym (GenValue sym)

Documentation

data Prim sym Source #

This type provides a lightweight syntactic framework for defining Cryptol primitives. The main purpose of this type is to provide an abstraction barrier that insulates the definitions of primitives from possible changes in the representation of values.

Constructors

PFun (SEval sym (GenValue sym) -> Prim sym)
PStrict (GenValue sym -> Prim sym)
PWordFun (SWord sym -> Prim sym)
PFloatFun (SFloat sym -> Prim sym)
PTyPoly (TValue -> Prim sym)
PNumPoly (Nat' -> Prim sym)
PFinPoly (Integer -> Prim sym)
PPrim (SEval sym (GenValue sym))
PVal (GenValue sym)

evalPrim :: Backend sym => sym -> Name -> Prim sym -> SEval sym (GenValue sym) Source #

Evaluate a primitive into a value computation