Fix extraction of primitive array literal

Fix #22365

Author: SkySkimmer

doc/changelog/13-extraction/22457-fix-extr-arr-Fixed.rst

@@ -0,0 +1,5 @@
+- **Fixed:**
+  extraction of primitive array literals
+  (`#22457 <https://github.com/rocq-prover/rocq/pull/22457>`_,
+  fixes `#22365 <https://github.com/rocq-prover/rocq/issues/22365>`_,
+  by Gaëtan Gilbert).

plugins/extraction/common.ml

@@ -63,11 +63,6 @@ let pp_boxed_tuple f = function
   | [x] -> f x
   | l -> pp_par true (hov 0 (prlist_with_sep (fun () -> str "," ++ spc ()) f l))
 
-let pp_array f = function
-  | [] -> mt ()
-  | [x] -> f x
-  | l -> pp_par true (prlist_with_sep (fun () -> str ";" ++ spc ()) f l)
-
 (** By default, in module Format, you can do horizontal placing of blocks
     even if they include newlines, as long as the number of chars in the
     blocks is less that a line length. To avoid this awkward situation,

plugins/extraction/common.mli

@@ -30,7 +30,6 @@ val pp_apply2 : Pp.t -> bool -> Pp.t list -> Pp.t
 
 val pp_tuple_light : (bool -> 'a -> Pp.t) -> 'a list -> Pp.t
 val pp_tuple : ('a -> Pp.t) -> 'a list -> Pp.t
-val pp_array : ('a -> Pp.t) -> 'a list -> Pp.t
 val pp_boxed_tuple : ('a -> Pp.t) -> 'a list -> Pp.t
 
 val pr_binding : Id.t list -> Pp.t

plugins/extraction/ocaml.ml

@@ -326,7 +326,7 @@ let rec pp_expr table par env args =
         str "(" ++ str (Pstring.compile s) ++ str ")"
     | MLparray(t,def) ->
       assert (args=[]);
-      let tuple = pp_array (pp_expr table true env []) (Array.to_list t) in
+      let tuple = prlist_with_sep pr_semicolon (pp_expr table true env []) (Array.to_list t) in
       let def = pp_expr table true env [] def in
       str "(ExtrNative.of_array [|" ++ tuple ++ str "|]" ++ spc () ++ def ++ str")"
 

test-suite/output/bug_22365.out

@@ -0,0 +1,8 @@
+File "./output/bug_22365.v", line 5, characters 0-17:
+Warning: The following axiom must be realized in the extracted code:
+ array.
+ [extraction-axiom-to-realize,extraction,default]
+(** val a3lit : nat array **)
+
+let a3lit =
+  (ExtrNative.of_array [|O; (S O); (S (S O))|] (S (S (S (S O)))))

test-suite/output/bug_22365.v

@@ -0,0 +1,5 @@
+From Corelib Require Import Array.PrimArray Numbers.Cyclic.Int63.PrimInt63 extraction.Extraction.
+
+Definition a3lit : PrimArray.array nat := [|0; 1; 2 | 4|].
+
+Extraction a3lit.