diff --git a/src/haz3lcore/statics/TypBase.re b/src/haz3lcore/statics/TypBase.re index 58690c3aec..cbb9cdd4b7 100644 --- a/src/haz3lcore/statics/TypBase.re +++ b/src/haz3lcore/statics/TypBase.re @@ -507,14 +507,14 @@ module rec Typ: { | String => "String" | Var(tvar) => tvar | List(t) => "[" ++ pretty_print(t) ++ "]" - | Arrow(t1, t2) => paren_pretty_print(t1) ++ "->" ++ pretty_print(t2) + | Arrow(t1, t2) => paren_pretty_print(t1) ++ " -> " ++ pretty_print(t2) | Sum(sm) => switch (sm) { | [] => "+?" | [t0] => "+" ++ ctr_pretty_print(t0) | [t0, ...ts] => List.fold_left( - (acc, t) => acc ++ "+" ++ ctr_pretty_print(t), + (acc, t) => acc ++ " + " ++ ctr_pretty_print(t), ctr_pretty_print(t0), ts, ) @@ -528,8 +528,8 @@ module rec Typ: { ts, ) ++ ")" - | Rec(tv, t) => "rec " ++ tv ++ "->" ++ pretty_print(t) - | Forall(tv, t) => "forall " ++ tv ++ "->" ++ pretty_print(t) + | Rec(tv, t) => "rec " ++ tv ++ " -> " ++ pretty_print(t) + | Forall(tv, t) => "forall " ++ tv ++ " -> " ++ pretty_print(t) } and ctr_pretty_print = ((ctr, typ)) => switch (typ) { diff --git a/src/haz3lcore/zipper/Projector.re b/src/haz3lcore/zipper/Projector.re index 9e65f580ff..95274faa2a 100644 --- a/src/haz3lcore/zipper/Projector.re +++ b/src/haz3lcore/zipper/Projector.re @@ -1,83 +1,155 @@ open Util; open Sexplib.Std; -[@deriving (show({with_path: false}), sexp, yojson)] -type infer = {expected_ty: option(Typ.t)}; - -[@deriving (show({with_path: false}), sexp, yojson)] -type t = - | Fold - | Infer(infer); +module type P = { + [@deriving (show({with_path: false}), sexp, yojson)] + type t; + let placeholder_length: t => int; //Projector + let to_string: t => string; //Projector //TODO: rename to ci_string or something + let can_project: (t, Piece.t) => bool; //ProjectorAction + let update: (option(Info.t), t) => t; // ProjectorsUpdate + //let toggle = (id: Id.t, z: Zipper.t, piece, d, rel) //ProjectorAction +}; -let to_string: t => string = - fun - | Fold => "F" - | Infer(_) => "I"; +module Fold: P = { + [@deriving (show({with_path: false}), sexp, yojson)] + type t = unit; + let to_string: t => string = () => "F"; + let can_project = ((): t, p: Piece.t): bool => Piece.is_convex(p); + let placeholder_length: t => int = () => 2; + let update = (_: option(Info.t), (): t): t => (); +}; -let placeholder_length: t => int = - fun - | Fold => 2 - | Infer({expected_ty: None, _}) => "-" |> String.length - | Infer({expected_ty: Some(expected_ty), _}) => - expected_ty |> Typ.pretty_print |> String.length; +module Infer: P = { + [@deriving (show({with_path: false}), sexp, yojson)] + type t = {expected_ty: option(Typ.t)}; -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 to_string: t => string = _ => "I"; + let can_project = (_: t, p: Piece.t): bool => + Piece.is_convex(p) + && ( + switch (p) { + | Tile(t) => t.mold.out == Exp || t.mold.out == Pat + | _ => false + } + ); + let placeholder_length: t => int = + fun + | {expected_ty: None, _} => "-" |> String.length + | {expected_ty: Some(expected_ty), _} => { + /* NOTE: This assumes pretty_print handles whitespace the same as view */ + //TODO(andrew): cleanup + print_endline("placeholder_ty: " ++ Typ.pretty_print(expected_ty)); + print_endline( + "placeholder_length " + ++ ( + expected_ty |> Typ.pretty_print |> String.length |> string_of_int + ), + ); + expected_ty |> Typ.pretty_print |> String.length; + }; + let update = (ci: option(Info.t), _: t): t => { + print_endline("updating infer projector"); + let expected_ty = + switch (ci) { + | Some(InfoExp({mode, _}) | InfoPat({mode, _})) => Mode.ty_of(mode) + | _ => Typ.Float + }; + {expected_ty: Some(expected_ty)}; + }; +}; [@deriving (show({with_path: false}), sexp, yojson)] -module Map = { - [@deriving (show({with_path: false}), sexp, yojson)] - type p = t; - open Id.Map; - [@deriving (show({with_path: false}), sexp, yojson)] - type t = Id.Map.t(p); - let empty = empty; - let find = find_opt; - let mem = mem; - let mapi = mapi; - let update = update; -}; +type t = + | Fold(Fold.t) + | Infer(Infer.t); -let placehold = (ps: Map.t, p: Piece.t) => - switch (Map.find(Piece.id(p), ps)) { - | None => p - | Some(pr) => placeholder(pr, Piece.id(p)) - }; +// let placeholder = (pr: P.t, id: Id.t): Piece.t => { +// Piece.Tile({ +// id, +// label: [String.make(P.placeholder_length(pr), ' ')], +// mold: Mold.mk_op(Any, []), +// shards: [0], +// children: [], +// }); +// }; +// let placeholder = (type p, module X: P with type t = p, pr: p, id: Id.t) => { +// Piece.Tile({ +// id, +// label: [String.make(X.placeholder_length(pr), ' ')], +// mold: Mold.mk_op(Any, []), +// shards: [0], +// children: [], +// }); +// }; -let rec of_segment = (projectors, seg: Segment.t): Segment.t => { - seg |> List.map(placehold(projectors)) |> List.map(of_piece(projectors)); -} -and of_piece = (projectors, p: Piece.t): Piece.t => { - switch (p) { - | Tile(t) => Tile(of_tile(projectors, t)) - | Grout(_) => p - | Secondary(_) => p +module MkProjectorM = (P: P) => { + [@deriving (show({with_path: false}), sexp, yojson)] + module Map = { + [@deriving (show({with_path: false}), sexp, yojson)] + type p = P.t; + open Id.Map; + [@deriving (show({with_path: false}), sexp, yojson)] + type t = Id.Map.t(p); + let empty = empty; + let find = find_opt; + let mem = mem; + let mapi = mapi; + let update = update; }; -} -and of_tile = (projectors, t: Tile.t): Tile.t => { - {...t, children: List.map(of_segment(projectors), t.children)}; -}; + let placeholder = (pr: P.t, id: Id.t) => { + Piece.Tile({ + id, + label: [String.make(P.placeholder_length(pr), ' ')], + mold: Mold.mk_op(Any, []), + shards: [0], + children: [], + }); + }; + let placehold = (ps: Map.t, p: Piece.t) => + switch (Map.find(Piece.id(p), ps)) { + | None => p + | Some(pr) => placeholder(pr, Piece.id(p)) + }; -let piece_is = (projectors: Map.t, p: option(Piece.t)) => - switch (p) { - | Some(p) when Map.mem(Piece.id(p), projectors) => - Map.mem(Piece.id(p), projectors) ? Some(Piece.id(p)) : None - | _ => None + let rec of_segment = (projectors, seg: Segment.t): Segment.t => { + seg + |> List.map(placehold(projectors)) + |> List.map(of_piece(projectors)); + } + and of_piece = (projectors, p: Piece.t): Piece.t => { + switch (p) { + | Tile(t) => Tile(of_tile(projectors, t)) + | Grout(_) => p + | Secondary(_) => p + }; + } + and of_tile = (projectors, t: Tile.t): Tile.t => { + {...t, children: List.map(of_segment(projectors), t.children)}; }; -let neighbor_is = (projectors, s: Siblings.t): (option(Id.t), option(Id.t)) => ( - piece_is(projectors, Siblings.left_neighbor(s)), - piece_is(projectors, Siblings.right_neighbor(s)), -); + let piece_is = (projectors: Map.t, p: option(Piece.t)) => + switch (p) { + | Some(p) when Map.mem(Piece.id(p), projectors) => + Map.mem(Piece.id(p), projectors) ? Some(Piece.id(p)) : None + | _ => None + }; + + let neighbor_is = + (projectors, s: Siblings.t): (option(Id.t), option(Id.t)) => ( + piece_is(projectors, Siblings.left_neighbor(s)), + piece_is(projectors, Siblings.right_neighbor(s)), + ); + + let selection_sides_is = + (projectors, s: Selection.t): (option(Id.t), option(Id.t)) => ( + piece_is(projectors, ListUtil.hd_opt(s.content)), + piece_is(projectors, ListUtil.last_opt(s.content)), + ); +}; + +module FoldPlaceholder = MkProjectorM(Fold); +module InferPlaceholder = MkProjectorM(Infer); -let selection_sides_is = - (projectors, s: Selection.t): (option(Id.t), option(Id.t)) => ( - piece_is(projectors, ListUtil.hd_opt(s.content)), - piece_is(projectors, ListUtil.last_opt(s.content)), -); +type tt = + | A(FoldPlaceholder.t); diff --git a/src/haz3lcore/zipper/action/ProjectorAction.re b/src/haz3lcore/zipper/action/ProjectorAction.re index 70172fe30e..f6155319e5 100644 --- a/src/haz3lcore/zipper/action/ProjectorAction.re +++ b/src/haz3lcore/zipper/action/ProjectorAction.re @@ -70,7 +70,7 @@ let update = (f, id, z) => { let set = (prj, id, z) => update(_ => prj, id, z); -let can_project = (prj: Projector.t, p: Piece.t) => +let can_project = (prj: Projector.t, p: Piece.t): bool => switch (prj) { | Infer(_) => Piece.is_convex(p) @@ -83,19 +83,18 @@ let can_project = (prj: Projector.t, p: Piece.t) => | 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) => +let toggle = (id: Id.t, z: Zipper.t, piece, d, rel) => switch (Projector.Map.find(id, z.projectors)) { | Some(Fold) => + let default_infer = Projector.Infer({expected_ty: None}); 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)) {