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>

4 files changed, 32 insertions, 9 deletions

diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 3bed329d31..bb062bfc11 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -86,7 +86,7 @@ let constr_val_discr_st sigma ts t =
     | Sort _ -> Label(SortLabel, [])
     | Evar _ -> Everything
     | Rel _ | Meta _ | Cast _ | LetIn _ | App _ | Case _ | Fix _ | CoFix _
-    | Proj _ | Int _ | Float _ -> Nothing
+    | Proj _ | Int _ | Float _ | Array _ -> Nothing
 
 let constr_pat_discr_st ts t =
   let open GlobRef in
diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 74f793cdfb..dfbcc9fbce 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -620,7 +620,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
                 end
               end
         end
-       | exception NotEvaluableConst (IsPrimitive p) when Stack.check_native_args p stack ->
+       | exception NotEvaluableConst (IsPrimitive (u,p)) when Stack.check_native_args p stack ->
           let kargs = CPrimitives.kind p in
           let (kargs,o) = Stack.get_next_primitive_args kargs stack in
           (* Should not fail thanks to [check_native_args] *)
@@ -759,9 +759,9 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
         |_ -> fold ()
       else fold ()
 
-    | Int _ | Float _ ->
+    | Int _ | Float _ | Array _ ->
       begin match Stack.strip_app stack with
