1 files changed, 89 insertions, 31 deletions

diff --git a/kernel/primred.ml b/kernel/primred.ml
index c475828cb3..90eeeb9be7 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -5,55 +5,71 @@ open Retroknowledge
 open Environ
 open CErrors
 
-let add_retroknowledge env action =
+type _ action_kind =
+  | IncompatTypes : _ prim_type -> Constant.t action_kind
+  | IncompatInd : _ prim_ind -> inductive action_kind
+
+type exn += IncompatibleDeclarations : 'a action_kind * 'a * 'a -> exn
+
+let check_same_types typ c1 c2 =
+  if not (Constant.equal c1 c2)
+  then raise (IncompatibleDeclarations (IncompatTypes typ, c1, c2))
+
+let check_same_inds ind i1 i2 =
+  if not (eq_ind i1 i2)
+  then raise (IncompatibleDeclarations (IncompatInd ind, i1, i2))
+
+let add_retroknowledge retro action =
   match action with
-  | Register_type(PT_int63,c) ->
-    let retro = env.retroknowledge in
-    let retro =
-      match retro.retro_int63 with
-      | None -> { retro with retro_int63 = Some c }
-      | Some c' -> assert (Constant.equal c c'); retro in
-    set_retroknowledge env retro
-  | Register_type(PT_float64,c) ->
-    let retro = env.retroknowledge in
-    let retro =
-      match retro.retro_float64 with
-      | None -> { retro with retro_float64 = Some c }
-      | Some c' -> assert (Constant.equal c c'); retro in
-    set_retroknowledge env retro
+  | Register_type(typ,c) ->
+    begin match typ with
+      | PT_int63 ->
+        (match retro.retro_int63 with
+         | None -> { retro with retro_int63 = Some c }
+         | Some c' -> check_same_types typ c c'; retro)
+
+      | PT_float64 ->
+        (match retro.retro_float64 with
+         | None -> { retro with retro_float64 = Some c }
+         | Some c' -> check_same_types typ c c'; retro)
+
+      | PT_array ->
+        (match retro.retro_array with
+         | None -> { retro with retro_array = Some c }
+         | Some c' -> check_same_types typ c c'; retro)
+    end
+
   | Register_ind(pit,ind) ->
-    let retro = env.retroknowledge in
-    let retro =
-      match pit with
+    begin match pit with
       | PIT_bool ->
         let r =
           match retro.retro_bool with
           | None -> ((ind,1), (ind,2))
