From e3764e1e857fce9b6d4cb018db676db3612c00a0 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 31 Aug 2020 08:52:05 +0200 Subject: Remove occurrences of Parray.reroot. --- kernel/cPrimitives.ml | 9 +-------- kernel/cPrimitives.mli | 1 - kernel/nativevalues.ml | 9 --------- kernel/nativevalues.mli | 4 ---- kernel/parray.mli | 1 - kernel/primred.ml | 5 ----- kernel/vmbytegen.ml | 1 - kernel/vmemitcodes.ml | 2 +- kernel/vmsymtable.ml | 2 -- kernel/vmvalues.ml | 1 - kernel/vmvalues.mli | 1 - test-suite/primitive/arrays/reroot.v | 22 ---------------------- theories/Array/PArray.v | 19 ------------------- theories/extraction/ExtrOCamlPArray.v | 1 - 14 files changed, 2 insertions(+), 76 deletions(-) delete mode 100644 test-suite/primitive/arrays/reroot.v diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index 314cb54d1d..5cd91b4e74 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -58,7 +58,6 @@ type t = | Arraydefault | Arrayset | Arraycopy - | Arrayreroot | Arraylength let parse = function @@ -110,7 +109,6 @@ let parse = function | "array_set" -> Arrayset | "array_length" -> Arraylength | "array_copy" -> Arraycopy - | "array_reroot" -> Arrayreroot | _ -> raise Not_found let equal (p1 : t) (p2 : t) = @@ -164,8 +162,7 @@ let hash = function | Arraydefault -> 45 | Arrayset -> 46 | Arraycopy -> 47 - | Arrayreroot -> 48 - | Arraylength -> 49 + | Arraylength -> 48 (* Should match names in nativevalues.ml *) let to_string = function @@ -216,7 +213,6 @@ let to_string = function | Arraydefault -> "arraydefault" | Arrayset -> "arrayset" | Arraycopy -> "arraycopy" - | Arrayreroot -> "arrayreroot" | Arraylength -> "arraylength" type const = @@ -302,7 +298,6 @@ let types = | Arraydefault -> [array_ty; PITT_param 1] | Arrayset -> [array_ty; int_ty; PITT_param 1; array_ty] | Arraycopy -> [array_ty; array_ty] - | Arrayreroot -> [array_ty; array_ty] | Arraylength -> [array_ty; int_ty] let one_param = @@ -360,7 +355,6 @@ let params = function | Arraydefault | Arrayset | Arraycopy - | Arrayreroot | Arraylength -> one_param let nparams x = List.length (params x) @@ -414,7 +408,6 @@ let univs = function | Arraydefault | Arrayset | Arraycopy - | Arrayreroot | Arraylength -> one_univ type arg_kind = diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 41b3bff465..0db643faf4 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -56,7 +56,6 @@ type t = | Arraydefault | Arrayset | Arraycopy - | Arrayreroot | Arraylength (** Can raise [Not_found]. diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 9e17f97a56..05c98e4b87 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -739,15 +739,6 @@ let arraycopy accu vA t = no_check_arraycopy t else accu vA t -let no_check_arrayreroot t = - of_parray (Parray.reroot (to_parray t)) -[@@ocaml.inline always] - -let arrayreroot accu vA t = - if is_parray t then - no_check_arrayreroot t - else accu vA t - let no_check_arraylength t = mk_uint (Parray.length (to_parray t)) [@@ocaml.inline always] diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 08c5bd7126..b9b75a9d7c 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -344,7 +344,6 @@ val arrayget : t -> t -> t -> t -> t (* accu A t n *) val arraydefault : t -> t -> t (* accu A t *) val arrayset : t -> t -> t -> t -> t -> t (* accu A t n v *) val arraycopy : t -> t -> t -> t (* accu A t *) -val arrayreroot : t -> t -> t -> t (* accu A t *) val arraylength : t -> t -> t -> t (* accu A t *) val arrayinit : t -> t -> t -> t (* accu A n f def *) val arraymap : t -> t -> t (* accu A B f t *) @@ -364,8 +363,5 @@ val no_check_arrayset : t -> t -> t -> t val no_check_arraycopy : t -> t [@@ocaml.inline always] -val no_check_arrayreroot : t -> t -[@@ocaml.inline always] - val no_check_arraylength : t -> t [@@ocaml.inline always] diff --git a/kernel/parray.mli b/kernel/parray.mli index 0276278bd0..8b6565c159 100644 --- a/kernel/parray.mli +++ b/kernel/parray.mli @@ -19,7 +19,6 @@ val default : 'a t -> 'a val make : Uint63.t -> 'a -> 'a t val init : Uint63.t -> (int -> 'a) -> 'a -> 'a t val copy : 'a t -> 'a t -val reroot : 'a t -> 'a t val map : ('a -> 'b) -> 'a t -> 'b t diff --git a/kernel/primred.ml b/kernel/primred.ml index 90eeeb9be7..f158cfacea 100644 --- a/kernel/primred.ml +++ b/kernel/primred.ml @@ -365,11 +365,6 @@ struct 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) diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml index 375b1aface..16a0f42664 100644 --- a/kernel/vmbytegen.ml +++ b/kernel/vmbytegen.ml @@ -508,7 +508,6 @@ let is_caml_prim = let open CPrimitives in function | Arraydefault | Arrayset | Arraycopy - | Arrayreroot | Arraylength -> true | _ -> false diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml index f913cb906c..ec8601edc9 100644 --- a/kernel/vmemitcodes.ml +++ b/kernel/vmemitcodes.ml @@ -262,7 +262,7 @@ let check_prim_op = function | Arraymake -> opISINT_CAML_CALL2 | Arrayget -> opISARRAY_INT_CAML_CALL2 | Arrayset -> opISARRAY_INT_CAML_CALL3 - | Arraydefault | Arraycopy | Arrayreroot | Arraylength -> + | Arraydefault | Arraycopy | Arraylength -> opISARRAY_CAML_CALL1 let emit_instr env = function diff --git a/kernel/vmsymtable.ml b/kernel/vmsymtable.ml index 4ad830a298..9d80dc578b 100644 --- a/kernel/vmsymtable.ml +++ b/kernel/vmsymtable.ml @@ -69,7 +69,6 @@ let parray_get = set_global Vmvalues.parray_get let parray_get_default = set_global Vmvalues.parray_get_default let parray_set = set_global Vmvalues.parray_set let parray_copy = set_global Vmvalues.parray_copy -let parray_reroot = set_global Vmvalues.parray_reroot let parray_length = set_global Vmvalues.parray_length (* table pour les structured_constant et les annotations des switchs *) @@ -135,7 +134,6 @@ let slot_for_caml_prim = | Arraydefault -> parray_get_default | Arrayset -> parray_set | Arraycopy -> parray_copy - | Arrayreroot -> parray_reroot | Arraylength -> parray_length | _ -> assert false diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 0678f37a0b..2068133b10 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -700,5 +700,4 @@ let parray_get = Obj.magic Parray.get let parray_get_default = Obj.magic Parray.default let parray_set = Obj.magic Parray.set let parray_copy = Obj.magic Parray.copy -let parray_reroot = Obj.magic Parray.reroot let parray_length = Obj.magic Parray.length diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 6632dc46b2..d15595766a 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -204,5 +204,4 @@ val parray_get : values val parray_get_default : values val parray_set : values val parray_copy : values -val parray_reroot : values val parray_length : values diff --git a/test-suite/primitive/arrays/reroot.v b/test-suite/primitive/arrays/reroot.v deleted file mode 100644 index 172a118cc7..0000000000 --- a/test-suite/primitive/arrays/reroot.v +++ /dev/null @@ -1,22 +0,0 @@ -From Coq Require Import Int63 PArray. - -Open Scope array_scope. - -Definition t : array nat := [| 1; 5; 2 | 4 |]. -Definition t' : array nat := PArray.reroot t. - -Definition foo1 := (eq_refl : t'.[1] = 5). -Definition foo2 := (eq_refl 5 <: t'.[1] = 5). -Definition foo3 := (eq_refl 5 <<: t'.[1] = 5). -Definition x1 := Eval compute in t'.[1]. -Definition foo4 := (eq_refl : x1 = 5). -Definition x2 := Eval cbn in t'.[1]. -Definition foo5 := (eq_refl : x2 = 5). - -Definition foo6 := (eq_refl : t.[1] = 5). -Definition foo7 := (eq_refl 5 <: t.[1] = 5). -Definition foo8 := (eq_refl 5 <<: t.[1] = 5). -Definition x3 := Eval compute in t.[1]. -Definition foo9 := (eq_refl : x3 = 5). -Definition x4 := Eval cbn in t.[1]. -Definition foo10 := (eq_refl : x4 = 5). diff --git a/theories/Array/PArray.v b/theories/Array/PArray.v index 3511ba0918..e91a5bf9ad 100644 --- a/theories/Array/PArray.v +++ b/theories/Array/PArray.v @@ -22,12 +22,6 @@ Arguments length {_} _. Primitive copy : forall A, array A -> array A := #array_copy. Arguments copy {_} _. -(* [reroot t] produces an array that is extensionaly equal to [t], but whose - history has been squashed. Useful when performing multiple accesses in an old - copy of an array that has been updated. *) -Primitive reroot : forall A, array A -> array A := #array_reroot. -Arguments reroot {_} _. - Module Export PArrayNotations. Declare Scope array_scope. @@ -64,9 +58,6 @@ Axiom length_set : forall A t i (a:A), Axiom get_copy : forall A (t:array A) i, (copy t).[i] = t.[i]. Axiom length_copy : forall A (t:array A), length (copy t) = length t. -Axiom get_reroot : forall A (t:array A) i, (reroot t).[i] = t.[i]. -Axiom length_reroot : forall A (t:array A), length (reroot t) = length t. - Axiom array_ext : forall A (t1 t2:array A), length t1 = length t2 -> (forall i, i t1.[i] = t2.[i]) -> @@ -94,16 +85,6 @@ Proof. rewrite !get_out_of_bounds in get_make; assumption. Qed. -Lemma default_reroot A (t:array A) : default (reroot t) = default t. -Proof. - assert (irr_lt : length t "Parray.default". Extract Constant PArray.set => "Parray.set". Extract Constant PArray.length => "Parray.length". Extract Constant PArray.copy => "Parray.copy". -Extract Constant PArray.reroot => "Parray.reroot". -- cgit v1.2.3