{-# OPTIONS_GHC -Wall #-}

module FFI.SimplifierTrace
  ( TraceElem
  , Trace
  , mkFfiSimplifierTrace
  , toEvalResult
  ) where

import FFI.CostInfo
import FFI.Untyped qualified as FFI
import PlutusCore.Evaluation.Machine.ExBudget
import PlutusCore.Evaluation.Machine.ExMemory
import UntypedPlutusCore qualified as UPLC
import UntypedPlutusCore.Evaluation.Machine.Cek
import UntypedPlutusCore.Transform.Certify.Hints qualified as Certify
import UntypedPlutusCore.Transform.Simplifier

import Data.Coerce
import Data.Functor
import Data.SatInt
import Data.Text qualified as T

type TraceElem a = (SimplifierStage, (Certify.Hints, (a, a)))
type Trace a = [TraceElem a]

mkFfiSimplifierTrace
  :: SimplifierTrace UPLC.Name UPLC.DefaultUni UPLC.DefaultFun a
  -> Trace FFI.UTerm
mkFfiSimplifierTrace :: forall a.
SimplifierTrace Name DefaultUni DefaultFun a -> Trace UTerm
mkFfiSimplifierTrace (SimplifierTrace [Simplification Name DefaultUni DefaultFun a]
simplTrace) = Trace UTerm -> Trace UTerm
forall a. [a] -> [a]
reverse (Trace UTerm -> Trace UTerm) -> Trace UTerm -> Trace UTerm
forall a b. (a -> b) -> a -> b
$ Simplification Name DefaultUni DefaultFun a
-> (SimplifierStage, (Hints, (UTerm, UTerm)))
forall {a}.
Simplification Name DefaultUni DefaultFun a
-> (SimplifierStage, (Hints, (UTerm, UTerm)))
toFfiAst (Simplification Name DefaultUni DefaultFun a
 -> (SimplifierStage, (Hints, (UTerm, UTerm))))
-> [Simplification Name DefaultUni DefaultFun a] -> Trace UTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Simplification Name DefaultUni DefaultFun a]
simplTrace
  where
    toFfiAst :: Simplification Name DefaultUni DefaultFun a
-> (SimplifierStage, (Hints, (UTerm, UTerm)))
toFfiAst (Simplification Term Name DefaultUni DefaultFun a
before SimplifierStage
stage Hints
hints Term Name DefaultUni DefaultFun a
after) =
      case (Term Name DefaultUni DefaultFun a
-> Either
     FreeVariableError (Term NamedDeBruijn DefaultUni DefaultFun a)
forall (m :: * -> *) (uni :: * -> *) fun ann.
MonadError FreeVariableError m =>
Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
UPLC.deBruijnTerm Term Name DefaultUni DefaultFun a
before, Term Name DefaultUni DefaultFun a
-> Either
     FreeVariableError (Term NamedDeBruijn DefaultUni DefaultFun a)
forall (m :: * -> *) (uni :: * -> *) fun ann.
MonadError FreeVariableError m =>
Term Name uni fun ann -> m (Term NamedDeBruijn uni fun ann)
UPLC.deBruijnTerm Term Name DefaultUni DefaultFun a
after) of
        (Right Term NamedDeBruijn DefaultUni DefaultFun a
before', Right Term NamedDeBruijn DefaultUni DefaultFun a
after') ->
          (SimplifierStage
stage, (Hints
hints, (Term NamedDeBruijn DefaultUni DefaultFun () -> UTerm
forall a. Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
FFI.conv (Term NamedDeBruijn DefaultUni DefaultFun a
-> Term NamedDeBruijn DefaultUni DefaultFun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term NamedDeBruijn DefaultUni DefaultFun a
before'), Term NamedDeBruijn DefaultUni DefaultFun () -> UTerm
forall a. Term NamedDeBruijn DefaultUni DefaultFun a -> UTerm
FFI.conv (Term NamedDeBruijn DefaultUni DefaultFun a
-> Term NamedDeBruijn DefaultUni DefaultFun ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Term NamedDeBruijn DefaultUni DefaultFun a
after'))))
        (Left (FreeVariableError
err :: UPLC.FreeVariableError), Either
  FreeVariableError (Term NamedDeBruijn DefaultUni DefaultFun a)
_) -> [Char] -> (SimplifierStage, (Hints, (UTerm, UTerm)))
forall a. HasCallStack => [Char] -> a
error ([Char] -> (SimplifierStage, (Hints, (UTerm, UTerm))))
-> [Char] -> (SimplifierStage, (Hints, (UTerm, UTerm)))
forall a b. (a -> b) -> a -> b
$ FreeVariableError -> [Char]
forall a. Show a => a -> [Char]
show FreeVariableError
err
        (Either
  FreeVariableError (Term NamedDeBruijn DefaultUni DefaultFun a)
_, Left (FreeVariableError
err :: UPLC.FreeVariableError)) -> [Char] -> (SimplifierStage, (Hints, (UTerm, UTerm)))
forall a. HasCallStack => [Char] -> a
error ([Char] -> (SimplifierStage, (Hints, (UTerm, UTerm))))
-> [Char] -> (SimplifierStage, (Hints, (UTerm, UTerm)))
forall a b. (a -> b) -> a -> b
$ FreeVariableError -> [Char]
forall a. Show a => a -> [Char]
show FreeVariableError
err

toEvalResult
  :: Maybe (CekEvaluationException UPLC.NamedDeBruijn UPLC.DefaultUni UPLC.DefaultFun)
  -> ExBudget
  -> EvalResult
toEvalResult :: Maybe (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
-> ExBudget -> EvalResult
toEvalResult Maybe (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
res ExBudget
budget = case Maybe (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
res of
  Just CekEvaluationException NamedDeBruijn DefaultUni DefaultFun
err -> Text -> Integer -> Integer -> EvalResult
EvalFailure ([Char] -> Text
T.pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ CekEvaluationException NamedDeBruijn DefaultUni DefaultFun
-> [Char]
forall a. Show a => a -> [Char]
show CekEvaluationException NamedDeBruijn DefaultUni DefaultFun
err) Integer
cpu Integer
mem
  Maybe (CekEvaluationException NamedDeBruijn DefaultUni DefaultFun)
Nothing -> Integer -> Integer -> EvalResult
EvalSuccess Integer
cpu Integer
mem
  where
    cpu :: Integer
cpu = SatInt -> Integer
forall a. Num a => SatInt -> a
fromSatInt (SatInt -> Integer) -> SatInt -> Integer
forall a b. (a -> b) -> a -> b
$ ExCPU -> SatInt
forall a b. Coercible a b => a -> b
coerce (ExBudget -> ExCPU
exBudgetCPU ExBudget
budget)
    mem :: Integer
mem = SatInt -> Integer
forall a. Num a => SatInt -> a
fromSatInt (SatInt -> Integer) -> SatInt -> Integer
forall a b. (a -> b) -> a -> b
$ ExMemory -> SatInt
forall a b. Coercible a b => a -> b
coerce (ExBudget -> ExMemory
exBudgetMemory ExBudget
budget)