Skip to content

Commit

Permalink
Create sub-models for editors
Browse files Browse the repository at this point in the history
Negabinary committed May 21, 2024
1 parent f810f62 commit 5fb83bc
Showing 24 changed files with 1,185 additions and 991 deletions.
61 changes: 35 additions & 26 deletions src/haz3lcore/dynamics/Stepper.re
Original file line number Diff line number Diff line change
@@ -14,7 +14,10 @@ type stepper_state =
| StepTimeout(EvalObj.t);

[@deriving (show({with_path: false}), sexp, yojson)]
type history = Aba.t((DHExp.t, Editor.t, EvaluatorState.t), step);
type a = (CachedStatics.statics, Editor.t, EvaluatorState.t);

[@deriving (show({with_path: false}), sexp, yojson)]
type history = Aba.t(a, step);

[@deriving (show({with_path: false}), sexp, yojson)]
type t = {
@@ -196,8 +199,8 @@ let should_hide_step = (~settings, x: step): (FilterAction.action, step) =>
};

let get_elab = ({history, _}: t): Elaborator.Elaboration.t => {
let (d, _, _) = Aba.last_a(history);
{d: d};
let (cs: CachedStatics.statics, _, _) = Aba.last_a(history);
{d: cs.term};
};

let get_next_steps = s => s.next_options;
@@ -212,12 +215,14 @@ let step_pending = (idx: int, stepper: t) => {
{...stepper, stepper_state: StepPending(idx)};
};

