Make sure undefined_type functions are generated before registers

When topologically sorting the top-level definitions, we add the
undefined_X functions for any type X to a registers dependencies if it
uses the type X, this ensures that any such functions are generated
before the register declaration. In theory this is only needed for
OCaml, but adding these edges in the definition graph shouldn't cause
any issues.

1 files changed, 11 insertions, 0 deletions

diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index fd43de16..75f55c9c 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -475,6 +475,8 @@ let fv_of_def consider_var consider_scatter_as_one all_defs = function
      List.fold_left Nameset.union Nameset.empty (List.map snd fvs)
   | DEF_scattered sdef -> fv_of_scattered consider_var consider_scatter_as_one all_defs sdef
   | DEF_reg_dec rdec -> fv_of_rd consider_var rdec
+  | DEF_constraint (id, _, _) ->
+     raise (Reporting.err_unreachable (id_loc id) __POS__ "Constraint should be re-written")
 
 let group_defs consider_scatter_as_one (Ast.Defs defs) =
   List.map (fun d -> (fv_of_def false consider_scatter_as_one defs d,d)) defs
@@ -549,6 +551,15 @@ let scc ?(original_order : string list option) (g : graph) =
 
 let add_def_to_graph (prelude, original_order, defset, graph) d =
   let bound, used = fv_of_def false true [] d in
+  let used = match d with
+    | DEF_reg_dec _ ->
+       (* For a register, we need to ensure that any undefined_type
+          functions for types used by the register are placed before
+          the register declaration. *)
+       let undefineds = Nameset.map (fun name -> "undefined_" ^ name) used in
+       Nameset.union undefineds used
+    | _ -> used
+  in
   try
     (* A definition may bind multiple identifiers, e.g. "let (x, y) = ...".
        We add all identifiers to the dependency graph as a cycle.  The actual