Collecting Array.smart_* functions into a module Array.Smart.

6 files changed, 63 insertions, 63 deletions

diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 641d424e2..0727eaeac 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -152,7 +152,7 @@ let rec map_lam_with_binders g f n lam =
   match lam with
   | Lrel _ | Lvar _  | Lconst _ | Lval _ | Lsort _ | Lind _ -> lam
   | Levar (evk, args) ->
-    let args' = Array.smartmap (f n) args in
+    let args' = Array.Smart.map (f n) args in
     if args == args' then lam else Levar (evk, args')
   | Lprod(dom,codom) ->
     let dom' = f n dom in
@@ -167,19 +167,19 @@ let rec map_lam_with_binders g f n lam =
     if body == body' && def == def' then lam else Llet(id,def',body')
   | Lapp(fct,args) ->
     let fct' = f n fct in
-    let args' = Array.smartmap (f n) args in
+    let args' = Array.Smart.map (f n) args in
     if fct == fct' && args == args' then lam else mkLapp fct' args'
   | Lcase(ci,rtbl,t,a,branches) ->
     let const = branches.constant_branches in
     let nonconst = branches.nonconstant_branches in
     let t' = f n t in
     let a' = f n a in
-    let const' = Array.smartmap (f n) const in
+    let const' = Array.Smart.map (f n) const in
     let on_b b =
       let (ids,body) = b in
       let body' = f (g (Array.length ids) n) body in
       if body == body' then b else (ids,body') in
-    let nonconst' = Array.smartmap on_b nonconst in
+    let nonconst' = Array.Smart.map on_b nonconst in
     let branches' =
       if const == const' && nonconst == nonconst' then
         branches
@@ -190,20 +190,20 @@ let rec map_lam_with_binders g f n lam =
     if t == t' && a == a' && branches == branches' then lam else
       Lcase(ci,rtbl,t',a',branches')
   | Lfix(init,(ids,ltypes,lbodies)) ->
-    let ltypes' = Array.smartmap (f n) ltypes in
-    let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in
+    let ltypes' = Array.Smart.map (f n) ltypes in
+    let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in
     if ltypes == ltypes' && lbodies == lbodies' then lam
     else Lfix(init,(ids,ltypes',lbodies'))
   | Lcofix(init,(ids,ltypes,lbodies)) ->
-    let ltypes' = Array.smartmap (f n) ltypes in
-    let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in
+    let ltypes' = Array.Smart.map (f n) ltypes in
+    let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in
     if ltypes == ltypes' && lbodies == lbodies' then lam
     else Lcofix(init,(ids,ltypes',lbodies'))
   | Lmakeblock(tag,args) ->
-    let args' = Array.smartmap (f n) args in
+    let args' = Array.Smart.map (f n) args in
     if args == args' then lam else Lmakeblock(tag,args')
   | Lprim(kn,ar,op,args) ->
-    let args' = Array.smartmap (f n) args in
+    let args' = Array.Smart.map (f n) args in
     if args == args' then lam else Lprim(kn,ar,op,args')
   | Lproj(i,kn,arg) ->
     let arg' = f n arg in
@@ -216,7 +216,7 @@ and map_uint g f n u =
   match u with
   | UintVal _ -> u
   | UintDigits(args) ->
-    let args' = Array.smartmap (f n) args in
+    let args' = Array.Smart.map (f n) args in
     if args == args' then u else UintDigits(args')
   | UintDecomp(a) ->
     let a' = f n a in
@@ -250,7 +250,7 @@ let rec lam_exsubst subst lam =
 
 let lam_subst_args subst args =
   if is_subs_id subst then args
-  else Array.smartmap (lam_exsubst subst) args
+  else Array.Smart.map (lam_exsubst subst) args
 
 (** Simplification of lambda expression *)
 
@@ -316,7 +316,7 @@ and simplify_app substf f substa args =
     simplify_app substf f subst_id args
   | _ -> mkLapp (simplify substf f) (simplify_args substa args)
 
-and simplify_args subst args = Array.smartmap (simplify subst) args
+and simplify_args subst args = Array.Smart.map (simplify subst) args
 
 and reduce_lapp substf lids body substa largs =
   match lids, largs with
