Skip to content

Commit

Permalink
updated formatter
Browse files Browse the repository at this point in the history
  • Loading branch information
reevafaisal committed Nov 5, 2024
1 parent 3285b47 commit e1bf644
Show file tree
Hide file tree
Showing 117 changed files with 495 additions and 2,491 deletions.
87 changes: 12 additions & 75 deletions src/haz3lcore/Measured.re
Original file line number Diff line number Diff line change
Expand Up @@ -128,13 +128,7 @@ let rec add_n_rows = (origin: Point.t, row_indent, n: abs_indent, map: t): t =>
| _ =>
map
|> add_n_rows(origin, row_indent, n - 1)
|> add_row(
origin.row + n - 1,
{
indent: row_indent,
max_col: origin.col,
},
)
|> add_row(origin.row + n - 1, {indent: row_indent, max_col: origin.col})
};

let add_lb = (id, indent, map) => {
Expand Down Expand Up @@ -186,10 +180,7 @@ let find_t = (t: Tile.t, map): measurement => {
}) {
| _ => failwith("find_t: inconsistent shard infor between tile and map")
};
{
origin: first.origin,
last: last.last,
};
{origin: first.origin, last: last.last};
};
let find_p = (~msg="", p: Piece.t, map): measurement =>
try(
Expand Down Expand Up @@ -221,10 +212,7 @@ let find_by_id = (id: Id.t, map: t): option(measurement) => {
shards,
"find_by_id",
);
Some({
origin: first.origin,
last: last.last,
});
Some({origin: first.origin, last: last.last});
| None =>
switch (Id.Map.find_opt(id, map.projectors)) {
| Some(m) => Some(m)
Expand Down Expand Up @@ -344,90 +332,39 @@ let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
contained_indent + (Id.Map.find(w.id, is_indented) ? 2 : 0);
};
let last =
Point.{
row: origin.row + 1,
col: container_indent + indent,
};
Point.{row: origin.row + 1, col: container_indent + indent};
let map =
map
|> add_w(
w,
{
origin,
last,
},
)
|> add_w(w, {origin, last})
|> add_row(
origin.row,
{
indent: row_indent,
max_col: origin.col,
},
{indent: row_indent, max_col: origin.col},
)
|> add_lb(w.id, indent);
(indent, last, map);
| Secondary(w) =>
let wspace_length =
Unicode.length(Secondary.get_string(w.content));
let last = {
...origin,
col: origin.col + wspace_length,
};
let map =
map
|> add_w(
w,
{
origin,
last,
},
);
let last = {...origin, col: origin.col + wspace_length};
let map = map |> add_w(w, {origin, last});
(contained_indent, last, map);
| Grout(g) =>
let last = {
...origin,
col: origin.col + 1,
};
let map =
map
|> add_g(
g,
{
origin,
last,
},
);
let last = {...origin, col: origin.col + 1};
let map = map |> add_g(g, {origin, last});
(contained_indent, last, map);
| Projector(p) =>
let token =
Projector.placeholder(p, Id.Map.find_opt(p.id, info_map));
let last = last_of_token(token, origin);
let map = extra_rows(token, origin, map);
let map =
add_pr(
p,
{
origin,
last,
},
map,
);
let map = add_pr(p, {origin, last}, map);
(contained_indent, last, map);
| Tile(t) =>
let add_shard = (origin, shard, map) => {
let token = List.nth(t.label, shard);
let map = extra_rows(token, origin, map);
let last = last_of_token(token, origin);
let map =
add_s(
t.id,
shard,
{
origin,
last,
},
map,
);
let map = add_s(t.id, shard, {origin, last}, map);
(last, map);
};
let (last, map) =
Expand Down
25 changes: 5 additions & 20 deletions src/haz3lcore/assistant/AssistantCtx.re
Original file line number Diff line number Diff line change
Expand Up @@ -10,10 +10,7 @@ let free_variables =
| None =>
let joint_use_typ = CoCtx.join(ctx, entries);
if (Typ.is_consistent(ctx, expected_ty, joint_use_typ)) {
Some({
content: name,
strategy: Pat(FromCoCtx(joint_use_typ)),
});
Some({content: name, strategy: Pat(FromCoCtx(joint_use_typ))});
} else {
None;
};
Expand All @@ -29,10 +26,7 @@ let bound_variables = (ty_expect: Typ.t, ctx: Ctx.t): list(Suggestion.t) =>
fun
| Ctx.VarEntry({typ, name, _})
when Typ.is_consistent(ctx, ty_expect, typ) =>
Some({
content: name,
strategy: Exp(Common(FromCtx(typ))),
})
Some({content: name, strategy: Exp(Common(FromCtx(typ)))})
| _ => None,
ctx,
);
Expand All @@ -45,10 +39,7 @@ let bound_constructors =
fun
| Ctx.ConstructorEntry({typ, name, _})
when Typ.is_consistent(ctx, ty, typ) =>
Some({
content: name,
strategy: wrap(FromCtx(typ)),
})
Some({content: name, strategy: wrap(FromCtx(typ))})
| _ => None,
ctx,
);
Expand Down Expand Up @@ -81,10 +72,7 @@ let bound_constructor_aps = (wrap, ty: Typ.t, ctx: Ctx.t): list(Suggestion.t) =>
when
Typ.is_consistent(ctx, ty, ty_out)
&& !Typ.is_consistent(ctx, ty, ty_arr) =>
Some({
content: name ++ "(",
strategy: wrap(FromCtxAp(ty_out)),
})
Some({content: name ++ "(", strategy: wrap(FromCtxAp(ty_out))})
| _ => None,
ctx,
);
Expand All @@ -94,10 +82,7 @@ let typ_context_entries = (ctx: Ctx.t): list(Suggestion.t) =>
List.filter_map(
fun
| Ctx.TVarEntry({kind: Singleton(_), name, _}) =>
Some({
content: name,
strategy: Typ(FromCtx),
})
Some({content: name, strategy: Typ(FromCtx)})
| _ => None,
ctx,
);
Expand Down
17 changes: 3 additions & 14 deletions src/haz3lcore/assistant/AssistantForms.re
Original file line number Diff line number Diff line change
Expand Up @@ -181,29 +181,18 @@ let suggest_form = (ty_map, delims_of_sort, ci: Info.t): list(Suggestion.t) => {
| Exp =>
List.map(
((content, ty)) =>
Suggestion.{
content,
strategy: Exp(Common(NewForm(ty))),
},
Suggestion.{content, strategy: Exp(Common(NewForm(ty)))},
filtered,
)
| Pat =>
List.map(
((content, ty)) =>
Suggestion.{
content,
strategy: Pat(Common(NewForm(ty))),
},
Suggestion.{content, strategy: Pat(Common(NewForm(ty)))},
filtered,
)
| _ =>
delims
|> List.map(content =>
Suggestion.{
content,
strategy: Typ(NewForm),
}
)
|> List.map(content => Suggestion.{content, strategy: Typ(NewForm)})
};
};

