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>

7 files changed, 50 insertions, 29 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index ef6f8652e9..f47cdd8bf0 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -155,7 +155,7 @@ let build_beq_scheme_deps kn =
         | None -> accu)
       | Rel _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | Proj _
       | Construct _ | Case _ | CoFix _ | Fix _ | Meta _ | Evar _ | Int _
-      | Float _ -> accu
+      | Float _ | Array _ -> accu
     in
     let u = Univ.Instance.empty in
     let constrs n = get_constructors env (make_ind_family (((kn, i), u),
@@ -293,6 +293,7 @@ let build_beq_scheme mode kn =
         | Evar _  -> raise (EqUnknown "existential variable")
         | Int _ -> raise (EqUnknown "int")
         | Float _ -> raise (EqUnknown "float")
+              | Array _ -> raise (EqUnknown "array")
     in
       aux t
   in
diff --git a/vernac/comPrimitive.ml b/vernac/comPrimitive.ml
index bcfbc049fa..110dcdc98a 100644
--- a/vernac/comPrimitive.ml
+++ b/vernac/comPrimitive.ml
@@ -8,30 +8,45 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-let do_primitive id prim typopt =
+open Names
+
+let declare id entry =
+  let _ : Constant.t =
+    Declare.declare_constant ~name:id ~kind:Decls.IsPrimitive (Declare.PrimitiveEntry entry)
+  in
+  Flags.if_verbose Feedback.msg_info Pp.(Id.print id ++ str " is declared")
+
+let do_primitive id udecl prim typopt =
   if Global.sections_are_opened () then
     CErrors.user_err Pp.(str "Declaring a primitive is not allowed in sections.");
   if Dumpglob.dump () then Dumpglob.dump_definition id false "ax";
-  let env = Global.env () in
-  let evd = Evd.from_env env in
-  let evd, typopt = Option.fold_left_map
-      Constrintern.(interp_type_evars_impls ~impls:empty_internalization_env env)
-      evd typopt
-  in
-  let evd = Evd.minimize_universes evd in
-  let uvars, impls, typopt = match typopt with
-    | None -> Univ.LSet.empty, [], None
-    | Some (ty,impls) ->
-      EConstr.universes_of_constr evd ty, impls, Some (EConstr.to_constr evd ty)
-  in
-  let evd = Evd.restrict_universe_context evd uvars in
-  let uctx = UState.check_mono_univ_decl (Evd.evar_universe_context evd) UState.default_univ_decl in
-  let entry = Entries.{
-      prim_entry_type = typopt;
-      prim_entry_univs = uctx;
+  let loc = id.CAst.loc in
+  let id = id.CAst.v in
+  match typopt with
+  | None ->
+    if Option.has_some udecl then
+      CErrors.user_err ?loc
+        Pp.(strbrk "Cannot use a universe declaration without a type when declaring primitives.");
+    declare id {Entries.prim_entry_type = None; prim_entry_content = prim}
+  | Some typ ->
+    let env = Global.env () in
+    let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
+    let auctx = CPrimitives.op_or_type_univs prim in
+    let evd, u = Evd.with_context_set UState.univ_flexible evd (UnivGen.fresh_instance auctx) in
+    let expected_typ = EConstr.of_constr @@ Typeops.type_of_prim_or_type env u prim in
+    let evd, (typ,impls) =
+      Constrintern.(interp_type_evars_impls ~impls:empty_internalization_env)
+        env evd typ
+    in
+    let evd = Evarconv.unify_delay env evd typ expected_typ in
+    let evd = Evd.minimize_universes evd in
+    let uvars = EConstr.universes_of_constr evd typ in
+    let evd = Evd.restrict_universe_context evd uvars in
+    let typ = EConstr.to_constr evd typ in
+    let univs = Evd.check_univ_decl ~poly:(not (Univ.AUContext.is_empty auctx)) evd udecl in
+    let entry = {
+      Entries.prim_entry_type = Some (typ,univs);
       prim_entry_content = prim;
     }
-  in
-  let _kn : Names.Constant.t =
-    Declare.declare_constant ~name:id.CAst.v ~kind:Decls.IsPrimitive (Declare.PrimitiveEntry entry) in
-  Flags.if_verbose Feedback.msg_info Pp.(Names.Id.print id.CAst.v ++ str " is declared")
+    in
+    declare id entry
diff --git a/vernac/comPrimitive.mli b/vernac/comPrimitive.mli
index 588eb7fdea..4d468f97b1 100644
--- a/vernac/comPrimitive.mli
+++ b/vernac/comPrimitive.mli
@@ -8,4 +8,9 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val do_primitive : Names.lident -> CPrimitives.op_or_type -> Constrexpr.constr_expr option -> unit
+val do_primitive
+  : Names.lident
+  -> Constrexpr.universe_decl_expr option
+  -> CPrimitives.op_or_type
+  -> Constrexpr.constr_expr option
+  -> unit
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index e1f1affb2f..e0550fd744 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -234,7 +234,7 @@ GRAMMAR EXTEND Gram
           { VernacRegister(g, RegisterCoqlib quid) }
       | IDENT "Register"; IDENT "Inline"; g = global ->
           { VernacRegister(g, RegisterInline) }
-      | IDENT "Primitive"; id = identref; typopt = OPT [ ":"; typ = lconstr -> { typ } ]; ":="; r = register_token ->
+      | IDENT "Primitive"; id = ident_decl; typopt = OPT [ ":"; typ = lconstr -> { typ } ]; ":="; r = register_token ->
           { VernacPrimitive(id, r, typopt) }
       | IDENT "Universe"; l = LIST1 identref -> { VernacUniverse l }
       | IDENT "Universes"; l = LIST1 identref -> { VernacUniverse l }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 7af6a6a405..cb108b68ae 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1262,7 +1262,7 @@ open Pputils
         )
       | VernacPrimitive(id,r,typopt) ->
          hov 2
-             (keyword "Primitive" ++ spc() ++ pr_lident id ++
+             (keyword "Primitive" ++ spc() ++ pr_ident_decl id ++
                 (Option.cata (fun ty -> spc() ++ str":" ++ pr_spc_lconstr ty) (mt()) typopt) ++ spc() ++
                 str ":=" ++ spc() ++
                 str (CPrimitives.op_or_type_to_string r))
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index b0e483ee74..6ed8c59f9f 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2221,10 +2221,10 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
     VtNoProof(fun () ->
         unsupported_attributes atts;
         vernac_register qid r)
-  | VernacPrimitive (id, prim, typopt) ->
+  | VernacPrimitive ((id, udecl), prim, typopt) ->
     VtDefault(fun () ->
         unsupported_attributes atts;
-        ComPrimitive.do_primitive id prim typopt)
+        ComPrimitive.do_primitive id udecl prim typopt)
   | VernacComments l ->
     VtDefault(fun () ->
         unsupported_attributes atts;
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 06ac7f8d48..d8e17d00e3 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -438,7 +438,7 @@ type nonrec vernac_expr =
   | VernacSearch of searchable * Goal_select.t option * search_restriction
   | VernacLocate of locatable
   | VernacRegister of qualid * register_kind
-  | VernacPrimitive of lident * CPrimitives.op_or_type * constr_expr option
+  | VernacPrimitive of ident_decl * CPrimitives.op_or_type * constr_expr option
   | VernacComments of comment list
 
   (* Proof management *)