Primitive persistent arrays

Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.

Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>

1 files changed, 20 insertions, 0 deletions

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 429e740403..61317f3ef2 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -65,6 +65,18 @@ let test_name_colon =
 
 let aliasvar = function { CAst.v = CPatAlias (_, na) } -> Some na | _ -> None
 
+let test_array_opening =
+  let open Pcoq.Lookahead in
+  to_entry "test_array_opening" begin
+    lk_kw "[" >> lk_kw "|" >> check_no_space
+  end
+
+let test_array_closing =
+  let open Pcoq.Lookahead in
+  to_entry "test_array_closing" begin
+    lk_kw "|" >> lk_kw "]" >> check_no_space
+  end
+
 }
 
 GRAMMAR EXTEND Gram
@@ -172,9 +184,17 @@ GRAMMAR EXTEND Gram
         { CAst.make ~loc @@ CNotation(None,(InConstrEntry,"{ _ }"),([c],[],[],[])) }
       | "`{"; c = operconstr LEVEL "200"; "}" ->
         { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) }
+      | test_array_opening; "["; "|"; ls = array_elems; "|"; def = lconstr; ty = type_cstr; test_array_closing; "|"; "]"; u = univ_instance ->
+        { let t = Array.make (List.length ls) def in
+          List.iteri (fun i e -> t.(i) <- e) ls;
+          CAst.make ~loc @@ CArray(u, t, def, ty)
+        }
       | "`("; c = operconstr LEVEL "200"; ")" ->
         { CAst.make ~loc @@ CGeneralization (Explicit, None, c) } ] ]
   ;
+  array_elems:
+    [ [ fs = LIST0 lconstr SEP ";" -> { fs } ]]
+  ;
   record_declaration:
     [ [ fs = fields_def -> { CAst.make ~loc @@ CRecord fs } ] ]
   ;