projection types are now gated by syntactic predicate. projection car…

…et dance is now more performant.

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

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))
+  };
+};

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 = {

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))
   };

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)

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)

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)
+    }
+  };