Prims.hs

{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE LambdaCase #-}
module Cryptol.Eval.Prims where

import Cryptol.Backend
import Cryptol.Eval.Type
import Cryptol.Eval.Value
import Cryptol.ModuleSystem.Name
import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
import Cryptol.Utils.Panic

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

-- | Evaluate a primitive into a value computation
evalPrim :: Backend sym => sym -> Name -> Prim sym -> SEval sym (GenValue sym)
evalPrim sym nm p = case p of
  PFun f      -> lam sym (evalPrim sym nm . f)
  PStrict f   -> lam sym (\x -> evalPrim sym nm . f =<< x)
  PWordFun f  -> lam sym (\x -> evalPrim sym nm . f =<< (fromVWord sym (show nm) =<< x))
  PFloatFun f -> flam sym (evalPrim sym nm . f)
  PTyPoly f   -> tlam sym (evalPrim sym nm . f)
  PNumPoly f  -> nlam sym (evalPrim sym nm . f)
  PFinPoly f  -> nlam sym (\case Inf -> panic "PFin" ["Unexpected `inf`", show nm];
                                 Nat n -> evalPrim sym nm (f n))
  PPrim m     -> m
  PVal v      -> pure v