diff options
Diffstat (limited to 'lib')
45 files changed, 1047 insertions, 813 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml index f7bd81f85d..d06d4b3768 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -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/cList.ml b/lib/cList.ml index 0ac372d8d8..ba592d13f3 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -48,6 +48,8 @@ sig val filteri : (int -> 'a -> bool) -> 'a list -> 'a list val smartfilter : ('a -> bool) -> 'a list -> 'a list + val extend : bool list -> 'a -> 'a list -> 'a list + val count : ('a -> bool) -> 'a list -> int val index : 'a eq -> 'a -> 'a list -> int val index0 : 'a eq -> 'a -> 'a list -> int val iteri : (int -> 'a -> unit) -> 'a list -> unit @@ -375,6 +377,18 @@ let rec smartfilter f l = match l with else h :: tl' else tl' +let rec extend l a l' = match l,l' with + | true::l, b::l' -> b :: extend l a l' + | false::l, l' -> a :: extend l a l' + | [], [] -> [] + | _ -> invalid_arg "extend" + +let count f l = + let rec aux acc = function + | [] -> acc + | h :: t -> if f h then aux (acc + 1) t else aux acc t in + aux 0 l + let rec index_f f x l n = match l with | [] -> raise Not_found | y :: l -> if f x y then n else index_f f x l (succ n) @@ -638,12 +652,13 @@ let rec split3 = function let (rx, ry, rz) = split3 l in (x::rx, y::ry, z::rz) let firstn n l = - let rec aux acc = function - | (0, l) -> List.rev acc - | (n, (h::t)) -> aux (h::acc) (pred n, t) + let rec aux acc n l = + match n, l with + | 0, _ -> List.rev acc + | n, h::t -> aux (h::acc) (pred n) t | _ -> failwith "firstn" in - aux [] (n,l) + aux [] n l let rec last = function | [] -> failwith "List.last" diff --git a/lib/cList.mli b/lib/cList.mli index 19eeb2509a..9c7b815c15 100644 --- a/lib/cList.mli +++ b/lib/cList.mli @@ -94,6 +94,11 @@ sig (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i [f ai = true], then [smartfilter f l == l] *) + val extend : bool list -> 'a -> 'a list -> 'a list +(** [extend l a [a1..an]] assumes that the number of [true] in [l] is [n]; + it extends [a1..an] by inserting [a] at the position of [false] in [l] *) + val count : ('a -> bool) -> 'a list -> int + val index : 'a eq -> 'a -> 'a list -> int (** [index] returns the 1st index of an element in a list (counting from 1). *) diff --git a/lib/cMap.ml b/lib/cMap.ml index 665e1a2163..4b058380c6 100644 --- a/lib/cMap.ml +++ b/lib/cMap.ml @@ -12,12 +12,20 @@ sig val compare : t -> t -> int end +module type MonadS = +sig + type +'a t + val return : 'a -> 'a t + val (>>=) : 'a t -> ('a -> 'b t) -> 'b t +end + module type S = Map.S module type ExtS = sig include CSig.MapS module Set : CSig.SetS with type elt = key + val get : key -> 'a t -> 'a val update : key -> 'a -> 'a t -> 'a t val modify : key -> (key -> 'a -> 'a) -> 'a t -> 'a t val domain : 'a t -> Set.t @@ -30,6 +38,12 @@ sig sig val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t end + module Monad(M : MonadS) : + sig + val fold : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t + val fold_left : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t + val fold_right : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t + end end module MapExt (M : Map.OrderedType) : @@ -47,6 +61,12 @@ sig sig val map : (M.t -> 'a -> M.t * 'b) -> 'a map -> 'b map end + module Monad(MS : MonadS) : + sig + val fold : (M.t -> 'a -> 'b -> 'b MS.t) -> 'a map -> 'b -> 'b MS.t + val fold_left : (M.t -> 'a -> 'b -> 'b MS.t) -> 'a map -> 'b -> 'b MS.t + val fold_right : (M.t -> 'a -> 'b -> 'b MS.t) -> 'a map -> 'b -> 'b MS.t + end end = struct (** This unsafe module is a way to access to the actual implementations of @@ -159,10 +179,34 @@ struct end + module Monad(M : MonadS) = + struct + + open M + + let rec fold_left f s accu = match map_prj s with + | MEmpty -> return accu + | MNode (l, k, v, r, h) -> + fold_left f l accu >>= fun accu -> + f k v accu >>= fun accu -> + fold_left f r accu + + let rec fold_right f s accu = match map_prj s with + | MEmpty -> return accu + | MNode (l, k, v, r, h) -> + fold_right f r accu >>= fun accu -> + f k v accu >>= fun accu -> + fold_right f l accu + + let fold = fold_left + + end + end module Make(M : Map.OrderedType) = struct include Map.Make(M) include MapExt(M) + let get k m = try find k m with Not_found -> assert false end diff --git a/lib/cMap.mli b/lib/cMap.mli index 2f243da83c..3ef7fa2c8a 100644 --- a/lib/cMap.mli +++ b/lib/cMap.mli @@ -14,6 +14,13 @@ sig val compare : t -> t -> int end +module type MonadS = +sig + type +'a t + val return : 'a -> 'a t + val (>>=) : 'a t -> ('a -> 'b t) -> 'b t +end + module type S = Map.S module type ExtS = @@ -24,6 +31,9 @@ sig module Set : CSig.SetS with type elt = key (** Sets used by the domain function *) + val get : key -> 'a t -> 'a + (** Same as {!find} but fails an assertion instead of raising [Not_found] *) + val update : key -> 'a -> 'a t -> 'a t (** Same as [add], but expects the key to be present, and thus faster. @raise Not_found when the key is unbound in the map. *) @@ -59,6 +69,14 @@ sig i.e.: for all (k : key) (x : 'a), compare (fst (f k x)) k = 0. *) end + module Monad(M : MonadS) : + sig + val fold : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t + val fold_left : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t + val fold_right : (key -> 'a -> 'b -> 'b M.t) -> 'a t -> 'b -> 'b M.t + end + (** Fold operators parameterized by any monad. *) + end module Make(M : Map.OrderedType) : ExtS with diff --git a/lib/cSig.mli b/lib/cSig.mli index e095c82cb0..151cfbdca5 100644 --- a/lib/cSig.mli +++ b/lib/cSig.mli @@ -14,6 +14,8 @@ type ('a, 'b) union = Inl of 'a | Inr of 'b type 'a until = Stop of 'a | Cont of 'a (** Used for browsable-until structures. *) +type (_, _) eq = Refl : ('a, 'a) eq + module type SetS = sig type elt @@ -46,6 +48,8 @@ end (** Redeclaration of OCaml set signature, to preserve compatibility. See OCaml documentation for more information. *) +module type EmptyS = sig end + module type MapS = sig type key diff --git a/lib/clib.mllib b/lib/clib.mllib index 9c9607abdb..c3ec4a696e 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -8,6 +8,7 @@ Hashcons CSet CMap Int +Dyn HMap Option Store @@ -27,13 +28,14 @@ CArray CStack Util Stateid -Feedback Pp Ppstyle +Xml_datatype +Richpp +Feedback Xml_lexer Xml_parser Xml_printer -Richpp CUnix Envars Aux_file diff --git a/lib/dyn.ml b/lib/dyn.ml index 04b32870ac..65d1442ac6 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -6,12 +6,68 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors -open Pp +module type TParam = +sig + type 'a t +end +module type PreS = +sig +type 'a tag +type t = Dyn : 'a tag * 'a -> t + +val create : string -> 'a tag +val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option +val repr : 'a tag -> string + +type any = Any : 'a tag -> any + +val name : string -> any option + +module Map(M : TParam) : +sig + type t + val empty : t + val add : 'a tag -> 'a M.t -> t -> t + val remove : 'a tag -> t -> t + val find : 'a tag -> t -> 'a M.t + val mem : 'a tag -> t -> bool + + type any = Any : 'a tag * 'a M.t -> any + + type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t } + val map : map -> t -> t + + val iter : (any -> unit) -> t -> unit + val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r + +end + +val dump : unit -> (int * string) list + +end + +module type S = +sig + include PreS + + module Easy : sig + val make_dyn : string -> ('a -> t) * (t -> 'a) + val inj : 'a -> 'a tag -> t + val prj : t -> 'a tag -> 'a option + end + +end + +module Make(M : CSig.EmptyS) = struct +module Self : PreS = struct (* Dynamics, programmed with DANGER !!! *) -type t = int * Obj.t +type 'a tag = int + +type t = Dyn : 'a tag * 'a -> t + +type any = Any : 'a tag -> any let dyntab = ref (Int.Map.empty : string Int.Map.t) (** Instead of working with tags as strings, which are costly, we use their @@ -24,27 +80,69 @@ let create (s : string) = let () = if Int.Map.mem hash !dyntab then let old = Int.Map.find hash !dyntab in - let msg = str "Dynamic tag collision: " ++ str s ++ str " vs. " ++ str old in - anomaly ~label:"Dyn.create" msg + let () = Printf.eprintf "Dynamic tag collision: %s vs. %s\n%!" s old in + assert false in let () = dyntab := Int.Map.add hash s !dyntab in - let infun v = (hash, Obj.repr v) in - let outfun (nh, rv) = - if Int.equal hash nh then Obj.magic rv - else - anomaly (str "dyn_out: expected " ++ str s) - in - (infun, outfun) + hash -let has_tag (s, _) tag = - let hash = Hashtbl.hash (tag : string) in - Int.equal s hash +let eq : 'a 'b. 'a tag -> 'b tag -> ('a, 'b) CSig.eq option = + fun h1 h2 -> if Int.equal h1 h2 then Some (Obj.magic CSig.Refl) else None -let tag (s,_) = +let repr s = try Int.Map.find s !dyntab with Not_found -> - anomaly (str "Unknown dynamic tag " ++ int s) + let () = Printf.eprintf "Unknown dynamic tag %i\n%!" s in + assert false -let pointer_equal (t1,o1) (t2,o2) = t1 = t2 && o1 == o2 +let name s = + let hash = Hashtbl.hash s in + if Int.Map.mem hash !dyntab then Some (Any hash) else None let dump () = Int.Map.bindings !dyntab + +module Map(M : TParam) = +struct +type t = Obj.t M.t Int.Map.t +let cast : 'a M.t -> 'b M.t = Obj.magic +let empty = Int.Map.empty +let add tag v m = Int.Map.add tag (cast v) m +let remove tag m = Int.Map.remove tag m +let find tag m = cast (Int.Map.find tag m) +let mem = Int.Map.mem + +type any = Any : 'a tag * 'a M.t -> any + +type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t } +let map f m = Int.Map.mapi f.map m + +let iter f m = Int.Map.iter (fun k v -> f (Any (k, v))) m +let fold f m accu = Int.Map.fold (fun k v accu -> f (Any (k, v)) accu) m accu +end + +end +include Self + +module Easy = struct +(* now tags are opaque, we can do the trick *) +let make_dyn (s : string) = + (fun (type a) (tag : a tag) -> + let infun : (a -> t) = fun x -> Dyn (tag, x) in + let outfun : (t -> a) = fun (Dyn (t, x)) -> + match eq tag t with + | None -> assert false + | Some CSig.Refl -> x + in + (infun, outfun)) + (create s) + +let inj x tag = Dyn(tag,x) +let prj : type a. t -> a tag -> a option = + fun (Dyn(tag',x)) tag -> + match eq tag tag' with + | None -> None + | Some CSig.Refl -> Some x +end + +end + diff --git a/lib/dyn.mli b/lib/dyn.mli index c040d8b0b8..448b11a18f 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -6,12 +6,58 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Dynamics. Use with extreme care. Not for kids. *) +(** Dynamically typed values *) -type t +module type TParam = +sig + type 'a t +end + +module type S = +sig +type 'a tag +type t = Dyn : 'a tag * 'a -> t + +val create : string -> 'a tag +val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option +val repr : 'a tag -> string + +type any = Any : 'a tag -> any + +val name : string -> any option + +module Map(M : TParam) : +sig + type t + val empty : t + val add : 'a tag -> 'a M.t -> t -> t + val remove : 'a tag -> t -> t + val find : 'a tag -> t -> 'a M.t + val mem : 'a tag -> t -> bool + + type any = Any : 'a tag * 'a M.t -> any + + type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t } + val map : map -> t -> t + + val iter : (any -> unit) -> t -> unit + val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r + +end -val create : string -> ('a -> t) * (t -> 'a) -val tag : t -> string -val has_tag : t -> string -> bool -val pointer_equal : t -> t -> bool val dump : unit -> (int * string) list + +module Easy : sig + + (* To create a dynamic type on the fly *) + val make_dyn : string -> ('a -> t) * (t -> 'a) + + (* For types declared with the [create] function above *) + val inj : 'a -> 'a tag -> t + val prj : t -> 'a tag -> 'a option +end + +end + +(** FIXME: use OCaml 4.02 generative functors when available *) +module Make(M : CSig.EmptyS) : S diff --git a/lib/envars.ml b/lib/envars.ml index 679e3fdfef..89ce528318 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -146,23 +146,12 @@ let coqpath = let exe s = s ^ Coq_config.exec_extension -let guess_camlbin () = which (user_path ()) (exe "ocamlc") +let guess_ocamlfind () = which (user_path ()) (exe "ocamlfind") -let camlbin () = - if !Flags.camlbin_spec then !Flags.camlbin else - if !Flags.boot then Coq_config.camlbin else - try guess_camlbin () with Not_found -> Coq_config.camlbin - -let ocamlc () = camlbin () / Coq_config.ocamlc - -let ocamlopt () = camlbin () / Coq_config.ocamlopt - -let camllib () = - if !Flags.boot then - Coq_config.camllib - else - let _, res = CUnix.run_command (ocamlc () ^ " -where") in - String.strip res +let ocamlfind () = + if !Flags.ocamlfind_spec then !Flags.ocamlfind else + if !Flags.boot then Coq_config.ocamlfind else + try guess_ocamlfind () / "ocamlfind" with Not_found -> Coq_config.ocamlfind (** {2 Camlp4 paths} *) @@ -173,9 +162,7 @@ let camlp4bin () = if !Flags.boot then Coq_config.camlp4bin else try guess_camlp4bin () with Not_found -> - let cb = camlbin () in - if Sys.file_exists (cb / exe Coq_config.camlp4) then cb - else Coq_config.camlp4bin + Coq_config.camlp4bin let camlp4 () = camlp4bin () / exe Coq_config.camlp4 @@ -183,7 +170,7 @@ let camlp4lib () = if !Flags.boot then Coq_config.camlp4lib else - let ex, res = CUnix.run_command (camlp4 () ^ " -where") in + let ex, res = CUnix.run_command (ocamlfind () ^ " query " ^ Coq_config.camlp4) in match ex with | Unix.WEXITED 0 -> String.strip res | _ -> "/dev/null" diff --git a/lib/envars.mli b/lib/envars.mli index d95b6f0995..90a42859b9 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -47,17 +47,8 @@ val coqroot : string the order it gets added to the search path. *) val coqpath : string list -(** [camlbin ()] is the path to the ocaml binaries. *) -val camlbin : unit -> string - -(** [camllib ()] is the path to the ocaml standard library. *) -val camllib : unit -> string - -(** [ocamlc ()] is the ocaml bytecode compiler that compiled this Coq. *) -val ocamlc : unit -> string - -(** [ocamlc ()] is the ocaml native compiler that compiled this Coq. *) -val ocamlopt : unit -> string +(** [camlbin ()] is the path to the ocamlfind binary. *) +val ocamlfind : unit -> string (** [camlp4bin ()] is the path to the camlp4 binary. *) val camlp4bin : unit -> string diff --git a/lib/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 cce0c6bc69..dce4372ec0 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -9,7 +9,7 @@ open Xml_datatype open Serialize -type message_level = +type level = | Debug of string | Info | Notice @@ -17,8 +17,8 @@ type message_level = | Error type message = { - message_level : message_level; - message_content : string; + message_level : level; + message_content : xml; } let of_message_level = function @@ -39,12 +39,12 @@ let to_message_level = let of_message msg = let lvl = of_message_level msg.message_level in - let content = Serialize.of_string msg.message_content 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_string content } + message_content = Serialize.to_xml content } | _ -> raise Serialize.Marshal_error let is_message = function @@ -169,3 +169,129 @@ let is_feedback = function | _ -> 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 { + message_level = lvl; + message_content = Richpp.of_richpp (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 162867626c..1e96f9a497 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -9,7 +9,7 @@ open Xml_datatype (* Old plain messages (used to be in Pp) *) -type message_level = +type level = | Debug of string | Info | Notice @@ -17,8 +17,8 @@ type message_level = | Error type message = { - message_level : message_level; - message_content : string; + message_level : level; + message_content : xml; } val of_message : message -> xml @@ -66,3 +66,80 @@ 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 2c23ec9849..c1ec9738ca 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -103,18 +103,20 @@ let we_are_parsing = ref false (* Current means no particular compatibility consideration. For correct comparisons, this constructor should remain the last one. *) -type compat_version = V8_2 | V8_3 | V8_4 | Current +type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current let compat_version = ref Current let version_strictly_greater v = match !compat_version, v with -| V8_2, (V8_2 | V8_3 | V8_4 | Current) -> false -| V8_3, (V8_3 | V8_4 | Current) -> false -| V8_4, (V8_4 | Current) -> false +| V8_2, (V8_2 | V8_3 | V8_4 | V8_5 | Current) -> false +| V8_3, (V8_3 | V8_4 | V8_5 | Current) -> false +| V8_4, (V8_4 | V8_5 | Current) -> false +| V8_5, (V8_5 | Current) -> false | Current, Current -> false | V8_3, V8_2 -> true | V8_4, (V8_2 | V8_3) -> true -| Current, (V8_2 | V8_3 | V8_4) -> true +| V8_5, (V8_2 | V8_3 | V8_4) -> true +| Current, (V8_2 | V8_3 | V8_4 | V8_5) -> true let version_less_or_equal v = not (version_strictly_greater v) @@ -122,6 +124,7 @@ let pr_version = function | V8_2 -> "8.2" | V8_3 -> "8.3" | V8_4 -> "8.4" + | V8_5 -> "8.5" | Current -> "current" (* Translate *) @@ -195,9 +198,9 @@ let is_standard_doc_url url = let coqlib_spec = ref false let coqlib = ref "(not initialized yet)" -(* Options for changing camlbin (used by coqmktop) *) -let camlbin_spec = ref false -let camlbin = ref Coq_config.camlbin +(* Options for changing ocamlfind (used by coqmktop) *) +let ocamlfind_spec = ref false +let ocamlfind = ref Coq_config.camlbin (* Options for changing camlp4bin (used by coqmktop) *) let camlp4bin_spec = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 69caad5b62..24780f0dcc 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -57,7 +57,7 @@ val raw_print : bool ref val record_print : bool ref val univ_print : bool ref -type compat_version = V8_2 | V8_3 | V8_4 | Current +type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current val compat_version : compat_version ref val version_strictly_greater : compat_version -> bool val version_less_or_equal : compat_version -> bool @@ -123,8 +123,8 @@ val coqlib_spec : bool ref val coqlib : string ref (** Options for specifying where OCaml binaries reside *) -val camlbin_spec : bool ref -val camlbin : string ref +val ocamlfind_spec : bool ref +val ocamlfind : string ref val camlp4bin_spec : bool ref val camlp4bin : string ref diff --git a/lib/future.ml b/lib/future.ml index e8f33db5e1..9cdc1c20e3 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -7,8 +7,9 @@ (************************************************************************) (* To deal with side effects we have to save/restore the system state *) -let freeze = ref (fun () -> assert false : unit -> Dyn.t) -let unfreeze = ref (fun _ -> () : Dyn.t -> unit) +type freeze +let freeze = ref (fun () -> assert false : unit -> freeze) +let unfreeze = ref (fun _ -> () : freeze -> unit) let set_freeze f g = freeze := f; unfreeze := g let not_ready_msg = ref (fun name -> @@ -58,7 +59,7 @@ type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computat and 'a comp = | Delegated of (unit -> unit) | Closure of (unit -> 'a) - | Val of 'a * Dyn.t option + | Val of 'a * freeze option | Exn of Exninfo.iexn (* Invariant: this exception is always "fixed" as in fix_exn *) and 'a comput = diff --git a/lib/future.mli b/lib/future.mli index 58f0a71ad8..114c591765 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -157,10 +157,11 @@ val transactify : ('a -> 'b) -> 'a -> 'b (** Debug: print a computation given an inner printing function. *) val print : ('a -> Pp.std_ppcmds) -> 'a computation -> Pp.std_ppcmds +type freeze (* These functions are needed to get rid of side effects. Thy are set for the outermos layer of the system, since they have to deal with the whole system state. *) -val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit +val set_freeze : (unit -> freeze) -> (freeze -> unit) -> unit val customize_not_ready_msg : (string -> Pp.std_ppcmds) -> unit val customize_not_here_msg : (string -> Pp.std_ppcmds) -> unit diff --git a/lib/genarg.ml b/lib/genarg.ml index cba54c1141..69408fb1a5 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -9,168 +9,160 @@ open Pp open Util -type argument_type = - (* Basic types *) - | IntOrVarArgType - | IdentArgType - | VarArgType - (* Specific types *) - | GenArgType - | ConstrArgType - | ConstrMayEvalArgType - | QuantHypArgType - | OpenConstrArgType - | ConstrWithBindingsArgType - | BindingsArgType - | RedExprArgType - | ListArgType of argument_type - | OptArgType of argument_type - | PairArgType of argument_type * argument_type - | ExtraArgType of string - -let rec argument_type_eq arg1 arg2 = match arg1, arg2 with -| IntOrVarArgType, IntOrVarArgType -> true -| IdentArgType, IdentArgType -> true -| VarArgType, VarArgType -> true -| GenArgType, GenArgType -> true -| ConstrArgType, ConstrArgType -> true -| ConstrMayEvalArgType, ConstrMayEvalArgType -> true -| QuantHypArgType, QuantHypArgType -> true -| OpenConstrArgType, OpenConstrArgType -> true -| ConstrWithBindingsArgType, ConstrWithBindingsArgType -> true -| BindingsArgType, BindingsArgType -> true -| RedExprArgType, RedExprArgType -> true -| ListArgType arg1, ListArgType arg2 -> argument_type_eq arg1 arg2 -| OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2 -| PairArgType (arg1l, arg1r), PairArgType (arg2l, arg2r) -> - argument_type_eq arg1l arg2l && argument_type_eq arg1r arg2r -| ExtraArgType s1, ExtraArgType s2 -> CString.equal s1 s2 -| _ -> false - -let rec pr_argument_type = function -| IntOrVarArgType -> str "int_or_var" -| IdentArgType -> str "ident" -| VarArgType -> str "var" -| GenArgType -> str "genarg" -| ConstrArgType -> str "constr" -| ConstrMayEvalArgType -> str "constr_may_eval" -| QuantHypArgType -> str "qhyp" -| OpenConstrArgType -> str "open_constr" -| ConstrWithBindingsArgType -> str "constr_with_bindings" -| BindingsArgType -> str "bindings" -| RedExprArgType -> str "redexp" -| ListArgType t -> pr_argument_type t ++ spc () ++ str "list" -| OptArgType t -> pr_argument_type t ++ spc () ++ str "opt" -| PairArgType (t1, t2) -> - str "("++ pr_argument_type t1 ++ spc () ++ - str "*" ++ spc () ++ pr_argument_type t2 ++ str ")" -| ExtraArgType s -> str s - -type ('raw, 'glob, 'top) genarg_type = argument_type +module ArgT = +struct + module DYN = Dyn.Make(struct end) + module Map = DYN.Map + type ('a, 'b, 'c) tag = ('a * 'b * 'c) DYN.tag + type any = Any : ('a, 'b, 'c) tag -> any + let eq = DYN.eq + let repr = DYN.repr + let create = DYN.create + let name s = match DYN.name s with + | None -> None + | Some (DYN.Any t) -> + Some (Any (Obj.magic t)) (** All created tags are made of triples *) +end + +type (_, _, _) genarg_type = +| ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type +| ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type +| OptArg : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type +| PairArg : ('a1, 'b1, 'c1) genarg_type * ('a2, 'b2, 'c2) genarg_type -> + ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type + +type argument_type = ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type + +let rec genarg_type_eq : type a1 a2 b1 b2 c1 c2. + (a1, b1, c1) genarg_type -> (a2, b2, c2) genarg_type -> + (a1 * b1 * c1, a2 * b2 * c2) CSig.eq option = +fun t1 t2 -> match t1, t2 with +| ExtraArg t1, ExtraArg t2 -> ArgT.eq t1 t2 +| ListArg t1, ListArg t2 -> + begin match genarg_type_eq t1 t2 with + | None -> None + | Some Refl -> Some Refl + end +| OptArg t1, OptArg t2 -> + begin match genarg_type_eq t1 t2 with + | None -> None + | Some Refl -> Some Refl + end +| PairArg (t1, u1), PairArg (t2, u2) -> + begin match genarg_type_eq t1 t2 with + | None -> None + | Some Refl -> + match genarg_type_eq u1 u2 with + | None -> None + | Some Refl -> Some Refl + end +| _ -> None + +let rec pr_genarg_type : type a b c. (a, b, c) genarg_type -> std_ppcmds = function +| ListArg t -> pr_genarg_type t ++ spc () ++ str "list" +| OptArg t -> pr_genarg_type t ++ spc () ++ str "opt" +| PairArg (t1, t2) -> + str "("++ pr_genarg_type t1 ++ spc () ++ + str "*" ++ spc () ++ pr_genarg_type t2 ++ str ")" +| ExtraArg s -> str (ArgT.repr s) + +let argument_type_eq arg1 arg2 = match arg1, arg2 with +| ArgumentType t1, ArgumentType t2 -> + match genarg_type_eq t1 t2 with + | None -> false + | Some Refl -> true + +let pr_argument_type (ArgumentType t) = pr_genarg_type t type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type (** Alias for concision *) (* Dynamics but tagged by a type expression *) -type rlevel -type glevel -type tlevel +type rlevel = [ `rlevel ] +type glevel = [ `glevel ] +type tlevel = [ `tlevel ] + +type (_, _) abstract_argument_type = +| Rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type +| Glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type +| Topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type + +type 'l generic_argument = GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument -type 'a generic_argument = argument_type * Obj.t type raw_generic_argument = rlevel generic_argument type glob_generic_argument = glevel generic_argument type typed_generic_argument = tlevel generic_argument -let rawwit t = t -let glbwit t = t -let topwit t = t - -let wit_list t = ListArgType t +let rawwit t = Rawwit t +let glbwit t = Glbwit t +let topwit t = Topwit t + +let wit_list t = ListArg t + +let wit_opt t = OptArg t + +let wit_pair t1 t2 = PairArg (t1, t2) + +let in_gen t o = GenArg (t, o) + +let abstract_argument_type_eq : + type a b l. (a, l) abstract_argument_type -> (b, l) abstract_argument_type -> (a, b) CSig.eq option = + fun t1 t2 -> match t1, t2 with + | Rawwit t1, Rawwit t2 -> + begin match genarg_type_eq t1 t2 with + | None -> None + | Some Refl -> Some Refl + end + | Glbwit t1, Glbwit t2 -> + begin match genarg_type_eq t1 t2 with + | None -> None + | Some Refl -> Some Refl + end + | Topwit t1, Topwit t2 -> + begin match genarg_type_eq t1 t2 with + | None -> None + | Some Refl -> Some Refl + end + +let out_gen (type a) (type l) (t : (a, l) abstract_argument_type) (o : l generic_argument) : a = + let GenArg (t', v) = o in + match abstract_argument_type_eq t t' with + | None -> failwith "out_gen" + | Some Refl -> v + +let has_type (GenArg (t, v)) u = match abstract_argument_type_eq t u with +| None -> false +| Some _ -> true + +let unquote : type l. (_, l) abstract_argument_type -> _ = function +| Rawwit t -> ArgumentType t +| Glbwit t -> ArgumentType t +| Topwit t -> ArgumentType t + +let genarg_tag (GenArg (t, _)) = unquote t -let wit_opt t = OptArgType t - -let wit_pair t1 t2 = PairArgType (t1,t2) - -let in_gen t o = (t,Obj.repr o) -let out_gen t (t',o) = if argument_type_eq t t' then Obj.magic o else failwith "out_gen" -let genarg_tag (s,_) = s - -let has_type (t, v) u = argument_type_eq t u - -let unquote x = x - -type ('a,'b) abstract_argument_type = argument_type type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type -type ('a, 'b, 'c, 'l) cast = Obj.t - -let raw = Obj.obj -let glb = Obj.obj -let top = Obj.obj - -type ('r, 'l) unpacker = - { unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c, 'l) cast -> 'r } - -let unpack pack (t, obj) = pack.unpacker t (Obj.obj obj) - -(** Type transformers *) - -type ('r, 'l) list_unpacker = - { list_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> - ('a list, 'b list, 'c list, 'l) cast -> 'r } - -let list_unpack pack (t, obj) = match t with -| ListArgType t -> pack.list_unpacker t (Obj.obj obj) -| _ -> failwith "out_gen" - -type ('r, 'l) opt_unpacker = - { opt_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> - ('a option, 'b option, 'c option, 'l) cast -> 'r } - -let opt_unpack pack (t, obj) = match t with -| OptArgType t -> pack.opt_unpacker t (Obj.obj obj) -| _ -> failwith "out_gen" - -type ('r, 'l) pair_unpacker = - { pair_unpacker : 'a1 'a2 'b1 'b2 'c1 'c2. - ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type -> - (('a1 * 'a2), ('b1 * 'b2), ('c1 * 'c2), 'l) cast -> 'r } - -let pair_unpack pack (t, obj) = match t with -| PairArgType (t1, t2) -> pack.pair_unpacker t1 t2 (Obj.obj obj) -| _ -> failwith "out_gen" - (** Creating args *) -let (arg0_map : Obj.t option String.Map.t ref) = ref String.Map.empty +module type Param = sig type ('raw, 'glb, 'top) t end +module ArgMap(M : Param) = +struct + type _ pack = Pack : ('raw, 'glb, 'top) M.t -> ('raw * 'glb * 'top) pack + include ArgT.Map(struct type 'a t = 'a pack end) +end -let create_arg opt name = - if String.Map.mem name !arg0_map then +let create_arg name = + match ArgT.name name with + | None -> ExtraArg (ArgT.create name) + | Some _ -> Errors.anomaly (str "generic argument already declared: " ++ str name) - else - let () = arg0_map := String.Map.add name (Obj.magic opt) !arg0_map in - ExtraArgType name let make0 = create_arg -let default_empty_value t = - let rec aux = function - | ListArgType _ -> Some (Obj.repr []) - | OptArgType _ -> Some (Obj.repr None) - | PairArgType(t1, t2) -> - (match aux t1, aux t2 with - | Some v1, Some v2 -> Some (Obj.repr (v1, v2)) - | _ -> None) - | ExtraArgType s -> - String.Map.find s !arg0_map - | _ -> None in - match aux t with - | Some v -> Some (Obj.obj v) - | None -> None - (** Registering genarg-manipulating functions *) module type GenObj = @@ -182,54 +174,31 @@ end module Register (M : GenObj) = struct - let arg0_map = - ref (String.Map.empty : (Obj.t, Obj.t, Obj.t) M.obj String.Map.t) + module GenMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) M.obj end) + let arg0_map = ref GenMap.empty let register0 arg f = match arg with - | ExtraArgType s -> - if String.Map.mem s !arg0_map then - let msg = str M.name ++ str " function already registered: " ++ str s in + | ExtraArg s -> + if GenMap.mem s !arg0_map then + let msg = str M.name ++ str " function already registered: " ++ str (ArgT.repr s) in Errors.anomaly msg else - arg0_map := String.Map.add s (Obj.magic f) !arg0_map + arg0_map := GenMap.add s (GenMap.Pack f) !arg0_map | _ -> assert false let get_obj0 name = - try String.Map.find name !arg0_map + try + let GenMap.Pack obj = GenMap.find name !arg0_map in obj with Not_found -> - match M.default (ExtraArgType name) with + match M.default (ExtraArg name) with | None -> - Errors.anomaly (str M.name ++ str " function not found: " ++ str name) + Errors.anomaly (str M.name ++ str " function not found: " ++ str (ArgT.repr name)) | Some obj -> obj (** For now, the following function is quite dummy and should only be applied to an extra argument type, otherwise, it will badly fail. *) let obj t = match t with - | ExtraArgType s -> Obj.magic (get_obj0 s) + | ExtraArg s -> get_obj0 s | _ -> assert false end - -(** Hackish part *) - -let arg0_names = ref (String.Map.empty : string String.Map.t) -(** We use this table to associate a name to a given witness, to use it with - the extension mechanism. This is REALLY ad-hoc, but I do not know how to - do so nicely either. *) - -let register_name0 t name = match t with -| ExtraArgType s -> - let () = assert (not (String.Map.mem s !arg0_names)) in - arg0_names := String.Map.add s name !arg0_names -| _ -> failwith "register_name0" - -let get_name0 name = - String.Map.find name !arg0_names - -module Unsafe = -struct - -let inj tpe x = (tpe, x) -let prj (_, x) = x - -end diff --git a/lib/genarg.mli b/lib/genarg.mli index 671d96b7bf..b8bb6af04a 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -68,18 +68,32 @@ ExtraArgType of string '_a '_b (** {5 Generic types} *) -type ('raw, 'glob, 'top) genarg_type +module ArgT : +sig + type ('a, 'b, 'c) tag + val eq : ('a1, 'b1, 'c1) tag -> ('a2, 'b2, 'c2) tag -> ('a1 * 'b1 * 'c1, 'a2 * 'b2 * 'c2) CSig.eq option + val repr : ('a, 'b, 'c) tag -> string + type any = Any : ('a, 'b, 'c) tag -> any + val name : string -> any option +end + +type (_, _, _) genarg_type = +| ExtraArg : ('a, 'b, 'c) ArgT.tag -> ('a, 'b, 'c) genarg_type +| ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type +| OptArg : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type +| PairArg : ('a1, 'b1, 'c1) genarg_type * ('a2, 'b2, 'c2) genarg_type -> + ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type (** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized one, and ['top] the internalized one. *) type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type (** Alias for concision when the three types agree. *) -val make0 : 'raw option -> string -> ('raw, 'glob, 'top) genarg_type +val make0 : string -> ('raw, 'glob, 'top) genarg_type (** Create a new generic type of argument: force to associate unique ML types at each of the three levels. *) -val create_arg : 'raw option -> string -> ('raw, 'glob, 'top) genarg_type +val create_arg : string -> ('raw, 'glob, 'top) genarg_type (** Alias for [make0]. *) (** {5 Specialized types} *) @@ -91,11 +105,14 @@ val create_arg : 'raw option -> string -> ('raw, 'glob, 'top) genarg_type out_gen is monomorphic over 'a, hence type-safe *) -type rlevel -type glevel -type tlevel +type rlevel = [ `rlevel ] +type glevel = [ `glevel ] +type tlevel = [ `tlevel ] -type ('a, 'co) abstract_argument_type +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 @@ -120,7 +137,7 @@ val topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type (** {5 Generic arguments} *) -type 'a generic_argument +type 'l generic_argument = GenArg : ('a, 'l) abstract_argument_type * 'a -> 'l generic_argument (** A inhabitant of ['level generic_argument] is a inhabitant of some type at level ['level], together with the representation of this type. *) @@ -141,66 +158,20 @@ val has_type : 'co generic_argument -> ('a, 'co) abstract_argument_type -> bool (** [has_type v t] tells whether [v] has type [t]. If true, it ensures that [out_gen t v] will not raise a dynamic type exception. *) -(** {6 Destructors} *) - -type ('a, 'b, 'c, 'l) cast - -val raw : ('a, 'b, 'c, rlevel) cast -> 'a -val glb : ('a, 'b, 'c, glevel) cast -> 'b -val top : ('a, 'b, 'c, tlevel) cast -> 'c - -type ('r, 'l) unpacker = - { unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c, 'l) cast -> 'r } - -val unpack : ('r, 'l) unpacker -> 'l generic_argument -> 'r -(** Existential-type destructors. *) - -(** {6 Manipulation of generic arguments} - -Those functions fail if they are applied to an argument which has not the right -dynamic type. *) - -type ('r, 'l) list_unpacker = - { list_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> - ('a list, 'b list, 'c list, 'l) cast -> 'r } - -val list_unpack : ('r, 'l) list_unpacker -> 'l generic_argument -> 'r - -type ('r, 'l) opt_unpacker = - { opt_unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> - ('a option, 'b option, 'c option, 'l) cast -> 'r } - -val opt_unpack : ('r, 'l) opt_unpacker -> 'l generic_argument -> 'r - -type ('r, 'l) pair_unpacker = - { pair_unpacker : 'a1 'a2 'b1 'b2 'c1 'c2. - ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type -> - (('a1 * 'a2), ('b1 * 'b2), ('c1 * 'c2), 'l) cast -> 'r } - -val pair_unpack : ('r, 'l) pair_unpacker -> 'l generic_argument -> 'r - (** {6 Type reification} *) -type argument_type = - (** Basic types *) - | IntOrVarArgType - | IdentArgType - | VarArgType - (** Specific types *) - | GenArgType - | ConstrArgType - | ConstrMayEvalArgType - | QuantHypArgType - | OpenConstrArgType - | ConstrWithBindingsArgType - | BindingsArgType - | RedExprArgType - | ListArgType of argument_type - | OptArgType of argument_type - | PairArgType of argument_type * argument_type - | ExtraArgType of string +type argument_type = ArgumentType : ('a, 'b, 'c) genarg_type -> argument_type + +(** {6 Equalities} *) val argument_type_eq : argument_type -> argument_type -> bool +val genarg_type_eq : + ('a1, 'b1, 'c1) genarg_type -> + ('a2, 'b2, 'c2) genarg_type -> + ('a1 * 'b1 * 'c1, 'a2 * 'b2 * 'c2) CSig.eq option +val abstract_argument_type_eq : + ('a, 'l) abstract_argument_type -> ('b, 'l) abstract_argument_type -> + ('a, 'b) CSig.eq option val pr_argument_type : argument_type -> Pp.std_ppcmds (** Print a human-readable representation for a given type. *) @@ -244,35 +215,3 @@ val wit_list : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_ty val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type -> ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type - -(** {5 Magic used by the parser} *) - -val default_empty_value : ('raw, 'glb, 'top) genarg_type -> 'raw option - -val register_name0 : ('a, 'b, 'c) genarg_type -> string -> unit -(** Used by the extension to give a name to types. The string should be the - absolute path of the argument witness, e.g. - [register_name0 wit_toto "MyArg.wit_toto"]. *) - -val get_name0 : string -> string -(** Return the absolute path of a given witness. *) - -(** {5 Unsafe loophole} *) - -module Unsafe : -sig - -(** Unsafe magic functions. Not for kids. This is provided here as a loophole to - escape this module. Do NOT use outside of the dedicated areas. NOT. EVER. *) - -val inj : argument_type -> Obj.t -> 'lev generic_argument -(** Injects an object as generic argument. !!!BEWARE!!! only do this as - [inj tpe x] where: - - 1. [tpe] is the reification of a [('a, 'b, 'c) genarg_type]; - 2. [x] has type ['a], ['b] or ['c] according to the return level ['lev]. *) - -val prj : 'lev generic_argument -> Obj.t -(** Recover the contents of a generic argument. *) - -end diff --git a/lib/hMap.ml b/lib/hMap.ml index ba6aad913f..778c366fd5 100644 --- a/lib/hMap.ml +++ b/lib/hMap.ml @@ -286,6 +286,8 @@ struct let m = Int.Map.find h s in Map.find k m + let get k s = try find k s with Not_found -> assert false + let split k s = assert false (** Cannot be implemented efficiently *) let map f s = @@ -329,4 +331,17 @@ struct Int.Map.map fs s end + module Monad(M : CMap.MonadS) = + struct + module IntM = Int.Map.Monad(M) + module ExtM = Map.Monad(M) + + let fold f s accu = + let ff _ m accu = ExtM.fold f m accu in + IntM.fold ff s accu + + let fold_left _ _ _ = assert false + let fold_right _ _ _ = assert false + end + end diff --git a/lib/hashcons.ml b/lib/hashcons.ml index 4a72b015c5..4eaacf9145 100644 --- a/lib/hashcons.ml +++ b/lib/hashcons.ml @@ -72,7 +72,7 @@ module Make (X : HashconsedType) : (S with type t = X.t and type u = X.u) = end -(* A few usefull wrappers: +(* A few useful wrappers: * takes as argument the function [generate] above and build a function of type * u -> t -> t that creates a fresh table each time it is applied to the * sub-hcons functions. *) @@ -96,20 +96,6 @@ let recursive_hcons h f u = let () = loop := hrec in hrec -(* A set of global hashcons functions *) -let hashcons_resets = ref [] -let init() = List.iter (fun f -> f()) !hashcons_resets - -(* [register_hcons h u] registers the hcons function h, result of the above - * wrappers. It returns another hcons function that always uses the same - * table, which can be reinitialized by init() - *) -let register_hcons h u = - let hf = ref (h u) in - let reset() = hf := h u in - hashcons_resets := reset :: !hashcons_resets; - (fun x -> !hf x) - (* Basic hashcons modules for string and obj. Integers do not need be hashconsed. *) @@ -194,18 +180,3 @@ module Hobj = Make( let eq = comp_obj let hash = Hashtbl.hash end) - -(* Hashconsing functions for string and obj. Always use the same - * global tables. The latter can be reinitialized with init() - *) -(* string : string -> string *) -(* obj : Obj.t -> Obj.t *) -let string = register_hcons (simple_hcons Hstring.generate Hstring.hcons) () -let obj = register_hcons (recursive_hcons Hobj.generate Hobj.hcons) () - -(* The unsafe polymorphic hashconsing function *) -let magic_hash (c : 'a) = - init(); - let r = obj (Obj.repr c) in - init(); - (Obj.magic r : 'a) diff --git a/lib/hashset.ml b/lib/hashset.ml index 04009fdf3c..af33544dc6 100644 --- a/lib/hashset.ml +++ b/lib/hashset.ml @@ -162,7 +162,7 @@ module Make (E : EqType) = t.hashes.(index) <- newhashes; if sz <= t.limit && newsz > t.limit then begin t.oversize <- t.oversize + 1; - for i = 0 to over_limit do test_shrink_bucket t done; + for _i = 0 to over_limit do test_shrink_bucket t done; end; if t.oversize > Array.length t.table / over_limit then resize t end else if Weak.check bucket i then begin diff --git a/lib/heap.ml b/lib/heap.ml index 187189fcaf..97ccadeba8 100644 --- a/lib/heap.ml +++ b/lib/heap.ml @@ -62,8 +62,6 @@ module Functional(X : Ordered) = struct let empty = Leaf - let is_empty t = t = Leaf - let rec add x = function | Leaf -> Node (Leaf, x, Leaf) diff --git a/lib/iStream.ml b/lib/iStream.ml index 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 6805ce4919..a6c09058dd 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -1,9 +1,9 @@ Errors Bigint -Dyn Segmenttree Unicodetable Unicode +Minisys System CThread Spawn 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 diff --git a/lib/option.ml b/lib/option.ml index 4ea613e4fd..fbb883d30a 100644 --- a/lib/option.ml +++ b/lib/option.ml @@ -41,8 +41,8 @@ let hash f = function exception IsNone -(** [get x] returns [y] where [x] is [Some y]. It raises IsNone - if [x] equals [None]. *) +(** [get x] returns [y] where [x] is [Some y]. + @raise [IsNone] if [x] equals [None]. *) let get = function | Some y -> y | _ -> raise IsNone diff --git a/lib/option.mli b/lib/option.mli index 409dff9d3d..5e085620e7 100644 --- a/lib/option.mli +++ b/lib/option.mli @@ -34,8 +34,8 @@ val compare : ('a -> 'a -> int) -> 'a option -> 'a option -> int (** Lift a hash to option types. *) val hash : ('a -> int) -> 'a option -> int -(** [get x] returns [y] where [x] is [Some y]. It raises IsNone - if [x] equals [None]. *) +(** [get x] returns [y] where [x] is [Some y]. + @raise IsNone if [x] equals [None]. *) val get : 'a option -> 'a (** [make x] returns [Some x]. *) @@ -54,7 +54,7 @@ val flatten : 'a option option -> 'a option val append : 'a option -> 'a option -> 'a option -(** {6 "Iterators"} ***) +(** {6 "Iterators"} *) (** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing otherwise. *) @@ -63,8 +63,8 @@ val iter : ('a -> unit) -> 'a option -> unit exception Heterogeneous (** [iter2 f x y] executes [f z w] if [x] equals [Some z] and [y] equals - [Some w]. It does nothing if both [x] and [y] are [None]. And raises - [Heterogeneous] otherwise. *) + [Some w]. It does nothing if both [x] and [y] are [None]. + @raise Heterogeneous otherwise. *) val iter2 : ('a -> 'b -> unit) -> 'a option -> 'b option -> unit (** [map f x] is [None] if [x] is [None] and [Some (f y)] if [x] is [Some y]. *) @@ -78,8 +78,8 @@ val smartmap : ('a -> 'a) -> 'a option -> 'a option val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a option -> 'b (** [fold_left2 f a x y] is [f z w] if [x] is [Some z] and [y] is [Some w]. - It is [a] if both [x] and [y] are [None]. Otherwise it raises - [Heterogeneous]. *) + It is [a] if both [x] and [y] are [None]. + @raise Heterogeneous otherwise. *) val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a (** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *) @@ -91,7 +91,7 @@ val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b option -> 'a * 'c option (** [cata f e x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *) val cata : ('a -> 'b) -> 'b -> 'a option -> 'b -(** {6 More Specific Operations} ***) +(** {6 More Specific Operations} *) (** [default a x] is [y] if [x] is [Some y] and [a] otherwise. *) val default : 'a -> 'a option -> 'a @@ -51,37 +51,19 @@ sig val prj : t -> 'a key -> 'a option end = struct - (** See module {Dyn} for more details. *) - type t = int * Obj.t +module Dyn = Dyn.Make(struct end) - type 'a key = int - - let dyntab = ref (Int.Map.empty : string Int.Map.t) - - let create (s : string) = - let hash = Hashtbl.hash s in - let () = assert (not (Int.Map.mem hash !dyntab)) in - let () = dyntab := Int.Map.add hash s !dyntab in - hash - - let inj x h = (h, Obj.repr x) - - let prj (nh, rv) h = - if Int.equal h nh then Some (Obj.magic rv) - else None +type t = Dyn.t +type 'a key = 'a Dyn.tag +let create = Dyn.create +let inj = Dyn.Easy.inj +let prj = Dyn.Easy.prj end open Pp_control -(* This should not be used outside of this file. Use - Flags.print_emacs instead. This one is updated when reading - command line options. This was the only way to make [Pp] depend on - an option without creating a circularity: [Flags] -> [Util] -> - [Pp] -> [Flags] *) -let print_emacs = ref false - (* The different kinds of blocks are: \begin{description} \item[hbox:] Horizontal block no line breaking; @@ -268,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)) @@ -297,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;*) @@ -350,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 : string; -} - -let of_message = Feedback.of_message -let to_message = Feedback.to_message -let is_message = Feedback.is_message - -type logger = message_level -> std_ppcmds -> unit - -let make_body info s = - emacs_quote (hov 0 (info ++ spc () ++ s)) - -let debugbody strm = emacs_quote_info (hov 0 (str "Debug:" ++ spc () ++ strm)) -let warnbody strm = make_body (str "Warning:") strm -let errorbody strm = make_body (str "Error:") strm -let infobody strm = emacs_quote_info strm - -let std_logger ~id:_ level msg = match level with -| Debug _ -> msgnl (debugbody msg) -| Info -> msgnl (hov 0 msg) -| Notice -> msgnl msg -| Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody msg)) () -| Error -> msgnl_with !err_ft (errorbody msg) - -let emacs_logger ~id:_ level mesg = match level with -| Debug _ -> msgnl (debugbody mesg) -| Info -> msgnl (infobody mesg) -| Notice -> msgnl mesg -| Warning -> Flags.if_warn (fun () -> msgnl_with !err_ft (warnbody mesg)) () -| Error -> msgnl_with !err_ft (errorbody mesg) - -let logger = ref std_logger - -let make_pp_emacs() = print_emacs:=true; logger:=emacs_logger -let make_pp_nonemacs() = print_emacs:=false; logger := std_logger - -let ft_logger old_logger ft ~id level mesg = match level with - | Debug _ -> msgnl_with ft (debugbody mesg) - | Info -> msgnl_with ft (infobody mesg) - | Notice -> msgnl_with ft mesg - | Warning -> old_logger ~id:id level mesg - | Error -> old_logger ~id:id level mesg - -let with_output_to_file fname func input = - let old_logger = !logger in - let channel = open_out (String.concat "." [fname; "out"]) in - logger := ft_logger old_logger (Format.formatter_of_out_channel channel); - try - let output = func input in - logger := old_logger; - close_out channel; - output - with reraise -> - let reraise = Backtrace.add_backtrace reraise in - logger := old_logger; - close_out channel; - Exninfo.iraise reraise - -let feedback_id = ref (Feedback.Edit 0) -let feedback_route = ref Feedback.default_route - (* If mixing some output and a goal display, please use msg_warning, so that interfaces (proofgeneral for example) can easily dispatch them to different windows. *) -let msg_info x = !logger ~id:!feedback_id Info x -let msg_notice x = !logger ~id:!feedback_id Notice x -let msg_warning x = !logger ~id:!feedback_id Warning x -let msg_error x = !logger ~id:!feedback_id Error x -let msg_debug x = !logger ~id:!feedback_id (Debug "_") x - -let set_logger l = logger := (fun ~id:_ lvl msg -> l lvl msg) - -let std_logger lvl msg = std_logger ~id:!feedback_id lvl msg - -(** Feedback *) - -let feeder = ref ignore -let set_id_for_feedback ?(route=Feedback.default_route) i = - feedback_id := i; feedback_route := route -let feedback ?state_id ?edit_id ?route what = - !feeder { - Feedback.contents = what; - Feedback.route = Option.default !feedback_route route; - Feedback.id = - match state_id, edit_id with - | Some id, _ -> Feedback.State id - | None, Some eid -> Feedback.Edit eid - | None, None -> !feedback_id; - } -let set_feeder f = feeder := f -let get_id_for_feedback () = !feedback_id, !feedback_route - -(** Utility *) - +(** Output to a string formatter *) let string_of_ppcmds c = - msg_with Format.str_formatter c; + Format.fprintf Format.str_formatter "@[%a@]" msg_with c; Format.flush_str_formatter () -let log_via_feedback () = logger := (fun ~id lvl msg -> - !feeder { - Feedback.contents = Feedback.Message { - message_level = lvl; - message_content = string_of_ppcmds msg }; - Feedback.route = !feedback_route; - Feedback.id = id }) - (* Copy paste from Util *) let pr_comma () = str "," ++ spc () let pr_semicolon () = str ";" ++ spc () let pr_bar () = str "|" ++ spc () let pr_arg pr x = spc () ++ pr x +let pr_non_empty_arg pr x = let pp = pr x in if ismt pp then mt () else spc () ++ pr x let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x @@ -607,3 +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 98219636bc..ced4b66032 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 : string; -} - -type logger = message_level -> std_ppcmds -> unit - -(** {6 output functions} - -[msg_notice] do not put any decoration on output by default. If -possible don't mix it with goal output (prefer msg_info or -msg_warning) so that interfaces can dispatch outputs easily. Once all -interfaces use the xml-like protocol this constraint can be -relaxed. *) -(* Should we advertise these functions more? Should they be the ONLY - allowed way to output something? *) - -val msg_info : std_ppcmds -> unit -(** Message that displays information, usually in verbose mode, such as [Foobar - is defined] *) - -val msg_notice : std_ppcmds -> unit -(** Message that should be displayed, such as [Print Foo] or [Show Bar]. *) - -val msg_warning : std_ppcmds -> unit -(** Message indicating that something went wrong, but without serious - consequences. *) - -val msg_error : std_ppcmds -> unit -(** Message indicating that something went really wrong, though still - recoverable; otherwise an exception would have been raised. *) - -val msg_debug : std_ppcmds -> unit -(** For debugging purposes *) - -val std_logger : logger -(** Standard logging function *) - -val set_logger : logger -> unit - -val log_via_feedback : unit -> unit - -val of_message : message -> Xml_datatype.xml -val to_message : Xml_datatype.xml -> message -val is_message : Xml_datatype.xml -> bool - - -(** {6 Feedback sent, even asynchronously, to the user interface} *) - -(* This stuff should be available to most of the system, line msg_* above. - * But I'm unsure this is the right place, especially for the global edit_id. - * - * Morally the parser gets a string and an edit_id, and gives back an AST. - * Feedbacks during the parsing phase are attached to this edit_id. - * The interpreter assigns an exec_id to the ast, and feedbacks happening - * during interpretation are attached to the exec_id. - * Only one among state_id and edit_id can be provided. *) - -val feedback : - ?state_id:Feedback.state_id -> ?edit_id:Feedback.edit_id -> - ?route:Feedback.route_id -> Feedback.feedback_content -> unit - -val set_id_for_feedback : - ?route:Feedback.route_id -> Feedback.edit_or_state_id -> unit -val set_feeder : (Feedback.feedback -> unit) -> unit -val get_id_for_feedback : unit -> Feedback.edit_or_state_id * Feedback.route_id - (** {6 Utilities} *) val string_of_ppcmds : std_ppcmds -> string @@ -199,6 +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,9 @@ 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{% }%}. } *) +(** {6 Low-level pretty-printing functions with and 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. *) - -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. *) - -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 *) +(** 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 +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 453df43def..fe3edd99ca 100644 --- a/lib/richpp.ml +++ b/lib/richpp.ml @@ -163,4 +163,38 @@ let xml_of_rich_pp tag_of_annotation attributes_of_annotation xml = in node xml +type richpp = xml +let repr xml = xml +let richpp_of_xml xml = xml +let richpp_of_string s = PCData s + +let richpp_of_pp pp = + let annotate t = match Pp.Tag.prj t Ppstyle.tag with + | None -> None + | Some key -> Some (Ppstyle.repr key) + in + let rec drop = function + | PCData s -> [PCData s] + | Element (_, annotation, cs) -> + let cs = List.concat (List.map drop cs) in + match annotation.annotation with + | None -> cs + | Some s -> [Element (String.concat "." s, [], cs)] + in + let xml = rich_pp annotate pp in + Element ("_", [], drop xml) + +let raw_print xml = + let buf = Buffer.create 1024 in + let rec print = function + | PCData s -> Buffer.add_string buf s + | Element (_, _, cs) -> List.iter print cs + in + let () = print xml in + Buffer.contents buf + +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 05c16621ba..807d52aba4 100644 --- a/lib/richpp.mli +++ b/lib/richpp.mli @@ -39,3 +39,29 @@ val xml_of_rich_pp : ('annotation -> (string * string) list) -> 'annotation located Xml_datatype.gxml -> Xml_datatype.xml + +(** {5 Enriched text} *) + +type richpp +(** Type of text with style annotations *) + +val richpp_of_pp : Pp.std_ppcmds -> richpp +(** Extract style information from formatted text *) + +val richpp_of_xml : Xml_datatype.xml -> richpp +(** Do not use outside of dedicated areas *) + +val richpp_of_string : string -> richpp +(** Make a styled text out of a normal string *) + +val repr : richpp -> Xml_datatype.xml +(** Observe the styled text as XML *) + +(** {5 Serialization} *) + +val of_richpp : richpp -> Xml_datatype.xml +val to_richpp : Xml_datatype.xml -> richpp + +(** Represent the semi-structured document as a string, dropping any additional + information. *) +val raw_print : richpp -> string diff --git a/lib/serialize.ml b/lib/serialize.ml index 79a79dd4e0..685ec6049c 100644 --- a/lib/serialize.ml +++ b/lib/serialize.ml @@ -114,3 +114,7 @@ let to_loc xml = 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 index 2a8e531639..d7c14e7e73 100644 --- a/lib/serialize.mli +++ b/lib/serialize.mli @@ -35,3 +35,5 @@ 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 fda4b4239a..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 diff --git a/lib/system.ml b/lib/system.ml index b4b3882d33..8b53a11d67 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -12,37 +12,27 @@ open Pp open Errors open Util -(* All subdirectories, recursively *) +include Minisys -let exists_dir dir = - try Sys.is_directory dir with Sys_error _ -> false - -let skipped_dirnames = ref ["CVS"; "_darcs"] - -let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames - -let ok_dirname f = - not (String.is_empty f) && f.[0] != '.' && - not (String.List.mem f !skipped_dirnames) && - (match Unicode.ident_refutation f with None -> true | _ -> false) - -let readdir dir = try Sys.readdir dir with any -> [||] +(** Returns the list of all recursive subdirectories of [root] in + depth-first search, with sons ordered as on the file system; + warns if [root] does not exist *) let all_subdirs ~unix_path:root = let l = ref [] in let add f rel = l := (f, rel) :: !l in - let rec traverse dir rel = - Array.iter (fun f -> - if ok_dirname f then - let file = Filename.concat dir f in - if exists_dir file then begin - let newrel = rel @ [f] in - add file newrel; - traverse file newrel - end) - (readdir dir) + let rec traverse path rel = + let f = function + | FileDir (path,f) -> + let newrel = rel @ [f] in + add path newrel; + traverse path newrel + | _ -> () + in process_directory f path in - if exists_dir root then traverse root []; + check_unix_dir (fun s -> Feedback.msg_warning (str s)) root; + if exists_dir root then traverse root [] + else Feedback.msg_warning (str ("Cannot open " ^ root)); List.rev !l (* Caching directory contents for efficient syntactic equality of file @@ -63,20 +53,22 @@ let make_dir_table dir = Array.fold_left filter_dotfiles StrSet.empty (readdir dir) let exists_in_dir_respecting_case dir bf = - let contents, cached = - try StrMap.find dir !dirmap, true with Not_found -> + let cache_dir dir = let contents = make_dir_table dir in dirmap := StrMap.add dir contents !dirmap; - contents, false in + contents in + let contents, fresh = + try + (* in batch mode, assume the directory content is still fresh *) + StrMap.find dir !dirmap, !Flags.batch_mode + with Not_found -> + (* in batch mode, we are not yet sure the directory exists *) + if !Flags.batch_mode && not (exists_dir dir) then StrSet.empty, true + else cache_dir dir, true in StrSet.mem bf contents || - if cached then begin + not fresh && (* rescan, there is a new file we don't know about *) - let contents = make_dir_table dir in - dirmap := StrMap.add dir contents !dirmap; - StrSet.mem bf contents - end - else - false + StrSet.mem bf (cache_dir dir) let file_exists_respecting_case path f = (* This function ensures that a file with expected lowercase/uppercase @@ -86,7 +78,7 @@ let file_exists_respecting_case path f = let df = Filename.dirname f in (String.equal df "." || aux df) && exists_in_dir_respecting_case (Filename.concat path df) bf - in Sys.file_exists (Filename.concat path f) && aux f + in (!Flags.batch_mode || Sys.file_exists (Filename.concat path f)) && aux f let rec search paths test = match paths with @@ -99,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()) @@ -155,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 = @@ -166,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 = @@ -295,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 fa675a4f02..4dbb3695d2 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -8,14 +8,46 @@ (** {5 Coqtop specific system utilities} *) +(** {6 Directories} *) + +type unix_path = string (* path in unix-style, with '/' separator *) + +type file_kind = + | FileDir of unix_path * (* basename of path: *) string + | FileRegular of string (* basename of file *) + +val (//) : unix_path -> string -> unix_path + +val exists_dir : unix_path -> bool + +(** [check_unix_dir warn path] calls [warn] with an appropriate + message if [path] looks does not look like a Unix path on Windows *) + +val check_unix_dir : (string -> unit) -> unix_path -> unit + +(** [exclude_search_in_dirname path] excludes [path] when processing + directories *) + +val exclude_directory : unix_path -> unit + +(** [process_directory f path] applies [f] on contents of directory + [path]; fails with Unix_error if the latter does not exists; skips + all files or dirs starting with "." *) + +val process_directory : (file_kind -> unit) -> unix_path -> unit + +(** [process_subdirectories f path] applies [f path/file file] on each + [file] of the directory [path]; fails with Unix_error if the + latter does not exists; kips all files or dirs starting with "." *) + +val process_subdirectories : (unix_path -> string -> unit) -> unix_path -> unit + (** {6 Files and load paths} *) (** Load path entries remember the original root given by the user. For efficiency, we keep the full path (field [directory]), the root path and the path relative to the root. *) -val exclude_search_in_dirname : string -> unit - val all_subdirs : unix_path:string -> (CUnix.physical_path * string list) list val is_in_path : CUnix.load_path -> string -> bool val is_in_system_path : string -> bool @@ -24,8 +56,6 @@ val where_in_path : val where_in_path_rex : CUnix.load_path -> Str.regexp -> (CUnix.physical_path * string) list -val exists_dir : string -> bool - val find_file_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string diff --git a/lib/unicode.ml b/lib/unicode.ml index 0dc4238ee4..7aa8d9d513 100644 --- a/lib/unicode.ml +++ b/lib/unicode.ml @@ -18,7 +18,7 @@ exception Unsupported to simplify the masking process. (This choice seems to be a good trade-off between speed and space after some benchmarks.) *) -(* A 256ko table, initially filled with zeros. *) +(* A 256 KiB table, initially filled with zeros. *) let table = Array.make (1 lsl 17) 0 (* Associate a 2-bit pattern to each status at position [i]. @@ -147,6 +147,11 @@ let utf8_of_unicode n = s end +(* If [s] is some UTF-8 encoded string + and [i] is a position of some UTF-8 character within [s] + then [next_utf8 s i] returns [(j,n)] where: + - [j] indicates the position of the next UTF-8 character + - [n] represents the UTF-8 character at index [i] *) let next_utf8 s i = let err () = invalid_arg "utf8" in let l = String.length s - i in diff --git a/lib/unicode.mli b/lib/unicode.mli index 00211164fb..aaf455dec5 100644 --- a/lib/unicode.mli +++ b/lib/unicode.mli @@ -10,17 +10,21 @@ type status = Letter | IdentPart | Symbol +(** This exception is raised when UTF-8 the input string contains unsupported UTF-8 characters. *) exception Unsupported -(** Classify a unicode char into 3 classes, or raise [Unsupported] *) +(** Classify a unicode char into 3 classes. + @raise Unsupported if the input string contains unsupported UTF-8 characters. *) val classify : int -> status -(** Check whether a given string be used as a legal identifier. - - [None] means yes - - [Some (b,s)] means no, with explanation [s] and severity [b] *) +(** Return [None] if a given string can be used as a (Coq) identifier. + Return [Some (b,s)] otherwise, where [s] is an explanation and [b] is severity. + @raise Unsupported if the input string contains unsupported UTF-8 characters. *) val ident_refutation : string -> (bool * string) option -(** First char of a string, converted to lowercase *) +(** First char of a string, converted to lowercase + @raise Unsupported if the input string contains unsupported UTF-8 characters. + @raise Assert_failure if the input string is empty. *) val lowercase_first_char : string -> string (** Return [true] if all UTF-8 characters in the input string are just plain diff --git a/lib/util.ml b/lib/util.ml index a20dba0fc4..009dfbe1c1 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -87,7 +87,13 @@ let matrix_transpose mat = let identity x = x -let compose f g x = f (g x) +(** Function composition: the mathematical [∘] operator. + + So [g % f] is a synonym for [fun x -> g (f x)]. + + Also because [%] is right-associative, [h % g % f] means [fun x -> h (g (f x))]. + *) +let (%) f g x = f (g x) let const x _ = x @@ -124,10 +130,26 @@ let delayed_force f = f () type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a +type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq + +module Union = +struct + let map f g = function + | Inl a -> Inl (f a) + | Inr b -> Inr (g b) + + (** Lifting equality onto union types. *) + let equal f g x y = match x, y with + | Inl x, Inl y -> f x y + | Inr x, Inr y -> g x y + | _, _ -> false + + let fold_left f g a = function + | Inl y -> f a y + | Inr y -> g a y +end -let map_union f g = function - | Inl a -> Inl (f a) - | Inr b -> Inr (g b) +let map_union = Union.map type iexn = Exninfo.iexn diff --git a/lib/util.mli b/lib/util.mli index 4156af6728..6bed7e3552 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -83,7 +83,15 @@ val matrix_transpose : 'a list list -> 'a list list (** {6 Functions. } *) val identity : 'a -> 'a -val compose : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b + +(** Function composition: the mathematical [∘] operator. + + So [g % f] is a synonym for [fun x -> g (f x)]. + + Also because [%] is right-associative, [h % g % f] means [fun x -> h (g (f x))]. +*) +val (%) : ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b + val const : 'a -> 'b -> 'a val iterate : ('a -> 'a) -> int -> 'a -> 'a val repeat : int -> ('a -> unit) -> 'a -> unit @@ -106,10 +114,20 @@ val iraise : iexn -> 'a type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b (** Union type *) +module Union : +sig + val map : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union + val equal : ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> ('a, 'b) union -> ('a, 'b) union -> bool + val fold_left : ('c -> 'a -> 'c) -> ('c -> 'b -> 'c) -> 'c -> ('a, 'b) union -> 'c +end + val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union +(** Alias for [Union.map] *) type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a (** Used for browsable-until structures. *) +type ('a, 'b) eq = ('a, 'b) CSig.eq = Refl : ('a, 'a) eq + val open_utf8_file_in : string -> in_channel (** Open an utf-8 encoded file and skip the byte-order mark if any. *) |