Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Updated-tutorial-systems #1414

Draft
wants to merge 12 commits into
base: dev
Choose a base branch
from
Prev Previous commit
Next Next commit
updated formatter
reevafaisal committed Nov 5, 2024
commit e1bf64404d12166869dd5013c294f751b55663f3
87 changes: 12 additions & 75 deletions src/haz3lcore/Measured.re
Original file line number Diff line number Diff line change
@@ -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) => {
@@ -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(
@@ -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)
@@ -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) =
25 changes: 5 additions & 20 deletions src/haz3lcore/assistant/AssistantCtx.re
Original file line number Diff line number Diff line change
@@ -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;
};
@@ -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,
);
@@ -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,
);
@@ -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,
);
@@ -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,
);
17 changes: 3 additions & 14 deletions src/haz3lcore/assistant/AssistantForms.re
Original file line number Diff line number Diff line change
@@ -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)})
};
};

15 changes: 2 additions & 13 deletions src/haz3lcore/assistant/TyDi.re
Original file line number Diff line number Diff line change
@@ -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)},
]
| _ => []
}
@@ -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
13 changes: 2 additions & 11 deletions src/haz3lcore/dynamics/Builtins.re
Original file line number Diff line number Diff line change
@@ -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)
12 changes: 2 additions & 10 deletions src/haz3lcore/dynamics/Casts.re
Original file line number Diff line number Diff line change
@@ -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)
@@ -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));
{
46 changes: 6 additions & 40 deletions src/haz3lcore/dynamics/DHExp.re
Original file line number Diff line number Diff line change
@@ -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
6 changes: 1 addition & 5 deletions src/haz3lcore/dynamics/Elaborator.re
Original file line number Diff line number Diff line change
@@ -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) =>
Loading