    {-# 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 :: forall sym.
    Backend sym =>
    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 a. a -> SEval sym a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure GenValue sym
    v