Skip to content

Commit

Permalink
Nests with single constructor are ADTs
Browse files Browse the repository at this point in the history
Before this commit, nests in mutually recursive ADTs with a single
constructor are always considered as enums.

Now, we consider such nests as ADTs.
  • Loading branch information
Halbaroth committed Apr 22, 2024
1 parent c4b46cb commit c5f5834
Show file tree
Hide file tree
Showing 2 changed files with 6 additions and 1 deletion.
2 changes: 1 addition & 1 deletion src/lib/frontend/d_cnf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -747,7 +747,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
Array.length dstrs = 0 && is_enum
) cases ([], true)
in
if is_enum
if is_enum && not contains_adts
then (
let ty = Ty.tsum name cns in
Cache.store_ty (DE.Ty.Const.hash ty_c) ty;
Expand Down
5 changes: 5 additions & 0 deletions src/lib/frontend/typechecker.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2538,6 +2538,11 @@ let rec type_decl (acc, env) d assertion_stack =
| TypeDecl l ->
let not_rec, are_rec = partition_non_rec l in

let not_rec, are_rec =
if Lists.is_empty are_rec then not_rec, are_rec
else [], List.rev_append not_rec are_rec
in

(* A. Typing types that are not recursive *)
let acc, env =
List.fold_left
Expand Down

0 comments on commit c5f5834

Please sign in to comment.