diff --git a/kernel/constr.ml b/kernel/constr.ml
index bc486210d..a1779b36d 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -509,7 +509,7 @@ let map f c = match kind c with
       else mkLetIn (na, b', t', k')
   | App (b,l) ->
       let b' = f b in
-      let l' = Array.smartmap f l in
+      let l' = Array.Smart.map f l in
       if b'==b && l'==l then c
       else mkApp (b', l')
   | Proj (p,t) ->
@@ -517,23 +517,23 @@ let map f c = match kind c with
       if t' == t then c
       else mkProj (p, t')
   | Evar (e,l) ->
-      let l' = Array.smartmap f l in
+      let l' = Array.Smart.map f l in
       if l'==l then c
       else mkEvar (e, l')
   | Case (ci,p,b,bl) ->
       let b' = f b in
       let p' = f p in
-      let bl' = Array.smartmap f bl in
+      let bl' = Array.Smart.map f bl in
       if b'==b && p'==p && bl'==bl then c
       else mkCase (ci, p', b', bl')
   | Fix (ln,(lna,tl,bl)) ->
-      let tl' = Array.smartmap f tl in
-      let bl' = Array.smartmap f bl in
+      let tl' = Array.Smart.map f tl in
+      let bl' = Array.Smart.map f bl in
       if tl'==tl && bl'==bl then c
       else mkFix (ln,(lna,tl',bl'))
   | CoFix(ln,(lna,tl,bl)) ->
-      let tl' = Array.smartmap f tl in
-      let bl' = Array.smartmap f bl in
+      let tl' = Array.Smart.map f tl in
+      let bl' = Array.Smart.map f bl in
       if tl'==tl && bl'==bl then c
       else mkCoFix (ln,(lna,tl',bl'))
 
@@ -565,7 +565,7 @@ let fold_map f accu c = match kind c with
       else accu, mkLetIn (na, b', t', k')
   | App (b,l) ->
       let accu, b' = f accu b in
-      let accu, l' = Array.smartfoldmap f accu l in
+      let accu, l' = Array.Smart.fold_left_map f accu l in
       if b'==b && l'==l then accu, c
       else accu, mkApp (b', l')
   | Proj (p,t) ->
@@ -573,23 +573,23 @@ let fold_map f accu c = match kind c with
       if t' == t then accu, c
       else accu, mkProj (p, t')
   | Evar (e,l) ->
-      let accu, l' = Array.smartfoldmap f accu l in
+      let accu, l' = Array.Smart.fold_left_map f accu l in
       if l'==l then accu, c
       else accu, mkEvar (e, l')
   | Case (ci,p,b,bl) ->
       let accu, b' = f accu b in
       let accu, p' = f accu p in
-      let accu, bl' = Array.smartfoldmap f accu bl in
+      let accu, bl' = Array.Smart.fold_left_map f accu bl in
       if b'==b && p'==p && bl'==bl then accu, c
       else accu, mkCase (ci, p', b', bl')
   | Fix (ln,(lna,tl,bl)) ->
-      let accu, tl' = Array.smartfoldmap f accu tl in
-      let accu, bl' = Array.smartfoldmap f accu bl in
+      let accu, tl' = Array.Smart.fold_left_map f accu tl in
+      let accu, bl' = Array.Smart.fold_left_map f accu bl in
       if tl'==tl && bl'==bl then accu, c
       else accu, mkFix (ln,(lna,tl',bl'))
   | CoFix(ln,(lna,tl,bl)) ->
-      let accu, tl' = Array.smartfoldmap f accu tl in
-      let accu, bl' = Array.smartfoldmap f accu bl in
+      let accu, tl' = Array.Smart.fold_left_map f accu tl in
+      let accu, bl' = Array.Smart.fold_left_map f accu bl in
       if tl'==tl && bl'==bl then accu, c
       else accu, mkCoFix (ln,(lna,tl',bl'))
 
@@ -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.smartmap f l al in
+    let al' = CArray.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.smartmap f l al in
+    let al' = CArray.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.smartmap f l bl in
+    let bl' = CArray.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.smartmap f l tl in
+    let tl' = CArray.Fun1.Smart.map f l tl in
     let l' = iterate g (Array.length tl) l in
-    let bl' = CArray.Fun1.smartmap f l' bl in
+    let bl' = CArray.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.smartmap f l tl in
+    let tl' = CArray.Fun1.Smart.map f l tl in
     let l' = iterate g (Array.length tl) l in
-    let bl' = CArray.Fun1.smartmap f l' bl in
+    let bl' = CArray.Fun1.Smart.map f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
 
 type instance_compare_fn = GlobRef.t -> int ->
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 3652a1ce4..90a6eb6f7 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -198,10 +198,10 @@ let subst_mind_packet sub mbp =
     mind_consnrealdecls = mbp.mind_consnrealdecls;
     mind_consnrealargs = mbp.mind_consnrealargs;
     mind_typename = mbp.mind_typename;
-    mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc;
+    mind_nf_lc = Array.Smart.map (subst_mps sub) mbp.mind_nf_lc;
     mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
     mind_arity = subst_ind_arity sub mbp.mind_arity;
-    mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc;
+    mind_user_lc = Array.Smart.map (subst_mps sub) mbp.mind_user_lc;
     mind_nrealargs = mbp.mind_nrealargs;
     mind_nrealdecls = mbp.mind_nrealdecls;
     mind_kelim = mbp.mind_kelim;
@@ -211,8 +211,8 @@ let subst_mind_packet sub mbp =
     mind_reloc_tbl = mbp.mind_reloc_tbl }
 
 let subst_mind_record sub (id, ps, pb as r) =
-  let ps' = Array.smartmap (subst_constant sub) ps in
-  let pb' = Array.smartmap (subst_const_proj sub) pb in
+  let ps' = Array.Smart.map (subst_constant sub) ps in
+  let pb' = Array.Smart.map (subst_const_proj sub) pb in
     if ps' == ps && pb' == pb then r
     else (id, ps', pb')
 
@@ -225,7 +225,7 @@ let subst_mind_body sub mib =
     mind_nparams_rec = mib.mind_nparams_rec;
     mind_params_ctxt =
       Context.Rel.map (subst_mps sub) mib.mind_params_ctxt;
-    mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
+    mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ;
     mind_universes = mib.mind_universes;
     mind_private = mib.mind_private;
     mind_typing_flags = mib.mind_typing_flags;
@@ -263,15 +263,15 @@ let hcons_ind_arity =
 (** Substitution of inductive declarations *)
 
 let hcons_mind_packet oib =
-  let user = Array.smartmap Constr.hcons oib.mind_user_lc in
-  let nf = Array.smartmap Constr.hcons oib.mind_nf_lc in
+  let user = Array.Smart.map Constr.hcons oib.mind_user_lc in
+  let nf = Array.Smart.map Constr.hcons oib.mind_nf_lc in
   (* Special optim : merge [mind_user_lc] and [mind_nf_lc] if possible *)
   let nf = if Array.equal (==) user nf then user else nf in
   { oib with
     mind_typename = Names.Id.hcons oib.mind_typename;
     mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt;
     mind_arity = hcons_ind_arity oib.mind_arity;
-    mind_consnames = Array.smartmap Names.Id.hcons oib.mind_consnames;
+    mind_consnames = Array.Smart.map Names.Id.hcons oib.mind_consnames;
     mind_user_lc = user;
     mind_nf_lc = nf }
 
@@ -283,7 +283,7 @@ let hcons_mind_universes miu =
 
 let hcons_mind mib =
   { mib with
-    mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets;
+    mind_packets = Array.Smart.map hcons_mind_packet mib.mind_packets;
     mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
     mind_universes = hcons_mind_universes mib.mind_universes }
 
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 9c2fa0546..0027ebecf 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -367,7 +367,7 @@ let rec map_kn f f' c =
 	  in
 	  let p' = func p in
 	  let ct' = func ct in
-	  let l' = Array.smartmap func l in
+          let l' = Array.Smart.map func l in
 	    if (ci.ci_ind==ci_ind && p'==p
 		&& l'==l && ct'==ct)then c
 	    else
@@ -396,21 +396,21 @@ let rec map_kn f f' c =
 	    else mkLetIn (na, b', t', ct')
       | App (ct,l) ->
 	  let ct' = func ct in
-	  let l' = Array.smartmap func l in
+          let l' = Array.Smart.map func l in
 	    if (ct'== ct && l'==l) then c
 	    else mkApp (ct',l')
       | Evar (e,l) ->
-	  let l' = Array.smartmap func l in
+          let l' = Array.Smart.map func l in
 	    if (l'==l) then c
 	    else mkEvar (e,l')
       | Fix (ln,(lna,tl,bl)) ->
-	  let tl' = Array.smartmap func tl in
-	  let bl' = Array.smartmap func bl in
+          let tl' = Array.Smart.map func tl in
+          let bl' = Array.Smart.map func bl in
 	    if (bl == bl'&& tl == tl') then c
 	    else mkFix (ln,(lna,tl',bl'))
       | CoFix(ln,(lna,tl,bl)) ->
-	  let tl' = Array.smartmap func tl in
-	  let bl' = Array.smartmap func bl in
+          let tl' = Array.Smart.map func tl in
+          let bl' = Array.Smart.map func bl in
 	    if (bl == bl'&& tl == tl') then c
 	    else mkCoFix (ln,(lna,tl',bl'))
       | _ -> c
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 01ddffe3e..12cd5fe83 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -102,10 +102,10 @@ let rec map_lam_with_binders g f n lam =
       if body == body' && def == def' then lam else Llet(id,def',body')
   | Lapp(fct,args) ->
       let fct' = f n fct in
-      let args' = Array.smartmap (f n) args in
+      let args' = Array.Smart.map (f n) args in
       if fct == fct' && args == args' then lam else mkLapp fct' args'
   | Lprim(prefix,kn,op,args) ->
-      let args' = Array.smartmap (f n) args in
+      let args' = Array.Smart.map (f n) args in
       if args == args' then lam else Lprim(prefix,kn,op,args')
   | Lcase(annot,t,a,br) ->
       let t' = f n t in
@@ -116,7 +116,7 @@ let rec map_lam_with_binders g f n lam =
 	  if Array.is_empty ids then f n body 
 	  else f (g (Array.length ids) n) body in
 	if body == body' then b else (cn,ids,body') in
-      let br' = Array.smartmap on_b br in
+      let br' = Array.Smart.map on_b br in
       if t == t' && a == a' && br == br' then lam else Lcase(annot,t',a',br')
   | Lif(t,bt,bf) ->
       let t' = f n t in
@@ -124,17 +124,17 @@ let rec map_lam_with_binders g f n lam =
       let bf' = f n bf in
       if t == t' && bt == bt' && bf == bf' then lam else Lif(t',bt',bf')
   | Lfix(init,(ids,ltypes,lbodies)) ->
-      let ltypes' = Array.smartmap (f n) ltypes in
-      let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in
+      let ltypes' = Array.Smart.map (f n) ltypes in
+      let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in
       if ltypes == ltypes' && lbodies == lbodies' then lam
       else Lfix(init,(ids,ltypes',lbodies'))
   | Lcofix(init,(ids,ltypes,lbodies)) ->
-      let ltypes' = Array.smartmap (f n) ltypes in
-      let lbodies' = Array.smartmap (f (g (Array.length ids) n)) lbodies in
+      let ltypes' = Array.Smart.map (f n) ltypes in
+      let lbodies' = Array.Smart.map (f (g (Array.length ids) n)) lbodies in
       if ltypes == ltypes' && lbodies == lbodies' then lam
       else Lcofix(init,(ids,ltypes',lbodies'))
   | Lmakeblock(prefix,cn,tag,args) ->
-      let args' = Array.smartmap (f n) args in
+      let args' = Array.Smart.map (f n) args in
       if args == args' then lam else Lmakeblock(prefix,cn,tag,args')
   | Luint u ->
     let u' = map_uint g f n u in
@@ -144,7 +144,7 @@ and map_uint g f n u =
   match u with
   | UintVal _ -> u
   | UintDigits(prefix,c,args) ->
-    let args' = Array.smartmap (f n) args in
+    let args' = Array.Smart.map (f n) args in
     if args == args' then u else UintDigits(prefix,c,args')
   | UintDecomp(prefix,c,a) ->
     let a' = f n a in
@@ -177,7 +177,7 @@ let rec lam_exsubst subst lam =
 
 let lam_subst_args subst args =
   if is_subs_id subst then args 
-  else Array.smartmap (lam_exsubst subst) args
+  else Array.Smart.map (lam_exsubst subst) args
   
 (** Simplification of lambda expression *)
       
@@ -272,7 +272,7 @@ and simplify_app substf f substa args =
   (* TODO | Lproj -> simplify if the argument is known or a known global *)
   | _ -> mkLapp (simplify substf f) (simplify_args substa args)
   
-and simplify_args subst args = Array.smartmap (simplify subst) args
+and simplify_args subst args = Array.Smart.map (simplify subst) args
 
 and reduce_lapp substf lids body substa largs =
   match lids, largs with
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8e19fa4e5..6bcffdd45 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -853,7 +853,7 @@ struct
   let length a = Array.length a
 
   let subst_fn fn t = 
-    let t' = CArray.smartmap fn t in
+    let t' = CArray.Smart.map fn t in
       if t' == t then t else of_array t'
 
   let levels x = LSet.of_array x
@@ -890,7 +890,7 @@ let subst_instance_level s l =
   | _ -> l
 
 let subst_instance_instance s i = 
-  Array.smartmap (fun l -> subst_instance_level s l) i
+  Array.Smart.map (fun l -> subst_instance_level s l) i
 
 let subst_instance_universe s u =
   let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in