Minor optimization

src/lustre/lustreAstNormalizer.ml

@@ -334,13 +334,17 @@ let extract_array_size = function
 
 let generalize_to_array_expr name ind_vars expr nexpr = 
   let vars = AH.vars expr in
-  let ind_vars = List.map (fun (i, _) -> i) (StringMap.bindings ind_vars) in
+  let ind_vars = List.map fst (StringMap.bindings ind_vars) in
   let ind_vars = List.filter (fun x -> A.SI.mem x vars) ind_vars in
-  let (eq_lhs, nexpr) = if List.length ind_vars = 0
-    then A.StructDef (dpos, [SingleIdent (dpos, name)]), nexpr
-    else A.StructDef (dpos, [ArrayDef (dpos, name, ind_vars)]),
+  let (eq_lhs, nexpr) =
+    match ind_vars with
+    | [] ->
+      A.StructDef (dpos, [SingleIdent (dpos, name)]), nexpr
+    | _ ->
+      A.StructDef (dpos, [ArrayDef (dpos, name, ind_vars)]),
       A.ArrayIndex (dpos, nexpr, A.Ident (dpos, List.hd ind_vars))
-  in eq_lhs, nexpr
+  in
+  eq_lhs, nexpr
 
 let mk_fresh_local force info pos is_ghost ind_vars expr_type expr =
   match (LocalCache.find_opt local_cache expr, force) with
@@ -369,14 +373,15 @@ let mk_fresh_array_ctor info pos ind_vars expr_type expr size_expr =
     equations = [(info.quantified_variables, info.contract_scope, eq_lhs, expr)]; }
   in nexpr, gids
 
-let mk_fresh_node_arg_local info pos is_const ind_vars expr_type expr =
+let mk_fresh_node_arg_local info pos is_const expr_type expr =
   match NodeArgCache.find_opt node_arg_cache expr with
   | Some nexpr -> nexpr, empty ()
   | None ->
   i := !i + 1;
   let prefix = HString.mk_hstring (string_of_int !i) in
   let name = HString.concat2 prefix (HString.mk_hstring "_gklocal") in
   let nexpr = A.Ident (pos, name) in
+  let ind_vars = info.inductive_variables in
   let (eq_lhs, nexpr) = generalize_to_array_expr name ind_vars expr nexpr in
   let gids = { (empty ()) with
     node_args = [(name, is_const, expr_type, expr)];
@@ -1193,7 +1198,7 @@ and normalize_expr ?guard info map =
         (StringMap.choose_opt info.inductive_variables) |> get |> snd
       else Chk.infer_type_expr info.context expr |> unwrap
       in
-      let iexpr, gids2 = mk_fresh_node_arg_local info pos is_const ivars ty nexpr in
+      let iexpr, gids2 = mk_fresh_node_arg_local info pos is_const ty nexpr in
       iexpr, union gids1 gids2, warnings
   in function
   (* ************************************************************************ *)

src/lustre/lustreNodeGen.ml

@@ -510,8 +510,7 @@ let rec expand_tuple' pos accum bounds lhs rhs =
 let expand_tuple pos lhs rhs = 
   (* Format.eprintf "expand_tuple: \n"; *)
   expand_tuple' pos [] []
-    (List.map (fun (i, e) -> (i, e)) (X.bindings lhs))
-    (List.map (fun (i, e) -> (i, e)) (X.bindings rhs))
+    (X.bindings lhs) (X.bindings rhs)
 
 let compile_contract_item map count scope kind pos name expr =
     let scope = List.map (fun (i, s) -> i, HString.string_of_hstring s) scope in