aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--interp/notation_ops.ml10
-rw-r--r--kernel/pre_env.ml2
-rw-r--r--lib/cArray.ml22
-rw-r--r--lib/cArray.mli20
-rw-r--r--lib/cList.ml20
-rw-r--r--lib/cList.mli18
-rw-r--r--lib/option.ml11
-rw-r--r--lib/option.mli8
-rw-r--r--library/nameops.ml11
-rw-r--r--library/nameops.mli10
-rw-r--r--plugins/ltac/tacinterp.ml18
-rw-r--r--pretyping/cases.ml4
-rw-r--r--vernac/command.ml2
13 files changed, 119 insertions, 37 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 5d703011d..565a7e642 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -104,7 +104,7 @@ let rec cases_pattern_fold_map ?loc g e = CAst.with_val (function
let e',na' = g e na in e', CAst.make ?loc @@ PatVar na'
| PatCstr (cstr,patl,na) ->
let e',na' = g e na in
- let e',patl' = List.fold_map (cases_pattern_fold_map ?loc g) e patl in
+ let e',patl' = List.fold_left_map (cases_pattern_fold_map ?loc g) e patl in
e', CAst.make ?loc @@ PatCstr (cstr,patl',na')
)
@@ -169,21 +169,21 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
let fold (idl,e) na = let (e,na) = g e na in ((Name.cons na idl,e),na) in
let eqnl' = List.map (fun (patl,rhs) ->
let ((idl,e),patl) =
- List.fold_map (cases_pattern_fold_map ?loc fold) ([],e) patl in
+ List.fold_left_map (cases_pattern_fold_map ?loc fold) ([],e) patl in
Loc.tag (idl,patl,f e rhs)) eqnl in
GCases (sty,Option.map (f e') rtntypopt,tml',eqnl')
| NLetTuple (nal,(na,po),b,c) ->
- let e',nal = List.fold_map g e nal in
+ let e',nal = List.fold_left_map g e nal in
let e'',na = g e na in
GLetTuple (nal,(na,Option.map (f e'') po),f e b,f e' c)
| NIf (c,(na,po),b1,b2) ->
let e',na = g e na in
GIf (f e c,(na,Option.map (f e') po),f e b1,f e b2)
| NRec (fk,idl,dll,tl,bl) ->
- let e,dll = Array.fold_map (List.fold_map (fun e (na,oc,b) ->
+ let e,dll = Array.fold_left_map (List.fold_left_map (fun e (na,oc,b) ->
let e,na = g e na in
(e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
- let e',idl = Array.fold_map (to_id g) e idl in
+ let e',idl = Array.fold_left_map (to_id g) e idl in
GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
| NCast (c,k) -> GCast (f e c,Miscops.map_cast_type (f e) k)
| NSort x -> GSort x
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 7b4fb4e86..94738d618 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -156,7 +156,7 @@ let map_named_val f ctxt =
in
(accu, d')
in
- let map, ctx = List.fold_map fold ctxt.env_named_map ctxt.env_named_ctx in
+ let map, ctx = List.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in
if map == ctxt.env_named_map then ctxt
else { env_named_ctx = ctx; env_named_map = map }
diff --git a/lib/cArray.ml b/lib/cArray.ml
index 85984d436..d08f24d49 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -53,8 +53,12 @@ sig
('a -> 'b -> 'c -> 'd) -> 'a array -> 'b array -> 'c array -> 'd array
val map_left : ('a -> 'b) -> 'a array -> 'b array
val iter2 : ('a -> 'b -> unit) -> 'a array -> 'b array -> unit
- val fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
+ val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
+ val fold_right_map : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
+ val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b array -> 'c array -> 'a * 'd array
+ val fold_right2_map : ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
+ val fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
val fold_map2' :
('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
val distinct : 'a array -> bool
@@ -433,7 +437,7 @@ let iter2 f v1 v2 =
let pure_functional = false
-let fold_map' f v e =
+let fold_right_map f v e =
if pure_functional then
let (l,e) =
Array.fold_right
@@ -445,18 +449,28 @@ else
let v' = Array.map (fun x -> let (y,e) = f x !e' in e' := e; y) v in
(v',!e')
-let fold_map f e v =
+let fold_map' = fold_right_map
+
+let fold_left_map f e v =
let e' = ref e in
let v' = Array.map (fun x -> let (e,y) = f !e' x in e' := e; y) v in
(!e',v')
-let fold_map2' f v1 v2 e =
+let fold_map = fold_left_map
+
+let fold_right2_map f v1 v2 e =
let e' = ref e in
let v' =
map2 (fun x1 x2 -> let (y,e) = f x1 x2 !e' in e' := e; y) v1 v2
in
(v',!e')
+let fold_map2' = fold_right2_map
+
+let fold_left2_map f e v1 v2 =
+ let e' = ref e in
+ let v' = map2 (fun x1 x2 -> let (e,y) = f !e' x1 x2 in e' := e; y) v1 v2 in
+ (!e',v')
let distinct v =
let visited = Hashtbl.create 23 in
diff --git a/lib/cArray.mli b/lib/cArray.mli
index 7e5c93b5d..325ff8edc 100644
--- a/lib/cArray.mli
+++ b/lib/cArray.mli
@@ -96,10 +96,28 @@ sig
val iter2 : ('a -> 'b -> unit) -> 'a array -> 'b array -> unit
(** Iter on two arrays. Raise [Invalid_argument "Array.iter2"] if sizes differ. *)
- val fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
+ val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
+ (** [fold_left_map f e_0 [|l_1...l_n|] = e_n,[|k_1...k_n|]]
+ where [(e_i,k_i)=f e_{i-1} l_i] *)
+
+ val fold_right_map : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
+ (** Same, folding on the right *)
+
+ val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b array -> 'c array -> 'a * 'd array
+ (** Same with two arrays, folding on the left *)
+
+ val fold_right2_map : ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
+ (** Same with two arrays, folding on the left *)
+
val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
+ (** @deprecated Same as [fold_left_map] *)
+
+ val fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
+ (** @deprecated Same as [fold_right_map] *)
+
val fold_map2' :
('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
+ (** @deprecated Same as [fold_right2_map] *)
val distinct : 'a array -> bool
(** Return [true] if every element of the array is unique (for default
diff --git a/lib/cList.ml b/lib/cList.ml
index cb84b6097..ca69628af 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -92,6 +92,10 @@ sig
val map_append : ('a -> 'b list) -> 'a list -> 'b list
val map_append2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
+ val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
+ val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
+ val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b list -> 'c list -> 'a * 'd list
+ val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a
val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
@@ -761,13 +765,15 @@ let share_tails l1 l2 =
in
shr_rev [] (List.rev l1, List.rev l2)
-let rec fold_map f e = function
+let rec fold_left_map f e = function
| [] -> (e,[])
| h::t ->
let e',h' = f e h in
- let e'',t' = fold_map f e' t in
+ let e'',t' = fold_left_map f e' t in
e'',h'::t'
+let fold_map = fold_left_map
+
(* (* tail-recursive version of the above function *)
let fold_map f e l =
let g (e,b') h =
@@ -779,9 +785,17 @@ let fold_map f e l =
*)
(* The same, based on fold_right, with the effect accumulated on the right *)
-let fold_map' f l e =
+let fold_right_map f l e =
List.fold_right (fun x (l,e) -> let (y,e) = f x e in (y::l,e)) l ([],e)
+let fold_map' = fold_right_map
+
+let fold_left2_map f e l l' =
+ List.fold_left2 (fun (e,l) x x' -> let (e,y) = f e x x' in (e,y::l)) (e,[]) l l'
+
+let fold_right2_map f l l' e =
+ List.fold_right2 (fun x x' (l,e) -> let (y,e) = f x x' e in (y::l,e)) l l' ([],e)
+
let map_assoc f = List.map (fun (x,a) -> (x,f a))
let rec assoc_f f a = function
diff --git a/lib/cList.mli b/lib/cList.mli
index d7d6614cd..8cb07da79 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -198,11 +198,25 @@ sig
val share_tails : 'a list -> 'a list -> 'a list * 'a list * 'a list
- val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
- (** [fold_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]]
+ val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
+ (** [fold_left_map f e_0 [l_1...l_n] = e_n,[k_1...k_n]]
where [(e_i,k_i)=f e_{i-1} l_i] *)
+ val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
+ (** Same, folding on the right *)
+
+ val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b list -> 'c list -> 'a * 'd list
+ (** Same with two lists, folding on the left *)
+
+ val fold_right2_map : ('b -> 'c -> 'a -> 'd * 'a) -> 'b list -> 'c list -> 'a -> 'd list * 'a
+ (** Same with two lists, folding on the right *)
+
+ val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
+ (** @deprecated Same as [fold_left_map] *)
+
val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
+ (** @deprecated Same as [fold_right_map] *)
+
val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b
val remove_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> ('a * 'b) list
diff --git a/lib/option.ml b/lib/option.ml
index 7cedffef0..98b168035 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -121,12 +121,19 @@ let fold_right f x a =
| Some y -> f y a
| _ -> a
-(** [fold_map f a x] is [a, f y] if [x] is [Some y], and [a] otherwise. *)
-let fold_map f a x =
+(** [fold_left_map f a x] is [a, f y] if [x] is [Some y], and [a] otherwise. *)
+let fold_left_map f a x =
match x with
| Some y -> let a, z = f a y in a, Some z
| _ -> a, None
+let fold_right_map f x a =
+ match x with
+ | Some y -> let z, a = f y a in Some z, a
+ | _ -> None, a
+
+let fold_map = fold_left_map
+
(** [cata f a x] is [a] if [x] is [None] and [f y] if [x] is [Some y]. *)
let cata f a = function
| Some c -> f c
diff --git a/lib/option.mli b/lib/option.mli
index c4d1ebc3a..66f05023f 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -85,7 +85,13 @@ val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a
(** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *)
val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
-(** [fold_map f a x] is [a, f y] if [x] is [Some y], and [a] otherwise. *)
+(** [fold_left_map f a x] is [a, f y] if [x] is [Some y], and [a] otherwise. *)
+val fold_left_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b option -> 'a * 'c option
+
+(** Same as [fold_left_map] on the right *)
+val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b option -> 'a -> 'c option * 'a
+
+(** @deprecated Same as [fold_left_map] *)
val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b option -> 'a * 'c option
(** [cata f e x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *)
diff --git a/library/nameops.ml b/library/nameops.ml
index adfe6f5a5..d598a63b8 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -130,7 +130,8 @@ sig
val fold_right : (Id.t -> 'a -> 'a) -> t -> 'a -> 'a
val iter : (Id.t -> unit) -> t -> unit
val map : (Id.t -> Id.t) -> t -> t
- val fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> t -> 'a * t
+ val fold_left_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> t -> 'a * t
+ val fold_right_map : (Id.t -> 'a -> Id.t * 'a) -> Name.t -> 'a -> Name.t * 'a
val get_id : t -> Id.t
val pick : t -> t -> t
val cons : t -> Id.t list -> Id.t list
@@ -160,10 +161,14 @@ struct
| Name id -> Name (f id)
| Anonymous -> Anonymous
- let fold_map f a = function
+ let fold_left_map f a = function
| Name id -> let (a, id) = f a id in (a, Name id)
| Anonymous -> a, Anonymous
+ let fold_right_map f na a = match na with
+ | Name id -> let (id, a) = f id a in (Name id, a)
+ | Anonymous -> Anonymous, a
+
let get_id = function
| Name id -> id
| Anonymous -> raise IsAnonymous
@@ -191,7 +196,7 @@ let out_name = get_id
let name_fold = fold_right
let name_iter = iter
let name_app = map
-let name_fold_map = fold_map
+let name_fold_map = fold_left_map
let name_cons = cons
let name_max = pick
let pr_name = print
diff --git a/library/nameops.mli b/library/nameops.mli
index 89aba2447..58cd6ed4e 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -66,10 +66,14 @@ module Name : sig
val map : (Id.t -> Id.t) -> Name.t -> t
(** [map f na] is [Anonymous] if [na] is [Anonymous] and [Name (f id)] if [na] is [Name id]. *)
- val fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
- (** [fold_map f na a] is [a',Name id'] when [na] is [Name id] and [f a id] is [(a',id')].
+ val fold_left_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
+ (** [fold_left_map f a na] is [a',Name id'] when [na] is [Name id] and [f a id] is [(a',id')].
It is [a,Anonymous] otherwise. *)
+ val fold_right_map : (Id.t -> 'a -> Id.t * 'a) -> Name.t -> 'a -> Name.t * 'a
+ (** [fold_right_map f na a] is [Name id',a'] when [na] is [Name id] and [f id a] is [(id',a')].
+ It is [Anonymous,a] otherwise. *)
+
val get_id : Name.t -> Id.t
(** [get_id] associates [id] to [Name id]. @raise IsAnonymous otherwise. *)
@@ -98,7 +102,7 @@ val name_app : (Id.t -> Id.t) -> Name.t -> Name.t
(** @deprecated Same as [Name.map] *)
val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
-(** @deprecated Same as [Name.fold_map] *)
+(** @deprecated Same as [Name.fold_left_map] *)
val name_max : Name.t -> Name.t -> Name.t
(** @deprecated Same as [Name.pick] *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 51eed2f4e..2a1e2b682 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -689,7 +689,7 @@ let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
(* dest_fun, List.assoc may raise Not_found *)
let sigma, c = interp_fun ist env sigma x in
sigma, [c] in
- let sigma, l = List.fold_map try_expand_ltac_var sigma l in
+ let sigma, l = List.fold_left_map try_expand_ltac_var sigma l in
sigma, List.flatten l
let interp_constr_list ist env sigma c =
@@ -908,18 +908,18 @@ and interp_intro_pattern_action ist env sigma = function
and interp_or_and_intro_pattern ist env sigma = function
| IntroAndPattern l ->
- let sigma, l = List.fold_map (interp_intro_pattern ist env) sigma l in
+ let sigma, l = List.fold_left_map (interp_intro_pattern ist env) sigma l in
sigma, IntroAndPattern l
| IntroOrPattern ll ->
- let sigma, ll = List.fold_map (interp_intro_pattern_list_as_list ist env) sigma ll in
+ let sigma, ll = List.fold_left_map (interp_intro_pattern_list_as_list ist env) sigma ll in
sigma, IntroOrPattern ll
and interp_intro_pattern_list_as_list ist env sigma = function
| [loc,IntroNaming (IntroIdentifier id)] as l ->
(try sigma, coerce_to_intro_pattern_list ?loc env sigma (Id.Map.find id ist.lfun)
with Not_found | CannotCoerceTo _ ->
- List.fold_map (interp_intro_pattern ist env) sigma l)
- | l -> List.fold_map (interp_intro_pattern ist env) sigma l
+ List.fold_left_map (interp_intro_pattern ist env) sigma l)
+ | l -> List.fold_left_map (interp_intro_pattern ist env) sigma l
let interp_intro_pattern_naming_option ist env sigma = function
| None -> None
@@ -973,7 +973,7 @@ let interp_bindings ist env sigma = function
let sigma, l = interp_open_constr_list ist env sigma l in
sigma, ImplicitBindings l
| ExplicitBindings l ->
- let sigma, l = List.fold_map (interp_binding ist env) sigma l in
+ let sigma, l = List.fold_left_map (interp_binding ist env) sigma l in
sigma, ExplicitBindings l
let interp_constr_with_bindings ist env sigma (c,bl) =
@@ -1671,7 +1671,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let env = Proofview.Goal.env gl in
let sigma = project gl in
let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in
- let sigma, cbo = Option.fold_map (interp_open_constr_with_bindings ist env) sigma cbo in
+ let sigma, cbo = Option.fold_left_map (interp_open_constr_with_bindings ist env) sigma cbo in
let named_tac =
let tac = Tactics.elim ev keep cb cbo in
name_atomic ~env (TacElim (ev,(keep,cb),cbo)) tac
@@ -1789,7 +1789,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let env = Proofview.Goal.env gl in
let sigma = project gl in
let sigma,l =
- List.fold_map begin fun sigma (c,(ipato,ipats),cls) ->
+ List.fold_left_map begin fun sigma (c,(ipato,ipats),cls) ->
(* TODO: move sigma as a side-effect *)
(* spiwack: the [*p] variants are for printing *)
let cp = c in
@@ -1803,7 +1803,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
in
let l,lp = List.split l in
let sigma,el =
- Option.fold_map (interp_open_constr_with_bindings ist env) sigma el in
+ Option.fold_left_map (interp_open_constr_with_bindings ist env) sigma el in
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(name_atomic ~env
(TacInductionDestruct(isrec,ev,(lp,el)))
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1a879f911..63775d737 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1753,14 +1753,14 @@ let build_inversion_problem loc env sigma tms t =
let cstr,u = destConstruct sigma f in
let n = constructor_nrealargs_env env cstr in
let l = List.lastn n (Array.to_list v) in
- let l,acc = List.fold_map' reveal_pattern l acc in
+ let l,acc = List.fold_right_map reveal_pattern l acc in
CAst.make (PatCstr (cstr,l,Anonymous)), acc
| _ -> make_patvar t acc in
let rec aux n env acc_sign tms acc =
match tms with
| [] -> [], acc_sign, acc
| (t, IsInd (_,IndType(indf,realargs),_)) :: tms ->
- let patl,acc = List.fold_map' reveal_pattern realargs acc in
+ let patl,acc = List.fold_right_map reveal_pattern realargs acc in
let pat,acc = make_patvar t acc in
let indf' = lift_inductive_family n indf in
let sign = make_arity_signature env sigma true indf' in
diff --git a/vernac/command.ml b/vernac/command.ml
index a315ac14e..0d6fd24cd 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -241,7 +241,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
else l
in
(* We intepret all declarations in the same evar_map, i.e. as a telescope. *)
- let _,l = List.fold_map (fun (env,ienv) (is_coe,(idl,c)) ->
+ let _,l = List.fold_left_map (fun (env,ienv) (is_coe,(idl,c)) ->
let t,imps = interp_assumption evdref env ienv [] c in
let env =
push_named_context (List.map (fun (_,id) -> LocalAssum (id,t)) idl) env in