Skip to content

Commit

Permalink
Abstract if node argument is enum variant
Browse files Browse the repository at this point in the history
Related commit: 33f64e4
  • Loading branch information
daniel-larraz committed Sep 3, 2024
1 parent aba45c0 commit 87832d2
Show file tree
Hide file tree
Showing 4 changed files with 40 additions and 3 deletions.
9 changes: 6 additions & 3 deletions src/lustre/lustreAstNormalizer.ml
Original file line number Diff line number Diff line change
Expand Up @@ -622,7 +622,10 @@ let get_type_of_id info node_id id =
Ctx.expand_type_syn info.context ty

(* If [expr] is already an id then we don't create a fresh local *)
let should_not_abstract force expr = not force && AH.expr_is_id expr
let should_not_abstract info force = function
| A.Ident (_, id) ->
not (Ctx.is_enum_variant info.context id) && not force
| _ -> false

let add_subrange_constraints info node_id kind vars =
vars
Expand Down Expand Up @@ -1587,7 +1590,7 @@ and rename_id info = function

and abstract_expr ?guard force info node_id map expr =
let nexpr, gids1, warnings = normalize_expr ?guard info node_id map expr in
if should_not_abstract force nexpr then
if should_not_abstract info force nexpr then
nexpr, gids1, warnings
else
let ivars = info.inductive_variables in
Expand Down Expand Up @@ -1657,7 +1660,7 @@ and normalize_expr ?guard info node_id map =
in
let abstract_node_arg ?guard force is_const info map expr =
let nexpr, gids1, warnings = normalize_expr ?guard info node_id map expr in
if should_not_abstract force nexpr then
if should_not_abstract info force nexpr then
nexpr, gids1, warnings
else
let ivars = info.inductive_variables in
Expand Down
6 changes: 6 additions & 0 deletions src/lustre/typeCheckerContext.ml
Original file line number Diff line number Diff line change
Expand Up @@ -306,6 +306,12 @@ let add_enum_variants: tc_context -> LA.ident -> LA.ident list -> tc_context
= fun ctx i vs -> {ctx with enum_vars = IMap.add i vs (ctx.enum_vars) }
(** Add an enumeration type and associated variants to the typing context *)

let is_enum_variant ctx id =
match lookup_const ctx id with
| Some (_, Some (UserType (_, _, uid)), _) ->
lookup_variants ctx uid != None
| _ -> false

let remove_ty: tc_context -> LA.ident -> tc_context
= fun ctx i -> {ctx with ty_ctx= IMap.remove i (ctx.ty_ctx)}
(** Removes a type binding *)
Expand Down
2 changes: 2 additions & 0 deletions src/lustre/typeCheckerContext.mli
Original file line number Diff line number Diff line change
Expand Up @@ -163,6 +163,8 @@ val add_ty_decl: tc_context -> LA.ident -> tc_context
val add_enum_variants: tc_context -> LA.ident -> LA.ident list -> tc_context
(** Add an enumeration type and associated variants to the typing context *)

val is_enum_variant: tc_context -> LA.ident -> bool

val remove_ty: tc_context -> LA.ident -> tc_context
(** Removes a type binding *)

Expand Down
26 changes: 26 additions & 0 deletions tests/regression/success/const_id_arg.lus
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@

type E = enum {A, B};

const C1: int;
const C2: int = 0;

node N2(x: int) returns (y: int);
let
y = x;
tel

node N3(x: E) returns (y: E);
let
y = x;
tel

node N1(const x: int) returns (y1,y2,y3: int; z: E);
let
y1 = N2(C1);
y2 = N2(x);
y3 = N2(C2);
z = N3(A);
check y1 = y2 => x = C1;
check y3 >= 0;
check z = A;
tel

0 comments on commit 87832d2

Please sign in to comment.