Skip to content

Commit

Permalink
Merge branch 'dev' into remove-dhexp
Browse files Browse the repository at this point in the history
  • Loading branch information
Negabinary committed May 2, 2024
2 parents f42c61d + a263747 commit 79c9b6a
Show file tree
Hide file tree
Showing 2 changed files with 19 additions and 13 deletions.
5 changes: 4 additions & 1 deletion src/haz3lcore/lang/Form.re
Original file line number Diff line number Diff line change
Expand Up @@ -302,7 +302,10 @@ let forms: list((string, t)) = [
("ap_exp", mk(ii, ["(", ")"], mk_post(P.ap, Exp, [Exp]))),
("ap_pat", mk(ii, ["(", ")"], mk_post(P.ap, Pat, [Pat]))),
("ap_typ", mk(ii, ["(", ")"], mk_post(P.ap, Typ, [Typ]))),
("ap_exp_typ", mk(ii, ["@<", ">"], mk_post(P.ap, Exp, [Typ]))),
(
"ap_exp_typ",
mk((Instant, Static), ["@<", ">"], mk_post(P.ap, Exp, [Typ])),
),
("at_sign", mk_nul_infix("@", P.eqs)), // HACK: SUBSTRING REQ
("case", mk(ds, ["case", "end"], mk_op(Exp, [Rul]))),
("test", mk(ds, ["test", "end"], mk_op(Exp, [Exp]))),
Expand Down
27 changes: 15 additions & 12 deletions src/haz3lcore/statics/Statics.re
Original file line number Diff line number Diff line change
Expand Up @@ -65,24 +65,26 @@ let map_m = (f, xs, m: Map.t) =>
let add_info = (ids: list(Id.t), info: Info.t, m: Map.t): Map.t =>
ids |> List.fold_left((m, id) => Id.Map.add(id, info, m), m);

let rec is_arrow_like = (t: Typ.t) => {
switch (t |> Typ.term_of) {
| Unknown(_) => true
| Arrow(_) => true
| Forall(_, t) => is_arrow_like(t)
| _ => false
};
};

let is_recursive = (ctx, p, def, syn: Typ.t) => {
switch (Pat.get_num_of_vars(p), Exp.get_num_of_functions(def)) {
| (Some(num_vars), Some(num_fns))
when num_vars != 0 && num_vars == num_fns =>
switch (Typ.term_of(Typ.normalize(ctx, syn))) {
| Unknown(_)
| Arrow(_) => num_vars == 1
let norm = Typ.normalize(ctx, syn);
switch (norm |> Typ.term_of) {
| Prod(syns) when List.length(syns) == num_vars =>
syns
|> List.for_all(x =>
switch (Typ.term_of(x)) {
| Typ.Unknown(_)
| Arrow(_) => true
| _ => false
}
)
syns |> List.for_all(is_arrow_like)
| _ when is_arrow_like(norm) => num_vars == 1
| _ => false
}
};
| _ => false
};
};
Expand Down Expand Up @@ -266,6 +268,7 @@ and uexp_to_info_map =
m,
);
| ListConcat(e1, e2) =>
let mode = Mode.of_list_concat(ctx, mode);
let ids = List.map(UExp.rep_id, [e1, e2]);
let (e1, m) = go(~mode, e1, m);
let (e2, m) = go(~mode, e2, m);
Expand Down

0 comments on commit 79c9b6a

Please sign in to comment.