Skip to content

Commit

Permalink
re-orgnize type definition before normalizing (#63)
Browse files Browse the repository at this point in the history
  • Loading branch information
butterunderflow authored Aug 23, 2024
2 parents 34862ee + 6f431e0 commit 84580ac
Show file tree
Hide file tree
Showing 5 changed files with 164 additions and 6 deletions.
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
61 changes: 61 additions & 0 deletions lib/typing/util.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,61 @@
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 (
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 if List.memq node cluster then
(* Find a node in current cluster => dircle detected! *)
failwith "Find a circle in alias dependency"
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 ())))
|}]

0 comments on commit 84580ac

Please sign in to comment.