-       | (_, Stack.Primitive(p,kn,rargs,kargs,cst_l')::s) ->
+       | (_, Stack.Primitive(p,(_,u as kn),rargs,kargs,cst_l')::s) ->
          let more_to_reduce = List.exists (fun k -> CPrimitives.Kwhnf = k) kargs in
          if more_to_reduce then
            let (kargs,o) = Stack.get_next_primitive_args kargs s in
@@ -775,8 +775,9 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
              try List.chop n args
              with List.IndexOutOfRange -> (args,[]) (* FIXME probably useless *)
            in
+           let s = extra_args @ s in
            let args = Array.of_list (Option.get (Stack.list_of_app_stack (rargs @ Stack.append_app [|x|] args))) in
-             begin match CredNative.red_prim env sigma p args with
+             begin match CredNative.red_prim env sigma p u args with
                | Some t -> whrec cst_l' (t,s)
                | None -> ((mkApp (mkConstU kn, args), s), cst_l)
              end
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index d5358faf59..ec770e2473 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -417,7 +417,7 @@ let compute_constructor_signatures ~rec_flag ((_,k as ity),u) =
     | RelDecl.LocalAssum _ :: c, recarg::rest ->
         let rest = analrec c rest in
         begin match Declareops.dest_recarg recarg with
-        | Norec | Imbr _  -> true :: rest
+        | Norec | Nested _  -> true :: rest
         | Mrec (_,j)  ->
             if rec_flag && Int.equal j k then true :: true :: rest
             else true :: rest
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 0f76fdda79..3bcd235b41 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -46,6 +46,7 @@ struct
     | DCoFix  of int * 't array * 't array
     | DInt    of Uint63.t
     | DFloat  of Float64.t
+    | DArray  of 't array * 't * 't
 
     (* special constructors only inside the left-hand side of DCtx or
        DApp. Used to encode lists of foralls/letins/apps as contexts *)
@@ -69,6 +70,7 @@ struct
           Some t' -> str ":=" ++ f t'
         | None -> str "") ++ spc() ++ str "::" ++ spc() ++ f tl
     | DNil -> str "[]"
+    | DArray _ -> str "ARRAY"
 
   (*
    * Functional iterators for the t datatype
@@ -86,6 +88,7 @@ struct
     | DCoFix(i,ta,ca) ->
         DCoFix (i,Array.map f ta,Array.map f ca)
     | DCons ((t,topt),u) -> DCons ((f t,Option.map f topt), f u)
+    | DArray (t,def,ty) -> DArray(Array.map f t, f def, f ty)
 
   let compare_ci ci1 ci2 =
     let c = ind_ord ci1.ci_ind ci2.ci_ind in
@@ -157,6 +160,17 @@ struct
 
   | DFloat _, _ -> -1 | _, DFloat _ -> 1
 
+  | DArray(t1,def1,ty1), DArray(t2,def2,ty2) ->
+    let c =  Array.compare cmp t1 t2 in
+    if c = 0 then
+      let c = cmp def1 def2 in
+      if c = 0 then
+      cmp ty1 ty2
+      else c
+    else c
+
+  | DArray _, _ -> -1 | _, DArray _ -> 1
+
   | DCons ((t1, ot1), u1), DCons ((t2, ot2), u2) ->
      let c = cmp t1 t2 in
      if Int.equal c 0 then
@@ -178,6 +192,7 @@ struct
         Array.fold_left f (Array.fold_left f acc ta) ca
     | DCoFix(i,ta,ca) ->
         Array.fold_left f (Array.fold_left f acc ta) ca
+    | DArray(t,def,ty) -> f (f (Array.fold_left f acc t) def) ty
     | DCons ((t,topt),u) -> f (Option.fold_left f (f acc t) topt) u
 
   let choose f = function
@@ -189,6 +204,7 @@ struct
     | DFix (ia,i,ta,ca) -> f ta.(0)
     | DCoFix (i,ta,ca) -> f ta.(0)
     | DCons ((t,topt),u) -> f u
+    | DArray(t,def,ty) -> f t.(0)
 
   let dummy_cmp () () = 0
 
@@ -208,10 +224,12 @@ struct
             Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2
         | DCoFix(i,ta1,ca1), DCoFix(_,ta2,ca2) ->
             Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2
+              | DArray(t1,def1,ty1), DArray(t2,def2,ty2) ->
+            f (f (Array.fold_left2 f acc t1 t2) def1 def2) ty1 ty2
         | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) ->
             f (Option.fold_left2 f (f acc t1 t2) topt1 topt2) u1 u2
         | (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _
-           | DFix _ | DCoFix _ | DCons _ | DInt _ | DFloat _), _ -> assert false
+           | DFix _ | DCoFix _ | DCons _ | DInt _ | DFloat _| DArray _), _ -> assert false
 
   let map2 (f:'a -> 'b -> 'c) (c1:'a t) (c2:'b t) : 'c t =
     let head w = map (fun _ -> ()) w in
@@ -230,14 +248,16 @@ struct
             DFix (ia,i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2)
         | DCoFix (i,ta1,ca1), DCoFix (_,ta2,ca2) ->
             DCoFix (i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2)
+              | DArray(t1,def1,ty1), DArray(t2,def2,ty2) ->
+                DArray(Array.map2 f t1 t2, f def1 def2, f ty1 ty2)
         | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) ->
             DCons ((f t1 t2,Option.lift2 f topt1 topt2), f u1 u2)
         | (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _
-           | DFix _ | DCoFix _ | DCons _ | DInt _ | DFloat _), _ -> assert false
+           | DFix _ | DCoFix _ | DCons _ | DInt _ | DFloat _ | DArray _), _ -> assert false
 
   let terminal = function
     | (DRel | DSort | DNil | DRef _ | DInt _ | DFloat _) -> true
-    | DLambda _ | DApp _ | DCase _ | DFix _ | DCoFix _ | DCtx _ | DCons _ ->
+    | DLambda _ | DApp _ | DCase _ | DFix _ | DCoFix _ | DCtx _ | DCons _ | DArray _ ->
       false
 
   let compare t1 t2 = compare dummy_cmp t1 t2
@@ -332,6 +352,8 @@ struct
         Term (DApp (Term (DRef (ConstRef (Projection.constant p))), pat_of_constr c))
     | Int i -> Term (DInt i)
     | Float f -> Term (DFloat f)
+    | Array (_u,t,def,ty) ->
+      Term (DArray (Array.map pat_of_constr t, pat_of_constr def, pat_of_constr ty))
 
     and ctx_of_constr ctx c = match Constr.kind c with
     | Prod (_,t,c)   -> ctx_of_constr (Term(DCons((pat_of_constr t,None),ctx))) c