From 33b5074f24270c202a9922f21d445c12cc6b3b3d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 23 May 2018 13:34:46 +0200 Subject: Collecting List.smart_* functions into a module List.Smart. --- pretyping/detyping.ml | 12 ++++++------ pretyping/glob_ops.ml | 10 +++++----- pretyping/patternops.ml | 4 ++-- pretyping/pretyping.ml | 2 +- pretyping/recordops.ml | 2 +- pretyping/typeclasses.ml | 10 +++++----- 6 files changed, 20 insertions(+), 20 deletions(-) (limited to 'pretyping') diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index ea2889dea..e306fd6b3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -920,7 +920,7 @@ let rec subst_cases_pattern subst = DAst.map (function | PatVar _ as pat -> pat | PatCstr (((kn,i),j),cpl,n) as pat -> let kn' = subst_mind subst kn - and cpl' = List.smartmap (subst_cases_pattern subst) cpl in + and cpl' = List.Smart.map (subst_cases_pattern subst) cpl in if kn' == kn && cpl' == cpl then pat else PatCstr (((kn',i),j),cpl',n) ) @@ -940,7 +940,7 @@ let rec subst_glob_constr subst = DAst.map (function | GApp (r,rl) as raw -> let r' = subst_glob_constr subst r - and rl' = List.smartmap (subst_glob_constr subst) rl in + and rl' = List.Smart.map (subst_glob_constr subst) rl in if r' == r && rl' == rl then raw else GApp(r',rl') @@ -964,7 +964,7 @@ let rec subst_glob_constr subst = DAst.map (function | GCases (sty,rtno,rl,branches) as raw -> let open CAst in let rtno' = Option.smartmap (subst_glob_constr subst) rtno - and rl' = List.smartmap (fun (a,x as y) -> + and rl' = List.Smart.map (fun (a,x as y) -> let a' = subst_glob_constr subst a in let (n,topt) = x in let topt' = Option.smartmap @@ -972,10 +972,10 @@ let rec subst_glob_constr subst = DAst.map (function let sp' = subst_mind subst sp in if sp == sp' then t else CAst.(make ?loc ((sp',i),y))) topt in if a == a' && topt == topt' then y else (a',(n,topt'))) rl - and branches' = List.smartmap + and branches' = List.Smart.map (fun ({loc;v=(idl,cpl,r)} as branch) -> let cpl' = - List.smartmap (subst_cases_pattern subst) cpl + List.Smart.map (subst_cases_pattern subst) cpl and r' = subst_glob_constr subst r in if cpl' == cpl && r' == r then branch else CAst.(make ?loc (idl,cpl',r'))) @@ -1003,7 +1003,7 @@ let rec subst_glob_constr subst = DAst.map (function let ra1' = Array.Smart.map (subst_glob_constr subst) ra1 and ra2' = Array.Smart.map (subst_glob_constr subst) ra2 in let bl' = Array.Smart.map - (List.smartmap (fun (na,k,obd,ty as dcl) -> + (List.Smart.map (fun (na,k,obd,ty as dcl) -> let ty' = subst_glob_constr subst ty in let obd' = Option.smartmap (subst_glob_constr subst) obd in if ty'==ty && obd'==obd then dcl else (na,k,obd',ty'))) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 95f02dceb..102e89400 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -338,7 +338,7 @@ let bound_glob_vars = pattern-matching expressions are usually rather small. *) let map_inpattern_binders f ({loc;v=(id,nal)} as x) = - let r = CList.smartmap f nal in + let r = CList.Smart.map f nal in if r == nal then x else CAst.make ?loc (id,r) @@ -355,7 +355,7 @@ let rec map_case_pattern_binders f = DAst.map (function | PatCstr (c,ps,na) as x -> let rna = f na in let rps = - CList.smartmap (fun p -> map_case_pattern_binders f p) ps + CList.Smart.map (fun p -> map_case_pattern_binders f p) ps in if rna == na && rps == ps then x else PatCstr(c,rps,rna) @@ -366,13 +366,13 @@ let map_cases_branch_binders f ({CAst.loc;v=(il,cll,rhs)} as x) : cases_clause = It is intended to be a superset of the free variable of the right-hand side, if I understand correctly. But I'm not sure when or how they are used. *) - let r = List.smartmap (fun cl -> map_case_pattern_binders f cl) cll in + let r = List.Smart.map (fun cl -> map_case_pattern_binders f cl) cll in if r == cll then x else CAst.make ?loc (il,r,rhs) let map_pattern_binders f tomatch branches = - CList.smartmap (fun tm -> map_tomatch_binders f tm) tomatch, - CList.smartmap (fun br -> map_cases_branch_binders f br) branches + CList.Smart.map (fun tm -> map_tomatch_binders f tm) tomatch, + CList.Smart.map (fun br -> map_cases_branch_binders f br) branches (** /mapping of names in binders *) diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index bc7ed6137..b425dc0e2 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -297,7 +297,7 @@ let rec subst_pattern subst pat = if f' == f && args' == args then pat else PApp (f',args') | PSoApp (i,args) -> - let args' = List.smartmap (subst_pattern subst) args in + let args' = List.Smart.map (subst_pattern subst) args in if args' == args then pat else PSoApp (i,args') | PLambda (name,c1,c2) -> @@ -334,7 +334,7 @@ let rec subst_pattern subst pat = let c' = subst_pattern subst c in if c' == c then br else (i,n,c') in - let branches' = List.smartmap subst_branch branches in + let branches' = List.Smart.map subst_branch branches in if cip' == cip && typ' == typ && c' == c && branches' == branches then pat else PCase(cip', typ', c', branches') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 6bf852fcd..de72f9427 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -421,7 +421,7 @@ let ltac_interp_name_env k0 lvar env sigma = let n = Context.Rel.length (rel_context env) - k0 in let ctxt,_ = List.chop n (rel_context env) in let open Context.Rel.Declaration in - let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in + let ctxt' = List.Smart.map (map_name (ltac_interp_name lvar)) ctxt in if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env else push_rel_context sigma ctxt' (pop_rel_context n env sigma) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 84aceeedd..334bfc895 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -69,7 +69,7 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) = let projs' = (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) - List.smartmap + List.Smart.map (Option.smartmap (fun kn -> fst (subst_con_kn subst kn))) projs in diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 11cc6c1f0..5ad9dc691 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -180,11 +180,11 @@ let subst_class (subst,cl) = let do_subst_con c = Mod_subst.subst_constant subst c and do_subst c = Mod_subst.subst_mps subst c and do_subst_gr gr = fst (subst_global subst gr) in - let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in + let do_subst_ctx = List.Smart.map (RelDecl.map_constr do_subst) in let do_subst_context (grs,ctx) = - List.smartmap (Option.smartmap do_subst_gr) grs, + List.Smart.map (Option.smartmap do_subst_gr) grs, do_subst_ctx ctx in - let do_subst_projs projs = List.smartmap (fun (x, y, z) -> + let do_subst_projs projs = List.Smart.map (fun (x, y, z) -> (x, y, Option.smartmap do_subst_con z)) projs in { cl_univs = cl.cl_univs; cl_impl = do_subst_gr cl.cl_impl; @@ -223,7 +223,7 @@ let discharge_class (_,cl) = | Some (_, ((tc,_), _)) -> Some tc.cl_impl) ctx' in - List.smartmap (Option.smartmap Lib.discharge_global) grs + List.Smart.map (Option.smartmap Lib.discharge_global) grs @ newgrs in grs', discharge_rel_context subst 1 ctx @ ctx' in let cl_impl' = Lib.discharge_global cl.cl_impl in @@ -239,7 +239,7 @@ let discharge_class (_,cl) = cl_impl = cl_impl'; cl_context = context; cl_props = props; - cl_projs = List.smartmap discharge_proj cl.cl_projs; + cl_projs = List.Smart.map discharge_proj cl.cl_projs; cl_strict = cl.cl_strict; cl_unique = cl.cl_unique } -- cgit v1.2.3