aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/cList.ml35
-rw-r--r--lib/cList.mli7
-rw-r--r--lib/cMap.ml10
-rw-r--r--lib/cMap.mli2
-rw-r--r--lib/cProfile.ml (renamed from lib/profile.ml)0
-rw-r--r--lib/cProfile.mli (renamed from lib/profile.mli)0
-rw-r--r--lib/cSig.mli6
-rw-r--r--lib/control.ml7
-rw-r--r--lib/control.mli3
-rw-r--r--lib/dyn.ml10
-rw-r--r--lib/dyn.mli1
-rw-r--r--lib/envars.ml12
-rw-r--r--lib/flags.ml39
-rw-r--r--lib/flags.mli39
-rw-r--r--lib/hMap.ml26
-rw-r--r--lib/lib.mllib2
-rw-r--r--lib/pp.ml1
-rw-r--r--lib/pp.mli3
-rw-r--r--lib/system.ml6
-rw-r--r--lib/system.mli3
20 files changed, 95 insertions, 117 deletions
diff --git a/lib/cList.ml b/lib/cList.ml
index ca69628af7..0ef7c3d8ba 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -96,6 +96,8 @@ sig
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_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list
+ val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list
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
@@ -446,6 +448,12 @@ let rec fold_left3 f accu l1 l2 l3 =
| (a1::l1, a2::l2, a3::l3) -> fold_left3 f (f accu a1 a2 a3) l1 l2 l3
| (_, _, _) -> invalid_arg "List.fold_left3"
+let rec fold_left4 f accu l1 l2 l3 l4 =
+ match (l1, l2, l3, l4) with
+ ([], [], [], []) -> accu
+ | (a1::l1, a2::l2, a3::l3, a4::l4) -> fold_left4 f (f accu a1 a2 a3 a4) l1 l2 l3 l4
+ | (_,_, _, _) -> invalid_arg "List.fold_left4"
+
(* [fold_right_and_left f [a1;...;an] hd =
f (f (... (f (f hd
an
@@ -765,12 +773,13 @@ let share_tails l1 l2 =
in
shr_rev [] (List.rev l1, List.rev l2)
+(* Poor man's monadic map *)
let rec fold_left_map f e = function
- | [] -> (e,[])
- | h::t ->
- let e',h' = f e h in
- let e'',t' = fold_left_map f e' t in
- e'',h'::t'
+ | [] -> (e,[])
+ | h::t ->
+ let e',h' = f e h in
+ let e'',t' = fold_left_map f e' t in
+ e'',h'::t'
let fold_map = fold_left_map
@@ -790,12 +799,26 @@ let fold_right_map f l e =
let fold_map' = fold_right_map
+let on_snd f (x,y) = (x,f y)
+
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'
+ on_snd List.rev @@
+ 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 fold_left3_map f e l l' l'' =
+ on_snd List.rev @@
+ fold_left3 (fun (e,l) x x' x'' -> let (e,y) = f e x x' x'' in (e,y::l)) (e,[]) l l' l''
+
+let fold_left4_map f e l1 l2 l3 l4 =
+ on_snd List.rev @@
+ fold_left4 (fun (e,l) x1 x2 x3 x4 -> let (e,y) = f e x1 x2 x3 x4 in (e,y::l)) (e,[]) l1 l2 l3 l4
+
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 8cb07da79c..f87db04cf4 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -211,7 +211,14 @@ sig
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_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list
+ (** Same with three lists, folding on the left *)
+
+ val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list
+ (** Same with four lists, folding on the left *)
+
val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
+ (* [@@ocaml.deprecated "Same as [fold_left_map]"] *)
(** @deprecated Same as [fold_left_map] *)
val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
diff --git a/lib/cMap.ml b/lib/cMap.ml
index 0ecb40209c..b4c4aedd0e 100644
--- a/lib/cMap.ml
+++ b/lib/cMap.ml
@@ -26,7 +26,7 @@ sig
include CSig.MapS
module Set : CSig.SetS with type elt = key
val get : key -> 'a t -> 'a
- val update : key -> 'a -> 'a t -> 'a t
+ val set : key -> 'a -> 'a t -> 'a t
val modify : key -> (key -> 'a -> 'a) -> 'a t -> 'a t
val domain : 'a t -> Set.t
val bind : (key -> 'a) -> Set.t -> 'a t
@@ -50,7 +50,7 @@ end
module MapExt (M : Map.OrderedType) :
sig
type 'a map = 'a Map.Make(M).t
- val update : M.t -> 'a -> 'a map -> 'a map
+ val set : M.t -> 'a -> 'a map -> 'a map
val modify : M.t -> (M.t -> 'a -> 'a) -> 'a map -> 'a map
val domain : 'a map -> Set.Make(M).t
val bind : (M.t -> 'a) -> Set.Make(M).t -> 'a map
@@ -93,19 +93,19 @@ struct
let set_prj : set -> _set = Obj.magic
let set_inj : _set -> set = Obj.magic
- let rec update k v (s : 'a map) : 'a map = match map_prj s with
+ let rec set k v (s : 'a map) : 'a map = match map_prj s with
| MEmpty -> raise Not_found
| MNode (l, k', v', r, h) ->
let c = M.compare k k' in
if c < 0 then
- let l' = update k v l in
+ let l' = set k v l in
if l == l' then s
else map_inj (MNode (l', k', v', r, h))
else if c = 0 then
if v' == v then s
else map_inj (MNode (l, k', v, r, h))
else
- let r' = update k v r in
+ let r' = set k v r in
if r == r' then s
else map_inj (MNode (l, k', v', r', h))
diff --git a/lib/cMap.mli b/lib/cMap.mli
index f65036139b..5e65bd200a 100644
--- a/lib/cMap.mli
+++ b/lib/cMap.mli
@@ -34,7 +34,7 @@ sig
val get : key -> 'a t -> 'a
(** Same as {!find} but fails an assertion instead of raising [Not_found] *)
- val update : key -> 'a -> 'a t -> 'a t
+ val set : key -> 'a -> 'a t -> 'a t
(** Same as [add], but expects the key to be present, and thus faster.
@raise Not_found when the key is unbound in the map. *)
diff --git a/lib/profile.ml b/lib/cProfile.ml
index 0bc226a450..0bc226a450 100644
--- a/lib/profile.ml
+++ b/lib/cProfile.ml
diff --git a/lib/profile.mli b/lib/cProfile.mli
index cae4397a11..cae4397a11 100644
--- a/lib/profile.mli
+++ b/lib/cProfile.mli
diff --git a/lib/cSig.mli b/lib/cSig.mli
index 6910cbbf03..32e9d2af0c 100644
--- a/lib/cSig.mli
+++ b/lib/cSig.mli
@@ -56,6 +56,12 @@ sig
val is_empty: 'a t -> bool
val mem: key -> 'a t -> bool
val add: key -> 'a -> 'a t -> 'a t
+ (* when Coq requires OCaml 4.06 or later, can add:
+
+ val update : key -> ('a option -> 'a option) -> 'a t -> 'a t
+
+ allowing Coq to use OCaml's "update"
+ *)
val singleton: key -> 'a -> 'a t
val remove: key -> 'a t -> 'a t
val merge:
diff --git a/lib/control.ml b/lib/control.ml
index d936d7557b..c6489938e8 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -12,15 +12,12 @@ let interrupt = ref false
let steps = ref 0
-let are_we_threading = lazy (
- match !Flags.async_proofs_mode with
- | Flags.APon -> true
- | _ -> false)
+let enable_thread_delay = ref false
let check_for_interrupt () =
if !interrupt then begin interrupt := false; raise Sys.Break end;
incr steps;
- if !steps = 1000 && Lazy.force are_we_threading then begin
+ if !enable_thread_delay && !steps = 1000 then begin
Thread.delay 0.001;
steps := 0;
end
diff --git a/lib/control.mli b/lib/control.mli
index f6c63ffb34..261b076931 100644
--- a/lib/control.mli
+++ b/lib/control.mli
@@ -8,6 +8,9 @@
(** Global control of Coq. *)
+(** Will periodically call [Thread.delay] if set to true *)
+val enable_thread_delay : bool ref
+
val interrupt : bool ref
(** Coq interruption: set the following boolean reference to interrupt Coq
(it eventually raises [Break], simulating a Ctrl-C) *)
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 83e673d2c0..64535d35f6 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -55,6 +55,8 @@ sig
include PreS
module Easy : sig
+
+ val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag
val make_dyn : string -> ('a -> t) * (t -> 'a)
val inj : 'a -> 'a tag -> t
val prj : t -> 'a tag -> 'a option
@@ -129,8 +131,9 @@ end
include Self
module Easy = struct
+
(* now tags are opaque, we can do the trick *)
-let make_dyn (s : string) =
+let make_dyn_tag (s : string) =
(fun (type a) (tag : a tag) ->
let infun : (a -> t) = fun x -> Dyn (tag, x) in
let outfun : (t -> a) = fun (Dyn (t, x)) ->
@@ -138,9 +141,12 @@ let make_dyn (s : string) =
| None -> assert false
| Some CSig.Refl -> x
in
- (infun, outfun))
+ infun, outfun, tag)
(create s)
+let make_dyn (s : string) =
+ let inf, outf, _ = make_dyn_tag s in inf, outf
+
let inj x tag = Dyn(tag,x)
let prj : type a. t -> a tag -> a option =
fun (Dyn(tag',x)) tag ->
diff --git a/lib/dyn.mli b/lib/dyn.mli
index e0e1a9d140..2206394e2d 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -53,6 +53,7 @@ val dump : unit -> (int * string) list
module Easy : sig
(* To create a dynamic type on the fly *)
+ val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag
val make_dyn : string -> ('a -> t) * (t -> 'a)
(* For types declared with the [create] function above *)
diff --git a/lib/envars.ml b/lib/envars.ml
index 206d750338..8ebf84057b 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -153,19 +153,17 @@ let coqpath =
let exe s = s ^ Coq_config.exec_extension
-let ocamlfind () =
- if !Flags.ocamlfind_spec then !Flags.ocamlfind else Coq_config.ocamlfind
+let ocamlfind () = Coq_config.ocamlfind
(** {2 Camlp4 paths} *)
let guess_camlp4bin () = which (user_path ()) (exe Coq_config.camlp4)
let camlp4bin () =
- if !Flags.camlp4bin_spec then !Flags.camlp4bin else
- if !Flags.boot then Coq_config.camlp4bin else
- try guess_camlp4bin ()
- with Not_found ->
- Coq_config.camlp4bin
+ if !Flags.boot then Coq_config.camlp4bin else
+ try guess_camlp4bin ()
+ with Not_found ->
+ Coq_config.camlp4bin
let camlp4 () = camlp4bin () / exe Coq_config.camlp4
diff --git a/lib/flags.ml b/lib/flags.ml
index ddc8f84825..644f66d02b 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -35,36 +35,10 @@ let record_aux_file = ref false
let test_mode = ref false
-type async_proofs = APoff | APonLazy | APon
-let async_proofs_mode = ref APoff
-type cache = Force
-let async_proofs_cache = ref None
-let async_proofs_n_workers = ref 1
-let async_proofs_n_tacworkers = ref 2
-let async_proofs_private_flags = ref None
-let async_proofs_full = ref false
-let async_proofs_never_reopen_branch = ref false
-let async_proofs_flags_for_workers = ref []
let async_proofs_worker_id = ref "master"
-type priority = Low | High
-let async_proofs_worker_priority = ref Low
-let string_of_priority = function Low -> "low" | High -> "high"
-let priority_of_string = function
- | "low" -> Low
- | "high" -> High
- | _ -> raise (Invalid_argument "priority_of_string")
-type tac_error_filter = [ `None | `Only of string list | `All ]
-let async_proofs_tac_error_resilience = ref (`Only [ "curly" ])
-let async_proofs_cmd_error_resilience = ref true
-
-let async_proofs_is_worker () =
- !async_proofs_worker_id <> "master"
-let async_proofs_is_master () =
- !async_proofs_mode = APon && !async_proofs_worker_id = "master"
-let async_proofs_delegation_threshold = ref 0.03
+let async_proofs_is_worker () = !async_proofs_worker_id <> "master"
let debug = ref false
-let stm_debug = ref false
let in_debugger = ref false
let in_toplevel = ref false
@@ -179,14 +153,6 @@ let is_standard_doc_url url =
let coqlib_spec = ref false
let coqlib = ref "(not initialized yet)"
-(* Options for changing ocamlfind (used by coqmktop) *)
-let ocamlfind_spec = ref false
-let ocamlfind = ref Coq_config.camlbin
-
-(* Options for changing camlp4bin (used by coqmktop) *)
-let camlp4bin_spec = ref false
-let camlp4bin = ref Coq_config.camlp4bin
-
(* Level of inlining during a functor application *)
let default_inline_level = 100
@@ -195,12 +161,11 @@ let set_inline_level = (:=) inline_level
let get_inline_level () = !inline_level
(* Native code compilation for conversion and normalization *)
-let native_compiler = ref false
+let output_native_objects = ref false
(* Print the mod uid associated to a vo file by the native compiler *)
let print_mod_uid = ref false
-let tactic_context_compat = ref false
let profile_ltac = ref false
let profile_ltac_cutoff = ref 2.0
diff --git a/lib/flags.mli b/lib/flags.mli
index c4afb83186..000862b2c6 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -21,35 +21,14 @@ val record_aux_file : bool ref
val test_mode : bool ref
(** Async-related flags *)
-type async_proofs = APoff | APonLazy | APon
-val async_proofs_mode : async_proofs ref
-type cache = Force
-val async_proofs_cache : cache option ref
-val async_proofs_n_workers : int ref
-val async_proofs_n_tacworkers : int ref
-val async_proofs_private_flags : string option ref
-val async_proofs_is_worker : unit -> bool
-val async_proofs_is_master : unit -> bool
-val async_proofs_full : bool ref
-val async_proofs_never_reopen_branch : bool ref
-val async_proofs_flags_for_workers : string list ref
val async_proofs_worker_id : string ref
-type priority = Low | High
-val async_proofs_worker_priority : priority ref
-val string_of_priority : priority -> string
-val priority_of_string : string -> priority
-type tac_error_filter = [ `None | `Only of string list | `All ]
-val async_proofs_tac_error_resilience : tac_error_filter ref
-val async_proofs_cmd_error_resilience : bool ref
-val async_proofs_delegation_threshold : float ref
+val async_proofs_is_worker : unit -> bool
+(** Debug flags *)
val debug : bool ref
val in_debugger : bool ref
val in_toplevel : bool ref
-(** Enable STM debugging *)
-val stm_debug : bool ref
-
val profile : bool
(* -ide_slave: printing will be more verbose, will affect stm caching *)
@@ -143,27 +122,17 @@ val is_standard_doc_url : string -> bool
val coqlib_spec : bool ref
val coqlib : string ref
-(** Options for specifying where OCaml binaries reside *)
-val ocamlfind_spec : bool ref
-val ocamlfind : string ref
-val camlp4bin_spec : bool ref
-val camlp4bin : string ref
-
(** Level of inlining during a functor application *)
val set_inline_level : int -> unit
val get_inline_level : unit -> int
val default_inline_level : int
-(** Native code compilation for conversion and normalization *)
-val native_compiler : bool ref
+(** When producing vo objects, also compile the native-code version *)
+val output_native_objects : bool ref
(** Print the mod uid associated to a vo file by the native compiler *)
val print_mod_uid : bool ref
-val tactic_context_compat : bool ref
-(** Set to [true] to trigger the compatibility bugged context matching (old
- context vs. appcontext) is set. *)
-
val profile_ltac : bool ref
val profile_ltac_cutoff : float ref
diff --git a/lib/hMap.ml b/lib/hMap.ml
index c69efdb711..37079af783 100644
--- a/lib/hMap.ml
+++ b/lib/hMap.ml
@@ -47,7 +47,7 @@ struct
try
let m = Int.Map.find h s in
let m = Set.add x m in
- Int.Map.update h m s
+ Int.Map.set h m s
with Not_found ->
let m = Set.singleton x in
Int.Map.add h m s
@@ -65,7 +65,7 @@ struct
if Set.is_empty m then
Int.Map.remove h s
else
- Int.Map.update h m s
+ Int.Map.set h m s
with Not_found -> s
let height s = Int.Map.height s
@@ -135,7 +135,7 @@ struct
let s' = Int.Map.find h accu in
let si = Set.filter (fun e -> not (Set.mem e s)) s' in
if Set.is_empty si then Int.Map.remove h accu
- else Int.Map.update h si accu
+ else Int.Map.set h si accu
with Not_found -> accu
in
Int.Map.fold fold s2 s1
@@ -242,11 +242,19 @@ struct
try
let m = Int.Map.find h s in
let m = Map.add k x m in
- Int.Map.update h m s
+ Int.Map.set h m s
with Not_found ->
let m = Map.singleton k x in
Int.Map.add h m s
+ (* when Coq requires OCaml 4.06 or later, the module type
+ CSig.MapS may include the signature of OCaml's "update",
+ requiring an implementation here, which could be just:
+
+ let update k f s = assert false (* not implemented *)
+
+ *)
+
let singleton k x =
let h = M.hash k in
Int.Map.singleton h (Map.singleton k x)
@@ -259,7 +267,7 @@ struct
if Map.is_empty m then
Int.Map.remove h s
else
- Int.Map.update h m s
+ Int.Map.set h m s
with Not_found -> s
let merge f s1 s2 =
@@ -359,7 +367,7 @@ struct
let h = M.hash k in
let m = Int.Map.find h s in
let m = Map.modify k f m in
- Int.Map.update h m s
+ Int.Map.set h m s
let bind f s =
let fb m = Map.bind f m in
@@ -367,11 +375,11 @@ struct
let domain s = Int.Map.map Map.domain s
- let update k x s =
+ let set k x s =
let h = M.hash k in
let m = Int.Map.find h s in
- let m = Map.update k x m in
- Int.Map.update h m s
+ let m = Map.set k x m in
+ Int.Map.set h m s
let smartmap f s =
let fs m = Map.smartmap f m in
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 8791f07417..66f939a910 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -9,7 +9,7 @@ System
CThread
Spawn
Trie
-Profile
+CProfile
Explore
Predicate
Rtree
diff --git a/lib/pp.ml b/lib/pp.ml
index c3338688d2..770e650cbd 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -208,6 +208,7 @@ let string_of_ppcmds c =
let pr_comma () = str "," ++ spc ()
let pr_semicolon () = str ";" ++ spc ()
let pr_bar () = str "|" ++ spc ()
+let pr_spcbar () = str " |" ++ spc ()
let pr_arg pr x = spc () ++ pr x
let pr_non_empty_arg pr x = let pp = pr x in if ismt pp then mt () else spc () ++ pr x
let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x
diff --git a/lib/pp.mli b/lib/pp.mli
index 2d11cad86e..d9be1c5ce9 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -120,6 +120,9 @@ val pr_semicolon : unit -> t
val pr_bar : unit -> t
(** Well-spaced pipe bar. *)
+val pr_spcbar : unit -> t
+(** Pipe bar with space before and after. *)
+
val pr_arg : ('a -> t) -> 'a -> t
(** Adds a space in front of its argument. *)
diff --git a/lib/system.ml b/lib/system.ml
index 4b5066ef41..2c8dbac7c0 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -309,9 +309,3 @@ let with_time time f x =
let msg2 = if time then "" else " (failure)" in
Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
raise e
-
-let process_id () =
- Printf.sprintf "%d:%s:%d" (Unix.getpid ())
- (if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id
- else "master")
- (Thread.id (Thread.self ()))
diff --git a/lib/system.mli b/lib/system.mli
index aa964abebe..c02bc9c8ac 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -105,6 +105,3 @@ val time_difference : time -> time -> float (** in seconds *)
val fmt_time_difference : time -> time -> Pp.t
val with_time : bool -> ('a -> 'b) -> 'a -> 'b
-
-(** {6 Name of current process.} *)
-val process_id : unit -> string
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 09:04:00 +0000