aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check.ml12
-rw-r--r--lib/cList.ml198
-rw-r--r--lib/cList.mli2
-rw-r--r--pretyping/evarconv.ml2
-rw-r--r--pretyping/evarutil.ml4
-rw-r--r--pretyping/evd.ml2
-rw-r--r--printing/printer.ml2
7 files changed, 119 insertions, 103 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 343c72788..a3fc6d0f7 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -149,20 +149,23 @@ let canonical_path_name p =
let find_logical_path phys_dir =
let phys_dir = canonical_path_name phys_dir in
- match List.filter2 (fun p d -> p = phys_dir) !load_paths with
+ let physical, logical = !load_paths in
+ match List.filter2 (fun p d -> p = phys_dir) physical logical with
| _,[dir] -> dir
| _,[] -> default_root_prefix
| _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
let remove_load_path dir =
- load_paths := List.filter2 (fun p d -> p <> dir) !load_paths
+ let physical, logical = !load_paths in
+ load_paths := List.filter2 (fun p d -> p <> dir) physical logical
let add_load_path (phys_path,coq_path) =
if !Flags.debug then
ppnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
str phys_path);
let phys_path = canonical_path_name phys_path in
- match List.filter2 (fun p d -> p = phys_path) !load_paths with
+ let physical, logical = !load_paths in
+ match List.filter2 (fun p d -> p = phys_path) physical logical with
| _,[dir] ->
if coq_path <> dir
(* If this is not the default -I . to coqtop *)
@@ -185,7 +188,8 @@ let add_load_path (phys_path,coq_path) =
| _ -> anomaly ("Two logical paths are associated to "^phys_path)
let load_paths_of_dir_path dir =
- fst (List.filter2 (fun p d -> d = dir) !load_paths)
+ let physical, logical = !load_paths in
+ fst (List.filter2 (fun p d -> d = dir) physical logical)
(************************************************************************)
(*s Locate absolute or partially qualified library names in the path *)
diff --git a/lib/cList.ml b/lib/cList.ml
index ee6b073ea..debfa09be 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -71,7 +71,7 @@ sig
val assign : 'a list -> int -> 'a -> 'a list
val distinct : 'a list -> bool
val duplicates : 'a list -> 'a list
- val filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
+ val filter2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
val map_filter : ('a -> 'b option) -> 'a list -> 'b list
val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
val filter_with : bool list -> 'a list -> 'a list
@@ -187,130 +187,130 @@ type 'a cell = {
external cast : 'a cell -> 'a list = "%identity"
+let rec map_loop f p = function
+| [] -> ()
+| x :: l ->
+ let c = { head = f x; tail = [] } in
+ p.tail <- cast c;
+ map_loop f c l
+
let map f = function
| [] -> []
| x :: l ->
- let rec loop p = function
- | [] -> ()
- | x :: l ->
- let c = { head = f x; tail = [] } in
- p.tail <- cast c;
- loop c l
- in
let c = { head = f x; tail = [] } in
- loop c l;
+ map_loop f c l;
cast c
+let rec map2_loop f p l1 l2 = match l1, l2 with
+| [], [] -> ()
+| x :: l1, y :: l2 ->
+ let c = { head = f x y; tail = [] } in
+ p.tail <- cast c;
+ map2_loop f c l1 l2
+| _ -> invalid_arg "List.map2"
+
let map2 f l1 l2 = match l1, l2 with
| [], [] -> []
| x :: l1, y :: l2 ->
- let rec loop p l1 l2 = match l1, l2 with
- | [], [] -> ()
- | x :: l1, y :: l2 ->
- let c = { head = f x y; tail = [] } in
- p.tail <- cast c;
- loop c l1 l2
- | _ -> invalid_arg "List.map2"
- in
let c = { head = f x y; tail = [] } in
- loop c l1 l2;
+ map2_loop f c l1 l2;
cast c
| _ -> invalid_arg "List.map2"
+let rec append_loop p tl = function
+| [] -> p.tail <- tl
+| x :: l ->
+ let c = { head = x; tail = [] } in
+ p.tail <- cast c;
+ append_loop c tl l
+
let append l1 l2 = match l1 with
| [] -> l2
| x :: l ->
- let rec loop p = function
- | [] -> p.tail <- l2
- | x :: l ->
- let c = { head = x; tail = [] } in
- p.tail <- cast c;
- loop c l
- in
let c = { head = x; tail = [] } in
- loop c l;
+ append_loop c l2 l;
cast c
+let rec copy p = function
+| [] -> p
+| x :: l ->
+ let c = { head = x; tail = [] } in
+ p.tail <- cast c;
+ copy c l
+
+let rec concat_loop p = function
+| [] -> ()
+| x :: l -> concat_loop (copy p x) l
+
let concat l =
- let rec copy p = function
- | [] -> p
- | x :: l ->
- let c = { head = x; tail = [] } in
- p.tail <- cast c;
- copy c l
- in
- let rec loop p = function
- | [] -> ()
- | x :: l -> loop (copy p x) l
- in
let dummy = { head = Obj.magic 0; tail = [] } in
- loop dummy l;
+ concat_loop dummy l;
dummy.tail
let flatten = concat
+let rec split_loop p q = function
+| [] -> ()
+| (x, y) :: l ->
+ let cl = { head = x; tail = [] } in
+ let cr = { head = y; tail = [] } in
+ p.tail <- cast cl;
+ q.tail <- cast cr;
+ split_loop cl cr l
+
let split = function
| [] -> [], []
| (x, y) :: l ->
- let rec loop p q = function
- | [] -> ()
- | (x, y) :: l ->
- let cl = { head = x; tail = [] } in
- let cr = { head = y; tail = [] } in
- p.tail <- cast cl;
- q.tail <- cast cr;
- loop cl cr l
- in
let cl = { head = x; tail = [] } in
let cr = { head = y; tail = [] } in
- loop cl cr l;
+ split_loop cl cr l;
(cast cl, cast cr)
+let rec combine_loop p l1 l2 = match l1, l2 with
+| [], [] -> ()
+| x :: l1, y :: l2 ->
+ let c = { head = (x, y); tail = [] } in
+ p.tail <- cast c;
+ combine_loop c l1 l2
+| _ -> invalid_arg "List.combine"
+
let combine l1 l2 = match l1, l2 with
| [], [] -> []
| x :: l1, y :: l2 ->
- let rec loop p l1 l2 = match l1, l2 with
- | [], [] -> ()
- | x :: l1, y :: l2 ->
- let c = { head = (x, y); tail = [] } in
- p.tail <- cast c;
- loop c l1 l2
- | _ -> invalid_arg "List.combine"
- in
let c = { head = (x, y); tail = [] } in
- loop c l1 l2;
+ combine_loop c l1 l2;
cast c
| _ -> invalid_arg "List.combine"
+let rec filter_loop f p = function
+| [] -> ()
+| x :: l ->
+ if f x then
+ let c = { head = x; tail = [] } in
+ let () = p.tail <- cast c in
+ filter_loop f c l
+ else
+ filter_loop f p l
+
let filter f l =
- let rec loop p = function
- | [] -> ()
- | x :: l ->
- if f x then
- let c = { head = x; tail = [] } in
- let () = p.tail <- cast c in
- loop c l
- else
- loop p l
- in
let c = { head = Obj.magic 0; tail = [] } in
- loop c l;
+ filter_loop f c l;
c.tail
(** FIXME: Already present in OCaml 4.00 *)
+let rec map_i_loop f i p = function
+| [] -> ()
+| x :: l ->
+ let c = { head = f i x; tail = [] } in
+ p.tail <- cast c;
+ map_i_loop f (succ i) c l
+
let map_i f i = function
| [] -> []
| x :: l ->
- let rec loop i p = function
- | [] -> ()
- | x :: l ->
- let c = { head = f i x; tail = [] } in
- p.tail <- cast c;
- loop (succ i) c l
- in
let c = { head = f i x; tail = [] } in
- loop (succ i) c l;
+ map_i_loop f (succ i) c l;
cast c
(** Extensions of OCaml Stdlib *)
@@ -335,7 +335,7 @@ let rec equal cmp l1 l2 =
| _ -> false
let intersect l1 l2 =
- List.filter (fun x -> List.mem x l2) l1
+ filter (fun x -> List.mem x l2) l1
let union l1 l2 =
let rec urec = function
@@ -357,16 +357,16 @@ let subtract l1 l2 =
let subtractq l1 l2 =
if l2 = [] then l1 else List.filter (fun x -> not (List.memq x l2)) l1
+let rec tabulate_loop f len p i =
+ if len <= i then ()
+ else
+ let c = { head = f i; tail = [] } in
+ let () = p.tail <- cast c in
+ tabulate_loop f len c (succ i)
+
let tabulate f len =
- let rec loop p i =
- if len <= i then ()
- else
- let c = { head = f i; tail = [] } in
- let () = p.tail <- cast c in
- loop c (succ i)
- in
let dummy = { head = Obj.magic 0; tail = [] } in
- loop dummy 0;
+ tabulate_loop f len dummy 0;
dummy.tail
let interval n m =
@@ -434,7 +434,7 @@ let rec smartfilter f l = match l with
if tl' == tl then l
else h :: tl'
else tl'
-
+
let index_f f x =
let rec index_x n = function
| y::l -> if f x y then n else index_x (succ n) l
@@ -599,12 +599,24 @@ let rec duplicates = function
let l' = duplicates l in
if List.mem x l then add_set x l' else l'
-let rec filter2 f = function
- | [], [] as p -> p
- | d::dp, l::lp ->
- let (dp',lp' as p) = filter2 f (dp,lp) in
- if f d l then d::dp', l::lp' else p
- | _ -> invalid_arg "List.filter2"
+let rec filter2_loop f p q l1 l2 = match l1, l2 with
+| [], [] -> ()
+| x :: l1, y :: l2 ->
+ if f x y then
+ let c1 = { head = x; tail = [] } in
+ let c2 = { head = y; tail = [] } in
+ let () = p.tail <- cast c1 in
+ let () = q.tail <- cast c2 in
+ filter2_loop f c1 c2 l1 l2
+ else
+ filter2_loop f p q l1 l2
+| _ -> invalid_arg "List.filter2"
+
+let filter2 f l1 l2 =
+ let c1 = { head = Obj.magic 0; tail = [] } in
+ let c2 = { head = Obj.magic 0; tail = [] } in
+ filter2_loop f c1 c2 l1 l2;
+ (c1.tail, c2.tail)
let rec map_filter f = function
| [] -> []
@@ -621,7 +633,7 @@ let map_filter_i f =
in aux 0
let filter_along f filter l =
- snd (filter2 (fun b c -> f b) (filter,l))
+ snd (filter2 (fun b c -> f b) filter l)
let filter_with filter l =
filter_along (fun x -> x) filter l
diff --git a/lib/cList.mli b/lib/cList.mli
index fbc87f301..2e0d519a1 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -97,7 +97,7 @@ sig
(** Return the list of unique elements which appear at least twice. Elements
are kept in the order of their first appearance. *)
- val filter2 : ('a -> 'b -> bool) -> 'a list * 'b list -> 'a list * 'b list
+ val filter2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
val map_filter : ('a -> 'b option) -> 'a list -> 'b list
val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 30f6de5c2..26b326713 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -635,7 +635,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
| Some _ -> error "Selection of specific occurrences not supported"
| None ->
let evty = set_holes evdref cty subst in
- let instance = snd (List.filter2 (fun b c -> b) (filter,instance)) in
+ let _, instance = List.filter2 (fun b c -> b) filter instance in
let evd,ev = new_evar_instance sign !evdref evty ~filter instance in
evdref := evd;
evsref := (fst (destEvar ev),evty)::!evsref;
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 45df12e46..7ccc9d493 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -249,7 +249,7 @@ let apply_subfilter filter subfilter =
filter ([], List.rev subfilter))
let extract_subfilter initial_filter refined_filter =
- snd (List.filter2 (fun b1 b2 -> b1) (initial_filter,refined_filter))
+ snd (List.filter2 (fun b1 b2 -> b1) initial_filter refined_filter)
(**********************)
(* Creating new evars *)
@@ -376,7 +376,7 @@ let restrict_evar_key evd evk filter candidates =
let sign = evar_hyps evi in
let src = evi.evar_source in
let evd,newevk = new_pure_evar evd sign ccl ~src ~filter ?candidates in
- let ctxt = snd (List.filter2 (fun b c -> b) (filter,evar_context evi)) in
+ let _, ctxt = List.filter2 (fun b c -> b) filter (evar_context evi) in
let id_inst = Array.of_list (List.map (fun (id,_,_) -> mkVar id) ctxt) in
Evd.define evk (mkEvar(newevk,id_inst)) evd,newevk
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index c838b422d..d24509c85 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -56,7 +56,7 @@ let evar_body evi = evi.evar_body
let evar_filter evi = evi.evar_filter
let evar_unfiltered_env evi = Global.env_of_context evi.evar_hyps
let evar_filtered_context evi =
- snd (List.filter2 (fun b c -> b) (evar_filter evi,evar_context evi))
+ snd (List.filter2 (fun b c -> b) (evar_filter evi) (evar_context evi))
let evar_env evi =
List.fold_right push_named (evar_filtered_context evi)
(reset_context (Global.env()))
diff --git a/printing/printer.ml b/printing/printer.ml
index 7d9d27e81..69fec870a 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -288,7 +288,7 @@ let pr_concl n sigma g =
(* display evar type: a context and a type *)
let pr_evgl_sign gl =
let ps = pr_named_context_of (evar_unfiltered_env gl) in
- let _,l = List.filter2 (fun b c -> not b) (evar_filter gl,evar_context gl) in
+ let _, l = List.filter2 (fun b c -> not b) (evar_filter gl) (evar_context gl) in
let ids = List.rev (List.map pi1 l) in
let warn =
if ids = [] then mt () else
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 16:24:21 +0000