Skip to content

Commit

Permalink
Merge branch 'dev' of github.com:hazelgrove/hazel into projectors
Browse files Browse the repository at this point in the history
  • Loading branch information
disconcision committed Apr 30, 2024
2 parents a08e621 + 34e33a0 commit 7e39389
Showing 1 changed file with 11 additions and 9 deletions.
20 changes: 11 additions & 9 deletions src/haz3lcore/statics/Statics.re
Original file line number Diff line number Diff line change
Expand Up @@ -64,21 +64,23 @@ 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) {
| Unknown(_) => true
| Arrow(_) => true
| Forall(_, t) => is_arrow_like(t)
| _ => false
};
};

let is_recursive = (ctx, p, def, syn: Typ.t) => {
switch (Term.UPat.get_num_of_vars(p), Term.UExp.get_num_of_functions(def)) {
| (Some(num_vars), Some(num_fns))
when num_vars != 0 && num_vars == num_fns =>
switch (Typ.normalize(ctx, syn)) {
| Unknown(_)
| Arrow(_) => num_vars == 1
| Prod(syns) when List.length(syns) == num_vars =>
syns
|> List.for_all(
fun
| Typ.Unknown(_)
| Arrow(_) => true
| _ => false,
)
syns |> List.for_all(is_arrow_like)
| t when is_arrow_like(t) => num_vars == 1
| _ => false
}
| _ => false
Expand Down

0 comments on commit 7e39389

Please sign in to comment.