aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--clib/cArray.ml12
-rw-r--r--clib/cArray.mli42
-rw-r--r--engine/eConstr.ml20
-rw-r--r--engine/termops.ml2
-rw-r--r--kernel/cClosure.ml32
-rw-r--r--kernel/constr.ml28
-rw-r--r--kernel/esubst.ml2
-rw-r--r--kernel/reduction.ml2
-rw-r--r--pretyping/reductionops.ml4
9 files changed, 78 insertions, 66 deletions
diff --git a/clib/cArray.ml b/clib/cArray.ml
index 6ea46655f..b26dae729 100644
--- a/clib/cArray.ml
+++ b/clib/cArray.ml
@@ -81,6 +81,18 @@ sig
val fold_left_map : ('a -> 'b -> 'a * 'b) -> 'a -> 'b array -> 'a * 'b array
val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'c) -> 'a -> 'b array -> 'c array -> 'a * 'c array
end
+ module Fun1 :
+ sig
+ val map : ('r -> 'a -> 'b) -> 'r -> 'a array -> 'b array
+ val smartmap : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array
+ [@@ocaml.deprecated "Same as [Fun1.Smart.map]"]
+ val iter : ('r -> 'a -> unit) -> 'r -> 'a array -> unit
+ val iter2 : ('r -> 'a -> 'b -> unit) -> 'r -> 'a array -> 'b array -> unit
+ module Smart :
+ sig
+ val map : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array
+ end
+ end
end
include Array
diff --git a/clib/cArray.mli b/clib/cArray.mli
index d800e79ed..8bf33f82f 100644
--- a/clib/cArray.mli
+++ b/clib/cArray.mli
@@ -163,32 +163,32 @@ sig
of the main ones, when the returned array is of same type as one of
the original array. *)
-end
-
-include ExtS
+ module Fun1 :
+ sig
+ val map : ('r -> 'a -> 'b) -> 'r -> 'a array -> 'b array
+ (** [Fun1.map f x v = map (f x) v] *)
-module Fun1 :
-sig
- val map : ('r -> 'a -> 'b) -> 'r -> 'a array -> 'b array
- (** [Fun1.map f x v = map (f x) v] *)
+ val smartmap : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array
+ [@@ocaml.deprecated "Same as [Fun1.Smart.map]"]
- val smartmap : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array
- [@@ocaml.deprecated "Same as [Fun1.Smart.map]"]
+ val iter : ('r -> 'a -> unit) -> 'r -> 'a array -> unit
+ (** [Fun1.iter f x v = iter (f x) v] *)
- val iter : ('r -> 'a -> unit) -> 'r -> 'a array -> unit
- (** [Fun1.iter f x v = iter (f x) v] *)
+ val iter2 : ('r -> 'a -> 'b -> unit) -> 'r -> 'a array -> 'b array -> unit
+ (** [Fun1.iter2 f x v1 v2 = iter (f x) v1 v2] *)
- val iter2 : ('r -> 'a -> 'b -> unit) -> 'r -> 'a array -> 'b array -> unit
- (** [Fun1.iter2 f x v1 v2 = iter (f x) v1 v2] *)
+ module Smart :
+ sig
+ val map : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array
+ (** [Fun1.Smart.map f x v = Smart.map (f x) v] *)
+ end
- module Smart :
- sig
- val map : ('r -> 'a -> 'a) -> 'r -> 'a array -> 'a array
- (** [Fun1.Smart.map f x v = Smart.map (f x) v] *)
end
+ (** The functions defined in this module are the same as the main ones, except
+ that they are all higher-order, and their function arguments have an
+ additional parameter. This allows us to prevent closure creation in critical
+ cases. *)
end
-(** The functions defined in this module are the same as the main ones, except
- that they are all higher-order, and their function arguments have an
- additional parameter. This allows us to prevent closure creation in critical
- cases. *)
+
+include ExtS
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index f14122ca1..f1530b2d1 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -339,7 +339,7 @@ let map_with_binders sigma g f l c0 = match kind sigma c0 with
else mkLetIn (na, b', t', c')
| App (c, al) ->
let c' = f l c in
- let al' = CArray.Fun1.Smart.map f l al in
+ let al' = Array.Fun1.Smart.map f l al in
if c' == c && al' == al then c0
else mkApp (c', al')
| Proj (p, t) ->
@@ -347,25 +347,25 @@ let map_with_binders sigma g f l c0 = match kind sigma c0 with
if t' == t then c0
else mkProj (p, t')
| Evar (e, al) ->
- let al' = CArray.Fun1.Smart.map f l al in
+ let al' = Array.Fun1.Smart.map f l al in
if al' == al then c0
else mkEvar (e, al')
| Case (ci, p, c, bl) ->
let p' = f l p in
let c' = f l c in
- let bl' = CArray.Fun1.Smart.map f l bl in
+ let bl' = Array.Fun1.Smart.map f l bl in
if p' == p && c' == c && bl' == bl then c0
else mkCase (ci, p', c', bl')
| Fix (ln, (lna, tl, bl)) ->
- let tl' = CArray.Fun1.Smart.map f l tl in
+ let tl' = Array.Fun1.Smart.map f l tl in
let l' = iterate g (Array.length tl) l in
- let bl' = CArray.Fun1.Smart.map f l' bl in
+ let bl' = Array.Fun1.Smart.map f l' bl in
if tl' == tl && bl' == bl then c0
else mkFix (ln,(lna,tl',bl'))
| CoFix(ln,(lna,tl,bl)) ->
- let tl' = CArray.Fun1.Smart.map f l tl in
+ let tl' = Array.Fun1.Smart.map f l tl in
let l' = iterate g (Array.length tl) l in
- let bl' = CArray.Fun1.Smart.map f l' bl in
+ let bl' = Array.Fun1.Smart.map f l' bl in
mkCoFix (ln,(lna,tl',bl'))
let iter sigma f c = match kind sigma c with
@@ -391,9 +391,9 @@ let iter_with_full_binders sigma g f n c =
| Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
| Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
| LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c
- | App (c,l) -> f n c; CArray.Fun1.iter f n l
- | Evar (_,l) -> CArray.Fun1.iter f n l
- | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl
+ | App (c,l) -> f n c; Array.Fun1.iter f n l
+ | Evar (_,l) -> Array.Fun1.iter f n l
+ | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
| Proj (p,c) -> f n c
| Fix (_,(lna,tl,bl)) ->
Array.iter (f n) tl;
diff --git a/engine/termops.ml b/engine/termops.ml
index c271d9d99..053fcc3db 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -931,7 +931,7 @@ let dependent_main noevar sigma m t =
match EConstr.kind sigma m, EConstr.kind sigma t with
| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
- CArray.Fun1.iter deprec m
+ Array.Fun1.iter deprec m
(Array.sub lt
(Array.length lm) ((Array.length lt) - (Array.length lm)))
| _, Cast (c,_,_) when noevar && isMeta sigma c -> ()
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 08114abc4..435cf0a79 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -482,7 +482,7 @@ let rec lft_fconstr n ft =
let lift_fconstr k f =
if Int.equal k 0 then f else lft_fconstr k f
let lift_fconstr_vect k v =
- if Int.equal k 0 then v else CArray.Fun1.map lft_fconstr k v
+ if Int.equal k 0 then v else Array.Fun1.map lft_fconstr k v
let clos_rel e i =
match expand_rel i e with
@@ -547,7 +547,7 @@ let mk_clos_vect env v = match v with
| [|v0; v1; v2|] -> [|mk_clos env v0; mk_clos env v1; mk_clos env v2|]
| [|v0; v1; v2; v3|] ->
[|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|]
-| v -> CArray.Fun1.map mk_clos env v
+| v -> Array.Fun1.map mk_clos env v
(* Translate the head constructor of t from constr to fconstr. This
function is parameterized by the function to apply on the direct
@@ -562,7 +562,7 @@ let mk_clos_deep clos_fun env t =
term = FCast (clos_fun env a, k, clos_fun env b)}
| App (f,v) ->
{ norm = Red;
- term = FApp (clos_fun env f, CArray.Fun1.map clos_fun env v) }
+ term = FApp (clos_fun env f, Array.Fun1.map clos_fun env v) }
| Proj (p,c) ->
{ norm = Red;
term = FProj (p, clos_fun env c) }
@@ -605,21 +605,21 @@ let rec to_constr constr_fun lfts v =
Array.map (fun b -> constr_fun lfts (mk_clos env b)) ve)
| FFix ((op,(lna,tys,bds)),e) ->
let n = Array.length bds in
- let ftys = CArray.Fun1.map mk_clos e tys in
- let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in
+ let ftys = Array.Fun1.map mk_clos e tys in
+ let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in
let lfts' = el_liftn n lfts in
- mkFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys,
- CArray.Fun1.map constr_fun lfts' fbds))
+ mkFix (op, (lna, Array.Fun1.map constr_fun lfts ftys,
+ Array.Fun1.map constr_fun lfts' fbds))
| FCoFix ((op,(lna,tys,bds)),e) ->
let n = Array.length bds in
- let ftys = CArray.Fun1.map mk_clos e tys in
- let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in
+ let ftys = Array.Fun1.map mk_clos e tys in
+ let fbds = Array.Fun1.map mk_clos (subs_liftn n e) bds in
let lfts' = el_liftn (Array.length bds) lfts in
- mkCoFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys,
- CArray.Fun1.map constr_fun lfts' fbds))
+ mkCoFix (op, (lna, Array.Fun1.map constr_fun lfts ftys,
+ Array.Fun1.map constr_fun lfts' fbds))
| FApp (f,ve) ->
mkApp (constr_fun lfts f,
- CArray.Fun1.map constr_fun lfts ve)
+ Array.Fun1.map constr_fun lfts ve)
| FProj (p,c) ->
mkProj (p,constr_fun lfts c)
@@ -1024,14 +1024,14 @@ and norm_head info tab m =
| FProd(na,dom,rng) ->
mkProd(na, kl info tab dom, kl info tab rng)
| FCoFix((n,(na,tys,bds)),e) ->
- let ftys = CArray.Fun1.map mk_clos e tys in
+ let ftys = Array.Fun1.map mk_clos e tys in
let fbds =
- CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
+ Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
mkCoFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
| FFix((n,(na,tys,bds)),e) ->
- let ftys = CArray.Fun1.map mk_clos e tys in
+ let ftys = Array.Fun1.map mk_clos e tys in
let fbds =
- CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
+ Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
| FEvar((i,args),env) ->
mkEvar(i, Array.map (fun a -> kl info tab (mk_clos env a)) args)
diff --git a/kernel/constr.ml b/kernel/constr.ml
index a1779b36d..8f83d6baa 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -468,16 +468,16 @@ let iter_with_binders g f n c = match kind c with
| Prod (_,t,c) -> f n t; f (g n) c
| Lambda (_,t,c) -> f n t; f (g n) c
| LetIn (_,b,t,c) -> f n b; f n t; f (g n) c
- | App (c,l) -> f n c; CArray.Fun1.iter f n l
- | Evar (_,l) -> CArray.Fun1.iter f n l
- | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl
+ | App (c,l) -> f n c; Array.Fun1.iter f n l
+ | Evar (_,l) -> Array.Fun1.iter f n l
+ | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
| Proj (p,c) -> f n c
| Fix (_,(_,tl,bl)) ->
- CArray.Fun1.iter f n tl;
- CArray.Fun1.iter f (iterate g (Array.length tl) n) bl
+ Array.Fun1.iter f n tl;
+ Array.Fun1.iter f (iterate g (Array.length tl) n) bl
| CoFix (_,(_,tl,bl)) ->
- CArray.Fun1.iter f n tl;
- CArray.Fun1.iter f (iterate g (Array.length tl) n) bl
+ Array.Fun1.iter f n tl;
+ Array.Fun1.iter f (iterate g (Array.length tl) n) bl
(* [map f c] maps [f] on the immediate subterms of [c]; it is
not recursive and the order with which subterms are processed is
@@ -625,7 +625,7 @@ let map_with_binders g f l c0 = match kind c0 with
else mkLetIn (na, b', t', c')
| App (c, al) ->
let c' = f l c in
- let al' = CArray.Fun1.Smart.map f l al in
+ let al' = Array.Fun1.Smart.map f l al in
if c' == c && al' == al then c0
else mkApp (c', al')
| Proj (p, t) ->
@@ -633,25 +633,25 @@ let map_with_binders g f l c0 = match kind c0 with
if t' == t then c0
else mkProj (p, t')
| Evar (e, al) ->
- let al' = CArray.Fun1.Smart.map f l al in
+ let al' = Array.Fun1.Smart.map f l al in
if al' == al then c0
else mkEvar (e, al')
| Case (ci, p, c, bl) ->
let p' = f l p in
let c' = f l c in
- let bl' = CArray.Fun1.Smart.map f l bl in
+ let bl' = Array.Fun1.Smart.map f l bl in
if p' == p && c' == c && bl' == bl then c0
else mkCase (ci, p', c', bl')
| Fix (ln, (lna, tl, bl)) ->
- let tl' = CArray.Fun1.Smart.map f l tl in
+ let tl' = Array.Fun1.Smart.map f l tl in
let l' = iterate g (Array.length tl) l in
- let bl' = CArray.Fun1.Smart.map f l' bl in
+ let bl' = Array.Fun1.Smart.map f l' bl in
if tl' == tl && bl' == bl then c0
else mkFix (ln,(lna,tl',bl'))
| CoFix(ln,(lna,tl,bl)) ->
- let tl' = CArray.Fun1.Smart.map f l tl in
+ let tl' = Array.Fun1.Smart.map f l tl in
let l' = iterate g (Array.length tl) l in
- let bl' = CArray.Fun1.Smart.map f l' bl in
+ let bl' = Array.Fun1.Smart.map f l' bl in
mkCoFix (ln,(lna,tl',bl'))
type instance_compare_fn = GlobRef.t -> int ->
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 91cc64523..4b8edf63f 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -140,7 +140,7 @@ let rec comp mk_cl s1 s2 =
| ESID _, _ -> s2
| SHIFT(k,s), _ -> subs_shft(k, comp mk_cl s s2)
| _, CONS(x,s') ->
- CONS(CArray.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s')
+ CONS(Array.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s')
| CONS(x,s), SHIFT(k,s') ->
let lg = Array.length x in
if k == lg then comp mk_cl s s'
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 81fbd4f5e..38106fbf6 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -84,7 +84,7 @@ let map_lift (l : lift) (v : fconstr array) = match v with
| [|c0; c1|] -> [|(l, c0); (l, c1)|]
| [|c0; c1; c2|] -> [|(l, c0); (l, c1); (l, c2)|]
| [|c0; c1; c2; c3|] -> [|(l, c0); (l, c1); (l, c2); (l, c3)|]
-| v -> CArray.Fun1.map (fun l t -> (l, t)) l v
+| v -> Array.Fun1.map (fun l t -> (l, t)) l v
let pure_stack lfts stk =
let rec pure_rec lfts stk =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index e07ed7711..6fde86837 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1404,7 +1404,7 @@ let plain_instance sigma s c =
| Meta p -> (try lift n (Metamap.find p s) with Not_found -> u)
| App (f,l) when isCast sigma f ->
let (f,_,t) = destCast sigma f in
- let l' = CArray.Fun1.Smart.map irec n l in
+ let l' = Array.Fun1.Smart.map irec n l in
(match EConstr.kind sigma f with
| Meta p ->
(* Don't flatten application nodes: this is used to extract a
@@ -1413,7 +1413,7 @@ let plain_instance sigma s c =
(try let g = Metamap.find p s in
match EConstr.kind sigma g with
| App _ ->
- let l' = CArray.Fun1.Smart.map lift 1 l' in
+ let l' = Array.Fun1.Smart.map lift 1 l' in
mkLetIn (Name default_plain_instance_ident,g,t,mkApp(mkRel 1, l'))
| _ -> mkApp (g,l')
with Not_found -> mkApp (f,l'))
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 14:53:26 +0000