-          | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in
+          | Some (((ind',_),_) as t) -> check_same_inds pit ind ind'; t in
         { retro with retro_bool = Some r }
       | PIT_carry ->
         let r =
           match retro.retro_carry with
           | None -> ((ind,1), (ind,2))
-          | Some (((ind',_),_) as t) -> assert (eq_ind ind ind'); t in
+          | Some (((ind',_),_) as t) -> check_same_inds pit ind ind'; t in
         { retro with retro_carry = Some r }
       | PIT_pair ->
         let r =
           match retro.retro_pair with
           | None -> (ind,1)
-          | Some ((ind',_) as t) -> assert (eq_ind ind ind'); t in
+          | Some ((ind',_) as t) -> check_same_inds pit ind ind'; t in
         { retro with retro_pair = Some r }
       | PIT_cmp ->
         let r =
           match retro.retro_cmp with
           | None -> ((ind,1), (ind,2), (ind,3))
-          | Some (((ind',_),_,_) as t) -> assert (eq_ind ind ind'); t in
+          | Some (((ind',_),_,_) as t) -> check_same_inds pit ind ind'; t in
         { retro with retro_cmp = Some r }
       | PIT_f_cmp ->
         let r =
           match retro.retro_f_cmp with
           | None -> ((ind,1), (ind,2), (ind,3), (ind,4))
-          | Some (((ind',_),_,_,_) as t) -> assert (eq_ind ind ind'); t in
+          | Some (((ind',_),_,_,_) as t) -> check_same_inds pit ind ind'; t in
         { retro with retro_f_cmp = Some r }
       | PIT_f_class ->
         let r =
@@ -62,10 +78,12 @@ let add_retroknowledge env action =
                      (ind,5), (ind,6), (ind,7), (ind,8),
                      (ind,9))
           | Some (((ind',_),_,_,_,_,_,_,_,_) as t) ->
-             assert (eq_ind ind ind'); t in
+            check_same_inds pit ind ind'; t in
         { retro with retro_f_class = Some r }
-    in
-    set_retroknowledge env retro
+    end
+
+let add_retroknowledge env action =
+  set_retroknowledge env (add_retroknowledge env.retroknowledge action)
 
 let get_int_type env =
   match env.retroknowledge.retro_int63 with
@@ -120,10 +138,12 @@ module type RedNativeEntries =
     type elem
     type args
     type evd (* will be unit in kernel, evar_map outside *)
+    type uinstance
 
     val get : args -> int -> elem
     val get_int : evd -> elem -> Uint63.t
     val get_float : evd -> elem -> Float64.t
+    val get_parray : evd -> elem -> elem Parray.t
     val mkInt : env -> Uint63.t -> elem
     val mkFloat : env -> Float64.t -> elem
     val mkBool : env -> bool -> elem
@@ -146,6 +166,7 @@ module type RedNativeEntries =
     val mkPInf : env -> elem
     val mkNInf : env -> elem
     val mkNaN : env -> elem
+    val mkArray : env -> uinstance -> elem Parray.t -> elem -> elem
   end
 
 module type RedNative =
@@ -153,17 +174,20 @@ module type RedNative =
    type elem
    type args
    type evd
-   val red_prim : env -> evd -> CPrimitives.t -> args -> elem option
+   type uinstance
+   val red_prim : env -> evd -> CPrimitives.t -> uinstance -> args -> elem option
  end
 
 module RedNative (E:RedNativeEntries) :
   RedNative with type elem = E.elem
   with type args = E.args
-  with type evd = E.evd =
+  with type evd = E.evd
+  with type uinstance = E.uinstance =
 struct
   type elem = E.elem
   type args = E.args
   type evd = E.evd
+  type uinstance = E.uinstance
 
   let get_int evd args i = E.get_int evd (E.get args i)
 
@@ -180,7 +204,9 @@ struct
 
   let get_float2 evd args = get_float evd args 0, get_float evd args 1
 
-  let red_prim_aux env evd op args =
+  let get_parray evd args i = E.get_parray evd (E.get args i)
+
+  let red_prim_aux env evd op u args =
     let open CPrimitives in
     match op with
     | Int63head0 ->
@@ -315,11 +341,43 @@ struct
       let f = get_float1 evd args in E.mkFloat env (Float64.next_up f)
     | Float64next_down ->
       let f = get_float1 evd args in E.mkFloat env (Float64.next_down f)
+    | Arraymake ->
+      let ty = E.get args 0 in
+      let i = get_int evd args 1 in
+      let d = E.get args 2 in
+      E.mkArray env u (Parray.make i d) ty
+    | Arrayget ->
+      let t = get_parray evd args 1 in
+      let i = get_int evd args 2 in
+      Parray.get t i
+    | Arraydefault ->
+      let t = get_parray evd args 1 in
+      Parray.default t
+    | Arrayset ->
+      let ty = E.get args 0 in
+      let t = get_parray evd args 1 in
+      let i = get_int evd args 2 in
+      let a = E.get args 3 in
+      let t' = Parray.set t i a in
+      E.mkArray env u t' ty
+    | Arraycopy ->
+      let ty = E.get args 0 in
+      let t = get_parray evd args 1 in
+      let t' = Parray.copy t in
+      E.mkArray env u t' ty
+    | Arrayreroot ->
+      let ar = E.get args 1 in
+      let t = E.get_parray evd ar in
+      let _ = Parray.reroot t in
+      ar
+    | Arraylength ->
+      let t = get_parray evd args 1 in
+      E.mkInt env (Parray.length t)
 
-  let red_prim env evd p args =
+  let red_prim env evd p u args =
     try
       let r =
-        red_prim_aux env evd p args
+        red_prim_aux env evd p u args
       in Some r
     with NativeDestKO -> None