Skip to content

Commit

Permalink
Reorder flattening of refinement types in pipeline
Browse files Browse the repository at this point in the history
The flattening must be done after instantiating polymorphic nodes.
  • Loading branch information
daniel-larraz committed Aug 30, 2024
1 parent cbace84 commit ea6472d
Show file tree
Hide file tree
Showing 2 changed files with 23 additions and 11 deletions.
22 changes: 11 additions & 11 deletions src/lustre/lustreInput.ml
Original file line number Diff line number Diff line change
Expand Up @@ -180,33 +180,33 @@ 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 *)
(* Step 10. 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

(* Step 12. Desugar imperative if block to ITEs *)
(* Step 11. Desugar imperative if block to ITEs *)
let* (sorted_node_contract_decls, gids) = (LDI.desugar_if_blocks global_ctx sorted_node_contract_decls gids) in

(* Step 13. Desugar frame blocks by adding node equations and guarding oracles. *)
(* Step 12. Desugar frame blocks by adding node equations and guarding oracles. *)
let* (sorted_node_contract_decls, warnings4) = LDF.desugar_frame_blocks sorted_node_contract_decls in

(* Step 14. Inline constants in node equations *)
(* Step 13. Inline constants in node equations *)
let* (inlined_global_ctx, const_inlined_nodes_and_contracts) =
IC.inline_constants global_ctx sorted_node_contract_decls
in

(* Step 15. Check that inductive array equations are well-founded *)
(* Step 14. Check that inductive array equations are well-founded *)
let* _ = LAD.check_inductive_array_dependencies inlined_global_ctx node_summary const_inlined_nodes_and_contracts in

(* Step 16. Infer tighter subrange constraints with abstract interpretation *)
(* Step 15. Infer tighter subrange constraints with abstract interpretation *)
let* _ = LIA.interpret_global_consts inlined_global_ctx const_inlined_type_and_consts in
let abstract_interp_ctx = LIA.interpret_program inlined_global_ctx gids const_inlined_nodes_and_contracts in

(* Step 17. Instantiate polymorphic nodes with concrete types *)
(* Step 16. Instantiate polymorphic nodes with concrete types *)
let inlined_global_ctx, const_inlined_nodes_and_contracts = LIP.instantiate_polymorphic_nodes inlined_global_ctx const_inlined_nodes_and_contracts in


(* Step 17. Flatten refinement types *)
let const_inlined_nodes_and_contracts = LFR.flatten_ref_types inlined_global_ctx const_inlined_nodes_and_contracts in

(* Step 18. Normalize AST: guard pres, abstract to locals where appropriate *)
let* (normalized_nodes_and_contracts, gids, warnings5) =
LAN.normalize inlined_global_ctx abstract_interp_ctx const_inlined_nodes_and_contracts gids
Expand Down
12 changes: 12 additions & 0 deletions tests/regression/success/flatten_ref_type_in_poly_node.lus
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@

type Nat = subtype { n: int | 0 <= n };

node N2<<T>>() returns (r: T);
let
r = any T;
tel

node N1() returns (z: Nat);
let
z = N2<<Nat>>();
tel

0 comments on commit ea6472d

Please sign in to comment.