Skip to content

Commit

Permalink
cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
disconcision committed Apr 30, 2024
1 parent f4d10f1 commit a08e621
Show file tree
Hide file tree
Showing 3 changed files with 42 additions and 58 deletions.
19 changes: 19 additions & 0 deletions src/haz3lcore/zipper/Zipper.re
Original file line number Diff line number Diff line change
Expand Up @@ -230,6 +230,15 @@ 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 select_caret = (d: Direction.t, z: t): option(t) =>
if (z.caret == Outer) {
select(d, z);
} else if (d == Left) {
z |> set_caret(Outer) |> move(Right) |> OptUtil.and_then(select(d));
} else {
z |> set_caret(Outer) |> select(d);
};

let pick_up = (z: t): t => {
let (selected, z) = update_selection(Selection.empty, z);
let selection =
Expand Down Expand Up @@ -473,3 +482,13 @@ let seg_for_view = smart_seg(~erase_buffer=false, ~dump_backpack=false);
let seg_for_sem = smart_seg(~erase_buffer=true, ~dump_backpack=true);

let seg_without_buffer = smart_seg(~erase_buffer=true, ~dump_backpack=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);
};
56 changes: 16 additions & 40 deletions src/haz3lcore/zipper/action/ProjectorAction.re
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
open Zipper;
open Util;
open OptUtil.Syntax;
//open OptUtil.Syntax;

let get_id_before = (seg, ancestors, projectors) =>
switch (Projector.split_seg(seg, projectors)) {
Expand Down Expand Up @@ -51,64 +51,40 @@ let neighbor_is =
(l, r);
};

/* Do move_action until the indicated piece is such that piece_p is true.
If no such piece is found, don't move. */
let rec do_until_sib =
(move: t => option(t), z_pred: Zipper.t => bool, z: t): option(t) =>
z_pred(z)
? Some(z)
: {
let* z = move(z);
do_until_sib(move, z_pred, z);
};

let is_right_of = (pid: Id.t, z) =>
let is_right_of = (id: Id.t, z) =>
switch (z.relatives.siblings, z.relatives.ancestors) {
| ((_, [r, ..._]), _) => Piece.id(r) == pid
| ((_, [r, ..._]), _) => Piece.id(r) == id
| ((_, []), []) => true // end of program
| ((_, []), _) => false
};

let is_left_of = (pid: Id.t, z) =>
let is_left_of = (id: Id.t, z) =>
switch (z.relatives.siblings, z.relatives.ancestors) {
| (([_, ..._] as ls, _), _) => Piece.id(ListUtil.last(ls)) == pid
| (([_, ..._] as ls, _), _) => Piece.id(ListUtil.last(ls)) == id
| (([], _), []) => true // beginning of program
| (([], _), _) => false
};

let is_on = (d: Direction.t, pid: Id.t) =>
let is_on = (d: Direction.t, id: Id.t) =>
switch (d) {
| Left => is_left_of(pid)
| Right => is_right_of(pid)
| Left => is_left_of(id)
| Right => is_right_of(id)
};

let skip_to = (d: Direction.t, proj_id, z) => {
let skip_to = (d: Direction.t, id, z) => {
// print_endline("ProjectorAction.skip_to");
do_until_sib(
Zipper.do_until(
Zipper.move(d),
is_on(d, proj_id),
is_on(d, id),
z,
);
};

//TODO(andrew): relocalize
let primary' = (d: Direction.t, z: Zipper.t): option(Zipper.t) =>
if (z.caret == Outer) {
Zipper.select(d, z);
} else if (d == Left) {
z
|> Zipper.set_caret(Outer)
|> Zipper.move(Right)
|> OptUtil.and_then(Zipper.select(d));
} else {
z |> Zipper.set_caret(Outer) |> Zipper.select(d);
};

let skip_select_to = (d: Direction.t, proj_id, z) => {
// print_endline("ProjectorAction.skip_to");
do_until_sib(
z => z |> primary'(d),
is_on(d, proj_id),
let skip_select_to = (d: Direction.t, id, z) => {
// print_endline("ProjectorAction.skip_select_to");
Zipper.do_until(
Zipper.select_caret(d),
is_on(d, id),
z,
);
};
25 changes: 7 additions & 18 deletions src/haz3lcore/zipper/action/Select.re
Original file line number Diff line number Diff line change
Expand Up @@ -4,29 +4,18 @@ open OptUtil.Syntax;
module Make = (M: Editor.Meta.S) => {
module Move = Move.Make(M);

let primary' = (d: Direction.t, z: Zipper.t): option(Zipper.t) =>
if (z.caret == Outer) {
Zipper.select(d, z);
} else if (d == Left) {
z
|> Zipper.set_caret(Outer)
|> Zipper.move(Right)
|> OptUtil.and_then(Zipper.select(d));
} else {
z |> Zipper.set_caret(Outer) |> Zipper.select(d);
};

let primary = (d: Direction.t, z: Zipper.t): option(Zipper.t) => {
let (l_proj, r_proj) =
ProjectorAction.neighbor_is(M.start_map, M.last_map, z);
switch (d, z.caret, (l_proj, r_proj)) {
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),
) {
| (Left, Outer, (Some(id), _)) =>
ProjectorAction.skip_select_to(Left, id, z)
| (Right, Outer, (_, Some(id))) =>
ProjectorAction.skip_select_to(Right, id, z)
| _ => primary'(d, z)
| _ => Zipper.select_caret(d, z)
};
};

let vertical = (d: Direction.t, ed: Zipper.t): option(Zipper.t) =>
Move.do_vertical(primary, d, ed);
Expand Down

0 comments on commit a08e621

Please sign in to comment.