Merge pull request #1069 from lorchrob/flatten-gen-imp-nodes

Rearrange pipeline steps to perform ref type flattening after imported node generation

src/lustre/lustreInput.ml

@@ -165,10 +165,7 @@ let type_check declarations =
     (* Step 8. Type check nodes and contracts *)
     let* global_ctx, warnings3 = TC.type_check_infer_nodes_and_contracts inlined_ctx sorted_node_contract_decls in
 
-    (* Step 9. Flatten refinement types *)
-    let sorted_node_contract_decls = LFR.flatten_ref_types global_ctx sorted_node_contract_decls in
-
-    (* Step 10. Generate imported nodes associated with refinement types if realizability checking is enabled *)
+    (* Step 9. Generate imported nodes associated with refinement types if realizability checking is enabled *)
     let sorted_node_contract_decls = 
       if List.mem `CONTRACTCK (Flags.enabled ()) 
       then 
@@ -177,6 +174,9 @@ let type_check declarations =
       else sorted_node_contract_decls
     in
 
+    (* Step 10. Flatten refinement types *)
+    let sorted_node_contract_decls = LFR.flatten_ref_types global_ctx sorted_node_contract_decls in
+
     (* Step 11. Remove multiple assignment from if blocks and frame blocks *)
     let sorted_node_contract_decls, gids = RMA.remove_mult_assign global_ctx sorted_node_contract_decls in