port stepper function

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

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)))