Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Merged
merged 1 commit into from
May 9, 2024
Merged

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

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions src/lustre/lustreInput.ml
View file
Open in desktop
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