Skip to content

Commit

Permalink
support recursive type definition (#60)
Browse files Browse the repository at this point in the history
  • Loading branch information
butterunderflow authored Aug 21, 2024
2 parents 10e7f20 + 9ddde16 commit 455d785
Show file tree
Hide file tree
Showing 9 changed files with 149 additions and 53 deletions.
34 changes: 20 additions & 14 deletions lib/syntax/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -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)))
Expand Down Expand Up @@ -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 }
Expand Down Expand Up @@ -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) }
;

Expand Down
6 changes: 4 additions & 2 deletions lib/syntax/parsetree.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 =
Expand All @@ -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 =
Expand Down
76 changes: 48 additions & 28 deletions lib/typing/check.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand All @@ -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
{
Expand Down
1 change: 1 addition & 0 deletions lib/typing/typedtree.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions lib/typing/types_in.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -108,4 +108,4 @@ let get_def name ty_defs =
when name' = name ->
true
| _ -> false)
ty_defs
ty_def_group
7 changes: 7 additions & 0 deletions tests/cram/test_dirs/interp.t/run.t
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@

$ $FF test_rec_ty.fun

$ ./test_rec_ty.fun.out
Matched second!


19 changes: 19 additions & 0 deletions tests/cram/test_dirs/interp.t/test_rec_ty.fun
Original file line number Diff line number Diff line change
@@ -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!"
33 changes: 26 additions & 7 deletions tests/regular/parse_test.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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"
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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" =
Expand Down Expand Up @@ -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 ()))
Expand Down Expand Up @@ -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 ())))))))
|}]
22 changes: 22 additions & 0 deletions tests/regular/typing_test.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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" =
Expand Down

0 comments on commit 455d785

Please sign in to comment.