Expand Down
15 changes: 2 additions & 13 deletions src/haz3lcore/assistant/TyDi.re
Original file line number Diff line number Diff line change
Expand Up @@ -9,10 +9,7 @@ let suggest_backpack = (z: Zipper.t): list(Suggestion.t) => {
| [{content, _}, ..._] =>
switch (content) {
| [Tile({label, shards: [idx], _})] when Zipper.can_put_down(z) => [
{
content: List.nth(label, idx),
strategy: Any(FromBackpack),
},
{content: List.nth(label, idx), strategy: Any(FromBackpack)},
]
| _ => []
}
Expand Down Expand Up @@ -55,15 +52,7 @@ let token_to_left = (z: Zipper.t): option(string) =>
let mk_unparsed_buffer =
(~sort: Sort.t, sibs: Siblings.t, t: Token.t): Segment.t => {
let mold = Siblings.mold_fitting_between(sort, Precedence.max, sibs);
[
Tile({
id: Id.mk(),
label: [t],
shards: [0],
children: [],
mold,
}),
];
[Tile({id: Id.mk(), label: [t], shards: [0], children: [], mold})];
};

/* If 'current' is a proper prefix of 'candidate', return the
Expand Down
13 changes: 2 additions & 11 deletions src/haz3lcore/dynamics/Builtins.re
Original file line number Diff line number Diff line change
Expand Up @@ -362,18 +362,9 @@ let ctx_init: Ctx.t = {
});
List.map(
fun
| (name, Const(typ, _)) =>
Ctx.VarEntry({
name,
typ,
id: Id.invalid,
})
| (name, Const(typ, _)) => Ctx.VarEntry({name, typ, id: Id.invalid})
| (name, Fn(t1, t2, _)) =>
Ctx.VarEntry({
name,
typ: Arrow(t1, t2) |> Typ.fresh,
id: Id.invalid,
}),
Ctx.VarEntry({name, typ: Arrow(t1, t2) |> Typ.fresh, id: Id.invalid}),
Pervasives.builtins,
)
|> Ctx.extend(_, meta)
Expand Down
12 changes: 2 additions & 10 deletions src/haz3lcore/dynamics/Casts.re
Original file line number Diff line number Diff line change
Expand Up @@ -187,11 +187,7 @@ let pattern_fixup = (p: DHPat.t): DHPat.t => {
let (p1, d1) = unwrap_casts(p1);
(
p1,
{
term: DHExp.Cast(d1, t1, t2),
copied: p.copied,
ids: p.ids,
}
{term: DHExp.Cast(d1, t1, t2), copied: p.copied, ids: p.ids}
|> transition_multiple,
);
| _ => (p, hole)
Expand All @@ -202,11 +198,7 @@ let pattern_fixup = (p: DHPat.t): DHPat.t => {
| EmptyHole => p
| Cast(d1, t1, t2) =>
let p1 = rewrap_casts((p, d1));
{
term: DHPat.Cast(p1, t1, t2),
copied: d.copied,
ids: d.ids,
};
{term: DHPat.Cast(p1, t1, t2), copied: d.copied, ids: d.ids};
| FailedCast(d1, t1, t2) =>
let p1 = rewrap_casts((p, d1));
{
Expand Down
46 changes: 6 additions & 40 deletions src/haz3lcore/dynamics/DHExp.re
Original file line number Diff line number Diff line change
Expand Up @@ -11,51 +11,17 @@ let term_of: t => term = IdTagged.term_of;
let fast_copy: (Id.t, t) => t = IdTagged.fast_copy;

let mk = (ids, term): t => {
{
ids,
copied: true,
term,
};
{ids, copied: true, term};
};

// TODO: make this function emit a map of changes
let replace_all_ids =
map_term(
~f_exp=
(continue, exp) =>
{
...exp,
ids: [Id.mk()],
}
|> continue,
~f_pat=
(continue, exp) =>
{
...exp,
ids: [Id.mk()],
}
|> continue,
~f_typ=
(continue, exp) =>
{
...exp,
ids: [Id.mk()],
}
|> continue,
~f_tpat=
(continue, exp) =>
{
...exp,
ids: [Id.mk()],
}
|> continue,
~f_rul=
(continue, exp) =>
{
...exp,
ids: [Id.mk()],
}
|> continue,
~f_exp=(continue, exp) => {...exp, ids: [Id.mk()]} |> continue,
~f_pat=(continue, exp) => {...exp, ids: [Id.mk()]} |> continue,
~f_typ=(continue, exp) => {...exp, ids: [Id.mk()]} |> continue,
~f_tpat=(continue, exp) => {...exp, ids: [Id.mk()]} |> continue,
~f_rul=(continue, exp) => {...exp, ids: [Id.mk()]} |> continue,
);

// TODO: make this function emit a map of changes
Expand Down
6 changes: 1 addition & 5 deletions src/haz3lcore/dynamics/Elaborator.re
Original file line number Diff line number Diff line change
Expand Up @@ -393,11 +393,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
let kind' =
switch (kind) {
| Residue(_) => kind
| Filter({act, pat}) =>
Filter({
act,
pat: elaborate(m, pat) |> fst,
})
| Filter({act, pat}) => Filter({act, pat: elaborate(m, pat) |> fst})
};
Filter(kind', e') |> rewrap |> cast_from(t);
| Closure(env, e) =>
Expand Down
Loading

0 comments on commit e1bf644

Please sign in to comment.