Skip to content

Commit c1e092f

Browse files
protzprotz
committed
Fix #676 
1 parent 4316b26 commit c1e092f

File tree

1 file changed

+131
-117
lines changed

1 file changed

+131
-117
lines changed

‎lib/Monomorphization.ml‎

Lines changed: 131 additions & 117 deletions
Original file line numberDiff line numberDiff line change
@@ -332,114 +332,135 @@ let monomorphize_data_types map = object(self)
332332
* order declarations as they are needed, including that of the node we are
333333
* visiting. *)
334334
method private visit_node (under_ref: bool) (n: node) =
335-
(* Because we have no equirecursive types, this should not loop *)
336-
let n = fst3 n, List.map (self#visit_typ under_ref) (snd3 n), thd3 n in
337-
let lid, args, cgs = n in
338-
(* White, gray or black? *)
339-
match Hashtbl.find state n with
340-
| exception Not_found ->
341-
let chosen_lid, flag = self#lid_of n in
342-
if Options.debug "data-types-traversal" then
343-
KPrint.bprintf "visiting %a: Not_found --> %a\n" ptyp (fold_tapp n) plid chosen_lid;
344-
let flag = if fst3 best_hint = n then thd3 best_hint @ flag else flag in
345-
if lid = tuple_lid then begin
346-
Hashtbl.add state n (Gray, chosen_lid);
347-
(* For tuples, we immediately know how to generate a definition. *)
348-
let fields = List.mapi (fun i arg -> Some (self#field_at i), (arg, false)) args in
349-
self#record (DType (chosen_lid, [ Common.Private ] @ flag, 0, 0, Flat fields));
350-
Hashtbl.replace state n (Black, chosen_lid)
351-
end else begin
352-
(* This specific node has not been visited yet. *)
353-
Hashtbl.add state n (Gray, chosen_lid);
354-
355-
let subst fields = List.map (fun (field, (t, m)) ->
356-
field, (DeBruijn.subst_tn args (DeBruijn.subst_ctn' cgs t), m)
357-
) fields in
358-
assert (not (Hashtbl.mem map lid) || not (has_variables args) && not (has_cg_variables cgs));
359-
begin match Hashtbl.find map lid with
360-
| exception Not_found ->
361-
(* Unknown, external non-polymorphic lid, e.g. Prims.int *)
362-
Hashtbl.replace state n (Black, chosen_lid)
363-
| flags, ((Variant _ | Flat _ | Union _) as def) when under_ref && not (Hashtbl.mem seen_declarations lid) ->
364-
(* FORWARD DECLARATION: this is unrelated to monomorphization (but we do it
365-
here anyway). An occurrence of `t<ts>*` appears before the definition of `t`; we
366-
pick a name, insert a forward declaration for `t<ts>`, then remember that *once we
367-
have see the definition of `t`*, we will insert the monomorphized `t___ts` at that
368-
specific location.
369-
370-
The comment below furthermore tries to explain why we do things this way (as
371-
opposed to inserting the monomorphized `t___ts` immediately).
372-
373-
Because this looks up a definition in the global map, the
374-
definitions are reordered according to the traversal order, which
375-
is generally a good idea (we accept more programs!), EXCEPT
376-
when the user relies on mutual recursion behind a reference
377-
(pointer) type. In that case, following the type dependency graph is
378-
generally not a good idea, since we may go from a valid
379-
ordering to an invalid one (see tests/MutualStruct.fst). So,
380-
the intent here (i.e., when under a ref type) is that:
381-
- tuple types ALWAYS get monomorphized on-demand (see
382-
above)
383-
- abbreviations are fine and won't cause further issues
384-
- data types, however, need to have their names allocated and a
385-
forward reference inserted (TODO: at most once), then the
386-
specific choice of type arguments need to be recorded as
387-
something we want to visit later (once we're done with this
388-
particular traversal)... *)
389-
if Options.debug "data-types-traversal" then
390-
KPrint.bprintf "DEFERRING %a\n" ptyp (fold_tapp n);
391-
if match def with Union _ -> true | _ -> false then
392-
self#record (DType (chosen_lid, flags, 0, 0, Forward FUnion))
393-
else
394-
self#record (DType (chosen_lid, flags, 0, 0, Forward FStruct));
395-
Hashtbl.add pending_monomorphizations lid (args, cgs);
396-
(* FORWARD DECLARATIONS: remove us from the state to make sure future occurences of the
397-
same situation send us through this codepath again *)
398-
Hashtbl.remove state n
399-
| flags, Variant branches ->
400-
let branches = List.map (fun (cons, fields) -> cons, subst fields) branches in
401-
let branches = self#visit_branches_t under_ref branches in
402-
self#record (DType (chosen_lid, flag @ flags, 0, 0, Variant branches));
403-
Hashtbl.replace state n (Black, chosen_lid)
404-
| flags, Flat fields ->
405-
let fields = self#visit_fields_t_opt under_ref (subst fields) in
406-
self#record (DType (chosen_lid, flag @ flags, 0, 0, Flat fields));
407-
Hashtbl.replace state n (Black, chosen_lid)
408-
| flags, Union fields ->
409-
let fields = List.map (fun (f, t) ->
335+
(* Fast-path: there are no type arguments (so: nothing to monomorphize here)
336+
and we are not under a ref (so: no forward declarations to insert here),
337+
so we do not visit this lid, and do not self#record it.
338+
339+
1. If we saw this lid, great.
340+
2. If we haven't seen this lid yet, no problem, its contents will be
341+
visited through self#visit_decl in the case where n = 0 && n_cgs = 0,
342+
and it will be inserted in its original spot, which has the nice
343+
side-effect of preserving the source order.*)
344+
if snd3 n = [] && thd3 n = [] && not under_ref then
345+
fst3 n
346+
else
347+
(* We recursively visit the arguments. This avoids inconsistencies where
348+
the map would previously record both t<u<v>> and t<u__v> which then
349+
required renormalizations and didn't work anyhow.
350+
351+
Because we have no equirecursive types, this should not loop *)
352+
let n = fst3 n, List.map (self#visit_typ under_ref) (snd3 n), thd3 n in
353+
let lid, args, cgs = n in
354+
(* White, gray or black? *)
355+
match Hashtbl.find state n with
356+
| exception Not_found ->
357+
let chosen_lid, flag = self#lid_of n in
358+
if Options.debug "data-types-traversal" then
359+
KPrint.bprintf "visiting %a: Not_found --> %a\n" ptyp (fold_tapp n) plid chosen_lid;
360+
let flag = if fst3 best_hint = n then thd3 best_hint @ flag else flag in
361+
if lid = tuple_lid then begin
362+
assert (args <> []);
363+
Hashtbl.add state n (Gray, chosen_lid);
364+
(* For tuples, we immediately know how to generate a definition. *)
365+
let fields = List.mapi (fun i arg -> Some (self#field_at i), (arg, false)) args in
366+
self#record (DType (chosen_lid, [ Common.Private ] @ flag, 0, 0, Flat fields));
367+
Hashtbl.replace state n (Black, chosen_lid)
368+
end else begin
369+
(* This specific node has not been visited yet. *)
370+
Hashtbl.add state n (Gray, chosen_lid);
371+
372+
let subst fields = List.map (fun (field, (t, m)) ->
373+
field, (DeBruijn.subst_tn args (DeBruijn.subst_ctn' cgs t), m)
374+
) fields in
375+
assert (not (Hashtbl.mem map lid) || not (has_variables args) && not (has_cg_variables cgs));
376+
begin match Hashtbl.find map lid with
377+
| exception Not_found ->
378+
(* Unknown, external non-polymorphic lid, e.g. Prims.int *)
379+
Hashtbl.replace state n (Black, chosen_lid)
380+
| flags, ((Variant _ | Flat _ | Union _) as def) when under_ref && not (Hashtbl.mem seen_declarations lid) ->
381+
(* FORWARD DECLARATION: this is unrelated to monomorphization (but we do it
382+
here anyway). An occurrence of `t<ts>*` appears before the definition of `t`; we
383+
pick a name, insert a forward declaration for `t<ts>`, then remember that *once we
384+
have see the definition of `t`, we will insert the monomorphized `t___ts` at that
385+
specific location.
386+
387+
The comment below furthermore tries to explain why we do things this way (as
388+
opposed to inserting the monomorphized `t___ts` immediately).
389+
390+
Because this looks up a definition in the global map, the
391+
definitions are reordered according to the traversal order, which
392+
is generally a good idea (we accept more programs!), EXCEPT
393+
when the user relies on mutual recursion behind a reference
394+
(pointer) type. In that case, following the type dependency graph is
395+
generally not a good idea, since we may go from a valid
396+
ordering to an invalid one (see tests/MutualStruct.fst). So,
397+
the intent here (i.e., when under a ref type) is that:
398+
- tuple types ALWAYS get monomorphized on-demand (see
399+
above)
400+
- abbreviations are fine and won't cause further issues
401+
- data types, however, need to have their names allocated and a
402+
forward reference inserted (TODO: at most once), then the
403+
specific choice of type arguments need to be recorded as
404+
something we want to visit later (once we're done with this
405+
particular traversal)... *)
406+
if Options.debug "data-types-traversal" then
407+
KPrint.bprintf "DEFERRING %a\n" ptyp (fold_tapp n);
408+
if match def with Union _ -> true | _ -> false then
409+
self#record (DType (chosen_lid, flags, 0, 0, Forward FUnion))
410+
else
411+
self#record (DType (chosen_lid, flags, 0, 0, Forward FStruct));
412+
Hashtbl.add pending_monomorphizations lid (args, cgs);
413+
(* FORWARD DECLARATIONS: remove us from the state to make sure future occurences of the
414+
same situation send us through this codepath again *)
415+
Hashtbl.remove state n
416+
| flags, Variant branches ->
417+
let branches = List.map (fun (cons, fields) -> cons, subst fields) branches in
418+
let branches = self#visit_branches_t under_ref branches in
419+
if args <> [] || cgs <> [] then
420+
self#record (DType (chosen_lid, flag @ flags, 0, 0, Variant branches));
421+
Hashtbl.replace state n (Black, chosen_lid)
422+
| flags, Flat fields ->
423+
let fields = self#visit_fields_t_opt under_ref (subst fields) in
424+
if args <> [] || cgs <> [] then
425+
self#record (DType (chosen_lid, flag @ flags, 0, 0, Flat fields));
426+
Hashtbl.replace state n (Black, chosen_lid)
427+
| flags, Union fields ->
428+
let fields = List.map (fun (f, t) ->
429+
let t = DeBruijn.subst_tn args t in
430+
let t = self#visit_typ under_ref t in
431+
f, t
432+
) fields in
433+
if args <> [] || cgs <> [] then
434+
self#record (DType (chosen_lid, flag @ flags, 0, 0, Union fields));
435+
Hashtbl.replace state n (Black, chosen_lid)
436+
| flags, Abbrev t ->
410437
let t = DeBruijn.subst_tn args t in
411438
let t = self#visit_typ under_ref t in
412-
f, t
413-
) fields in
414-
self#record (DType (chosen_lid, flag @ flags, 0, 0, Union fields));
415-
Hashtbl.replace state n (Black, chosen_lid)
416-
| flags, Abbrev t ->
417-
let t = DeBruijn.subst_tn args t in
418-
let t = self#visit_typ under_ref t in
419-
self#record (DType (chosen_lid, flag @ flags, 0, 0, Abbrev t));
420-
Hashtbl.replace state n (Black, chosen_lid)
421-
| _ ->
422-
Hashtbl.replace state n (Black, chosen_lid)
423-
end
424-
end;
425-
chosen_lid
426-
| Gray, chosen_lid ->
427-
(* FORWARD DECLARATION: simple case of a recursive type that needs a forward declaration *)
428-
if Options.debug "data-types-traversal" then
429-
KPrint.bprintf "visiting %a: Gray\n" ptyp (fold_tapp n);
430-
begin match Hashtbl.find map lid with
431-
| exception Not_found ->
432-
()
433-
| flags, Union _ ->
434-
self#record (DType (chosen_lid, flags, 0, 0, Forward FUnion))
435-
| flags, _ ->
436-
self#record (DType (chosen_lid, flags, 0, 0, Forward FStruct))
437-
end;
438-
chosen_lid
439-
| Black, chosen_lid ->
440-
if Options.debug "data-types-traversal" then
441-
KPrint.bprintf "visiting %a: Black\n" ptyp (fold_tapp n);
442-
chosen_lid
439+
if args <> [] || cgs <> [] then
440+
self#record (DType (chosen_lid, flag @ flags, 0, 0, Abbrev t));
441+
Hashtbl.replace state n (Black, chosen_lid)
442+
| _ ->
443+
Hashtbl.replace state n (Black, chosen_lid)
444+
end
445+
end;
446+
chosen_lid
447+
| Gray, chosen_lid ->
448+
(* FORWARD DECLARATION: simple case of a recursive type that needs a forward declaration *)
449+
if Options.debug "data-types-traversal" then
450+
KPrint.bprintf "visiting %a: Gray\n" ptyp (fold_tapp n);
451+
begin match Hashtbl.find map lid with
452+
| exception Not_found ->
453+
()
454+
| flags, Union _ ->
455+
self#record (DType (chosen_lid, flags, 0, 0, Forward FUnion))
456+
| flags, _ ->
457+
self#record (DType (chosen_lid, flags, 0, 0, Forward FStruct))
458+
end;
459+
chosen_lid
460+
| Black, chosen_lid ->
461+
if Options.debug "data-types-traversal" then
462+
KPrint.bprintf "visiting %a: Black\n" ptyp (fold_tapp n);
463+
chosen_lid
443464

444465
(* Top-level, non-parameterized declarations are root of our graph traversal.
445466
* This also visits, via occurrences in code, applications of parameterized
@@ -514,18 +535,11 @@ let monomorphize_data_types map = object(self)
514535

515536
| DType (lid, _, n_cgs, n, (Flat _ | Variant _ | Abbrev _ | Union _)) ->
516537
assert (n = 0 && n_cgs = 0);
517-
(* Regular traversal logic, as below. *)
518-
ignore (self#visit_decl false d);
519-
(* FORWARD DECLARATIONS: we force a visit of this (non-polymorphic) type definition, for
520-
the sole side-effect of remembering that we have seen it, and that further occurrences
521-
of it need not generate a forward declaration (i.e. mark it Black, because
522-
under_ref=false).
523-
524-
Note that `visit_node` will insert our own definition in the pending list, flushed by
525-
`clear` -- ignore and don't insert twice. *)
526-
ignore (self#visit_node false (lid, [], []));
538+
(* This was not inserted earlier (see comment at the beginning of
539+
visit_node, so we visit it here *)
540+
let d = self#visit_decl false d in
527541
Hashtbl.add seen_declarations lid ();
528-
self#clear ()
542+
self#clear () @ [ d ]
529543

530544
| _ ->
531545
(* Not a type, e.g. a global; needs to be retained. *)

0 commit comments

Comments
 (0)