From 944f62d08b7d78bcb20dd12ba138891d432b5987 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 13 May 2018 15:21:10 +0200 Subject: Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works. --- clib/cArray.ml | 12 ++++++++++++ clib/cArray.mli | 42 +++++++++++++++++++++--------------------- engine/eConstr.ml | 20 ++++++++++---------- engine/termops.ml | 2 +- kernel/cClosure.ml | 32 ++++++++++++++++---------------- kernel/constr.ml | 28 ++++++++++++++-------------- kernel/esubst.ml | 2 +- kernel/reduction.ml | 2 +- pretyping/reductionops.ml | 4 ++-- 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')) -- cgit v1.2.3