Skip to content

Commit

Permalink
experiment with module type. not compiling
Browse files Browse the repository at this point in the history
  • Loading branch information
disconcision committed May 19, 2024
1 parent c7654f4 commit 97e8afa
Show file tree
Hide file tree
Showing 3 changed files with 148 additions and 77 deletions.
8 changes: 4 additions & 4 deletions src/haz3lcore/statics/TypBase.re
Original file line number Diff line number Diff line change
Expand Up @@ -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,
)
Expand All @@ -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) {
Expand Down
208 changes: 140 additions & 68 deletions src/haz3lcore/zipper/Projector.re
Original file line number Diff line number Diff line change
@@ -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);
9 changes: 4 additions & 5 deletions src/haz3lcore/zipper/action/ProjectorAction.re
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)) {
Expand Down

0 comments on commit 97e8afa

Please sign in to comment.