Make stepper update with elaboration

hazelgrove · May 17, 2024 · f810f62 · f810f62
1 parent eab25e9
commit f810f62
Show file tree

Hide file tree

Showing 6 changed files with 52 additions and 40 deletions.
diff --git a/src/haz3lcore/dynamics/Stepper.re b/src/haz3lcore/dynamics/Stepper.re
@@ -212,16 +212,6 @@ let step_pending = (idx: int, stepper: t) => {
   {...stepper, stepper_state: StepPending(idx)};
 };
 
-let init = ({d}: Elaborator.Elaboration.t) => {
-  let state = EvaluatorState.init;
-  let editor = ExpToSegment.exp_to_editor(~inline=false, d);
-  {
-    history: Aba.singleton((d, editor, state)),
-    next_options: decompose(d, state),
-    stepper_state: StepperReady,
-  };
-};
-
 let rec evaluate_pending = (~settings, s: t) => {
   switch (s.stepper_state) {
   | StepperDone
@@ -280,6 +270,17 @@ let rec evaluate_full = (~settings, s: t) => {
   };
 };
 
+let init = ({d}: Elaborator.Elaboration.t, ~settings) => {
+  let state = EvaluatorState.init;
+  let editor = ExpToSegment.exp_to_editor(~inline=false, d);
+  {
+    history: Aba.singleton((d, editor, state)),
+    next_options: decompose(d, state),
+    stepper_state: StepperReady,
+  }
+  |> evaluate_pending(~settings);
+};
+
 let timeout =
   fun
   | {stepper_state: StepPending(idx), _} as s => {
@@ -375,7 +376,8 @@ let get_history = (~settings, stepper) => {
       ((d, editor, state)) =>
         Aba.singleton(Aba.singleton((d, editor, state))),
       stepper.history,
-    );
+    )
+    |> Aba.map_a(Aba.rev(x => x, x => x));
   let replace_id = (x, y, (s, z)) => (s, x == z ? y : z);
   let track_ids =
       (

diff --git a/src/haz3lcore/prog/ModelResult.re b/src/haz3lcore/prog/ModelResult.re
@@ -16,15 +16,15 @@ type t =
 let init_eval = (elab: Elaborator.Elaboration.t) =>
   Evaluation({elab, evaluation: ResultPending, previous: ResultPending});
 
-let update_elab = elab =>
+let update_elab = (elab, ~settings) =>
   fun
   | NoElab =>
     Evaluation({elab, evaluation: ResultPending, previous: ResultPending})
   | Evaluation({evaluation, _}) =>
     Evaluation({elab, evaluation: ResultPending, previous: evaluation})
   | Stepper(s) as s' when DHExp.fast_equal(elab.d, Stepper.get_elab(s).d) => s'
   | Stepper(_) => {
-      Stepper(Stepper.init(elab));
+      Stepper(Stepper.init(elab, ~settings));
     };
 
 let update_stepper = f =>
@@ -94,10 +94,10 @@ let timeout: t => t =
     Evaluation({...e, evaluation: ResultFail(Timeout), previous: evaluation})
   | Stepper(s) => Stepper(Stepper.timeout(s));
 
-let toggle_stepper =
+let toggle_stepper = (~settings) =>
   fun
   | NoElab => NoElab
-  | Evaluation({elab, _}) => Stepper(Stepper.init(elab))
+  | Evaluation({elab, _}) => Stepper(Stepper.init(~settings, elab))
   | Stepper(s) =>
     Evaluation({
       elab: Stepper.get_elab(s),

diff --git a/src/haz3lcore/prog/ModelResults.re b/src/haz3lcore/prog/ModelResults.re
@@ -22,15 +22,15 @@ type t = M.t(ModelResult.t);
 let init_eval = (ds: list((Key.t, Elaborator.Elaboration.t))): t =>
   ds |> List.to_seq |> of_seq |> map(ModelResult.init_eval);
 
-let update_elabs =
+let update_elabs = (~settings) =>
   List.fold_right(((k, elab), acc) =>
     update(
       k,
       v =>
         Some(
           v
           |> Option.value(~default=ModelResult.NoElab)
-          |> ModelResult.update_elab(elab),
+          |> ModelResult.update_elab(~settings, elab),
         ),
       acc,
     )

diff --git a/src/haz3lweb/Log.re b/src/haz3lweb/Log.re
@@ -12,6 +12,8 @@ let is_action_logged: UpdateAction.t => bool =
   | FinishImportAll(_)
   | FinishImportScratchpad(_)
   | Benchmark(_)
+  | UpdateResult(_)
+  | UpdateEvals(_)
   | DebugConsole(_) => false
   | Reset
   | TAB
@@ -28,8 +30,6 @@ let is_action_logged: UpdateAction.t => bool =
   | Undo
   | Redo
   | MoveToNextHole(_)
-  | UpdateResult(_)
-  | UpdateEvals(_)
   | ToggleStepper(_)
   | StepperAction(_, StepForward(_) | StepBackward | HideStepper)
   | UpdateExplainThisModel(_) => true;

diff --git a/src/haz3lweb/Update.re b/src/haz3lweb/Update.re
@@ -210,7 +210,12 @@ let schedule_evaluation = (~schedule_action, model: Model.t): unit =>
       );
     };
     /* Not sending stepper to worker for now bc closure perf */
-    let new_rs = model.results |> ModelResults.update_elabs(elabs);
+    let new_rs =
+      model.results
+      |> ModelResults.update_elabs(
+           ~settings=model.settings.core.evaluation,
+           elabs,
+         );
     let step_rs = ModelResults.to_step(new_rs);
     if (!ModelResults.is_empty(step_rs)) {
       let new_rs =
@@ -548,7 +553,9 @@ let rec apply =
                Some(
                  v
                  |> Option.value(~default=NoElab: ModelResult.t)
-                 |> ModelResult.toggle_stepper,
+                 |> ModelResult.toggle_stepper(
+                      ~settings=model.settings.core.evaluation,
+                    ),
                )
              ),
       })

diff --git a/src/haz3lweb/view/Cell.re b/src/haz3lweb/view/Cell.re
@@ -186,7 +186,7 @@ let stepper_view =
     Stepper.get_history(~settings=settings.core.evaluation, stepper);
   switch (history) {
   | [] => []
-  | [hd, ...tl] =>
+  | [hd, ..._] =>
     let button_back =
       Widgets.button_d(
         Icons.undo,
@@ -276,26 +276,29 @@ let stepper_view =
       (
         settings.core.evaluation.stepper_history
           ? {
-            let steps: list((bool, Stepper.step_info)) =
-              List.map(
-                step =>
-                  [
-                    (false, step),
-                    ...settings.core.evaluation.show_hidden_steps
-                         ? Stepper.hidden_steps_of_info(step)
-                           |> List.map(x => (true, x))
-                         : [],
-                  ],
-                tl,
+              let steps: list((bool, Stepper.step_info)) =
+                List.map(
+                  step =>
+                    [
+                      (false, step),
+                      ...settings.core.evaluation.show_hidden_steps
+                           ? Stepper.hidden_steps_of_info(step)
+                             |> List.map(x => (true, x))
+                           : [],
+                    ],
+                  history,
+                )
+                |> List.flatten;
+              List.mapi(
+                (idx, (hidden, step)) =>
+                  previous_step(~hidden, ~idx=idx + 1, step),
+                steps |> List.rev,
               )
               |> List.flatten;
-            List.mapi(
-              (idx, (hidden, step)) =>
-                previous_step(~hidden, ~idx=idx + 1, step),
-              steps,
-            )
-            |> List.flatten;
-          }
+            }
+            |> List.rev
+            |> List.tl
+            |> List.rev
           : []
       )
       @ [current]