Show hidden steps (#1219)

src/haz3lcore/dynamics/Stepper.re

@@ -413,9 +413,9 @@ let get_justification: step_kind => string =
   | VarLookup => "variable lookup"
   | CastAp
   | Cast => "cast calculus"
-  | CompleteFilter => "unidentified step"
-  | CompleteClosure => "unidentified step"
-  | FunClosure => "unidentified step"
+  | CompleteFilter => "complete filter"
+  | CompleteClosure => "complete closure"
+  | FunClosure => "function closure"
   | Skip => "skipped steps";
 
 let get_history = (~settings, stepper) => {

src/haz3lcore/prog/CoreSettings.re

@@ -12,6 +12,7 @@ module Evaluation = {
     // TODO[Matt]: Move this to somewhere where it is a per-scratch setting
     stepper_history: bool,
     show_settings: bool,
+    show_hidden_steps: bool,
   };
 
   let init = {
@@ -23,6 +24,7 @@ module Evaluation = {
     show_stepper_filters: false,
     stepper_history: false,
     show_settings: false,
+    show_hidden_steps: false,
   };
 };
 

src/haz3lweb/Init.ml

@@ -20,6 +20,7 @@ let startup : PersistentData.t =
                 show_stepper_filters = false;
                 stepper_history = false;
                 show_settings = false;
+                show_hidden_steps = false;
               };
           };
         async_evaluation = false;

src/haz3lweb/Update.re

@@ -93,6 +93,10 @@ let update_settings =
           ...evaluation,
           show_settings: !evaluation.show_settings,
         }
+      | ShowHiddenSteps => {
+          ...evaluation,
+          show_hidden_steps: !evaluation.show_hidden_steps,
+        }
       };
     };
     {

src/haz3lweb/UpdateAction.re

@@ -11,7 +11,8 @@ type evaluation_settings_action =
   | ShowFixpoints
   | ShowLookups
   | ShowFilters
-  | ShowSettings;
+  | ShowSettings
+  | ShowHiddenSteps;
 
 [@deriving (show({with_path: false}), sexp, yojson)]
 type settings_action =
@@ -178,7 +179,8 @@ let reevaluate_post_update: t => bool =
         ShowCaseClauses | ShowFnBodies | ShowCasts | ShowRecord | ShowFixpoints |
         ShowLookups |
         ShowFilters |
-        ShowSettings,
+        ShowSettings |
+        ShowHiddenSteps,
       ) =>
       false
     | Elaborate

src/haz3lweb/view/NutMenu.re

@@ -94,6 +94,12 @@ let settings_menu =
       evaluation.show_stepper_filters,
       Evaluation(ShowFilters),
     ),
+    toggle(
+      "🤫",
+      "Show Hidden Steps",
+      evaluation.show_hidden_steps,
+      Evaluation(ShowHiddenSteps),
+    ),
     toggle(
       "?",
       "Show Docs Sidebar",

src/haz3lweb/view/StepperView.re

@@ -66,6 +66,12 @@ let settings_modal = (~inject, settings: CoreSettings.Evaluation.t) => {
         settings.show_stepper_filters,
         Evaluation(ShowFilters),
       ),
+      setting(
+        "🤫",
+        "show hidden steps",
+        settings.show_hidden_steps,
+        Evaluation(ShowHiddenSteps),
+      ),
     ]),
     div(
       ~attr=
@@ -101,27 +107,6 @@ let stepper_view =
     } else {
       ([], []);
     };
-  let dh_code_current = d =>
-    div(
-      ~attr=Attr.classes(["result"]),
-      [
-        DHCode.view(
-          ~inject,
-          ~settings,
-          ~selected_hole_instance=None,
-          ~font_metrics,
-          ~width=80,
-          ~previous_step=
-            previous
-            |> List.nth_opt(_, 0)
-            |> Option.map((x: Stepper.step_with_previous) => x.step),
-          ~next_steps=Stepper.get_next_steps(stepper),
-          ~hidden_steps=hidden,
-          ~result_key,
-          d,
-        ),
-      ],
-    );
   let dh_code_previous = (step_with_previous: Stepper.step_with_previous) =>
     div(
       ~attr=Attr.classes(["result"]),
@@ -150,39 +135,101 @@ let stepper_view =
     );
   let eval_settings =
     Widgets.button(Icons.gear, _ => inject(Set(Evaluation(ShowSettings))));
