From 0a280d77a098945aa903f62aac6897ef8b11bb2d Mon Sep 17 00:00:00 2001
From: James Chapman <james.chapman@iohk.io>
Date: Mon, 17 Jan 2022 17:11:07 +0000
Subject: [PATCH] port stepper function

---
 plutus-metatheory/src/Algorithmic/Evaluation.lagda | 4 ++--
 plutus-metatheory/src/Main.lagda                   | 8 ++++----
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/plutus-metatheory/src/Algorithmic/Evaluation.lagda b/plutus-metatheory/src/Algorithmic/Evaluation.lagda
index 2f7a12ddbfd..2d3c331bf8a 100644
--- a/plutus-metatheory/src/Algorithmic/Evaluation.lagda
+++ b/plutus-metatheory/src/Algorithmic/Evaluation.lagda
@@ -11,7 +11,7 @@ open import Utils
 open import Type
 open import Type.BetaNormal
 open import Algorithmic
-open import Algorithmic.Reduction
+open import Algorithmic.ReductionEC
 \end{code}
 
 ## Evaluation
@@ -42,7 +42,7 @@ data Finished {A : ∅ ⊢Nf⋆ *} :  (N : ∅ ⊢ A) →  Set where
 --   neutral : {L : ∅ ⊢ A} → Neutral L → Finished L
 \end{code}
 Given a term `L` of type `A`, the evaluator will, for some `N`, return
-a reduction sequence from `L` to `N` and an indication of whether
+Ma reduction sequence from `L` to `N` and an indication of whether
 reduction finished.
 \begin{code}
 data Steps : ∀ {A : ∅ ⊢Nf⋆ *} → ∅ ⊢ A → Set where
diff --git a/plutus-metatheory/src/Main.lagda b/plutus-metatheory/src/Main.lagda
index 5937a226ff2..abb39688d5a 100644
--- a/plutus-metatheory/src/Main.lagda
+++ b/plutus-metatheory/src/Main.lagda
@@ -40,6 +40,9 @@ open import Algorithmic.Reduction
 open import Algorithmic.CK
 open import Algorithmic.CEKV
 open import Algorithmic.Erasure
+import Algorithmic.Evaluation as L
+
+
 
 -- There's a long prelude here that could go in a different file but
 -- currently it's only used here
@@ -267,8 +270,7 @@ just t' ← withE runtimeError $ U.stepper maxsteps (ε ; [] ▻ erase t)
   return $ prettyPrintUTm (U.extricateU0 (U.discharge V))
 executePLC TL t = do
   (A ,, t) ← withE (λ e → typeError (uglyTypeError e)) $ typeCheckPLC t
-  just t' ← withE runtimeError $ Algorithmic.Reduction.progressor maxsteps t
-    where nothing → inj₁ (runtimeError userError)
+  t' ← withE runtimeError $ L.stepper t maxsteps
   return (prettyPrintTm (unshifter Z (extricateScope (extricate t'))))
 executePLC TCK t = do
   (A ,, t) ← withE (λ e → typeError (uglyTypeError e)) $ typeCheckPLC t
@@ -508,8 +510,6 @@ normalizeTypeTerm t = do
 
 -- Haskell interface to (typechecked and proven correct) reduction
 
-import Algorithmic.Evaluation as L
-
 runTL : Term → Either ERROR Term
 runTL t = do
   tDB ← withE scopeError (scopeCheckTm {0}{Z} (shifter Z (convTm t)))