diff options
Diffstat (limited to 'lib')
47 files changed, 700 insertions, 1947 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml index f7bd81f85d..096305b987 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 @@ -88,7 +88,7 @@ let load_aux_file_for vfile = | 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); + Feedback.msg_warning 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 127827ab6a..86e322b71d 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/ephemeron.ml b/lib/cEphemeron.ml index a38ea11e10..a38ea11e10 100644 --- a/lib/ephemeron.ml +++ b/lib/cEphemeron.ml diff --git a/lib/ephemeron.mli b/lib/cEphemeron.mli index 1200e4e208..1200e4e208 100644 --- a/lib/ephemeron.mli +++ b/lib/cEphemeron.mli diff --git a/lib/cSet.ml b/lib/cSet.ml index 3eeff29fe1..037cdc3568 100644 --- a/lib/cSet.ml +++ b/lib/cSet.ml @@ -57,7 +57,7 @@ struct open Hashset.Combine type t = set type u = M.t -> M.t - let equal s1 s2 = s1 == s2 || eqeq (spine s1 []) (spine s2 []) + let eq s1 s2 = s1 == s2 || eqeq (spine s1 []) (spine s2 []) let hash s = Set.fold (fun v accu -> combine (H.hash v) accu) s 0 let hashcons = umap end diff --git a/lib/clib.mllib b/lib/clib.mllib index 3c1c5da33c..1e33173ee1 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -21,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 676467e464..65d1442ac6 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -11,7 +11,7 @@ sig type 'a t end -module type S = +module type PreS = sig type 'a tag type t = Dyn : 'a tag * 'a -> t @@ -44,10 +44,23 @@ sig end val dump : unit -> (int * string) list + end -module Make(M : CSig.EmptyS) = -struct +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 'a tag = int @@ -108,3 +121,28 @@ 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 c94fa764ba..448b11a18f 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -6,7 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Dynamics. Use with extreme care. Not for kids. *) +(** Dynamically typed values *) + module type TParam = sig type 'a t @@ -46,6 +47,16 @@ end 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 *) diff --git a/lib/errors.ml b/lib/errors.ml index c1d224dfcd..8982dde148 100644 --- a/lib/errors.ml +++ b/lib/errors.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) diff --git a/lib/explore.ml b/lib/explore.ml index 587db11563..aa7bddf2b4 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 1a90685de6..d6f580fd16 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -7,51 +7,14 @@ (************************************************************************) open Xml_datatype -open Serialize -type message_level = +type level = | Debug of string | Info | Notice | Warning | Error -type message = { - message_level : message_level; - message_content : xml; -} - -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_xml 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_xml 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 @@ -71,8 +34,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 + (* Old generic messages *) + | Message of level * Richpp.richpp type feedback = { id : edit_or_state_id; @@ -80,92 +45,127 @@ 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 = 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 s = quoter (hov 0 (info ++ s)) + +(* Generic logger *) +let gen_logger dbg err level msg = match level with + | Debug _ -> msgnl (make_body dbg dbg_str msg) + | Info -> msgnl (make_body dbg info_str msg) + | Notice -> msgnl msg + | Warning -> Flags.if_warn (fun () -> + msgnl_with !err_ft (make_body err warn_str msg)) () + | Error -> msgnl_with !err_ft (make_body err err_str msg) + +(** Standard loggers *) +let std_logger = gen_logger (fun x -> x) (fun x -> x) + +(* Color logger *) +let color_terminal_logger level strm = + let msg = Ppstyle.color_msg in + match level with + | Debug _ -> msg ~header:("Debug", Ppstyle.debug_tag) !std_ft strm + | Info -> msg !std_ft strm + | Notice -> msg !std_ft strm + | Warning -> + let header = ("Warning", Ppstyle.warning_tag) in + Flags.if_warn (fun () -> msg ~header !err_ft strm) () + | Error -> msg ~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 x = !logger Info x +let msg_notice x = !logger Notice x +let msg_warning x = !logger Warning x +let msg_error x = !logger Error x +let msg_debug x = !logger (Debug "_") x + +(** Feeders *) +let feeder = ref ignore +let set_feeder f = feeder := f + +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 = + !feeder { + contents = what; + route = Option.default !feedback_route route; + id = Option.default !feedback_id id; + } + +let feedback_logger lvl msg = + feedback ~route:!feedback_route ~id:!feedback_id + (Message (lvl, Richpp.richpp_of_pp msg)) + +(* Output to file *) +let ft_logger old_logger ft 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 level mesg + | Error -> old_logger 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 0d8e20230d..50ffd22db9 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 = +type level = | Debug of string | Info | Notice | Warning | Error -type message = { - message_level : message_level; - message_content : xml; -} - -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 @@ -54,15 +46,88 @@ type feedback_content = (* Extra metadata *) | Custom of Loc.t * string * xml (* Old generic messages *) - | Message of message + | Message of level * 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 = 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 + + +(** [set_feeder] A feeder processes the feedback, [ignore] by default *) +val set_feeder : (feedback -> unit) -> 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 : Pp.std_ppcmds -> unit +(** Message that displays information, usually in verbose mode, such as [Foobar + is defined] *) + +val msg_notice : Pp.std_ppcmds -> unit +(** Message that should be displayed, such as [Print Foo] or [Show Bar]. *) + +val msg_warning : Pp.std_ppcmds -> unit +(** Message indicating that something went wrong, but without serious + consequences. *) + +val msg_error : Pp.std_ppcmds -> unit +(** Message indicating that something went really wrong, though still + recoverable; otherwise an exception would have been raised. *) + +val msg_debug : Pp.std_ppcmds -> unit +(** For debugging purposes *) + + + diff --git a/lib/flags.ml b/lib/flags.ml index c1ec9738ca..ba19c7a63b 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 @@ -220,6 +225,7 @@ let native_compiler = ref false let print_mod_uid = ref false let tactic_context_compat = ref false +let profile_ltac = ref false let dump_bytecode = ref false let set_dump_bytecode = (:=) dump_bytecode diff --git a/lib/flags.mli b/lib/flags.mli index 24780f0dcc..8fe64d24fa 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 @@ -143,6 +148,8 @@ 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 + (** 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 ff16286c4f..9cdc1c20e3 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -63,7 +63,7 @@ and 'a comp = | Exn of Exninfo.iexn (* Invariant: this exception is always "fixed" as in fix_exn *) and 'a comput = - | Ongoing of string * (UUID.t * fix_exn * 'a comp ref) Ephemeron.key + | Ongoing of string * (UUID.t * fix_exn * 'a comp ref) CEphemeron.key | Finished of 'a and 'a computation = 'a comput ref @@ -71,13 +71,13 @@ and 'a computation = 'a comput ref let unnamed = "unnamed" let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x = - ref (Ongoing (name, Ephemeron.create (uuid, f, Pervasives.ref x))) + ref (Ongoing (name, CEphemeron.create (uuid, f, Pervasives.ref x))) let get x = match !x with | Finished v -> unnamed, UUID.invalid, id, ref (Val (v,None)) | Ongoing (name, x) -> - try let uuid, fix, c = Ephemeron.get x in name, uuid, fix, c - with Ephemeron.InvalidKey -> + try let uuid, fix, c = CEphemeron.get x in name, uuid, fix, c + with CEphemeron.InvalidKey -> name, UUID.invalid, id, ref (Exn (NotHere name, Exninfo.null)) type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn ] diff --git a/lib/genarg.ml b/lib/genarg.ml index c7273ac93e..69408fb1a5 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -9,83 +9,30 @@ open Pp open Util -module ValT = Dyn.Make(struct end) -module ArgT = Dyn.Make(struct end) - -module Val = +module ArgT = struct - - type 'a typ = 'a ValT.tag - - type _ tag = - | Base : 'a typ -> 'a tag - | List : 'a tag -> 'a list tag - | Opt : 'a tag -> 'a option tag - | Pair : 'a tag * 'b tag -> ('a * 'b) tag - - type t = Dyn : 'a tag * 'a -> t - - let rec eq : type a b. a tag -> b tag -> (a, b) CSig.eq option = - fun t1 t2 -> match t1, t2 with - | Base t1, Base t2 -> ValT.eq t1 t2 - | List t1, List t2 -> - begin match eq t1 t2 with - | None -> None - | Some Refl -> Some Refl - end - | Opt t1, Opt t2 -> - begin match eq t1 t2 with - | None -> None - | Some Refl -> Some Refl - end - | Pair (t1, u1), Pair (t2, u2) -> - begin match eq t1 t2 with - | None -> None - | Some Refl -> - match eq u1 u2 with - | None -> None - | Some Refl -> Some Refl - end - | _ -> None - - let rec repr : type a. a tag -> std_ppcmds = function - | Base t -> str (ValT.repr t) - | List t -> repr t ++ spc () ++ str "list" - | Opt t -> repr t ++ spc () ++ str "option" - | Pair (t1, t2) -> str "(" ++ repr t1 ++ str " * " ++ repr t2 ++ str ")" - + 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 argument_type = - (* Specific types *) - | 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 -| 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 -| 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 (_, _, _) genarg_type = -| ExtraArg : ('a * 'b * 'c) ArgT.tag -> ('a, 'b, 'c) 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 = @@ -111,6 +58,22 @@ fun t1 t2 -> match t1, t2 with 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 *) @@ -120,11 +83,6 @@ type rlevel = [ `rlevel ] type glevel = [ `glevel ] type tlevel = [ `tlevel ] -type _ level = -| Rlevel : rlevel level -| Glevel : glevel level -| Tlevel : tlevel 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 @@ -177,16 +135,10 @@ let has_type (GenArg (t, v)) u = match abstract_argument_type_eq t u with | None -> false | Some _ -> true -let rec untype : type a b c. (a, b, c) genarg_type -> argument_type = function -| ExtraArg t -> ExtraArgType (ArgT.repr t) -| ListArg t -> ListArgType (untype t) -| OptArg t -> OptArgType (untype t) -| PairArg (t1, t2) -> PairArgType (untype t1, untype t2) - let unquote : type l. (_, l) abstract_argument_type -> _ = function -| Rawwit t -> untype t -| Glbwit t -> untype t -| Topwit t -> untype t +| Rawwit t -> ArgumentType t +| Glbwit t -> ArgumentType t +| Topwit t -> ArgumentType t let genarg_tag (GenArg (t, _)) = unquote t @@ -194,48 +146,6 @@ 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 = -| Rcast : 'a -> ('a, 'b, 'c, rlevel) cast -| Gcast : 'b -> ('a, 'b, 'c, glevel) cast -| Tcast : 'c -> ('a, 'b, 'c, tlevel) cast - -let raw : ('a, 'b, 'c, rlevel) cast -> _ = function Rcast x -> x -let glb : ('a, 'b, 'c, glevel) cast -> _ = function Gcast x -> x -let top : ('a, 'b, 'c, tlevel) cast -> _ = function Tcast x -> x - -(** 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 (type l) (pack : (_, l) list_unpacker) (GenArg (t, obj) : l generic_argument) = match t with -| Rawwit (ListArg t) -> pack.list_unpacker t (Rcast obj) -| Glbwit (ListArg t) -> pack.list_unpacker t (Gcast obj) -| Topwit (ListArg t) -> pack.list_unpacker t (Tcast 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 (type l) (pack : (_, l) opt_unpacker) (GenArg (t, obj) : l generic_argument) = match t with -| Rawwit (OptArg t) -> pack.opt_unpacker t (Rcast obj) -| Glbwit (OptArg t) -> pack.opt_unpacker t (Gcast obj) -| Topwit (OptArg t) -> pack.opt_unpacker t (Tcast 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 (type l) (pack : (_, l) pair_unpacker) (GenArg (t, obj) : l generic_argument) = match t with -| Rawwit (PairArg (t1, t2)) -> pack.pair_unpacker t1 t2 (Rcast obj) -| Glbwit (PairArg (t1, t2)) -> pack.pair_unpacker t1 t2 (Gcast obj) -| Topwit (PairArg (t1, t2)) -> pack.pair_unpacker t1 t2 (Tcast obj) -| _ -> failwith "out_gen" - (** Creating args *) module type Param = sig type ('raw, 'glb, 'top) t end @@ -245,48 +155,14 @@ struct include ArgT.Map(struct type 'a t = 'a pack end) end -type ('raw, 'glb, 'top) load = { - nil : 'raw option; - dyn : 'top Val.tag; -} - -module LoadMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) load end) - -let arg0_map = ref LoadMap.empty - -let create_arg opt ?dyn name = +let create_arg name = match ArgT.name name with + | None -> ExtraArg (ArgT.create name) | Some _ -> Errors.anomaly (str "generic argument already declared: " ++ str name) - | None -> - let dyn = match dyn with None -> Val.Base (ValT.create name) | Some dyn -> dyn in - let obj = LoadMap.Pack { nil = opt; dyn; } in - let name = ArgT.create name in - let () = arg0_map := LoadMap.add name obj !arg0_map in - ExtraArg name let make0 = create_arg -let rec default_empty_value : type a b c. (a, b, c) genarg_type -> a option = function -| ListArg _ -> Some [] -| OptArg _ -> Some None -| PairArg (t1, t2) -> - begin match default_empty_value t1, default_empty_value t2 with - | Some v1, Some v2 -> Some (v1, v2) - | _ -> None - end -| ExtraArg s -> - match LoadMap.find s !arg0_map with LoadMap.Pack obj -> obj.nil - -let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function -| ListArg t -> Val.List (val_tag t) -| OptArg t -> Val.Opt (val_tag t) -| PairArg (t1, t2) -> Val.Pair (val_tag t1, val_tag t2) -| ExtraArg s -> - match LoadMap.find s !arg0_map with LoadMap.Pack obj -> obj.dyn - -let val_tag = function Topwit t -> val_tag t - (** Registering genarg-manipulating functions *) module type GenObj = @@ -326,17 +202,3 @@ struct | _ -> assert false end - -(** Hackish part *) - -let arg0_names = ref (String.Map.empty : string String.Map.t) - -let register_name0 t name = match t with -| ExtraArg s -> - let s = ArgT.repr s in - 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 diff --git a/lib/genarg.mli b/lib/genarg.mli index ce0536cf49..d7ad9b93b4 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,107 +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} *) module ArgT : sig - type 'a tag - val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option - val repr : 'a tag -> string - type any = Any : 'a tag -> any + 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 +| 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 -(** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized - one, and ['top] the internalized one. *) - -module Val : -sig - type 'a typ - - type _ tag = - | Base : 'a typ -> 'a tag - | List : 'a tag -> 'a list tag - | Opt : 'a tag -> 'a option tag - | Pair : 'a tag * 'b tag -> ('a * 'b) tag - - type t = Dyn : 'a tag * 'a -> t - - val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option - val repr: 'a tag -> Pp.std_ppcmds - -end -(** Dynamic types for toplevel values. While the generic types permit to relate - objects at various levels of interpretation, toplevel values are wearing - their own type regardless of where they came from. This allows to use the - same runtime representation for several generic types. *) type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type (** Alias for concision when the three types agree. *) -val make0 : 'raw option -> ?dyn:'top Val.tag -> 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 -> ?dyn:'top Val.tag -> 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 = [ `rlevel ] type glevel = [ `glevel ] type tlevel = [ `tlevel ] +(** 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 at level ['co] represented by an OCaml value of type ['a]. *) type 'a raw_abstract_argument_type = ('a, rlevel) abstract_argument_type (** Specialized type at raw level. *) @@ -179,20 +131,9 @@ 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 Dynamic toplevel values} *) - -val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag -(** Retrieve the dynamic type associated to a toplevel genarg. Only works for - ground generic arguments. *) - (** {6 Type reification} *) -type argument_type = - (** Specific types *) - | 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} *) @@ -239,23 +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. *) diff --git a/lib/hashcons.ml b/lib/hashcons.ml index b5192dbb8c..4eaacf9145 100644 --- a/lib/hashcons.ml +++ b/lib/hashcons.ml @@ -15,7 +15,7 @@ * of objects of type t (u usually has the form (t1->t1)*(t2->t2)*...). * [hashcons u x] is a function that hash-cons the sub-structures of x using * the hash-consing functions u provides. - * [equal] is a comparison function. It is allowed to use physical equality + * [eq] is a comparison function. It is allowed to use physical equality * on the sub-terms hash-consed by the hashcons function. * [hash] is the hash function given to the Hashtbl.Make function * @@ -27,7 +27,7 @@ module type HashconsedType = type t type u val hashcons : u -> t -> t - val equal : t -> t -> bool + val eq : t -> t -> bool val hash : t -> int end @@ -53,7 +53,7 @@ module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) = (* We create the type of hashtables for t, with our comparison fun. * An invariant is that the table never contains two entries equals - * w.r.t (=), although the equality on keys is X.equal. This is + * w.r.t (=), although the equality on keys is X.eq. This is * granted since we hcons the subterms before looking up in the table. *) module Htbl = Hashset.Make(X) @@ -110,7 +110,7 @@ module Hlist (D:HashedType) = let hashcons (hrec,hdata) = function | x :: l -> hdata x :: hrec l | l -> l - let equal l1 l2 = + let eq l1 l2 = l1 == l2 || match l1, l2 with | [], [] -> true @@ -130,7 +130,7 @@ module Hstring = Make( type t = string type u = unit let hashcons () s =(* incr accesstr;*) s - external equal : string -> string -> bool = "caml_string_equal" "noalloc" + external eq : string -> string -> bool = "caml_string_equal" "noalloc" (** Copy from CString *) let rec hash len s i accu = if i = len then accu @@ -177,6 +177,6 @@ module Hobj = Make( type t = Obj.t type u = (Obj.t -> Obj.t) * unit let hashcons (hrec,_) = hash_obj hrec - let equal = comp_obj + let eq = comp_obj let hash = Hashtbl.hash end) diff --git a/lib/hashcons.mli b/lib/hashcons.mli index 04754ba1db..150899cef5 100644 --- a/lib/hashcons.mli +++ b/lib/hashcons.mli @@ -14,9 +14,9 @@ module type HashconsedType = sig (** {6 Generic hashconsing signature} - Given an equivalence relation [equal], a hashconsing function is a + Given an equivalence relation [eq], a hashconsing function is a function that associates the same canonical element to two elements - related by [equal]. Usually, the element chosen is canonical w.r.t. + related by [eq]. Usually, the element chosen is canonical w.r.t. physical equality [(==)], so as to reduce memory consumption and enhance efficiency of equality tests. @@ -32,15 +32,15 @@ module type HashconsedType = Usually a tuple of functions. *) val hashcons : u -> t -> t (** The actual hashconsing function, using its fist argument to recursively - hashcons substructures. It should be compatible with [equal], that is - [equal x (hashcons f x) = true]. *) - val equal : t -> t -> bool + hashcons substructures. It should be compatible with [eq], that is + [eq x (hashcons f x) = true]. *) + val eq : t -> t -> bool (** A comparison function. It is allowed to use physical equality on the sub-terms hashconsed by the [hashcons] function, but it should be insensible to shallow copy of the compared object. *) val hash : t -> int (** A hash function passed to the underlying hashtable structure. [hash] - should be compatible with [equal], i.e. if [equal x y = true] then + should be compatible with [eq], i.e. if [eq x y = true] then [hash x = hash y]. *) end diff --git a/lib/hashset.ml b/lib/hashset.ml index b2795c6b1f..af33544dc6 100644 --- a/lib/hashset.ml +++ b/lib/hashset.ml @@ -16,7 +16,7 @@ module type EqType = sig type t - val equal : t -> t -> bool + val eq : t -> t -> bool end type statistics = { @@ -183,7 +183,7 @@ module Make (E : EqType) = if i >= sz then ifnotfound index else if h = hashes.(i) then begin match Weak.get bucket i with - | Some v when E.equal v d -> v + | Some v when E.eq v d -> v | _ -> loop (i + 1) end else loop (i + 1) in diff --git a/lib/hashset.mli b/lib/hashset.mli index 05d4fe379a..733c89621c 100644 --- a/lib/hashset.mli +++ b/lib/hashset.mli @@ -16,7 +16,7 @@ module type EqType = sig type t - val equal : t -> t -> bool + val eq : t -> t -> bool end type statistics = { diff --git a/lib/iStream.ml b/lib/iStream.ml index c9f4d4a111..26a666e176 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 a9181c51c1..a6c09058dd 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -3,6 +3,7 @@ Bigint Segmenttree Unicodetable Unicode +Minisys System CThread Spawn @@ -14,6 +15,6 @@ Rtree Heap Unionfind Genarg -Ephemeron +CEphemeron Future RemoteCounter diff --git a/lib/minisys.ml b/lib/minisys.ml new file mode 100644 index 0000000000..25e4d79c4e --- /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 @@ -57,24 +57,13 @@ module Dyn = Dyn.Make(struct end) type t = Dyn.t type 'a key = 'a Dyn.tag let create = Dyn.create -let inj x k = Dyn.Dyn (k, x) -let prj : type a. t -> a key -> a option = fun dyn k -> - let Dyn.Dyn (k', x) = dyn in - match Dyn.eq k k' with - | None -> None - | Some CSig.Refl -> Some x +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; @@ -261,7 +250,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)) @@ -290,29 +279,29 @@ 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 ())) + com_if ft (Lazy.from_fun(fun()->Format.pp_print_if_newline ft ())) | Ppcmd_comment i -> let coms = split_com [] [] i !comments in (* Format.pp_open_hvbox ft 0;*) @@ -343,181 +332,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 : Xml_datatype.xml; -} - -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 printer = logger := (fun ~id lvl msg -> - !feeder { - Feedback.contents = Feedback.Message { - message_level = lvl; - message_content = printer 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 @@ -600,3 +438,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 015151bc90..a18744c376 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -6,32 +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 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 (** {6 Manipulation commands} *) @@ -100,87 +92,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 : Xml_datatype.xml; -} - -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 : (std_ppcmds -> Xml_datatype.xml) -> 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 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. *) - -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 +114,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 +166,13 @@ 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]. } *) - -(** 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 bb73fbdf56..b068788c92 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,23 @@ 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 ?header ft strm = let pptag = tag in let open Pp in - let msg ?header ft strm = - let strm = match header with + let strm = match header with | None -> hov 0 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 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 97b5869f9b..1cd701ed4e 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 : ?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/richpp.ml b/lib/richpp.ml index fe3edd99ca..a98273edb2 100644 --- a/lib/richpp.ml +++ b/lib/richpp.ml @@ -194,7 +194,3 @@ let raw_print xml = let () = print xml in Buffer.contents buf -let of_richpp x = Element ("richpp", [], [x]) -let to_richpp xml = match xml with -| Element ("richpp", [], [x]) -> x -| _ -> raise Serialize.Marshal_error diff --git a/lib/richpp.mli b/lib/richpp.mli index 807d52aba4..287d265a8f 100644 --- a/lib/richpp.mli +++ b/lib/richpp.mli @@ -57,10 +57,7 @@ val richpp_of_string : string -> richpp val repr : richpp -> Xml_datatype.xml (** Observe the styled text as XML *) -(** {5 Serialization} *) - -val of_richpp : richpp -> Xml_datatype.xml -val to_richpp : Xml_datatype.xml -> richpp +(** {5 Debug/Compat} *) (** Represent the semi-structured document as a string, dropping any additional information. *) diff --git a/lib/serialize.ml b/lib/serialize.ml deleted file mode 100644 index 685ec6049c..0000000000 --- a/lib/serialize.ml +++ /dev/null @@ -1,120 +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 - -let of_xml x = Element ("xml", [], [x]) -let to_xml xml = match xml with -| Element ("xml", [], [x]) -> x -| _ -> raise Marshal_error diff --git a/lib/serialize.mli b/lib/serialize.mli deleted file mode 100644 index d7c14e7e73..0000000000 --- a/lib/serialize.mli +++ /dev/null @@ -1,39 +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 -val of_xml : xml -> xml -val to_xml : xml -> xml diff --git a/lib/spawn.ml b/lib/spawn.ml index 4d35ded90f..2b9c4ccac1 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -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 @@ -220,10 +206,13 @@ let stats { oob_req; oob_resp; alive } = input_value oob_resp let rec wait p = - try snd (Unix.waitpid [] p.pid) - with - | Unix.Unix_error (Unix.EINTR, _, _) -> wait p - | Unix.Unix_error _ -> Unix.WEXITED 0o400 + (* On windows kill is not reliable, so wait may never return. *) + if Sys.os_type = "Unix" then + try snd (Unix.waitpid [] p.pid) + with + | Unix.Unix_error (Unix.EINTR, _, _) -> wait p + | Unix.Unix_error _ -> Unix.WEXITED 0o400 + else Unix.WEXITED 0o400 end @@ -267,8 +256,13 @@ let stats { oob_req; oob_resp; alive } = flush oob_req; let RespStats g = input_value oob_resp in g -let wait { pid = unixpid } = - try snd (Unix.waitpid [] unixpid) - with Unix.Unix_error _ -> Unix.WEXITED 0o400 +let rec wait p = + (* On windows kill is not reliable, so wait may never return. *) + if Sys.os_type = "Unix" then + try snd (Unix.waitpid [] p.pid) + with + | Unix.Unix_error (Unix.EINTR, _, _) -> wait p + | Unix.Unix_error _ -> Unix.WEXITED 0o400 + else Unix.WEXITED 0o400 end diff --git a/lib/stateid.ml b/lib/stateid.ml index 59cf206e2e..500581a39e 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 2c12c30c3c..cd8fddf0ce 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 13cfad4aef..8b53a11d67 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -12,63 +12,7 @@ open Pp open Errors open Util -(** 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 process_directory f path = - Array.iter (apply_subdir f path) (Sys.readdir path) - -let process_subdirectories f path = - let f = function FileDir (path,base) -> f path base | FileRegular _ -> () in - process_directory f path +include Minisys (** Returns the list of all recursive subdirectories of [root] in depth-first search, with sons ordered as on the file system; @@ -86,9 +30,9 @@ let all_subdirs ~unix_path:root = | _ -> () in process_directory f path in - check_unix_dir (fun s -> msg_warning (str s)) root; + check_unix_dir (fun s -> Feedback.msg_warning (str s)) root; if exists_dir root then traverse root [] - else msg_warning (str ("Cannot open " ^ root)); + else Feedback.msg_warning (str ("Cannot open " ^ root)); List.rev !l (* Caching directory contents for efficient syntactic equality of file @@ -106,7 +50,7 @@ let dirmap = ref StrMap.empty let make_dir_table dir = let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in - Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir) + Array.fold_left filter_dotfiles StrSet.empty (readdir dir) let exists_in_dir_respecting_case dir bf = let cache_dir dir = @@ -147,7 +91,7 @@ let where_in_path ?(warn=true) path filename = | (lpe, f) :: l' -> let () = match l' with | _ :: _ when warn -> - msg_warning + Feedback.msg_warning (str filename ++ str " has been found in" ++ spc () ++ hov 0 (str "[ " ++ hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon()) @@ -203,7 +147,7 @@ let is_in_system_path filename = 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"); + Feedback.msg_warning (str "system variable PATH not found"); false let open_trapping_failure name = @@ -214,7 +158,7 @@ let open_trapping_failure name = let try_remove filename = try Sys.remove filename with e when Errors.noncritical e -> - msg_warning + Feedback.msg_warning (str"Could not remove file " ++ str filename ++ str" which is corrupted!") let error_corrupted file s = @@ -262,7 +206,8 @@ let skip_in_segment f ch = seek_in ch stop; stop, digest_in f ch -exception Bad_magic_number of string +type magic_number_error = {filename: string; actual: int; expected: int} +exception Bad_magic_number of magic_number_error let raw_extern_state magic filename = let channel = open_trapping_failure filename in @@ -272,8 +217,12 @@ let raw_extern_state magic filename = let raw_intern_state magic filename = try let channel = open_in_bin filename in - if not (Int.equal (input_binary_int filename channel) magic) then - raise (Bad_magic_number filename); + let actual_magic = input_binary_int filename channel in + if not (Int.equal actual_magic magic) then + raise (Bad_magic_number { + filename=filename; + actual=actual_magic; + expected=magic}); channel with | End_of_file -> error_corrupted filename "premature end of file" @@ -303,9 +252,11 @@ let intern_state magic filename = let with_magic_number_check f a = try f a - with Bad_magic_number fname -> + with Bad_magic_number {filename=fname;actual=actual;expected=expected} -> errorlabstrm "with_magic_number_check" - (str"File " ++ str fname ++ strbrk" has bad magic number." ++ spc () ++ + (str"File " ++ str fname ++ strbrk" has bad magic number " ++ + int actual ++ str" (expected " ++ int expected ++ str")." ++ + spc () ++ strbrk "It is corrupted or was compiled with another version of Coq.") (* Time stamps. *) @@ -336,13 +287,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 e1190dfb55..4dbb3695d2 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -64,9 +64,11 @@ val file_exists_respecting_case : string -> string -> bool (** {6 I/O functions } *) (** Generic input and output functions, parameterized by a magic number and a suffix. The intern functions raise the exception [Bad_magic_number] - when the check fails, with the full file name. *) + when the check fails, with the full file name and expected/observed magic + numbers. *) -exception Bad_magic_number of string +type magic_number_error = {filename: string; actual: int; expected: int} +exception Bad_magic_number of magic_number_error val raw_extern_state : int -> string -> out_channel diff --git a/lib/unicode.ml b/lib/unicode.ml index 05998bb804..dc852d9819 100644 --- a/lib/unicode.ml +++ b/lib/unicode.ml @@ -173,6 +173,13 @@ let next_utf8 s i = (c land 0x3F) lsl 6 + (d land 0x3F) else err () +let is_utf8 s = + let rec check i = + let (off, _) = next_utf8 s i in + check (i + off) + in + try check 0 with End_of_input -> true | Invalid_argument _ -> false + (* Check the well-formedness of an identifier *) let initial_refutation j n s = @@ -233,14 +240,94 @@ let is_basic_ascii s = !ok let ascii_of_ident s = - if is_basic_ascii s then s else - let i = ref 0 and out = ref "" in - begin try while true do + let len = String.length s in + let has_UU i = + i+2 < len && s.[i]='_' && s.[i+1]='U' && s.[i+2]='U' + in + let i = ref 0 in + while !i < len && Char.code s.[!i] < 128 && not (has_UU !i) do + incr i + done; + if !i = len then s else + let out = Buffer.create (2*len) in + Buffer.add_substring out s 0 !i; + while !i < len do let j, n = next_utf8 s !i in - out := - if n >= 128 - then Printf.sprintf "%s__U%04x_" !out n - else Printf.sprintf "%s%c" !out s.[!i]; - i := !i + j - done with End_of_input -> () end; - !out + if n >= 128 then + (Printf.bprintf out "_UU%04x_" n; i := !i + j) + else if has_UU !i then + (Buffer.add_string out "_UUU"; i := !i + 3) + else + (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 72d1f29504..1f8bd44eee 100644 --- a/lib/unicode.mli +++ b/lib/unicode.mli @@ -27,12 +27,22 @@ val ident_refutation : string -> (bool * string) option @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 ASCII characters. - Returns [false] otherwise. *) +(** Return [true] if all UTF-8 characters in the input string are just plain + ASCII characters. Returns [false] otherwise. *) val is_basic_ascii : string -> bool -(** [ascii_of_ident s] maps UTF-8 string to a string composed solely from ASCII characters. - Those UTF-8 characters which do not have their ASCII counterparts are - translated to ["__Uxxxx_"] where {i xxxx} are four hexadecimal digits. - @raise Unsupported if the input string contains unsupported UTF-8 characters. *) +(** [ascii_of_ident s] maps UTF-8 string to a string composed solely from ASCII + characters. The non-ASCII characters are translated to ["_UUxxxx_"] where + {i xxxx} is the Unicode index of the character in hexadecimal (from four + to six hex digits). To avoid potential name clashes, any preexisting + substring ["_UU"] is turned into ["_UUU"]. *) 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 0f79c10df1..009dfbe1c1 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -132,9 +132,24 @@ 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 -let map_union f g = function - | Inl a -> Inl (f a) - | Inr b -> Inr (g b) +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 = Union.map type iexn = Exninfo.iexn diff --git a/lib/util.mli b/lib/util.mli index 559874bb83..6bed7e3552 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -114,7 +114,15 @@ 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. *) diff --git a/lib/xml_lexer.mli b/lib/xml_lexer.mli deleted file mode 100644 index e61cb055f7..0000000000 --- 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 290f2c89ab..0000000000 --- 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 8db3f9e8ba..0000000000 --- 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 ac2eab352f..0000000000 --- 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 e7e4d0cebc..0000000000 --- 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 f24f51fff5..0000000000 --- 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 |