From 8194591da5c928c22eadf6ec20673eba5a694c73 Mon Sep 17 00:00:00 2001 From: disconcision Date: Fri, 3 May 2024 00:05:00 -0400 Subject: [PATCH] improved movement for convex projs --- src/haz3lcore/zipper/Editor.re | 10 - src/haz3lcore/zipper/Projector.re | 245 +++++++----------- src/haz3lcore/zipper/action/Move.re | 17 +- src/haz3lcore/zipper/action/Perform.re | 18 +- .../zipper/action/ProjectorAction.re | 123 ++------- src/haz3lcore/zipper/action/Select.re | 14 +- 6 files changed, 150 insertions(+), 277 deletions(-) diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/zipper/Editor.re index 4840335ad9..5a80cc4e0f 100644 --- a/src/haz3lcore/zipper/Editor.re +++ b/src/haz3lcore/zipper/Editor.re @@ -13,8 +13,6 @@ module Meta = { tiles: TileMap.t, holes: list(Grout.t), buffer_ids: list(Id.t), - start_map: Projector.start_map, - last_map: Projector.start_map, }; let init = (z: Zipper.t) => { @@ -40,8 +38,6 @@ module Meta = { terms, holes: Segment.holes(segment), buffer_ids: Selection.buffer_ids(z.selection), - start_map: Projector.mk_start_map(z.projectors, term_ranges), - last_map: Projector.mk_last_map(z.projectors, term_ranges), }; }; @@ -49,8 +45,6 @@ module Meta = { let touched: Touched.t; let measured: Measured.t; let term_ranges: TermRanges.t; - let start_map: Projector.start_map; - let last_map: Projector.start_map; let col_target: int; }; let module_of_t = (m: t): (module S) => @@ -60,8 +54,6 @@ module Meta = { let measured = m.measured; let term_ranges = m.term_ranges; let col_target = m.col_target; - let start_map = m.start_map; - let last_map = m.last_map; }); // should not be serializing @@ -117,8 +109,6 @@ module Meta = { terms, holes: is_edit ? Segment.holes(segment) : meta.holes, buffer_ids: Selection.buffer_ids(z.selection), - start_map: Projector.mk_start_map(z.projectors, term_ranges), - last_map: Projector.mk_last_map(z.projectors, term_ranges), }; }; }; diff --git a/src/haz3lcore/zipper/Projector.re b/src/haz3lcore/zipper/Projector.re index eaac774a2e..9f505924b7 100644 --- a/src/haz3lcore/zipper/Projector.re +++ b/src/haz3lcore/zipper/Projector.re @@ -15,6 +15,11 @@ let toggle_fold: p => p = | Normal => Fold | Fold => Normal; +let placeholder_length: p => int = + fun + | Normal => (-666) + | Fold => 2; + [@deriving (show({with_path: false}), sexp, yojson)] module Map = { open Id.Map; @@ -31,64 +36,83 @@ module Map = { type t = p; -let rep_id = (seg, r) => r |> Aba.first_a |> List.nth(seg) |> Piece.id; - -let rec left_idx = (skel: Skel.t): int => { - switch (skel) { - | Op(r) - | Pre(r, _) => Aba.first_a(r) - | Post(s, _) - | Bin(s, _, _) => left_idx(s) - }; -}; - -let rec right_idx = (skel: Skel.t): int => { - switch (skel) { - | Op(r) - | Post(_, r) => Aba.first_a(r) - | Pre(_, s) - | Bin(_, _, s) => right_idx(s) - }; -}; - -let get_extreme_idxs = (skel: Skel.t): (int, int) => ( - left_idx(skel), - right_idx(skel), -); - -type projector_range = { - id: Id.t, - start: int, - last: int, -}; - -let get_range = (seg: Segment.t, ps: Map.t): option((Id.t, (int, int))) => { - let rec go = (skel: Skel.t) => { - let id = rep_id(seg, Skel.root(skel)); - switch (Id.Map.find_opt(id, ps)) { - | Some(_) => - let (l, r) = get_extreme_idxs(skel); - Some((id, (l, r))); - | None => - switch (skel) { - | Op(_) => None - | Pre(_, r) => go(r) - | Post(l, _) => go(l) - | Bin(l, _, r) => - switch (go(l)) { - | Some(x) => Some(x) - | None => go(r) - } - } - }; - }; - go(Segment.skel(seg)); -}; +// let rep_id = (seg, r) => r |> Aba.first_a |> List.nth(seg) |> Piece.id; + +// let rec left_idx = (skel: Skel.t): int => { +// switch (skel) { +// | Op(r) +// | Pre(r, _) => Aba.first_a(r) +// | Post(s, _) +// | Bin(s, _, _) => left_idx(s) +// }; +// }; + +// let rec right_idx = (skel: Skel.t): int => { +// switch (skel) { +// | Op(r) +// | Post(_, r) => Aba.first_a(r) +// | Pre(_, s) +// | Bin(_, _, s) => right_idx(s) +// }; +// }; + +// let get_extreme_idxs = (skel: Skel.t): (int, int) => ( +// left_idx(skel), +// right_idx(skel), +// ); + +// type projector_range = { +// id: Id.t, +// start: int, +// last: int, +// }; + +// let get_range = (seg: Segment.t, ps: Map.t): option((Id.t, (int, int))) => { +// let rec go = (skel: Skel.t) => { +// let id = rep_id(seg, Skel.root(skel)); +// switch (Id.Map.find_opt(id, ps)) { +// | Some(_) => +// let (l, r) = get_extreme_idxs(skel); +// Some((id, (l, r))); +// | None => +// switch (skel) { +// | Op(_) => None +// | Pre(_, r) => go(r) +// | Post(l, _) => go(l) +// | Bin(l, _, r) => +// switch (go(l)) { +// | Some(x) => Some(x) +// | None => go(r) +// } +// } +// }; +// }; +// go(Segment.skel(seg)); +// }; + +// let get_ranges = (seg: Segment.t, ps: Map.t): list((Id.t, (int, int))) => { +// let rec go = (skel: Skel.t) => { +// let id = rep_id(seg, Skel.root(skel)); +// switch (Id.Map.find_opt(id, ps)) { +// | Some(_) => +// let (l, r) = get_extreme_idxs(skel); +// [(id, (l, r))]; +// | None => +// switch (skel) { +// | Op(_) => [] +// | Pre(_, r) => go(r) +// | Post(l, _) => go(l) +// | Bin(l, _, r) => go(l) @ go(r) +// } +// }; +// }; +// go(Segment.skel(seg)); +// }; let split_seg = - (seg: Segment.t, ps: Map.t) + (seg: Segment.t, range: option((Id.t, (int, int)))) : option((Segment.t, Segment.t, Segment.t, Id.t)) => { - switch (get_range(seg, ps)) { + switch (range) { | None => None | Some((id, (start, last))) => //TODO(andrew): numeric edge cases? @@ -99,48 +123,26 @@ let split_seg = }; }; -let placeholder_tile = (s: string, id: Id.t): Tile.t => { - id, - label: [s], - mold: Mold.mk_op(Any, []), - shards: [0], - children: [], -}; - -let project_mid = (id, p: option(t), mid): Segment.t => - //TODO(andrew): prrobably shouldn't just duplicate this id in the general case? - switch (p) { - | Some(Fold) => [Tile(placeholder_tile(" ", id))] - //[Grout({id, shape: Convex})] - | Some(Normal) - | None => mid - }; - -let project_seg = (p, seg: Segment.t): Segment.t => { - // print_endline("project_seg"); - switch (split_seg(seg, p)) { - | Some((pre, mid_og, suf, proj_id)) => - /*TODO(andrew): need to find a way to handle multiple projectors per segment, - i.e. wasn't thinking about ones in disjoint subtrees */ - // print_endline( - // "split: segment length: " - // ++ string_of_int(List.length(seg)) - // ++ " as divided into: " - // ++ string_of_int(List.length(pre)) - // ++ " " - // ++ string_of_int(List.length(mid_og)) - // ++ " " - // ++ string_of_int(List.length(suf)), - // ); - pre @ project_mid(proj_id, Map.find(proj_id, p), mid_og) @ suf - | None => - // print_endline("no split"); - seg +let placeholder = (pr: t, id: Id.t): Piece.t => + Piece.Tile({ + id, + label: [String.make(placeholder_length(pr), ' ')], + mold: Mold.mk_op(Any, []), + shards: [0], + children: [], + }); + +let placehold = (prjs, p: Piece.t) => + switch (Map.find(Piece.id(p), prjs)) { + | None + | Some(Normal) => p + | Some(pr) => + //TODO(andrew): Maybe shouldn't just duplicate this id in the general case? + placeholder(pr, Piece.id(p)) }; -}; let rec of_segment = (projectors, seg: Segment.t): Segment.t => { - seg |> project_seg(projectors) |> List.map(of_piece(projectors)); + seg |> List.map(placehold(projectors)) |> List.map(of_piece(projectors)); } and of_piece = (projectors, p: Piece.t): Piece.t => { switch (p) { @@ -153,66 +155,17 @@ and of_tile = (projectors, t: Tile.t): Tile.t => { {...t, children: List.map(of_segment(projectors), t.children)}; }; -type start_entry = { - proj_id: Id.t, - t, - start_id: Id.t, - last_id: Id.t, -}; -/* map indexed by start_id instead of proj_id */ -type start_map = Id.Map.t(start_entry); -let guy_of = (id, t, (start, last)) => { - proj_id: id, - t, - start_id: Piece.id(start), - last_id: Piece.id(last), -}; -let guy_of_rev = (id, t, (start, last)) => { - proj_id: id, - t, - start_id: Piece.id(last), - last_id: Piece.id(start), -}; -let proj_info = (term_ranges, id: Id.t, t: t, acc: start_map) => { - //print_endline("proj_info for id: " ++ Id.to_string(id)); - switch (Id.Map.find_opt(id, term_ranges)) { - | Some(range) => - let guy = guy_of(id, t, range); - Id.Map.add(guy.start_id, guy, acc); - | _ => - print_endline("ERROR: mk_nu_proj_map: no term range for projector"); - acc; - }; -}; -let proj_info_rev = (term_ranges, id: Id.t, t: t, acc: start_map) => { - // print_endline("proj_info for id: " ++ Id.to_string(id)); - switch (Id.Map.find_opt(id, term_ranges)) { - | Some(range) => - let guy = guy_of(id, t, range); - Id.Map.add(guy.last_id, guy, acc); - | _ => - print_endline("ERROR: mk_nu_proj_map: no term range for projector"); - acc; - }; -}; - -let mk_start_map = (projectors: Map.t, term_ranges: TermRanges.t): start_map => - Map.fold(proj_info(term_ranges), projectors, Id.Map.empty); - -let mk_last_map = (projectors: Map.t, term_ranges: TermRanges.t): start_map => - Map.fold(proj_info_rev(term_ranges), projectors, Id.Map.empty); - let fake_measured = (p: Map.t, measured: Measured.t, term_ranges: TermRanges.t): Measured.t => Map.fold( - (id, _p: t, measured: Measured.t) => { + (id, pr: t, measured: Measured.t) => { switch ( Measured.find_by_id(id, measured), Id.Map.find_opt(id, term_ranges), ) { | (Some(m), Some((p_start, p_last))) => - let p_start = Piece.Tile(placeholder_tile(" ", Piece.id(p_start))); - let p_last = Piece.Tile(placeholder_tile(" ", Piece.id(p_last))); + let p_start = placeholder(pr, Piece.id(p_start)); + let p_last = placeholder(pr, Piece.id(p_last)); let measured = Measured.add_p(p_start, m, measured); let measured = Measured.add_p(p_last, m, measured); print_endline("fake_measured: added placeholder tiles:"); diff --git a/src/haz3lcore/zipper/action/Move.re b/src/haz3lcore/zipper/action/Move.re index 441df3a943..2b318d2bbf 100644 --- a/src/haz3lcore/zipper/action/Move.re +++ b/src/haz3lcore/zipper/action/Move.re @@ -6,7 +6,7 @@ open Sexplib.Std; [@deriving (show({with_path: false}), sexp, yojson)] type movability = | CanEnter(int, int) - | SkipTo(ProjectorAction.thing) + | SkipTo(Id.t) | CanPass | CantEven; @@ -23,12 +23,7 @@ let movability = (chunkiness: chunkiness, label, delim_idx): movability => { }; let neighbor_movability = - ( - start_map: Projector.start_map, - last_map: Projector.start_map, - chunkiness: chunkiness, - {relatives: {siblings, ancestors}, _} as z: t, - ) + (chunkiness: chunkiness, {relatives: {siblings, ancestors}, _} as z: t) : (movability, movability) => { let movability = movability(chunkiness); let (supernhbr_l, supernhbr_r) = @@ -40,7 +35,7 @@ let neighbor_movability = ) }; let (l_nhbr, r_nhbr) = Siblings.neighbors(siblings); - let (l_proj, r_proj) = ProjectorAction.neighbor_is(start_map, last_map, z); + let (l_proj, r_proj) = ProjectorAction.neighbor_is(z); let l = switch (l_proj, l_nhbr) { | (Some(l_proj_id), _) => SkipTo(l_proj_id) @@ -87,11 +82,7 @@ module Make = (M: Editor.Meta.S) => { z |> Zipper.set_caret(Inner(d_init, c_max)) |> Zipper.move(d); let primary = (chunkiness: chunkiness, d: Direction.t, z: t): option(t) => { - switch ( - d, - z.caret, - neighbor_movability(M.start_map, M.last_map, chunkiness, z), - ) { + switch (d, z.caret, neighbor_movability(chunkiness, z)) { /* this case maybe shouldn't be necessary but currently covers an edge (select an open parens to left of a multichar token and press left) */ | _ when z.selection.content != [] => pop_move(d, z) diff --git a/src/haz3lcore/zipper/action/Perform.re b/src/haz3lcore/zipper/action/Perform.re index bf27beeb0a..5c1f6e5ab1 100644 --- a/src/haz3lcore/zipper/action/Perform.re +++ b/src/haz3lcore/zipper/action/Perform.re @@ -59,11 +59,15 @@ let go_z = let select_term_current = z => switch (Indicated.index(z)) { - | None => Error(Action.Failure.Cant_select) + | None => + print_endline("PERFORM.select_term_current: no index"); + Error(Action.Failure.Cant_select); | Some(id) => switch (Select.term(id, z)) { | Some(z) => Ok(z) - | None => Error(Action.Failure.Cant_select) + | None => + print_endline("PERFORM.select_term_current: Select.term failed"); + Error(Action.Failure.Cant_select); } }; @@ -97,15 +101,17 @@ let go_z = Ok(z); | Some(z) => print_endline("PERFORM: jump_to_id succeeded"); - switch (select_term_current(z)) { - | Ok(z) => Ok(directional_unselect(Direction.toggle(d), z)) - | Error(_err) => Ok(z) - }; + Ok(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"); Ok(directional_unselect(Direction.toggle(d), z)); }; + // Ok(z); } | Move(d) => Move.go(d, z) |> Result.of_option(~error=Action.Failure.Cant_move) diff --git a/src/haz3lcore/zipper/action/ProjectorAction.re b/src/haz3lcore/zipper/action/ProjectorAction.re index 599733b208..03deeca6cf 100644 --- a/src/haz3lcore/zipper/action/ProjectorAction.re +++ b/src/haz3lcore/zipper/action/ProjectorAction.re @@ -1,120 +1,49 @@ open Zipper; open Util; -//open OptUtil.Syntax; -[@deriving (show({with_path: false}), sexp, yojson)] -type relation = - | Parent - | Sibling; - -[@deriving (show({with_path: false}), sexp, yojson)] -type thing = { - id: Id.t, - relation, -}; - -let get_id_before = (seg, ancestors, projectors): option(thing) => - switch (Projector.split_seg(seg, projectors)) { - | Some(([_, ..._] as xs, _, _, _)) => - Some({id: Piece.id(ListUtil.last(xs)), relation: Sibling}) - | Some(([], _, _, _)) => - switch (Ancestors.parent(ancestors)) { - | Some(a) => - print_endline("prev_id: empty pre using parent"); - print_endline("parent id: " ++ Id.show(a.id)); - Some({id: a.id, relation: Parent}); - | None => - print_endline("prev_id: empty pre no ancestor"); - None; //TODO(andrew) //Id.invalid; - } - | None => - print_endline("prev_id: None"); - None; //TODO(andrew) //Id.invalid; - }; - -let get_id_after = (seg, ancestors, projectors): option(thing) => - switch (Projector.split_seg(seg, projectors)) { - | Some((_, _, [hd, ..._], _)) => - Some({id: Piece.id(hd), relation: Sibling}) - | Some((_, _, [], _)) => - switch (Ancestors.parent(ancestors)) { - | Some(a) => - print_endline("next_id: empty pre using parent"); - print_endline("parent id: " ++ Id.show(a.id)); - Some({id: a.id, relation: Parent}); - | None => - print_endline("next_id: empty pre no ancestor"); - None; //TODO(andrew) //Id.invalid; - } - | None => - print_endline("next_id: empty post"); - None; //TODO(andrew) //Id.invalid; +let piece_is = (projectors, nhbr) => + switch (nhbr) { + | Some(p) when Projector.Map.mem(Piece.id(p), projectors) => + Projector.Map.mem(Piece.id(p), projectors) ? Some(Piece.id(p)) : None + | _ => None }; let neighbor_is = - ( - start_map: Projector.start_map, - last_map: Projector.start_map, - {relatives: {siblings, ancestors}, projectors, _}: t, - ) - : (option(thing), option(thing)) => { - let (l_nhbr, r_nhbr) = Siblings.neighbors(siblings); - let seg = (siblings |> fst) @ (siblings |> snd); - let l = - switch (l_nhbr) { - | Some(p) when Projector.Map.mem(Piece.id(p), last_map) => - get_id_before(seg, ancestors, projectors) - | _ => None - }; - let r = - switch (r_nhbr) { - | Some(p) when Projector.Map.mem(Piece.id(p), start_map) => - get_id_after(seg, ancestors, projectors) - | _ => None - }; - (l, r); -}; + ({relatives: {siblings, _}, projectors, _}: t) + : (option(Id.t), option(Id.t)) => ( + piece_is(projectors, Siblings.left_neighbor(siblings)), + piece_is(projectors, Siblings.right_neighbor(siblings)), +); -let id_right_of_z = (id: Id.t, z) => - switch (z.relatives.siblings, z.relatives.ancestors) { - | ((_, [r, ..._]), _) => Piece.id(r) == id - | ((_, []), []) => true // end of program - | ((_, []), _) => false - }; - -let id_left_of_z = (id: Id.t, z) => - switch (z.relatives.siblings, z.relatives.ancestors) { - | (([_, ..._] as ls, _), _) => Piece.id(ListUtil.last(ls)) == id - | (([], _), []) => true // beginning of program - | (([], _), _) => false - }; - -let id_on = (d: Direction.t, id: Id.t) => +let id_on = (d: Direction.t, id: Id.t, z: Zipper.t): bool => switch (d) { - | Left => id_left_of_z(id) - | Right => id_right_of_z(id) - }; - -let d2 = (relation, d) => - switch (relation) { - | Sibling => d - | Parent => Direction.toggle(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 + } }; -let skip_to = (d: Direction.t, {id, relation}, z) => { +let skip_to = (d: Direction.t, id: Id.t, z: Zipper.t): option(Zipper.t) => { // print_endline("ProjectorAction.skip_to"); Zipper.do_until( Zipper.move(d), - id_on(d2(relation, d), id), + id_on(Direction.toggle(d), id), z, ); }; -let skip_select_to = (d: Direction.t, {id, relation}, z) => { +let skip_select_to = + (d: Direction.t, id: Id.t, z: Zipper.t): option(Zipper.t) => { // print_endline("ProjectorAction.skip_select_to"); Zipper.do_until( Zipper.select_caret(d), - id_on(d2(relation, d), id), + id_on(Direction.toggle(d), id), z, ); }; diff --git a/src/haz3lcore/zipper/action/Select.re b/src/haz3lcore/zipper/action/Select.re index 6c86b3c266..2b67c2939f 100644 --- a/src/haz3lcore/zipper/action/Select.re +++ b/src/haz3lcore/zipper/action/Select.re @@ -5,11 +5,7 @@ module Make = (M: Editor.Meta.S) => { module Move = Move.Make(M); let primary = (d: Direction.t, z: Zipper.t): option(Zipper.t) => - switch ( - d, - z.caret, - ProjectorAction.neighbor_is(M.start_map, M.last_map, z), - ) { + switch (d, z.caret, ProjectorAction.neighbor_is(z)) { | (Left, Outer, (Some(id), _)) => ProjectorAction.skip_select_to(Left, id, z) | (Right, Outer, (_, Some(id))) => @@ -22,13 +18,21 @@ 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); + print_endline("Select.range: last"); Move.do_towards(primary, last, z); }; 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); + print_endline( + "Select.term: l: " + ++ Id.show(Piece.id(l)) + ++ " r: " + ++ Id.show(Piece.id(r)), + ); range(Piece.id(l), Piece.id(r), z); };