1{-# LANGUAGE ImplicitParams #-}
2{-# LANGUAGE LambdaCase #-}
3module Cryptol.Eval.Prims where
4
5import Cryptol.Backend
6import Cryptol.Eval.Type
7import Cryptol.Eval.Value
8import Cryptol.ModuleSystem.Name
9import Cryptol.TypeCheck.Solver.InfNat(Nat'(..))
10import Cryptol.Utils.Panic
11
12-- | This type provides a lightweight syntactic framework for defining
13--   Cryptol primitives.  The main purpose of this type is to provide
14--   an abstraction barrier that insulates the definitions of primitives
15--   from possible changes in the representation of values.
16data Prim sym
17  = PFun (SEval sym (GenValue sym) -> Prim sym)
18  | PStrict (GenValue sym -> Prim sym)
19  | PWordFun (SWord sym -> Prim sym)
20  | PFloatFun (SFloat sym -> Prim sym)
21  | PTyPoly (TValue -> Prim sym)
22  | PNumPoly (Nat' -> Prim sym)
23  | PFinPoly (Integer -> Prim sym)
24  | PPrim (SEval sym (GenValue sym))
25  | PVal (GenValue sym)
26
27-- | Evaluate a primitive into a value computation
28evalPrim :: Backend sym => sym -> Name -> Prim sym -> SEval sym (GenValue sym)
29evalPrim sym nm p = case p of
30  PFun f      -> lam sym (evalPrim sym nm . f)
31  PStrict f   -> lam sym (\x -> evalPrim sym nm . f =<< x)
32  PWordFun f  -> lam sym (\x -> evalPrim sym nm . f =<< (fromVWord sym (show nm) =<< x))
33  PFloatFun f -> flam sym (evalPrim sym nm . f)
34  PTyPoly f   -> tlam sym (evalPrim sym nm . f)
35  PNumPoly f  -> nlam sym (evalPrim sym nm . f)
36  PFinPoly f  -> nlam sym (\case Inf -> panic "PFin" ["Unexpected `inf`", show nm];
37                                 Nat n -> evalPrim sym nm (f n))
38  PPrim m     -> m
39  PVal v      -> pure v
40