aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/aux_file.ml9
-rw-r--r--lib/aux_file.mli3
-rw-r--r--lib/cErrors.ml (renamed from lib/errors.ml)13
-rw-r--r--lib/cErrors.mli (renamed from lib/errors.mli)0
-rw-r--r--lib/cList.ml83
-rw-r--r--lib/cList.mli10
-rw-r--r--lib/cMap.ml50
-rw-r--r--lib/cMap.mli21
-rw-r--r--lib/cSig.mli4
-rw-r--r--lib/cWarnings.ml120
-rw-r--r--lib/cWarnings.mli34
-rw-r--r--lib/clib.mllib7
-rw-r--r--lib/dyn.ml134
-rw-r--r--lib/dyn.mli58
-rw-r--r--lib/envars.ml27
-rw-r--r--lib/envars.mli13
-rw-r--r--lib/explore.ml2
-rw-r--r--lib/feedback.ml265
-rw-r--r--lib/feedback.mli105
-rw-r--r--lib/flags.ml43
-rw-r--r--lib/flags.mli15
-rw-r--r--lib/future.ml25
-rw-r--r--lib/future.mli3
-rw-r--r--lib/genarg.ml319
-rw-r--r--lib/genarg.mli182
-rw-r--r--lib/hMap.ml116
-rw-r--r--lib/hashcons.ml31
-rw-r--r--lib/hashset.ml2
-rw-r--r--lib/heap.ml2
-rw-r--r--lib/iStream.ml6
-rw-r--r--lib/lib.mllib5
-rw-r--r--lib/loc.ml5
-rw-r--r--lib/loc.mli17
-rw-r--r--lib/minisys.ml74
-rw-r--r--lib/option.ml4
-rw-r--r--lib/option.mli16
-rw-r--r--lib/pp.ml243
-rw-r--r--lib/pp.mli143
-rw-r--r--lib/ppstyle.ml45
-rw-r--r--lib/ppstyle.mli14
-rw-r--r--lib/profile.ml2
-rw-r--r--lib/remoteCounter.ml4
-rw-r--r--lib/richpp.ml30
-rw-r--r--lib/richpp.mli23
-rw-r--r--lib/serialize.ml116
-rw-r--r--lib/serialize.mli37
-rw-r--r--lib/spawn.ml18
-rw-r--r--lib/stateid.ml26
-rw-r--r--lib/stateid.mli11
-rw-r--r--lib/system.ml123
-rw-r--r--lib/system.mli38
-rw-r--r--lib/unicode.ml77
-rw-r--r--lib/unicode.mli20
-rw-r--r--lib/util.ml30
-rw-r--r--lib/util.mli20
-rw-r--r--lib/xml_lexer.mli44
-rw-r--r--lib/xml_lexer.mll317
-rw-r--r--lib/xml_parser.ml232
-rw-r--r--lib/xml_parser.mli106
-rw-r--r--lib/xml_printer.ml145
-rw-r--r--lib/xml_printer.mli29
61 files changed, 1569 insertions, 2147 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index f7bd81f85..c6c7b4242 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -25,9 +25,9 @@ let mk_absolute vfile =
if Filename.is_relative vfile then CUnix.correct_path vfile (Sys.getcwd ())
else vfile
-let start_aux_file_for vfile =
- let vfile = mk_absolute vfile in
- oc := Some (open_out (aux_file_name_for vfile));
+let start_aux_file ~aux_file:output_file ~v_file =
+ let vfile = mk_absolute v_file in
+ oc := Some (open_out output_file);
Printf.fprintf (Option.get !oc) "COQAUX%d %s %s\n"
version (Digest.to_hex (Digest.file vfile)) vfile
@@ -87,8 +87,7 @@ let load_aux_file_for vfile =
| End_of_file -> !h
| Sys_error s | Scanf.Scan_failure s
| Failure s | Invalid_argument s ->
- Flags.if_verbose
- Pp.msg_warning Pp.(str"Loading file "++str aux_fname++str": "++str s);
+ Flags.if_verbose Feedback.msg_info Pp.(str"Loading file "++str aux_fname++str": "++str s);
empty_aux_file
let set h loc k v = set h (Loc.unloc loc) k v
diff --git a/lib/aux_file.mli b/lib/aux_file.mli
index 127827ab6..86e322b71 100644
--- a/lib/aux_file.mli
+++ b/lib/aux_file.mli
@@ -17,7 +17,8 @@ module H : Map.S with type key = int * int
module M : Map.S with type key = string
val contents : aux_file -> string M.t H.t
-val start_aux_file_for : string -> unit
+val aux_file_name_for : string -> string
+val start_aux_file : aux_file:string -> v_file:string -> unit
val stop_aux_file : unit -> unit
val recording : unit -> bool
diff --git a/lib/errors.ml b/lib/cErrors.ml
index c1d224dfc..c69c7e400 100644
--- a/lib/errors.ml
+++ b/lib/cErrors.ml
@@ -16,6 +16,13 @@ let push = Backtrace.add_backtrace
exception Anomaly of string option * std_ppcmds (* System errors *)
+let _ =
+ let pr = function
+ | Anomaly (s, pp) -> Some ("\"Anomaly: " ^ string_of_ppcmds pp ^ "\"")
+ | _ -> None
+ in
+ Printexc.register_printer pr
+
let make_anomaly ?label pp =
Anomaly (label, pp)
@@ -86,7 +93,9 @@ let print_backtrace e = match Backtrace.get_backtrace e with
let print_anomaly askreport e =
if askreport then
- hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ str "Please report.")
+ hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++
+ strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++
+ str ".")
else
hov 0 (raw_anomaly e)
@@ -137,5 +146,5 @@ let handled e =
let fatal_error info anomaly =
let msg = info ++ fnl () in
pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg;
- flush_all ();
+ Format.pp_print_flush !Pp_control.err_ft ();
exit (if anomaly then 129 else 1)
diff --git a/lib/errors.mli b/lib/cErrors.mli
index e5dad93fd..e5dad93fd 100644
--- a/lib/errors.mli
+++ b/lib/cErrors.mli
diff --git a/lib/cList.ml b/lib/cList.ml
index 0ac372d8d..c8283e3c7 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -47,7 +47,11 @@ sig
('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
val filteri :
(int -> 'a -> bool) -> 'a list -> 'a list
+ val partitioni :
+ (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
val smartfilter : ('a -> bool) -> 'a list -> 'a list
+ val extend : bool list -> 'a -> 'a list -> 'a list
+ val count : ('a -> bool) -> 'a list -> int
val index : 'a eq -> 'a -> 'a list -> int
val index0 : 'a eq -> 'a -> 'a list -> int
val iteri : (int -> 'a -> unit) -> 'a list -> unit
@@ -61,6 +65,7 @@ sig
val except : 'a eq -> 'a -> 'a list -> 'a list
val remove : 'a eq -> 'a -> 'a list -> 'a list
val remove_first : ('a -> bool) -> 'a list -> 'a list
+ val extract_first : ('a -> bool) -> 'a list -> 'a list * 'a
val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val sep_last : 'a list -> 'a * 'a list
@@ -375,6 +380,18 @@ let rec smartfilter f l = match l with
else h :: tl'
else tl'
+let rec extend l a l' = match l,l' with
+ | true::l, b::l' -> b :: extend l a l'
+ | false::l, l' -> a :: extend l a l'
+ | [], [] -> []
+ | _ -> invalid_arg "extend"
+
+let count f l =
+ let rec aux acc = function
+ | [] -> acc
+ | h :: t -> if f h then aux (acc + 1) t else aux acc t in
+ aux 0 l
+
let rec index_f f x l n = match l with
| [] -> raise Not_found
| y :: l -> if f x y then n else index_f f x l (succ n)
@@ -445,6 +462,14 @@ let rec remove_first p = function
| b::l -> b::remove_first p l
| [] -> raise Not_found
+let extract_first p li =
+ let rec loop rev_left = function
+ | [] -> raise Not_found
+ | x::right ->
+ if p x then List.rev_append rev_left right, x
+ else loop (x :: rev_left) right
+ in loop [] li
+
let insert p v l =
let rec insrec = function
| [] -> [v]
@@ -472,6 +497,15 @@ let filteri p =
in
filter_i_rec 0
+let partitioni p =
+ let rec aux i = function
+ | [] -> [], []
+ | x :: l ->
+ let (l1, l2) = aux (succ i) l in
+ if p i x then (x :: l1, l2)
+ else (l1, x :: l2)
+ in aux 0
+
let rec sep_last = function
| [] -> failwith "sep_last"
| hd::[] -> (hd,[])
@@ -567,19 +601,35 @@ let filter2 f l1 l2 =
filter2_loop f c1 c2 l1 l2;
(c1.tail, c2.tail)
-let rec map_filter f = function
- | [] -> []
- | x::l ->
- let l' = map_filter f l in
- match f x with None -> l' | Some y -> y::l'
+let rec map_filter_loop f p = function
+ | [] -> ()
+ | x :: l ->
+ match f x with
+ | None -> map_filter_loop f p l
+ | Some y ->
+ let c = { head = y; tail = [] } in
+ p.tail <- cast c;
+ map_filter_loop f c l
+
+let map_filter f l =
+ let c = { head = Obj.magic 0; tail = [] } in
+ map_filter_loop f c l;
+ c.tail
-let map_filter_i f =
- let rec aux i = function
- | [] -> []
- | x::l ->
- let l' = aux (succ i) l in
- match f i x with None -> l' | Some y -> y::l'
- in aux 0
+let rec map_filter_i_loop f i p = function
+ | [] -> ()
+ | x :: l ->
+ match f i x with
+ | None -> map_filter_i_loop f (succ i) p l
+ | Some y ->
+ let c = { head = y; tail = [] } in
+ p.tail <- cast c;
+ map_filter_i_loop f (succ i) c l
+
+let map_filter_i f l =
+ let c = { head = Obj.magic 0; tail = [] } in
+ map_filter_i_loop f 0 c l;
+ c.tail
let rec filter_with filter l = match filter, l with
| [], [] -> []
@@ -638,12 +688,13 @@ let rec split3 = function
let (rx, ry, rz) = split3 l in (x::rx, y::ry, z::rz)
let firstn n l =
- let rec aux acc = function
- | (0, l) -> List.rev acc
- | (n, (h::t)) -> aux (h::acc) (pred n, t)
+ let rec aux acc n l =
+ match n, l with
+ | 0, _ -> List.rev acc
+ | n, h::t -> aux (h::acc) (pred n) t
| _ -> failwith "firstn"
in
- aux [] (n,l)
+ aux [] n l
let rec last = function
| [] -> failwith "List.last"
diff --git a/lib/cList.mli b/lib/cList.mli
index 19eeb2509..bc8749b4f 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -89,11 +89,17 @@ sig
val map4 : ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list ->
'd list -> 'e list
val filteri : (int -> 'a -> bool) -> 'a list -> 'a list
+ val partitioni : (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
val smartfilter : ('a -> bool) -> 'a list -> 'a list
(** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
[f ai = true], then [smartfilter f l == l] *)
+ val extend : bool list -> 'a -> 'a list -> 'a list
+(** [extend l a [a1..an]] assumes that the number of [true] in [l] is [n];
+ it extends [a1..an] by inserting [a] at the position of [false] in [l] *)
+ val count : ('a -> bool) -> 'a list -> int
+
val index : 'a eq -> 'a -> 'a list -> int
(** [index] returns the 1st index of an element in a list (counting from 1). *)
@@ -119,6 +125,10 @@ sig
val remove_first : ('a -> bool) -> 'a list -> 'a list
(** Remove the first element satisfying a predicate, or raise [Not_found] *)
+ val extract_first : ('a -> bool) -> 'a list -> 'a list * 'a
+ (** Remove and return the first element satisfying a predicate,
+ or raise [Not_found] *)
+
val insert : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
(** Insert at the (first) position so that if the list is ordered wrt to the
total order given as argument, the order is preserved *)
diff --git a/lib/cMap.ml b/lib/cMap.ml
index 665e1a216..ba0873ffa 100644
--- a/lib/cMap.ml
+++ b/lib/cMap.ml
@@ -12,12 +12,20 @@ sig
val compare : t -> t -> int
end
+module type MonadS =
+sig
+ type +'a t
+ val return : 'a -> 'a t
+ val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+end
+
module type S = Map.S
module type ExtS =
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 modify : key -> (key -> 'a -> 'a) -> 'a t -> 'a t
val domain : 'a t -> Set.t
@@ -26,10 +34,17 @@ sig
val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val smartmap : ('a -> 'a) -> 'a t -> 'a t
val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t
+ val height : 'a t -> int
module Unsafe :
sig
val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t
end
+ module Monad(M : MonadS) :
+ sig
+ val fold : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+ val fold_left : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+ val fold_right : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+ end
end
module MapExt (M : Map.OrderedType) :
@@ -43,10 +58,17 @@ sig
val fold_right : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b
val smartmap : ('a -> 'a) -> 'a map -> 'a map
val smartmapi : (M.t -> 'a -> 'a) -> 'a map -> 'a map
+ val height : 'a map -> int
module Unsafe :
sig
val map : (M.t -> 'a -> M.t * 'b) -> 'a map -> 'b map
end
+ module Monad(MS : MonadS) :
+ sig
+ val fold : (M.t -> 'a -> 'b -> 'b MS.t) -> 'a map -> 'b -> 'b MS.t
+ val fold_left : (M.t -> 'a -> 'b -> 'b MS.t) -> 'a map -> 'b -> 'b MS.t
+ val fold_right : (M.t -> 'a -> 'b -> 'b MS.t) -> 'a map -> 'b -> 'b MS.t
+ end
end =
struct
(** This unsafe module is a way to access to the actual implementations of
@@ -148,6 +170,10 @@ struct
if l == l' && r == r' && v == v' then s
else map_inj (MNode (l', k, v', r', h))
+ let height s = match map_prj s with
+ | MEmpty -> 0
+ | MNode (_, _, _, _, h) -> h
+
module Unsafe =
struct
@@ -159,10 +185,34 @@ struct
end
+ module Monad(M : MonadS) =
+ struct
+
+ open M
+
+ let rec fold_left f s accu = match map_prj s with
+ | MEmpty -> return accu
+ | MNode (l, k, v, r, h) ->
+ fold_left f l accu >>= fun accu ->
+ f k v accu >>= fun accu ->
+ fold_left f r accu
+
+ let rec fold_right f s accu = match map_prj s with
+ | MEmpty -> return accu
+ | MNode (l, k, v, r, h) ->
+ fold_right f r accu >>= fun accu ->
+ f k v accu >>= fun accu ->
+ fold_right f l accu
+
+ let fold = fold_left
+
+ end
+
end
module Make(M : Map.OrderedType) =
struct
include Map.Make(M)
include MapExt(M)
+ let get k m = try find k m with Not_found -> assert false
end
diff --git a/lib/cMap.mli b/lib/cMap.mli
index 2f243da83..2838b374e 100644
--- a/lib/cMap.mli
+++ b/lib/cMap.mli
@@ -14,6 +14,13 @@ sig
val compare : t -> t -> int
end
+module type MonadS =
+sig
+ type +'a t
+ val return : 'a -> 'a t
+ val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
+end
+
module type S = Map.S
module type ExtS =
@@ -24,6 +31,9 @@ sig
module Set : CSig.SetS with type elt = key
(** Sets used by the domain function *)
+ 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
(** Same as [add], but expects the key to be present, and thus faster.
@raise Not_found when the key is unbound in the map. *)
@@ -51,6 +61,9 @@ sig
val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t
(** As [mapi] but tries to preserve sharing. *)
+ val height : 'a t -> int
+ (** An indication of the logarithmic size of a map *)
+
module Unsafe :
sig
val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t
@@ -59,6 +72,14 @@ sig
i.e.: for all (k : key) (x : 'a), compare (fst (f k x)) k = 0. *)
end
+ module Monad(M : MonadS) :
+ sig
+ val fold : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+ val fold_left : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+ val fold_right : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t
+ end
+ (** Fold operators parameterized by any monad. *)
+
end
module Make(M : Map.OrderedType) : ExtS with
diff --git a/lib/cSig.mli b/lib/cSig.mli
index e095c82cb..151cfbdca 100644
--- a/lib/cSig.mli
+++ b/lib/cSig.mli
@@ -14,6 +14,8 @@ type ('a, 'b) union = Inl of 'a | Inr of 'b
type 'a until = Stop of 'a | Cont of 'a
(** Used for browsable-until structures. *)
+type (_, _) eq = Refl : ('a, 'a) eq
+
module type SetS =
sig
type elt
@@ -46,6 +48,8 @@ end
(** Redeclaration of OCaml set signature, to preserve compatibility. See OCaml
documentation for more information. *)
+module type EmptyS = sig end
+
module type MapS =
sig
type key
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
new file mode 100644
index 000000000..720f54606
--- /dev/null
+++ b/lib/cWarnings.ml
@@ -0,0 +1,120 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Pp
+
+type status =
+ Disabled | Enabled | AsError
+
+type t = {
+ default : status;
+ category : string;
+ status : status;
+}
+
+let warnings : (string, t) Hashtbl.t = Hashtbl.create 97
+let categories : (string, string list) Hashtbl.t = Hashtbl.create 97
+
+let current_loc = ref Loc.ghost
+let flags = ref "default"
+
+let set_current_loc = (:=) current_loc
+
+let get_flags () = !flags
+
+let add_warning_in_category ~name ~category =
+ let ws =
+ try
+ Hashtbl.find categories category
+ with Not_found -> []
+ in
+ Hashtbl.replace categories category (name::ws)
+
+let create ~name ~category ?(default=Enabled) pp =
+ Hashtbl.add warnings name { default; category; status = default };
+ add_warning_in_category ~name ~category;
+ if default <> Disabled then
+ add_warning_in_category ~name ~category:"default";
+ fun ?loc x -> let w = Hashtbl.find warnings name in
+ match w.status with
+ | Disabled -> ()
+ | AsError ->
+ let loc = Option.default !current_loc loc in
+ CErrors.user_err_loc (loc,"_",pp x)
+ | Enabled ->
+ let msg =
+ pp x ++ spc () ++ str "[" ++ str name ++ str "," ++
+ str category ++ str "]"
+ in
+ let loc = Option.default !current_loc loc in
+ Feedback.msg_warning ~loc msg
+
+let warn_unknown_warning =
+ create ~name:"unknown-warning" ~category:"toplevel"
+ (fun name -> strbrk "Unknown warning name: " ++ str name)
+
+let set_warning_status ~name status =
+ try
+ let w = Hashtbl.find warnings name in
+ Hashtbl.replace warnings name { w with status = status }
+ with Not_found -> warn_unknown_warning name
+
+let reset_default_warnings () =
+ Hashtbl.iter (fun name w ->
+ Hashtbl.replace warnings name { w with status = w.default })
+ warnings
+
+let set_all_warnings_status status =
+ Hashtbl.iter (fun name w ->
+ Hashtbl.replace warnings name { w with status })
+ warnings
+
+let parse_flag s =
+ if String.length s > 1 then
+ match String.get s 0 with
+ | '+' -> (AsError, String.sub s 1 (String.length s - 1))
+ | '-' -> (Disabled, String.sub s 1 (String.length s - 1))
+ | _ -> (Enabled, s)
+ else CErrors.error "Invalid warnings flag"
+
+let rec do_all_keyword = function
+ | [] -> []
+ | (status, name as item) :: items ->
+ if CString.equal name "all" then
+ (set_all_warnings_status status; do_all_keyword items)
+ else item :: do_all_keyword items
+
+let rec do_categories = function
+ | [] -> []
+ | (status, name as item) :: items ->
+ try
+ let names = Hashtbl.find categories name in
+ List.iter (fun name -> set_warning_status name status) names;
+ do_categories items
+ with Not_found -> item :: do_categories items
+
+let rec parse_warnings items =
+ List.iter (fun (status, name) -> set_warning_status ~name status) items
+
+(* For compatibility, we accept "none" *)
+let parse_flags s =
+ if CString.equal s "none" then begin
+ Flags.make_warn false;
+ set_all_warnings_status Disabled
+ end
+ else begin
+ Flags.make_warn true;
+ let reg = Str.regexp "[ ,]+" in
+ let items = List.map parse_flag (Str.split reg s) in
+ let items = do_all_keyword items in
+ let items = do_categories items in
+ parse_warnings items
+ end
+
+let set_flags s =
+ flags := s; reset_default_warnings (); parse_flags s
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
new file mode 100644
index 000000000..351554284
--- /dev/null
+++ b/lib/cWarnings.mli
@@ -0,0 +1,34 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+type status =
+ Disabled | Enabled | AsError
+
+(*
+type 'a repr = {
+ print : 'a -> Pp.std_ppcmds;
+ kind : string;
+ enabled : bool;
+}
+ *)
+
+val set_current_loc : Loc.t -> unit
+
+val create : name:string -> category:string -> ?default:status ->
+ ('a -> Pp.std_ppcmds) -> ?loc:Loc.t -> 'a -> unit
+
+(*
+val emit : 'a t -> 'a -> unit
+
+type any = Any : string * string * 'a repr -> any
+
+val dump : unit -> any list
+ *)
+
+val get_flags : unit -> string
+val set_flags : string -> unit
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 9c9607abd..1e33173ee 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -8,6 +8,7 @@ Hashcons
CSet
CMap
Int
+Dyn
HMap
Option
Store
@@ -20,20 +21,16 @@ Control
Loc
CList
CString
-Serialize
Deque
CObj
CArray
CStack
Util
Stateid
-Feedback
Pp
Ppstyle
-Xml_lexer
-Xml_parser
-Xml_printer
Richpp
+Feedback
CUnix
Envars
Aux_file
diff --git a/lib/dyn.ml b/lib/dyn.ml
index 04b32870a..65d1442ac 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -6,12 +6,68 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
-open Pp
+module type TParam =
+sig
+ type 'a t
+end
+module type PreS =
+sig
+type 'a tag
+type t = Dyn : 'a tag * 'a -> t
+
+val create : string -> 'a tag
+val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
+val repr : 'a tag -> string
+
+type any = Any : 'a tag -> any
+
+val name : string -> any option
+
+module Map(M : TParam) :
+sig
+ type t
+ val empty : t
+ val add : 'a tag -> 'a M.t -> t -> t
+ val remove : 'a tag -> t -> t
+ val find : 'a tag -> t -> 'a M.t
+ val mem : 'a tag -> t -> bool
+
+ type any = Any : 'a tag * 'a M.t -> any
+
+ type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t }
+ val map : map -> t -> t
+
+ val iter : (any -> unit) -> t -> unit
+ val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
+
+end
+
+val dump : unit -> (int * string) list
+
+end
+
+module type S =
+sig
+ include PreS
+
+ module Easy : sig
+ val make_dyn : string -> ('a -> t) * (t -> 'a)
+ val inj : 'a -> 'a tag -> t
+ val prj : t -> 'a tag -> 'a option
+ end
+
+end
+
+module Make(M : CSig.EmptyS) = struct
+module Self : PreS = struct
(* Dynamics, programmed with DANGER !!! *)
-type t = int * Obj.t
+type 'a tag = int
+
+type t = Dyn : 'a tag * 'a -> t
+
+type any = Any : 'a tag -> any
let dyntab = ref (Int.Map.empty : string Int.Map.t)
(** Instead of working with tags as strings, which are costly, we use their
@@ -24,27 +80,69 @@ let create (s : string) =
let () =
if Int.Map.mem hash !dyntab then
let old = Int.Map.find hash !dyntab in
- let msg = str "Dynamic tag collision: " ++ str s ++ str " vs. " ++ str old in
- anomaly ~label:"Dyn.create" msg
+ let () = Printf.eprintf "Dynamic tag collision: %s vs. %s\n%!" s old in
+ assert false
in
let () = dyntab := Int.Map.add hash s !dyntab in
- let infun v = (hash, Obj.repr v) in
- let outfun (nh, rv) =
- if Int.equal hash nh then Obj.magic rv
- else
- anomaly (str "dyn_out: expected " ++ str s)
- in
- (infun, outfun)
+ hash
-let has_tag (s, _) tag =
- let hash = Hashtbl.hash (tag : string) in
- Int.equal s hash
+let eq : 'a 'b. 'a tag -> 'b tag -> ('a, 'b) CSig.eq option =
+ fun h1 h2 -> if Int.equal h1 h2 then Some (Obj.magic CSig.Refl) else None
-let tag (s,_) =
+let repr s =
try Int.Map.find s !dyntab
with Not_found ->
- anomaly (str "Unknown dynamic tag " ++ int s)
+ let () = Printf.eprintf "Unknown dynamic tag %i\n%!" s in
+ assert false
-let pointer_equal (t1,o1) (t2,o2) = t1 = t2 && o1 == o2
+let name s =
+ let hash = Hashtbl.hash s in
+ if Int.Map.mem hash !dyntab then Some (Any hash) else None
let dump () = Int.Map.bindings !dyntab
+
+module Map(M : TParam) =
+struct
+type t = Obj.t M.t Int.Map.t
+let cast : 'a M.t -> 'b M.t = Obj.magic
+let empty = Int.Map.empty
+let add tag v m = Int.Map.add tag (cast v) m
+let remove tag m = Int.Map.remove tag m
+let find tag m = cast (Int.Map.find tag m)
+let mem = Int.Map.mem
+
+type any = Any : 'a tag * 'a M.t -> any
+
+type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t }
+let map f m = Int.Map.mapi f.map m
+
+let iter f m = Int.Map.iter (fun k v -> f (Any (k, v))) m
+let fold f m accu = Int.Map.fold (fun k v accu -> f (Any (k, v)) accu) m accu
+end
+
+end
+include Self
+
+module Easy = struct
+(* now tags are opaque, we can do the trick *)
+let make_dyn (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)) ->
+ match eq tag t with
+ | None -> assert false
+ | Some CSig.Refl -> x
+ in
+ (infun, outfun))
+ (create s)
+
+let inj x tag = Dyn(tag,x)
+let prj : type a. t -> a tag -> a option =
+ fun (Dyn(tag',x)) tag ->
+ match eq tag tag' with
+ | None -> None
+ | Some CSig.Refl -> Some x
+end
+
+end
+
diff --git a/lib/dyn.mli b/lib/dyn.mli
index c040d8b0b..448b11a18 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -6,12 +6,58 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(** Dynamics. Use with extreme care. Not for kids. *)
+(** Dynamically typed values *)
-type t
+module type TParam =
+sig
+ type 'a t
+end
+
+module type S =
+sig
+type 'a tag
+type t = Dyn : 'a tag * 'a -> t
+
+val create : string -> 'a tag
+val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
+val repr : 'a tag -> string
+
+type any = Any : 'a tag -> any
+
+val name : string -> any option
+
+module Map(M : TParam) :
+sig
+ type t
+ val empty : t
+ val add : 'a tag -> 'a M.t -> t -> t
+ val remove : 'a tag -> t -> t
+ val find : 'a tag -> t -> 'a M.t
+ val mem : 'a tag -> t -> bool
+
+ type any = Any : 'a tag * 'a M.t -> any
+
+ type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t }
+ val map : map -> t -> t
+
+ val iter : (any -> unit) -> t -> unit
+ val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r
+
+end
-val create : string -> ('a -> t) * (t -> 'a)
-val tag : t -> string
-val has_tag : t -> string -> bool
-val pointer_equal : t -> t -> bool
val dump : unit -> (int * string) list
+
+module Easy : sig
+
+ (* To create a dynamic type on the fly *)
+ val make_dyn : string -> ('a -> t) * (t -> 'a)
+
+ (* For types declared with the [create] function above *)
+ val inj : 'a -> 'a tag -> t
+ val prj : t -> 'a tag -> 'a option
+end
+
+end
+
+(** FIXME: use OCaml 4.02 generative functors when available *)
+module Make(M : CSig.EmptyS) : S
diff --git a/lib/envars.ml b/lib/envars.ml
index 679e3fdfe..89ce52831 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -146,23 +146,12 @@ let coqpath =
let exe s = s ^ Coq_config.exec_extension
-let guess_camlbin () = which (user_path ()) (exe "ocamlc")
+let guess_ocamlfind () = which (user_path ()) (exe "ocamlfind")
-let camlbin () =
- if !Flags.camlbin_spec then !Flags.camlbin else
- if !Flags.boot then Coq_config.camlbin else
- try guess_camlbin () with Not_found -> Coq_config.camlbin
-
-let ocamlc () = camlbin () / Coq_config.ocamlc
-
-let ocamlopt () = camlbin () / Coq_config.ocamlopt
-
-let camllib () =
- if !Flags.boot then
- Coq_config.camllib
- else
- let _, res = CUnix.run_command (ocamlc () ^ " -where") in
- String.strip res
+let ocamlfind () =
+ if !Flags.ocamlfind_spec then !Flags.ocamlfind else
+ if !Flags.boot then Coq_config.ocamlfind else
+ try guess_ocamlfind () / "ocamlfind" with Not_found -> Coq_config.ocamlfind
(** {2 Camlp4 paths} *)
@@ -173,9 +162,7 @@ let camlp4bin () =
if !Flags.boot then Coq_config.camlp4bin else
try guess_camlp4bin ()
with Not_found ->
- let cb = camlbin () in
- if Sys.file_exists (cb / exe Coq_config.camlp4) then cb
- else Coq_config.camlp4bin
+ Coq_config.camlp4bin
let camlp4 () = camlp4bin () / exe Coq_config.camlp4
@@ -183,7 +170,7 @@ let camlp4lib () =
if !Flags.boot then
Coq_config.camlp4lib
else
- let ex, res = CUnix.run_command (camlp4 () ^ " -where") in
+ let ex, res = CUnix.run_command (ocamlfind () ^ " query " ^ Coq_config.camlp4) in
match ex with
| Unix.WEXITED 0 -> String.strip res
| _ -> "/dev/null"
diff --git a/lib/envars.mli b/lib/envars.mli
index d95b6f099..90a42859b 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -47,17 +47,8 @@ val coqroot : string
the order it gets added to the search path. *)
val coqpath : string list
-(** [camlbin ()] is the path to the ocaml binaries. *)
-val camlbin : unit -> string
-
-(** [camllib ()] is the path to the ocaml standard library. *)
-val camllib : unit -> string
-
-(** [ocamlc ()] is the ocaml bytecode compiler that compiled this Coq. *)
-val ocamlc : unit -> string
-
-(** [ocamlc ()] is the ocaml native compiler that compiled this Coq. *)
-val ocamlopt : unit -> string
+(** [camlbin ()] is the path to the ocamlfind binary. *)
+val ocamlfind : unit -> string
(** [camlp4bin ()] is the path to the camlp4 binary. *)
val camlp4bin : unit -> string
diff --git a/lib/explore.ml b/lib/explore.ml
index 587db1156..aa7bddf2b 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -27,7 +27,7 @@ module Make = functor(S : SearchProblem) -> struct
| [i] -> int i
| i :: l -> pp_rec l ++ str "." ++ int i
in
- msg_debug (h 0 (pp_rec p) ++ pp)
+ Feedback.msg_debug (h 0 (pp_rec p) ++ pp)
(*s Depth first search. *)
diff --git a/lib/feedback.ml b/lib/feedback.ml
index cce0c6bc6..dd1ca2af3 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -7,51 +7,14 @@
(************************************************************************)
open Xml_datatype
-open Serialize
-type message_level =
- | Debug of string
+type level =
+ | Debug
| Info
| Notice
| Warning
| Error
-type message = {
- message_level : message_level;
- message_content : string;
-}
-
-let of_message_level = function
- | Debug s ->
- Serialize.constructor "message_level" "debug" [Xml_datatype.PCData s]
- | Info -> Serialize.constructor "message_level" "info" []
- | Notice -> Serialize.constructor "message_level" "notice" []
- | Warning -> Serialize.constructor "message_level" "warning" []
- | Error -> Serialize.constructor "message_level" "error" []
-let to_message_level =
- Serialize.do_match "message_level" (fun s args -> match s with
- | "debug" -> Debug (Serialize.raw_string args)
- | "info" -> Info
- | "notice" -> Notice
- | "warning" -> Warning
- | "error" -> Error
- | _ -> raise Serialize.Marshal_error)
-
-let of_message msg =
- let lvl = of_message_level msg.message_level in
- let content = Serialize.of_string msg.message_content in
- Xml_datatype.Element ("message", [], [lvl; content])
-let to_message xml = match xml with
- | Xml_datatype.Element ("message", [], [lvl; content]) -> {
- message_level = to_message_level lvl;
- message_content = Serialize.to_string content }
- | _ -> raise Serialize.Marshal_error
-
-let is_message = function
- | Xml_datatype.Element ("message", _, _) -> true
- | _ -> false
-
-
type edit_id = int
type state_id = Stateid.t
type edit_or_state_id = Edit of edit_id | State of state_id
@@ -61,7 +24,6 @@ type feedback_content =
| Processed
| Incomplete
| Complete
- | ErrorMsg of Loc.t * string
| ProcessingIn of string
| InProgress of int
| WorkerStatus of string * string
@@ -71,8 +33,10 @@ type feedback_content =
| GlobDef of Loc.t * string * string * string
| FileDependency of string option * string
| FileLoaded of string * string
+ (* Extra metadata *)
| Custom of Loc.t * string * xml
- | Message of message
+ (* Generic messages *)
+ | Message of level * Loc.t option * Richpp.richpp
type feedback = {
id : edit_or_state_id;
@@ -80,92 +44,135 @@ type feedback = {
route : route_id;
}
-let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
- | "addedaxiom", _ -> AddedAxiom
- | "processed", _ -> Processed
- | "processingin", [where] -> ProcessingIn (to_string where)
- | "incomplete", _ -> Incomplete
- | "complete", _ -> Complete
- | "globref", [loc; filepath; modpath; ident; ty] ->
- GlobRef(to_loc loc, to_string filepath,
- to_string modpath, to_string ident, to_string ty)
- | "globdef", [loc; ident; secpath; ty] ->
- GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty)
- | "errormsg", [loc; s] -> ErrorMsg (to_loc loc, to_string s)
- | "inprogress", [n] -> InProgress (to_int n)
- | "workerstatus", [ns] ->
- let n, s = to_pair to_string to_string ns in
- WorkerStatus(n,s)
- | "goals", [loc;s] -> Goals (to_loc loc, to_string s)
- | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x)
- | "filedependency", [from; dep] ->
- FileDependency (to_option to_string from, to_string dep)
- | "fileloaded", [dirpath; filename] ->
- FileLoaded (to_string dirpath, to_string filename)
- | "message", [m] -> Message (to_message m)
- | _ -> raise Marshal_error)
-let of_feedback_content = function
- | AddedAxiom -> constructor "feedback_content" "addedaxiom" []
- | Processed -> constructor "feedback_content" "processed" []
- | ProcessingIn where ->
- constructor "feedback_content" "processingin" [of_string where]
- | Incomplete -> constructor "feedback_content" "incomplete" []
- | Complete -> constructor "feedback_content" "complete" []
- | GlobRef(loc, filepath, modpath, ident, ty) ->
- constructor "feedback_content" "globref" [
- of_loc loc;
- of_string filepath;
- of_string modpath;
- of_string ident;
- of_string ty ]
- | GlobDef(loc, ident, secpath, ty) ->
- constructor "feedback_content" "globdef" [
- of_loc loc;
- of_string ident;
- of_string secpath;
- of_string ty ]
- | ErrorMsg(loc, s) ->
- constructor "feedback_content" "errormsg" [of_loc loc; of_string s]
- | InProgress n -> constructor "feedback_content" "inprogress" [of_int n]
- | WorkerStatus(n,s) ->
- constructor "feedback_content" "workerstatus"
- [of_pair of_string of_string (n,s)]
- | Goals (loc,s) ->
- constructor "feedback_content" "goals" [of_loc loc;of_string s]
- | Custom (loc, name, x) ->
- constructor "feedback_content" "custom" [of_loc loc; of_string name; x]
- | FileDependency (from, depends_on) ->
- constructor "feedback_content" "filedependency" [
- of_option of_string from;
- of_string depends_on]
- | FileLoaded (dirpath, filename) ->
- constructor "feedback_content" "fileloaded" [
- of_string dirpath;
- of_string filename ]
- | Message m -> constructor "feedback_content" "message" [ of_message m ]
-
-let of_edit_or_state_id = function
- | Edit id -> ["object","edit"], of_edit_id id
- | State id -> ["object","state"], Stateid.to_xml id
-
-let of_feedback msg =
- let content = of_feedback_content msg.contents in
- let obj, id = of_edit_or_state_id msg.id in
- let route = string_of_int msg.route in
- Element ("feedback", obj @ ["route",route], [id;content])
-let to_feedback xml = match xml with
- | Element ("feedback", ["object","edit";"route",route], [id;content]) -> {
- id = Edit(to_edit_id id);
- route = int_of_string route;
- contents = to_feedback_content content }
- | Element ("feedback", ["object","state";"route",route], [id;content]) -> {
- id = State(Stateid.of_xml id);
- route = int_of_string route;
- contents = to_feedback_content content }
- | _ -> raise Marshal_error
-
-let is_feedback = function
- | Element ("feedback", _, _) -> true
- | _ -> false
-
let default_route = 0
+
+(** Feedback and logging *)
+open Pp
+open Pp_control
+
+type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit
+
+let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ())
+let msgnl strm = msgnl_with !std_ft strm
+
+(* XXX: This is really painful! *)
+module Emacs = struct
+
+ (* Special chars for emacs, to detect warnings inside goal output *)
+ let emacs_quote_start = String.make 1 (Char.chr 254)
+ let emacs_quote_end = String.make 1 (Char.chr 255)
+
+ let emacs_quote_err g =
+ hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end)
+
+ let emacs_quote_info_start = "<infomsg>"
+ let emacs_quote_info_end = "</infomsg>"
+
+ let emacs_quote_info g =
+ hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end)
+
+end
+
+open Emacs
+
+let dbg_str = str "Debug:" ++ spc ()
+let info_str = mt ()
+let warn_str = str "Warning:" ++ spc ()
+let err_str = str "Error:" ++ spc ()
+
+let make_body quoter info ?loc s =
+ let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
+ quoter (hov 0 (loc ++ info ++ s))
+
+(* Generic logger *)
+let gen_logger dbg err ?loc level msg = match level with
+ | Debug -> msgnl (make_body dbg dbg_str ?loc msg)
+ | Info -> msgnl (make_body dbg info_str ?loc msg)
+ (* XXX: What to do with loc here? *)
+ | Notice -> msgnl msg
+ | Warning -> Flags.if_warn (fun () ->
+ msgnl_with !err_ft (make_body err warn_str ?loc msg)) ()
+ | Error -> msgnl_with !err_ft (make_body err err_str ?loc msg)
+
+(** Standard loggers *)
+let std_logger = gen_logger (fun x -> x) (fun x -> x)
+
+(* Color logger *)
+let color_terminal_logger ?loc level strm =
+ let msg = Ppstyle.color_msg in
+ match level with
+ | Debug -> msg ?loc ~header:("Debug", Ppstyle.debug_tag) !std_ft strm
+ | Info -> msg ?loc !std_ft strm
+ | Notice -> msg ?loc !std_ft strm
+ | Warning -> Flags.if_warn (fun () ->
+ msg ?loc ~header:("Warning", Ppstyle.warning_tag) !err_ft strm) ()
+ | Error -> msg ?loc ~header:("Error", Ppstyle.error_tag) !err_ft strm
+
+(* Rules for emacs:
+ - Debug/info: emacs_quote_info
+ - Warning/Error: emacs_quote_err
+ - Notice: unquoted
+ *)
+let emacs_logger = gen_logger emacs_quote_info emacs_quote_err
+
+let logger = ref std_logger
+let set_logger l = logger := l
+
+let msg_info ?loc x = !logger ?loc Info x
+let msg_notice ?loc x = !logger ?loc Notice x
+let msg_warning ?loc x = !logger ?loc Warning x
+let msg_error ?loc x = !logger ?loc Error x
+let msg_debug ?loc x = !logger ?loc Debug x
+
+(** Feeders *)
+let feeders = ref []
+let add_feeder f = feeders := f :: !feeders
+
+let debug_feeder = function
+ | { contents = Message (Debug, loc, pp) } ->
+ msg_debug ?loc (Pp.str (Richpp.raw_print pp))
+ | _ -> ()
+
+let feedback_id = ref (Edit 0)
+let feedback_route = ref default_route
+
+let set_id_for_feedback ?(route=default_route) i =
+ feedback_id := i; feedback_route := route
+
+let feedback ?id ?route what =
+ let m = {
+ contents = what;
+ route = Option.default !feedback_route route;
+ id = Option.default !feedback_id id;
+ } in
+ List.iter (fun f -> f m) !feeders
+
+let feedback_logger ?loc lvl msg =
+ feedback ~route:!feedback_route ~id:!feedback_id
+ (Message (lvl, loc, Richpp.richpp_of_pp msg))
+
+(* Output to file *)
+let ft_logger old_logger ft ?loc level mesg =
+ let id x = x in
+ match level with
+ | Debug -> msgnl_with ft (make_body id dbg_str mesg)
+ | Info -> msgnl_with ft (make_body id info_str mesg)
+ | Notice -> msgnl_with ft mesg
+ | Warning -> old_logger ?loc level mesg
+ | Error -> old_logger ?loc level mesg
+
+let with_output_to_file fname func input =
+ let old_logger = !logger in
+ let channel = open_out (String.concat "." [fname; "out"]) in
+ logger := ft_logger old_logger (Format.formatter_of_out_channel channel);
+ try
+ let output = func input in
+ logger := old_logger;
+ close_out channel;
+ output
+ with reraise ->
+ let reraise = Backtrace.add_backtrace reraise in
+ logger := old_logger;
+ close_out channel;
+ Exninfo.iraise reraise
+
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 162867626..48b1c19a6 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -9,27 +9,19 @@
open Xml_datatype
(* Old plain messages (used to be in Pp) *)
-type message_level =
- | Debug of string
+type level =
+ | Debug
| Info
| Notice
| Warning
| Error
-type message = {
- message_level : message_level;
- message_content : string;
-}
-
-val of_message : message -> xml
-val to_message : xml -> message
-val is_message : xml -> bool
-
(** Coq "semantic" infos obtained during parsing/execution *)
type edit_id = int
type state_id = Stateid.t
type edit_or_state_id = Edit of edit_id | State of state_id
+
type route_id = int
val default_route : route_id
@@ -39,7 +31,6 @@ type feedback_content =
| Processed
| Incomplete
| Complete
- | ErrorMsg of Loc.t * string
(* STM optional data *)
| ProcessingIn of string
| InProgress of int
@@ -53,16 +44,92 @@ type feedback_content =
| FileLoaded of string * string
(* Extra metadata *)
| Custom of Loc.t * string * xml
- (* Old generic messages *)
- | Message of message
+ (* Generic messages *)
+ | Message of level * Loc.t option * Richpp.richpp
type feedback = {
- id : edit_or_state_id; (* The document part concerned *)
+ id : edit_or_state_id; (* The document part concerned *)
contents : feedback_content; (* The payload *)
- route : route_id; (* Extra routing info *)
+ route : route_id; (* Extra routing info *)
}
-val of_feedback : feedback -> xml
-val to_feedback : xml -> feedback
-val is_feedback : xml -> bool
+(** {6 Feedback sent, even asynchronously, to the user interface} *)
+
+(** Moved here from pp.ml *)
+
+(* Morally the parser gets a string and an edit_id, and gives back an AST.
+ * Feedbacks during the parsing phase are attached to this edit_id.
+ * The interpreter assignes an exec_id to the ast, and feedbacks happening
+ * during interpretation are attached to the exec_id.
+ * Only one among state_id and edit_id can be provided. *)
+
+(** A [logger] takes a level plus a pretty printing doc and logs it *)
+type logger = ?loc:Loc.t -> level -> Pp.std_ppcmds -> unit
+
+(** [set_logger l] makes the [msg_*] to use [l] for logging *)
+val set_logger : logger -> unit
+
+(** [std_logger] standard logger to [stdout/stderr] *)
+val std_logger : logger
+
+val color_terminal_logger : logger
+(* This logger will apply the proper {!Pp_style} tags, and in
+ particular use the formatters {!Pp_control.std_ft} and
+ {!Pp_control.err_ft} to display those messages. Be careful this is
+ not compatible with the Emacs mode! *)
+
+(** [feedback_logger] will produce feedback messages instead IO events *)
+val feedback_logger : logger
+val emacs_logger : logger
+
+
+(** [add_feeder] feeders observe the feedback *)
+val add_feeder : (feedback -> unit) -> unit
+
+(** Prints feedback messages of kind Message(Debug,_) using msg_debug *)
+val debug_feeder : feedback -> unit
+
+(** [feedback ?id ?route fb] produces feedback fb, with [route] and
+ [id] set appropiatedly, if absent, it will use the defaults set by
+ [set_id_for_feedback] *)
+val feedback :
+ ?id:edit_or_state_id -> ?route:route_id -> feedback_content -> unit
+
+(** [set_id_for_feedback route id] Set the defaults for feedback *)
+val set_id_for_feedback : ?route:route_id -> edit_or_state_id -> unit
+
+(** [with_output_to_file file f x] executes [f x] with logging
+ redirected to a file [file] *)
+val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
+
+(** {6 output functions}
+
+[msg_notice] do not put any decoration on output by default. If
+possible don't mix it with goal output (prefer msg_info or
+msg_warning) so that interfaces can dispatch outputs easily. Once all
+interfaces use the xml-like protocol this constraint can be
+relaxed. *)
+(* Should we advertise these functions more? Should they be the ONLY
+ allowed way to output something? *)
+
+val msg_info : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+(** Message that displays information, usually in verbose mode, such as [Foobar
+ is defined] *)
+
+val msg_notice : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+(** Message that should be displayed, such as [Print Foo] or [Show Bar]. *)
+
+val msg_warning : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+(** Message indicating that something went wrong, but without serious
+ consequences. *)
+
+val msg_error : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+(** Message indicating that something went really wrong, though still
+ recoverable; otherwise an exception would have been raised. *)
+
+val msg_debug : ?loc:Loc.t -> Pp.std_ppcmds -> unit
+(** For debugging purposes *)
+
+
+
diff --git a/lib/flags.ml b/lib/flags.ml
index 2c23ec984..65873e521 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -47,6 +47,7 @@ let batch_mode = ref false
type compilation_mode = BuildVo | BuildVio | Vio2Vo
let compilation_mode = ref BuildVo
+let compilation_output_name = ref None
let test_mode = ref false
@@ -68,11 +69,15 @@ 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 [ "par" ; "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 debug = ref false
let in_debugger = ref false
@@ -103,25 +108,33 @@ let we_are_parsing = ref false
(* Current means no particular compatibility consideration.
For correct comparisons, this constructor should remain the last one. *)
-type compat_version = V8_2 | V8_3 | V8_4 | Current
+type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current
let compat_version = ref Current
-let version_strictly_greater v = match !compat_version, v with
-| V8_2, (V8_2 | V8_3 | V8_4 | Current) -> false
-| V8_3, (V8_3 | V8_4 | Current) -> false
-| V8_4, (V8_4 | Current) -> false
-| Current, Current -> false
-| V8_3, V8_2 -> true
-| V8_4, (V8_2 | V8_3) -> true
-| Current, (V8_2 | V8_3 | V8_4) -> true
-
+let version_compare v1 v2 = match v1, v2 with
+| V8_2, V8_2 -> 0
+| V8_2, (V8_3 | V8_4 | V8_5 | Current) -> -1
+| V8_3, V8_2 -> 1
+| V8_3, V8_3 -> 0
+| V8_3, (V8_4 | V8_5 | Current) -> -1
+| V8_4, (V8_2 | V8_3) -> 1
+| V8_4, V8_4 -> 0
+| V8_4, (V8_5 | Current) -> -1
+| V8_5, (V8_2 | V8_3 | V8_4) -> 1
+| V8_5, V8_5 -> 0
+| V8_5, Current -> -1
+| Current, Current -> 0
+| Current, (V8_2 | V8_3 | V8_4 | V8_5) -> 1
+
+let version_strictly_greater v = version_compare !compat_version v > 0
let version_less_or_equal v = not (version_strictly_greater v)
let pr_version = function
| V8_2 -> "8.2"
| V8_3 -> "8.3"
| V8_4 -> "8.4"
+ | V8_5 -> "8.5"
| Current -> "current"
(* Translate *)
@@ -164,7 +177,7 @@ let make_polymorphic_flag b =
let program_mode = ref false
let is_program_mode () = !program_mode
-let warn = ref false
+let warn = ref true
let make_warn flag = warn := flag; ()
let if_warn f x = if !warn then f x
@@ -195,9 +208,9 @@ let is_standard_doc_url url =
let coqlib_spec = ref false
let coqlib = ref "(not initialized yet)"
-(* Options for changing camlbin (used by coqmktop) *)
-let camlbin_spec = ref false
-let camlbin = ref Coq_config.camlbin
+(* 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
@@ -217,6 +230,8 @@ let native_compiler = ref false
let print_mod_uid = ref false
let tactic_context_compat = ref false
+let profile_ltac = ref false
+let profile_ltac_cutoff = ref 2.0
let dump_bytecode = ref false
let set_dump_bytecode = (:=) dump_bytecode
diff --git a/lib/flags.mli b/lib/flags.mli
index 69caad5b6..9dc0c9c04 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -14,6 +14,7 @@ val load_init : bool ref
val batch_mode : bool ref
type compilation_mode = BuildVo | BuildVio | Vio2Vo
val compilation_mode : compilation_mode ref
+val compilation_output_name : string option ref
val test_mode : bool ref
@@ -34,6 +35,10 @@ 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 debug : bool ref
val in_debugger : bool ref
@@ -57,8 +62,9 @@ val raw_print : bool ref
val record_print : bool ref
val univ_print : bool ref
-type compat_version = V8_2 | V8_3 | V8_4 | Current
+type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current
val compat_version : compat_version ref
+val version_compare : compat_version -> compat_version -> int
val version_strictly_greater : compat_version -> bool
val version_less_or_equal : compat_version -> bool
val pr_version : compat_version -> string
@@ -123,8 +129,8 @@ val coqlib_spec : bool ref
val coqlib : string ref
(** Options for specifying where OCaml binaries reside *)
-val camlbin_spec : bool ref
-val camlbin : string ref
+val ocamlfind_spec : bool ref
+val ocamlfind : string ref
val camlp4bin_spec : bool ref
val camlp4bin : string ref
@@ -143,6 +149,9 @@ 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
+
(** Dump the bytecode after compilation (for debugging purposes) *)
val dump_bytecode : bool ref
val set_dump_bytecode : bool -> unit
diff --git a/lib/future.ml b/lib/future.ml
index e8f33db5e..ea0382a63 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -7,8 +7,9 @@
(************************************************************************)
(* To deal with side effects we have to save/restore the system state *)
-let freeze = ref (fun () -> assert false : unit -> Dyn.t)
-let unfreeze = ref (fun _ -> () : Dyn.t -> unit)
+type freeze
+let freeze = ref (fun () -> assert false : unit -> freeze)
+let unfreeze = ref (fun _ -> () : freeze -> unit)
let set_freeze f g = freeze := f; unfreeze := g
let not_ready_msg = ref (fun name ->
@@ -29,10 +30,10 @@ let customize_not_here_msg f = not_here_msg := f
exception NotReady of string
exception NotHere of string
-let _ = Errors.register_handler (function
+let _ = CErrors.register_handler (function
| NotReady name -> !not_ready_msg name
| NotHere name -> !not_here_msg name
- | _ -> raise Errors.Unhandled)
+ | _ -> raise CErrors.Unhandled)
type fix_exn = Exninfo.iexn -> Exninfo.iexn
let id x = prerr_endline "Future: no fix_exn.\nYou have probably created a Future.computation from a value without passing the ~fix_exn argument. You probably want to chain with an already existing future instead."; x
@@ -58,7 +59,7 @@ type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computat
and 'a comp =
| Delegated of (unit -> unit)
| Closure of (unit -> 'a)
- | Val of 'a * Dyn.t option
+ | Val of 'a * freeze option
| Exn of Exninfo.iexn (* Invariant: this exception is always "fixed" as in fix_exn *)
and 'a comput =
@@ -135,7 +136,7 @@ let rec compute ~pure ck : 'a value =
let state = if pure then None else Some (!freeze ()) in
c := Val (data, state); `Val data
with e ->
- let e = Errors.push e in
+ let e = CErrors.push e in
let e = fix_exn e in
match e with
| (NotReady _, _) -> `Exn e
@@ -155,9 +156,9 @@ let chain ~pure ck f =
| Val (v, Some state) -> Closure (fun () -> !unfreeze state; f v)
| Val (v, None) ->
match !ck with
- | Finished _ -> Errors.anomaly(Pp.str
+ | Finished _ -> CErrors.anomaly(Pp.str
"Future.chain ~pure:false call on an already joined computation")
- | Ongoing _ -> Errors.anomaly(Pp.strbrk(
+ | Ongoing _ -> CErrors.anomaly(Pp.strbrk(
"Future.chain ~pure:false call on a pure computation. "^
"This can happen if the computation was initial created with "^
"Future.from_val or if it was Future.chain ~pure:true with a "^
@@ -169,7 +170,7 @@ let replace kx y =
let _, _, _, x = get kx in
match !x with
| Exn _ -> x := Closure (fun () -> force ~pure:false y)
- | _ -> Errors.anomaly
+ | _ -> CErrors.anomaly
(Pp.str "A computation can be replaced only if is_exn holds")
let purify f x =
@@ -179,13 +180,13 @@ let purify f x =
!unfreeze state;
v
with e ->
- let e = Errors.push e in !unfreeze state; Exninfo.iraise e
+ let e = CErrors.push e in !unfreeze state; Exninfo.iraise e
let transactify f x =
let state = !freeze () in
try f x
with e ->
- let e = Errors.push e in !unfreeze state; Exninfo.iraise e
+ let e = CErrors.push e in !unfreeze state; Exninfo.iraise e
let purify_future f x = if is_over x then f x else purify f x
let compute x = purify_future (compute ~pure:false) x
@@ -212,7 +213,7 @@ let map2 ?greedy f x l =
let xi = chain ?greedy ~pure:true x (fun x ->
try List.nth x i
with Failure _ | Invalid_argument _ ->
- Errors.anomaly (Pp.str "Future.map2 length mismatch")) in
+ CErrors.anomaly (Pp.str "Future.map2 length mismatch")) in
f xi y) 0 l
let print f kx =
diff --git a/lib/future.mli b/lib/future.mli
index 58f0a71ad..114c59176 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -157,10 +157,11 @@ val transactify : ('a -> 'b) -> 'a -> 'b
(** Debug: print a computation given an inner printing function. *)
val print : ('a -> Pp.std_ppcmds) -> 'a computation -> Pp.std_ppcmds
+type freeze
(* These functions are needed to get rid of side effects.
Thy are set for the outermos layer of the system, since they have to
deal with the whole system state. *)
-val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit
+val set_freeze : (unit -> freeze) -> (freeze -> unit) -> unit
val customize_not_ready_msg : (string -> Pp.std_ppcmds) -> unit
val customize_not_here_msg : (string -> Pp.std_ppcmds) -> unit
diff --git a/lib/genarg.ml b/lib/genarg.ml
index cba54c114..05c828d5f 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -9,168 +9,160 @@
open Pp
open Util
-type argument_type =
- (* Basic types *)
- | IntOrVarArgType
- | IdentArgType
- | VarArgType
- (* Specific types *)
- | GenArgType
- | ConstrArgType
- | ConstrMayEvalArgType
- | QuantHypArgType
- | OpenConstrArgType
- | ConstrWithBindingsArgType
- | BindingsArgType
- | RedExprArgType
- | ListArgType of argument_type
- | OptArgType of argument_type
- | PairArgType of argument_type * argument_type
- | ExtraArgType of string
-
-let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
-| IntOrVarArgType, IntOrVarArgType -> true
-| IdentArgType, IdentArgType -> true
-| VarArgType, VarArgType -> true
-| GenArgType, GenArgType -> true
-| ConstrArgType, ConstrArgType -> true
-| ConstrMayEvalArgType, ConstrMayEvalArgType -> true
-| QuantHypArgType, QuantHypArgType -> true
-| OpenConstrArgType, OpenConstrArgType -> true
-| ConstrWithBindingsArgType, ConstrWithBindingsArgType -> true
-| BindingsArgType, BindingsArgType -> true
-| RedExprArgType, RedExprArgType -> true
-| ListArgType arg1, ListArgType arg2 -> argument_type_eq arg1 arg2
-| OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2
-| PairArgType (arg1l, arg1r), PairArgType (arg2l, arg2r) ->
- argument_type_eq arg1l arg2l && argument_type_eq arg1r arg2r
-| ExtraArgType s1, ExtraArgType s2 -> CString.equal s1 s2
-| _ -> false
-
-let rec pr_argument_type = function
-| IntOrVarArgType -> str "int_or_var"
-| IdentArgType -> str "ident"
-| VarArgType -> str "var"
-| GenArgType -> str "genarg"
-| ConstrArgType -> str "constr"
-| ConstrMayEvalArgType -> str "constr_may_eval"
-| QuantHypArgType -> str "qhyp"
-| OpenConstrArgType -> str "open_constr"
-| ConstrWithBindingsArgType -> str "constr_with_bindings"
-| BindingsArgType -> str "bindings"
-| RedExprArgType -> str "redexp"
-| ListArgType t -> pr_argument_type t ++ spc () ++ str "list"
-| OptArgType t -> pr_argument_type t ++ spc () ++ str "opt"
-| PairArgType (t1, t2) ->
- str "("++ pr_argument_type t1 ++ spc () ++
- str "*" ++ spc () ++ pr_argument_type t2 ++ str ")"
-| ExtraArgType s -> str s
-
-type ('raw, 'glob, 'top) genarg_type = argument_type
+module ArgT =
+struct
+ module DYN = Dyn.Make(struct end)
+ module Map = DYN.Map
+ type ('a, 'b, 'c) tag = ('a * 'b * 'c) DYN.tag
+ type any = Any : ('a, 'b, 'c) tag -> any
+ let eq = DYN.eq
+ let repr = DYN.repr
+ let create = DYN.create
+ let name s = match DYN.name s with
+ | None -> None
+ | Some (DYN.Any t) ->
+ Some (Any (Obj.magic t)) (** All created tags are made of triples *)
+end
+
+type (_, _, _) genarg_type =
+| ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type
+| ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
+| OptArg : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
+| PairArg : ('a1, 'b1, 'c1) genarg_type * ('a2, 'b2, 'c2) genarg_type ->
+ ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type
+
+type argument_type = ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type
+
+let rec genarg_type_eq : type a1 a2 b1 b2 c1 c2.
+ (a1, b1, c1) genarg_type -> (a2, b2, c2) genarg_type ->
+ (a1 * b1 * c1, a2 * b2 * c2) CSig.eq option =
+fun t1 t2 -> match t1, t2 with
+| ExtraArg t1, ExtraArg t2 -> ArgT.eq t1 t2
+| ListArg t1, ListArg t2 ->
+ begin match genarg_type_eq t1 t2 with
+ | None -> None
+ | Some Refl -> Some Refl
+ end
+| OptArg t1, OptArg t2 ->
+ begin match genarg_type_eq t1 t2 with
+ | None -> None
+ | Some Refl -> Some Refl
+ end
+| PairArg (t1, u1), PairArg (t2, u2) ->
+ begin match genarg_type_eq t1 t2 with
+ | None -> None
+ | Some Refl ->
+ match genarg_type_eq u1 u2 with
+ | None -> None
+ | Some Refl -> Some Refl
+ end
+| _ -> None
+
+let rec pr_genarg_type : type a b c. (a, b, c) genarg_type -> std_ppcmds = function
+| ListArg t -> pr_genarg_type t ++ spc () ++ str "list"
+| OptArg t -> pr_genarg_type t ++ spc () ++ str "opt"
+| PairArg (t1, t2) ->
+ str "("++ pr_genarg_type t1 ++ spc () ++
+ str "*" ++ spc () ++ pr_genarg_type t2 ++ str ")"
+| ExtraArg s -> str (ArgT.repr s)
+
+let argument_type_eq arg1 arg2 = match arg1, arg2 with
+| ArgumentType t1, ArgumentType t2 ->
+ match genarg_type_eq t1 t2 with
+ | None -> false
+ | Some Refl -> true
+
+let pr_argument_type (ArgumentType t) = pr_genarg_type t
type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
(** Alias for concision *)
(* Dynamics but tagged by a type expression *)
-type rlevel
-type glevel
-type tlevel
+type rlevel = [ `rlevel ]
+type glevel = [ `glevel ]
+type tlevel = [ `tlevel ]
+
+type (_, _) abstract_argument_type =
+| Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type
+| Glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type
+| Topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type
+
+type 'l generic_argument = GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument
-type 'a generic_argument = argument_type * Obj.t
type raw_generic_argument = rlevel generic_argument
type glob_generic_argument = glevel generic_argument
type typed_generic_argument = tlevel generic_argument
-let rawwit t = t
-let glbwit t = t
-let topwit t = t
-
-let wit_list t = ListArgType t
+let rawwit t = Rawwit t
+let glbwit t = Glbwit t
+let topwit t = Topwit t
+
+let wit_list t = ListArg t
+
+let wit_opt t = OptArg t
+
+let wit_pair t1 t2 = PairArg (t1, t2)
+
+let in_gen t o = GenArg (t, o)
+
+let abstract_argument_type_eq :
+ type a b l. (a, l) abstract_argument_type -> (b, l) abstract_argument_type -> (a, b) CSig.eq option =
+ fun t1 t2 -> match t1, t2 with
+ | Rawwit t1, Rawwit t2 ->
+ begin match genarg_type_eq t1 t2 with
+ | None -> None
+ | Some Refl -> Some Refl
+ end
+ | Glbwit t1, Glbwit t2 ->
+ begin match genarg_type_eq t1 t2 with
+ | None -> None
+ | Some Refl -> Some Refl
+ end
+ | Topwit t1, Topwit t2 ->
+ begin match genarg_type_eq t1 t2 with
+ | None -> None
+ | Some Refl -> Some Refl
+ end
+
+let out_gen (type a) (type l) (t : (a, l) abstract_argument_type) (o : l generic_argument) : a =
+ let GenArg (t', v) = o in
+ match abstract_argument_type_eq t t' with
+ | None -> failwith "out_gen"
+ | Some Refl -> v
+
+let has_type (GenArg (t, v)) u = match abstract_argument_type_eq t u with
+| None -> false
+| Some _ -> true
+
+let unquote : type l. (_, l) abstract_argument_type -> _ = function
+| Rawwit t -> ArgumentType t
+| Glbwit t -> ArgumentType t
+| Topwit t -> ArgumentType t
+
+let genarg_tag (GenArg (t, _)) = unquote t
-let wit_opt t = OptArgType t
-
-let wit_pair t1 t2 = PairArgType (t1,t2)
-
-let in_gen t o = (t,Obj.repr o)
-let out_gen t (t',o) = if argument_type_eq t t' then Obj.magic o else failwith "out_gen"
-let genarg_tag (s,_) = s
-
-let has_type (t, v) u = argument_type_eq t u
-
-let unquote x = x
-
-type ('a,'b) abstract_argument_type = argument_type
type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type
type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type
type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type
-type ('a, 'b, 'c, 'l) cast = Obj.t
-
-let raw = Obj.obj
-let glb = Obj.obj
-let top = Obj.obj
-
-type ('r, 'l) unpacker =
- { unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c, 'l) cast -> 'r }
-
-let unpack pack (t, obj) = pack.unpacker t (Obj.obj obj)
-
-(** Type transformers *)
-
-type ('r, 'l) list_unpacker =
- { list_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type ->
- ('a list, 'b list, 'c list, 'l) cast -> 'r }
-
-let list_unpack pack (t, obj) = match t with
-| ListArgType t -> pack.list_unpacker t (Obj.obj obj)
-| _ -> failwith "out_gen"
-
-type ('r, 'l) opt_unpacker =
- { opt_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type ->
- ('a option, 'b option, 'c option, 'l) cast -> 'r }
-
-let opt_unpack pack (t, obj) = match t with
-| OptArgType t -> pack.opt_unpacker t (Obj.obj obj)
-| _ -> failwith "out_gen"
-
-type ('r, 'l) pair_unpacker =
- { pair_unpacker : 'a1 'a2 'b1 'b2 'c1 'c2.
- ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type ->
- (('a1 * 'a2), ('b1 * 'b2), ('c1 * 'c2), 'l) cast -> 'r }
-
-let pair_unpack pack (t, obj) = match t with
-| PairArgType (t1, t2) -> pack.pair_unpacker t1 t2 (Obj.obj obj)
-| _ -> failwith "out_gen"
-
(** Creating args *)
-let (arg0_map : Obj.t option String.Map.t ref) = ref String.Map.empty
+module type Param = sig type ('raw, 'glb, 'top) t end
+module ArgMap(M : Param) =
+struct
+ type _ pack = Pack : ('raw, 'glb, 'top) M.t -> ('raw * 'glb * 'top) pack
+ include ArgT.Map(struct type 'a t = 'a pack end)
+end
-let create_arg opt name =
- if String.Map.mem name !arg0_map then
- Errors.anomaly (str "generic argument already declared: " ++ str name)
- else
- let () = arg0_map := String.Map.add name (Obj.magic opt) !arg0_map in
- ExtraArgType name
+let create_arg name =
+ match ArgT.name name with
+ | None -> ExtraArg (ArgT.create name)
+ | Some _ ->
+ CErrors.anomaly (str "generic argument already declared: " ++ str name)
let make0 = create_arg
-let default_empty_value t =
- let rec aux = function
- | ListArgType _ -> Some (Obj.repr [])
- | OptArgType _ -> Some (Obj.repr None)
- | PairArgType(t1, t2) ->
- (match aux t1, aux t2 with
- | Some v1, Some v2 -> Some (Obj.repr (v1, v2))
- | _ -> None)
- | ExtraArgType s ->
- String.Map.find s !arg0_map
- | _ -> None in
- match aux t with
- | Some v -> Some (Obj.obj v)
- | None -> None
-
(** Registering genarg-manipulating functions *)
module type GenObj =
@@ -182,54 +174,31 @@ end
module Register (M : GenObj) =
struct
- let arg0_map =
- ref (String.Map.empty : (Obj.t, Obj.t, Obj.t) M.obj String.Map.t)
+ module GenMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) M.obj end)
+ let arg0_map = ref GenMap.empty
let register0 arg f = match arg with
- | ExtraArgType s ->
- if String.Map.mem s !arg0_map then
- let msg = str M.name ++ str " function already registered: " ++ str s in
- Errors.anomaly msg
+ | ExtraArg s ->
+ if GenMap.mem s !arg0_map then
+ let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) in
+ CErrors.anomaly msg
else
- arg0_map := String.Map.add s (Obj.magic f) !arg0_map
+ arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map
| _ -> assert false
let get_obj0 name =
- try String.Map.find name !arg0_map
+ try
+ let GenMap.Pack obj = GenMap.find name !arg0_map in obj
with Not_found ->
- match M.default (ExtraArgType name) with
+ match M.default (ExtraArg name) with
| None ->
- Errors.anomaly (str M.name ++ str " function not found: " ++ str name)
+ CErrors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name))
| Some obj -> obj
(** For now, the following function is quite dummy and should only be applied
to an extra argument type, otherwise, it will badly fail. *)
let obj t = match t with
- | ExtraArgType s -> Obj.magic (get_obj0 s)
+ | ExtraArg s -> get_obj0 s
| _ -> assert false
end
-
-(** Hackish part *)
-
-let arg0_names = ref (String.Map.empty : string String.Map.t)
-(** We use this table to associate a name to a given witness, to use it with
- the extension mechanism. This is REALLY ad-hoc, but I do not know how to
- do so nicely either. *)
-
-let register_name0 t name = match t with
-| ExtraArgType s ->
- let () = assert (not (String.Map.mem s !arg0_names)) in
- arg0_names := String.Map.add s name !arg0_names
-| _ -> failwith "register_name0"
-
-let get_name0 name =
- String.Map.find name !arg0_names
-
-module Unsafe =
-struct
-
-let inj tpe x = (tpe, x)
-let prj (_, x) = x
-
-end
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 671d96b7b..d7ad9b93b 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -6,6 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+(** Generic arguments used by the extension mechanisms of several Coq ASTs. *)
+
(** The route of a generic argument, from parsing to evaluation.
In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc.
@@ -34,69 +36,57 @@ In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc.
effective use
{% \end{%}verbatim{% }%}
-To distinguish between the uninterpreted (raw), globalized and
+To distinguish between the uninterpreted, globalized and
interpreted worlds, we annotate the type [generic_argument] by a
-phantom argument which is either [constr_expr], [glob_constr] or
-[constr].
+phantom argument.
-Transformation for each type :
-{% \begin{%}verbatim{% }%}
-tag raw open type cooked closed type
-
-BoolArgType bool bool
-IntArgType int int
-IntOrVarArgType int or_var int
-StringArgType string (parsed w/ "") string
-PreIdentArgType string (parsed w/o "") (vernac only)
-IdentArgType true identifier identifier
-IdentArgType false identifier (pattern_ident) identifier
-IntroPatternArgType intro_pattern_expr intro_pattern_expr
-VarArgType identifier located identifier
-RefArgType reference global_reference
-QuantHypArgType quantified_hypothesis quantified_hypothesis
-ConstrArgType constr_expr constr
-ConstrMayEvalArgType constr_expr may_eval constr
-OpenConstrArgType open_constr_expr open_constr
-ConstrWithBindingsArgType constr_expr with_bindings constr with_bindings
-BindingsArgType constr_expr bindings constr bindings
-List0ArgType of argument_type
-List1ArgType of argument_type
-OptArgType of argument_type
-ExtraArgType of string '_a '_b
-{% \end{%}verbatim{% }%}
*)
(** {5 Generic types} *)
-type ('raw, 'glob, 'top) genarg_type
-(** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized
- one, and ['top] the internalized one. *)
+module ArgT :
+sig
+ type ('a, 'b, 'c) tag
+ val eq : ('a1, 'b1, 'c1) tag -> ('a2, 'b2, 'c2) tag -> ('a1 * 'b1 * 'c1, 'a2 * 'b2 * 'c2) CSig.eq option
+ val repr : ('a, 'b, 'c) tag -> string
+ type any = Any : ('a, 'b, 'c) tag -> any
+ val name : string -> any option
+end
+
+(** Generic types. The first parameter is the OCaml lowest level, the second one
+ is the globalized level, and third one the internalized level. *)
+type (_, _, _) genarg_type =
+| ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type
+| ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
+| OptArg : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
+| PairArg : ('a1, 'b1, 'c1) genarg_type * ('a2, 'b2, 'c2) genarg_type ->
+ ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type
type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
(** Alias for concision when the three types agree. *)
-val make0 : 'raw option -> string -> ('raw, 'glob, 'top) genarg_type
+val make0 : string -> ('raw, 'glob, 'top) genarg_type
(** Create a new generic type of argument: force to associate
unique ML types at each of the three levels. *)
-val create_arg : 'raw option -> string -> ('raw, 'glob, 'top) genarg_type
+val create_arg : string -> ('raw, 'glob, 'top) genarg_type
(** Alias for [make0]. *)
(** {5 Specialized types} *)
(** All of [rlevel], [glevel] and [tlevel] must be non convertible
- to ensure the injectivity of the type inference from type
- ['co generic_argument] to [('a,'co) abstract_argument_type];
- this guarantees that, for 'co fixed, the type of
- out_gen is monomorphic over 'a, hence type-safe
-*)
+ to ensure the injectivity of the GADT type inference. *)
-type rlevel
-type glevel
-type tlevel
+type rlevel = [ `rlevel ]
+type glevel = [ `glevel ]
+type tlevel = [ `tlevel ]
-type ('a, 'co) abstract_argument_type
-(** Type at level ['co] represented by an OCaml value of type ['a]. *)
+(** Generic types at a fixed level. The first parameter embeds the OCaml type
+ and the second one the level. *)
+type (_, _) abstract_argument_type =
+| Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type
+| Glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type
+| Topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type
type 'a raw_abstract_argument_type = ('a, rlevel) abstract_argument_type
(** Specialized type at raw level. *)
@@ -120,7 +110,7 @@ val topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type
(** {5 Generic arguments} *)
-type 'a generic_argument
+type 'l generic_argument = GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument
(** A inhabitant of ['level generic_argument] is a inhabitant of some type at
level ['level], together with the representation of this type. *)
@@ -141,66 +131,20 @@ val has_type : 'co generic_argument -> ('a, 'co) abstract_argument_type -> bool
(** [has_type v t] tells whether [v] has type [t]. If true, it ensures that
[out_gen t v] will not raise a dynamic type exception. *)
-(** {6 Destructors} *)
-
-type ('a, 'b, 'c, 'l) cast
-
-val raw : ('a, 'b, 'c, rlevel) cast -> 'a
-val glb : ('a, 'b, 'c, glevel) cast -> 'b
-val top : ('a, 'b, 'c, tlevel) cast -> 'c
-
-type ('r, 'l) unpacker =
- { unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c, 'l) cast -> 'r }
-
-val unpack : ('r, 'l) unpacker -> 'l generic_argument -> 'r
-(** Existential-type destructors. *)
-
-(** {6 Manipulation of generic arguments}
-
-Those functions fail if they are applied to an argument which has not the right
-dynamic type. *)
-
-type ('r, 'l) list_unpacker =
- { list_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type ->
- ('a list, 'b list, 'c list, 'l) cast -> 'r }
-
-val list_unpack : ('r, 'l) list_unpacker -> 'l generic_argument -> 'r
-
-type ('r, 'l) opt_unpacker =
- { opt_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type ->
- ('a option, 'b option, 'c option, 'l) cast -> 'r }
-
-val opt_unpack : ('r, 'l) opt_unpacker -> 'l generic_argument -> 'r
-
-type ('r, 'l) pair_unpacker =
- { pair_unpacker : 'a1 'a2 'b1 'b2 'c1 'c2.
- ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type ->
- (('a1 * 'a2), ('b1 * 'b2), ('c1 * 'c2), 'l) cast -> 'r }
-
-val pair_unpack : ('r, 'l) pair_unpacker -> 'l generic_argument -> 'r
-
(** {6 Type reification} *)
-type argument_type =
- (** Basic types *)
- | IntOrVarArgType
- | IdentArgType
- | VarArgType
- (** Specific types *)
- | GenArgType
- | ConstrArgType
- | ConstrMayEvalArgType
- | QuantHypArgType
- | OpenConstrArgType
- | ConstrWithBindingsArgType
- | BindingsArgType
- | RedExprArgType
- | ListArgType of argument_type
- | OptArgType of argument_type
- | PairArgType of argument_type * argument_type
- | ExtraArgType of string
+type argument_type = ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type
+
+(** {6 Equalities} *)
val argument_type_eq : argument_type -> argument_type -> bool
+val genarg_type_eq :
+ ('a1, 'b1, 'c1) genarg_type ->
+ ('a2, 'b2, 'c2) genarg_type ->
+ ('a1 * 'b1 * 'c1, 'a2 * 'b2 * 'c2) CSig.eq option
+val abstract_argument_type_eq :
+ ('a, 'l) abstract_argument_type -> ('b, 'l) abstract_argument_type ->
+ ('a, 'b) CSig.eq option
val pr_argument_type : argument_type -> Pp.std_ppcmds
(** Print a human-readable representation for a given type. *)
@@ -236,43 +180,13 @@ sig
end
-(** {5 Basic generic type constructors} *)
+(** {5 Compatibility layer}
-(** {6 Parameterized types} *)
+The functions below are aliases for generic_type constructors.
+
+*)
val wit_list : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type ->
('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type
-
-(** {5 Magic used by the parser} *)
-
-val default_empty_value : ('raw, 'glb, 'top) genarg_type -> 'raw option
-
-val register_name0 : ('a, 'b, 'c) genarg_type -> string -> unit
-(** Used by the extension to give a name to types. The string should be the
- absolute path of the argument witness, e.g.
- [register_name0 wit_toto "MyArg.wit_toto"]. *)
-
-val get_name0 : string -> string
-(** Return the absolute path of a given witness. *)
-
-(** {5 Unsafe loophole} *)
-
-module Unsafe :
-sig
-
-(** Unsafe magic functions. Not for kids. This is provided here as a loophole to
- escape this module. Do NOT use outside of the dedicated areas. NOT. EVER. *)
-
-val inj : argument_type -> Obj.t -> 'lev generic_argument
-(** Injects an object as generic argument. !!!BEWARE!!! only do this as
- [inj tpe x] where:
-
- 1. [tpe] is the reification of a [('a, 'b, 'c) genarg_type];
- 2. [x] has type ['a], ['b] or ['c] according to the return level ['lev]. *)
-
-val prj : 'lev generic_argument -> Obj.t
-(** Recover the contents of a generic argument. *)
-
-end
diff --git a/lib/hMap.ml b/lib/hMap.ml
index ba6aad913..ea76e7427 100644
--- a/lib/hMap.ml
+++ b/lib/hMap.ml
@@ -68,34 +68,91 @@ struct
Int.Map.update h m s
with Not_found -> s
+ let height s = Int.Map.height s
+
+ let is_smaller s1 s2 = height s1 <= height s2 + 3
+
+ (** Assumes s1 << s2 *)
+ let fast_union s1 s2 =
+ let fold h s accu =
+ try Int.Map.modify h (fun _ s' -> Set.fold Set.add s s') accu
+ with Not_found -> Int.Map.add h s accu
+ in
+ Int.Map.fold fold s1 s2
+
let union s1 s2 =
- let fu _ m1 m2 = match m1, m2 with
- | None, None -> None
- | (Some _ as m), None | None, (Some _ as m) -> m
- | Some m1, Some m2 -> Some (Set.union m1 m2)
+ if is_smaller s1 s2 then fast_union s1 s2
+ else if is_smaller s2 s1 then fast_union s2 s1
+ else
+ let fu _ m1 m2 = match m1, m2 with
+ | None, None -> None
+ | (Some _ as m), None | None, (Some _ as m) -> m
+ | Some m1, Some m2 -> Some (Set.union m1 m2)
+ in
+ Int.Map.merge fu s1 s2
+
+ (** Assumes s1 << s2 *)
+ let fast_inter s1 s2 =
+ let fold h s accu =
+ try
+ let s' = Int.Map.find h s2 in
+ let si = Set.filter (fun e -> Set.mem e s') s in
+ if Set.is_empty si then accu
+ else Int.Map.add h si accu
+ with Not_found -> accu
in
- Int.Map.merge fu s1 s2
+ Int.Map.fold fold s1 Int.Map.empty
let inter s1 s2 =
- let fu _ m1 m2 = match m1, m2 with
- | None, None -> None
- | Some _, None | None, Some _ -> None
- | Some m1, Some m2 ->
- let m = Set.inter m1 m2 in
- if Set.is_empty m then None else Some m
+ if is_smaller s1 s2 then fast_inter s1 s2
+ else if is_smaller s2 s1 then fast_inter s2 s1
+ else
+ let fu _ m1 m2 = match m1, m2 with
+ | None, None -> None
+ | Some _, None | None, Some _ -> None
+ | Some m1, Some m2 ->
+ let m = Set.inter m1 m2 in
+ if Set.is_empty m then None else Some m
+ in
+ Int.Map.merge fu s1 s2
+
+ (** Assumes s1 << s2 *)
+ let fast_diff_l s1 s2 =
+ let fold h s accu =
+ try
+ let s' = Int.Map.find h s2 in
+ let si = Set.filter (fun e -> not (Set.mem e s')) s in
+ if Set.is_empty si then accu
+ else Int.Map.add h si accu
+ with Not_found -> Int.Map.add h s accu
in
- Int.Map.merge fu s1 s2
+ Int.Map.fold fold s1 Int.Map.empty
+
+ (** Assumes s2 << s1 *)
+ let fast_diff_r s1 s2 =
+ let fold h s accu =
+ try
+ 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
+ with Not_found -> accu
+ in
+ Int.Map.fold fold s2 s1
let diff s1 s2 =
- let fu _ m1 m2 = match m1, m2 with
- | None, None -> None
- | (Some _ as m), None -> m
- | None, Some _ -> None
- | Some m1, Some m2 ->
- let m = Set.diff m1 m2 in
- if Set.is_empty m then None else Some m
- in
- Int.Map.merge fu s1 s2
+ if is_smaller s1 s2 then fast_diff_l s1 s2
+ else if is_smaller s2 s2 then fast_diff_r s1 s2
+ else
+ let fu _ m1 m2 = match m1, m2 with
+ | None, None -> None
+ | (Some _ as m), None -> m
+ | None, Some _ -> None
+ | Some m1, Some m2 ->
+ let m = Set.diff m1 m2 in
+ if Set.is_empty m then None else Some m
+ in
+ Int.Map.merge fu s1 s2
let compare s1 s2 = Int.Map.compare Set.compare s1 s2
@@ -286,6 +343,8 @@ struct
let m = Int.Map.find h s in
Map.find k m
+ let get k s = try find k s with Not_found -> assert false
+
let split k s = assert false (** Cannot be implemented efficiently *)
let map f s =
@@ -322,6 +381,8 @@ struct
let fs m = Map.smartmapi f m in
Int.Map.smartmap fs s
+ let height s = Int.Map.height s
+
module Unsafe =
struct
let map f s =
@@ -329,4 +390,17 @@ struct
Int.Map.map fs s
end
+ module Monad(M : CMap.MonadS) =
+ struct
+ module IntM = Int.Map.Monad(M)
+ module ExtM = Map.Monad(M)
+
+ let fold f s accu =
+ let ff _ m accu = ExtM.fold f m accu in
+ IntM.fold ff s accu
+
+ let fold_left _ _ _ = assert false
+ let fold_right _ _ _ = assert false
+ end
+
end
diff --git a/lib/hashcons.ml b/lib/hashcons.ml
index 4a72b015c..4eaacf914 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.ml
@@ -72,7 +72,7 @@ module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) =
end
-(* A few usefull wrappers:
+(* A few useful wrappers:
* takes as argument the function [generate] above and build a function of type
* u -> t -> t that creates a fresh table each time it is applied to the
* sub-hcons functions. *)
@@ -96,20 +96,6 @@ let recursive_hcons h f u =
let () = loop := hrec in
hrec
-(* A set of global hashcons functions *)
-let hashcons_resets = ref []
-let init() = List.iter (fun f -> f()) !hashcons_resets
-
-(* [register_hcons h u] registers the hcons function h, result of the above
- * wrappers. It returns another hcons function that always uses the same
- * table, which can be reinitialized by init()
- *)
-let register_hcons h u =
- let hf = ref (h u) in
- let reset() = hf := h u in
- hashcons_resets := reset :: !hashcons_resets;
- (fun x -> !hf x)
-
(* Basic hashcons modules for string and obj. Integers do not need be
hashconsed. *)
@@ -194,18 +180,3 @@ module Hobj = Make(
let eq = comp_obj
let hash = Hashtbl.hash
end)
-
-(* Hashconsing functions for string and obj. Always use the same
- * global tables. The latter can be reinitialized with init()
- *)
-(* string : string -> string *)
-(* obj : Obj.t -> Obj.t *)
-let string = register_hcons (simple_hcons Hstring.generate Hstring.hcons) ()
-let obj = register_hcons (recursive_hcons Hobj.generate Hobj.hcons) ()
-
-(* The unsafe polymorphic hashconsing function *)
-let magic_hash (c : 'a) =
- init();
- let r = obj (Obj.repr c) in
- init();
- (Obj.magic r : 'a)
diff --git a/lib/hashset.ml b/lib/hashset.ml
index 04009fdf3..af33544dc 100644
--- a/lib/hashset.ml
+++ b/lib/hashset.ml
@@ -162,7 +162,7 @@ module Make (E : EqType) =
t.hashes.(index) <- newhashes;
if sz <= t.limit && newsz > t.limit then begin
t.oversize <- t.oversize + 1;
- for i = 0 to over_limit do test_shrink_bucket t done;
+ for _i = 0 to over_limit do test_shrink_bucket t done;
end;
if t.oversize > Array.length t.table / over_limit then resize t
end else if Weak.check bucket i then begin
diff --git a/lib/heap.ml b/lib/heap.ml
index 187189fca..97ccadeba 100644
--- a/lib/heap.ml
+++ b/lib/heap.ml
@@ -62,8 +62,6 @@ module Functional(X : Ordered) = struct
let empty = Leaf
- let is_empty t = t = Leaf
-
let rec add x = function
| Leaf ->
Node (Leaf, x, Leaf)
diff --git a/lib/iStream.ml b/lib/iStream.ml
index c9f4d4a11..26a666e17 100644
--- a/lib/iStream.ml
+++ b/lib/iStream.ml
@@ -14,11 +14,11 @@ type 'a node = ('a,'a t) u
and 'a t = 'a node Lazy.t
-let empty = Lazy.lazy_from_val Nil
+let empty = Lazy.from_val Nil
-let cons x s = Lazy.lazy_from_val (Cons (x, s))
+let cons x s = Lazy.from_val (Cons (x, s))
-let thunk = Lazy.lazy_from_fun
+let thunk = Lazy.from_fun
let rec make_node f s = match f s with
| Nil -> Nil
diff --git a/lib/lib.mllib b/lib/lib.mllib
index 6805ce491..8791f0741 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,9 +1,10 @@
-Errors
+CErrors
+CWarnings
Bigint
-Dyn
Segmenttree
Unicodetable
Unicode
+Minisys
System
CThread
Spawn
diff --git a/lib/loc.ml b/lib/loc.ml
index afdab928c..0f9864a9a 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -8,7 +8,6 @@
(* Locations management *)
-
type t = {
fname : string; (** filename *)
line_nb : int; (** start line number *)
@@ -19,7 +18,7 @@ type t = {
ep : int; (** end position *)
}
-let create fname line_nb bol_pos (bp, ep) = {
+let create fname line_nb bol_pos bp ep = {
fname = fname; line_nb = line_nb; bol_pos = bol_pos;
line_nb_last = line_nb; bol_pos_last = bol_pos; bp = bp; ep = ep; }
@@ -54,8 +53,6 @@ let merge loc1 loc2 =
let unloc loc = (loc.bp, loc.ep)
-let represent loc = (loc.fname, loc.line_nb, loc.bol_pos, loc.bp, loc.ep)
-
let dummy_loc = ghost
let join_loc = merge
diff --git a/lib/loc.mli b/lib/loc.mli
index f39cd2670..c08e097a8 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -8,7 +8,15 @@
(** {5 Basic types} *)
-type t
+type t = {
+ fname : string; (** filename *)
+ line_nb : int; (** start line number *)
+ bol_pos : int; (** position of the beginning of start line *)
+ line_nb_last : int; (** end line number *)
+ bol_pos_last : int; (** position of the beginning of end line *)
+ bp : int; (** start position *)
+ ep : int; (** end position *)
+}
type 'a located = t * 'a
(** Embed a location in a type *)
@@ -17,9 +25,9 @@ type 'a located = t * 'a
(** This is inherited from CAMPL4/5. *)
-val create : string -> int -> int -> (int * int) -> t
+val create : string -> int -> int -> int -> int -> t
(** Create a location from a filename, a line number, a position of the
- beginning of the line and a pair of start and end position *)
+ beginning of the line, a start and end position *)
val unloc : t -> int * int
(** Return the start and end position of a location *)
@@ -35,9 +43,6 @@ val is_ghost : t -> bool
val merge : t -> t -> t
-val represent : t -> (string * int * int * int * int)
-(** Return the arguments given in [create] *)
-
(** {5 Located exceptions} *)
val add_loc : Exninfo.info -> t -> Exninfo.info
diff --git a/lib/minisys.ml b/lib/minisys.ml
new file mode 100644
index 000000000..25e4d79c4
--- /dev/null
+++ b/lib/minisys.ml
@@ -0,0 +1,74 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Minisys regroups some code that used to be in System.
+ Unlike System, this module has no dependency and could
+ be used for initial compilation target such as coqdep_boot.
+ The functions here are still available in System thanks to
+ an include. For the signature, look at the top of system.mli
+*)
+
+(** Dealing with directories *)
+
+type unix_path = string (* path in unix-style, with '/' separator *)
+
+type file_kind =
+ | FileDir of unix_path * (* basename of path: *) string
+ | FileRegular of string (* basename of file *)
+
+(* Copy of Filename.concat but assuming paths to always be POSIX *)
+
+let (//) dirname filename =
+ let l = String.length dirname in
+ if l = 0 || dirname.[l-1] = '/'
+ then dirname ^ filename
+ else dirname ^ "/" ^ filename
+
+(* Excluding directories; We avoid directories starting with . as well
+ as CVS and _darcs and any subdirs given via -exclude-dir *)
+
+let skipped_dirnames = ref ["CVS"; "_darcs"]
+
+let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames
+
+let ok_dirname f =
+ not (f = "") && f.[0] != '.' &&
+ not (List.mem f !skipped_dirnames) (*&&
+ (match Unicode.ident_refutation f with None -> true | _ -> false)*)
+
+(* Check directory can be opened *)
+
+let exists_dir dir =
+ try Sys.is_directory dir with Sys_error _ -> false
+
+let check_unix_dir warn dir =
+ if (Sys.os_type = "Win32" || Sys.os_type = "Cygwin") &&
+ (String.length dir > 2 && dir.[1] = ':' ||
+ String.contains dir '\\' ||
+ String.contains dir ';')
+ then warn ("assuming " ^ dir ^
+ " to be a Unix path even if looking like a Win32 path.")
+
+let apply_subdir f path name =
+ (* we avoid all files and subdirs starting by '.' (e.g. .svn) *)
+ (* as well as skipped files like CVS, ... *)
+ if ok_dirname name then
+ let path = if path = "." then name else path//name in
+ match try (Unix.stat path).Unix.st_kind with Unix.Unix_error _ -> Unix.S_BLK with
+ | Unix.S_DIR -> f (FileDir (path,name))
+ | Unix.S_REG -> f (FileRegular name)
+ | _ -> ()
+
+let readdir dir = try Sys.readdir dir with any -> [||]
+
+let process_directory f path =
+ Array.iter (apply_subdir f path) (readdir path)
+
+let process_subdirectories f path =
+ let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in
+ process_directory f path
diff --git a/lib/option.ml b/lib/option.ml
index 4ea613e4f..fbb883d30 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -41,8 +41,8 @@ let hash f = function
exception IsNone
-(** [get x] returns [y] where [x] is [Some y]. It raises IsNone
- if [x] equals [None]. *)
+(** [get x] returns [y] where [x] is [Some y].
+ @raise [IsNone] if [x] equals [None]. *)
let get = function
| Some y -> y
| _ -> raise IsNone
diff --git a/lib/option.mli b/lib/option.mli
index 409dff9d3..5e085620e 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -34,8 +34,8 @@ val compare : ('a -> 'a -> int) -> 'a option -> 'a option -> int
(** Lift a hash to option types. *)
val hash : ('a -> int) -> 'a option -> int
-(** [get x] returns [y] where [x] is [Some y]. It raises IsNone
- if [x] equals [None]. *)
+(** [get x] returns [y] where [x] is [Some y].
+ @raise IsNone if [x] equals [None]. *)
val get : 'a option -> 'a
(** [make x] returns [Some x]. *)
@@ -54,7 +54,7 @@ val flatten : 'a option option -> 'a option
val append : 'a option -> 'a option -> 'a option
-(** {6 "Iterators"} ***)
+(** {6 "Iterators"} *)
(** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing
otherwise. *)
@@ -63,8 +63,8 @@ val iter : ('a -> unit) -> 'a option -> unit
exception Heterogeneous
(** [iter2 f x y] executes [f z w] if [x] equals [Some z] and [y] equals
- [Some w]. It does nothing if both [x] and [y] are [None]. And raises
- [Heterogeneous] otherwise. *)
+ [Some w]. It does nothing if both [x] and [y] are [None].
+ @raise Heterogeneous otherwise. *)
val iter2 : ('a -> 'b -> unit) -> 'a option -> 'b option -> unit
(** [map f x] is [None] if [x] is [None] and [Some (f y)] if [x] is [Some y]. *)
@@ -78,8 +78,8 @@ val smartmap : ('a -> 'a) -> 'a option -> 'a option
val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a option -> 'b
(** [fold_left2 f a x y] is [f z w] if [x] is [Some z] and [y] is [Some w].
- It is [a] if both [x] and [y] are [None]. Otherwise it raises
- [Heterogeneous]. *)
+ It is [a] if both [x] and [y] are [None].
+ @raise Heterogeneous otherwise. *)
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. *)
@@ -91,7 +91,7 @@ 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] *)
val cata : ('a -> 'b) -> 'b -> 'a option -> 'b
-(** {6 More Specific Operations} ***)
+(** {6 More Specific Operations} *)
(** [default a x] is [y] if [x] is [Some y] and [a] otherwise. *)
val default : 'a -> 'a option -> 'a
diff --git a/lib/pp.ml b/lib/pp.ml
index 4f50e3e19..8291e7462 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -51,37 +51,19 @@ sig
val prj : t -> 'a key -> 'a option
end =
struct
- (** See module {Dyn} for more details. *)
- type t = int * Obj.t
+module Dyn = Dyn.Make(struct end)
- type 'a key = int
-
- let dyntab = ref (Int.Map.empty : string Int.Map.t)
-
- let create (s : string) =
- let hash = Hashtbl.hash s in
- let () = assert (not (Int.Map.mem hash !dyntab)) in
- let () = dyntab := Int.Map.add hash s !dyntab in
- hash
-
- let inj x h = (h, Obj.repr x)
-
- let prj (nh, rv) h =
- if Int.equal h nh then Some (Obj.magic rv)
- else None
+type t = Dyn.t
+type 'a key = 'a Dyn.tag
+let create = Dyn.create
+let inj = Dyn.Easy.inj
+let prj = Dyn.Easy.prj
end
open Pp_control
-(* This should not be used outside of this file. Use
- Flags.print_emacs instead. This one is updated when reading
- command line options. This was the only way to make [Pp] depend on
- an option without creating a circularity: [Flags] -> [Util] ->
- [Pp] -> [Flags] *)
-let print_emacs = ref false
-
(* The different kinds of blocks are:
\begin{description}
\item[hbox:] Horizontal block no line breaking;
@@ -95,17 +77,6 @@ let print_emacs = ref false
\end{description}
*)
-let comments = ref []
-
-let rec split_com comacc acc pos = function
- [] -> comments := List.rev acc; comacc
- | ((b,e),c as com)::coms ->
- (* Take all comments that terminates before pos, or begin exactly
- at pos (used to print comments attached after an expression) *)
- if e<=pos || pos=b then split_com (c::comacc) acc pos coms
- else split_com comacc (com::acc) pos coms
-
-
type block_type =
| Pp_hbox of int
| Pp_vbox of int
@@ -129,7 +100,7 @@ type 'a ppcmd_token =
| Ppcmd_open_box of block_type
| Ppcmd_close_box
| Ppcmd_close_tbox
- | Ppcmd_comment of int
+ | Ppcmd_comment of string list
| Ppcmd_open_tag of Tag.t
| Ppcmd_close_tag
@@ -195,7 +166,7 @@ let tab () = Glue.atom(Ppcmd_set_tab)
let fnl () = Glue.atom(Ppcmd_force_newline)
let pifb () = Glue.atom(Ppcmd_print_if_broken)
let ws n = Glue.atom(Ppcmd_white_space n)
-let comment n = Glue.atom(Ppcmd_comment n)
+let comment l = Glue.atom(Ppcmd_comment l)
(* derived commands *)
let mt () = Glue.empty
@@ -215,6 +186,25 @@ let strbrk s =
else if p = n then [] else [str (String.sub s p (n-p))]
in List.fold_left (++) Glue.empty (aux 0 0)
+let pr_loc_pos loc =
+ if Loc.is_ghost loc then (str"<unknown>")
+ else
+ let loc = Loc.unloc loc in
+ int (fst loc) ++ str"-" ++ int (snd loc)
+
+let pr_loc loc =
+ if Loc.is_ghost loc then str"<unknown>" ++ fnl ()
+ else
+ let fname = loc.Loc.fname in
+ if CString.equal fname "" then
+ Loc.(str"Toplevel input, characters " ++ int loc.bp ++
+ str"-" ++ int loc.ep ++ str":" ++ fnl ())
+ else
+ Loc.(str"File " ++ str "\"" ++ str fname ++ str "\"" ++
+ str", line " ++ int loc.line_nb ++ str", characters " ++
+ int (loc.bp-loc.bol_pos) ++ str"-" ++ int (loc.ep-loc.bol_pos) ++
+ str":" ++ fnl())
+
let ismt = is_empty
(* boxing commands *)
@@ -268,7 +258,7 @@ let rec pr_com ft s =
let n = String.index s '\n' in
String.sub s 0 n, Some (String.sub s (n+1) (String.length s - n - 1))
with Not_found -> s,None in
- com_if ft (Lazy.lazy_from_val());
+ com_if ft (Lazy.from_val());
(* let s1 =
if String.length s1 <> 0 && s1.[0] = ' ' then
(Format.pp_print_space ft (); String.sub s1 1 (String.length s1 - 1))
@@ -297,31 +287,30 @@ let pp_dirs ?pp_tag ft =
begin match tok with
| Str_def s ->
let n = utf8_length s in
- com_if ft (Lazy.lazy_from_val()); Format.pp_print_as ft n s
+ com_if ft (Lazy.from_val()); Format.pp_print_as ft n s
| Str_len (s, n) ->
- com_if ft (Lazy.lazy_from_val()); Format.pp_print_as ft n s
+ com_if ft (Lazy.from_val()); Format.pp_print_as ft n s
end
| Ppcmd_box(bty,ss) -> (* Prevent evaluation of the stream! *)
- com_if ft (Lazy.lazy_from_val());
+ com_if ft (Lazy.from_val());
pp_open_box bty ;
if not (Format.over_max_boxes ()) then Glue.iter pp_cmd ss;
Format.pp_close_box ft ()
- | Ppcmd_open_box bty -> com_if ft (Lazy.lazy_from_val()); pp_open_box bty
+ | Ppcmd_open_box bty -> com_if ft (Lazy.from_val()); pp_open_box bty
| Ppcmd_close_box -> Format.pp_close_box ft ()
| Ppcmd_close_tbox -> Format.pp_close_tbox ft ()
| Ppcmd_white_space n ->
- com_if ft (Lazy.lazy_from_fun (fun()->Format.pp_print_break ft n 0))
+ com_if ft (Lazy.from_fun (fun()->Format.pp_print_break ft n 0))
| Ppcmd_print_break(m,n) ->
- com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_break ft m n))
+ com_if ft (Lazy.from_fun(fun()->Format.pp_print_break ft m n))
| Ppcmd_set_tab -> Format.pp_set_tab ft ()
| Ppcmd_print_tbreak(m,n) ->
- com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_tbreak ft m n))
+ com_if ft (Lazy.from_fun(fun()->Format.pp_print_tbreak ft m n))
| Ppcmd_force_newline ->
com_brk ft; Format.pp_force_newline ft ()
| Ppcmd_print_if_broken ->
- com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_if_newline ft ()))
- | Ppcmd_comment i ->
- let coms = split_com [] [] i !comments in
+ com_if ft (Lazy.from_fun(fun()->Format.pp_print_if_newline ft ()))
+ | Ppcmd_comment coms ->
(* Format.pp_open_hvbox ft 0;*)
List.iter (pr_com ft) coms(*;
Format.pp_close_box ft ()*)
@@ -350,181 +339,30 @@ let pp_dirs ?pp_tag ft =
let () = Format.pp_print_flush ft () in
Exninfo.iraise reraise
-
-
-(* pretty print on stdout and stderr *)
-
-(* Special chars for emacs, to detect warnings inside goal output *)
-let emacs_quote_start = String.make 1 (Char.chr 254)
-let emacs_quote_end = String.make 1 (Char.chr 255)
-
-let emacs_quote_info_start = "<infomsg>"
-let emacs_quote_info_end = "</infomsg>"
-
-let emacs_quote g =
- if !print_emacs then hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end)
- else hov 0 g
-
-let emacs_quote_info g =
- if !print_emacs then hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end)
- else hov 0 g
-
-
(* pretty printing functions WITHOUT FLUSH *)
let pp_with ?pp_tag ft strm =
pp_dirs ?pp_tag ft (Glue.atom (Ppdir_ppcmds strm))
-let ppnl_with ft strm =
- pp_dirs ft (Glue.atom (Ppdir_ppcmds (strm ++ fnl ())))
-
(* pretty printing functions WITH FLUSH *)
let msg_with ft strm =
pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_flush))
-let msgnl_with ft strm =
- pp_dirs ft (Glue.atom(Ppdir_ppcmds strm) ++ Glue.atom(Ppdir_print_newline))
-
-(* pretty printing functions WITHOUT FLUSH *)
-let pp x = pp_with !std_ft x
-let ppnl x = ppnl_with !std_ft x
-let pperr x = pp_with !err_ft x
-let pperrnl x = ppnl_with !err_ft x
-let message s = ppnl (str s)
-let pp_flush x = Format.pp_print_flush !std_ft x
-let pperr_flush x = Format.pp_print_flush !err_ft x
-let flush_all () =
- flush stderr; flush stdout; pp_flush (); pperr_flush ()
-
-(* pretty printing functions WITH FLUSH *)
-let msg x = msg_with !std_ft x
-let msgnl x = msgnl_with !std_ft x
-let msgerr x = msg_with !err_ft x
-let msgerrnl x = msgnl_with !err_ft x
-
-(* Logging management *)
-
-type message_level = Feedback.message_level =
- | Debug of string
- | Info
- | Notice
- | Warning
- | Error
-
-type message = Feedback.message = {
- message_level : message_level;
- message_content : string;
-}
-
-let of_message = Feedback.of_message
-let to_message = Feedback.to_message
-let is_message = Feedback.is_message
-
-type logger = message_level -> std_ppcmds -> unit
-
-let make_body info s =
- emacs_quote (hov 0 (info ++ spc () ++ s))
-
-let debugbody strm = emacs_quote_info (hov 0 (str "Debug:" ++ spc () ++ strm))
-let warnbody strm = make_body (str "Warning:") strm
-let errorbody strm = make_body (str "Error:") strm
-let infobody strm = emacs_quote_info strm
-
-let std_logger ~id:_ level msg = match level with
-| Debug _ -> msgnl (debugbody msg)
-| Info -> msgnl (hov 0 msg)
-| Notice -> msgnl msg
-| Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody msg)) ()
-| Error -> msgnl_with !err_ft (errorbody msg)
-
-let emacs_logger ~id:_ level mesg = match level with
-| Debug _ -> msgnl (debugbody mesg)
-| Info -> msgnl (infobody mesg)
-| Notice -> msgnl mesg
-| Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody mesg)) ()
-| Error -> msgnl_with !err_ft (errorbody mesg)
-
-let logger = ref std_logger
-
-let make_pp_emacs() = print_emacs:=true; logger:=emacs_logger
-let make_pp_nonemacs() = print_emacs:=false; logger := std_logger
-
-let ft_logger old_logger ft ~id level mesg = match level with
- | Debug _ -> msgnl_with ft (debugbody mesg)
- | Info -> msgnl_with ft (infobody mesg)
- | Notice -> msgnl_with ft mesg
- | Warning -> old_logger ~id:id level mesg
- | Error -> old_logger ~id:id level mesg
-
-let with_output_to_file fname func input =
- let old_logger = !logger in
- let channel = open_out (String.concat "." [fname; "out"]) in
- logger := ft_logger old_logger (Format.formatter_of_out_channel channel);
- try
- let output = func input in
- logger := old_logger;
- close_out channel;
- output
- with reraise ->
- let reraise = Backtrace.add_backtrace reraise in
- logger := old_logger;
- close_out channel;
- Exninfo.iraise reraise
-
-let feedback_id = ref (Feedback.Edit 0)
-let feedback_route = ref Feedback.default_route
-
(* If mixing some output and a goal display, please use msg_warning,
so that interfaces (proofgeneral for example) can easily dispatch
them to different windows. *)
-let msg_info x = !logger ~id:!feedback_id Info x
-let msg_notice x = !logger ~id:!feedback_id Notice x
-let msg_warning x = !logger ~id:!feedback_id Warning x
-let msg_error x = !logger ~id:!feedback_id Error x
-let msg_debug x = !logger ~id:!feedback_id (Debug "_") x
-
-let set_logger l = logger := (fun ~id:_ lvl msg -> l lvl msg)
-
-let std_logger lvl msg = std_logger ~id:!feedback_id lvl msg
-
-(** Feedback *)
-
-let feeder = ref ignore
-let set_id_for_feedback ?(route=Feedback.default_route) i =
- feedback_id := i; feedback_route := route
-let feedback ?state_id ?edit_id ?route what =
- !feeder {
- Feedback.contents = what;
- Feedback.route = Option.default !feedback_route route;
- Feedback.id =
- match state_id, edit_id with
- | Some id, _ -> Feedback.State id
- | None, Some eid -> Feedback.Edit eid
- | None, None -> !feedback_id;
- }
-let set_feeder f = feeder := f
-let get_id_for_feedback () = !feedback_id, !feedback_route
-
-(** Utility *)
-
+(** Output to a string formatter *)
let string_of_ppcmds c =
- msg_with Format.str_formatter c;
+ Format.fprintf Format.str_formatter "@[%a@]" msg_with c;
Format.flush_str_formatter ()
-let log_via_feedback () = logger := (fun ~id lvl msg ->
- !feeder {
- Feedback.contents = Feedback.Message {
- message_level = lvl;
- message_content = string_of_ppcmds msg };
- Feedback.route = !feedback_route;
- Feedback.id = id })
-
(* Copy paste from Util *)
let pr_comma () = str "," ++ spc ()
let pr_semicolon () = str ";" ++ spc ()
let pr_bar () = 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
let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x
@@ -607,3 +445,4 @@ let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v
let prvect elem v = prvect_with_sep mt elem v
let surround p = hov 1 (str"(" ++ p ++ str")")
+
diff --git a/lib/pp.mli b/lib/pp.mli
index 98219636b..f607e99db 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -6,33 +6,24 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(** Modify pretty printing functions behavior for emacs ouput (special
- chars inserted at some places). This function should called once in
- module [Options], that's all. *)
-val make_pp_emacs:unit -> unit
-val make_pp_nonemacs:unit -> unit
-
-val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
-
(** Pretty-printers. *)
type std_ppcmds
(** {6 Formatting commands} *)
-val str : string -> std_ppcmds
+val str : string -> std_ppcmds
val stras : int * string -> std_ppcmds
-val brk : int * int -> std_ppcmds
-val tbrk : int * int -> std_ppcmds
-val tab : unit -> std_ppcmds
-val fnl : unit -> std_ppcmds
-val pifb : unit -> std_ppcmds
-val ws : int -> std_ppcmds
-val mt : unit -> std_ppcmds
-val ismt : std_ppcmds -> bool
-
-val comment : int -> std_ppcmds
-val comments : ((int * int) * string) list ref
+val brk : int * int -> std_ppcmds
+val tbrk : int * int -> std_ppcmds
+val tab : unit -> std_ppcmds
+val fnl : unit -> std_ppcmds
+val pifb : unit -> std_ppcmds
+val ws : int -> std_ppcmds
+val mt : unit -> std_ppcmds
+val ismt : std_ppcmds -> bool
+
+val comment : string list -> std_ppcmds
(** {6 Manipulation commands} *)
@@ -100,87 +91,10 @@ sig
(** Project an object from a tag. *)
end
-type tag_handler = Tag.t -> Format.tag
-
val tag : Tag.t -> std_ppcmds -> std_ppcmds
val open_tag : Tag.t -> std_ppcmds
val close_tag : unit -> std_ppcmds
-(** {6 Sending messages to the user} *)
-type message_level = Feedback.message_level =
- | Debug of string
- | Info
- | Notice
- | Warning
- | Error
-
-type message = Feedback.message = {
- message_level : message_level;
- message_content : string;
-}
-
-type logger = message_level -> std_ppcmds -> unit
-
-(** {6 output functions}
-
-[msg_notice] do not put any decoration on output by default. If
-possible don't mix it with goal output (prefer msg_info or
-msg_warning) so that interfaces can dispatch outputs easily. Once all
-interfaces use the xml-like protocol this constraint can be
-relaxed. *)
-(* Should we advertise these functions more? Should they be the ONLY
- allowed way to output something? *)
-
-val msg_info : std_ppcmds -> unit
-(** Message that displays information, usually in verbose mode, such as [Foobar
- is defined] *)
-
-val msg_notice : std_ppcmds -> unit
-(** Message that should be displayed, such as [Print Foo] or [Show Bar]. *)
-
-val msg_warning : std_ppcmds -> unit
-(** Message indicating that something went wrong, but without serious
- consequences. *)
-
-val msg_error : std_ppcmds -> unit
-(** Message indicating that something went really wrong, though still
- recoverable; otherwise an exception would have been raised. *)
-
-val msg_debug : std_ppcmds -> unit
-(** For debugging purposes *)
-
-val std_logger : logger
-(** Standard logging function *)
-
-val set_logger : logger -> unit
-
-val log_via_feedback : unit -> unit
-
-val of_message : message -> Xml_datatype.xml
-val to_message : Xml_datatype.xml -> message
-val is_message : Xml_datatype.xml -> bool
-
-
-(** {6 Feedback sent, even asynchronously, to the user interface} *)
-
-(* This stuff should be available to most of the system, line msg_* above.
- * But I'm unsure this is the right place, especially for the global edit_id.
- *
- * Morally the parser gets a string and an edit_id, and gives back an AST.
- * Feedbacks during the parsing phase are attached to this edit_id.
- * The interpreter assigns an exec_id to the ast, and feedbacks happening
- * during interpretation are attached to the exec_id.
- * Only one among state_id and edit_id can be provided. *)
-
-val feedback :
- ?state_id:Feedback.state_id -> ?edit_id:Feedback.edit_id ->
- ?route:Feedback.route_id -> Feedback.feedback_content -> unit
-
-val set_id_for_feedback :
- ?route:Feedback.route_id -> Feedback.edit_or_state_id -> unit
-val set_feeder : (Feedback.feedback -> unit) -> unit
-val get_id_for_feedback : unit -> Feedback.edit_or_state_id * Feedback.route_id
-
(** {6 Utilities} *)
val string_of_ppcmds : std_ppcmds -> string
@@ -199,6 +113,9 @@ val pr_bar : unit -> std_ppcmds
val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds
(** Adds a space in front of its argument. *)
+val pr_non_empty_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds
+(** Adds a space in front of its argument if non empty. *)
+
val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
(** Inner object preceded with a space if [Some], nothing otherwise. *)
@@ -248,31 +165,15 @@ val surround : std_ppcmds -> std_ppcmds
val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
-(** {6 Low-level pretty-printing functions {% \emph{%}without flush{% }%}. } *)
-
-val pp_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit
-
-(** {6 Pretty-printing functions {% \emph{%}without flush{% }%} on [stdout] and [stderr]. } *)
+val pr_loc : Loc.t -> std_ppcmds
-(** These functions are low-level interface to printing and should not be used
- in usual code. Consider using the [msg_*] function family instead. *)
+(** {6 Low-level pretty-printing functions with and without flush} *)
-val pp : std_ppcmds -> unit
-val ppnl : std_ppcmds -> unit
-val pperr : std_ppcmds -> unit
-val pperrnl : std_ppcmds -> unit
-val pperr_flush : unit -> unit
-val pp_flush : unit -> unit
-val flush_all: unit -> unit
-
-(** {6 Deprecated functions} *)
-
-(** DEPRECATED. Do not use in newly written code. *)
+(** FIXME: These ignore the logging settings and call [Format] directly *)
+type tag_handler = Tag.t -> Format.tag
-val msg_with : Format.formatter -> std_ppcmds -> unit
+(** [msg_with fmt pp] Print [pp] to [fmt] and flush [fmt] *)
+val msg_with : Format.formatter -> std_ppcmds -> unit
-val msg : std_ppcmds -> unit
-val msgnl : std_ppcmds -> unit
-val msgerr : std_ppcmds -> unit
-val msgerrnl : std_ppcmds -> unit
-val message : string -> unit (** = pPNL *)
+(** [msg_with fmt pp] Print [pp] to [fmt] and don't flush [fmt] *)
+val pp_with : ?pp_tag:tag_handler -> Format.formatter -> std_ppcmds -> unit
diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml
index bb73fbdf5..ecfaa822c 100644
--- a/lib/ppstyle.ml
+++ b/lib/ppstyle.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Util
+module String = CString
type t = string
(** We use the concatenated string, with dots separating each string. We
@@ -107,8 +107,11 @@ let pp_tag t = match Pp.Tag.prj t tag with
| None -> ""
| Some key -> key
+let clear_tag_fn = ref (fun () -> ())
+
let init_color_output () =
let push_tag, pop_tag, clear_tag = make_style_stack !tags in
+ clear_tag_fn := clear_tag;
let tag_handler = {
Format.mark_open_tag = push_tag;
Format.mark_close_tag = pop_tag;
@@ -116,34 +119,24 @@ let init_color_output () =
Format.print_close_tag = ignore;
} in
let open Pp_control in
- let () = Format.pp_set_mark_tags !std_ft true in
- let () = Format.pp_set_mark_tags !err_ft true in
- let () = Format.pp_set_formatter_tag_functions !std_ft tag_handler in
- let () = Format.pp_set_formatter_tag_functions !err_ft tag_handler in
+ Format.pp_set_mark_tags !std_ft true;
+ Format.pp_set_mark_tags !err_ft true;
+ Format.pp_set_formatter_tag_functions !std_ft tag_handler;
+ Format.pp_set_formatter_tag_functions !err_ft tag_handler
+
+let color_msg ?loc ?header ft strm =
let pptag = tag in
let open Pp in
- let msg ?header ft strm =
- let strm = match header with
- | None -> hov 0 strm
+ let ploc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
+ let strm = match header with
+ | None -> hov 0 (ploc ++ strm)
| Some (h, t) ->
let tag = Pp.Tag.inj t pptag in
let h = Pp.tag tag (str h ++ str ":") in
- hov 0 (h ++ spc () ++ strm)
- in
- pp_with ~pp_tag ft strm;
- Format.pp_print_newline ft ();
- Format.pp_print_flush ft ();
- (** In case something went wrong, we reset the stack *)
- clear_tag ();
- in
- let logger level strm = match level with
- | Debug _ -> msg ~header:("Debug", debug_tag) !std_ft strm
- | Info -> msg !std_ft strm
- | Notice -> msg !std_ft strm
- | Warning ->
- let header = ("Warning", warning_tag) in
- Flags.if_warn (fun () -> msg ~header !err_ft strm) ()
- | Error -> msg ~header:("Error", error_tag) !err_ft strm
+ hov 0 (ploc ++ h ++ spc () ++ strm)
in
- let () = set_logger logger in
- ()
+ pp_with ~pp_tag ft strm;
+ Format.pp_print_newline ft ();
+ Format.pp_print_flush ft ();
+ (** In case something went wrong, we reset the stack *)
+ !clear_tag_fn ()
diff --git a/lib/ppstyle.mli b/lib/ppstyle.mli
index 97b5869f9..b07fcd5d4 100644
--- a/lib/ppstyle.mli
+++ b/lib/ppstyle.mli
@@ -11,7 +11,8 @@
(** {5 Style tags} *)
-type t
+type t = string
+
(** Style tags *)
val make : ?style:Terminal.style -> string list -> t
@@ -46,12 +47,11 @@ val dump : unit -> (t * Terminal.style option) list
(** {5 Setting color output} *)
val init_color_output : unit -> unit
-(** Once called, all tags defined here will use their current style when
- printed. To this end, this function redefines the loggers used when sending
- messages to the user. The program will in particular use the formatters
- {!Pp_control.std_ft} and {!Pp_control.err_ft} to display those messages,
- with additional syle information provided by this module. Be careful this is
- not compatible with the Emacs mode! *)
+
+val color_msg : ?loc:Loc.t -> ?header:string * Format.tag ->
+ Format.formatter -> Pp.std_ppcmds -> unit
+(** {!color_msg ?header fmt pp} will format according to the tags
+ defined in this file *)
val pp_tag : Pp.tag_handler
(** Returns the name of a style tag that is understandable by the formatters
diff --git a/lib/profile.ml b/lib/profile.ml
index 2350cd43a..0910db3fe 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -260,7 +260,7 @@ let time_overhead_B_C () =
let _dw = dummy_spent_alloc () in
let _dt = get_time () in
()
- with e when Errors.noncritical e -> assert false
+ with e when CErrors.noncritical e -> assert false
done;
let after = get_time () in
let beforeloop = get_time () in
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml
index 6cc48c874..e7646fb79 100644
--- a/lib/remoteCounter.ml
+++ b/lib/remoteCounter.ml
@@ -25,7 +25,7 @@ let new_counter ~name a ~incr ~build =
(* - in the main process there is a race condition between slave
managers (that are threads) and the main thread, hence the mutex *)
if Flags.async_proofs_is_worker () then
- Errors.anomaly(Pp.str"Slave processes must install remote counters");
+ CErrors.anomaly(Pp.str"Slave processes must install remote counters");
Mutex.lock m; let x = f () in Mutex.unlock m;
build x in
let mk_thsafe_remote_getter f () =
@@ -33,7 +33,7 @@ let new_counter ~name a ~incr ~build =
let getter = ref(mk_thsafe_local_getter (fun () -> !data := incr !!data; !!data)) in
let installer f =
if not (Flags.async_proofs_is_worker ()) then
- Errors.anomaly(Pp.str"Only slave processes can install a remote counter");
+ CErrors.anomaly(Pp.str"Only slave processes can install a remote counter");
getter := mk_thsafe_remote_getter f in
(fun () -> !getter ()), installer
diff --git a/lib/richpp.ml b/lib/richpp.ml
index 453df43de..a98273edb 100644
--- a/lib/richpp.ml
+++ b/lib/richpp.ml
@@ -163,4 +163,34 @@ let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml =
in
node xml
+type richpp = xml
+
+let repr xml = xml
+let richpp_of_xml xml = xml
+let richpp_of_string s = PCData s
+
+let richpp_of_pp pp =
+ let annotate t = match Pp.Tag.prj t Ppstyle.tag with
+ | None -> None
+ | Some key -> Some (Ppstyle.repr key)
+ in
+ let rec drop = function
+ | PCData s -> [PCData s]
+ | Element (_, annotation, cs) ->
+ let cs = List.concat (List.map drop cs) in
+ match annotation.annotation with
+ | None -> cs
+ | Some s -> [Element (String.concat "." s, [], cs)]
+ in
+ let xml = rich_pp annotate pp in
+ Element ("_", [], drop xml)
+
+let raw_print xml =
+ let buf = Buffer.create 1024 in
+ let rec print = function
+ | PCData s -> Buffer.add_string buf s
+ | Element (_, _, cs) -> List.iter print cs
+ in
+ let () = print xml in
+ Buffer.contents buf
diff --git a/lib/richpp.mli b/lib/richpp.mli
index 05c16621b..287d265a8 100644
--- a/lib/richpp.mli
+++ b/lib/richpp.mli
@@ -39,3 +39,26 @@ val xml_of_rich_pp :
('annotation -> (string * string) list) ->
'annotation located Xml_datatype.gxml ->
Xml_datatype.xml
+
+(** {5 Enriched text} *)
+
+type richpp
+(** Type of text with style annotations *)
+
+val richpp_of_pp : Pp.std_ppcmds -> richpp
+(** Extract style information from formatted text *)
+
+val richpp_of_xml : Xml_datatype.xml -> richpp
+(** Do not use outside of dedicated areas *)
+
+val richpp_of_string : string -> richpp
+(** Make a styled text out of a normal string *)
+
+val repr : richpp -> Xml_datatype.xml
+(** Observe the styled text as XML *)
+
+(** {5 Debug/Compat} *)
+
+(** Represent the semi-structured document as a string, dropping any additional
+ information. *)
+val raw_print : richpp -> string
diff --git a/lib/serialize.ml b/lib/serialize.ml
deleted file mode 100644
index 79a79dd4e..000000000
--- a/lib/serialize.ml
+++ /dev/null
@@ -1,116 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Xml_datatype
-
-exception Marshal_error
-
-(** Utility functions *)
-
-let rec get_attr attr = function
- | [] -> raise Not_found
- | (k, v) :: l when CString.equal k attr -> v
- | _ :: l -> get_attr attr l
-
-let massoc x l =
- try get_attr x l
- with Not_found -> raise Marshal_error
-
-let constructor t c args = Element (t, ["val", c], args)
-let do_match t mf = function
- | Element (s, attrs, args) when CString.equal s t ->
- let c = massoc "val" attrs in
- mf c args
- | _ -> raise Marshal_error
-
-let singleton = function
- | [x] -> x
- | _ -> raise Marshal_error
-
-let raw_string = function
- | [] -> ""
- | [PCData s] -> s
- | _ -> raise Marshal_error
-
-(** Base types *)
-
-let of_unit () = Element ("unit", [], [])
-let to_unit : xml -> unit = function
- | Element ("unit", [], []) -> ()
- | _ -> raise Marshal_error
-
-let of_bool (b : bool) : xml =
- if b then constructor "bool" "true" []
- else constructor "bool" "false" []
-let to_bool : xml -> bool = do_match "bool" (fun s _ -> match s with
- | "true" -> true
- | "false" -> false
- | _ -> raise Marshal_error)
-
-let of_list (f : 'a -> xml) (l : 'a list) =
- Element ("list", [], List.map f l)
-let to_list (f : xml -> 'a) : xml -> 'a list = function
- | Element ("list", [], l) -> List.map f l
- | _ -> raise Marshal_error
-
-let of_option (f : 'a -> xml) : 'a option -> xml = function
- | None -> Element ("option", ["val", "none"], [])
- | Some x -> Element ("option", ["val", "some"], [f x])
-let to_option (f : xml -> 'a) : xml -> 'a option = function
- | Element ("option", ["val", "none"], []) -> None
- | Element ("option", ["val", "some"], [x]) -> Some (f x)
- | _ -> raise Marshal_error
-
-let of_string (s : string) : xml = Element ("string", [], [PCData s])
-let to_string : xml -> string = function
- | Element ("string", [], l) -> raw_string l
- | _ -> raise Marshal_error
-
-let of_int (i : int) : xml = Element ("int", [], [PCData (string_of_int i)])
-let to_int : xml -> int = function
- | Element ("int", [], [PCData s]) ->
- (try int_of_string s with Failure _ -> raise Marshal_error)
- | _ -> raise Marshal_error
-
-let of_pair (f : 'a -> xml) (g : 'b -> xml) (x : 'a * 'b) : xml =
- Element ("pair", [], [f (fst x); g (snd x)])
-let to_pair (f : xml -> 'a) (g : xml -> 'b) : xml -> 'a * 'b = function
- | Element ("pair", [], [x; y]) -> (f x, g y)
- | _ -> raise Marshal_error
-
-let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) CSig.union -> xml = function
- | CSig.Inl x -> Element ("union", ["val","in_l"], [f x])
- | CSig.Inr x -> Element ("union", ["val","in_r"], [g x])
-let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) CSig.union = function
- | Element ("union", ["val","in_l"], [x]) -> CSig.Inl (f x)
- | Element ("union", ["val","in_r"], [x]) -> CSig.Inr (g x)
- | _ -> raise Marshal_error
-
-(** More elaborate types *)
-
-let of_edit_id i = Element ("edit_id",["val",string_of_int i],[])
-let to_edit_id = function
- | Element ("edit_id",["val",i],[]) ->
- let id = int_of_string i in
- assert (id <= 0 );
- id
- | _ -> raise Marshal_error
-
-let of_loc loc =
- let start, stop = Loc.unloc loc in
- Element ("loc",[("start",string_of_int start);("stop",string_of_int stop)],[])
-let to_loc xml =
- match xml with
- | Element ("loc", l,[]) ->
- (try
- let start = massoc "start" l in
- let stop = massoc "stop" l in
- Loc.make_loc (int_of_string start, int_of_string stop)
- with Not_found | Invalid_argument _ -> raise Marshal_error)
- | _ -> raise Marshal_error
-
diff --git a/lib/serialize.mli b/lib/serialize.mli
deleted file mode 100644
index 2a8e53163..000000000
--- a/lib/serialize.mli
+++ /dev/null
@@ -1,37 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Xml_datatype
-
-exception Marshal_error
-
-val massoc: string -> (string * string) list -> string
-val constructor: string -> string -> xml list -> xml
-val do_match: string -> (string -> xml list -> 'b) -> xml -> 'b
-val singleton: 'a list -> 'a
-val raw_string: xml list -> string
-val of_unit: unit -> xml
-val to_unit: xml -> unit
-val of_bool: bool -> xml
-val to_bool: xml -> bool
-val of_list: ('a -> xml) -> 'a list -> xml
-val to_list: (xml -> 'a) -> xml -> 'a list
-val of_option: ('a -> xml) -> 'a option -> xml
-val to_option: (xml -> 'a) -> xml -> 'a option
-val of_string: string -> xml
-val to_string: xml -> string
-val of_int: int -> xml
-val to_int: xml -> int
-val of_pair: ('a -> xml) -> ('b -> xml) -> 'a * 'b -> xml
-val to_pair: (xml -> 'a) -> (xml -> 'b) -> xml -> 'a * 'b
-val of_union: ('a -> xml) -> ('b -> xml) -> ('a, 'b) CSig.union -> xml
-val to_union: (xml -> 'a) -> (xml -> 'b) -> xml -> ('a, 'b) CSig.union
-val of_edit_id: int -> xml
-val to_edit_id: xml -> int
-val of_loc : Loc.t -> xml
-val to_loc : xml -> Loc.t
diff --git a/lib/spawn.ml b/lib/spawn.ml
index fda4b4239..479176973 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -43,7 +43,7 @@ module type MainLoopModel = sig
end
(* Common code *)
-let assert_ b s = if not b then Errors.anomaly (Pp.str s)
+let assert_ b s = if not b then CErrors.anomaly (Pp.str s)
(* According to http://caml.inria.fr/mantis/view.php?id=5325
* you can't use the same socket for both writing and reading (may change
@@ -78,20 +78,6 @@ let accept (sr,sw) =
set_binary_mode_out cout true;
(csr, csw), cin, cout
-let handshake cin cout =
- try
- output_value cout (Hello (proto_version,Unix.getpid ())); flush cout;
- match input_value cin with
- | Hello(v, pid) when v = proto_version ->
- prerr_endline (Printf.sprintf "Handshake with %d OK" pid);
- pid
- | _ -> raise (Failure "handshake protocol")
- with
- | Failure s | Invalid_argument s | Sys_error s ->
- pr_err ("Handshake failed: " ^ s); raise (Failure "handshake")
- | End_of_file ->
- pr_err "Handshake failed: End_of_file"; raise (Failure "handshake")
-
let spawn_sock env prog args =
let main_sock, main_sock_name = mk_socket_channel () in
let extra = [| prog; "-main-channel"; main_sock_name |] in
@@ -206,7 +192,7 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ())
let live = callback cl ~read_all:(fun () -> ML.read_all gchan) in
if not live then kill p;
live
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
pr_err ("Async reader raised: " ^ (Printexc.to_string e));
kill p;
false) gchan
diff --git a/lib/stateid.ml b/lib/stateid.ml
index 59cf206e2..500581a39 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Xml_datatype
-
type t = int
let initial = 1
let dummy = 0
@@ -15,20 +13,14 @@ let fresh, in_range =
let cur = ref initial in
(fun () -> incr cur; !cur), (fun id -> id >= 0 && id <= !cur)
let to_string = string_of_int
-let of_int id = assert(in_range id); id
+let of_int id =
+ (* Coqide too to parse ids too, but cannot check if they are valid.
+ * Hence we check for validity only if we are an ide slave. *)
+ if !Flags.ide_slave then assert (in_range id);
+ id
let to_int id = id
let newer_than id1 id2 = id1 > id2
-let of_xml = function
- | Element ("state_id",["val",i],[]) ->
- let id = int_of_string i in
- (* Coqide too to parse ids too, but cannot check if they are valid.
- * Hence we check for validity only if we are an ide slave. *)
- if !Flags.ide_slave then assert(in_range id);
- id
- | _ -> raise (Invalid_argument "to_state_id")
-let to_xml i = Element ("state_id",["val",string_of_int i],[])
-
let state_id_info : (t * t) Exninfo.t = Exninfo.make ()
let add exn ?(valid = initial) id =
Exninfo.add exn state_id_info (valid, id)
@@ -37,7 +29,13 @@ let get exn = Exninfo.get exn state_id_info
let equal = Int.equal
let compare = Int.compare
-module Set = Set.Make(struct type t = int let compare = compare end)
+module Self = struct
+ type t = int
+ let compare = compare
+ let equal = equal
+end
+
+module Set = Set.Make(Self)
type ('a,'b) request = {
exn_info : t * t;
diff --git a/lib/stateid.mli b/lib/stateid.mli
index 2c12c30c3..cd8fddf0c 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -6,26 +6,23 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Xml_datatype
-
type t
val equal : t -> t -> bool
val compare : t -> t -> int
-module Set : Set.S with type elt = t
+module Self : Map.OrderedType with type t = t
+module Set : Set.S with type elt = t and type t = Set.Make(Self).t
val initial : t
val dummy : t
val fresh : unit -> t
val to_string : t -> string
+
val of_int : int -> t
val to_int : t -> int
-val newer_than : t -> t -> bool
-(* XML marshalling *)
-val to_xml : t -> xml
-val of_xml : xml -> t
+val newer_than : t -> t -> bool
(* Attaches to an exception the concerned state id, plus an optional
* state id that is a valid state id before the error.
diff --git a/lib/system.ml b/lib/system.ml
index b4b3882d3..af9aa5c07 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -9,40 +9,33 @@
(* $Id$ *)
open Pp
-open Errors
open Util
-(* All subdirectories, recursively *)
+include Minisys
-let exists_dir dir =
- try Sys.is_directory dir with Sys_error _ -> false
+(** Returns the list of all recursive subdirectories of [root] in
+ depth-first search, with sons ordered as on the file system;
+ warns if [root] does not exist *)
-let skipped_dirnames = ref ["CVS"; "_darcs"]
-
-let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames
-
-let ok_dirname f =
- not (String.is_empty f) && f.[0] != '.' &&
- not (String.List.mem f !skipped_dirnames) &&
- (match Unicode.ident_refutation f with None -> true | _ -> false)
-
-let readdir dir = try Sys.readdir dir with any -> [||]
+let warn_cannot_open_dir =
+ CWarnings.create ~name:"cannot-open-dir" ~category:"filesystem"
+ (fun dir -> str ("Cannot open directory " ^ dir))
let all_subdirs ~unix_path:root =
let l = ref [] in
let add f rel = l := (f, rel) :: !l in
- let rec traverse dir rel =
- Array.iter (fun f ->
- if ok_dirname f then
- let file = Filename.concat dir f in
- if exists_dir file then begin
- let newrel = rel @ [f] in
- add file newrel;
- traverse file newrel
- end)
- (readdir dir)
+ let rec traverse path rel =
+ let f = function
+ | FileDir (path,f) ->
+ let newrel = rel @ [f] in
+ add path newrel;
+ traverse path newrel
+ | _ -> ()
+ in process_directory f path
in
- if exists_dir root then traverse root [];
+ check_unix_dir (fun s -> Feedback.msg_warning (str s)) root;
+ if exists_dir root then traverse root []
+ else warn_cannot_open_dir root;
List.rev !l
(* Caching directory contents for efficient syntactic equality of file
@@ -63,20 +56,22 @@ let make_dir_table dir =
Array.fold_left filter_dotfiles StrSet.empty (readdir dir)
let exists_in_dir_respecting_case dir bf =
- let contents, cached =
- try StrMap.find dir !dirmap, true with Not_found ->
+ let cache_dir dir =
let contents = make_dir_table dir in
dirmap := StrMap.add dir contents !dirmap;
- contents, false in
+ contents in
+ let contents, fresh =
+ try
+ (* in batch mode, assume the directory content is still fresh *)
+ StrMap.find dir !dirmap, !Flags.batch_mode
+ with Not_found ->
+ (* in batch mode, we are not yet sure the directory exists *)
+ if !Flags.batch_mode && not (exists_dir dir) then StrSet.empty, true
+ else cache_dir dir, true in
StrSet.mem bf contents ||
- if cached then begin
+ not fresh &&
(* rescan, there is a new file we don't know about *)
- let contents = make_dir_table dir in
- dirmap := StrMap.add dir contents !dirmap;
- StrSet.mem bf contents
- end
- else
- false
+ StrSet.mem bf (cache_dir dir)
let file_exists_respecting_case path f =
(* This function ensures that a file with expected lowercase/uppercase
@@ -86,26 +81,29 @@ let file_exists_respecting_case path f =
let df = Filename.dirname f in
(String.equal df "." || aux df)
&& exists_in_dir_respecting_case (Filename.concat path df) bf
- in Sys.file_exists (Filename.concat path f) && aux f
+ in (!Flags.batch_mode || Sys.file_exists (Filename.concat path f)) && aux f
let rec search paths test =
match paths with
| [] -> []
| lpe :: rem -> test lpe @ search rem test
+let warn_ambiguous_file_name =
+ CWarnings.create ~name:"ambiguous-file-name" ~category:"filesystem"
+ (fun (filename,l,f) -> str filename ++ str " has been found in" ++ spc () ++
+ hov 0 (str "[ " ++
+ hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon())
+ (fun (lpe,_) -> str lpe) l)
+ ++ str " ];") ++ fnl () ++
+ str "loading " ++ str f)
+
+
let where_in_path ?(warn=true) path filename =
let check_and_warn l = match l with
| [] -> raise Not_found
| (lpe, f) :: l' ->
let () = match l' with
- | _ :: _ when warn ->
- msg_warning
- (str filename ++ str " has been found in" ++ spc () ++
- hov 0 (str "[ " ++
- hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon())
- (fun (lpe,_) -> str lpe) l)
- ++ str " ];") ++ fnl () ++
- str "loading " ++ str f)
+ | _ :: _ when warn -> warn_ambiguous_file_name (filename,l,f)
| _ -> ()
in
(lpe, f)
@@ -134,7 +132,7 @@ let find_file_in_path ?(warn=true) paths filename =
let root = Filename.dirname filename in
root, filename
else
- errorlabstrm "System.find_file_in_path"
+ CErrors.errorlabstrm "System.find_file_in_path"
(hov 0 (str "Can't find file" ++ spc () ++ str filename))
else
(* the name is considered to be the transcription as a relative
@@ -142,7 +140,7 @@ let find_file_in_path ?(warn=true) paths filename =
to be locate respecting case *)
try where_in_path ~warn paths filename
with Not_found ->
- errorlabstrm "System.find_file_in_path"
+ CErrors.errorlabstrm "System.find_file_in_path"
(hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++
str "on loadpath"))
@@ -150,27 +148,34 @@ let is_in_path lpath filename =
try ignore (where_in_path ~warn:false lpath filename); true
with Not_found -> false
+let warn_path_not_found =
+ CWarnings.create ~name:"path-not-found" ~category:"filesystem"
+ (fun () -> str "system variable PATH not found")
+
let is_in_system_path filename =
try
let lpath = CUnix.path_to_list (Sys.getenv "PATH") in
is_in_path lpath filename
with Not_found ->
- msg_warning (str "system variable PATH not found");
+ warn_path_not_found ();
false
let open_trapping_failure name =
try open_out_bin name
- with e when Errors.noncritical e ->
- errorlabstrm "System.open" (str "Can't open " ++ str name)
+ with e when CErrors.noncritical e ->
+ CErrors.errorlabstrm "System.open" (str "Can't open " ++ str name)
+
+let warn_cannot_remove_file =
+ CWarnings.create ~name:"cannot-remove-file" ~category:"filesystem"
+ (fun filename -> str"Could not remove file " ++ str filename ++ str" which is corrupted!")
let try_remove filename =
try Sys.remove filename
- with e when Errors.noncritical e ->
- msg_warning
- (str"Could not remove file " ++ str filename ++ str" which is corrupted!")
+ with e when CErrors.noncritical e ->
+ warn_cannot_remove_file filename
let error_corrupted file s =
- errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
+ CErrors.errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
let input_binary_int f ch =
try input_binary_int ch
@@ -243,11 +248,11 @@ let extern_state magic filename val_0 =
marshal_out channel val_0;
close_out channel
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
let () = try_remove filename in
iraise reraise
with Sys_error s ->
- errorlabstrm "System.extern_state" (str "System error: " ++ str s)
+ CErrors.errorlabstrm "System.extern_state" (str "System error: " ++ str s)
let intern_state magic filename =
try
@@ -256,12 +261,12 @@ let intern_state magic filename =
close_in channel;
v
with Sys_error s ->
- errorlabstrm "System.intern_state" (str "System error: " ++ str s)
+ CErrors.errorlabstrm "System.intern_state" (str "System error: " ++ str s)
let with_magic_number_check f a =
try f a
with Bad_magic_number {filename=fname;actual=actual;expected=expected} ->
- errorlabstrm "with_magic_number_check"
+ CErrors.errorlabstrm "with_magic_number_check"
(str"File " ++ str fname ++ strbrk" has bad magic number " ++
int actual ++ str" (expected " ++ int expected ++ str")." ++
spc () ++
@@ -295,13 +300,13 @@ let with_time time f x =
let y = f x in
let tend = get_time() in
let msg2 = if time then "" else " (successful)" in
- msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
+ Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
y
with e ->
let tend = get_time() in
let msg = if time then "" else "Finished failing transaction in " in
let msg2 = if time then "" else " (failure)" in
- msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
+ Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2);
raise e
let process_id () =
diff --git a/lib/system.mli b/lib/system.mli
index fa675a4f0..4dbb3695d 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -8,14 +8,46 @@
(** {5 Coqtop specific system utilities} *)
+(** {6 Directories} *)
+
+type unix_path = string (* path in unix-style, with '/' separator *)
+
+type file_kind =
+ | FileDir of unix_path * (* basename of path: *) string
+ | FileRegular of string (* basename of file *)
+
+val (//) : unix_path -> string -> unix_path
+
+val exists_dir : unix_path -> bool
+
+(** [check_unix_dir warn path] calls [warn] with an appropriate
+ message if [path] looks does not look like a Unix path on Windows *)
+
+val check_unix_dir : (string -> unit) -> unix_path -> unit
+
+(** [exclude_search_in_dirname path] excludes [path] when processing
+ directories *)
+
+val exclude_directory : unix_path -> unit
+
+(** [process_directory f path] applies [f] on contents of directory
+ [path]; fails with Unix_error if the latter does not exists; skips
+ all files or dirs starting with "." *)
+
+val process_directory : (file_kind -> unit) -> unix_path -> unit
+
+(** [process_subdirectories f path] applies [f path/file file] on each
+ [file] of the directory [path]; fails with Unix_error if the
+ latter does not exists; kips all files or dirs starting with "." *)
+
+val process_subdirectories : (unix_path -> string -> unit) -> unix_path -> unit
+
(** {6 Files and load paths} *)
(** Load path entries remember the original root
given by the user. For efficiency, we keep the full path (field
[directory]), the root path and the path relative to the root. *)
-val exclude_search_in_dirname : string -> unit
-
val all_subdirs : unix_path:string -> (CUnix.physical_path * string list) list
val is_in_path : CUnix.load_path -> string -> bool
val is_in_system_path : string -> bool
@@ -24,8 +56,6 @@ val where_in_path :
val where_in_path_rex :
CUnix.load_path -> Str.regexp -> (CUnix.physical_path * string) list
-val exists_dir : string -> bool
-
val find_file_in_path :
?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
diff --git a/lib/unicode.ml b/lib/unicode.ml
index 0dc4238ee..dc852d981 100644
--- a/lib/unicode.ml
+++ b/lib/unicode.ml
@@ -18,7 +18,7 @@ exception Unsupported
to simplify the masking process. (This choice seems to be a good
trade-off between speed and space after some benchmarks.) *)
-(* A 256ko table, initially filled with zeros. *)
+(* A 256 KiB table, initially filled with zeros. *)
let table = Array.make (1 lsl 17) 0
(* Associate a 2-bit pattern to each status at position [i].
@@ -147,6 +147,11 @@ let utf8_of_unicode n =
s
end
+(* If [s] is some UTF-8 encoded string
+ and [i] is a position of some UTF-8 character within [s]
+ then [next_utf8 s i] returns [(j,n)] where:
+ - [j] indicates the position of the next UTF-8 character
+ - [n] represents the UTF-8 character at index [i] *)
let next_utf8 s i =
let err () = invalid_arg "utf8" in
let l = String.length s - i in
@@ -256,3 +261,73 @@ let ascii_of_ident s =
(Buffer.add_char out s.[!i]; incr i)
done;
Buffer.contents out
+
+(* Compute length of an UTF-8 encoded string
+ Rem 1 : utf8_length <= String.length (equal if pure ascii)
+ Rem 2 : if used for an iso8859_1 encoded string, the result is
+ wrong in very rare cases. Such a wrong case corresponds to any
+ sequence of a character in range 192..253 immediately followed by a
+ character in range 128..191 (typical case in french is "déçu" which
+ is counted 3 instead of 4); then no real harm to use always
+ utf8_length even if using an iso8859_1 encoding *)
+
+(** FIXME: duplicate code with Pp *)
+
+let utf8_length s =
+ let len = String.length s
+ and cnt = ref 0
+ and nc = ref 0
+ and p = ref 0 in
+ while !p < len do
+ begin
+ match s.[!p] with
+ | '\000'..'\127' -> nc := 0 (* ascii char *)
+ | '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *)
+ | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *)
+ | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *)
+ | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *)
+ | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *)
+ | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *)
+ | '\254'..'\255' -> nc := 0 (* invalid byte *)
+ end ;
+ incr p ;
+ while !p < len && !nc > 0 do
+ match s.[!p] with
+ | '\128'..'\191' (* next continuation byte *) -> incr p ; decr nc
+ | _ (* not a continuation byte *) -> nc := 0
+ done ;
+ incr cnt
+ done ;
+ !cnt
+
+(* Variant of String.sub for UTF8 character positions *)
+let utf8_sub s start_u len_u =
+ let len_b = String.length s
+ and end_u = start_u + len_u
+ and cnt = ref 0
+ and nc = ref 0
+ and p = ref 0 in
+ let start_b = ref len_b in
+ while !p < len_b && !cnt < end_u do
+ if !cnt <= start_u then start_b := !p ;
+ begin
+ match s.[!p] with
+ | '\000'..'\127' -> nc := 0 (* ascii char *)
+ | '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *)
+ | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *)
+ | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *)
+ | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *)
+ | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *)
+ | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *)
+ | '\254'..'\255' -> nc := 0 (* invalid byte *)
+ end ;
+ incr p ;
+ while !p < len_b && !nc > 0 do
+ match s.[!p] with
+ | '\128'..'\191' (* next continuation byte *) -> incr p ; decr nc
+ | _ (* not a continuation byte *) -> nc := 0
+ done ;
+ incr cnt
+ done ;
+ let end_b = !p in
+ String.sub s !start_b (end_b - !start_b)
diff --git a/lib/unicode.mli b/lib/unicode.mli
index 00211164f..1f8bd44ee 100644
--- a/lib/unicode.mli
+++ b/lib/unicode.mli
@@ -10,17 +10,21 @@
type status = Letter | IdentPart | Symbol
+(** This exception is raised when UTF-8 the input string contains unsupported UTF-8 characters. *)
exception Unsupported
-(** Classify a unicode char into 3 classes, or raise [Unsupported] *)
+(** Classify a unicode char into 3 classes.
+ @raise Unsupported if the input string contains unsupported UTF-8 characters. *)
val classify : int -> status
-(** Check whether a given string be used as a legal identifier.
- - [None] means yes
- - [Some (b,s)] means no, with explanation [s] and severity [b] *)
+(** Return [None] if a given string can be used as a (Coq) identifier.
+ Return [Some (b,s)] otherwise, where [s] is an explanation and [b] is severity.
+ @raise Unsupported if the input string contains unsupported UTF-8 characters. *)
val ident_refutation : string -> (bool * string) option
-(** First char of a string, converted to lowercase *)
+(** First char of a string, converted to lowercase
+ @raise Unsupported if the input string contains unsupported UTF-8 characters.
+ @raise Assert_failure if the input string is empty. *)
val lowercase_first_char : string -> string
(** Return [true] if all UTF-8 characters in the input string are just plain
@@ -36,3 +40,9 @@ val ascii_of_ident : string -> string
(** Validate an UTF-8 string *)
val is_utf8 : string -> bool
+
+(** Return the length of a valid UTF-8 string. *)
+val utf8_length : string -> int
+
+(** Variant of {!String.sub} for UTF-8 strings. *)
+val utf8_sub : string -> int -> int -> string
diff --git a/lib/util.ml b/lib/util.ml
index a20dba0fc..009dfbe1c 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -87,7 +87,13 @@ let matrix_transpose mat =
let identity x = x
-let compose f g x = f (g x)
+(** Function composition: the mathematical [∘] operator.
+
+ So [g % f] is a synonym for [fun x -> g (f x)].
+
+ Also because [%] is right-associative, [h % g % f] means [fun x -> h (g (f x))].
+ *)
+let (%) f g x = f (g x)
let const x _ = x
@@ -124,10 +130,26 @@ let delayed_force f = f ()
type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
+type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq
+
+module Union =
+struct
+ let map f g = function
+ | Inl a -> Inl (f a)
+ | Inr b -> Inr (g b)
+
+ (** Lifting equality onto union types. *)
+ let equal f g x y = match x, y with
+ | Inl x, Inl y -> f x y
+ | Inr x, Inr y -> g x y
+ | _, _ -> false
+
+ let fold_left f g a = function
+ | Inl y -> f a y
+ | Inr y -> g a y
+end
-let map_union f g = function
- | Inl a -> Inl (f a)
- | Inr b -> Inr (g b)
+let map_union = Union.map
type iexn = Exninfo.iexn
diff --git a/lib/util.mli b/lib/util.mli
index 4156af672..6bed7e355 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -83,7 +83,15 @@ val matrix_transpose : 'a list list -> 'a list list
(** {6 Functions. } *)
val identity : 'a -> 'a
-val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
+
+(** Function composition: the mathematical [∘] operator.
+
+ So [g % f] is a synonym for [fun x -> g (f x)].
+
+ Also because [%] is right-associative, [h % g % f] means [fun x -> h (g (f x))].
+*)
+val (%) : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b
+
val const : 'a -> 'b -> 'a
val iterate : ('a -> 'a) -> int -> 'a -> 'a
val repeat : int -> ('a -> unit) -> 'a -> unit
@@ -106,10 +114,20 @@ val iraise : iexn -> 'a
type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
(** Union type *)
+module Union :
+sig
+ val map : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union
+ val equal : ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> ('a, 'b) union -> ('a, 'b) union -> bool
+ val fold_left : ('c -> 'a -> 'c) -> ('c -> 'b -> 'c) -> 'c -> ('a, 'b) union -> 'c
+end
+
val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union
+(** Alias for [Union.map] *)
type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
(** Used for browsable-until structures. *)
+type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq
+
val open_utf8_file_in : string -> in_channel
(** Open an utf-8 encoded file and skip the byte-order mark if any. *)
diff --git a/lib/xml_lexer.mli b/lib/xml_lexer.mli
deleted file mode 100644
index e61cb055f..000000000
--- a/lib/xml_lexer.mli
+++ /dev/null
@@ -1,44 +0,0 @@
-(*
- * Xml Light, an small Xml parser/printer with DTD support.
- * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License as published by the Free Software Foundation; either
- * version 2.1 of the License, or (at your option) any later version.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this library; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
- *)
-
-type error =
- | EUnterminatedComment
- | EUnterminatedString
- | EIdentExpected
- | ECloseExpected
- | ENodeExpected
- | EAttributeNameExpected
- | EAttributeValueExpected
- | EUnterminatedEntity
-
-exception Error of error
-
-type token =
- | Tag of string * (string * string) list * bool
- | PCData of string
- | Endtag of string
- | Eof
-
-type pos = int * int * int * int
-
-val init : Lexing.lexbuf -> unit
-val close : unit -> unit
-val token : Lexing.lexbuf -> token
-val pos : Lexing.lexbuf -> pos
-val restore : pos -> unit
diff --git a/lib/xml_lexer.mll b/lib/xml_lexer.mll
deleted file mode 100644
index 290f2c89a..000000000
--- a/lib/xml_lexer.mll
+++ /dev/null
@@ -1,317 +0,0 @@
-{(*
- * Xml Light, an small Xml parser/printer with DTD support.
- * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License as published by the Free Software Foundation; either
- * version 2.1 of the License, or (at your option) any later version.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this library; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
- *)
-
-open Lexing
-
-type error =
- | EUnterminatedComment
- | EUnterminatedString
- | EIdentExpected
- | ECloseExpected
- | ENodeExpected
- | EAttributeNameExpected
- | EAttributeValueExpected
- | EUnterminatedEntity
-
-exception Error of error
-
-type pos = int * int * int * int
-
-type token =
- | Tag of string * (string * string) list * bool
- | PCData of string
- | Endtag of string
- | Eof
-
-let last_pos = ref 0
-and current_line = ref 0
-and current_line_start = ref 0
-
-let tmp = Buffer.create 200
-
-let idents = Hashtbl.create 0
-
-let _ = begin
- Hashtbl.add idents "nbsp;" " ";
- Hashtbl.add idents "gt;" ">";
- Hashtbl.add idents "lt;" "<";
- Hashtbl.add idents "amp;" "&";
- Hashtbl.add idents "apos;" "'";
- Hashtbl.add idents "quot;" "\"";
-end
-
-let init lexbuf =
- current_line := 1;
- current_line_start := lexeme_start lexbuf;
- last_pos := !current_line_start
-
-let close lexbuf =
- Buffer.reset tmp
-
-let pos lexbuf =
- !current_line , !current_line_start ,
- !last_pos ,
- lexeme_start lexbuf
-
-let restore (cl,cls,lp,_) =
- current_line := cl;
- current_line_start := cls;
- last_pos := lp
-
-let newline lexbuf =
- incr current_line;
- last_pos := lexeme_end lexbuf;
- current_line_start := !last_pos
-
-let error lexbuf e =
- last_pos := lexeme_start lexbuf;
- raise (Error e)
-
-}
-
-let newline = ['\n']
-let break = ['\r']
-let space = [' ' '\t']
-let identchar = ['A'-'Z' 'a'-'z' '_' '0'-'9' ':' '-' '.']
-let ident = ['A'-'Z' 'a'-'z' '_' ':'] identchar*
-let entitychar = ['A'-'Z' 'a'-'z']
-let pcchar = [^ '\r' '\n' '<' '>' '&']
-
-rule token = parse
- | newline | (newline break) | break
- {
- newline lexbuf;
- PCData "\n"
- }
- | "<!--"
- {
- last_pos := lexeme_start lexbuf;
- comment lexbuf;
- token lexbuf
- }
- | "<?"
- {
- last_pos := lexeme_start lexbuf;
- header lexbuf;
- token lexbuf;
- }
- | '<' space* '/' space*
- {
- last_pos := lexeme_start lexbuf;
- let tag = ident_name lexbuf in
- ignore_spaces lexbuf;
- close_tag lexbuf;
- Endtag tag
- }
- | '<' space*
- {
- last_pos := lexeme_start lexbuf;
- let tag = ident_name lexbuf in
- ignore_spaces lexbuf;
- let attribs, closed = attributes lexbuf in
- Tag(tag, attribs, closed)
- }
- | "&#"
- {
- last_pos := lexeme_start lexbuf;
- Buffer.reset tmp;
- Buffer.add_string tmp (lexeme lexbuf);
- PCData (pcdata lexbuf)
- }
- | '&'
- {
- last_pos := lexeme_start lexbuf;
- Buffer.reset tmp;
- Buffer.add_string tmp (entity lexbuf);
- PCData (pcdata lexbuf)
- }
- | pcchar+
- {
- last_pos := lexeme_start lexbuf;
- Buffer.reset tmp;
- Buffer.add_string tmp (lexeme lexbuf);
- PCData (pcdata lexbuf)
- }
- | eof { Eof }
- | _
- { error lexbuf ENodeExpected }
-
-and ignore_spaces = parse
- | newline | (newline break) | break
- {
- newline lexbuf;
- ignore_spaces lexbuf
- }
- | space +
- { ignore_spaces lexbuf }
- | ""
- { () }
-
-and comment = parse
- | newline | (newline break) | break
- {
- newline lexbuf;
- comment lexbuf
- }
- | "-->"
- { () }
- | eof
- { raise (Error EUnterminatedComment) }
- | _
- { comment lexbuf }
-
-and header = parse
- | newline | (newline break) | break
- {
- newline lexbuf;
- header lexbuf
- }
- | "?>"
- { () }
- | eof
- { error lexbuf ECloseExpected }
- | _
- { header lexbuf }
-
-and pcdata = parse
- | newline | (newline break) | break
- {
- Buffer.add_char tmp '\n';
- newline lexbuf;
- pcdata lexbuf
- }
- | pcchar+
- {
- Buffer.add_string tmp (lexeme lexbuf);
- pcdata lexbuf
- }
- | "&#"
- {
- Buffer.add_string tmp (lexeme lexbuf);
- pcdata lexbuf;
- }
- | '&'
- {
- Buffer.add_string tmp (entity lexbuf);
- pcdata lexbuf
- }
- | ""
- { Buffer.contents tmp }
-
-and entity = parse
- | entitychar+ ';'
- {
- let ident = lexeme lexbuf in
- try
- Hashtbl.find idents (String.lowercase ident)
- with
- Not_found -> "&" ^ ident
- }
- | _ | eof
- { raise (Error EUnterminatedEntity) }
-
-and ident_name = parse
- | ident
- { lexeme lexbuf }
- | _ | eof
- { error lexbuf EIdentExpected }
-
-and close_tag = parse
- | '>'
- { () }
- | _ | eof
- { error lexbuf ECloseExpected }
-
-and attributes = parse
- | '>'
- { [], false }
- | "/>"
- { [], true }
- | "" (* do not read a char ! *)
- {
- let key = attribute lexbuf in
- let data = attribute_data lexbuf in
- ignore_spaces lexbuf;
- let others, closed = attributes lexbuf in
- (key, data) :: others, closed
- }
-
-and attribute = parse
- | ident
- { lexeme lexbuf }
- | _ | eof
- { error lexbuf EAttributeNameExpected }
-
-and attribute_data = parse
- | space* '=' space* '"'
- {
- Buffer.reset tmp;
- last_pos := lexeme_end lexbuf;
- dq_string lexbuf
- }
- | space* '=' space* '\''
- {
- Buffer.reset tmp;
- last_pos := lexeme_end lexbuf;
- q_string lexbuf
- }
- | _ | eof
- { error lexbuf EAttributeValueExpected }
-
-and dq_string = parse
- | '"'
- { Buffer.contents tmp }
- | '\\' [ '"' '\\' ]
- {
- Buffer.add_char tmp (lexeme_char lexbuf 1);
- dq_string lexbuf
- }
- | '&'
- {
- Buffer.add_string tmp (entity lexbuf);
- dq_string lexbuf
- }
- | eof
- { raise (Error EUnterminatedString) }
- | _
- {
- Buffer.add_char tmp (lexeme_char lexbuf 0);
- dq_string lexbuf
- }
-
-and q_string = parse
- | '\''
- { Buffer.contents tmp }
- | '\\' [ '\'' '\\' ]
- {
- Buffer.add_char tmp (lexeme_char lexbuf 1);
- q_string lexbuf
- }
- | '&'
- {
- Buffer.add_string tmp (entity lexbuf);
- q_string lexbuf
- }
- | eof
- { raise (Error EUnterminatedString) }
- | _
- {
- Buffer.add_char tmp (lexeme_char lexbuf 0);
- q_string lexbuf
- }
diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml
deleted file mode 100644
index 8db3f9e8b..000000000
--- a/lib/xml_parser.ml
+++ /dev/null
@@ -1,232 +0,0 @@
-(*
- * Xml Light, an small Xml parser/printer with DTD support.
- * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
- * Copyright (C) 2003 Jacques Garrigue
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License as published by the Free Software Foundation; either
- * version 2.1 of the License, or (at your option) any later version.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this library; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
- *)
-
-open Printf
-open Xml_datatype
-
-type xml = Xml_datatype.xml
-
-type error_pos = {
- eline : int;
- eline_start : int;
- emin : int;
- emax : int;
-}
-
-type error_msg =
- | UnterminatedComment
- | UnterminatedString
- | UnterminatedEntity
- | IdentExpected
- | CloseExpected
- | NodeExpected
- | AttributeNameExpected
- | AttributeValueExpected
- | EndOfTagExpected of string
- | EOFExpected
- | Empty
-
-type error = error_msg * error_pos
-
-exception Error of error
-
-exception File_not_found of string
-
-type t = {
- mutable check_eof : bool;
- mutable concat_pcdata : bool;
- source : Lexing.lexbuf;
- stack : Xml_lexer.token Stack.t;
-}
-
-type source =
- | SChannel of in_channel
- | SString of string
- | SLexbuf of Lexing.lexbuf
-
-exception Internal_error of error_msg
-exception NoMoreData
-
-let xml_error = ref (fun _ -> assert false)
-let file_not_found = ref (fun _ -> assert false)
-
-let is_blank s =
- let len = String.length s in
- let break = ref true in
- let i = ref 0 in
- while !break && !i < len do
- let c = s.[!i] in
- (* no '\r' because we replaced them in the lexer *)
- if c = ' ' || c = '\n' || c = '\t' then incr i
- else break := false
- done;
- !i = len
-
-let _raises e f =
- xml_error := e;
- file_not_found := f
-
-let make source =
- let source = match source with
- | SChannel chan -> Lexing.from_channel chan
- | SString s -> Lexing.from_string s
- | SLexbuf lexbuf -> lexbuf
- in
- let () = Xml_lexer.init source in
- {
- check_eof = false;
- concat_pcdata = true;
- source = source;
- stack = Stack.create ();
- }
-
-let check_eof p v = p.check_eof <- v
-
-let pop s =
- try
- Stack.pop s.stack
- with
- Stack.Empty ->
- Xml_lexer.token s.source
-
-let push t s =
- Stack.push t s.stack
-
-let canonicalize l =
- let has_elt = List.exists (function Element _ -> true | _ -> false) l in
- if has_elt then List.filter (function PCData s -> not (is_blank s) | _ -> true) l
- else l
-
-let rec read_xml do_not_canonicalize s =
- let rec read_node s =
- match pop s with
- | Xml_lexer.PCData s -> PCData s
- | Xml_lexer.Tag (tag, attr, true) -> Element (tag, attr, [])
- | Xml_lexer.Tag (tag, attr, false) ->
- let elements = read_elems tag s in
- let elements =
- if do_not_canonicalize then elements else canonicalize elements
- in
- Element (tag, attr, elements)
- | t ->
- push t s;
- raise NoMoreData
-
- and read_elems tag s =
- let elems = ref [] in
- (try
- while true do
- let node = read_node s in
- match node, !elems with
- | PCData c , (PCData c2) :: q ->
- elems := PCData (c2 ^ c) :: q
- | _, l ->
- elems := node :: l
- done
- with
- NoMoreData -> ());
- match pop s with
- | Xml_lexer.Endtag s when s = tag -> List.rev !elems
- | t -> raise (Internal_error (EndOfTagExpected tag))
- in
- match read_node s with
- | (Element _) as node ->
- node
- | PCData c ->
- if is_blank c then
- read_xml do_not_canonicalize s
- else
- raise (Xml_lexer.Error Xml_lexer.ENodeExpected)
-
-let convert = function
- | Xml_lexer.EUnterminatedComment -> UnterminatedComment
- | Xml_lexer.EUnterminatedString -> UnterminatedString
- | Xml_lexer.EIdentExpected -> IdentExpected
- | Xml_lexer.ECloseExpected -> CloseExpected
- | Xml_lexer.ENodeExpected -> NodeExpected
- | Xml_lexer.EAttributeNameExpected -> AttributeNameExpected
- | Xml_lexer.EAttributeValueExpected -> AttributeValueExpected
- | Xml_lexer.EUnterminatedEntity -> UnterminatedEntity
-
-let error_of_exn xparser = function
- | NoMoreData when pop xparser = Xml_lexer.Eof -> Empty
- | NoMoreData -> NodeExpected
- | Internal_error e -> e
- | Xml_lexer.Error e -> convert e
- | e ->
- (*let e = Errors.push e in: We do not record backtrace here. *)
- raise e
-
-let do_parse do_not_canonicalize xparser =
- try
- Xml_lexer.init xparser.source;
- let x = read_xml do_not_canonicalize xparser in
- if xparser.check_eof && pop xparser <> Xml_lexer.Eof then raise (Internal_error EOFExpected);
- Xml_lexer.close ();
- x
- with any ->
- Xml_lexer.close ();
- raise (!xml_error (error_of_exn xparser any) xparser.source)
-
-let parse ?(do_not_canonicalize=false) p =
- do_parse do_not_canonicalize p
-
-let error_msg = function
- | UnterminatedComment -> "Unterminated comment"
- | UnterminatedString -> "Unterminated string"
- | UnterminatedEntity -> "Unterminated entity"
- | IdentExpected -> "Ident expected"
- | CloseExpected -> "Element close expected"
- | NodeExpected -> "Xml node expected"
- | AttributeNameExpected -> "Attribute name expected"
- | AttributeValueExpected -> "Attribute value expected"
- | EndOfTagExpected tag -> sprintf "End of tag expected : '%s'" tag
- | EOFExpected -> "End of file expected"
- | Empty -> "Empty"
-
-let error (msg,pos) =
- if pos.emin = pos.emax then
- sprintf "%s line %d character %d" (error_msg msg) pos.eline
- (pos.emin - pos.eline_start)
- else
- sprintf "%s line %d characters %d-%d" (error_msg msg) pos.eline
- (pos.emin - pos.eline_start) (pos.emax - pos.eline_start)
-
-let line e = e.eline
-
-let range e =
- e.emin - e.eline_start , e.emax - e.eline_start
-
-let abs_range e =
- e.emin , e.emax
-
-let pos source =
- let line, lstart, min, max = Xml_lexer.pos source in
- {
- eline = line;
- eline_start = lstart;
- emin = min;
- emax = max;
- }
-
-let () = _raises (fun x p ->
- (* local cast : Xml.error_msg -> error_msg *)
- Error (x, pos p))
- (fun f -> File_not_found f)
diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli
deleted file mode 100644
index ac2eab352..000000000
--- a/lib/xml_parser.mli
+++ /dev/null
@@ -1,106 +0,0 @@
-(*
- * Xml Light, an small Xml parser/printer with DTD support.
- * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License as published by the Free Software Foundation; either
- * version 2.1 of the License, or (at your option) any later version.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this library; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
- *)
-
-(** Xml Light Parser
-
- While basic parsing functions can be used in the {!Xml} module, this module
- is providing a way to create, configure and run an Xml parser.
-
-*)
-
-
-(** An Xml node is either
- [Element (tag-name, attributes, children)] or [PCData text] *)
-type xml = Xml_datatype.xml
-
-(** Abstract type for an Xml parser. *)
-type t
-
-(** {6:exc Xml Exceptions} *)
-
-(** Several exceptions can be raised when parsing an Xml document : {ul
- {li {!Xml.Error} is raised when an xml parsing error occurs. the
- {!Xml.error_msg} tells you which error occurred during parsing
- and the {!Xml.error_pos} can be used to retrieve the document
- location where the error occurred at.}
- {li {!Xml.File_not_found} is raised when an error occurred while
- opening a file with the {!Xml.parse_file} function.}
- }
- *)
-
-type error_pos
-
-type error_msg =
- | UnterminatedComment
- | UnterminatedString
- | UnterminatedEntity
- | IdentExpected
- | CloseExpected
- | NodeExpected
- | AttributeNameExpected
- | AttributeValueExpected
- | EndOfTagExpected of string
- | EOFExpected
- | Empty
-
-type error = error_msg * error_pos
-
-exception Error of error
-
-exception File_not_found of string
-
-(** Get a full error message from an Xml error. *)
-val error : error -> string
-
-(** Get the Xml error message as a string. *)
-val error_msg : error_msg -> string
-
-(** Get the line the error occurred at. *)
-val line : error_pos -> int
-
-(** Get the relative character range (in current line) the error occurred at.*)
-val range : error_pos -> int * int
-
-(** Get the absolute character range the error occurred at. *)
-val abs_range : error_pos -> int * int
-
-val pos : Lexing.lexbuf -> error_pos
-
-(** Several kind of resources can contain Xml documents. *)
-type source =
-| SChannel of in_channel
-| SString of string
-| SLexbuf of Lexing.lexbuf
-
-(** This function returns a new parser with default options. *)
-val make : source -> t
-
-(** When a Xml document is parsed, the parser may check that the end of the
- document is reached, so for example parsing ["<A/><B/>"] will fail instead
- of returning only the A element. You can turn on this check by setting
- [check_eof] to [true] {i (by default, check_eof is false, unlike
- in the original Xmllight)}. *)
-val check_eof : t -> bool -> unit
-
-(** Once the parser is configured, you can run the parser on a any kind
- of xml document source to parse its contents into an Xml data structure.
-
- When [do_not_canonicalize] is set, the XML document is given as
- is, without trying to remove blank PCDATA elements. *)
-val parse : ?do_not_canonicalize:bool -> t -> xml
diff --git a/lib/xml_printer.ml b/lib/xml_printer.ml
deleted file mode 100644
index e7e4d0ceb..000000000
--- a/lib/xml_printer.ml
+++ /dev/null
@@ -1,145 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Xml_datatype
-
-type xml = Xml_datatype.xml
-
-type target = TChannel of out_channel | TBuffer of Buffer.t
-
-type t = target
-
-let make x = x
-
-let buffer_pcdata tmp text =
- let output = Buffer.add_string tmp in
- let output' = Buffer.add_char tmp in
- let l = String.length text in
- for p = 0 to l-1 do
- match text.[p] with
- | ' ' -> output "&nbsp;";
- | '>' -> output "&gt;"
- | '<' -> output "&lt;"
- | '&' ->
- if p < l - 1 && text.[p + 1] = '#' then
- output' '&'
- else
- output "&amp;"
- | '\'' -> output "&apos;"
- | '"' -> output "&quot;"
- | c -> output' c
- done
-
-let buffer_attr tmp (n,v) =
- let output = Buffer.add_string tmp in
- let output' = Buffer.add_char tmp in
- output' ' ';
- output n;
- output "=\"";
- let l = String.length v in
- for p = 0 to l - 1 do
- match v.[p] with
- | '\\' -> output "\\\\"
- | '"' -> output "\\\""
- | '<' -> output "&lt;"
- | '&' -> output "&amp;"
- | c -> output' c
- done;
- output' '"'
-
-let to_buffer tmp x =
- let pcdata = ref false in
- let output = Buffer.add_string tmp in
- let output' = Buffer.add_char tmp in
- let rec loop = function
- | Element (tag,alist,[]) ->
- output' '<';
- output tag;
- List.iter (buffer_attr tmp) alist;
- output "/>";
- pcdata := false;
- | Element (tag,alist,l) ->
- output' '<';
- output tag;
- List.iter (buffer_attr tmp) alist;
- output' '>';
- pcdata := false;
- List.iter loop l;
- output "</";
- output tag;
- output' '>';
- pcdata := false;
- | PCData text ->
- if !pcdata then output' ' ';
- buffer_pcdata tmp text;
- pcdata := true;
- in
- loop x
-
-let pcdata_to_string s =
- let b = Buffer.create 13 in
- buffer_pcdata b s;
- Buffer.contents b
-
-let to_string x =
- let b = Buffer.create 200 in
- to_buffer b x;
- Buffer.contents b
-
-let to_string_fmt x =
- let tmp = Buffer.create 200 in
- let output = Buffer.add_string tmp in
- let output' = Buffer.add_char tmp in
- let rec loop ?(newl=false) tab = function
- | Element (tag, alist, []) ->
- output tab;
- output' '<';
- output tag;
- List.iter (buffer_attr tmp) alist;
- output "/>";
- if newl then output' '\n';
- | Element (tag, alist, [PCData text]) ->
- output tab;
- output' '<';
- output tag;
- List.iter (buffer_attr tmp) alist;
- output ">";
- buffer_pcdata tmp text;
- output "</";
- output tag;
- output' '>';
- if newl then output' '\n';
- | Element (tag, alist, l) ->
- output tab;
- output' '<';
- output tag;
- List.iter (buffer_attr tmp) alist;
- output ">\n";
- List.iter (loop ~newl:true (tab^" ")) l;
- output tab;
- output "</";
- output tag;
- output' '>';
- if newl then output' '\n';
- | PCData text ->
- buffer_pcdata tmp text;
- if newl then output' '\n';
- in
- loop "" x;
- Buffer.contents tmp
-
-let print t xml =
- let tmp, flush = match t with
- | TChannel oc ->
- let b = Buffer.create 200 in
- b, (fun () -> Buffer.output_buffer oc b; flush oc)
- | TBuffer b ->
- b, (fun () -> ())
- in
- to_buffer tmp xml;
- flush ()
diff --git a/lib/xml_printer.mli b/lib/xml_printer.mli
deleted file mode 100644
index f24f51fff..000000000
--- a/lib/xml_printer.mli
+++ /dev/null
@@ -1,29 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-type xml = Xml_datatype.xml
-
-type t
-type target = TChannel of out_channel | TBuffer of Buffer.t
-
-val make : target -> t
-
-(** Print the xml data structure to a source into a compact xml string (without
- any user-readable formating ). *)
-val print : t -> xml -> unit
-
-(** Print the xml data structure into a compact xml string (without
- any user-readable formating ). *)
-val to_string : xml -> string
-
-(** Print the xml data structure into an user-readable string with
- tabs and lines break between different nodes. *)
-val to_string_fmt : xml -> string
-
-(** Print PCDATA as a string by escaping XML entities. *)
-val pcdata_to_string : string -> string