let rec evaluate_pending = (~settings, s: t) => {
let rec evaluate_pending = (~settings: CoreSettings.t, s: t) => {
switch (s.stepper_state) {
| StepperDone
| StepTimeout(_) => s
| StepperReady =>
let next' = s.next_options |> List.map(should_hide_eval_obj(~settings));
let next' =
s.next_options
|> List.map(should_hide_eval_obj(~settings=settings.evaluation));
let next'' = List.mapi((i, x) => (i, x), next');
switch (
List.find_opt(((_, (act, _))) => act == FilterAction.Eval, next'')
@@ -228,7 +233,7 @@ let rec evaluate_pending = (~settings, s: t) => {
};
| StepPending(i) =>
let eo = List.nth(s.next_options, i);
let (d, _, state) = Aba.hd(s.history);
let ({term: d, _}: CachedStatics.statics, _, state) = Aba.hd(s.history);
let state_ref = ref(state);
let d_loc' =
(
@@ -250,8 +255,9 @@ let rec evaluate_pending = (~settings, s: t) => {
};
let new_state = state_ref^;
let editor = ExpToSegment.exp_to_editor(~inline=false, d');
let statics = CachedStatics.statics_of_term(~settings, d', editor);
{
history: s.history |> Aba.cons((d', editor, new_state), new_step),
history: s.history |> Aba.cons((statics, editor, new_state), new_step),
stepper_state: StepperReady,
next_options: decompose(d', new_state),
}
@@ -273,8 +279,9 @@ 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);
let statics = CachedStatics.statics_of_term(~settings, d, editor);
{
history: Aba.singleton((d, editor, state)),
history: Aba.singleton((statics, editor, state)),
next_options: decompose(d, state),
stepper_state: StepperReady,
}
@@ -304,8 +311,8 @@ let step_backward = (~settings, s: t) => {
{
history: h',
next_options: {
let (d, _, st) = Aba.hd(h');
decompose(d, st);
let (cs, _, st) = Aba.hd(h');
decompose(cs.term, st);
},
stepper_state: StepperDone,
};
@@ -356,8 +363,7 @@ let get_justification: step_kind => string =
| UnOp(Meta(Unquote)) => failwith("INVALID STEP");

type step_info = {
hidden_history:
Aba.t((DHExp.t, Editor.t, EvaluatorState.t), (step, Id.t)),
hidden_history: Aba.t(a, (step, Id.t)),
chosen_step: option(step), // The step that was taken next
previous_step: option((step, Id.t)) // The step that will be displayed above this one (an Id in included because it may have changed since the step was taken)
};
@@ -448,30 +454,33 @@ let (sexp_of_persistent, persistent_of_sexp) =
);

let to_persistent_history = history =>
Aba.map_a(((d, _, s)) => (d, s), history);
Aba.map_a((({term: d, _}, _, s): a) => (d, s), history);

// Remove EvalObj.t objects from stepper to prevent problems when loading
let to_persistent: t => persistent =
({history, _}) => {persistent_history: history |> to_persistent_history};

let from_persistent_history = history =>
let from_persistent_history = (~settings, history) =>
Aba.map_a(
((d, s)) => (d, ExpToSegment.exp_to_editor(d, ~inline=false), s),
((d, s)) => {
let editor = ExpToSegment.exp_to_editor(d, ~inline=false);
let statics = CachedStatics.statics_of_term(~settings, d, editor);
(statics, editor, s);
},
history,
);

let from_persistent: persistent => t =
({persistent_history}) => {
let history = persistent_history |> from_persistent_history;
{
history,
next_options: {
let (d, _, state) = Aba.hd(history);
decompose(d, state);
},
stepper_state: StepperDone,
};
let from_persistent = (~settings, {persistent_history}) => {
let history = persistent_history |> from_persistent_history(~settings);
{
history,
next_options: {
let ({term: d, _}: CachedStatics.statics, _, state) = Aba.hd(history);
decompose(d, state);
},
stepper_state: StepperDone,
};
};

type selection = int;

8 changes: 8 additions & 0 deletions src/haz3lcore/prog/CachedStatics.re
Original file line number Diff line number Diff line change
@@ -7,6 +7,14 @@ type statics = {
error_ids: list(Id.t),
};

let statics_of_term = (~settings, term: UExp.t, editor: Editor.t): statics => {
let info_map =
Interface.Statics.mk_map_ctx(settings, Builtins.ctx_init, term);
let error_ids =
Statics.Map.error_ids(editor.state.meta.term_ranges, info_map);
{term, info_map, error_ids};
};

let empty_statics: statics = {
term: UExp.{ids: [Id.invalid], copied: false, term: Tuple([])},
info_map: Id.Map.empty,
29 changes: 25 additions & 4 deletions src/haz3lcore/prog/ModelResult.re
Original file line number Diff line number Diff line change
@@ -49,8 +49,7 @@ let run_pending = (~settings: CoreSettings.t) =>
evaluation: Interface.evaluate(~settings, elab.d),
})
| Evaluation(_) as e => e
| Stepper(s) =>
Stepper(Stepper.evaluate_pending(~settings=settings.evaluation, s));
| Stepper(s) => Stepper(Stepper.evaluate_pending(~settings, s));

let update_evaluation =
(
@@ -134,10 +133,10 @@ let to_persistent: t => persistent =
| Evaluation(_) => Evaluation
| Stepper(s) => Stepper(Stepper.to_persistent(s));

let of_persistent: persistent => t =
let of_persistent = (~settings) =>
fun
| Evaluation => NoElab
| Stepper(s) => Stepper(Stepper.from_persistent(s));
| Stepper(s) => Stepper(Stepper.from_persistent(~settings, s));

[@deriving (show({with_path: false}), sexp, yojson)]
type selection = int;
@@ -167,3 +166,25 @@ let put_selected_editor = (~selection: selection, mr: t, editor) =>
| Evaluation(_) => mr
| Stepper(s) => Stepper(Stepper.put_selected_editor(~selection, s, editor))
};

let get_elaboration = mr =>
switch (mr) {
| NoElab => None
| Evaluation({elab, _}) => Some(elab)
| Stepper(s) => Some(Stepper.get_elab(s))
};

let perform = (~settings, idx, action, mr) => {
get_selected_editor(~selection=idx, mr)
|> Option.map(editor =>
editor
|> Perform.go(~settings, action)
|> (
fun
| Ok(editor) => editor
| Error(e) => raise(Action.Failure.Exception(e))
)
|> put_selected_editor(~selection=idx, mr)
)
|> Option.value(~default=mr);
};
8 changes: 4 additions & 4 deletions src/haz3lcore/statics/Statics.re
Original file line number Diff line number Diff line change
@@ -229,10 +229,10 @@ and uexp_to_info_map =
let go_pat = upat_to_info_map(~ctx, ~ancestors);
let atomic = self => add(~self, ~co_ctx=CoCtx.empty, m);
switch (term) {
| Closure(_) =>
failwith(
"TODO: implement closure type checking - see how dynamic type assignment does it",
)
| Closure(_, e) =>
// TODO: implement closure type checking properly - see how dynamic type assignment does it
let (e, m) = go(~mode, e, m);
add(~self=Just(e.ty), ~co_ctx=e.co_ctx, m);
| MultiHole(tms) =>
let (co_ctxs, m) = multi(~ctx, ~ancestors, m, tms);
add(~self=IsMulti, ~co_ctx=CoCtx.union(co_ctxs), m);
2 changes: 2 additions & 0 deletions src/haz3lcore/zipper/action/Action.re
Original file line number Diff line number Diff line change
@@ -71,6 +71,8 @@ module Failure = {
| Cant_paste
| Cant_undo
| Cant_redo;

exception Exception(t);
};

module Result = {
17 changes: 0 additions & 17 deletions src/haz3lcore/zipper/action/Perform.re
Original file line number Diff line number Diff line change
@@ -208,23 +208,6 @@ let rec go_z =
};
};

// let paste_into_zip = (z: Zipper.t, str: string): option(Zipper.t) => {
// /* HACK(andrew): These two perform calls are a hack to
// deal with the fact that pasting something like "let a = b in"
// won't trigger the barfing of the "in"; to trigger this, we
// insert a space, and then we immediately delete it. */
// let settings = CoreSettings.off;
// let* z = zipper_of_string(~zipper_init=z, str);
// switch (Perform.go_z(~settings, Insert(" "), z)) {
// | Error(_) => None
// | Ok(z) =>
// switch (Perform.go_z(~settings, Destruct(Left), z)) {
// | Error(_) => None
// | Ok(z) => Some(z)
// }
// };
// };

let go =
(~settings: CoreSettings.t, a: Action.t, ed: Editor.t)
: Action.Result.t(Editor.t) =>
7 changes: 4 additions & 3 deletions src/haz3lweb/Export.re
Original file line number Diff line number Diff line change
@@ -22,8 +22,9 @@ type all_f22 = {
let mk_all = (~instructor_mode, ~log) => {
let settings = Store.Settings.export();
let explainThisModel = Store.ExplainThisModel.export();
let scratch = Store.Scratch.export();
let documentation = Store.Documentation.export();
let scratch = Store.Scratch.export(~settings=Haz3lcore.CoreSettings.off);
let documentation =
Store.Documentation.export(~settings=Haz3lcore.CoreSettings.off);
let exercise =
Store.Exercise.export(
~specs=ExerciseSettings.exercises,
@@ -53,7 +54,7 @@ let import_all = (data, ~specs) => {
let settings = Store.Settings.import(all.settings);
Store.ExplainThisModel.import(all.explainThisModel);
let instructor_mode = settings.instructor_mode;
Store.Scratch.import(all.scratch);
Store.Scratch.import(~settings=settings.core, all.scratch);
Store.Exercise.import(all.exercise, ~specs, ~instructor_mode);
Log.import(all.log);
};
25 changes: 10 additions & 15 deletions src/haz3lweb/Model.re
Original file line number Diff line number Diff line change
@@ -57,21 +57,20 @@ let mk = (editors, results, statics) => {
let blank =
mk(Editors.Scratch(0, []), ModelResults.empty, CachedStatics.empty);

let load_editors =
(~mode: Settings.mode, ~instructor_mode: bool)
: (Editors.t, ModelResults.t) =>
switch (mode) {
let load_editors = (~settings: Settings.t): (Editors.t, ModelResults.t) =>
switch (settings.mode) {
| Scratch =>
let (idx, slides, results) = Store.Scratch.load();
let (idx, slides, results) = Store.Scratch.load(~settings=settings.core);
(Scratch(idx, slides), results);
| Documentation =>
let (name, slides, results) = Store.Documentation.load();
let (name, slides, results) =
Store.Documentation.load(~settings=settings.core);
(Documentation(name, slides), results);
| Exercises =>
let (n, specs, exercise) =
Store.Exercise.load(
~specs=ExerciseSettings.exercises,
~instructor_mode,
~instructor_mode=settings.instructor_mode,
);
(Exercises(n, specs, exercise), ModelResults.empty);
};
@@ -90,11 +89,7 @@ let save_editors =
let load = (init_model: t): t => {
let settings = Store.Settings.load();
let explainThisModel = Store.ExplainThisModel.load();
let (editors, results) =
load_editors(
~mode=settings.mode,
~instructor_mode=settings.instructor_mode,
);
let (editors, results) = load_editors(~settings);
let ui_state = init_model.ui_state;
let statics = Editors.mk_statics(~settings, editors);
{editors, settings, results, statics, explainThisModel, ui_state};
@@ -114,10 +109,10 @@ let reset = (model: t): t => {
/* Reset model to default, including in localstorage,
but don't otherwise erase localstorage, allowing
e.g. api keys to persist */
ignore(Store.Settings.init());
let settings = Store.Settings.init().core;
ignore(Store.ExplainThisModel.init());
ignore(Store.Scratch.init());
ignore(Store.Documentation.init());
ignore(Store.Scratch.init(~settings));
ignore(Store.Documentation.init(~settings));
ignore(Store.Exercise.init(~instructor_mode=true));
let new_model = load(blank);
{
40 changes: 20 additions & 20 deletions src/haz3lweb/Store.re
Original file line number Diff line number Diff line change
@@ -121,14 +121,14 @@ module Scratch = {
|> ModelResults.bindings,
);

let of_persistent = ((idx, slides, results): persistent) => {
let of_persistent = (~settings, (idx, slides, results): persistent) => {
(
idx,
List.map(ScratchSlide.unpersist, slides),
results
|> List.to_seq
|> ModelResults.of_seq
|> ModelResults.map(ModelResult.of_persistent),
|> ModelResults.map(ModelResult.of_persistent(~settings)),
);
};

@@ -144,23 +144,23 @@ module Scratch = {
JsUtil.set_localstore(save_scratch_key, serialize(scratch));
};

let init = () => {
let scratch = of_persistent(Init.startup.scratch);
let init = (~settings) => {
let scratch = of_persistent(~settings, Init.startup.scratch);
save(scratch);
scratch;
};

let load = () =>
let load = (~settings) =>
switch (JsUtil.get_localstore(save_scratch_key)) {
| None => init()
| None => init(~settings)
| Some(data) =>
try(deserialize(data)) {
| _ => init()
try(deserialize(~settings, data)) {
| _ => init(~settings)
}
};

let export = () => serialize(load());
let import = data => save(deserialize(data));
let export = (~settings) => serialize(load(~settings));
let import = (~settings, data) => save(deserialize(~settings, data));
};

module Documentation = {
@@ -186,14 +186,14 @@ module Documentation = {
|> ModelResults.bindings,
);

let of_persistent = ((string, slides, results): persistent) => {
let of_persistent = (~settings, (string, slides, results): persistent) => {
(
string,
List.map(unpersist, slides),
results
|> List.to_seq
|> ModelResults.of_seq
|> ModelResults.map(ModelResult.of_persistent),
|> ModelResults.map(ModelResult.of_persistent(~settings)),
);
};

@@ -209,23 +209,23 @@ module Documentation = {
JsUtil.set_localstore(save_documentation_key, serialize(slides));
};

let init = () => {
let documentation = of_persistent(Init.startup.documentation);
let init = (~settings) => {
let documentation = of_persistent(~settings, Init.startup.documentation);
save(documentation);
documentation;
};

let load = () =>
let load = (~settings) =>
switch (JsUtil.get_localstore(save_documentation_key)) {
| None => init()
| None => init(~settings)
| Some(data) =>
try(deserialize(data)) {
| _ => init()
try(deserialize(~settings, data)) {
| _ => init(~settings)
}
};

let export = () => serialize(load());
let import = data => save(deserialize(data));
let export = (~settings) => serialize(load(~settings));
let import = (~settings, data) => save(deserialize(~settings, data));
};

module Exercise = {
28 changes: 7 additions & 21 deletions src/haz3lweb/Update.re
Original file line number Diff line number Diff line change
@@ -212,10 +212,7 @@ 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(
~settings=model.settings.core.evaluation,
elabs,
);
|> ModelResults.update_elabs(~settings=model.settings.core, elabs);
let step_rs = ModelResults.to_step(new_rs);
if (!ModelResults.is_empty(step_rs)) {
let new_rs =
@@ -303,8 +300,11 @@ let switch_scratch_slide =
let export_persistent_data = () => {
let data: PersistentData.t = {
documentation:
Store.Documentation.load() |> Store.Documentation.to_persistent,
scratch: Store.Scratch.load() |> Store.Scratch.to_persistent,
Store.Documentation.load(~settings=CoreSettings.off)
|> Store.Documentation.to_persistent,
scratch:
Store.Scratch.load(~settings=CoreSettings.off)
|> Store.Scratch.to_persistent,
settings: Store.Settings.load(),
};
let contents =
@@ -524,18 +524,6 @@ let rec apply =
model.results
|> ModelResults.find(key)
|> ModelResult.step_forward(idx);
let _ = print_endline("Ouch");
let _ =
print_endline(
Stepper.show_stepper_state(
(
fun
| (Stepper(s): ModelResult.t) => s
| _ => failwith("")
)(r).
stepper_state,
),
);
Ok({...model, results: model.results |> ModelResults.add(key, r)});
| StepperAction(key, StepBackward) =>
let r =
@@ -553,9 +541,7 @@ let rec apply =
Some(
v
|> Option.value(~default=NoElab: ModelResult.t)
|> ModelResult.toggle_stepper(
~settings=model.settings.core.evaluation,
),
|> ModelResult.toggle_stepper(~settings=model.settings.core),
)
),
})
540 changes: 0 additions & 540 deletions src/haz3lweb/view/Cell.re

This file was deleted.

202 changes: 0 additions & 202 deletions src/haz3lweb/view/CodeEditor.re

This file was deleted.

107 changes: 61 additions & 46 deletions src/haz3lweb/view/Deco.re
Original file line number Diff line number Diff line change
@@ -2,25 +2,21 @@ open Virtual_dom.Vdom;
open Util;
open Haz3lcore;

module Deco =
(
M: {
let font_metrics: FontMetrics.t;
let map: Measured.t;
let show_backpack_targets: bool;
let terms: TermMap.t;
let term_ranges: TermRanges.t;
let error_ids: list(Id.t);
let tiles: TileMap.t;
let next_steps: list(Id.t);
},
) => {
let font_metrics = M.font_metrics;
module Deco = (M: {
let ui_state: Model.ui_state;
let editor: Editor.t;
}) => {
let font_metrics = M.ui_state.font_metrics;
let map = M.editor.state.meta.measured;
let show_backpack_targets = M.ui_state.show_backpack_targets;
let terms = M.editor.state.meta.terms;
let term_ranges = M.editor.state.meta.term_ranges;
let tiles = M.editor.state.meta.tiles;

let tile = id => Id.Map.find(id, M.tiles);
let tile = id => Id.Map.find(id, tiles);

let caret = (z: Zipper.t): list(Node.t) => {
let origin = Zipper.caret_point(M.map, z);
let origin = Zipper.caret_point(map, z);
let shape = Zipper.caret_direction(z);
let side =
switch (Indicated.piece(z)) {
@@ -46,11 +42,11 @@ module Deco =
switch (p) {
| Tile(t) => sel_of_tile(~start_shape, t)
| Grout(g) => [
Some(sel_shard_svg(~start_shape, Measured.find_g(g, M.map), p)),
Some(sel_shard_svg(~start_shape, Measured.find_g(g, map), p)),
]
| Secondary(w) when Secondary.is_linebreak(w) => [None]
| Secondary(w) => [
Some(sel_shard_svg(~start_shape, Measured.find_w(w, M.map), p)),
Some(sel_shard_svg(~start_shape, Measured.find_w(w, map), p)),
]
};
let start_shape =
@@ -62,7 +58,7 @@ module Deco =
}
and sel_of_tile = (~start_shape, t: Tile.t): list(option(shard_data)) => {
let tile_shards =
Measured.find_shards(t, M.map)
Measured.find_shards(t, map)
|> List.filter(((i, _)) => List.mem(i, t.shards))
|> List.map(((index, measurement)) =>
[
@@ -120,12 +116,12 @@ module Deco =
};
let range: option((Measured.Point.t, Measured.Point.t)) = {
// if (Piece.has_ends(p)) {
let id = Id.Map.find(Piece.id(p), M.terms) |> Any.rep_id;
switch (TermRanges.find_opt(id, M.term_ranges)) {
let id = Id.Map.find(Piece.id(p), terms) |> Any.rep_id;
switch (TermRanges.find_opt(id, term_ranges)) {
| None => None
| Some((p_l, p_r)) =>
let l = Measured.find_p(p_l, M.map).origin;
let r = Measured.find_p(p_r, M.map).last;
let l = Measured.find_p(p_l, map).origin;
let r = Measured.find_p(p_r, map).last;
Some((l, r));
};
};
@@ -138,19 +134,19 @@ module Deco =
| None => []
| Some(range) =>
let tiles =
Id.Map.find(Piece.id(p), M.terms)
Id.Map.find(Piece.id(p), terms)
|> Any.ids
/* NOTE(andrew): dark_ids were originally filtered here.
* Leaving this comment in place in case issues in the
* future are traced back to here.
* |> List.filter(id => id >= 0)*/
|> List.map(id => {
let t = tile(id);
(id, t.mold, Measured.find_shards(t, M.map));
(id, t.mold, Measured.find_shards(t, map));
});
PieceDec.indicated(
~font_metrics,
~rows=M.map.rows,
~rows=map.rows,
~caret=(Piece.id(p), index),
~tiles,
range,
@@ -179,10 +175,10 @@ module Deco =
switch (Siblings.neighbors((l, r))) {
| (None, None) => failwith("impossible")
| (_, Some(p)) =>
let m = Measured.find_p(p, M.map);
let m = Measured.find_p(p, map);
Measured.{origin: m.origin, last: m.origin};
| (Some(p), _) =>
let m = Measured.find_p(p, M.map);
let m = Measured.find_p(p, map);
Measured.{origin: m.last, last: m.last};
};
let profile =
@@ -210,15 +206,11 @@ module Deco =
};

let backpack = (z: Zipper.t): list(Node.t) => [
BackpackView.view(
~font_metrics,
~origin=Zipper.caret_point(M.map, z),
z,
),
BackpackView.view(~font_metrics, ~origin=Zipper.caret_point(map, z), z),
];

let targets' = (backpack, seg) => {
M.show_backpack_targets && Backpack.restricted(backpack)
show_backpack_targets && Backpack.restricted(backpack)
? targets(backpack, seg) : [];
};

@@ -228,20 +220,20 @@ module Deco =
deco:
((Measured.Point.t, Measured.Point.t, SvgUtil.Path.t)) => Node.t,
) => {
let (p_l, p_r) = TermRanges.find(id, M.term_ranges);
let l = Measured.find_p(p_l, M.map).origin;
let r = Measured.find_p(p_r, M.map).last;
let (p_l, p_r) = TermRanges.find(id, term_ranges);
let l = Measured.find_p(p_l, map).origin;
let r = Measured.find_p(p_r, map).last;
open SvgUtil.Path;
let r_edge =
ListUtil.range(~lo=l.row, r.row + 1)
|> List.concat_map(i => {
let row = Measured.Rows.find(i, M.map.rows);
let row = Measured.Rows.find(i, map.rows);
[h(~x=i == r.row ? r.col : row.max_col), v_(~dy=1)];
});
let l_edge =
ListUtil.range(~lo=l.row, r.row + 1)
|> List.rev_map(i => {
let row = Measured.Rows.find(i, M.map.rows);
let row = Measured.Rows.find(i, map.rows);
[h(~x=i == l.row ? l.col : row.indent), v_(~dy=-1)];
})
|> List.concat;
@@ -279,16 +271,16 @@ module Deco =
};

// faster info_map traversal
let err_holes = (_z: Zipper.t) =>
List.map(term_highlight(~clss=["err-hole"]), M.error_ids);
let err_holes = error_ids =>
List.map(term_highlight(~clss=["err-hole"]), error_ids);

let next_steps = (_z: Zipper.t, ~inject) => {
let tiles = List.filter_map(TileMap.find_opt(_, M.tiles), M.next_steps);
let next_steps = (next_steps, ~inject) => {
let tiles = List.filter_map(TileMap.find_opt(_, tiles), next_steps);
List.mapi(
(i, t: Tile.t) => {
let id = Tile.id(t);
let mold = t.mold;
let shards = Measured.find_shards(t, M.map);
let shards = Measured.find_shards(t, map);
PieceDec.next_step_shards_indicated(
~font_metrics,
~caret=(Id.invalid, 0),
@@ -301,13 +293,36 @@ module Deco =
|> List.flatten;
};

let all = (zipper, sel_seg) =>
let taken_step = taken_step => {
let tiles =
List.filter_map(
TileMap.find_opt(_, tiles),
taken_step |> Option.to_list,
);
List.map(
(t: Tile.t) => {
let id = Tile.id(t);
let mold = t.mold;
let shards = Measured.find_shards(t, map);
PieceDec.taken_step_shards_indicated(
~font_metrics,
~caret=(Id.invalid, 0),
(id, mold, shards),
);
},
tiles,
)
|> List.flatten;
};

let statics = eh => err_holes(eh);

let editor = (zipper, sel_seg) =>
List.concat([
caret(zipper),
indicated_piece_deco(zipper),
selected_pieces(zipper),
backpack(zipper),
targets'(zipper.backpack, sel_seg),
err_holes(zipper),
]);
};
81 changes: 44 additions & 37 deletions src/haz3lweb/view/ExerciseMode.re
Original file line number Diff line number Diff line change
@@ -2,6 +2,8 @@ open Haz3lcore;
open Virtual_dom.Vdom;
open Node;

type model = Exercise.stitched(CellEditor.model);

type vis_marked('a) =
| InstructorOnly(unit => 'a)
| Always('a);
@@ -20,7 +22,7 @@ let render_cells = (settings: Settings.t, v: list(vis_marked(Node.t))) => {
let view =
(
~select,
~inject,
~inject_global,
~ui_state: Model.ui_state,
~selection: option((Exercise.pos, Editors.Selection.cell)),
~settings: Settings.t,
@@ -55,27 +57,53 @@ let view =
~editor: Editor.t,
~caption: string,
~subcaption: option(string)=?,
~footer=?,
~di: Exercise.DynamicsItem.t,
this_pos,
~result_kind=CellResult.View.NoResults,
this_pos: Exercise.pos,
) => {
Cell.editor_view(
CellEditor.view(
~select=s => select((this_pos, s)),
~selected=
switch (selection) {
| Some((pos, s)) when pos == this_pos => Some(s)
| _ => None
},
~error_ids=
Statics.Map.error_ids(editor.state.meta.term_ranges, di.info_map),
~inject,
~inject=
fun
| ResultAction(StepperEditorAction(_, a))
| MainEditor(a) => inject_global(UpdateAction.PerformAction(a))
| ResultAction(StepperAction(a)) =>
inject_global(
UpdateAction.StepperAction(
Exercise.key_for_statics(this_pos),
a,
),
)
| ResultAction(ToggleStepper) =>
inject_global(
UpdateAction.ToggleStepper(Exercise.key_for_statics(this_pos)),
),
~inject_global,
~ui_state,
~settings,
~highlights,
~result_kind,
~caption=Cell.caption(caption, ~rest=?subcaption),
~test_results=ModelResult.test_results(di.result),
~footer?,
editor,
{
editor: {
editor,
statics: {
term: di.term,
info_map: di.info_map,
error_ids:
Statics.Map.error_ids(
editor.state.meta.term_ranges,
di.info_map,
),
},
},
result: di.result,
},
);
};

@@ -136,7 +164,7 @@ let view =
switch (specific_ctx) {
| None => Node.div([text("No context available")]) // TODO show exercise configuration error
| Some(specific_ctx) =>
CtxInspector.ctx_view(~inject, specific_ctx)
CtxInspector.ctx_view(~inject=inject_global, specific_ctx)
};
};
};
@@ -160,13 +188,7 @@ let view =
~subcaption=": Your Tests vs. Correct Implementation",
~editor=eds.your_tests.tests,
~di=test_validation,
~footer=[
Grading.TestValidationReport.view(
~inject,
grading_report.test_validation_report,
grading_report.point_distribution.test_validation,
),
],
~result_kind=TestResults,
),
);

@@ -189,7 +211,7 @@ let view =
let mutation_testing_view =
Always(
Grading.MutationTestingReport.view(
~inject,
~inject=inject_global,
grading_report.mutation_testing_report,
grading_report.point_distribution.mutation_testing,
),
@@ -202,17 +224,7 @@ let view =
~caption="Your Implementation",
~editor=eds.your_impl,
~di=user_impl,
~footer=
Cell.footer(
~locked=false,
~settings,
~select=s => select((YourImpl, s)),
~inject,
~ui_state,
~selected=None,
~result=user_impl.result,
~result_key=Exercise.user_impl_key,
),
~result_kind=EvalResults,
),
);
};
@@ -229,12 +241,7 @@ let view =
": Your Tests (code synchronized with Test Validation cell above) vs. Your Implementation",
~editor=eds.your_tests.tests,
~di=user_tests,
~footer=[
Cell.test_report_footer_view(
~inject,
~test_results=ModelResult.test_results(user_tests.result),
),
],
~result_kind=TestResults,
),
);

@@ -252,7 +259,7 @@ let view =
let impl_grading_view =
Always(
Grading.ImplGradingReport.view(
~inject,
~inject=inject_global,
~report=grading_report.impl_grading_report,
~syntax_report=grading_report.syntax_report,
~max_points=grading_report.point_distribution.impl_grading,
89 changes: 65 additions & 24 deletions src/haz3lweb/view/ExplainThis.re
Original file line number Diff line number Diff line change
@@ -209,21 +209,16 @@ let expander_deco =
~docs: ExplainThisModel.t,
~settings: Settings.t,
~inject,
~ui_state as {font_metrics, _}: Model.ui_state,
~ui_state as {font_metrics, _} as ui_state: Model.ui_state,
~options: list((ExplainThisForm.form_id, Segment.t)),
~group: ExplainThisForm.group,
~doc: ExplainThisForm.form,
editor,
) => {
module Deco =
Deco.Deco({
let font_metrics = font_metrics;
let map = Measured.of_segment(doc.syntactic_form);
let show_backpack_targets = false;
let (_term, terms) = MakeTerm.go(doc.syntactic_form);
let term_ranges = TermRanges.mk(doc.syntactic_form);
let tiles = TileMap.mk(doc.syntactic_form);
let error_ids = [];
let next_steps = [];
let editor = editor;
let ui_state = ui_state;
});
switch (doc.expandable_id, List.length(options)) {
| (None, _)
@@ -331,7 +326,6 @@ let expander_deco =

let example_view =
(
~select,
~inject,
~ui_state,
~settings: Settings.t,
@@ -346,7 +340,7 @@ let example_view =
div(
~attr=Attr.id("examples"),
List.mapi(
(idx, {term, message, sub_id, _}: ExplainThisForm.example) => {
(_, {term, message, sub_id, _}: ExplainThisForm.example) => {
let feedback =
settings.explainThis.show_feedback
? [
@@ -362,13 +356,49 @@ let example_view =
div(
~attr=clss(["example"]),
[
Cell.locked(
~segment=term,
~target_id="example" ++ string_of_int(idx),
CellEditor.view(
~select=_ => Ui_effect.Ignore,
~inject=_ => Ui_effect.Ignore,
~inject_global=_ => Ui_effect.Ignore,
~ui_state,
~settings,
~select,
~inject,
~highlights=None,
~selected=None,
~caption=None,
~locked=true,
{
let editor =
Editor.init(~read_only=true, Zipper.unzip(term));
let (term, _) =
MakeTerm.from_zip_for_sem(editor.state.zipper);
let statics =
CachedStatics.statics_of_term(
~settings=settings.core,
term,
editor,
);
let result: ModelResult.t =
settings.core.dynamics
? Evaluation({
elab: {
d: term,
},
evaluation:
Interface.evaluate(
~settings=settings.core,
term,
),
previous: ResultPending,
})
: NoElab;
{
editor: {
editor,
statics,
},
result,
};
},
),
div(
~attr=clss(["explanation"]),
@@ -474,6 +504,8 @@ let get_doc =
|> List.to_seq
|> Id.Map.of_seq
|> Option.some;
let editor =
Editor.init(~read_only=true, doc.syntactic_form |> Zipper.unzip);
let expander_deco =
expander_deco(
~docs,
@@ -483,21 +515,30 @@ let get_doc =
~options,
~group,
~doc,
editor,
);
let highlight_deco =
switch (highlights) {
| Some(highlights) =>
module Deco =
Deco.Deco({
let editor = editor;
let ui_state = ui_state;
});
Deco.color_highlights(ColorSteps.to_list(highlights));
| None => []
};
let statics = CachedStatics.empty_statics;
let syntactic_form_view =
Cell.locked_no_statics(
~select=_ => Ui_effect.Ignore,
~inject,
ReadOnlyEditor.view(
~ui_state,
~segment=doc.syntactic_form,
~highlights,
~settings,
~overlays=highlight_deco @ [expander_deco],
~sort,
~expander_deco,
{editor, statics},
);
let example_view =
example_view(
~select=_ => Ui_effect.Ignore,
~inject,
~ui_state,
~settings,
@@ -506,7 +547,7 @@ let get_doc =
~examples=doc.examples,
~model=docs,
);
(syntactic_form_view, ([explanation], color_map), example_view);
([syntactic_form_view], ([explanation], color_map), example_view);
| Colorings =>
let (_, color_map) = mk_translation(~inject=None, explanation_msg);
([], ([], color_map), []);
7 changes: 6 additions & 1 deletion src/haz3lweb/view/Page.re
Original file line number Diff line number Diff line change
@@ -65,6 +65,11 @@ let main_view =
~inject: UpdateAction.t => Ui_effect.t(unit),
{settings, editors, explainThisModel, results, statics, ui_state, _}: Model.t,
) => {
let _ =
switch (ui_state.active_editor) {
| Some(ae) => print_endline("SELECTED: " ++ Editors.Selection.show(ae))
| None => print_endline("NO ACTIVE EDITOR")
};
let cursor_info =
Editors.get_cursor_info(
~selection=ui_state.active_editor,
@@ -160,7 +165,7 @@ let main_view =
inject(
UpdateAction.MakeActive(Editors.Selection.Exercises(pos, sel)),
),
~inject,
~inject_global=inject,
~ui_state,
~settings,
~selection,
51 changes: 21 additions & 30 deletions src/haz3lweb/view/ScratchMode.re
Original file line number Diff line number Diff line change
@@ -3,50 +3,41 @@ open Haz3lcore;
let view =
(
~select,
~inject,
~inject: UpdateAction.t => Ui_effect.t(unit),
~ui_state: Model.ui_state,
~settings: Settings.t,
~highlights,
~results: ModelResults.t,
~result_key,
~statics as {error_ids, _}: CachedStatics.statics,
~statics: CachedStatics.statics,
~selected,
editor: Editor.t,
) => {
let result = ModelResults.lookup(results, result_key);
let test_results = Util.OptUtil.and_then(ModelResult.test_results, result);
let footer =
settings.core.elaborate || settings.core.dynamics
? result
|> Option.map(result =>
Cell.footer(
~locked=false,
~settings,
~select,
~inject,
~ui_state,
~result,
~selected=
switch (selected) {
| Some(Editors.Selection.Result(i)) => Some(i)
| _ => None
},
~result_key,
)
)
: None;
let result = ModelResults.lookup(results, result_key) |> Option.get;
[
Cell.editor_view(
CellEditor.view(
~select,
~inject,
~inject=
fun
| MainEditor(a) => inject(PerformAction(a))
| ResultAction(StepperAction(a)) =>
inject(StepperAction(result_key, a))
| ResultAction(ToggleStepper) => inject(ToggleStepper(result_key))
| ResultAction(StepperEditorAction(_, a)) =>
inject(PerformAction(a)),
~inject_global=inject,
~ui_state,
~settings,
~error_ids,
~test_results,
~footer?,
~highlights,
~selected,
editor,
~locked=false,
{
editor: {
editor,
statics,
},
result,
},
),
];
};
38 changes: 37 additions & 1 deletion src/haz3lweb/view/dec/PieceDec.re
Original file line number Diff line number Diff line change
@@ -128,7 +128,12 @@ let next_step_indicated =
~shapes,
~path_cls,
~base_cls,
~attr=[Attr.on_mousedown(_ => {inject()})],
~attr=[
Attr.on_mousedown(_ => {
print_endline("CLICK!");
inject();
}),
],
measurement,
);
};
@@ -154,6 +159,37 @@ let next_step_shards_indicated =
shards,
);

let taken_step_indicated =
(
~font_metrics,
~has_caret,
~shapes,
~sort,
~measurement: Measured.measurement,
)
: t => {
let path_cls =
["tile-path", "raised", Sort.to_string(sort)]
@ (has_caret ? ["indicated-caret"] : ["indicated"]);
let base_cls = ["tile-taken-step"];
simple_shard(~font_metrics, ~shapes, ~path_cls, ~base_cls, measurement);
};

let taken_step_shards_indicated =
(~font_metrics: FontMetrics.t, ~caret: (Id.t, int), (id, mold, shards))
: list(t) =>
List.map(
((index, measurement)) =>
taken_step_indicated(
~font_metrics,
~has_caret=caret == (id, index),
~shapes=Mold.nib_shapes(~index, mold),
~sort=mold.out,
~measurement,
),
shards,
);

let shadowfudge = Path.cmdfudge(~y=DecUtil.shadow_adj);

let shards_of_tiles = tiles =>
45 changes: 45 additions & 0 deletions src/haz3lweb/view/editor/Cell.re
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
open Haz3lcore;
open Virtual_dom.Vdom;
open Node;

let narrative_cell = (content: Node.t) =>
div(
~attr=Attr.class_("cell"),
[div(~attr=Attr.class_("cell-chapter"), [content])],
);

let simple_cell_item = (content: list(Node.t)) =>
div(~attr=Attr.classes(["cell-item"]), content);

let caption = (~rest: option(string)=?, bolded: string) =>
div(
~attr=Attr.many([Attr.classes(["cell-caption"])]),
[strong([text(bolded)])] @ (rest |> Option.map(text) |> Option.to_list),
);

let simple_cell_view = (items: list(t)) =>
div(~attr=Attr.class_("cell"), items);

let report_footer_view = content => {
div(~attr=Attr.classes(["cell-item", "cell-report"]), content);
};

let test_report_footer_view = (~inject, ~test_results: option(TestResults.t)) => {
report_footer_view([TestView.test_summary(~inject, ~test_results)]);
};

let panel = (~classes=[], content, ~footer: option(t)) => {
simple_cell_view(
[div(~attr=Attr.classes(["cell-item", "panel"] @ classes), content)]
@ Option.to_list(footer),
);
};

let title_cell = title => {
simple_cell_view([
div(
~attr=Attr.class_("title-cell"),
[div(~attr=Attr.class_("title-text"), [text(title)])],
),
]);
};
83 changes: 83 additions & 0 deletions src/haz3lweb/view/editor/CellEditor.re
Original file line number Diff line number Diff line change
@@ -0,0 +1,83 @@
open Haz3lcore;
open Virtual_dom.Vdom;
open Node;

type model = {
editor: CodeEditor.model,
result: ModelResult.t,
};

type action =
| MainEditor(CodeEditor.action)
| ResultAction(CellResult.action);

let update = ReadOnlyEditor.update;

let calculate = ReadOnlyEditor.calculate;

type event = CodeEditor.event;

let view =
(
~select: Editors.Selection.cell => Ui_effect.t(unit),
~inject,
~inject_global,
~ui_state: Model.ui_state,
~settings: Settings.t,
~highlights: option(ColorSteps.colorMap),
~selected: option(Editors.Selection.cell),
~caption: option(Node.t)=?,
~sort=?,
~result_kind=?,
~locked=false,
model,
) => {
let (footer, overlays) =
CellResult.view(
~signal=
fun
| MakeActive(a) => select(a)
| MouseUp => inject_global(Update.SetMeta(Mouseup))
| MouseDown => inject_global(Update.SetMeta(Mousedown)),
~inject=a => inject(ResultAction(a)),
~inject_global,
~ui_state,
~settings,
~selected=selected == Some(Result(0)),
~result_kind?,
~locked,
model.result,
);
div(
~attr=
Attr.classes([
"cell",
Option.is_some(selected) ? "selected" : "deselected",
locked ? "locked" : "unlocked",
]),
Option.to_list(caption)
@ [
CodeEditor.view(
~signal=
locked
? _ => Ui_effect.Ignore
: fun
| MouseUp => inject_global(Update.SetMeta(Mouseup))
| MouseDown => inject_global(Update.SetMeta(Mousedown))
| MakeActive => select(Editors.Selection.MainEditor),
~inject=
locked
? _ => Ui_effect.Ignore
: (action => inject_global(PerformAction(action))),
~ui_state,
~settings,
~selected=selected == Some(MainEditor),
~highlights,
~overlays=overlays(model.editor.editor),
~sort?,
model.editor,
),
]
@ footer,
);
};
435 changes: 435 additions & 0 deletions src/haz3lweb/view/editor/CellResult.re

Large diffs are not rendered by default.

149 changes: 149 additions & 0 deletions src/haz3lweb/view/editor/CodeEditor.re
Original file line number Diff line number Diff line change
@@ -0,0 +1,149 @@
open Js_of_ocaml;
open Haz3lcore;
open Virtual_dom.Vdom;
type editor_id = string;

type model = ReadOnlyEditor.model;

type action = ReadOnlyEditor.action;

let update = ReadOnlyEditor.update;

let calculate = ReadOnlyEditor.calculate;

type event =
| MakeActive
| MouseUp
| MouseDown;

module View = {
let get_goal =
(
~font_metrics: FontMetrics.t,
text_box: Js.t(Dom_html.element),
e: Js.t(Dom_html.mouseEvent),
) => {
let rect = text_box##getBoundingClientRect;
let goal_x = float_of_int(e##.clientX);
let goal_y = float_of_int(e##.clientY);
Measured.Point.{
row: Float.to_int((goal_y -. rect##.top) /. font_metrics.row_height),
col:
Float.(
to_int(round((goal_x -. rect##.left) /. font_metrics.col_width))
),
};
};

let mousedown_overlay = (~signal, ~inject, ~font_metrics) =>
Node.div(
~attr=
Attr.many(
Attr.[
id("mousedown-overlay"),
on_mouseup(_ => signal(MouseUp)),
on_mousemove(e => {
let mouse_handler =
e##.target |> Js.Opt.get(_, _ => failwith("no target"));
let text_box =
JsUtil.get_child_with_class(
mouse_handler##.parentNode
|> Js.Opt.get(_, _ => failwith(""))
|> Js.Unsafe.coerce,
"code-container",
)
|> Option.get;
let goal = get_goal(~font_metrics, text_box, e);
inject(Action.Select(Resize(Goal(Point(goal)))));
}),
],
),
[],
);

let mousedown_handler = (~signal, ~inject, ~font_metrics, evt) => {
let goal =
get_goal(
~font_metrics,
evt##.currentTarget
|> Js.Opt.get(_, _ => failwith(""))
|> JsUtil.get_child_with_class(_, "code-container")
|> Option.get,
evt,
);
switch (JsUtil.ctrl_held(evt), JsUtil.num_clicks(evt)) {
| (true, _) =>
Effect.Many([
signal(MakeActive),
inject(Action.Move(Goal(Point(goal)))),
inject(Action.Jump(BindingSiteOfIndicatedVar)),
])
| (false, 1) =>
Effect.Many([
signal(MouseDown),
signal(MakeActive),
inject(Action.Move(Goal(Point(goal)))),
])
| (false, 2) => inject(Action.Select(Tile(Current)))
| (false, 3 | _) => inject(Action.Select(Smart))
};
};

let view =
(
~signal: event => Ui_effect.t(unit),
~inject: action => Ui_effect.t(unit),
~ui_state: Model.ui_state,
~settings: Settings.t,
~selected: bool,
~highlights: option(ColorSteps.colorMap),
~overlays: list(Node.t)=[],
~sort=?,
model: model,
) => {
let edit_decos = {
module Deco =
Deco.Deco({
let editor = model.editor;
let ui_state = ui_state;
});
Deco.editor(model.editor.state.zipper, model.editor.state.meta.segment)
@ (
switch (highlights) {
| Some(colorMap) =>
Deco.color_highlights(ColorSteps.to_list(colorMap))
| _ => []
}
);
};
let overlays = edit_decos @ overlays;
let code_view =
ReadOnlyEditor.view(~ui_state, ~settings, ~overlays, ~sort?, model);
let mousedown_overlay =
selected && ui_state.mousedown
? [
mousedown_overlay(
~signal,
~inject,
~font_metrics=ui_state.font_metrics,
),
]
: [];
let on_mousedown =
mousedown_handler(
~signal,
~inject,
~font_metrics=ui_state.font_metrics,
);
Node.div(
~attr=
Attr.many([
Attr.classes(["cell-item"]),
Attr.on_mousedown(on_mousedown),
]),
mousedown_overlay @ [code_view],
);
};
};

let view = View.view;
64 changes: 64 additions & 0 deletions src/haz3lweb/view/editor/ReadOnlyEditor.re
Original file line number Diff line number Diff line change
@@ -0,0 +1,64 @@
open Virtual_dom.Vdom;
open Util.Result.Syntax;
open Haz3lcore;

type model = {
// Update:
editor: Editor.t,
// Calculate:
statics: CachedStatics.statics,
};

type action = Action.t;

let update = (~settings, action, model) => {
let+ editor = Perform.go(~settings, action, model.editor);
{editor, statics: model.statics};
};

let calculate = (~settings, ~stitch, {editor, statics} as model) => {
let term = MakeTerm.from_zip_for_sem(editor.state.zipper) |> fst |> stitch;
if (Exp.fast_equal(term, statics.term)) {
model;
} else {
{
editor,
statics: CachedStatics.statics_of_term(~settings, term, editor),
};
};
};

// There are no events for a read-only editor
type event;

// read-only editors cannot be selected
type selection;

let view =
(
~ui_state: Model.ui_state,
~settings,
~overlays: list(Node.t)=[],
~sort=Sort.root,
model: model,
) => {
let code_text_view =
Code.view(
~sort,
~font_metrics=ui_state.font_metrics,
~settings,
model.editor,
);
let statics_decos = {
module Deco =
Deco.Deco({
let ui_state = ui_state;
let editor = model.editor;
});
Deco.statics(model.statics.error_ids);
};
Node.div(
~attr=Attr.many([Attr.classes(["code-container"])]),
[code_text_view] @ statics_decos @ overlays,
);
};
60 changes: 60 additions & 0 deletions src/haz3lweb/view/editor/StepperEditor.re
Original file line number Diff line number Diff line change
@@ -0,0 +1,60 @@
open Haz3lcore;

module Stepped = {
type model = {
editor: ReadOnlyEditor.model,
step: EvaluatorStep.step,
step_id: Id.t,
};

type action = ReadOnlyEditor.action;

type event = ReadOnlyEditor.event;

type selection = ReadOnlyEditor.selection;

let view =
(~ui_state: Model.ui_state, ~settings, ~overlays=[], model: model) => {
let overlays = {
module Deco =
Deco.Deco({
let editor = model.editor.editor;
let ui_state = ui_state;
});
overlays @ Deco.taken_step(Some(model.step_id));
};
ReadOnlyEditor.view(~ui_state, ~settings, ~overlays, model.editor);
};
};

module Steppable = {
type model = {
editor: CodeEditor.model,
next_steps: list(Id.t),
};

type action = CodeEditor.action;

type event =
| TakeStep(int);

let view =
(
~signal: event => Ui_effect.t(unit),
~ui_state: Model.ui_state,
~settings,
~overlays=[],
model: model,
) => {
let overlays = {
module Deco =
Deco.Deco({
let editor = model.editor.editor;
let ui_state = ui_state;
});
overlays
@ Deco.next_steps(model.next_steps, ~inject=x => signal(TakeStep(x)));
};
ReadOnlyEditor.view(~ui_state, ~settings, ~overlays, model.editor);
};
};

0 comments on commit 5fb83bc

Please sign in to comment.