{-# 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 -> Name -> Prim sym -> SEval sym (GenValue sym)
evalPrim sym
sym Name
nm Prim sym
p = case Prim sym
p of
  PFun SEval sym (GenValue sym) -> Prim sym
f      -> sym
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
lam sym
sym (sym -> Name -> Prim sym -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> Name -> Prim sym -> SEval sym (GenValue sym)
evalPrim sym
sym Name
nm (Prim sym -> SEval sym (GenValue sym))
-> (SEval sym (GenValue sym) -> Prim sym)
-> SEval sym (GenValue sym)
-> SEval sym (GenValue sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SEval sym (GenValue sym) -> Prim sym
f)
  PStrict GenValue sym -> Prim sym
f   -> sym
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
lam sym
sym (\SEval sym (GenValue sym)
x -> sym -> Name -> Prim sym -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> Name -> Prim sym -> SEval sym (GenValue sym)
evalPrim sym
sym Name
nm (Prim sym -> SEval sym (GenValue sym))
-> (GenValue sym -> Prim sym)
-> GenValue sym
-> SEval sym (GenValue sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenValue sym -> Prim sym
f (GenValue sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym) -> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
x)
  PWordFun SWord sym -> Prim sym
f  -> sym
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> (SEval sym (GenValue sym) -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
lam sym
sym (\SEval sym (GenValue sym)
x -> sym -> Name -> Prim sym -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> Name -> Prim sym -> SEval sym (GenValue sym)
evalPrim sym
sym Name
nm (Prim sym -> SEval sym (GenValue sym))
-> (SWord sym -> Prim sym) -> SWord sym -> SEval sym (GenValue sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SWord sym -> Prim sym
f (SWord sym -> SEval sym (GenValue sym))
-> SEval sym (SWord sym) -> SEval sym (GenValue sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (sym -> String -> GenValue sym -> SEval sym (SWord sym)
forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord sym
sym (Name -> String
forall a. Show a => a -> String
show Name
nm) (GenValue sym -> SEval sym (SWord sym))
-> SEval sym (GenValue sym) -> SEval sym (SWord sym)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< SEval sym (GenValue sym)
x))
  PFloatFun SFloat sym -> Prim sym
f -> sym
-> (SFloat sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> (SFloat sym -> SEval sym (GenValue sym))
-> SEval sym (GenValue sym)
flam sym
sym (sym -> Name -> Prim sym -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> Name -> Prim sym -> SEval sym (GenValue sym)
evalPrim sym
sym Name
nm (Prim sym -> SEval sym (GenValue sym))
-> (SFloat sym -> Prim sym)
-> SFloat sym
-> SEval sym (GenValue sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SFloat sym -> Prim sym
f)
  PTyPoly TValue -> Prim sym
f   -> sym
-> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> (TValue -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
tlam sym
sym (sym -> Name -> Prim sym -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> Name -> Prim sym -> SEval sym (GenValue sym)
evalPrim sym
sym Name
nm (Prim sym -> SEval sym (GenValue sym))
-> (TValue -> Prim sym) -> TValue -> SEval sym (GenValue sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TValue -> Prim sym
f)
  PNumPoly Nat' -> Prim sym
f  -> sym
-> (Nat' -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> (Nat' -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
nlam sym
sym (sym -> Name -> Prim sym -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> Name -> Prim sym -> SEval sym (GenValue sym)
evalPrim sym
sym Name
nm (Prim sym -> SEval sym (GenValue sym))
-> (Nat' -> Prim sym) -> Nat' -> SEval sym (GenValue sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat' -> Prim sym
f)
  PFinPoly Integer -> Prim sym
f  -> sym
-> (Nat' -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym
-> (Nat' -> SEval sym (GenValue sym)) -> SEval sym (GenValue sym)
nlam sym
sym (\case Nat'
Inf -> String -> [String] -> SEval sym (GenValue sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"PFin" [String
"Unexpected `inf`", Name -> String
forall a. Show a => a -> String
show Name
nm];
                                 Nat Integer
n -> sym -> Name -> Prim sym -> SEval sym (GenValue sym)
forall sym.
Backend sym =>
sym -> Name -> Prim sym -> SEval sym (GenValue sym)
evalPrim sym
sym Name
nm (Integer -> Prim sym
f Integer
n))
  PPrim SEval sym (GenValue sym)
m     -> SEval sym (GenValue sym)
m
  PVal GenValue sym
v      -> GenValue sym -> SEval sym (GenValue sym)
forall (f :: * -> *) a. Applicative f => a -> f a
pure GenValue sym
v