-  let current =
-    switch (stepper.current) {
-    | StepperOK(d, _) =>
+
+  let rec previous_step =
+          (~hidden=false, step: Stepper.step_with_previous): list(Node.t) => {
+    [
       div(
-        ~attr=Attr.classes(["cell-item", "cell-result"]),
+        ~attr=
+          Attr.classes(
+            ["cell-item", "cell-result"] @ (hidden ? ["hidden"] : []),
+          ),
         [
           div(~attr=Attr.class_("equiv"), [Node.text("≡")]),
-          dh_code_current(d),
-          button_back,
-          eval_settings,
-          show_history,
-          hide_stepper,
+          dh_code_previous(step),
+          div(
+            ~attr=Attr.classes(["stepper-justification"]),
+            [
+              Node.text(
+                Stepper.get_justification(step.step.knd)
+                ++ (hidden ? " (hidden)" : ""),
+              ),
+            ],
+          ),
         ],
+      ),
+    ]
+    @ (
+      (
+        settings.show_hidden_steps
+          ? List.map(
+              step =>
+                {step, previous: None, hidden: []}
+                |> previous_step(~hidden=true),
+              step.hidden,
+            )
+          : []
       )
-    // TODO[Matt]: show errors and waiting
-    | StepTimeout
-    | StepPending(_, _, _) => div([])
-    };
-
-  let previous_step = (step: Stepper.step_with_previous) => {
+      |> List.flatten
+    );
+  };
+  let dh_code_current = d =>
     div(
-      ~attr=Attr.classes(["cell-item", "cell-result"]),
+      ~attr=Attr.classes(["result"]),
       [
-        div(~attr=Attr.class_("equiv"), [Node.text("≡")]),
-        dh_code_previous(step),
-        div(
-          ~attr=Attr.classes(["stepper-justification"]),
-          [Node.text(Stepper.get_justification(step.step.knd))],
+        DHCode.view(
+          ~inject,
+          ~settings,
+          ~selected_hole_instance=None,
+          ~font_metrics,
+          ~width=80,
+          ~previous_step=
+            previous
+            |> List.nth_opt(_, 0)
+            |> Option.map((x: Stepper.step_with_previous) => x.step),
+          ~next_steps=Stepper.get_next_steps(stepper),
+          ~hidden_steps=hidden,
+          ~result_key,
+          d,
         ),
       ],
     );
-  };
-  let nodes_previous = List.map(previous_step, previous);
-  List.fold_left((x, y) => List.cons(y, x), [current], nodes_previous)
+
+  let current =
+    (
+      (
+        settings.show_hidden_steps
+          ? List.map(
+              step =>
+                {step, previous: None, hidden: []}
+                |> previous_step(~hidden=true),
+              hidden,
+            )
+          : []
+      )
+      |> List.flatten
+      |> List.rev
+    )
+    @ [
+      switch (stepper.current) {
+      | StepperOK(d, _) =>
+        div(
+          ~attr=Attr.classes(["cell-item", "cell-result"]),
+          [
+            div(~attr=Attr.class_("equiv"), [Node.text("≡")]),
+            dh_code_current(d),
+            button_back,
+            eval_settings,
+            show_history,
+            hide_stepper,
+          ],
+        )
+      // TODO[Matt]: show errors and waiting
+      | StepTimeout
+      | StepPending(_, _, _) => div([])
+      },
+    ];
+  let nodes_previous = List.map(previous_step, previous) |> List.flatten;
+  List.fold_left((x, y) => List.cons(y, x), current, nodes_previous)
   @ (settings.show_settings ? settings_modal(~inject, settings) : []);
 };

src/haz3lweb/www/style.css

@@ -1799,6 +1799,10 @@ svg.expandable path {
   padding: 0.1em 0.4em 0.1em 0.4em;
 }
 
+.cell-result.hidden {
+  background-color: #E8DCBF;
+}
+
 .cell-result .toggle-switch {
   mix-blend-mode: luminosity;
 }