diff --git a/src/haz3lcore/tiles/Piece.re b/src/haz3lcore/tiles/Piece.re index 86205585d6..4fa01da541 100644 --- a/src/haz3lcore/tiles/Piece.re +++ b/src/haz3lcore/tiles/Piece.re @@ -84,6 +84,12 @@ let disassemble = (p: t): segment => let shapes = get(_ => None, g => Some(Grout.shapes(g)), t => Some(Tile.shapes(t))); +let is_convex = (p: t): bool => + switch (shapes(p)) { + | Some((Convex, Convex)) => true + | _ => false + }; + let is_grout: t => bool = fun | Grout(_) => true diff --git a/src/haz3lcore/zipper/Editor.re b/src/haz3lcore/zipper/Editor.re index d638d246d5..3004070f9d 100644 --- a/src/haz3lcore/zipper/Editor.re +++ b/src/haz3lcore/zipper/Editor.re @@ -249,3 +249,15 @@ let map_projectors = (f: (Id.t, Projector.t) => Projector.t, ed: t) => z => {...z, projectors: Projector.Map.mapi(f, z.projectors)}, ed, ); + +//TODO(andrew): use or lose +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)) { + | Some(tile) => Some(Tile(tile)) + | None => + List.find_opt((g: Grout.t) => g.id == id, ed.state.meta.holes) + |> Option.map(g => Piece.Grout(g)) + }; +}; diff --git a/src/haz3lcore/zipper/action/Action.re b/src/haz3lcore/zipper/action/Action.re index 93b1cffebf..5fcb01ea5c 100644 --- a/src/haz3lcore/zipper/action/Action.re +++ b/src/haz3lcore/zipper/action/Action.re @@ -70,7 +70,8 @@ module Failure = { | Cant_insert | Cant_destruct | Cant_select - | Cant_put_down; + | Cant_put_down + | Cant_project; }; module Result = { diff --git a/src/haz3lcore/zipper/action/Indicated.re b/src/haz3lcore/zipper/action/Indicated.re index 3df1f3cb5c..f9e3a3fcd4 100644 --- a/src/haz3lcore/zipper/action/Indicated.re +++ b/src/haz3lcore/zipper/action/Indicated.re @@ -85,10 +85,11 @@ let shard_index = (z: Zipper.t): option(int) => } }; +let for_index = + piece'(~no_ws=false, ~ign=Piece.is_secondary, ~trim_secondary=false); + let index = (z: Zipper.t): option(Id.t) => - switch ( - piece'(~no_ws=false, ~ign=Piece.is_secondary, ~trim_secondary=false, z) - ) { + switch (for_index(z)) { | None => None | Some((p, _, _)) => Some(Piece.id(p)) }; diff --git a/src/haz3lcore/zipper/action/Move.re b/src/haz3lcore/zipper/action/Move.re index 55eae54546..a60c4149ff 100644 --- a/src/haz3lcore/zipper/action/Move.re +++ b/src/haz3lcore/zipper/action/Move.re @@ -82,11 +82,12 @@ 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) => { - print_endline("Move.primary"); 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) + /* Need this case to avoid moving sub-caret onto projectors: */ + | _ when Zipper.projector_move(d, z) != None => Zipper.move(d, z) | (Left, Outer, (CanEnter(dlm, c_max), _)) => inner_end(d, dlm, c_max, z) | (Left, Outer, _) => Zipper.move(d, z) diff --git a/src/haz3lcore/zipper/action/Perform.re b/src/haz3lcore/zipper/action/Perform.re index 7ef1124719..ae7508b1b2 100644 --- a/src/haz3lcore/zipper/action/Perform.re +++ b/src/haz3lcore/zipper/action/Perform.re @@ -49,7 +49,7 @@ let go_z = } }; - let selection_dance = (z, d, pid): t => { + 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)); @@ -77,53 +77,11 @@ let go_z = }; }; - let la = (id, z: t, pid, d) => - switch (Projector.Map.find(id, z.projectors)) { - | Some(p) => - switch (p) { - | Fold => - let f = _ => - //TODO(andrew) - Some(Projector.Infer({expected_ty: None})); - {...z, projectors: Projector.Map.update(id, f, z.projectors)}; - | Infer(_) => { - ...z, - projectors: Projector.Map.remove(id, z.projectors), - } - } - | None => - let z = { - ...z, - projectors: Projector.Map.add(id, Projector.Fold, z.projectors), - }; - selection_dance(z, d, pid); - }; - - let proj_loj = (p: Action.project, z: t, pid, d) => - switch (p) { - | ToggleFold => - print_endline("Project.go: ToggleFold"); - switch (Indicated.index(z)) { - | Some(id) => la(id, z, pid, d) - | None => z - }; - | Toggle(id) => - print_endline("Project.go: Toggle Id"); - la(id, z, pid, d); - }; - switch (a) { - | Project(p) => - switch ( - Indicated.piece'( - ~no_ws=false, - ~ign=Piece.is_secondary, - ~trim_secondary=false, - z, - ) - ) { - | None => Error(Action.Failure.Cant_move) - | Some((pid, d, _)) => Ok(proj_loj(p, z, pid, d)) + | Project(a) => + switch (ProjectorAction.go(a, z)) { + | None => Error(Action.Failure.Cant_project) + | Some(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 e02fb281e7..7ec201d34e 100644 --- a/src/haz3lcore/zipper/action/ProjectorAction.re +++ b/src/haz3lcore/zipper/action/ProjectorAction.re @@ -47,3 +47,68 @@ let of_zipper = (z: Zipper.t): Zipper.t => { }, }; }; + +let move_out_of_piece = + (d: Util.Direction.t, rel: Indicated.relation, z: Zipper.t): Zipper.t => + /* Might not work for pieces with more than 2 delims */ + switch (rel) { + | Sibling => {...z, caret: Outer} + | Parent => + switch (Zipper.move(d, {...z, caret: Outer})) { + | Some(z) => z + | None => z + } + }; + +let update = (f, id, z) => { + ...z, + projectors: Projector.Map.update(id, f, z.projectors), +}; + +let set = (prj, id, z) => update(_ => prj, id, z); + +let can_project = (prj: Projector.t, p: Piece.t) => + switch (prj) { + | Infer(_) => + Piece.is_convex(p) + && ( + switch (p) { + | Tile(t) => t.mold.out == Exp || t.mold.out == Pat + | _ => false + } + ) + | Fold => Piece.is_convex(p) + }; + +let default_infer: Projector.t = Infer({expected_ty: None}); + +let project = (prj, id, d, rel, z) => + z |> set(Some(prj), id) |> move_out_of_piece(d, rel) |> Option.some; + +let toggle = (id, z: Zipper.t, piece, d, rel) => + switch (Projector.Map.find(id, z.projectors)) { + | Some(Fold) => + if (can_project(default_infer, piece)) { + project(default_infer, id, d, rel, z); + } else { + Some(set(None, id, z)); + } + | Some(Infer(_)) => Some(set(None, id, z)) + | None when Piece.is_convex(piece) => + if (can_project(Fold, piece)) { + project(Fold, id, d, rel, z); + } else { + None; + } + | None => None + }; + +let go = (a: Action.project, z: Zipper.t) => + switch (Indicated.for_index(z)) { + | None => None + | Some((p, d, rel)) => + switch (a) { + | ToggleFold => toggle(Piece.id(p), z, p, d, rel) + | Toggle(id) => toggle(id, z, p, d, rel) + } + };