{-# OPTIONS_GHC -Wall #-}

module FFI.OptimizerTrace
  ( Trace
  , mkFfiOptimizerTrace
  , 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 (Hints)
import UntypedPlutusCore.Transform.Optimizer
import Prelude hiding (head)

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

-- A certifier trace is a non-empty list of asts of type `a`, separated by the
-- optimizer pass that ran and the hints that were emitted
type Trace a = NonEmptySep (OptStage, Hints) a

mkFfiOptimizerTrace
  :: OptimizerTrace UPLC.Name UPLC.DefaultUni UPLC.DefaultFun a
  -> Trace FFI.UTerm
mkFfiOptimizerTrace :: forall a.
OptimizerTrace Name DefaultUni DefaultFun a -> Trace UTerm
mkFfiOptimizerTrace (OptimizerTrace [Optimization Name DefaultUni DefaultFun a]
simplNonEmptySep) = [Optimization Name DefaultUni DefaultFun a] -> Trace UTerm
forall a.
[Optimization Name DefaultUni DefaultFun a] -> Trace UTerm
go ([Optimization Name DefaultUni DefaultFun a]
-> [Optimization Name DefaultUni DefaultFun a]
forall a. [a] -> [a]
reverse [Optimization Name DefaultUni DefaultFun a]
simplNonEmptySep)
  where
    go
      :: [Optimization UPLC.Name UPLC.DefaultUni UPLC.DefaultFun a]
      -> Trace FFI.UTerm
    go :: forall a.
[Optimization Name DefaultUni DefaultFun a] -> Trace UTerm
go [] = [Char] -> Trace UTerm
forall a. HasCallStack => [Char] -> a
error [Char]
"Empty trace"
    go [Optimization Term Name DefaultUni DefaultFun a
before OptStage
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') ->
          UTerm -> (OptStage, Hints) -> Trace UTerm -> Trace UTerm
forall sep a. a -> sep -> NonEmptySep sep a -> NonEmptySep sep a
Cons
            (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'))
            (OptStage
stage, Hints
hints)
            (UTerm -> Trace UTerm
forall sep a. a -> NonEmptySep sep a
Singleton (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] -> Trace UTerm
forall a. HasCallStack => [Char] -> a
error ([Char] -> Trace UTerm) -> [Char] -> Trace 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] -> Trace UTerm
forall a. HasCallStack => [Char] -> a
error ([Char] -> Trace UTerm) -> [Char] -> Trace UTerm
forall a b. (a -> b) -> a -> b
$ FreeVariableError -> [Char]
forall a. Show a => a -> [Char]
show FreeVariableError
err
    -- ignore _after, it should be equal to subsequent before
    go (Optimization Term Name DefaultUni DefaultFun a
before OptStage
stage Hints
hints Term Name DefaultUni DefaultFun a
_after : [Optimization Name DefaultUni DefaultFun a]
xs) =
      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 of
        Right Term NamedDeBruijn DefaultUni DefaultFun a
before' ->
          UTerm -> (OptStage, Hints) -> Trace UTerm -> Trace UTerm
forall sep a. a -> sep -> NonEmptySep sep a -> NonEmptySep sep a
Cons (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')) (OptStage
stage, Hints
hints) ([Optimization Name DefaultUni DefaultFun a] -> Trace UTerm
forall a.
[Optimization Name DefaultUni DefaultFun a] -> Trace UTerm
go [Optimization Name DefaultUni DefaultFun a]
xs)
        Left (FreeVariableError
err :: UPLC.FreeVariableError) -> [Char] -> Trace UTerm
forall a. HasCallStack => [Char] -> a
error ([Char] -> Trace UTerm) -> [Char] -> Trace 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)