From a473d339a62d5cd6dc55e7b21b570def29f60658 Mon Sep 17 00:00:00 2001 From: disconcision Date: Thu, 16 May 2024 23:29:16 -0400 Subject: [PATCH] projectors large-scale cleanup --- src/haz3lcore/tiles/Grout.re | 2 - src/haz3lcore/tiles/Piece.re | 7 -- src/haz3lcore/tiles/Secondary.re | 2 - src/haz3lcore/tiles/Tile.re | 2 - src/haz3lcore/zipper/Editor.re | 24 ++-- src/haz3lcore/zipper/Printer.re | 32 +++++ src/haz3lcore/zipper/Projector.re | 154 +------------------------ src/haz3lcore/zipper/action/Move.re | 6 +- src/haz3lcore/zipper/action/Perform.re | 39 +------ src/haz3lcore/zipper/action/Select.re | 2 +- src/haz3lschool/Exercise.re | 3 +- src/haz3lweb/Editors.re | 3 - src/haz3lweb/ScratchSlide.re | 2 +- src/haz3lweb/Update.re | 1 - src/haz3lweb/UpdateAction.re | 2 +- src/haz3lweb/util/JsUtil.re | 37 +++--- src/haz3lweb/view/Cell.re | 4 +- src/haz3lweb/view/ExerciseMode.re | 5 +- src/haz3lweb/view/Icons.re | 9 -- 19 files changed, 74 insertions(+), 262 deletions(-) diff --git a/src/haz3lcore/tiles/Grout.re b/src/haz3lcore/tiles/Grout.re index 57aa4431fd..496de68f10 100644 --- a/src/haz3lcore/tiles/Grout.re +++ b/src/haz3lcore/tiles/Grout.re @@ -57,5 +57,3 @@ let merge = (gs: list(t)): option(t) => | Some((_, ft)) => hd.shape == ft.shape ? Some(hd) : None } }; - -let update_id = (g: t, id: Id.t): t => {...g, id}; diff --git a/src/haz3lcore/tiles/Piece.re b/src/haz3lcore/tiles/Piece.re index 4fa01da541..eb2b91e6d3 100644 --- a/src/haz3lcore/tiles/Piece.re +++ b/src/haz3lcore/tiles/Piece.re @@ -151,10 +151,3 @@ let mold_of = (~shape=Nib.Shape.Convex, p: t) => | Grout(g) => Mold.of_grout(g, Any) | Secondary(_) => Mold.of_secondary({sort: Any, shape}) }; - -let update_id = (p: t, id: Id.t): t => - switch (p) { - | Tile(t) => Tile(Tile.update_id(id, t)) - | Grout(g) => Grout(Grout.update_id(g, id)) - | Secondary(w) => Secondary(Secondary.update_id(w, id)) - }; diff --git a/src/haz3lcore/tiles/Secondary.re b/src/haz3lcore/tiles/Secondary.re index 3f5da66e76..7ef17b16a1 100644 --- a/src/haz3lcore/tiles/Secondary.re +++ b/src/haz3lcore/tiles/Secondary.re @@ -68,5 +68,3 @@ let get_string: secondary_content => string = }; let id = w => w.id; - -let update_id = (w: t, id) => {...w, id}; diff --git a/src/haz3lcore/tiles/Tile.re b/src/haz3lcore/tiles/Tile.re index ae18ee8c90..10c7c41e42 100644 --- a/src/haz3lcore/tiles/Tile.re +++ b/src/haz3lcore/tiles/Tile.re @@ -156,5 +156,3 @@ let pop_r = (tile: t): (segment, piece) => // }; // }; // }; - -let update_id = (id, t: t) => {...t, id}; diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/zipper/Editor.re index 3004070f9d..d1394f76af 100644 --- a/src/haz3lcore/zipper/Editor.re +++ b/src/haz3lcore/zipper/Editor.re @@ -11,7 +11,7 @@ module Meta = { segment_projected: Segment.t, measured_projected: Measured.t, term_projected: Term.UExp.t, - term_ranges_projected: TermRanges.t, + term_ranges: TermRanges.t, terms: TermMap.t, tiles: TileMap.t, holes: list(Grout.t), @@ -34,7 +34,7 @@ module Meta = { measured_real, measured_projected: Measured.of_segment(segment_projected), segment_projected, - term_ranges_projected: TermRanges.mk(segment_projected), + term_ranges: TermRanges.mk(segment_projected), tiles: TileMap.mk(segment_projected), term_projected, terms, @@ -43,11 +43,10 @@ module Meta = { }; }; - //TODO(andrew): what is this module used for? module type S = { let touched: Touched.t; let measured_projected: Measured.t; - let term_ranges_projected: TermRanges.t; + let term_ranges: TermRanges.t; let col_target: int; }; let module_of_t = (m: t): (module S) => @@ -55,7 +54,7 @@ module Meta = { { let touched = m.touched; let measured_projected = m.measured_projected; - let term_ranges_projected = m.term_ranges_projected; + let term_ranges = m.term_ranges; let col_target = m.col_target; }); @@ -88,8 +87,8 @@ module Meta = { segment_projected, ) : measured_real; - let term_ranges_projected = - is_edit ? TermRanges.mk(segment_projected) : meta.term_ranges_projected; + let term_ranges = + is_edit ? TermRanges.mk(segment_projected) : meta.term_ranges; let col_target = switch (a) { | Move(Local(Up | Down)) @@ -113,7 +112,7 @@ module Meta = { measured_projected, segment_real, segment_projected, - term_ranges_projected, + term_ranges, tiles: is_edit ? TileMap.mk(segment_projected) : meta.tiles, term_projected, terms, @@ -235,15 +234,6 @@ let trailing_hole_ctx = (ed: t, info_map: Statics.Map.t) => { let get_projectors = (ed: t) => ed.state.zipper.projectors; -let get_projector = (id: Id.t, ed: t) => - Projector.Map.find(id, ed.state.zipper.projectors); - -let add_projector = (id: Id.t, p: Projector.t, ed: t) => - update_z( - z => {...z, projectors: Projector.Map.add(id, p, z.projectors)}, - ed, - ); - let map_projectors = (f: (Id.t, Projector.t) => Projector.t, ed: t) => update_z( z => {...z, projectors: Projector.Map.mapi(f, z.projectors)}, diff --git a/src/haz3lcore/zipper/Printer.re b/src/haz3lcore/zipper/Printer.re index 2a1fea8493..5614c2ff86 100644 --- a/src/haz3lcore/zipper/Printer.re +++ b/src/haz3lcore/zipper/Printer.re @@ -91,6 +91,38 @@ 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/Projector.re b/src/haz3lcore/zipper/Projector.re index e48a28466c..ecbbcafc27 100644 --- a/src/haz3lcore/zipper/Projector.re +++ b/src/haz3lcore/zipper/Projector.re @@ -51,9 +51,7 @@ module Map = { let placehold = (ps: Map.t, p: Piece.t) => switch (Map.find(Piece.id(p), ps)) { | None => p - | Some(pr) => - //TODO(andrew): Maybe shouldn't just duplicate this id in the general case? - placeholder(pr, Piece.id(p)) + | Some(pr) => placeholder(pr, Piece.id(p)) }; let rec of_segment = (projectors, seg: Segment.t): Segment.t => { @@ -87,153 +85,3 @@ let selection_sides_is = piece_is(projectors, ListUtil.hd_opt(s.content)), piece_is(projectors, ListUtil.last_opt(s.content)), ); - -/* - projector map has ids of projectors - can use infomap to get ancestors of projectors - - projector map has projector type - but for each projector we also need: - - it's extent (to use for measured) - - clarification: 'range of projector': extent in base syntax - - vs 'domain of projector': extent in view (eg collapsed entirely for fold) - - it's view function (to use for view) - - it's action function (to use for action dispatch - we might want to pre-derive: - - parent segment - - the range of the projector in the segment - - measured side: - recurse into segment, accumulating ancestor list - i guess this alternatingly comes from enclosing tiles and segment skels - i guess inside a segment, we recurse into the skel, tracking going through ancestors - from the ancestor list until we hit a tile - whose id is the target id - then we subsistute in a token consisting only of spaces/linebreaks which - takes up the space of the projector (which i guess should be a starting - and ending offset in the frame of the parent editor) - - - view side: - recurse into segment, accumulating ancestor list - i guess this alternatingly comes from enclosing tiles and segment skels - i guess inside a segment, we recurse into the skel, tracking going through ancestors - from the ancestor list until we hit a tile - whose id is the target id - - maybe to make things easier: - if for each projector we know its parent segment - and know what range of the segment 0 <= start < end < length(seg) corresponds to the projector - - ok, new plan: - in view_of_segment, we recurse the skel looking for projectors. the first (topmost) one we find, - we find it's range in the segment, and create new segment to render, consisting of the segment - vefore the projector subrange, a placeholder for the projector subrange, and the segment after - the projector subrange. we don't handle any drawing for the projector; that goes through Deco - - for first pass we dont need full recursion, so can just have a deco type that is subeditors - for first pass subeditor will just be stub views, so they can be treated as inline/tokens - (for higher phases will want to be able to insert full editors, so will likely need editors - to have programable starting col, so that we can draw them as if they were just a subsegment - of the parent editor) - - - action side: - - for opaque projectors, we will prohibit movement into them, - and make forming them eject the cursor. as long as we - ensure the cursor cant move into one, we can dont - need to worry about whether we're inside one for action permissions - - so for basic movement actions, we make moving left into an - opaque leaf projector jump to its right, and vice versa - - (phase 1.5 we allow a single cursor state on the projector itself) - - actions: movement - - phase 1.0: move past subview - - phase 1.5: move onto subview - - phase 2: move into subview - - for phase 1.5, we probably need to extend caret position to - model the cursor being on the projector itself. being in this - state will dispatch keyboard input to the projector's handler - - old: - type t = - | Outer - | Inner(int, int); - - v2: - type inner = - | Token(int, int) - | SubCell(Id.t); - type t = - | Outer - | Inner(inner); - - v3: - type base = - | Outer - | Inner(int, int); - type t = - | Base(base) - | SubCell(Id.t, t); // supports nested subcells - - - - primary movement needs to check if the piece we're trying to move into starts/ends - a subcell. if so, we (phase i) skip over it or (phase ii) move into it, ie set caret - position to Subcell(Id.t,og_caret_pos) - - 2024-02-26 - want to add some entries to Measured - right now the placeholder approach is that a monotoken is introduced - with the same id as the projector root term. this seems to work well - in the case where the projector root tile is convex, as this means that - the delims on the left and right of the projected segment are shards of - the same tile. but actually even this creates some issues actually, - see the FuCkNASTY hackzz in Measured. - - in general we are concerned with caret positions to the left and right - of the projected segment. caret_point/base_point is excepting there - because they are looking for ids not found in measured, in the case - of infix operators on both sides so they can't currently be folded. - - not sure if its a good idea, but one approach is to make sure that - the ids in Measured include the left and right delims of the projected - segment instead of the root id. - - but we probably dont want to add multiple tiles to the projection zipper. - but maybe we could add ids after the fact, copying some measurements - by querying the measurements of the placeholder tile. - - collapsed segments: - - [1]: root is 1, L is 1, R is 1 - [(1)]: root is [(,)], L is [(], R is [)] - [1+2] : root is +, L is 1, R is 2 - [let x = 1 in 4] root is [let,=,in], L is [let], R is 4 - (mythical postfix operator:) - [5!] root is [,], L is 5, L is [!] - - ideally the placeholder tile should correspond to the left and right - delims of the projected segment so as to make measured accesses - seamless. so what if: - placeholder tiles uses two shards, one for the left delim and - one for the right delim - then after we run Measured we get the placeholder measurement, - and create (up to) two new entries in the Measured map, one for - the left delim and one for the right delim, - - NOTE: currently the FuCkNASTY occurs on the right delim - of a collapsed "(1+2)" segment, but not a "1" segment - - - Current status: - singletons and convex seem to work fine - can fold [fun, ->] and [let, =, in], can unfold (from one side at least), - some movement problems - can fold infix ops if surrounded by parens; movement bugged, cant unfold - - */ diff --git a/src/haz3lcore/zipper/action/Move.re b/src/haz3lcore/zipper/action/Move.re index a60c4149ff..aa327631e4 100644 --- a/src/haz3lcore/zipper/action/Move.re +++ b/src/haz3lcore/zipper/action/Move.re @@ -104,7 +104,6 @@ module Make = (M: Editor.Meta.S) => { }; let is_at_side_of_row = (d: Direction.t, z: Zipper.t) => { - print_endline("Move.is_at_side_of_row"); let Measured.Point.{row, col} = caret_point(z); switch (Zipper.move(d, z)) { | None => true @@ -177,7 +176,6 @@ module Make = (M: Editor.Meta.S) => { /* Here f should be a function which results in strict d-wards movement of the caret. Iterate f until we get to the closet caret position to a target derived from the initial position */ - print_endline("Move.do_vertical"); let cur_p = caret_point(z); let goal = Measured.Point.{ @@ -239,10 +237,10 @@ module Make = (M: Editor.Meta.S) => { | Some(z) => Some(z) }; - let jump_to_id = (~init=Direction.Left, z: t, id: Id.t): option(t) => { + let jump_to_id = (z: t, id: Id.t): option(t) => { let* {origin, _} = Measured.find_by_id(id, M.measured_projected); let z = - switch (init == Left ? to_start(z) : to_end(z)) { + switch (to_start(z)) { | None => z | Some(z) => z }; diff --git a/src/haz3lcore/zipper/action/Perform.re b/src/haz3lcore/zipper/action/Perform.re index ae7508b1b2..ea1867aaeb 100644 --- a/src/haz3lcore/zipper/action/Perform.re +++ b/src/haz3lcore/zipper/action/Perform.re @@ -3,12 +3,13 @@ open Zipper; let is_write_action = (a: Action.t) => { switch (a) { + //TODO: revist as projectors grow + | Project(_) => false | Move(_) | MoveToNextHole(_) | Unselect(_) | Jump(_) | Select(_) => false - | Project(_) //TODO(andrew): ?? | Destruct(_) | Insert(_) | Pick_up @@ -37,46 +38,14 @@ let go_z = let select_term_current = z => switch (Indicated.index(z)) { - | None => - print_endline("PERFORM.select_term_current: no index"); - Error(Action.Failure.Cant_select); + | None => Error(Action.Failure.Cant_select) | Some(id) => switch (Select.term(id, z)) { | Some(z) => Ok(z) - | None => - print_endline("PERFORM.select_term_current: Select.term failed"); - Error(Action.Failure.Cant_select); + | None => Error(Action.Failure.Cant_select) } }; - let _selection_dance = (z, d, pid): t => { - //TODO(andrew): clean up hacky movement - print_endline("PERFORM: going to start"); - print_endline("direction: " ++ Direction.show(d)); - //d == Left ? Move.to_end(z) : Move.to_start(z) - switch (select_term_current(z)) { - | Error(_err) => - //TODO(andrew): deal with this properly - //figure out why selection is failing (metrics issue?) - print_endline("PERFORM: ERROR couldn't select, going to start instead"); - switch (Move.jump_to_id(~init=Left, z, Piece.id(pid))) { - | None => - print_endline("PERFORM: jump_to_id failed"); - z; - | Some(z) => - print_endline("PERFORM: jump_to_id succeeded"); - z; - // switch (select_term_current(z)) { - // | Ok(z) => Ok(directional_unselect(Direction.toggle(d), z)) - // | Error(_err) => Ok(z) - // }; - }; - | Ok(z) => - print_endline("PERFORM: select_term_current succeeded"); - directional_unselect(Direction.toggle(d), z); - }; - }; - switch (a) { | Project(a) => switch (ProjectorAction.go(a, z)) { diff --git a/src/haz3lcore/zipper/action/Select.re b/src/haz3lcore/zipper/action/Select.re index 6a198a4e5f..4eff98afdf 100644 --- a/src/haz3lcore/zipper/action/Select.re +++ b/src/haz3lcore/zipper/action/Select.re @@ -29,7 +29,7 @@ module Make = (M: Editor.Meta.S) => { let term = (id: Id.t, z: Zipper.t): option(Zipper.t) => { //TODO: check if selection is already a term: no-op in this case - let* (l, r) = TermRanges.find_opt(id, M.term_ranges_projected); + let* (l, r) = TermRanges.find_opt(id, M.term_ranges); print_endline( "Select.term: l: " ++ Id.show(Piece.id(l)) diff --git a/src/haz3lschool/Exercise.re b/src/haz3lschool/Exercise.re index 6867a18388..b9f6165ace 100644 --- a/src/haz3lschool/Exercise.re +++ b/src/haz3lschool/Exercise.re @@ -588,8 +588,7 @@ module F = (ExerciseEnv: ExerciseEnv) => { let wrap = (term, editor: Editor.t): TermItem.t => { term, - term_ranges: editor.state.meta.term_ranges_projected, - //TODO(andrew): what is this for? + term_ranges: editor.state.meta.term_ranges, }; let term_of = (editor: Editor.t): Term.UExp.t => diff --git a/src/haz3lweb/Editors.re b/src/haz3lweb/Editors.re index fbfdb0ae00..28bce5be19 100644 --- a/src/haz3lweb/Editors.re +++ b/src/haz3lweb/Editors.re @@ -179,8 +179,5 @@ let switch_example_slide = (editors: t, name: string): option(t) => | Documentation(_, slides) => Some(Documentation(name, slides)) }; -let get_projectors = (editors: t): Projector.Map.t => - editors |> get_editor |> Editor.get_projectors; - let map_projectors = (editors: t, f: (Id.t, Projector.t) => Projector.t): t => put_editor(editors |> get_editor |> Editor.map_projectors(f), editors); diff --git a/src/haz3lweb/ScratchSlide.re b/src/haz3lweb/ScratchSlide.re index a95bbc0167..09860711ed 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_projected, info_map); + Statics.Map.error_ids(editor.state.meta.term_ranges, info_map); {term, info_map, error_ids}; }; diff --git a/src/haz3lweb/Update.re b/src/haz3lweb/Update.re index 8e2fa5b9d3..ff51baad26 100644 --- a/src/haz3lweb/Update.re +++ b/src/haz3lweb/Update.re @@ -221,7 +221,6 @@ let update_cached_data = (~schedule_action, update, m: Model.t): Model.t => { ? { print_endline("UPDATING STATICS"); let statics = Editors.mk_statics(~settings=m.settings, m.editors); - print_endline("UPDATING PROJECTORS"); ProjectorsUpdate.update_all({...m, statics}); } : m; diff --git a/src/haz3lweb/UpdateAction.re b/src/haz3lweb/UpdateAction.re index e4ce0b4840..2003a48d15 100644 --- a/src/haz3lweb/UpdateAction.re +++ b/src/haz3lweb/UpdateAction.re @@ -279,7 +279,7 @@ let should_scroll_to_caret = | Put_down | RotateBackpack | MoveToBackpackTarget(_) => true - | Project(_) //TODO(andrew) + | Project(_) | Unselect(_) | Select(All) => false } diff --git a/src/haz3lweb/util/JsUtil.re b/src/haz3lweb/util/JsUtil.re index 1b8685f6b3..d9a7efc7fc 100644 --- a/src/haz3lweb/util/JsUtil.re +++ b/src/haz3lweb/util/JsUtil.re @@ -3,11 +3,13 @@ open Virtual_dom.Vdom; let get_elem_by_id = id => { let doc = Dom_html.document; - Js.Opt.get(doc##getElementById(Js.string(id)), () => { - assert - (false) - //print_endline(id); - }); + Js.Opt.get( + doc##getElementById(Js.string(id)), + () => { + print_endline(id); + assert(false); + }, + ); }; let date_now = () => { @@ -121,18 +123,21 @@ let copy = (str: string) => { ); }; -let scroll_cursor_into_view_if_needed = () => { - let caret_elem = get_elem_by_id("caret"); - let main = get_elem_by_id("main"); - let main_rect = main##getBoundingClientRect; - let caret_rect = caret_elem##getBoundingClientRect; - - if (caret_rect##.top < main_rect##.top) { - caret_elem##scrollIntoView(Js._true); - } else if (caret_rect##.bottom > main_rect##.bottom) { - caret_elem##scrollIntoView(Js._false); +let scroll_cursor_into_view_if_needed = () => + try({ + let caret_elem = get_elem_by_id("caret"); + let main = get_elem_by_id("main"); + let main_rect = main##getBoundingClientRect; + let caret_rect = caret_elem##getBoundingClientRect; + + if (caret_rect##.top < main_rect##.top) { + caret_elem##scrollIntoView(Js._true); + } else if (caret_rect##.bottom > main_rect##.bottom) { + caret_elem##scrollIntoView(Js._false); + }; + }) { + | Assert_failure(_) => () }; -}; module Fragment = { let set_current = frag => { diff --git a/src/haz3lweb/view/Cell.re b/src/haz3lweb/view/Cell.re index ccb8cda2b7..1aeed58a06 100644 --- a/src/haz3lweb/view/Cell.re +++ b/src/haz3lweb/view/Cell.re @@ -124,7 +124,7 @@ let deco = state: { meta: { z_projected, - term_ranges_projected, + term_ranges, segment_projected, measured_projected, terms, @@ -140,7 +140,7 @@ let deco = Deco.Deco({ let map = measured_projected; let terms = terms; - let term_ranges = term_ranges_projected; + let term_ranges = term_ranges; let tiles = tiles; let font_metrics = font_metrics; let show_backpack_targets = show_backpack_targets; diff --git a/src/haz3lweb/view/ExerciseMode.re b/src/haz3lweb/view/ExerciseMode.re index 28f4fa2c86..52302e7493 100644 --- a/src/haz3lweb/view/ExerciseMode.re +++ b/src/haz3lweb/view/ExerciseMode.re @@ -60,10 +60,7 @@ let view = Cell.editor_view( ~selected=pos == this_pos, ~error_ids= - Statics.Map.error_ids( - editor.state.meta.term_ranges_projected, - di.info_map, - ), + Statics.Map.error_ids(editor.state.meta.term_ranges, di.info_map), ~inject, ~ui_state, ~mousedown_updates=[SwitchEditor(this_pos)], diff --git a/src/haz3lweb/view/Icons.re b/src/haz3lweb/view/Icons.re index 9957445b48..1067286891 100644 --- a/src/haz3lweb/view/Icons.re +++ b/src/haz3lweb/view/Icons.re @@ -57,15 +57,6 @@ let star = ], ); -let fold = - simple_icon( - ~view="0 0 1200 1200", - [ - "m875 625h-275c-13.805 0-25-11.195-25-25v-267.19h50v206.83l407.32-407.32 35.359 35.352-407.32 407.32h214.64z", - "m125 200c0-13.809 11.191-25 25-25h500v50h-475v800h800v-475h50v500c0 13.805-11.195 25-25 25h-850c-13.809 0-25-11.195-25-25z", - ], - ); - let bomb = simple_icon( ~view="0 0 1200 1200",