From dac2dff99677401ae79004da899b42a21c5adff0 Mon Sep 17 00:00:00 2001 From: butterunderflow Date: Wed, 21 Aug 2024 23:50:49 +0800 Subject: [PATCH] support recursive type definition --- lib/syntax/parser.mly | 34 +++++---- lib/syntax/parsetree.ml | 6 +- lib/typing/check.ml | 76 ++++++++++++------- lib/typing/typedtree.ml | 1 + lib/typing/types_in.ml | 4 +- tests/cram/test_dirs/interp.t/run.t | 6 ++ tests/cram/test_dirs/interp.t/test_interp.fun | 19 +++++ tests/regular/parse_test.ml | 33 ++++++-- tests/regular/typing_test.ml | 22 ++++++ 9 files changed, 148 insertions(+), 53 deletions(-) create mode 100644 tests/cram/test_dirs/interp.t/run.t create mode 100644 tests/cram/test_dirs/interp.t/test_interp.fun diff --git a/lib/syntax/parser.mly b/lib/syntax/parser.mly index aeff2e3..b395a25 100644 --- a/lib/syntax/parser.mly +++ b/lib/syntax/parser.mly @@ -94,17 +94,20 @@ program: top_levels: | (* empty *) { [] } - | td=type_def rest=top_levels + | td=type_def_group rest=top_levels { - TopTypeDef td :: rest } + TopTypeDef td :: rest + } | LET x=IDENT EQ e=expr rest=top_levels { TopLet (x, e) - :: rest } + :: rest + } | LET REC funcs=separated_list(AND, function_bind) rest=top_levels { TopLetRec funcs - :: rest } + :: rest + } | EXTERNAL x=IDENT COLON te=type_expr EQ s=STRING rest=top_levels { TopExternal (x, te, String.(sub s 1 (length s - 2))) @@ -148,22 +151,25 @@ functor_bind: { (m_name, (mp, m_body)) } type_def: - | TYPE LPAREN tvs=separated_list(COMMA, TYPEVAR) RPAREN n=IDENT - EQ OR? vs=separated_list(OR, variant) %prec over_TOP + | LPAREN tvs=separated_list(COMMA, TYPEVAR) RPAREN n=IDENT EQ + OR? vs=separated_list(OR, variant) %prec over_TOP { TDAdt (n, (List.map Ident.from tvs), vs) } - | TYPE UNIT n=IDENT - EQ OR? vs=separated_list(OR, variant) %prec over_TOP + | UNIT n=IDENT EQ + OR? vs=separated_list(OR, variant) %prec over_TOP { TDAdt (n, [], vs) } - | TYPE tv=TYPEVAR n=IDENT + | tv=TYPEVAR n=IDENT EQ OR? vs=separated_list(OR, variant) %prec over_TOP { TDAdt (n, [ Ident.from tv ], vs) } - | TYPE n=IDENT - EQ OR? vs=separated_list(OR, variant) %prec over_TOP + | n=IDENT EQ OR? vs=separated_list(OR, variant) %prec over_TOP { TDAdt (n, [], vs) } - | TYPE n=IDENT - EQ te=type_expr %prec over_TOP + | n=IDENT EQ te=type_expr %prec over_TOP { TDAlias (n, te) } + +type_def_group: + | TYPE defs=separated_nonempty_list(AND, type_def) { defs } +; + pattern: | n=IDENT { PVar n } (* variable pattern *) | c=constant { PVal c } @@ -280,7 +286,7 @@ sig_comp: { SpecAbstTy (t, (List.map Ident.from tvs)) } | TYPE UNIT t=IDENT { SpecAbstTy (t, []) } - | def=type_def { SpecManiTy def } + | def=type_def_group { SpecManiTy def } | MODULE m_name=MIDENT COLON mt=mod_type { SpecMod (m_name, mt) } ; diff --git a/lib/syntax/parsetree.ml b/lib/syntax/parsetree.ml index 0b0352d..54ef50d 100644 --- a/lib/syntax/parsetree.ml +++ b/lib/syntax/parsetree.ml @@ -27,7 +27,7 @@ and program = top_level list and top_level = | TopLet of string * expr | TopLetRec of (string * lambda) list - | TopTypeDef of ty_def + | TopTypeDef of ty_def_group | TopMod of string * mod_expr | TopModSig of string * mod_ty | TopExternal of string * ty * string @@ -91,7 +91,7 @@ and adt_def = string * ty_paras * evariant list and spec = | SpecVal of string * ty | SpecAbstTy of string * ty_paras - | SpecManiTy of ty_def + | SpecManiTy of ty_def_group | SpecMod of (string * mod_ty) and ty = @@ -107,6 +107,8 @@ and ty_def = | TDRecord of string * ty_paras * (string * ty) list | TDAlias of string * ty +and ty_def_group = ty_def list + and ty_paras = Ident.ident list and mod_ty = diff --git a/lib/typing/check.ml b/lib/typing/check.ml index c45acce..d0ae8d1 100644 --- a/lib/typing/check.ml +++ b/lib/typing/check.ml @@ -294,51 +294,71 @@ and check_ann e te env = e_typed (* typing top levels *) -and check_top_level (top : T.top_level) env : top_level * Env.t = +and check_top_level (top : T.top_level) env : top_level list * Env.t = let old_pool = !tv_pool in reset_pool (); - let top_typed = + let tops_typed, env = match top with | T.TopLet (x, e) -> let e_typed0, env = check_let_binding x e env in - (TopLet (x, e_typed0), env) + ([ TopLet (x, e_typed0) ], env) | T.TopLetRec binds -> let env, vars, lams = check_letrec_binding binds env in let binds = List.combine vars lams in - (TopLetRec binds, env) - | T.TopTypeDef (TDAdt (name, ty_para_names, _) as def_ext) -> - let tid = Env.mk_tid name env in - - let normalize_env = - (* special environment for normalizing type definition, with typed - definition pushed as an opaque type *) - Env.add_type_def (I.TDOpaque (name, ty_para_names)) 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 constructors = analyze_constructors tid ty_para_names bs in - let env = Env.add_constrs constructors env in - (TopTypeDef def, env) - | T.TopTypeDef (_ as def_ext) -> - let def = normalize_def def_ext env in - (TopTypeDef def, Env.add_type_def def env) + ([ TopLetRec binds ], env) + | T.TopTypeDef defs -> + let defs, env = check_ty_def_group defs env in + (defs, env) | T.TopMod (name, me) -> let me_typed = check_mod me env in - ( TopMod (name, me_typed), + ( [ TopMod (name, me_typed) ], Env.add_module name (get_mod_ty me_typed) env ) | T.TopModSig (name, ext_mt) -> let mt = normalize_mt ext_mt env in - (TopModSig (name, mt), Env.add_module_sig name mt env) + ([ TopModSig (name, mt) ], Env.add_module_sig name mt env) | T.TopExternal (name, e_ty, ext_name) -> P.enter_level (); let te = normalize e_ty Let env in P.exit_level (); let gen = P.generalize te env in - (TopExternal (name, te, ext_name), Env.add_value name gen env) + ([ TopExternal (name, te, ext_name) ], Env.add_value name gen env) in tv_pool := old_pool; - top_typed + (tops_typed, env) + +and check_ty_def_group defs env = + (* Create a temporary special environment for normalizing type definition, + with typed definition pushed as an opaque type. We push type definitions + to this environment by first *) + let normalize_env = + List.fold_left + (fun env def -> + match def with + | T.TDAdt (name, ty_para_names, _) -> + Env.add_type_def (I.TDOpaque (name, ty_para_names)) env + | T.TDRecord (name, _, _) + | T.TDAlias (name, _) -> + Env.add_type_def (I.TDOpaque (name, [])) env) + env defs + in + let normalized_defs, env = + List.fold_left + (fun (acc, 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 constructors = analyze_constructors tid ty_para_names bs in + let env = Env.add_constrs constructors env in + (TopTypeDef def :: acc, env) + | _ as def_ext -> + let def = normalize_def def_ext normalize_env in + (TopTypeDef def :: acc, Env.add_type_def def env)) + ([], env) defs + in + (normalized_defs, env) and analyze_constructors (tid : I.ty_id) para_names (bs : I.variant list) : (string * (I.bind_ty * int)) list = @@ -365,9 +385,9 @@ and check_top_levels (prog : T.top_level list) env : program * Env.t = match prog with | [] -> ([], env) | top :: rest -> - let top_typed0, env = check_top_level top env in - let rest_typed1, env = check_top_levels rest env in - (top_typed0 :: rest_typed1, env) + let tops_typed0, env = check_top_level top env in + let rest_tops_typed1, env = check_top_levels rest env in + (tops_typed0 @ rest_tops_typed1, env) and make_mt_by_scope { diff --git a/lib/typing/typedtree.ml b/lib/typing/typedtree.ml index 42b8b93..45d84af 100644 --- a/lib/typing/typedtree.ml +++ b/lib/typing/typedtree.ml @@ -46,6 +46,7 @@ and top_level = | TopLet of string * expr | TopLetRec of (string * lambda_typed) list | TopTypeDef of ty_def + (* type definitions in typedtree are free to recursive by design *) | TopMod of string * mod_expr | TopModSig of string * mod_ty | TopExternal of string * ty * string diff --git a/lib/typing/types_in.ml b/lib/typing/types_in.ml index 5a38678..59915ab 100644 --- a/lib/typing/types_in.ml +++ b/lib/typing/types_in.ml @@ -97,7 +97,7 @@ let get_def_name (td : ty_def) = | TDAlias (name, _) -> name -let get_def name ty_defs = +let get_def name ty_def_group = List.find (fun td -> match td with @@ -108,4 +108,4 @@ let get_def name ty_defs = when name' = name -> true | _ -> false) - ty_defs + ty_def_group diff --git a/tests/cram/test_dirs/interp.t/run.t b/tests/cram/test_dirs/interp.t/run.t new file mode 100644 index 0000000..304a6e4 --- /dev/null +++ b/tests/cram/test_dirs/interp.t/run.t @@ -0,0 +1,6 @@ + + $ $FF test_interp.fun + + $ ./test_interp.fun.out + + diff --git a/tests/cram/test_dirs/interp.t/test_interp.fun b/tests/cram/test_dirs/interp.t/test_interp.fun new file mode 100644 index 0000000..c2d16ab --- /dev/null +++ b/tests/cram/test_dirs/interp.t/test_interp.fun @@ -0,0 +1,19 @@ +external println_str : string -> unit = "ff_builtin_println_str" + +external add : int -> int -> int = "ff_builtin_add" + +type 'a tree = + | Leaf of 'a + | Node of ('a * 'a forest) + +and 'a forest = + | EmptyForest + | ConsForest of ('a tree * 'a forest) + + +let x = Node (1, ConsForest (Leaf 1, EmptyForest)) + +let _ = + match x with + | Node (x, ConsForest (Leaf 2, EmptyForest)) -> println_str "Matched first!" + | Node (x, ConsForest (Leaf 1, EmptyForest)) -> println_str "Matched second!" diff --git a/tests/regular/parse_test.ml b/tests/regular/parse_test.ml index 0bc3609..203fbb8 100644 --- a/tests/regular/parse_test.ml +++ b/tests/regular/parse_test.ml @@ -815,7 +815,7 @@ let%expect_test "Test: full program parsing" = (MERestrict ((desc (MEStruct - ((TopTypeDef (TDAdt t () ((Nil ())))) + ((TopTypeDef ((TDAdt t () ((Nil ()))))) (TopLet x ((desc (ECons Nil)) (start_loc @@ -845,7 +845,7 @@ let%expect_test "Test: full program parsing" = [%expect {| ((TopModSig MIntf - (MTSig ((SpecManiTy (TDAdt t () ((Nil ())))) (SpecVal x (TCons t ())))))) + (MTSig ((SpecManiTy ((TDAdt t () ((Nil ()))))) (SpecVal x (TCons t ())))))) |}]; print_parsed_program @@ -950,7 +950,7 @@ functor type t = a list -> b |}; [%expect - {| ((TopTypeDef (TDAlias t (TArrow (TCons list ((TCons a ()))) (TCons b ()))))) |}]; + {| ((TopTypeDef ((TDAlias t (TArrow (TCons list ((TCons a ()))) (TCons b ())))))) |}]; print_parsed_program {| external x : int -> int -> int = "ff_add" @@ -1213,12 +1213,12 @@ let result = print_int (sum 4) {| type 'a t = Nil |}; - [%expect {| ((TopTypeDef (TDAdt t ('a/0) ((Nil ()))))) |}]; + [%expect {| ((TopTypeDef ((TDAdt t ('a/0) ((Nil ())))))) |}]; print_parsed_program {| type t = | Nil |}; - [%expect {| ((TopTypeDef (TDAdt t () ((Nil ()))))) |}]; + [%expect {| ((TopTypeDef ((TDAdt t () ((Nil ())))))) |}]; print_parsed_program {| let x = let rec f = fun x -> 1 @@ -1261,6 +1261,25 @@ let result = print_int (sum 4) (start_loc ((pos_fname "") (pos_lnum 5) (pos_bol 87) (pos_cnum 100))) (end_loc ((pos_fname "") (pos_lnum 5) (pos_bol 87) (pos_cnum 101))) (attrs ())))) + |}]; + print_parsed_program + {| + type additive = + | Add of (atom * atom) + and () multiple = + | Mul of (additive * additive) + | Div of (additive * additive) + and atom = + | Var of string + |}; + [%expect + {| + ((TopTypeDef + ((TDAdt additive () ((Add ((TTuple ((TCons atom ()) (TCons atom ()))))))) + (TDAdt multiple () + ((Mul ((TTuple ((TCons additive ()) (TCons additive ()))))) + (Div ((TTuple ((TCons additive ()) (TCons additive ()))))))) + (TDAdt atom () ((Var ((TCons string ())))))))) |}] let%expect_test "Test: path parsing" = @@ -1514,7 +1533,7 @@ let%expect_test "Test: module expression" = ((pos_fname "") (pos_lnum 3) (pos_bol 14) (pos_cnum 29))) (end_loc ((pos_fname "") (pos_lnum 3) (pos_bol 14) (pos_cnum 30))) (attrs ()))) - (TopTypeDef (TDAdt a () ((Cons ((TCons int ()))) (Nil ()))))))) + (TopTypeDef ((TDAdt a () ((Cons ((TCons int ()))) (Nil ())))))))) (start_loc ((pos_fname "") (pos_lnum 2) (pos_bol 1) (pos_cnum 6))) (end_loc ((pos_fname "") (pos_lnum 8) (pos_bol 91) (pos_cnum 99))) (attrs ())) @@ -1594,5 +1613,5 @@ let%expect_test "Test: module type" = (MTSig ((SpecVal x (TCons int ())) (SpecAbstTy t ()) (SpecVal m (TArrow (TCons t ()) (TCons t ()))) - (SpecManiTy (TDAdt i_list () ((Cons ((TCons int ()))) (Nil ())))))) + (SpecManiTy ((TDAdt i_list () ((Cons ((TCons int ()))) (Nil ()))))))) |}] diff --git a/tests/regular/typing_test.ml b/tests/regular/typing_test.ml index 0900b25..1b2753a 100644 --- a/tests/regular/typing_test.ml +++ b/tests/regular/typing_test.ml @@ -1181,6 +1181,28 @@ external print_int : int -> int = "ff_builtin_print_int" (mod_sigs ()) (mod_defs ()) (owned_mods ())) (MTMod (id 5) (val_defs ()) (constr_defs ()) (ty_defs ((TDOpaque t ()))) (mod_sigs ()) (mod_defs ()) (owned_mods ()))))) + |}]; + + print_typed + {| + type additive = + | Add of (atom * atom) + and () multiple = + | Mul of (additive * additive) + | Div of (additive * additive) + and atom = + | Int of int + |}; + [%expect + {| + ((TopTypeDef (TDAdt atom () ((Int ((TCons (0 int) ())))))) + (TopTypeDef + (TDAdt multiple () + ((Mul ((TTuple ((TCons (0 additive) ()) (TCons (0 additive) ()))))) + (Div ((TTuple ((TCons (0 additive) ()) (TCons (0 additive) ())))))))) + (TopTypeDef + (TDAdt additive () + ((Add ((TTuple ((TCons (0 atom) ()) (TCons (0 atom) ()))))))))) |}] let%expect_test "Error reporting test" =