aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/cArray.ml26
-rw-r--r--lib/cArray.mli20
-rw-r--r--lib/cList.ml20
-rw-r--r--lib/cList.mli18
-rw-r--r--lib/clib.mllib1
-rw-r--r--lib/dAst.ml41
-rw-r--r--lib/dAst.mli28
-rw-r--r--lib/loc.ml13
-rw-r--r--lib/loc.mli8
-rw-r--r--lib/option.ml11
-rw-r--r--lib/option.mli8
11 files changed, 175 insertions, 19 deletions
diff --git a/lib/cArray.ml b/lib/cArray.ml
index 85984d4362..013585735c 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
@@ -330,7 +334,7 @@ let smartmap f (ar : 'a array) =
Array.unsafe_set ans !i v;
incr i;
while !i < len do
- let v = Array.unsafe_get ar !i in
+ let v = Array.unsafe_get ans !i in
let v' = f v in
if v != v' then Array.unsafe_set ans !i v';
incr i
@@ -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
@@ -513,7 +527,7 @@ struct
Array.unsafe_set ans !i v;
incr i;
while !i < len do
- let v = Array.unsafe_get ar !i in
+ let v = Array.unsafe_get ans !i in
let v' = f arg v in
if v != v' then Array.unsafe_set ans !i v';
incr i
diff --git a/lib/cArray.mli b/lib/cArray.mli
index 7e5c93b5da..325ff8edcc 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 cb84b6097f..ca69628af7 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 d7d6614cd3..8cb07da79c 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/clib.mllib b/lib/clib.mllib
index d5c938fe54..5c1f7d9af8 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -19,6 +19,7 @@ Flags
Control
Loc
CAst
+DAst
CList
CString
Deque
diff --git a/lib/dAst.ml b/lib/dAst.ml
new file mode 100644
index 0000000000..0fe323d013
--- /dev/null
+++ b/lib/dAst.ml
@@ -0,0 +1,41 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open CAst
+
+type ('a, _) thunk =
+| Value : 'a -> ('a, 'b) thunk
+| Thunk : 'a Lazy.t -> ('a, [ `thunk ]) thunk
+
+type ('a, 'b) t = ('a, 'b) thunk CAst.t
+
+let map_thunk (type s) f : (_, s) thunk -> (_, s) thunk = function
+| Value x -> Value (f x)
+| Thunk k -> Thunk (lazy (f (Lazy.force k)))
+
+let get_thunk (type s) : ('a, s) thunk -> 'a = function
+| Value x -> x
+| Thunk k -> Lazy.force k
+
+let get x = get_thunk x.v
+
+let make ?loc v = CAst.make ?loc (Value v)
+
+let delay ?loc v = CAst.make ?loc (Thunk (Lazy.from_fun v))
+
+let map f n = CAst.map (fun x -> map_thunk f x) n
+
+let map_with_loc f n =
+ CAst.map_with_loc (fun ?loc x -> map_thunk (fun x -> f ?loc x) x) n
+
+let map_from_loc f (loc, x) =
+ make ?loc (f ?loc x)
+
+let with_val f n = f (get n)
+
+let with_loc_val f n = f ?loc:n.CAst.loc (get n)
diff --git a/lib/dAst.mli b/lib/dAst.mli
new file mode 100644
index 0000000000..5b51677fc6
--- /dev/null
+++ b/lib/dAst.mli
@@ -0,0 +1,28 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Lazy AST node wrapper. Only used for [glob_constr] as of today. *)
+
+type ('a, _) thunk =
+| Value : 'a -> ('a, 'b) thunk
+| Thunk : 'a Lazy.t -> ('a, [ `thunk ]) thunk
+
+type ('a, 'b) t = ('a, 'b) thunk CAst.t
+
+val get : ('a, 'b) t -> 'a
+val get_thunk : ('a, 'b) thunk -> 'a
+
+val make : ?loc:Loc.t -> 'a -> ('a, 'b) t
+val delay : ?loc:Loc.t -> (unit -> 'a) -> ('a, [ `thunk ]) t
+
+val map : ('a -> 'b) -> ('a, 'c) t -> ('b, 'c) t
+val map_with_loc : (?loc:Loc.t -> 'a -> 'b) -> ('a, 'c) t -> ('b, 'c) t
+val map_from_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a Loc.located -> ('b, 'c) t
+
+val with_val : ('a -> 'b) -> ('a, 'c) t -> 'b
+val with_loc_val : (?loc:Loc.t -> 'a -> 'b) -> ('a, 'c) t -> 'b
diff --git a/lib/loc.ml b/lib/loc.ml
index 9f036d90f9..06da13d44f 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -8,8 +8,12 @@
(* Locations management *)
+type source =
+ | InFile of string
+ | ToplevelInput
+
type t = {
- fname : string; (** filename *)
+ fname : source; (** filename or toplevel input *)
line_nb : int; (** start line number *)
bol_pos : int; (** position of the beginning of start line *)
line_nb_last : int; (** end line number *)
@@ -23,10 +27,15 @@ let create fname line_nb bol_pos bp ep = {
line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; }
let make_loc (bp, ep) = {
- fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
+ fname = ToplevelInput; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0;
bp = bp; ep = ep; }
+let mergeable loc1 loc2 =
+ loc1.fname = loc2.fname
+
let merge loc1 loc2 =
+ if not (mergeable loc1 loc2) then
+ failwith "Trying to merge unmergeable locations.";
if loc1.bp < loc2.bp then
if loc1.ep < loc2.ep then {
fname = loc1.fname;
diff --git a/lib/loc.mli b/lib/loc.mli
index 1fbaae8368..d4061e0446 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -8,8 +8,12 @@
(** {5 Basic types} *)
+type source =
+ | InFile of string
+ | ToplevelInput
+
type t = {
- fname : string; (** filename *)
+ fname : source; (** filename or toplevel input *)
line_nb : int; (** start line number *)
bol_pos : int; (** position of the beginning of start line *)
line_nb_last : int; (** end line number *)
@@ -22,7 +26,7 @@ type t = {
(** This is inherited from CAMPL4/5. *)
-val create : string -> int -> int -> int -> int -> t
+val create : source -> int -> int -> int -> int -> t
(** Create a location from a filename, a line number, a position of the
beginning of the line, a start and end position *)
diff --git a/lib/option.ml b/lib/option.ml
index 7cedffef08..98b1680354 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 c4d1ebc3a7..66f05023f7 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] *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 05:21:07 +0000