diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/aux_file.ml | 9 | ||||
| -rw-r--r-- | lib/aux_file.mli | 3 | ||||
| -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.ml | 83 | ||||
| -rw-r--r-- | lib/cList.mli | 10 | ||||
| -rw-r--r-- | lib/cMap.ml | 50 | ||||
| -rw-r--r-- | lib/cMap.mli | 21 | ||||
| -rw-r--r-- | lib/cSig.mli | 4 | ||||
| -rw-r--r-- | lib/cWarnings.ml | 120 | ||||
| -rw-r--r-- | lib/cWarnings.mli | 34 | ||||
| -rw-r--r-- | lib/clib.mllib | 7 | ||||
| -rw-r--r-- | lib/dyn.ml | 134 | ||||
| -rw-r--r-- | lib/dyn.mli | 58 | ||||
| -rw-r--r-- | lib/envars.ml | 27 | ||||
| -rw-r--r-- | lib/envars.mli | 13 | ||||
| -rw-r--r-- | lib/explore.ml | 2 | ||||
| -rw-r--r-- | lib/feedback.ml | 265 | ||||
| -rw-r--r-- | lib/feedback.mli | 105 | ||||
| -rw-r--r-- | lib/flags.ml | 43 | ||||
| -rw-r--r-- | lib/flags.mli | 15 | ||||
| -rw-r--r-- | lib/future.ml | 25 | ||||
| -rw-r--r-- | lib/future.mli | 3 | ||||
| -rw-r--r-- | lib/genarg.ml | 319 | ||||
| -rw-r--r-- | lib/genarg.mli | 182 | ||||
| -rw-r--r-- | lib/hMap.ml | 116 | ||||
| -rw-r--r-- | lib/hashcons.ml | 31 | ||||
| -rw-r--r-- | lib/hashset.ml | 2 | ||||
| -rw-r--r-- | lib/heap.ml | 2 | ||||
| -rw-r--r-- | lib/iStream.ml | 6 | ||||
| -rw-r--r-- | lib/lib.mllib | 5 | ||||
| -rw-r--r-- | lib/loc.ml | 5 | ||||
| -rw-r--r-- | lib/loc.mli | 17 | ||||
| -rw-r--r-- | lib/minisys.ml | 74 | ||||
| -rw-r--r-- | lib/option.ml | 4 | ||||
| -rw-r--r-- | lib/option.mli | 16 | ||||
| -rw-r--r-- | lib/pp.ml | 243 | ||||
| -rw-r--r-- | lib/pp.mli | 143 | ||||
| -rw-r--r-- | lib/ppstyle.ml | 45 | ||||
| -rw-r--r-- | lib/ppstyle.mli | 14 | ||||
| -rw-r--r-- | lib/profile.ml | 2 | ||||
| -rw-r--r-- | lib/remoteCounter.ml | 4 | ||||
| -rw-r--r-- | lib/richpp.ml | 30 | ||||
| -rw-r--r-- | lib/richpp.mli | 23 | ||||
| -rw-r--r-- | lib/serialize.ml | 116 | ||||
| -rw-r--r-- | lib/serialize.mli | 37 | ||||
| -rw-r--r-- | lib/spawn.ml | 18 | ||||
| -rw-r--r-- | lib/stateid.ml | 26 | ||||
| -rw-r--r-- | lib/stateid.mli | 11 | ||||
| -rw-r--r-- | lib/system.ml | 123 | ||||
| -rw-r--r-- | lib/system.mli | 38 | ||||
| -rw-r--r-- | lib/unicode.ml | 77 | ||||
| -rw-r--r-- | lib/unicode.mli | 20 | ||||
| -rw-r--r-- | lib/util.ml | 30 | ||||
| -rw-r--r-- | lib/util.mli | 20 | ||||
| -rw-r--r-- | lib/xml_lexer.mli | 44 | ||||
| -rw-r--r-- | lib/xml_lexer.mll | 317 | ||||
| -rw-r--r-- | lib/xml_parser.ml | 232 | ||||
| -rw-r--r-- | lib/xml_parser.mli | 106 | ||||
| -rw-r--r-- | lib/xml_printer.ml | 145 | ||||
| -rw-r--r-- | lib/xml_printer.mli | 29 |
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 @@ -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 " "; - | '>' -> output ">" - | '<' -> output "<" - | '&' -> - if p < l - 1 && text.[p + 1] = '#' then - output' '&' - else - output "&" - | '\'' -> output "'" - | '"' -> output """ - | 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 "<" - | '&' -> output "&" - | 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 |