Skip to content

Commit

Permalink
Rearrange pipeline steps to perform ref type flattening after importe…
Browse files Browse the repository at this point in the history
…d node generation
  • Loading branch information
lorchrob committed May 9, 2024
1 parent 53b9b5e commit 99c0279
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions src/lustre/lustreInput.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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

Expand Down

0 comments on commit 99c0279

Please sign in to comment.