From 2e1299f7ece1937be18a17f3233bf91326f78815 Mon Sep 17 00:00:00 2001 From: disconcision Date: Sat, 18 May 2024 00:50:41 -0400 Subject: [PATCH] principled editor meta for projectors --- src/haz3lcore/Measured.re | 25 +--- src/haz3lcore/zipper/Editor.re | 138 ++++++++---------- src/haz3lcore/zipper/Printer.re | 52 ++----- src/haz3lcore/zipper/Zipper.re | 47 +++--- src/haz3lcore/zipper/action/Move.re | 12 +- .../zipper/action/ProjectorAction.re | 21 +-- src/haz3lcore/zipper/action/Select.re | 7 +- src/haz3lschool/Exercise.re | 2 +- src/haz3lweb/ScratchSlide.re | 2 +- src/haz3lweb/view/Cell.re | 20 +-- src/haz3lweb/view/Code.re | 9 +- src/haz3lweb/view/ExerciseMode.re | 5 +- .../view/assistant/UpdateAssistant.re | 3 +- 13 files changed, 134 insertions(+), 209 deletions(-) diff --git a/src/haz3lcore/Measured.re b/src/haz3lcore/Measured.re index bf84e425ed..0b849ac195 100644 --- a/src/haz3lcore/Measured.re +++ b/src/haz3lcore/Measured.re @@ -199,35 +199,18 @@ let find_t = (t: Tile.t, map): measurement => { let last = ListUtil.assoc_err(Tile.r_shard(t), shards, "find_t"); (first, last); }) { - | _ => - print_endline("FuCkNASTY hackzz"); - let s = shards |> List.hd; - (s |> snd, s |> snd); + | _ => failwith("find_t: inconsistent shard infor between tile and map") + // let s = shards |> List.hd; + // (s |> snd, s |> snd); }; {origin: first.origin, last: last.last}; }; -// let find_a = ({shards: (l, r), _} as a: Ancestor.t, map) => -// List.assoc(l @ r, Id.Map.find(a.id, map.tiles)); let find_p = (~msg="", p: Piece.t, map): measurement => try( p |> Piece.get( w => find_w(w, map), - g => - //TODO(andrew): find better way to reconcile this - try(find_g(g, map)) { - | _ => - find_t( - { - id: g.id, - label: [String.make(2, ' ')], - mold: Mold.mk_op(Any, []), - shards: [0], - children: [], - }, - map, - ) - }, + g => find_g(g, map), t => find_t(t, map), ) ) { diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/zipper/Editor.re index b72353f632..86387a6d31 100644 --- a/src/haz3lcore/zipper/Editor.re +++ b/src/haz3lcore/zipper/Editor.re @@ -2,15 +2,12 @@ open Sexplib.Std; open Util; module Meta = { - type t = { - col_target: int, - touched: Touched.t, - segment_real: Segment.t, - measured_real: Measured.t, - z_projected: Zipper.t, - segment_projected: Segment.t, - measured_projected: Measured.t, - term_projected: Term.UExp.t, + /* Derived data for projected zipper */ + type projected = { + z: Zipper.t, + segment: Segment.t, + measured: Measured.t, + term: Term.UExp.t, term_ranges: TermRanges.t, terms: TermMap.t, tiles: TileMap.t, @@ -18,34 +15,39 @@ module Meta = { buffer_ids: list(Id.t), }; + type t = { + col_target: int, + touched: Touched.t, + projected, + }; + + let init_projected = (z_projected: Zipper.t): projected => { + let segment = Zipper.unselect_and_zip(z_projected); + let (term, terms) = MakeTerm.go(segment); + { + z: z_projected, + segment, + term, + terms, + term_ranges: TermRanges.mk(segment), + tiles: TileMap.mk(segment), + holes: Segment.holes(segment), + measured: Measured.of_segment(segment), + buffer_ids: Selection.buffer_ids(z_projected.selection), + }; + }; + let init = (z: Zipper.t) => { - let segment_real = Zipper.unselect_and_zip(z); - let measured_real = Measured.of_segment(segment_real); - let is_proj = !Id.Map.is_empty(z.projectors); - let z_projected = is_proj ? ProjectorAction.of_zipper(z) : z; - let segment_projected = - is_proj ? Zipper.unselect_and_zip(z_projected) : segment_real; - let (term_projected, terms) = MakeTerm.go(segment_projected); { col_target: 0, touched: Touched.empty, - z_projected, - segment_real, - measured_real, - measured_projected: Measured.of_segment(segment_projected), - segment_projected, - term_ranges: TermRanges.mk(segment_projected), - tiles: TileMap.mk(segment_projected), - term_projected, - terms, - holes: Segment.holes(segment_projected), - buffer_ids: Selection.buffer_ids(z.selection), + projected: z |> ProjectorAction.of_zipper |> init_projected, }; }; module type S = { let touched: Touched.t; - let measured_projected: Measured.t; + let measured: Measured.t; let term_ranges: TermRanges.t; let col_target: int; }; @@ -53,8 +55,8 @@ module Meta = { (module { let touched = m.touched; - let measured_projected = m.measured_projected; - let term_ranges = m.term_ranges; + let measured = m.projected.measured; + let term_ranges = m.projected.term_ranges; let col_target = m.col_target; }); @@ -64,58 +66,40 @@ module Meta = { let yojson_of_t = _ => failwith("Editor.Meta.yojson_of_t"); let t_of_yojson = _ => failwith("Editor.Meta.t_of_yojson"); + let next_projected = (z, ~touched, ~old) => { + let segment = Zipper.unselect_and_zip(z); + let (term, terms) = MakeTerm.go(segment); + let measured = Measured.of_segment(~touched, ~old, segment); + { + z, + segment, + term, + terms, + measured, + term_ranges: TermRanges.mk(segment), + tiles: TileMap.mk(segment), + holes: Segment.holes(segment), + buffer_ids: Selection.buffer_ids(z.selection), + }; + }; + let next = (~effects: list(Effect.t)=[], a: Action.t, z: Zipper.t, meta: t): t => { - let {touched, measured_real, measured_projected, col_target, _} = meta; - let touched = Touched.update(Time.tick(), effects, touched); - //TODO(andrew): gate appropriate things on edit - let is_edit = Action.is_edit(a); - let is_proj = !Id.Map.is_empty(z.projectors); - let segment_real = - is_edit ? Zipper.unselect_and_zip(z) : meta.segment_real; - let measured_real = - Measured.of_segment(~touched, ~old=measured_real, segment_real); - let z_projected = is_proj ? ProjectorAction.of_zipper(z) : z; - let segment_projected = - is_proj - ? Projector.of_segment(z.projectors, segment_real) : segment_real; - let measured_projected = - is_proj - ? Measured.of_segment( - ~touched, - ~old=measured_projected, - segment_projected, - ) - : measured_real; - let term_ranges = - is_edit ? TermRanges.mk(segment_projected) : meta.term_ranges; + let touched = Touched.update(Time.tick(), effects, meta.touched); let col_target = switch (a) { | Move(Local(Up | Down)) - | Select(Resize(Local(Up | Down))) => col_target + | Select(Resize(Local(Up | Down))) => meta.col_target + | _ => Zipper.caret_point(meta.projected.measured, meta.projected.z).col + }; + let z_projected = ProjectorAction.of_zipper(z); + let projected = + switch (Action.is_edit(a)) { + | false => {...meta.projected, z: z_projected} | _ => - print_endline("Editor.next.caret_point"); - Zipper.caret_point(measured_projected, z_projected).col; + next_projected(z_projected, ~touched, ~old=meta.projected.measured) }; - let (term_projected, terms) = - is_edit - ? MakeTerm.go(segment_projected) : (meta.term_projected, meta.terms); - { - col_target, - touched, - z_projected, - measured_real, - measured_projected, - segment_real, - segment_projected, - term_ranges, - tiles: is_edit ? TileMap.mk(segment_projected) : meta.tiles, - term_projected, - terms, - //NOTE(andrew): this is seg_project bc otherwise Code.of_hole crashes - holes: is_edit ? Segment.holes(segment_projected) : meta.holes, - buffer_ids: Selection.buffer_ids(z.selection), - }; + {touched, col_target, projected}; }; }; @@ -240,10 +224,10 @@ let map_projectors = (f: (Id.t, Projector.t) => Projector.t, ed: t) => let get_projected_piece = (ed: t, id: Id.t): option(Piece.t) => { /* Assumes for the moment that the projected thing is either * a tile or a grout (not secondary or segment) */ - switch (Id.Map.find_opt(id, ed.state.meta.tiles)) { + switch (Id.Map.find_opt(id, ed.state.meta.projected.tiles)) { | Some(tile) => Some(Tile(tile)) | None => - List.find_opt((g: Grout.t) => g.id == id, ed.state.meta.holes) + List.find_opt((g: Grout.t) => g.id == id, ed.state.meta.projected.holes) |> Option.map(g => Piece.Grout(g)) }; }; diff --git a/src/haz3lcore/zipper/Printer.re b/src/haz3lcore/zipper/Printer.re index 5614c2ff86..a96108a219 100644 --- a/src/haz3lcore/zipper/Printer.re +++ b/src/haz3lcore/zipper/Printer.re @@ -60,9 +60,11 @@ let to_rows = }; }; -let pretty_print = (~measured: Measured.t, z: Zipper.t): string => +let pretty_print = + (~holes: option(string)=Some(""), ~measured: Measured.t, z: Zipper.t) + : string => to_rows( - ~holes=None, + ~holes, ~measured, ~caret=None, ~indent=" ", @@ -70,20 +72,24 @@ let pretty_print = (~measured: Measured.t, z: Zipper.t): string => ) |> String.concat("\n"); -let to_string_editor = - (~holes: option(string)=Some(""), editor: Editor.t): string => +let zipper_to_string = + (~holes: option(string)=Some(""), z: Zipper.t): string => to_rows( ~holes, - ~measured=editor.state.meta.measured_real, + ~measured=Zipper.measured(z), ~caret=None, ~indent="", - ~segment=seg_of_zip(editor.state.zipper), + ~segment=seg_of_zip(z), ) |> String.concat("\n"); +let to_string_editor = + (~holes: option(string)=Some(""), editor: Editor.t): string => + zipper_to_string(~holes, editor.state.zipper); + let to_string_selection = (editor: Editor.t): string => to_rows( - ~measured=editor.state.meta.measured_real, + ~measured=Zipper.measured(editor.state.zipper), ~caret=None, ~indent=" ", ~holes=None, @@ -91,38 +97,6 @@ let to_string_selection = (editor: Editor.t): string => ) |> String.concat("\n"); -let to_log = (~measured: Measured.t, z: Zipper.t): t => { - code: - to_rows( - ~holes=None, - ~measured, - ~caret=Some(Zipper.caret_point(measured, z)), - ~indent=" ", - ~segment=seg_of_zip(z), - ), - selection: z.selection.content |> of_segment(~holes=None) |> lines_to_list, - backpack: - List.map( - (s: Selection.t) => - s.content |> of_segment(~holes=None) |> lines_to_list, - z.backpack, - ), -}; - -let to_log_flat = (~measured, z: Zipper.t): string => { - let {code, selection, backpack} = to_log(~measured, z); - Printf.sprintf( - "CODE:\n%s\nSELECTION:\n%s\n%s\n", - String.concat("\n", code), - String.concat("\n", selection), - backpack - |> List.mapi((i, b) => - Printf.sprintf("BP(%d):\n %s\n", i, String.concat("\n", b)) - ) - |> String.concat(""), - ); -}; - let zipper_of_string = (~zipper_init=Zipper.init(), str: string): option(Zipper.t) => { let insert = (z: option(Zipper.t), c: string): option(Zipper.t) => { diff --git a/src/haz3lcore/zipper/Zipper.re b/src/haz3lcore/zipper/Zipper.re index db89a3fc71..8f01ce414d 100644 --- a/src/haz3lcore/zipper/Zipper.re +++ b/src/haz3lcore/zipper/Zipper.re @@ -317,30 +317,6 @@ let move = (d: Direction.t, z: t): option(t) => let select = (d: Direction.t, z: t): option(t) => d == z.selection.focus ? grow_selection(z) : shrink_selection(z); -// let id_on = (d: Direction.t, id: Id.t, z: t): bool => -// switch (d) { -// | Left => -// switch (z.relatives.siblings, z.relatives.ancestors) { -// | (([_, ..._] as ls, _), _) => Piece.id(ListUtil.last(ls)) == id -// | _ => false -// } -// | Right => -// switch (z.relatives.siblings, z.relatives.ancestors) { -// | ((_, [r, ..._]), _) => Piece.id(r) == id -// | _ => false -// } -// }; - -/* Loop action until pred is satisfied */ -// let rec do_until = -// (action: t => option(t), pred: t => bool, z: t): option(t) => -// pred(z) -// ? Some(z) -// : { -// let* z = action(z); -// do_until(action, pred, z); -// }; - let pick_up = (z: t): t => { let (selected, z) = update_selection(Selection.empty, z); let selection = @@ -468,9 +444,32 @@ let caret_direction = (z: t): option(Direction.t) => } }; +let get_projector = (z: t, id: Id.t): option(Projector.t) => + Projector.Map.find(id, z.projectors); + +let measured = z => { + z |> unselect_and_zip |> Measured.of_segment; +}; + let base_point = (measured: Measured.t, z: t): Measured.Point.t => { switch (representative_piece(z)) { | Some((p, d)) => + /* NOTE(andrew): Below conversion necessary because sometimes + * we call this with measured based on projected zipper + * measurements but also z is the non-projected zipper. + * This should work okay since the core movement/selection + * actions in Zipper avoid cursor positions around pieces + * which would be absent in the projected zipper. The problem + * is the projected tile itself. Specifically because looking + * up measurements is not currently homogenous; it takes a + * piece, not an id. Piece-based lookups will fail if (say) + * a Grout becomes a Tile. Hence we convert pieces that + * would be projected to their placeholders before lookup */ + let p = + switch (get_projector(z, Piece.id(p))) { + | Some(pr) => Projector.placeholder(pr, Piece.id(p)) + | None => p + }; let seg = Piece.disassemble(p); switch (d) { | Left => diff --git a/src/haz3lcore/zipper/action/Move.re b/src/haz3lcore/zipper/action/Move.re index aa327631e4..fe16b5fb05 100644 --- a/src/haz3lcore/zipper/action/Move.re +++ b/src/haz3lcore/zipper/action/Move.re @@ -61,15 +61,7 @@ let neighbor_movability = }; module Make = (M: Editor.Meta.S) => { - let caret_point = t => { - // print_endline("Move.caret_point"); - Zipper.caret_point( - M.measured_projected, - //TODO(andrew): why real here? if use projected, - // get caret point errs but only for grout not tiles - t, - ); - }; + let caret_point = t => Zipper.caret_point(M.measured, t); let pop_out = z => Some(z |> Zipper.set_caret(Outer)); let pop_move = (d, z) => z |> Zipper.set_caret(Outer) |> Zipper.move(d); @@ -238,7 +230,7 @@ module Make = (M: Editor.Meta.S) => { }; let jump_to_id = (z: t, id: Id.t): option(t) => { - let* {origin, _} = Measured.find_by_id(id, M.measured_projected); + let* {origin, _} = Measured.find_by_id(id, M.measured); let z = switch (to_start(z)) { | None => z diff --git a/src/haz3lcore/zipper/action/ProjectorAction.re b/src/haz3lcore/zipper/action/ProjectorAction.re index 7ec201d34e..2a018f9f5b 100644 --- a/src/haz3lcore/zipper/action/ProjectorAction.re +++ b/src/haz3lcore/zipper/action/ProjectorAction.re @@ -37,16 +37,19 @@ let of_selection = }; }; -let of_zipper = (z: Zipper.t): Zipper.t => { - { - ...z, - selection: of_selection(z.projectors, z.selection), - relatives: { - ancestors: of_ancestors(z.projectors, z.relatives.ancestors), - siblings: of_siblings(z.projectors, z.relatives.siblings), - }, +let of_zipper = (z: Zipper.t): Zipper.t => + if (Id.Map.is_empty(z.projectors)) { + z; + } else { + { + ...z, + selection: of_selection(z.projectors, z.selection), + relatives: { + ancestors: of_ancestors(z.projectors, z.relatives.ancestors), + siblings: of_siblings(z.projectors, z.relatives.siblings), + }, + }; }; -}; let move_out_of_piece = (d: Util.Direction.t, rel: Indicated.relation, z: Zipper.t): Zipper.t => diff --git a/src/haz3lcore/zipper/action/Select.re b/src/haz3lcore/zipper/action/Select.re index 4eff98afdf..b905e0cb02 100644 --- a/src/haz3lcore/zipper/action/Select.re +++ b/src/haz3lcore/zipper/action/Select.re @@ -22,7 +22,7 @@ module Make = (M: Editor.Meta.S) => { let range = (l: Id.t, r: Id.t, z: Zipper.t): option(Zipper.t) => { let* z = Move.jump_to_id(z, l); print_endline("Select.range: first"); - let* Measured.{last, _} = Measured.find_by_id(r, M.measured_projected); + let* Measured.{last, _} = Measured.find_by_id(r, M.measured); print_endline("Select.range: last"); Move.do_towards(Zipper.select, last, z); }; @@ -41,7 +41,7 @@ module Make = (M: Editor.Meta.S) => { let tile = (id: Id.t, z: Zipper.t): option(Zipper.t) => { let* z = Move.jump_to_id(z, id); - let* Measured.{last, _} = Measured.find_by_id(id, M.measured_projected); + let* Measured.{last, _} = Measured.find_by_id(id, M.measured); Move.do_towards(primary, last, z); }; @@ -49,8 +49,7 @@ module Make = (M: Editor.Meta.S) => { switch (d) { | Goal(Piece(_)) => failwith("Select.go not implemented for Piece Goal") | Goal(Point(goal)) => - let anchor = - z |> Zipper.toggle_focus |> Zipper.caret_point(M.measured_projected); + let anchor = z |> Zipper.toggle_focus |> Zipper.caret_point(M.measured); Move.do_towards(~anchor, primary, goal, z); | Extreme(d) => Move.do_extreme(primary, d, z) | Local(d) => diff --git a/src/haz3lschool/Exercise.re b/src/haz3lschool/Exercise.re index b9f6165ace..ed0ab06529 100644 --- a/src/haz3lschool/Exercise.re +++ b/src/haz3lschool/Exercise.re @@ -588,7 +588,7 @@ module F = (ExerciseEnv: ExerciseEnv) => { let wrap = (term, editor: Editor.t): TermItem.t => { term, - term_ranges: editor.state.meta.term_ranges, + term_ranges: editor.state.meta.projected.term_ranges, }; let term_of = (editor: Editor.t): Term.UExp.t => diff --git a/src/haz3lweb/ScratchSlide.re b/src/haz3lweb/ScratchSlide.re index 09860711ed..0c346aaa7b 100644 --- a/src/haz3lweb/ScratchSlide.re +++ b/src/haz3lweb/ScratchSlide.re @@ -51,6 +51,6 @@ let mk_statics = let term = MakeTerm.from_zip_for_sem(editor.state.zipper) |> fst; let info_map = Interface.Statics.mk_map_ctx(settings.core, ctx_init, term); let error_ids = - Statics.Map.error_ids(editor.state.meta.term_ranges, info_map); + Statics.Map.error_ids(editor.state.meta.projected.term_ranges, info_map); {term, info_map, error_ids}; }; diff --git a/src/haz3lweb/view/Cell.re b/src/haz3lweb/view/Cell.re index 1aeed58a06..e6f89dea54 100644 --- a/src/haz3lweb/view/Cell.re +++ b/src/haz3lweb/view/Cell.re @@ -123,12 +123,7 @@ let deco = { state: { meta: { - z_projected, - term_ranges, - segment_projected, - measured_projected, - terms, - tiles, + projected: {z, term_ranges, segment, measured, terms, tiles, _}, _, }, _, @@ -138,7 +133,7 @@ let deco = ) => { module Deco = Deco.Deco({ - let map = measured_projected; + let map = measured; let terms = terms; let term_ranges = term_ranges; let tiles = tiles; @@ -146,19 +141,12 @@ let deco = let show_backpack_targets = show_backpack_targets; let error_ids = error_ids; }); - let decos = - selected - ? Deco.all(~inject, z_projected, segment_projected) : Deco.err_holes(); + let decos = selected ? Deco.all(~inject, z, segment) : Deco.err_holes(); let decos = switch (test_results) { | None => decos | Some(test_results) => - decos - @ test_result_layer( - ~font_metrics, - ~measured=measured_projected, - test_results, - ) // TODO move into decos + decos @ test_result_layer(~font_metrics, ~measured, test_results) // TODO move into decos }; switch (highlights) { | Some(colorMap) => diff --git a/src/haz3lweb/view/Code.re b/src/haz3lweb/view/Code.re index 5f7a9a5ba0..191db619be 100644 --- a/src/haz3lweb/view/Code.re +++ b/src/haz3lweb/view/Code.re @@ -164,7 +164,7 @@ let view = ~settings: Settings.t, { state: { - meta: {measured_projected, buffer_ids, segment_projected, holes, _}, + meta: {projected: {measured, buffer_ids, segment, holes, _}, _}, _, }, _, @@ -173,11 +173,10 @@ let view = : Node.t => { module Text = Text({ - let map = measured_projected; + let map = measured; let settings = settings; }); - let code = Text.of_segment(buffer_ids, false, sort, segment_projected); - let holes = - List.map(of_hole(~measured=measured_projected, ~font_metrics), holes); + let code = Text.of_segment(buffer_ids, false, sort, segment); + let holes = List.map(of_hole(~measured, ~font_metrics), holes); div(~attr=Attr.class_("code"), [span_c("code-text", code), ...holes]); }; diff --git a/src/haz3lweb/view/ExerciseMode.re b/src/haz3lweb/view/ExerciseMode.re index 52302e7493..ea1e8d6a84 100644 --- a/src/haz3lweb/view/ExerciseMode.re +++ b/src/haz3lweb/view/ExerciseMode.re @@ -60,7 +60,10 @@ let view = Cell.editor_view( ~selected=pos == this_pos, ~error_ids= - Statics.Map.error_ids(editor.state.meta.term_ranges, di.info_map), + Statics.Map.error_ids( + editor.state.meta.projected.term_ranges, + di.info_map, + ), ~inject, ~ui_state, ~mousedown_updates=[SwitchEditor(this_pos)], diff --git a/src/haz3lweb/view/assistant/UpdateAssistant.re b/src/haz3lweb/view/assistant/UpdateAssistant.re index 8b7f006c30..5452ba291f 100644 --- a/src/haz3lweb/view/assistant/UpdateAssistant.re +++ b/src/haz3lweb/view/assistant/UpdateAssistant.re @@ -68,7 +68,8 @@ let apply = * first hole. This should be revisited if completions are * refactored to use a more structured buffer format */ module M = (val Editor.Meta.module_of_t(editor.state.meta)); - let start = Zipper.caret_point(M.measured_projected, z); + let start = + Zipper.caret_point(M.measured, editor.state.meta.projected.z); let rec do_actions = (model, actions: list(UpdateAction.t)) => switch (actions) { | [] => Ok(model)