From f2ab2825077bf8344d2e55be433efb1891212589 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 23 May 2018 13:34:22 +0200 Subject: Collecting Array.smart_* functions into a module Array.Smart. --- kernel/clambda.ml | 26 +++++++++++++------------- kernel/constr.ml | 42 +++++++++++++++++++++--------------------- kernel/declareops.ml | 18 +++++++++--------- kernel/mod_subst.ml | 14 +++++++------- kernel/nativelambda.ml | 22 +++++++++++----------- kernel/univ.ml | 4 ++-- 6 files changed, 63 insertions(+), 63 deletions(-) (limited to 'kernel') 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 -- cgit v1.2.3