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.

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

Abstract if node argument is enum variant #1097

Merged
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
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