From db59852c9b198ca9cf576e326bb5bed0faf0ee60 Mon Sep 17 00:00:00 2001 From: Matt Keenan <31668468+Negabinary@users.noreply.github.com> Date: Fri, 30 Jan 2026 16:34:16 -0500 Subject: [PATCH 1/7] Write out steps --- src/web/app/editors/stepper/MissingStep.re | 449 +++++++++++++----- src/web/app/editors/stepper/RewriteChecker.re | 32 ++ 2 files changed, 363 insertions(+), 118 deletions(-) diff --git a/src/web/app/editors/stepper/MissingStep.re b/src/web/app/editors/stepper/MissingStep.re index a88b7ac3f0..a86375056f 100644 --- a/src/web/app/editors/stepper/MissingStep.re +++ b/src/web/app/editors/stepper/MissingStep.re @@ -13,6 +13,11 @@ module Model = { cached_exp: Calc.saved(Exp.t), cached_result: option(bool), }) + | WrittenStepOpen({ + editor: CodeEditable.Model.t, + cached_exp: Calc.saved(Exp.t), + cached_result: option(bool), + }) | NoneOpen; [@deriving (show({with_path: false}), sexp, yojson)] @@ -61,8 +66,11 @@ module Update = { type t = | ToggleAxioms | ProposeRewrite + | ProposeWrittenStep | UpdateResult(bool) + | UpdateWrittenStepResult(bool) | RewriteEditorAction(CodeEditable.Update.t) + | WriteStepEditorAction(CodeEditable.Update.t) | AxiomBoxAction(AxiomsBox.Update.t); let update = (~settings, action, model: Model.t): Updated.t(Model.t) => { @@ -72,6 +80,7 @@ module Update = { switch (model.open_box) { | NoneOpen | RewritesOpen(_) => Model.AxiomsOpen(AxiomsBox.Model.init) + | WrittenStepOpen(_) => Model.AxiomsOpen(AxiomsBox.Model.init) | AxiomsOpen(_) => Model.NoneOpen }; Model.{ @@ -83,7 +92,8 @@ module Update = { let open_box = switch (model.open_box) { | NoneOpen - | AxiomsOpen(_) => + | AxiomsOpen(_) + | WrittenStepOpen(_) => Model.RewritesOpen({ editor: CodeEditable.Model.mk(Editor.Model.mk(Zipper.init())), cached_exp: Calc.Pending, @@ -96,6 +106,24 @@ module Update = { open_box, } |> Updated.return_quiet(~recalculate=true, ~logged=true); + | (ProposeWrittenStep, _) => + let open_box = + switch (model.open_box) { + | NoneOpen + | AxiomsOpen(_) + | RewritesOpen(_) => + Model.WrittenStepOpen({ + editor: CodeEditable.Model.mk(Editor.Model.mk(Zipper.init())), + cached_exp: Calc.Pending, + cached_result: None, + }) + | WrittenStepOpen(_) => Model.NoneOpen + }; + Model.{ + ...model, + open_box, + } + |> Updated.return_quiet(~recalculate=true, ~logged=true); | (RewriteEditorAction(action), RewritesOpen({editor, _} as r)) => let* new_editor = CodeEditable.Update.update(~settings, action, editor); Model.{ @@ -106,7 +134,18 @@ module Update = { editor: new_editor, }), }; - | (RewriteEditorAction(_), _) => model |> Updated.raise_invalid_action + | (RewriteEditorAction(_), _) => model |> Updated.return_quiet + | (WriteStepEditorAction(action), WrittenStepOpen({editor, _} as r)) => + let* new_editor = CodeEditable.Update.update(~settings, action, editor); + Model.{ + ...model, + open_box: + Model.WrittenStepOpen({ + ...r, + editor: new_editor, + }), + }; + | (WriteStepEditorAction(_), _) => model |> Updated.return_quiet | (UpdateResult(result), RewritesOpen(r)) => Model.{ ...model, @@ -117,7 +156,18 @@ module Update = { }), } |> Updated.return_quiet(~logged=true) - | (UpdateResult(_), _) => model |> Updated.raise_invalid_action + | (UpdateResult(_), _) => model |> Updated.return_quiet + | (UpdateWrittenStepResult(result), WrittenStepOpen(r)) => + Model.{ + ...model, + open_box: + Model.WrittenStepOpen({ + ...r, + cached_result: Some(result), + }), + } + |> Updated.return_quiet + | (UpdateWrittenStepResult(_), _) => model |> Updated.return_quiet | (AxiomBoxAction(action), AxiomsOpen(m)) => let* updated = AxiomsBox.Update.update(~settings, action, m); Model.{ @@ -132,8 +182,11 @@ module Update = { switch (action) { | ToggleAxioms | ProposeRewrite + | ProposeWrittenStep | UpdateResult(_) + | UpdateWrittenStepResult(_) | RewriteEditorAction(_) + | WriteStepEditorAction(_) | AxiomBoxAction(_) => false }; }; @@ -267,6 +320,37 @@ module Update = { cached_exp: cached_exp |> Calc.save, cached_result: cached_result |> Calc.get_value, }); + | WrittenStepOpen({editor, cached_exp, cached_result}) => + // Calculate syntax, holes, types, etc for the editor + let editor = + CodeEditable.Update.calculate( + ~settings, + ~is_edited=true, + ~is_dynamic_term=true, + ~dynamics=Dynamics.Map.empty, + ~stitch=x => x, + ~ctx=Calc.get_value(ctx) |> SemanticCtx.get_ctx, + editor, + ); + // Extract an exp from the editor + let cached_exp = + Calc.set( + ~eq=Exp.fast_equal, + CodeEditable.Model.get_statics(editor).elaborated, + cached_exp, + ); + // Reset result if editor changes + let cached_result = + Calc.Calculated(cached_result) + |> { + let.calc _ = cached_exp; + None; + }; + Model.WrittenStepOpen({ + editor, + cached_exp: cached_exp |> Calc.save, + cached_result: cached_result |> Calc.get_value, + }); | AxiomsOpen(m) => AxiomsOpen( AxiomsBox.Update.calculate(~info_map, ~ctx, ~selected_exp, m), @@ -299,6 +383,7 @@ module Selection = { [@deriving (show({with_path: false}), sexp, yojson)] type t = | RewriteEditor(CodeEditable.Selection.t) + | WriteStepEditor(CodeEditable.Selection.t) | AxiomBoxSelection(AxiomsBox.Selection.t); let get_cursor_info = (~selection: t, model: Model.t): cursor(Update.t) => { @@ -307,6 +392,10 @@ module Selection = { let+ ci = CodeEditable.Selection.get_cursor_info(~selection, editor); Update.RewriteEditorAction(ci); | (RewriteEditor(_), _) => empty + | (WriteStepEditor(selection), WrittenStepOpen({editor, _})) => + let+ ci = CodeEditable.Selection.get_cursor_info(~selection, editor); + Update.WriteStepEditorAction(ci); + | (WriteStepEditor(_), _) => empty | (AxiomBoxSelection(selection), AxiomsOpen(m)) => let+ ci = AxiomsBox.Selection.get_cursor_info(~selection, m); Update.AxiomBoxAction(ci); @@ -320,6 +409,10 @@ module Selection = { CodeEditable.Selection.handle_key_event(~selection, editor, event) |> Option.map(x => Update.RewriteEditorAction(x)) | (RewriteEditor(_), _) => None + | (WriteStepEditor(selection), WrittenStepOpen({editor, _})) => + CodeEditable.Selection.handle_key_event(~selection, editor, event) + |> Option.map(x => Update.WriteStepEditorAction(x)) + | (WriteStepEditor(_), _) => None | (AxiomBoxSelection(selection), AxiomsOpen(m)) => AxiomsBox.Selection.handle_key_event(~selection, m, event) |> Option.map(x => Update.AxiomBoxAction(x)) @@ -452,6 +545,234 @@ module View = { && Exp.is_fun(Calc.get_saved_exc(model.full_exp)); }; + let view_rewrites_box = (editor, cached_exp, cached_result) => { + let unboxed_cached_exp = + Calc.get_saved_exc(~print="cached exp not calculated", cached_exp); + let unboxed_selected_exp = + Option.value( + ~default=EmptyHole |> Exp.fresh, + Calc.get_saved_exc( + ~print="selected exp not calculated", + model.selected_exp, + ), + ); + [ + // one element list with a div + // with a list containing two elements + // an Editor for user to propose their rewrite + // a button to submit the rewrite + div_c( + "rewrite-box", + [ + Node.text("Replace: "), + CodeViewable.view_any( + ~globals, + ~settings= + ExpToSegment.Settings.of_core( + ~inline=false, + ~fold_fn_bodies=`Text, + globals.settings.core, + ), + Exp(unboxed_selected_exp), + ), + Node.text("With: "), + div_c( + "inline-editor-wrapper", + [ + CodeEditable.View.view( + ~globals, + ~signal= + fun + | MakeActive => signal(MakeActive(RewriteEditor())), + ~inject=x => inject(RewriteEditorAction(x)), + ~selected= + switch (selected) { + | Some(RewriteEditor ()) => true + | _ => false + }, + ~dynamics=Dynamics.Map.empty, + editor, + ), + ], + ), + ] + @ { + switch (cached_result) { + | Some(true) => [ + Node.text("Valid"), + Widgets.button( + ~clss=["proof-button"], + Node.text("Replace"), + ~tooltip="replace", + _ => + signal( + AddAlgebriteStep( + ProofHacks.exp_idx( + unboxed_selected_exp, + model.full_exp + |> Calc.get_saved_exc(~print="full_exp"), + ), + unboxed_selected_exp, + unboxed_cached_exp + |> Substitution.in_exp( + model.cached_env + |> Calc.get_saved_exc(~print="env not cached"), + ), + ), + ) + ), + ] + | Some(false) => [Node.text("Invalid")] + | None => [ + Widgets.button( + ~clss=["proof-button"], + Node.text("Check"), + _ => + inject( + UpdateResult( + RewriteChecker.check_rewrite( + unboxed_selected_exp + |> Substitution.in_exp( + model.cached_env + |> Calc.get_saved_exc( + ~print="env not cached", + ), + ), + unboxed_cached_exp + |> Substitution.in_exp( + model.cached_env + |> Calc.get_saved_exc( + ~print="env not cached", + ), + ), + ), + ), + ), + ~tooltip="check", + ), + ] + }; + }, + ), + ]; + }; + + let view_written_step_box = (editor, cached_exp, cached_result) => { + let unboxed_cached_exp = + Calc.get_saved_exc(~print="cached exp not calculated", cached_exp); + let unboxed_selected_exp = + Option.value( + ~default=EmptyHole |> Exp.fresh, + Calc.get_saved_exc( + ~print="selected exp not calculated", + model.selected_exp, + ), + ); + [ + // one element list with a div + // with a list containing two elements + // an Editor for user to propose their rewrite + // a button to submit the rewrite + div_c( + "rewrite-box", + [ + Node.text("Replace: "), + CodeViewable.view_any( + ~globals, + ~settings= + ExpToSegment.Settings.of_core( + ~inline=false, + ~fold_fn_bodies=`Text, + globals.settings.core, + ), + Exp(unboxed_selected_exp), + ), + Node.text("With: "), + div_c( + "inline-editor-wrapper", + [ + CodeEditable.View.view( + ~globals, + ~signal= + fun + | MakeActive => signal(MakeActive(WriteStepEditor())), + ~inject=x => inject(WriteStepEditorAction(x)), + ~selected= + switch (selected) { + | Some(WriteStepEditor ()) => true + | _ => false + }, + ~dynamics=Dynamics.Map.empty, + editor, + ), + ], + ), + ] + @ { + switch (cached_result) { + | Some(true) => [ + Node.text("Valid"), + Widgets.button( + ~clss=["proof-button"], + Node.text("Replace"), + ~tooltip="replace", + _ => + signal( + AddAlgebriteStep( + ProofHacks.exp_idx( + unboxed_selected_exp, + model.full_exp + |> Calc.get_saved_exc(~print="full_exp"), + ), + unboxed_selected_exp, + unboxed_cached_exp + |> Substitution.in_exp( + model.cached_env + |> Calc.get_saved_exc(~print="env not cached"), + ), + ), + ) + ), + ] + | Some(false) => [Node.text("Invalid")] + | None => [ + Widgets.button( + ~clss=["proof-button"], + Node.text("Check"), + _ => + inject( + UpdateWrittenStepResult( + RewriteChecker.check_written_step( + ~settings=globals.settings.core, + ~env= + model.cached_env + |> Calc.get_saved_exc(~print="env not cached"), + unboxed_selected_exp + |> Substitution.in_exp( + model.cached_env + |> Calc.get_saved_exc( + ~print="env not cached", + ), + ), + unboxed_cached_exp + |> Substitution.in_exp( + model.cached_env + |> Calc.get_saved_exc( + ~print="env not cached", + ), + ), + ), + ), + ), + ~tooltip="check", + ), + ] + }; + }, + ), + ]; + }; + // I want to make a bunch of buttons here: // Evaluate [TODO], Rewrite, Axioms, Cases, let buttons = @@ -503,6 +824,10 @@ module View = { ) @ [ proof_button(~callback=inject(ProposeRewrite), "Algebra ▼"), + proof_button( + ~callback=inject(ProposeWrittenStep), + "Write Step ▼", + ), proof_button(~callback=inject(ToggleAxioms), "Assumptions ▼"), proof_button( ~callback= @@ -576,121 +901,9 @@ module View = { ), ] | RewritesOpen({editor, cached_exp, cached_result}) => - let unboxed_cached_exp = - Calc.get_saved_exc( - ~print="cached exp not calculated", - cached_exp, - ); - let unboxed_selected_exp = - Option.value( - ~default=EmptyHole |> Exp.fresh, - Calc.get_saved_exc( - ~print="selected exp not calculated", - model.selected_exp, - ), - ); - [ - // one element list with a div - // with a list containing two elements - // an Editor for user to propose their rewrite - // a button to submit the rewrite - div_c( - "rewrite-box", - [ - Node.text("Replace: "), - CodeViewable.view_any( - ~globals, - ~settings= - ExpToSegment.Settings.of_core( - ~inline=false, - ~fold_fn_bodies=`Text, - globals.settings.core, - ), - Exp(unboxed_selected_exp), - ), - Node.text("With: "), - div_c( - "inline-editor-wrapper", - [ - CodeEditable.View.view( - ~globals, - ~signal= - fun - | MakeActive => - signal(MakeActive(RewriteEditor())), - ~inject=x => inject(RewriteEditorAction(x)), - ~selected= - switch (selected) { - | Some(RewriteEditor ()) => true - | _ => false - }, - ~dynamics=Dynamics.Map.empty, - editor, - ), - ], - ), - ] - @ { - switch (cached_result) { - | Some(true) => [ - Node.text("Valid"), - Widgets.button( - ~clss=["proof-button"], - Node.text("Replace"), - ~tooltip="replace", - _ => - signal( - AddAlgebriteStep( - ProofHacks.exp_idx( - unboxed_selected_exp, - model.full_exp - |> Calc.get_saved_exc(~print="full_exp"), - ), - unboxed_selected_exp, - unboxed_cached_exp - |> Substitution.in_exp( - model.cached_env - |> Calc.get_saved_exc( - ~print="env not cached", - ), - ), - ), - ) - ), - ] - | Some(false) => [Node.text("Invalid")] - | None => [ - Widgets.button( - ~clss=["proof-button"], - Node.text("Check"), - _ => - inject( - UpdateResult( - RewriteChecker.check_rewrite( - unboxed_selected_exp - |> Substitution.in_exp( - model.cached_env - |> Calc.get_saved_exc( - ~print="env not cached", - ), - ), - unboxed_cached_exp - |> Substitution.in_exp( - model.cached_env - |> Calc.get_saved_exc( - ~print="env not cached", - ), - ), - ), - ), - ), - ~tooltip="check", - ), - ] - }; - }, - ), - ]; + view_rewrites_box(editor, cached_exp, cached_result) + | WrittenStepOpen({editor, cached_exp, cached_result}) => + view_written_step_box(editor, cached_exp, cached_result) }; }, ), diff --git a/src/web/app/editors/stepper/RewriteChecker.re b/src/web/app/editors/stepper/RewriteChecker.re index 04cdf881c8..5bfacf71c9 100644 --- a/src/web/app/editors/stepper/RewriteChecker.re +++ b/src/web/app/editors/stepper/RewriteChecker.re @@ -85,3 +85,35 @@ let check_rewrite = (from_: Exp.t, to_: Exp.t): bool => { checkEquality(left_str, right_str); }; }; + +let check_written_step = (~settings, ~env, from_: Exp.t, to_: Exp.t): bool => { + // checking using evaluation steps + let rec get_next_exps = (exp: Exp.t): list(Exp.t) => { + switch (EvaluatorStep.get_status(~settings, exp, env)) { + | EvaluatorStep.AutoStep(step) => + switch (EvaluatorStep.take_step(step)) { + | Some(next_exp) => get_next_exps(next_exp) @ [next_exp] + | None => [] + } + | AvailableSteps(steps) => + List.filter_map(EvaluatorStep.take_step, steps) + }; + }; + let next_exps = get_next_exps(from_); + List.exists( + e => + Equality.equality( + Equality.{ + ...Equality.semantic_settings, + env1: Some(env), + env2: Some(env), + ignore_ascriptions: true, + }, + ). + exp( + e, + to_, + ), + next_exps, + ); +}; From 677e6469876436975215826bf4be7f7c66126177 Mon Sep 17 00:00:00 2001 From: Matt Keenan <31668468+Negabinary@users.noreply.github.com> Date: Thu, 5 Feb 2026 09:56:20 -0500 Subject: [PATCH 2/7] add step justification --- src/web/app/editors/stepper/MissingStep.re | 12 +- src/web/app/editors/stepper/RewriteChecker.re | 37 ++++- src/web/app/editors/stepper/StepperBase.re | 90 +++++++++- src/web/app/editors/stepper/WrittenStep.re | 155 ++++++++++++++++++ 4 files changed, 277 insertions(+), 17 deletions(-) create mode 100644 src/web/app/editors/stepper/WrittenStep.re diff --git a/src/web/app/editors/stepper/MissingStep.re b/src/web/app/editors/stepper/MissingStep.re index a86375056f..52ad0ca605 100644 --- a/src/web/app/editors/stepper/MissingStep.re +++ b/src/web/app/editors/stepper/MissingStep.re @@ -16,7 +16,7 @@ module Model = { | WrittenStepOpen({ editor: CodeEditable.Model.t, cached_exp: Calc.saved(Exp.t), - cached_result: option(bool), + cached_result: option(option(string)), }) | NoneOpen; @@ -68,7 +68,7 @@ module Update = { | ProposeRewrite | ProposeWrittenStep | UpdateResult(bool) - | UpdateWrittenStepResult(bool) + | UpdateWrittenStepResult(option(string)) | RewriteEditorAction(CodeEditable.Update.t) | WriteStepEditorAction(CodeEditable.Update.t) | AxiomBoxAction(AxiomsBox.Update.t); @@ -429,6 +429,7 @@ module View = { | HideStepper | AddAxiomStep(string, int, Exp.t, Direction.t, string) | AddAlgebriteStep(int, Exp.t, Exp.t) + | AddWrittenStep(string, int, Exp.t, Exp.t) | MakeActive(Selection.t) | TakeStep(int) | Refl(int); @@ -710,7 +711,7 @@ module View = { ] @ { switch (cached_result) { - | Some(true) => [ + | Some(Some(j)) => [ Node.text("Valid"), Widgets.button( ~clss=["proof-button"], @@ -718,7 +719,8 @@ module View = { ~tooltip="replace", _ => signal( - AddAlgebriteStep( + AddWrittenStep( + j, ProofHacks.exp_idx( unboxed_selected_exp, model.full_exp @@ -734,7 +736,7 @@ module View = { ) ), ] - | Some(false) => [Node.text("Invalid")] + | Some(None) => [Node.text("Invalid")] | None => [ Widgets.button( ~clss=["proof-button"], diff --git a/src/web/app/editors/stepper/RewriteChecker.re b/src/web/app/editors/stepper/RewriteChecker.re index 5bfacf71c9..14284af1de 100644 --- a/src/web/app/editors/stepper/RewriteChecker.re +++ b/src/web/app/editors/stepper/RewriteChecker.re @@ -86,22 +86,42 @@ let check_rewrite = (from_: Exp.t, to_: Exp.t): bool => { }; }; -let check_written_step = (~settings, ~env, from_: Exp.t, to_: Exp.t): bool => { +let check_written_step = + (~settings, ~env, from_: Exp.t, to_: Exp.t): option(string) => { + let rec take_auto_steps = (exp: Exp.t): Exp.t => { + switch (EvaluatorStep.get_status(~settings, exp, env)) { + | EvaluatorStep.AutoStep(step) => + switch (EvaluatorStep.take_step(step)) { + | Some(next_exp) => take_auto_steps(next_exp) + | None => exp + } + | AvailableSteps(_) => exp + }; + }; + let take_and_justify = (es: EvaluatorStep.step): option((string, Exp.t)) => { + switch (EvaluatorStep.take_step(es)) { + | Some(next_exp) => + let kind = EvaluatorStep.get_step_kind(es); + let justification = Transition.stepper_justification(kind); + let final_exp = take_auto_steps(next_exp); + Some((justification, final_exp)); + | None => None + }; + }; // checking using evaluation steps - let rec get_next_exps = (exp: Exp.t): list(Exp.t) => { + let rec get_next_exps = (exp: Exp.t): list((string, Exp.t)) => { switch (EvaluatorStep.get_status(~settings, exp, env)) { | EvaluatorStep.AutoStep(step) => switch (EvaluatorStep.take_step(step)) { - | Some(next_exp) => get_next_exps(next_exp) @ [next_exp] + | Some(next_exp) => get_next_exps(next_exp) | None => [] } - | AvailableSteps(steps) => - List.filter_map(EvaluatorStep.take_step, steps) + | AvailableSteps(steps) => List.filter_map(take_and_justify, steps) }; }; let next_exps = get_next_exps(from_); - List.exists( - e => + List.find_opt( + ((_, e)) => Equality.equality( Equality.{ ...Equality.semantic_settings, @@ -115,5 +135,6 @@ let check_written_step = (~settings, ~env, from_: Exp.t, to_: Exp.t): bool => { to_, ), next_exps, - ); + ) + |> Option.map(fst); }; diff --git a/src/web/app/editors/stepper/StepperBase.re b/src/web/app/editors/stepper/StepperBase.re index 52fe31fa13..f166801f93 100644 --- a/src/web/app/editors/stepper/StepperBase.re +++ b/src/web/app/editors/stepper/StepperBase.re @@ -16,6 +16,7 @@ type step_kind_model = | MissingStep(MissingStep.Model.t) | AxiomStep(AxiomStep.model'(step_model)) | AlgebriteStep(AlgebriteStep.model'(step_model)) + | WrittenStep(WrittenStep.model'(step_model)) and step_model = { // Calculated @@ -48,6 +49,7 @@ type persistent_step_kind = | MissingStep(MissingStep.Model.persistent) | AxiomStep(AxiomStep.persistent'(persistent_step)) | AlgebriteStep(AlgebriteStep.persistent'(persistent_step)) + | WrittenStep(WrittenStep.persistent'(persistent_step)) and persistent_step = { step_kind: persistent_step_kind, @@ -62,6 +64,7 @@ type step_kind_action = | MissingStep(MissingStep.Update.t) | AxiomStep(AxiomStep.action'(step_action)) | AlgebriteStep(AlgebriteStep.action'(step_action)) + | WrittenStep(WrittenStep.action'(step_action)) and step_action = | StepKindAction(step_kind_action) @@ -72,7 +75,8 @@ and step_action = | AddInduction(option(Exp.t)) | AddForall | AddAxiomStep(string, int, Exp.t, Direction.t, string) - | AddAlgebriteStep(int, Exp.t, Exp.t); + | AddAlgebriteStep(int, Exp.t, Exp.t) + | AddWrittenStep(string, int, Exp.t, Exp.t); [@deriving (show({with_path: false}), sexp, yojson)] type step_kind_focus = @@ -82,6 +86,7 @@ type step_kind_focus = | MissingStep(MissingStep.Selection.t) | AxiomStep(AxiomStep.focus'(step_focus)) | AlgebriteStep(AlgebriteStep.focus'(step_focus)) + | WrittenStep(WrittenStep.focus'(step_focus)) and step_focus = | StepKindFocus(step_kind_focus) @@ -107,6 +112,7 @@ module rec StepKind: { module MissingStep = MissingStep; // This could be functorized too. module AxiomStep = AxiomStep.F(Stepper); module AlgebriteStep = AlgebriteStep.F(Stepper); + module WrittenStep = WrittenStep.F(Stepper); [@deriving (show({with_path: false}), sexp, yojson)] type model = step_kind_model; @@ -125,6 +131,7 @@ module rec StepKind: { | MissingStep(m) => MissingStep(MissingStep.Model.persist(m)) | AxiomStep(m) => AxiomStep(AxiomStep.persist(m)) | AlgebriteStep(m) => AlgebriteStep(AlgebriteStep.persist(m)) + | WrittenStep(m) => WrittenStep(WrittenStep.persist(m)) }; }; @@ -136,6 +143,7 @@ module rec StepKind: { | MissingStep(m) => MissingStep(MissingStep.Model.unpersist(m)) | AxiomStep(m) => AxiomStep(AxiomStep.unpersist(m)) | AlgebriteStep(m) => AlgebriteStep(AlgebriteStep.unpersist(m)) + | WrittenStep(m) => WrittenStep(WrittenStep.unpersist(m)) }; }; @@ -167,10 +175,14 @@ module rec StepKind: { | (AlgebriteStep(a), AlgebriteStep(m)) => let* s = AlgebriteStep.update(~settings, a, m); (AlgebriteStep(s): model); + | (WrittenStep(a), WrittenStep(m)) => + let* s = WrittenStep.update(~settings, a, m); + (WrittenStep(s): model); | ( SingleStep(_) | InductionStep(_) | ForallStep(_) | MissingStep(_) | AxiomStep(_) | - AlgebriteStep(_), + AlgebriteStep(_) | + WrittenStep(_), _, ) => model |> Updated.raise_invalid_action @@ -186,6 +198,7 @@ module rec StepKind: { | MissingStep(action) => MissingStep.Update.can_undo(action) | AxiomStep(action) => AxiomStep.can_undo(action) | AlgebriteStep(action) => AlgebriteStep.can_undo(action) + | WrittenStep(action) => WrittenStep.can_undo(action) }; }; @@ -331,6 +344,19 @@ module rec StepKind: { m, ); (AlgebriteStep(m): model, h, e, v); + | WrittenStep(m) => + let+ (m, h, e, v) = + WrittenStep.calculate( + ~settings, + ~hidden, + ~exp, + ~ctx, + ~editor, + ~info_map, + ~ana, + m, + ); + (WrittenStep(m): model, h, e, v); }; let get_cursor_info = (~focus: focus, model: model) => @@ -355,10 +381,14 @@ module rec StepKind: { | (AlgebriteStep(focus), AlgebriteStep(model)) => let+ focus_info = AlgebriteStep.get_cursor_info(~focus, model); (AlgebriteStep(focus_info): action); + | (WrittenStep(focus), WrittenStep(model)) => + let+ focus_info = WrittenStep.get_cursor_info(~focus, model); + (WrittenStep(focus_info): action); | ( SingleStep(_) | InductionStep(_) | ForallStep(_) | MissingStep(_) | AxiomStep(_) | - AlgebriteStep(_), + AlgebriteStep(_) | + WrittenStep(_), _, ) => Cursor.empty } @@ -385,10 +415,14 @@ module rec StepKind: { | (AlgebriteStep(focus), AlgebriteStep(model)) => AlgebriteStep.handle_key_event(~focus, ~event, model) |> Option.map((x): action => AlgebriteStep(x)) + | (WrittenStep(focus), WrittenStep(model)) => + WrittenStep.handle_key_event(~focus, ~event, model) + |> Option.map((x): action => WrittenStep(x)) | ( SingleStep(_) | InductionStep(_) | ForallStep(_) | MissingStep(_) | AxiomStep(_) | - AlgebriteStep(_), + AlgebriteStep(_) | + WrittenStep(_), _, ) => None @@ -466,6 +500,17 @@ module rec StepKind: { ~take_focus=x => take_focus(AlgebriteStep(x)), m, ) + | WrittenStep(m) => + WrittenStep.view_content( + ~focus= + switch (focus) { + | Some(WrittenStep(f)) => Some(f) + | _ => None + }, + ~inject=x => inject(WrittenStep(x)), + ~take_focus=x => take_focus(WrittenStep(x)), + m, + ) }; f(~globals, ~hide_stepper, ~undo, ~is_toplevel); }; @@ -569,6 +614,22 @@ module rec StepKind: { ~is_toplevel, m, ) + | WrittenStep(m) => + WrittenStep.view_justification( + ~globals, + ~focus= + switch (focus) { + | Some(WrittenStep(f)) => Some(f) + | Some(_) + | None => None + }, + ~inject=x => inject(WrittenStep(x)), + ~take_focus=x => take_focus(WrittenStep(x)), + ~hide_stepper, + ~undo, + ~is_toplevel, + m, + ) }; } @@ -724,6 +785,24 @@ and Stepper: { } |> return | (AddAlgebriteStep(_, _, _), _, _) => model |> raise_invalid_action + | ( + AddWrittenStep(justification, at_idx, at_exp, with_exp), + MissingStep(_), + _, + ) => + { + ...model, + step_kind: + WrittenStep({ + at_idx, + at_exp, + with_exp, + justification, + next_exp: Calc.Pending, + }), + } + |> return + | (AddWrittenStep(_, _, _, _), _, _) => model |> raise_invalid_action | (StepKindAction(sk_action), _, _) => let* new_step_kind = StepKind.update(~settings, sk_action, model.step_kind); @@ -745,6 +824,7 @@ and Stepper: { | AddForall => true | AddAxiomStep(_) => true | AddAlgebriteStep(_) => true + | AddWrittenStep(_) => true | StepKindAction(action) => StepKind.can_undo(action) }; }; @@ -1022,6 +1102,8 @@ and Stepper: { inject(AddAxiomStep(name, idx, e1, dir, eq)) | AddAlgebriteStep(idx, e1, e2) => inject(AddAlgebriteStep(idx, e1, e2)) + | AddWrittenStep(just, idx, e1, e2) => + inject(AddWrittenStep(just, idx, e1, e2)) | TakeStep(i) => inject(StepForward(i)) | Refl(i) => { let refl_exps = diff --git a/src/web/app/editors/stepper/WrittenStep.re b/src/web/app/editors/stepper/WrittenStep.re new file mode 100644 index 0000000000..332d67c5d9 --- /dev/null +++ b/src/web/app/editors/stepper/WrittenStep.re @@ -0,0 +1,155 @@ +open Util; +open Language; +open StepInterface; +open OptUtil.Syntax; +open Calc.Syntax; + +/* Types are defined outside the functor to make it + easier to use them in other files. */ + +[@deriving (show({with_path: false}), sexp, yojson)] +type model'('stepper) = { + at_idx: int, + at_exp: Exp.t, + with_exp: Exp.t, + justification: string, + next_exp: Calc.saved(Exp.t), +}; + +[@deriving (show({with_path: false}), sexp, yojson)] +type persistent'('stepper) = { + at_idx: int, + at_exp: Exp.t, + with_exp: Exp.t, + justification: string, +}; + +[@deriving (show({with_path: false}), sexp, yojson)] +type action'('step) = + |; + +[@deriving (show({with_path: false}), sexp, yojson)] +type focus'('step) = + |; + +/* The methods in this file, like the other step files, are + parameterized by a Stepper module that implements the + stepper interface. This allows us to use steppers inside + steps inside steppers. The lines below can be copied as + boilerplate to other steps.*/ +module F = + (Stepper: STEPPER) + + : ( + STEP with + type model = model'(Stepper.model) and + type persistent = persistent'(Stepper.persistent) and + type action = action'(Stepper.action) and + type focus = focus'(Stepper.focus) + ) => { + [@deriving (show({with_path: false}), sexp, yojson)] + type model = model'(Stepper.model); + [@deriving (show({with_path: false}), sexp, yojson)] + type persistent = persistent'(Stepper.persistent); + [@deriving (show({with_path: false}), sexp, yojson)] + type action = action'(Stepper.action); + [@deriving (show({with_path: false}), sexp, yojson)] + type focus = focus'(Stepper.focus); + + let persist = (model: model): persistent => { + { + at_idx: model.at_idx, + at_exp: model.at_exp, + with_exp: model.with_exp, + justification: model.justification, + }; + }; + + let unpersist = (p: persistent): model => { + { + at_idx: p.at_idx, + at_exp: p.at_exp, + with_exp: p.with_exp, + justification: p.justification, + next_exp: Calc.Pending, + }; + }; + + let update = (~settings as _: Settings.t, action: action, _model: model) => + switch (action) { + | _ => . + }; + + let can_undo = _ => false; + + let calculate = + ( + ~settings as _: Calc.t(CoreSettings.t), + ~hidden: Calc.saved(bool), + ~exp: Calc.t(Exp.t), + ~ctx as _: Calc.t(SemanticCtx.t), + ~editor as _: Calc.t(CodeSelectable.Model.t), + ~info_map as _, + ~ana as _, + model: model, + ) => { + let {at_idx, at_exp, with_exp, next_exp, justification} = model; + let+ next_exp = + next_exp + |> Calc.map_saved(Option.some) + |> { + let.calc exp = exp; + let* e = ProofHacks.nth_exp(at_exp, at_idx, exp); + Some(ProofHacks.replace_exp_id(e |> DHExp.rep_id, exp, with_exp)); + } + |> Calc.to_option; + ( + { + at_idx, + at_exp, + with_exp, + next_exp: next_exp |> Calc.save, + justification, + }, + hidden |> Calc.set(false), + Some(next_exp), + Calc.OldValue(Some(true)), + ); + }; + + let get_cursor_info = (~focus: focus, _model: model) => + switch (focus) { + | _ => . + }; + + let handle_key_event = (~focus: focus, ~event as _: Key.t, _model: model) => + switch (focus) { + | _ => . + }; + + let view_justification = + ( + ~globals as _: Globals.t, + ~focus as _: option(focus), + ~inject as _: action => Ui_effect.t(unit), + ~take_focus as _: focus => Ui_effect.t(unit), + ~hide_stepper as _: Ui_effect.t(unit), + ~undo as _: option(Ui_effect.t(unit)), + ~is_toplevel as _: bool, + m: model, + ) => + WebUtil.Node.text(m.justification); + + let view_content = + ( + ~globals as _: Globals.t, + ~focus as _: option(focus), + ~inject as _: action => Ui_effect.t(unit), + ~take_focus as _: focus => Ui_effect.t(unit), + ~hide_stepper as _: Ui_effect.t(unit), + ~undo as _: option(Ui_effect.t(unit)), + ~is_toplevel as _: bool, + _model: model, + ) => + []; +}; From 99c84f85b04ca9914d6152e61e7b26f84074ae6f Mon Sep 17 00:00:00 2001 From: Matt Keenan <31668468+Negabinary@users.noreply.github.com> Date: Thu, 5 Feb 2026 10:24:42 -0500 Subject: [PATCH 3/7] Add settings to toggle write out steps --- src/language/CoreSettings.re | 2 ++ src/web/Settings.re | 6 ++++ src/web/app/editors/result/StepperEditor.re | 36 ++++++++++++--------- src/web/app/editors/stepper/MissingStep.re | 18 ++++++++--- src/web/view/NutMenu.re | 6 ++++ 5 files changed, 48 insertions(+), 20 deletions(-) diff --git a/src/language/CoreSettings.re b/src/language/CoreSettings.re index 1526fb6d1b..f0a6be3abb 100644 --- a/src/language/CoreSettings.re +++ b/src/language/CoreSettings.re @@ -16,6 +16,7 @@ module Evaluation = { show_settings: bool, show_hidden_steps: bool, enable_proof: bool, + write_out_steps: bool, }; let init = { @@ -31,6 +32,7 @@ module Evaluation = { show_settings: false, show_hidden_steps: false, enable_proof: false, + write_out_steps: false, }; }; diff --git a/src/web/Settings.re b/src/web/Settings.re index ece884c8b0..d2502bfc8c 100644 --- a/src/web/Settings.re +++ b/src/web/Settings.re @@ -38,6 +38,7 @@ module Model = { stepper_history: false, show_settings: false, show_hidden_steps: false, + write_out_steps: false, enable_proof: false, }, }, @@ -103,6 +104,7 @@ module Update = { | ShowLookups | ShowFilters | ShowSettings + | WriteOutSteps | ShowHiddenSteps; [@deriving (show({with_path: false}), sexp, yojson)] @@ -240,6 +242,10 @@ module Update = { ...evaluation, show_hidden_steps: !evaluation.show_hidden_steps, } + | WriteOutSteps => { + ...evaluation, + write_out_steps: !evaluation.write_out_steps, + } }; { ...settings, diff --git a/src/web/app/editors/result/StepperEditor.re b/src/web/app/editors/result/StepperEditor.re index aa6f551dab..3c7b8843c1 100644 --- a/src/web/app/editors/result/StepperEditor.re +++ b/src/web/app/editors/result/StepperEditor.re @@ -84,6 +84,7 @@ module View = { ~font_metrics: FontMetrics.t, ~inject: Update.t => Ui_effect.t(unit), ~selected_id: option(Id.t), + ~write_out_steps: bool, signal: event => Ui_effect.t(unit), model: Model.t, ) => { @@ -104,7 +105,6 @@ module View = { ), ) ); - let taken_steps = (taken_steps: list(Id.t)) => taken_steps |> List.filter_map(TermData.root_tile(_, syntax.term_data)) @@ -129,20 +129,25 @@ module View = { ); taken_steps(model.taken_steps) - @ next_steps(model.next_steps, ~inject=x => - { - open OptUtil.Syntax; - let+ range = - TermData.extreme_measures( - List.nth(model.next_steps, x), - model.editor.editor.syntax.term_data, - model.editor.editor.syntax.measured, - ); - Some(List.nth(model.next_steps, x)) == selected_id - ? signal(TakeStep(x)) : inject(Select(PointToPoint(range))); - } - |> Option.value(~default=Ui_effect.Ignore) - ) + @ ( + write_out_steps + ? [] + : next_steps(model.next_steps, ~inject=x => + { + open OptUtil.Syntax; + let+ range = + TermData.extreme_measures( + List.nth(model.next_steps, x), + model.editor.editor.syntax.term_data, + model.editor.editor.syntax.measured, + ); + Some(List.nth(model.next_steps, x)) == selected_id + ? signal(TakeStep(x)) + : inject(Select(PointToPoint(range))); + } + |> Option.value(~default=Ui_effect.Ignore) + ) + ) @ refl_steps(model.refls, ~inject=x => { open OptUtil.Syntax; @@ -189,6 +194,7 @@ module View = { @ deco( ~syntax=model.editor.editor.syntax, ~font_metrics=globals.font_metrics, + ~write_out_steps=globals.settings.core.evaluation.write_out_steps, ~inject, ~selected_id, signal, diff --git a/src/web/app/editors/stepper/MissingStep.re b/src/web/app/editors/stepper/MissingStep.re index 52ad0ca605..db6792186e 100644 --- a/src/web/app/editors/stepper/MissingStep.re +++ b/src/web/app/editors/stepper/MissingStep.re @@ -193,7 +193,7 @@ module Update = { let calculate = ( - ~settings, + ~settings: CoreSettings.t, exp, info_map, ctx: Calc.t(SemanticCtx.t), @@ -285,6 +285,7 @@ module Update = { s => e |> Exp.rep_id == EvaluatorStep.get_step_id(s), next_steps, ) + || settings.evaluation.write_out_steps ); }; let open_box = @@ -511,6 +512,7 @@ module View = { switch ( model.selected_exp |> Calc.get_saved_exc(~print="Selected Exp") ) { + | _ when globals.settings.core.evaluation.write_out_steps => None | Some(selected_exp) => List.find_index( x => x == (selected_exp |> Exp.rep_id), @@ -824,12 +826,18 @@ module View = { ] : [] ) + @ ( + globals.settings.core.evaluation.write_out_steps + ? [ + proof_button( + ~callback=inject(ProposeWrittenStep), + "Write Step ▼", + ), + ] + : [] + ) @ [ proof_button(~callback=inject(ProposeRewrite), "Algebra ▼"), - proof_button( - ~callback=inject(ProposeWrittenStep), - "Write Step ▼", - ), proof_button(~callback=inject(ToggleAxioms), "Assumptions ▼"), proof_button( ~callback= diff --git a/src/web/view/NutMenu.re b/src/web/view/NutMenu.re index 5777fbb6ea..ada8a343f6 100644 --- a/src/web/view/NutMenu.re +++ b/src/web/view/NutMenu.re @@ -108,6 +108,12 @@ let stepper_group = (~globals: Globals.t) => { s.enable_proof, Evaluation(EnableProof), ), + ( + "✏️", + "Write out steps", + s.write_out_steps, + Evaluation(WriteOutSteps), + ), ], ); }; From e9e5496e0dac8daa282813ce40bcf62d869ad786 Mon Sep 17 00:00:00 2001 From: Matt Keenan <31668468+Negabinary@users.noreply.github.com> Date: Thu, 5 Feb 2026 17:37:13 -0500 Subject: [PATCH 4/7] Fix drag propagation issue --- src/web/app/editors/stepper/MissingStep.re | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/web/app/editors/stepper/MissingStep.re b/src/web/app/editors/stepper/MissingStep.re index db6792186e..51a106aa9a 100644 --- a/src/web/app/editors/stepper/MissingStep.re +++ b/src/web/app/editors/stepper/MissingStep.re @@ -497,6 +497,8 @@ module View = { ~attrs=[ Attr.classes(["proof-button"]), Attr.on_pointerdown(_ => Virtual_dom.Vdom.Effect.Stop_propagation), + Attr.on_pointerup(_ => Virtual_dom.Vdom.Effect.Stop_propagation), + Attr.on_mousemove(_ => Virtual_dom.Vdom.Effect.Stop_propagation), Attr.on_click(_ => Ui_effect.Many([ callback, @@ -876,6 +878,12 @@ module View = { Attr.on_pointerdown(_ => Virtual_dom.Vdom.Effect.Stop_propagation ), + Attr.on_pointerup(_ => + Virtual_dom.Vdom.Effect.Stop_propagation + ), + Attr.on_mousemove(_ => + Virtual_dom.Vdom.Effect.Stop_propagation + ), ], [buttons] @ { From abde22a3db505612f4398ff088827129405ad634 Mon Sep 17 00:00:00 2001 From: Matt Keenan <31668468+Negabinary@users.noreply.github.com> Date: Thu, 5 Feb 2026 17:42:59 -0500 Subject: [PATCH 5/7] Reword write step box --- src/web/app/editors/stepper/MissingStep.re | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/web/app/editors/stepper/MissingStep.re b/src/web/app/editors/stepper/MissingStep.re index 51a106aa9a..8488bbb697 100644 --- a/src/web/app/editors/stepper/MissingStep.re +++ b/src/web/app/editors/stepper/MissingStep.re @@ -681,7 +681,7 @@ module View = { div_c( "rewrite-box", [ - Node.text("Replace: "), + Node.text("From: "), CodeViewable.view_any( ~globals, ~settings= @@ -692,7 +692,7 @@ module View = { ), Exp(unboxed_selected_exp), ), - Node.text("With: "), + Node.text("Take a step to: "), div_c( "inline-editor-wrapper", [ @@ -833,7 +833,7 @@ module View = { ? [ proof_button( ~callback=inject(ProposeWrittenStep), - "Write Step ▼", + "Take Step ▼", ), ] : [] From d503b8c04d0cb2095aab8ec56fe5c3735cfce28e Mon Sep 17 00:00:00 2001 From: Matt Keenan <31668468+Negabinary@users.noreply.github.com> Date: Fri, 6 Feb 2026 11:30:21 -0500 Subject: [PATCH 6/7] Per-exercise setting --- src/web/exercises/TheoremExerciseSpec.re | 1 + src/web/exercises/examples/ReverseReverse.ml | 1 + src/web/exercises/examples/TheoremTemplate.ml | 1 + src/web/view/TheoremExerciseMode.re | 64 ++++++++++++++++--- 4 files changed, 59 insertions(+), 8 deletions(-) diff --git a/src/web/exercises/TheoremExerciseSpec.re b/src/web/exercises/TheoremExerciseSpec.re index a2d3b89f77..29862362b1 100644 --- a/src/web/exercises/TheoremExerciseSpec.re +++ b/src/web/exercises/TheoremExerciseSpec.re @@ -8,4 +8,5 @@ type t = { prelude: Haz3lcore.Zipper.t, lemmas: Haz3lcore.Zipper.t, theorem: Haz3lcore.Zipper.t, + write_out_steps: bool, }; diff --git a/src/web/exercises/examples/ReverseReverse.ml b/src/web/exercises/examples/ReverseReverse.ml index d767715741..a9adb6cd7e 100644 --- a/src/web/exercises/examples/ReverseReverse.ml +++ b/src/web/exercises/examples/ReverseReverse.ml @@ -4,6 +4,7 @@ let exercise : TheoremExerciseSpec.t = Option.get (Haz3lcore.Id.of_string "f2132f9f-a452-481b-ba9a-c40e7d2346aa"); title = "Reverse! Reverse!"; prompt = "Show that this implementation of list reverse is its own inverse."; + write_out_steps = true; prelude = { refractors = Haz3lcore.ZipperBase.Refractor.init; diff --git a/src/web/exercises/examples/TheoremTemplate.ml b/src/web/exercises/examples/TheoremTemplate.ml index ed122555da..9a6cac0cb6 100644 --- a/src/web/exercises/examples/TheoremTemplate.ml +++ b/src/web/exercises/examples/TheoremTemplate.ml @@ -4,6 +4,7 @@ let exercise : TheoremExerciseSpec.t = Option.get (Haz3lcore.Id.of_string "f2132f9f-a452-481b-ba9a-c40e7d2346aa"); title = ""; prompt = ""; + write_out_steps = true; prelude = { refractors = Haz3lcore.ZipperBase.Refractor.init; diff --git a/src/web/view/TheoremExerciseMode.re b/src/web/view/TheoremExerciseMode.re index b43baaef23..36cccb917c 100644 --- a/src/web/view/TheoremExerciseMode.re +++ b/src/web/view/TheoremExerciseMode.re @@ -21,6 +21,7 @@ module Model = { title: string, prompt: string, cells, + write_out_steps: bool, }; [@deriving (show({with_path: false}), sexp, yojson)] @@ -48,6 +49,7 @@ module Model = { result: persistent.theorem |> EvalResult.Model.unpersist, }, }, + write_out_steps: spec.write_out_steps, }; }; @@ -61,6 +63,7 @@ module Model = { lemmas: CellEditor.Model.mk(Editor.Model.mk(spec.lemmas)), theorem: CellEditor.Model.mk(Editor.Model.mk(spec.theorem)), }, + write_out_steps: spec.write_out_steps, }; }; @@ -72,6 +75,7 @@ module Model = { prelude: model.cells.prelude.editor.editor.state.zipper, lemmas: model.cells.lemmas.editor.editor.state.zipper, theorem: model.cells.theorem.editor.editor.state.zipper, + write_out_steps: model.write_out_steps, }; }; @@ -83,6 +87,32 @@ module Model = { }; }; +let override_core_settings = + (settings: Language.CoreSettings.t, model: Model.t) => { + { + ...settings, + evaluation: { + ...settings.evaluation, + write_out_steps: + model.write_out_steps || settings.evaluation.write_out_steps, + }, + }; +}; + +let override_settings = (settings: Settings.t, model: Model.t) => { + { + ...settings, + core: override_core_settings(settings.core, model), + }; +}; + +let override_globals = (globals: Globals.t, model: Model.t) => { + { + ...globals, + settings: override_settings(globals.settings, model), + }; +}; + module Update = { open Updated; @@ -90,11 +120,13 @@ module Update = { type t = | UpdateTitle(string) | UpdatePrompt(string) + | ToggleWriteOutSteps | Prelude(CellEditor.Update.t) | Lemmas(CellEditor.Update.t) | Theorem(CellEditor.Update.t); let update = (~settings: Settings.t, action: t, model: Model.t) => { + let settings = override_settings(settings, model); switch (action) { | UpdateTitle(new_title) when settings.instructor_mode => Updated.return({ @@ -112,6 +144,14 @@ module Update = { | UpdatePrompt(_) => print_endline("Instructor-only action"); Updated.return_quiet(model); + | ToggleWriteOutSteps when settings.instructor_mode => + Updated.return({ + ...model, + write_out_steps: !model.write_out_steps, + }) + | ToggleWriteOutSteps => + print_endline("Instructor-only action"); + Updated.return_quiet(model); | Prelude(action) when settings.instructor_mode => let* new_cell = CellEditor.Update.update(~settings, action, model.cells.prelude); @@ -199,6 +239,7 @@ module Update = { switch (action) { | UpdateTitle(_) => true | UpdatePrompt(_) => true + | ToggleWriteOutSteps => true | Prelude(action) => CellEditor.Update.can_undo(action) | Lemmas(action) => CellEditor.Update.can_undo(action) | Theorem(action) => CellEditor.Update.can_undo(action) @@ -207,6 +248,7 @@ module Update = { let calculate = (~settings, ~is_edited, ~schedule_action, model: Model.t): Model.t => { + let settings = override_core_settings(settings, model); // Work out the terms let just_prelude_term = MakeTerm.from_zip_for_sem( @@ -441,6 +483,7 @@ module View = { ~selection: option(Selection.t), model: Model.t, ) => { + let globals = override_globals(globals, model); let title_view = CellCommon.simple_cell_view([ div( @@ -471,6 +514,16 @@ module View = { ), ]); + let write_out_steps_view = + CellCommon.simple_cell_view([ + text("Force writing out proof steps:"), + Widgets.toggle_named("", model.write_out_steps, _ => + inject(Update.ToggleWriteOutSteps) + ), + ]); + let write_out_steps_view = + globals.settings.instructor_mode ? [write_out_steps_view] : []; + let prompt_view = CellCommon.simple_cell_view([ globals.settings.instructor_mode @@ -542,13 +595,8 @@ module View = { |> Option.value(~default=(Float.nan, Float.nan)), ); - [ - score_view, - title_view, - prompt_view, - prelude_view, - lemmas_view, - theorem_view, - ]; + [score_view, title_view] + @ write_out_steps_view + @ [prompt_view, prelude_view, lemmas_view, theorem_view]; }; }; From 5896058e0553361b6fd87d345b132a16186c1f02 Mon Sep 17 00:00:00 2001 From: Matt Keenan <31668468+Negabinary@users.noreply.github.com> Date: Tue, 10 Feb 2026 10:43:05 -0500 Subject: [PATCH 7/7] Retain highlight --- src/web/app/editors/cell/CellEditor.re | 2 +- src/web/app/editors/code/CodeEditable.re | 115 +++++++++++-------- src/web/app/editors/result/EvalResult.re | 2 +- src/web/app/editors/stepper/InductionCase.re | 4 +- src/web/app/editors/stepper/InductionStep.re | 4 +- src/web/app/editors/stepper/MissingStep.re | 40 +++++-- src/web/app/editors/stepper/StepperBase.re | 8 +- 7 files changed, 112 insertions(+), 63 deletions(-) diff --git a/src/web/app/editors/cell/CellEditor.re b/src/web/app/editors/cell/CellEditor.re index 75090b5ce7..4294cb36a4 100644 --- a/src/web/app/editors/cell/CellEditor.re +++ b/src/web/app/editors/cell/CellEditor.re @@ -247,7 +247,7 @@ module View = { locked ? _ => Ui_effect.Ignore : (action => inject(MainEditor(action))), - ~selected=selected == Some(MainEditor), + ~selected=selected == Some(MainEditor) ? Yes : No, ~overlays=overlays(model.editor.editor), ~dynamics=EvalResult.Model.dynamics(model.result), model.editor, diff --git a/src/web/app/editors/code/CodeEditable.re b/src/web/app/editors/code/CodeEditable.re index 64994b983e..854d14cb18 100644 --- a/src/web/app/editors/code/CodeEditable.re +++ b/src/web/app/editors/code/CodeEditable.re @@ -229,7 +229,7 @@ module View = { let deco = ( - ~expand_selection=false, + ~expand_selection, ~syntax: CachedSyntax.t, ~globals: Globals.t, z: Zipper.t, @@ -263,65 +263,86 @@ module View = { ), ]; + type selected = + | Yes + | JustHighlight + | No; + let view = ( ~globals: Globals.t, ~signal: event => Ui_effect.t(unit), ~inject: Update.t => Ui_effect.t(unit), - ~selected: bool, + ~selected: selected, ~overlays: list(Node.t)=[], ~dynamics: Language.Dynamics.Map.t, - ~expand_selection=?, + ~expand_selection=false, model: Model.t, ) => { /* Sync document-level click listener for closing context menu */ ContextMenuListener.sync( - selected && Model.context_menu_is_open(model), + selected == Yes && Model.context_menu_is_open(model), inject(ContextMenu(ContextMenu.Model.Close)), ); let edit_decos = - selected - ? deco( - ~expand_selection?, + switch (selected) { + | Yes => + deco( + ~expand_selection, + ~syntax=model.editor.syntax, + ~globals, + model.editor.state.zipper, + ) + @ [ + Arms.Refractors.all( + ~font_metrics=globals.font_metrics, ~syntax=model.editor.syntax, - ~globals, + ~dynamics, model.editor.state.zipper, - ) - @ [ - Arms.Refractors.all( - ~font_metrics=globals.font_metrics, - ~syntax=model.editor.syntax, - ~dynamics, - model.editor.state.zipper, - ), - ] - @ ( - switch (model.context_menu) { - | Some(selected_index) => [ - /* Backdrop for scroll-close. Click handling is done via - ContextMenuListener's document-level event listener. */ - Node.div( - ~attrs=[ - Attr.classes(["context-menu-backdrop"]), - Attr.on_wheel(_ => - inject(ContextMenu(ContextMenu.Model.Close)) - ), - ], - [], - ), - ContextMenu.view( - ~inject=a => inject(Perform(a)), - ~syntax=model.editor.syntax, - ~info_map=model.statics.info_map, - ~font_metrics=globals.font_metrics, - ~selected_index, - model.editor.state.zipper, - ), - ] - | None => [] - } - ) - : []; + ), + ] + @ ( + switch (model.context_menu) { + | Some(selected_index) => [ + /* Backdrop for scroll-close. Click handling is done via + ContextMenuListener's document-level event listener. */ + Node.div( + ~attrs=[ + Attr.classes(["context-menu-backdrop"]), + Attr.on_wheel(_ => + inject(ContextMenu(ContextMenu.Model.Close)) + ), + ], + [], + ), + ContextMenu.view( + ~inject=a => inject(Perform(a)), + ~syntax=model.editor.syntax, + ~info_map=model.statics.info_map, + ~font_metrics=globals.font_metrics, + ~selected_index, + model.editor.state.zipper, + ), + ] + | None => [] + } + ) + | JustHighlight => [ + ( + expand_selection + ? Highlight.selection_expanded( + ~term_data=model.editor.syntax.term_data, + ) + : Highlight.selection + )( + ~measured=model.editor.syntax.measured, + ~shape_map=model.editor.syntax.shape_map, + ~font_metrics=globals.font_metrics, + model.editor.state.zipper, + ), + ] + | No => [] + }; let zipper = model.editor.state.zipper; let refractor_data = RefractorView.mk_data( @@ -336,7 +357,7 @@ module View = { ~statics=model.statics.info_map, ~dynamics, ~sample_cursor=zipper.refractors.sample_cursor, - ~editor_active=selected, + ~editor_active=selected != No, ); let visible = globals.visible_rows; let refractors_model = @@ -361,7 +382,7 @@ module View = { ~statics=model.statics.info_map, ~dynamics, ~sample_cursor=zipper.refractors.sample_cursor, - ~editor_active=selected, + ~editor_active=selected != No, ), model.editor.syntax.projector_list, ); @@ -441,7 +462,7 @@ module View = { Node.div( ~attrs=[ Attr.classes( - ["cell-item", "code-editor"] @ (selected ? ["selected"] : []), + ["cell-item", "code-editor"] @ (selected != No ? ["selected"] : []), ), Attr.on_contextmenu(evt => switch (Pointer.Event.mk(evt)) { diff --git a/src/web/app/editors/result/EvalResult.re b/src/web/app/editors/result/EvalResult.re index bb34f4edd9..26eb3001ac 100644 --- a/src/web/app/editors/result/EvalResult.re +++ b/src/web/app/editors/result/EvalResult.re @@ -464,7 +464,7 @@ module View = { ~globals, ~signal, ~inject, - ~selected=selected == Some(Evaluation()), + ~selected=selected == Some(Evaluation()) ? Yes : No, ~locked, model.result |> Calc.get_value, editor |> Calc.get_saved_exc(~print="result editor missing"), diff --git a/src/web/app/editors/stepper/InductionCase.re b/src/web/app/editors/stepper/InductionCase.re index 7ca5776829..4be56bbf94 100644 --- a/src/web/app/editors/stepper/InductionCase.re +++ b/src/web/app/editors/stepper/InductionCase.re @@ -329,8 +329,8 @@ module F = (Stepper: STEPPER) => { ~inject=x => inject(PatternUpdate(x)), ~selected= switch (focus) { - | Some(Pattern ()) => true - | _ => false + | Some(Pattern ()) => Yes + | _ => No }, ~dynamics=Dynamics.Map.empty, model.pattern, diff --git a/src/web/app/editors/stepper/InductionStep.re b/src/web/app/editors/stepper/InductionStep.re index 073cba731e..40ffd77f2f 100644 --- a/src/web/app/editors/stepper/InductionStep.re +++ b/src/web/app/editors/stepper/InductionStep.re @@ -397,9 +397,9 @@ module F = ~inject=x => inject(ScrutUpdate(x)), ~selected= switch (focus) { - | Some(Scrut(_)) => true + | Some(Scrut(_)) => Yes | Some(_) - | None => false + | None => No }, ~dynamics=Dynamics.Map.empty, model.scrut, diff --git a/src/web/app/editors/stepper/MissingStep.re b/src/web/app/editors/stepper/MissingStep.re index 8488bbb697..c638b7b7d1 100644 --- a/src/web/app/editors/stepper/MissingStep.re +++ b/src/web/app/editors/stepper/MissingStep.re @@ -592,8 +592,8 @@ module View = { ~inject=x => inject(RewriteEditorAction(x)), ~selected= switch (selected) { - | Some(RewriteEditor ()) => true - | _ => false + | Some(RewriteEditor ()) => Yes + | _ => No }, ~dynamics=Dynamics.Map.empty, editor, @@ -704,8 +704,8 @@ module View = { ~inject=x => inject(WriteStepEditorAction(x)), ~selected= switch (selected) { - | Some(WriteStepEditor ()) => true - | _ => false + | Some(WriteStepEditor ()) => Yes + | _ => No }, ~dynamics=Dynamics.Map.empty, editor, @@ -779,6 +779,8 @@ module View = { ]; }; + let text_arrow = (b: bool) => if (b) {"▲"} else {"▼"}; + // I want to make a bunch of buttons here: // Evaluate [TODO], Rewrite, Axioms, Cases, let buttons = @@ -833,14 +835,38 @@ module View = { ? [ proof_button( ~callback=inject(ProposeWrittenStep), - "Take Step ▼", + "Take Step " + ++ text_arrow( + switch (model.open_box) { + | Model.WrittenStepOpen(_) => true + | _ => false + }, + ), ), ] : [] ) @ [ - proof_button(~callback=inject(ProposeRewrite), "Algebra ▼"), - proof_button(~callback=inject(ToggleAxioms), "Assumptions ▼"), + proof_button( + ~callback=inject(ProposeRewrite), + "Algebra " + ++ text_arrow( + switch (model.open_box) { + | Model.RewritesOpen(_) => true + | _ => false + }, + ), + ), + proof_button( + ~callback=inject(ToggleAxioms), + "Assumptions " + ++ text_arrow( + switch (model.open_box) { + | Model.AxiomsOpen(_) => true + | _ => false + }, + ), + ), proof_button( ~callback= Ui_effect.Many([ diff --git a/src/web/app/editors/stepper/StepperBase.re b/src/web/app/editors/stepper/StepperBase.re index f166801f93..289b02b34e 100644 --- a/src/web/app/editors/stepper/StepperBase.re +++ b/src/web/app/editors/stepper/StepperBase.re @@ -1071,9 +1071,11 @@ and Stepper: { }, ~inject=x => inject(EditorAction(x)), ~selected= - switch (focus) { - | Some(Here(_)) => true - | _ => false + switch (focus, model.step_kind) { + | (Some(Here(_)), _) => Yes + | (_, MissingStep({open_box: NoneOpen, _})) => No + | (_, MissingStep(_)) => JustHighlight + | _ => No }, ~selected_id=selected_exp |> Option.map(Exp.rep_id), ~overlays=