Extensional array equality bug fix

src/lustre/lustreAstHelpers.ml

@@ -89,6 +89,16 @@ let rec expr_contains_call = function
   | Call (_, _, _) | Condact (_, _, _, _, _, _) | RestartEvery (_, _, _, _) | ChooseOp (_, _, _, _)
     -> true
 
+let rec type_contains_array = function
+  | IntRange _ -> false
+  | TupleType (_, tys) | GroupType (_, tys) ->
+    List.fold_left (fun acc ty -> acc || type_contains_array ty) false tys
+  | RecordType (_, _, tys) ->
+    List.fold_left (fun acc (_, _, ty) -> acc || type_contains_array ty)
+      false tys
+  | ArrayType _ -> true
+  | _ -> false
+
 let rec type_contains_subrange = function
   | IntRange _ -> true
   | TupleType (_, tys) | GroupType (_, tys) ->

src/lustre/lustreAstHelpers.mli

@@ -48,6 +48,9 @@ val type_arity : lustre_type -> int * int
 val type_contains_subrange : lustre_type -> bool
 (** Returns true if the lustre type expression contains an IntRange or if it is an IntRange *)
 
+val type_contains_array : lustre_type -> bool 
+(** Returns true if the lustre type expression contains an array or if it is an array *)
+
 val substitute_naive : HString.t -> expr -> expr -> expr
 (** Substitute second param for first param in third param. 
     ChooseOp and Quantifier are not supported due to introduction of bound variables. *)

src/lustre/lustreTypeChecker.ml

@@ -920,7 +920,7 @@ and infer_type_comp_op: tc_context -> Lib.position -> LA.expr -> LA.expr
   match op with
   | Neq  | Eq ->
     R.ifM (eq_lustre_type ctx ty1 ty2)
-      (if LH.is_type_array ty1 then
+      (if LH.type_contains_array ty1 then
          type_error pos (Unsupported "Extensional array equality is not supported")
        else
          R.ok (LA.Bool pos)

tests/ounit/lustre/lustreTypeChecker/extensional_array_equality2.lus

@@ -0,0 +1,5 @@
+node N() returns(A: [int^2^3, int]);
+let
+  check (A = pre A);
+  --%MAIN;
+tel

tests/ounit/lustre/testLustreFrontend.ml

@@ -587,6 +587,10 @@ let _ = run_test_tt_main ("frontend LustreTypeChecker error tests" >::: [
     match load_file "./lustreTypeChecker/extensional_array_equality.lus" with
     | Error (`LustreTypeCheckerError (_, Unsupported _)) -> true
     | _ -> false);
+  mk_test "test extensional array equality 2" (fun () ->
+    match load_file "./lustreTypeChecker/extensional_array_equality2.lus" with
+    | Error (`LustreTypeCheckerError (_, Unsupported _)) -> true
+    | _ -> false);
   mk_test "test expected record type" (fun () ->
     match load_file "./lustreTypeChecker/expected_record_type.lus" with
     | Error (`LustreTypeCheckerError (_, ExpectedRecordType _)) -> true