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

re-orgnize type definition before normalizing #63

Merged
merged 2 commits into from
Aug 23, 2024
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 9 additions & 5 deletions lib/typing/check.ml
Original file line number Diff line number Diff line change
Expand Up @@ -338,22 +338,26 @@ and check_ty_def_group defs env =
Env.add_type_def (I.TDOpaque (name, [])) env)
env defs
in
let normalized_defs, env =
let defs = Util.reorg_ty_defs defs in
let normalized_defs, env, _ =
List.fold_left
(fun (acc, env) def ->
(fun (acc, env, normalize_env) def ->
match def with
| T.TDAdt (name, ty_para_names, _) as def_ext ->
let tid = Env.mk_tid name env in
let def = normalize_def def_ext normalize_env in
let[@warning "-8"] (I.TDAdt (_, _, bs)) = def in
let env = Env.add_type_def def env in
let normalize_env = Env.add_type_def def normalize_env in
let constructors = analyze_constructors tid ty_para_names bs in
let env = Env.add_constrs constructors env in
(TopTypeDef def :: acc, env)
(TopTypeDef def :: acc, env, normalize_env)
| _ as def_ext ->
let def = normalize_def def_ext normalize_env in
(TopTypeDef def :: acc, Env.add_type_def def env))
([], env) defs
( TopTypeDef def :: acc,
Env.add_type_def def env,
Env.add_type_def def normalize_env ))
([], env, normalize_env) defs
in
(normalized_defs, env)

Expand Down
58 changes: 58 additions & 0 deletions lib/typing/util.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
module P = Syntax.Parsetree

(** Two invariants must hold:
1. A new type definition can be correctly normalize
when its componnet type expressionss can be correctly
normalized
2. A type expression that indicate a type alias,
can be correctly normalized when the normalized alias
definition already added in environment.
*)
let reorg_ty_defs (defs : P.ty_def list) =
(* analyze alias dependency *)
let analyze_deps defs =
List.fold_left
(fun acc def ->
match def with
| P.TDAlias (_, P.TCons (alias, _)) -> (
match
List.find_opt
(fun def ->
match def with
| P.TDAdt (name', _, _)
| P.TDRecord (name', _, _)
| P.TDAlias (name', _) ->
alias = name')
defs
with
| Some def' -> (def, def') :: acc
| None -> acc)
| _ -> acc)
[] defs
|> List.rev
in
let graph = analyze_deps defs in
let alias_defs, no_alias_defs =
List.fold_left
(fun (ads, nads) def ->
match def with
| P.TDAlias _ -> (def :: ads, nads)
| _ -> (ads, def :: nads))
([], []) defs
in
let no_alias_defs = List.rev no_alias_defs in
let visited = ref [] in
let rec dfs graph cluster node =
if not (List.memq node !visited) then (
Copy link
Owner Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Report an error when circle detected

let cluster = node :: cluster in
visited := node :: !visited;
match List.assoc_opt node graph with
| Some neighber when List.memq neighber alias_defs ->
dfs graph cluster neighber
| _ -> cluster)
else cluster
in
let clusters =
List.fold_left (fun acc def -> dfs graph [] def :: acc) [] alias_defs
in
List.flatten (List.rev clusters) @ no_alias_defs
1 change: 0 additions & 1 deletion tests/cram/test_dirs/interp.t/test_rec_ty.fun
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@ and 'a forest =
| EmptyForest
| ConsForest of ('a tree * 'a forest)


let x = Node (1, ConsForest (Leaf 1, EmptyForest))

let _ =
Expand Down
41 changes: 41 additions & 0 deletions tests/regular/typing_test.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1203,6 +1203,47 @@ external print_int : int -> int = "ff_builtin_print_int"
(TopTypeDef
(TDAdt additive ()
((Add ((TTuple ((TCons (0 atom) ()) (TCons (0 atom) ())))))))))
|}];
print_typed
{|
type 'a list =
| Nil
| Cons of ('a * 'a list)

type env = int list

and t =
| Closure of (string * env)

let x = Closure ("x", Nil)

|};
[%expect
{|
((TopTypeDef
(TDAdt list ('a/0)
((Nil ())
(Cons ((TTuple ((TQVar 'a/0) (TCons (0 list) ((TQVar 'a/0))))))))))
(TopTypeDef
(TDAdt t ()
((Closure
((TTuple
((TCons (0 string) ()) (TCons (0 list) ((TCons (0 int) ()))))))))))
(TopTypeDef (TDAlias env (TCons (0 list) ((TCons (0 int) ())))))
(TopLet x
(EApp
(ECons Closure 0
(TArrow
(TTuple
((TCons (0 string) ()) (TCons (0 list) ((TCons (0 int) ())))))
(TCons (0 t) ())))
(ETuple
((EConst (CString "\"x\"") (TCons (0 string) ()))
(ECons Nil 0 (TCons (0 list) ((TVar (Link (TCons (0 int) ())))))))
(TTuple
((TCons (0 string) ())
(TCons (0 list) ((TVar (Link (TCons (0 int) ()))))))))
(TVar (Link (TCons (0 t) ()))))))
|}]

let%expect_test "Error reporting test" =
Expand Down
53 changes: 53 additions & 0 deletions tests/regular/typing_util_test.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,53 @@
open Syntax.Parsing
open Typing
module U = Util
module P = Syntax.Parsetree

let print_sexp s =
Printf.printf "%s\n" (Sexplib.Sexp.to_string_hum ?indent:(Some 2) s)

let%expect_test "Test: type def reorg" =
let print_ty_defs_reorgnized str =
Ident.refresh ();
let prog = parse_string_program str in
let[@warning "-8"] (Some defs) =
List.find_map
(fun top ->
match top with
| P.TopTypeDef defs -> Some defs
| _ -> None)
prog
in
defs |> U.reorg_ty_defs |> P.sexp_of_ty_def_group |> print_sexp
in
print_ty_defs_reorgnized {|
type z = y

and y = x

and x = int
|};
[%expect
{|
((TDAlias x (TCons int ())) (TDAlias y (TCons x ()))
(TDAlias z (TCons y ())))
|}];

print_ty_defs_reorgnized
{|
type z = y

and y = x

and x = int

and a = x

and b = a
and c = b
|};
[%expect
{|
((TDAlias x (TCons int ())) (TDAlias a (TCons x ())) (TDAlias b (TCons a ()))
(TDAlias c (TCons b ())) (TDAlias y (TCons x ())) (TDAlias z (TCons y ())))
|}]
Loading