Merge pull request #1097 from daniel-larraz/abstract-enum-variant

Abstract if node argument is enum variant

src/lustre/lustreAstNormalizer.ml

@@ -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
@@ -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
@@ -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

src/lustre/typeCheckerContext.ml

@@ -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  *)

src/lustre/typeCheckerContext.mli

@@ -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  *)
 

tests/regression/success/const_id_arg.lus

@@ -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