From 77101ea44d88983ec399c8662b81f9392d92110b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 10 Sep 2015 10:40:49 +0200 Subject: Fixing the XML lexer definition of names to match the standard. --- lib/xml_lexer.mll | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'lib') diff --git a/lib/xml_lexer.mll b/lib/xml_lexer.mll index f6943dd132..0b541ee047 100644 --- a/lib/xml_lexer.mll +++ b/lib/xml_lexer.mll @@ -88,7 +88,8 @@ let error lexbuf e = let newline = ['\n'] let break = ['\r'] let space = [' ' '\t'] -let identchar = ['A'-'Z' 'a'-'z' '_' '0'-'9' ':' '-'] +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' '<' '>' '&'] @@ -226,7 +227,7 @@ and entity = parse { raise (Error EUnterminatedEntity) } and ident_name = parse - | identchar+ + | ident { lexeme lexbuf } | _ | eof { error lexbuf EIdentExpected } @@ -252,7 +253,7 @@ and attributes = parse } and attribute = parse - | identchar+ + | ident { lexeme lexbuf } | _ | eof { error lexbuf EAttributeNameExpected } -- cgit v1.2.3 From 3140d22d75ac3f30e97c799a05819b8838d167ca Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 10 Sep 2015 10:54:41 +0200 Subject: Fixing previous patch. --- lib/xml_lexer.mll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/xml_lexer.mll b/lib/xml_lexer.mll index 0b541ee047..290f2c89ab 100644 --- a/lib/xml_lexer.mll +++ b/lib/xml_lexer.mll @@ -89,7 +89,7 @@ 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 ident = ['A'-'Z' 'a'-'z' '_' ':'] identchar* let entitychar = ['A'-'Z' 'a'-'z'] let pcchar = [^ '\r' '\n' '<' '>' '&'] -- cgit v1.2.3 From b712864e9cf499f1298c1aca1ad8a8b17e145079 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 18 Sep 2015 12:12:05 +0200 Subject: Revert "On MacOS X, ensuring that files found in the file system have the" and "Continuing incomplete 4b5af0d6e9ec1 (on MacOS X, ensuring that files" and "Continuing 4b5af0d6e9 and 69941d4e19 about filename case check on MacOS X." This reverts commits 4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606 and 69941d4e195650bf59285b897c14d6287defea0f and e7043eec55085f4101bfb126d8829de6f6086c5a. Trying to emulate a case sensitive file system on top of a case aware one is too costly: 3x slowdown when compiling the stdlib or CompCert. --- lib/envars.ml | 19 +++---------------- lib/system.ml | 16 ++-------------- lib/system.mli | 2 -- 3 files changed, 5 insertions(+), 32 deletions(-) (limited to 'lib') diff --git a/lib/envars.ml b/lib/envars.ml index ac0b6f722e..b0eed8386b 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -39,25 +39,12 @@ let path_to_list p = let user_path () = path_to_list (Sys.getenv "PATH") (* may raise Not_found *) - (* Duplicated from system.ml to minimize dependencies *) -let file_exists_respecting_case f = - if Coq_config.arch = "Darwin" then - (* ensure that the file exists with expected case on the - case-insensitive but case-preserving default MacOS file system *) - let rec aux f = - let bf = Filename.basename f in - let df = Filename.dirname f in - String.equal df "." || String.equal df "/" || - aux df && Array.exists (String.equal bf) (Sys.readdir df) - in aux f - else Sys.file_exists f - let rec which l f = match l with | [] -> raise Not_found | p :: tl -> - if file_exists_respecting_case (p / f) then + if Sys.file_exists (p / f) then p else which tl f @@ -115,7 +102,7 @@ let _ = If the check fails, then [oth ()] is evaluated. *) let check_file_else ~dir ~file oth = let path = if Coq_config.local then coqroot else coqroot / dir in - if file_exists_respecting_case (path / file) then path else oth () + if Sys.file_exists (path / file) then path else oth () let guess_coqlib fail = let prelude = "theories/Init/Prelude.vo" in @@ -147,7 +134,7 @@ let coqpath = let coqpath = getenv_else "COQPATH" (fun () -> "") in let make_search_path path = let paths = path_to_list path in - let valid_paths = List.filter file_exists_respecting_case paths in + let valid_paths = List.filter Sys.file_exists paths in List.rev valid_paths in make_search_path coqpath diff --git a/lib/system.ml b/lib/system.ml index 27e21204cc..d1cdd8efc9 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -53,18 +53,6 @@ let all_subdirs ~unix_path:root = if exists_dir root then traverse root []; List.rev !l -let file_exists_respecting_case f = - if Coq_config.arch = "Darwin" then - (* ensure that the file exists with expected case on the - case-insensitive but case-preserving default MacOS file system *) - let rec aux f = - let bf = Filename.basename f in - let df = Filename.dirname f in - (String.equal df "." || String.equal df "/" || aux df) - && Array.exists (String.equal bf) (Sys.readdir df) - in aux f - else Sys.file_exists f - let rec search paths test = match paths with | [] -> [] @@ -89,7 +77,7 @@ let where_in_path ?(warn=true) path filename = in check_and_warn (search path (fun lpe -> let f = Filename.concat lpe filename in - if file_exists_respecting_case f then [lpe,f] else [])) + if Sys.file_exists f then [lpe,f] else [])) let where_in_path_rex path rex = search path (fun lpe -> @@ -105,7 +93,7 @@ let where_in_path_rex path rex = let find_file_in_path ?(warn=true) paths filename = if not (Filename.is_implicit filename) then - if file_exists_respecting_case filename then + if Sys.file_exists filename then let root = Filename.dirname filename in root, filename else diff --git a/lib/system.mli b/lib/system.mli index 051e92f166..a3d66d577a 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -29,8 +29,6 @@ val exists_dir : string -> bool val find_file_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string -val file_exists_respecting_case : 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] -- cgit v1.2.3 From f4584f8a332c9077844e227c8b86d3cb1daf8b12 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 14 Sep 2015 16:40:28 +0200 Subject: Adding rich printing primitives. --- lib/richpp.ml | 34 ++++++++++++++++++++++++++++++++++ lib/richpp.mli | 26 ++++++++++++++++++++++++++ lib/serialize.ml | 4 ++++ lib/serialize.mli | 2 ++ 4 files changed, 66 insertions(+) (limited to 'lib') diff --git a/lib/richpp.ml b/lib/richpp.ml index c4a9c39d5a..fff989ce0a 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 a0d3c374b2..7e4b58c9a6 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 aa2e3f02a4..b14bfb2833 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 34d3e054cd..f4eac5a6b9 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 -- cgit v1.2.3 From f20fce1259563f2081fadc62ccab1304bb8161d5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 21 Aug 2015 19:00:59 +0200 Subject: Rich printing of messages. --- lib/feedback.ml | 6 +++--- lib/feedback.mli | 2 +- lib/pp.ml | 6 +++--- lib/pp.mli | 4 ++-- 4 files changed, 9 insertions(+), 9 deletions(-) (limited to 'lib') diff --git a/lib/feedback.ml b/lib/feedback.ml index a5e16ea04c..1726da2fdb 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -18,7 +18,7 @@ type message_level = type message = { message_level : message_level; - message_content : string; + 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 diff --git a/lib/feedback.mli b/lib/feedback.mli index 52a0e9fe6f..38c867f5b5 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -18,7 +18,7 @@ type message_level = type message = { message_level : message_level; - message_content : string; + message_content : xml; } val of_message : message -> xml diff --git a/lib/pp.ml b/lib/pp.ml index 30bc30a9ad..01df2510cf 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -412,7 +412,7 @@ type message_level = Feedback.message_level = type message = Feedback.message = { message_level : message_level; - message_content : string; + message_content : Xml_datatype.xml; } let of_message = Feedback.of_message @@ -511,11 +511,11 @@ let string_of_ppcmds c = msg_with Format.str_formatter c; Format.flush_str_formatter () -let log_via_feedback () = logger := (fun ~id lvl msg -> +let log_via_feedback printer = logger := (fun ~id lvl msg -> !feeder { Feedback.contents = Feedback.Message { message_level = lvl; - message_content = string_of_ppcmds msg }; + message_content = printer msg }; Feedback.route = !feedback_route; Feedback.id = id }) diff --git a/lib/pp.mli b/lib/pp.mli index 3b1123a9dc..d034e67617 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -116,7 +116,7 @@ type message_level = Feedback.message_level = type message = Feedback.message = { message_level : message_level; - message_content : string; + message_content : Xml_datatype.xml; } type logger = message_level -> std_ppcmds -> unit @@ -154,7 +154,7 @@ val std_logger : logger val set_logger : logger -> unit -val log_via_feedback : unit -> 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 -- cgit v1.2.3 From 82a618e8a4945752698a7900c8af7a51091f7b1b Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 29 Sep 2015 17:05:45 +0200 Subject: Prevent States.intern_state and System.extern_intern from looking up files in the loadpath. This patch causes a bit of code duplication (because of the .coq suffix added to state files) but it makes it clear which part of the code is looking up files in the loadpath and for what purpose. Also it makes the interface of System.extern_intern and System.raw_extern_intern much saner. --- lib/system.ml | 11 +++++------ lib/system.mli | 6 +++--- 2 files changed, 8 insertions(+), 9 deletions(-) (limited to 'lib') diff --git a/lib/system.ml b/lib/system.ml index d1cdd8efc9..139effd9fa 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -178,7 +178,7 @@ let raw_extern_intern magic = let extern_state filename = let channel = open_trapping_failure filename in output_binary_int channel magic; - filename, channel + channel and intern_state filename = try let channel = open_in_bin filename in @@ -191,11 +191,11 @@ let raw_extern_intern magic = in (extern_state,intern_state) -let extern_intern ?(warn=true) magic = +let extern_intern magic = let (raw_extern,raw_intern) = raw_extern_intern magic in - let extern_state name val_0 = + let extern_state filename val_0 = try - let (filename,channel) = raw_extern name in + let channel = raw_extern filename in try marshal_out channel val_0; close_out channel @@ -205,9 +205,8 @@ let extern_intern ?(warn=true) magic = iraise reraise with Sys_error s -> errorlabstrm "System.extern_state" (str "System error: " ++ str s) - and intern_state paths name = + and intern_state filename = try - let _,filename = find_file_in_path ~warn paths name in let channel = raw_intern filename in let v = marshal_in filename channel in close_in channel; diff --git a/lib/system.mli b/lib/system.mli index a3d66d577a..5797502e9f 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -37,10 +37,10 @@ val find_file_in_path : exception Bad_magic_number of string val raw_extern_intern : int -> - (string -> string * out_channel) * (string -> in_channel) + (string -> out_channel) * (string -> in_channel) -val extern_intern : ?warn:bool -> int -> - (string -> 'a -> unit) * (CUnix.load_path -> string -> 'a) +val extern_intern : int -> + (string -> 'a -> unit) * (string -> 'a) val with_magic_number_check : ('a -> 'b) -> 'a -> 'b -- cgit v1.2.3 From 05ab666a1283de5500dbc0520d18bdb05d95f286 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 29 Sep 2015 17:45:27 +0200 Subject: Make the interface of System.raw_extern_intern much saner. There is no reason (any longer?) to create simultaneous closures for interning and externing files. This patch makes the code more readable by separating both functions and their signatures. --- lib/system.ml | 71 +++++++++++++++++++++++++++------------------------------- lib/system.mli | 10 +++++---- 2 files changed, 39 insertions(+), 42 deletions(-) (limited to 'lib') diff --git a/lib/system.ml b/lib/system.ml index 139effd9fa..ddc56956c5 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -174,47 +174,42 @@ let skip_in_segment f ch = exception Bad_magic_number of string -let raw_extern_intern magic = - let extern_state filename = - let channel = open_trapping_failure filename in - output_binary_int channel magic; +let raw_extern_state magic filename = + let channel = open_trapping_failure filename in + output_binary_int channel magic; + channel + +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); channel - and intern_state 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); - channel - with - | End_of_file -> error_corrupted filename "premature end of file" - | Failure s | Sys_error s -> error_corrupted filename s - in - (extern_state,intern_state) + with + | End_of_file -> error_corrupted filename "premature end of file" + | Failure s | Sys_error s -> error_corrupted filename s -let extern_intern magic = - let (raw_extern,raw_intern) = raw_extern_intern magic in - let extern_state filename val_0 = - try - let channel = raw_extern filename in - try - marshal_out channel val_0; - close_out channel - with reraise -> - let reraise = Errors.push reraise in - let () = try_remove filename in - iraise reraise - with Sys_error s -> - errorlabstrm "System.extern_state" (str "System error: " ++ str s) - and intern_state filename = +let extern_state magic filename val_0 = + try + let channel = raw_extern_state magic filename in try - let channel = raw_intern filename in - let v = marshal_in filename channel in - close_in channel; - v - with Sys_error s -> - errorlabstrm "System.intern_state" (str "System error: " ++ str s) - in - (extern_state,intern_state) + marshal_out channel val_0; + close_out channel + with reraise -> + let reraise = Errors.push reraise in + let () = try_remove filename in + iraise reraise + with Sys_error s -> + errorlabstrm "System.extern_state" (str "System error: " ++ str s) + +let intern_state magic filename = + try + let channel = raw_intern_state magic filename in + let v = marshal_in filename channel in + close_in channel; + v + with Sys_error s -> + errorlabstrm "System.intern_state" (str "System error: " ++ str s) let with_magic_number_check f a = try f a diff --git a/lib/system.mli b/lib/system.mli index 5797502e9f..247d528b97 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -36,11 +36,13 @@ val find_file_in_path : exception Bad_magic_number of string -val raw_extern_intern : int -> - (string -> out_channel) * (string -> in_channel) +val raw_extern_state : int -> string -> out_channel -val extern_intern : int -> - (string -> 'a -> unit) * (string -> 'a) +val raw_intern_state : int -> string -> in_channel + +val extern_state : int -> string -> 'a -> unit + +val intern_state : int -> string -> 'a val with_magic_number_check : ('a -> 'b) -> 'a -> 'b -- cgit v1.2.3 From 832ef36c5b066f5cb50a85b9a1450eaf7dcb9e44 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 2 Oct 2015 14:41:29 +0200 Subject: emacs output mode: Added tag to debug messages. So that they display in response buffer. --- lib/pp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/pp.ml b/lib/pp.ml index 30bc30a9ad..1711008ead 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -424,7 +424,7 @@ type logger = message_level -> std_ppcmds -> unit let make_body info s = emacs_quote (hov 0 (info ++ spc () ++ s)) -let debugbody strm = hov 0 (str "Debug:" ++ spc () ++ strm) +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 -- cgit v1.2.3 From 173f07a8386bf4d3d45b49d3dc01ab047b3ad4f9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 28 Sep 2015 16:50:25 +0200 Subject: Future: make not-here/not-ready messages customizable --- lib/future.ml | 20 +++++++++++++------- lib/future.mli | 3 +++ 2 files changed, 16 insertions(+), 7 deletions(-) (limited to 'lib') diff --git a/lib/future.ml b/lib/future.ml index 02d3702d77..78a158264b 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -11,21 +11,27 @@ let freeze = ref (fun () -> assert false : unit -> Dyn.t) let unfreeze = ref (fun _ -> () : Dyn.t -> unit) let set_freeze f g = freeze := f; unfreeze := g -exception NotReady of string -exception NotHere of string -let _ = Errors.register_handler (function - | NotReady name -> +let not_ready_msg = ref (fun name -> Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^ "Please wait or pass "^ "the \"-async-proofs off\" option to CoqIDE to disable "^ "asynchronous script processing and don't pass \"-quick\" to "^ - "coqc.") - | NotHere name -> + "coqc.")) +let not_here_msg = ref (fun name -> Pp.strbrk("The value you are asking for ("^name^") is not available "^ "in this process. If you really need this, pass "^ "the \"-async-proofs off\" option to CoqIDE to disable "^ "asynchronous script processing and don't pass \"-quick\" to "^ - "coqc.") + "coqc.")) + +let customize_not_ready_msg f = not_ready_msg := f +let customize_not_here_msg f = not_here_msg := f + +exception NotReady of string +exception NotHere of string +let _ = Errors.register_handler (function + | NotReady name -> !not_ready_msg name + | NotHere name -> !not_here_msg name | _ -> raise Errors.Unhandled) type fix_exn = Exninfo.iexn -> Exninfo.iexn diff --git a/lib/future.mli b/lib/future.mli index 324d5f7d10..de2282ae92 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -161,3 +161,6 @@ val print : ('a -> Pp.std_ppcmds) -> 'a computation -> Pp.std_ppcmds 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 customize_not_ready_msg : (string -> Pp.std_ppcmds) -> unit +val customize_not_here_msg : (string -> Pp.std_ppcmds) -> unit -- cgit v1.2.3 From 188ab7f76459ab46e0ea139da8b4331d958c7102 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 5 Oct 2015 18:39:06 +0200 Subject: Spawn: use each socket exclusively for writing or reading According to http://caml.inria.fr/mantis/view.php?id=5325 you can't use the same socket for both writing and reading. The result is lockups (may be fixed in 4.03). --- lib/spawn.ml | 44 ++++++++++++++++++++++++++++---------------- 1 file changed, 28 insertions(+), 16 deletions(-) (limited to 'lib') diff --git a/lib/spawn.ml b/lib/spawn.ml index 9b63be70aa..851c6a2235 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -45,26 +45,38 @@ end (* Common code *) let assert_ b s = if not b then Errors.anomaly (Pp.str s) +(* According to http://caml.inria.fr/mantis/view.php?id=5325 + * you can't use the same socket for both writing and reading (may change + * in 4.03 *) let mk_socket_channel () = let open Unix in - let s = socket PF_INET SOCK_STREAM 0 in - bind s (ADDR_INET (inet_addr_loopback,0)); - listen s 1; - match getsockname s with - | ADDR_INET(host, port) -> - s, string_of_inet_addr host ^":"^ string_of_int port + let sr = socket PF_INET SOCK_STREAM 0 in + bind sr (ADDR_INET (inet_addr_loopback,0)); listen sr 1; + let sw = socket PF_INET SOCK_STREAM 0 in + bind sw (ADDR_INET (inet_addr_loopback,0)); listen sw 1; + match getsockname sr, getsockname sw with + | ADDR_INET(host, portr), ADDR_INET(_, portw) -> + (sr, sw), + string_of_inet_addr host + ^":"^ string_of_int portr ^":"^ string_of_int portw | _ -> assert false -let accept s = - let r, _, _ = Unix.select [s] [] [] accept_timeout in +let accept (sr,sw) = + let r, _, _ = Unix.select [sr] [] [] accept_timeout in if r = [] then raise (Failure (Printf.sprintf "The spawned process did not connect back in %2.1fs" accept_timeout)); - let cs, _ = Unix.accept s in - Unix.close s; - let cin, cout = Unix.in_channel_of_descr cs, Unix.out_channel_of_descr cs in + let csr, _ = Unix.accept sr in + Unix.close sr; + let cin = Unix.in_channel_of_descr csr in set_binary_mode_in cin true; + let w, _, _ = Unix.select [sw] [] [] accept_timeout in + if w = [] then raise (Failure (Printf.sprintf + "The spawned process did not connect back in %2.1fs" accept_timeout)); + let csw, _ = Unix.accept sw in + Unix.close sw; + let cout = Unix.out_channel_of_descr csw in set_binary_mode_out cout true; - cs, cin, cout + (csr, csw), cin, cout let handshake cin cout = try @@ -116,7 +128,7 @@ let spawn_pipe env prog args = let cout = Unix.out_channel_of_descr master2worker_w in set_binary_mode_in cin true; set_binary_mode_out cout true; - pid, cin, cout, worker2master_r + pid, cin, cout, (worker2master_r, master2worker_w) let filter_args args = let rec aux = function @@ -180,10 +192,10 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ()) = let pid, oob_resp, oob_req, cin, cout, main, is_sock = spawn_with_control prefer_sock env prog args in - Unix.set_nonblock main; + Unix.set_nonblock (fst main); let gchan = - if is_sock then ML.async_chan_of_socket main - else ML.async_chan_of_file main in + if is_sock then ML.async_chan_of_socket (fst main) + else ML.async_chan_of_file (fst main) in let alive, watch = true, None in let p = { cin; cout; gchan; pid; oob_resp; oob_req; alive; watch } in p.watch <- Some ( -- cgit v1.2.3 From 27bad55f6f87af2ae3ad7921d71c02e333a853bb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 5 Oct 2015 19:02:05 +0200 Subject: CThread: blocking read + threads now works --- lib/cThread.ml | 14 ++------------ 1 file changed, 2 insertions(+), 12 deletions(-) (limited to 'lib') diff --git a/lib/cThread.ml b/lib/cThread.ml index 2d1f10bf39..9cbdf5a9ea 100644 --- a/lib/cThread.ml +++ b/lib/cThread.ml @@ -8,22 +8,12 @@ type thread_ic = in_channel -let prepare_in_channel_for_thread_friendly_io ic = - Unix.set_nonblock (Unix.descr_of_in_channel ic); ic - -let safe_wait_timed_read fd time = - try Thread.wait_timed_read fd time - with Unix.Unix_error (Unix.EINTR, _, _) -> - (** On Unix, the above function may raise this exception when it is - interrupted by a signal. (It uses Unix.select internally.) *) - false +let prepare_in_channel_for_thread_friendly_io ic = ic let thread_friendly_read_fd fd s ~off ~len = let rec loop () = try Unix.read fd s off len - with Unix.Unix_error((Unix.EWOULDBLOCK|Unix.EAGAIN|Unix.EINTR),_,_) -> - while not (safe_wait_timed_read fd 0.05) do Thread.yield () done; - loop () + with Unix.Unix_error(Unix.EINTR,_,_) -> loop () in loop () -- cgit v1.2.3 From 4a0fd14dcae807e0e681cfc14daca978cb4a36e9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 6 Oct 2015 16:43:50 +0200 Subject: aux_file: export API to ease writing of a Proof Using annotator. --- lib/aux_file.ml | 2 ++ lib/aux_file.mli | 4 ++++ 2 files changed, 6 insertions(+) (limited to 'lib') diff --git a/lib/aux_file.ml b/lib/aux_file.ml index c9018c9ee9..5dedb0d0ac 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -42,6 +42,8 @@ module M = Map.Make(String) type data = string M.t type aux_file = data H.t +let contents x = x + let empty_aux_file = H.empty let get aux loc key = M.find key (H.find (Loc.unloc loc) aux) diff --git a/lib/aux_file.mli b/lib/aux_file.mli index e340fc6547..b672d3db28 100644 --- a/lib/aux_file.mli +++ b/lib/aux_file.mli @@ -13,6 +13,10 @@ val get : aux_file -> Loc.t -> string -> string val empty_aux_file : aux_file val set : aux_file -> Loc.t -> string -> string -> aux_file +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 stop_aux_file : unit -> unit val recording : unit -> bool -- cgit v1.2.3 From ed95f122f3c68becc09c653471dc2982b346d343 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 13 Oct 2015 18:30:47 +0200 Subject: Fix some typos. --- lib/xml_parser.mli | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'lib') diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli index cefb4af897..87ef787770 100644 --- a/lib/xml_parser.mli +++ b/lib/xml_parser.mli @@ -36,10 +36,10 @@ type t (** 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 occured during parsing + {!Xml.error_msg} tells you which error occurred during parsing and the {!Xml.error_pos} can be used to retreive the document - location where the error occured at.} - {li {!Xml.File_not_found} is raised when and error occured while + location where the error occurred at.} + {li {!Xml.File_not_found} is raised when and error occurred while opening a file with the {!Xml.parse_file} function.} } *) @@ -71,13 +71,13 @@ val error : error -> string (** Get the Xml error message as a string. *) val error_msg : error_msg -> string -(** Get the line the error occured at. *) +(** Get the line the error occurred at. *) val line : error_pos -> int -(** Get the relative character range (in current line) the error occured at.*) +(** 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 occured at. *) +(** Get the absolute character range the error occurred at. *) val abs_range : error_pos -> int * int val pos : Lexing.lexbuf -> error_pos -- cgit v1.2.3 From f617aeef08441e83b13f839ce767b840fddbcf7d Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 14 Oct 2015 10:39:55 +0200 Subject: Fix some typos. --- lib/xml_parser.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'lib') diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli index 87ef787770..ac2eab352f 100644 --- a/lib/xml_parser.mli +++ b/lib/xml_parser.mli @@ -37,9 +37,9 @@ type t (** 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 retreive the document + 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 and error occurred while + {li {!Xml.File_not_found} is raised when an error occurred while opening a file with the {!Xml.parse_file} function.} } *) @@ -98,7 +98,7 @@ val make : source -> t in the original Xmllight)}. *) val check_eof : t -> bool -> unit -(** Once the parser is configurated, you can run the parser on a any kind +(** 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 -- cgit v1.2.3 From c8b57f62f5ad12f8926f57fcdbc5bb2ee3c63eff Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 13 Oct 2015 11:40:22 +0200 Subject: Miscellaneous typos, spacing, US spelling in comments or variable names. --- lib/future.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/future.mli b/lib/future.mli index de2282ae92..adc15e49c7 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -91,13 +91,13 @@ val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation * When a future enters the environment a corresponding hook is run to perform * some work. If this fails, then its failure has to be annotated with the * same state id that corresponds to the future computation end. I.e. Qed - * is split into two parts, the lazy one (the future) and the eagher one + * is split into two parts, the lazy one (the future) and the eager one * (the hook), both performing some computations for the same state id. *) val fix_exn_of : 'a computation -> fix_exn (* Run remotely, returns the function to assign. If not blocking (the default) it raises NotReady if forced before the - delage assigns it. *) + delegate assigns it. *) type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation] val create_delegate : ?blocking:bool -> name:string -> -- cgit v1.2.3 From de32427bd2785c365374c554b4b74e97749cb995 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 19 Oct 2015 11:28:30 +0200 Subject: Fixed #4274, bad formatting of messages in emacs mode. --- lib/pp.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/pp.ml b/lib/pp.ml index 1711008ead..4ed4b17791 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -362,11 +362,11 @@ let emacs_quote_info_start = "" let emacs_quote_info_end = "" let emacs_quote g = - if !print_emacs then str emacs_quote_start ++ hov 0 g ++ str emacs_quote_end + 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 str emacs_quote_info_start++fnl() ++ hov 0 g ++ str emacs_quote_info_end + 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 -- cgit v1.2.3 From 3940441dffdfc3a8f968760c249f6a2e8a1e0912 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 22 Sep 2015 09:05:44 +0200 Subject: Generalizing the patch to bug #2554 on fixing path looking with correct case on MacOS X whose file system is case-insensitive but case-preserving (HFS+ configured in case-insensitive mode). Generalized it to any case-preserving case-insensitive file system, which makes it applicable to Windows with NTFS used in case-insensitive mode but also to Linux when mounting a case-insensitive file system. Removed the blow-up of the patch, improved the core of the patch by checking whether the case is correct only for the suffix part of the file to be found (not for the part which corresponds to the path in which where to look), and finally used a cache so that the effect of the patch is not observable. Note that the cache is implemented in a way not synchronous with backtracking what implies e.g. that a file compiled in the middle of an interactive session would not be found until Coq is restarted, even by backtracking before the corresponding Require. For history see commits b712864e9cf499f1298c1aca1ad8a8b17e145079, 4b5af0d6e9ec1343a2c3ff9f856a019fa93c3606 69941d4e195650bf59285b897c14d6287defea0f e7043eec55085f4101bfb126d8829de6f6086c5a. as well as https://coq.inria.fr/bugs/show_bug.cgi?id=2554 discussion on coq-club "8.5 and MathClasses" (May 2015) discussion on coqdev "Coq awfully slow on MacOS X" (Sep 2015) --- lib/envars.ml | 5 ++++- lib/system.ml | 50 +++++++++++++++++++++++++++++++++++++++++++++++++- lib/system.mli | 2 ++ 3 files changed, 55 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/envars.ml b/lib/envars.ml index b0eed8386b..2b8af917fa 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -39,6 +39,8 @@ let path_to_list p = let user_path () = path_to_list (Sys.getenv "PATH") (* may raise Not_found *) +(* Finding a name in path using the equality provided by the file system *) +(* whether it is case-sensitive or case-insensitive *) let rec which l f = match l with | [] -> @@ -99,7 +101,8 @@ let _ = (** [check_file_else ~dir ~file oth] checks if [file] exists in the installation directory [dir] given relatively to [coqroot]. If this Coq is only locally built, then [file] must be in [coqroot]. - If the check fails, then [oth ()] is evaluated. *) + If the check fails, then [oth ()] is evaluated. + Using file system equality seems well enough for this heuristic *) let check_file_else ~dir ~file oth = let path = if Coq_config.local then coqroot else coqroot / dir in if Sys.file_exists (path / file) then path else oth () diff --git a/lib/system.ml b/lib/system.ml index ddc56956c5..02d5e963ff 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -53,6 +53,49 @@ let all_subdirs ~unix_path:root = if exists_dir root then traverse root []; List.rev !l +(* Caching directory contents for efficient syntactic equality of file + names even on case-preserving but case-insensitive file systems *) + +module StrMod = struct + type t = string + let compare = compare +end + +module StrMap = Map.Make(StrMod) +module StrSet = Set.Make(StrMod) + +let dirmap = ref StrMap.empty + +let make_dir_table dir = + let b = ref StrSet.empty in + let a = Unix.opendir dir in + (try + while true do + let s = Unix.readdir a in + if s.[0] != '.' then b := StrSet.add s !b + done + with + | End_of_file -> ()); + Unix.closedir a; !b + +let exists_in_dir_respecting_case dir bf = + let contents = + try StrMap.find dir !dirmap with Not_found -> + let contents = make_dir_table dir in + dirmap := StrMap.add dir contents !dirmap; + contents in + StrSet.mem bf contents + +let file_exists_respecting_case path f = + (* This function ensures that a file with expected lowercase/uppercase + is the correct one, even on case-insensitive file systems *) + let rec aux f = + let bf = Filename.basename f in + 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 + let rec search paths test = match paths with | [] -> [] @@ -77,7 +120,7 @@ let where_in_path ?(warn=true) path filename = in check_and_warn (search path (fun lpe -> let f = Filename.concat lpe filename in - if Sys.file_exists f then [lpe,f] else [])) + if file_exists_respecting_case lpe filename then [lpe,f] else [])) let where_in_path_rex path rex = search path (fun lpe -> @@ -93,6 +136,8 @@ let where_in_path_rex path rex = let find_file_in_path ?(warn=true) paths filename = if not (Filename.is_implicit filename) then + (* the name is considered to be a physical name and we use the file + system rules (e.g. possible case-insensitivity) to find it *) if Sys.file_exists filename then let root = Filename.dirname filename in root, filename @@ -100,6 +145,9 @@ let find_file_in_path ?(warn=true) paths filename = errorlabstrm "System.find_file_in_path" (hov 0 (str "Can't find file" ++ spc () ++ str filename)) else + (* the name is considered to be the transcription as a relative + physical name of a logical name, so we deal with it as a name + to be locate respecting case *) try where_in_path ~warn paths filename with Not_found -> errorlabstrm "System.find_file_in_path" diff --git a/lib/system.mli b/lib/system.mli index 247d528b97..c2d64fe0d0 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -29,6 +29,8 @@ val exists_dir : string -> bool val find_file_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string +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] -- cgit v1.2.3 From b1a5fe3686ecd5b03e5c7c2efd95716a8e5270ea Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 4 Nov 2015 22:22:17 +0100 Subject: Fix for case-insensitive path looking continued (#2554): Adding a second chance to dynamically regenerate the file system cache when a file is not found (suggested by Guillaume M.). --- lib/system.ml | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) (limited to 'lib') diff --git a/lib/system.ml b/lib/system.ml index 02d5e963ff..2e35a98f7f 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -79,12 +79,20 @@ let make_dir_table dir = Unix.closedir a; !b let exists_in_dir_respecting_case dir bf = - let contents = - try StrMap.find dir !dirmap with Not_found -> + let contents, cached = + try StrMap.find dir !dirmap, true with Not_found -> let contents = make_dir_table dir in dirmap := StrMap.add dir contents !dirmap; - contents in - StrSet.mem bf contents + contents, false in + StrSet.mem bf contents || + if cached then begin + (* 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 let file_exists_respecting_case path f = (* This function ensures that a file with expected lowercase/uppercase -- cgit v1.2.3 From 153d77d00ccbacf22aa5d70ca2c1cacab2749339 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 4 Dec 2015 21:46:12 +0100 Subject: Specializing the Dyn module to each usecase. Actually, we never mix the various uses of each dynamic type created through the Dyn module. To enforce this statically, we functorize the Dyn module so that we recover a fresh instance at each use point. --- lib/cSig.mli | 2 ++ lib/dyn.ml | 15 +++++++++++++++ lib/dyn.mli | 6 ++++++ lib/future.ml | 7 ++++--- lib/future.mli | 3 ++- 5 files changed, 29 insertions(+), 4 deletions(-) (limited to 'lib') diff --git a/lib/cSig.mli b/lib/cSig.mli index 2a8bda2936..4463e8d9c6 100644 --- a/lib/cSig.mli +++ b/lib/cSig.mli @@ -45,3 +45,5 @@ sig end (** Redeclaration of OCaml set signature, to preserve compatibility. See OCaml documentation for more information. *) + +module type EmptyS = sig end diff --git a/lib/dyn.ml b/lib/dyn.ml index 056b687313..60167ef1ba 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -9,6 +9,19 @@ open Errors open Pp +module type S = +sig +type t + +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 +end + +module Make(M : CSig.EmptyS) = +struct (* Dynamics, programmed with DANGER !!! *) type t = int * Obj.t @@ -48,3 +61,5 @@ let tag (s,_) = let pointer_equal (t1,o1) (t2,o2) = t1 = t2 && o1 == o2 let dump () = Int.Map.bindings !dyntab + +end \ No newline at end of file diff --git a/lib/dyn.mli b/lib/dyn.mli index cac912aca1..55c4f0ce8f 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -8,6 +8,8 @@ (** Dynamics. Use with extreme care. Not for kids. *) +module type S = +sig type t val create : string -> ('a -> t) * (t -> 'a) @@ -15,3 +17,7 @@ val tag : t -> string val has_tag : t -> string -> bool val pointer_equal : t -> t -> bool val dump : unit -> (int * string) list +end + +(** FIXME: use OCaml 4.02 generative functors when available *) +module Make(M : CSig.EmptyS) : S diff --git a/lib/future.ml b/lib/future.ml index 78a158264b..b6012ed207 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 adc15e49c7..29b71b70a8 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 -- cgit v1.2.3 From 895d34a264d9d90adfe4f0618c3bb0663dc01615 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 5 Dec 2015 12:53:20 +0100 Subject: Leveraging GADTs to provide a better Dyn API. --- lib/cSig.mli | 2 ++ lib/dyn.ml | 31 ++++++++++++------------------- lib/dyn.mli | 10 +++++----- lib/util.ml | 1 + lib/util.mli | 2 ++ 5 files changed, 22 insertions(+), 24 deletions(-) (limited to 'lib') diff --git a/lib/cSig.mli b/lib/cSig.mli index 4463e8d9c6..796e58cbfb 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 diff --git a/lib/dyn.ml b/lib/dyn.ml index 60167ef1ba..0571f3b5d6 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -11,12 +11,12 @@ open Pp module type S = sig -type t +type 'a tag +type t = Dyn : 'a tag * 'a -> t -val create : string -> ('a -> t) * (t -> 'a) -val tag : t -> string -val has_tag : t -> string -> bool -val pointer_equal : t -> t -> bool +val create : string -> 'a tag +val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option +val repr : 'a tag -> string val dump : unit -> (int * string) list end @@ -24,7 +24,9 @@ module Make(M : CSig.EmptyS) = struct (* Dynamics, programmed with DANGER !!! *) -type t = int * Obj.t +type 'a tag = int + +type t = Dyn : 'a tag * 'a -> t let dyntab = ref (Int.Map.empty : string Int.Map.t) (** Instead of working with tags as strings, which are costly, we use their @@ -41,25 +43,16 @@ let create (s : string) = anomaly ~label:"Dyn.create" msg 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 pointer_equal (t1,o1) (t2,o2) = t1 = t2 && o1 == o2 - let dump () = Int.Map.bindings !dyntab end \ No newline at end of file diff --git a/lib/dyn.mli b/lib/dyn.mli index 55c4f0ce8f..28587859e1 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -10,12 +10,12 @@ module type S = sig -type t +type 'a tag +type t = Dyn : 'a tag * 'a -> t -val create : string -> ('a -> t) * (t -> 'a) -val tag : t -> string -val has_tag : t -> string -> bool -val pointer_equal : t -> t -> bool +val create : string -> 'a tag +val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option +val repr : 'a tag -> string val dump : unit -> (int * string) list end diff --git a/lib/util.ml b/lib/util.ml index a20dba0fc4..b67539918d 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -124,6 +124,7 @@ 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 let map_union f g = function | Inl a -> Inl (f a) diff --git a/lib/util.mli b/lib/util.mli index 1dc405fcbe..0ce6cc6603 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -111,5 +111,7 @@ val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union 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. *) -- cgit v1.2.3 From 126a3c998c62bfd9f9b570f12b2e29576dd94cdd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 5 Dec 2015 13:43:07 +0100 Subject: Factorizing unsafe code by relying on the new Dyn module. --- lib/clib.mllib | 1 + lib/dyn.ml | 10 ++++------ lib/lib.mllib | 1 - lib/pp.ml | 29 +++++++++++------------------ 4 files changed, 16 insertions(+), 25 deletions(-) (limited to 'lib') diff --git a/lib/clib.mllib b/lib/clib.mllib index 7ff1d29359..1770df1993 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -8,6 +8,7 @@ Hashcons CSet CMap Int +Dyn HMap Option Store diff --git a/lib/dyn.ml b/lib/dyn.ml index 0571f3b5d6..826cfaf8db 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -6,9 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors -open Pp - module type S = sig type 'a tag @@ -39,8 +36,8 @@ 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 hash @@ -51,7 +48,8 @@ let eq : 'a 'b. 'a tag -> 'b tag -> ('a, 'b) CSig.eq option = 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 dump () = Int.Map.bindings !dyntab diff --git a/lib/lib.mllib b/lib/lib.mllib index f3f6ad8fc7..a9181c51c1 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -1,6 +1,5 @@ Errors Bigint -Dyn Segmenttree Unicodetable Unicode diff --git a/lib/pp.ml b/lib/pp.ml index 146d3562dd..a1913c98f7 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -51,25 +51,18 @@ sig val prj : t -> 'a key -> 'a option end = struct - (** See module {Dyn} for more details. *) - type t = int * Obj.t - - 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 +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 end -- cgit v1.2.3 From ce9e7c2a842d7ec7734b58af64de9283de963e37 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 4 Dec 2015 19:25:08 +0100 Subject: Replace Unix.readdir by Sys.readdir in dir cache. This makes the function sightly more portable. --- lib/system.ml | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) (limited to 'lib') diff --git a/lib/system.ml b/lib/system.ml index 2e35a98f7f..91b2f5afaf 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -67,16 +67,8 @@ module StrSet = Set.Make(StrMod) let dirmap = ref StrMap.empty let make_dir_table dir = - let b = ref StrSet.empty in - let a = Unix.opendir dir in - (try - while true do - let s = Unix.readdir a in - if s.[0] != '.' then b := StrSet.add s !b - done - with - | End_of_file -> ()); - Unix.closedir a; !b + 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) let exists_in_dir_respecting_case dir bf = let contents, cached = -- cgit v1.2.3 From 9d45d45f3a8718581a001af4576ca87feb741073 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 9 Dec 2015 14:56:17 +0100 Subject: Remove remaining occurrences of Unix.readdir. --- lib/system.ml | 30 ++++++++++-------------------- 1 file changed, 10 insertions(+), 20 deletions(-) (limited to 'lib') diff --git a/lib/system.ml b/lib/system.ml index 91b2f5afaf..f860bd2f7e 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -11,12 +11,11 @@ open Pp open Errors open Util -open Unix (* All subdirectories, recursively *) let exists_dir dir = - try let _ = closedir (opendir dir) in true with Unix_error _ -> false + try Sys.is_directory dir with Sys_error _ -> false let skipped_dirnames = ref ["CVS"; "_darcs"] @@ -31,24 +30,15 @@ let all_subdirs ~unix_path:root = let l = ref [] in let add f rel = l := (f, rel) :: !l in let rec traverse dir rel = - let dirh = opendir dir in - try - while true do - let f = readdir dirh in - if ok_dirname f then - let file = Filename.concat dir f in - try - begin match (stat file).st_kind with - | S_DIR -> - let newrel = rel @ [f] in - add file newrel; - traverse file newrel - | _ -> () - end - with Unix_error (e,s1,s2) -> () - done - with End_of_file -> - closedir dirh + Array.iter (fun f -> + if ok_dirname f then + let file = Filename.concat dir f in + if Sys.is_directory file then begin + let newrel = rel @ [f] in + add file newrel; + traverse file newrel + end) + (Sys.readdir dir) in if exists_dir root then traverse root []; List.rev !l -- cgit v1.2.3 From 20e1829ad3de42dd322af972c6f9a585f40738ef Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 10 Dec 2015 16:40:38 +0100 Subject: Fixing compilation with OCaml 3.12 after commit 9d45d45f3a87 on removing "open Unix" from lib/system.ml. --- lib/system.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/system.ml b/lib/system.ml index f860bd2f7e..a902229609 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -262,7 +262,7 @@ type time = float * float * float let get_time () = let t = Unix.times () in - (Unix.gettimeofday(), t.tms_utime, t.tms_stime) + (Unix.gettimeofday(), t.Unix.tms_utime, t.Unix.tms_stime) (* Keep only 3 significant digits *) let round f = (floor (f *. 1e3)) *. 1e-3 -- cgit v1.2.3 From 0e4f4788f710d58754b1909395b1fe9d5e001d69 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 12 Dec 2015 18:16:01 +0100 Subject: Removing dead unsafe code in Genarg. --- lib/genarg.ml | 8 -------- lib/genarg.mli | 20 -------------------- 2 files changed, 28 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index 42458ecb31..149d872c52 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -225,11 +225,3 @@ let register_name0 t name = match t with 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 a269f92774..3a18581d7b 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -256,23 +256,3 @@ val register_name0 : ('a, 'b, 'c) genarg_type -> string -> unit 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 -- cgit v1.2.3 From d58957f63d36e2da41f6f839a2d94cb0db4c8125 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 14 Dec 2015 10:44:22 +0100 Subject: Remove some occurrences of Unix.opendir. --- lib/system.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'lib') diff --git a/lib/system.ml b/lib/system.ml index b57c02a14f..b641aad91b 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -64,9 +64,7 @@ let apply_subdir f path name = | _ -> () let process_directory f path = - let dirh = Unix.opendir path in - try while true do apply_subdir f path (Unix.readdir dirh) done - with End_of_file -> Unix.closedir dirh + 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 -- cgit v1.2.3 From f439001caa24671d03d8816964ceb8e483660e70 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 10 Dec 2015 12:32:56 +0100 Subject: Adding compatibility flag for 8.5. Soon needing a more algebraic view at version numbers... --- lib/flags.ml | 13 ++++++++----- lib/flags.mli | 2 +- 2 files changed, 9 insertions(+), 6 deletions(-) (limited to 'lib') diff --git a/lib/flags.ml b/lib/flags.ml index 9a0d4b5ec1..96415ed263 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -101,18 +101,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) @@ -120,6 +122,7 @@ let pr_version = function | V8_2 -> "8.2" | V8_3 -> "8.3" | V8_4 -> "8.4" + | V8_5 -> "8.5" | Current -> "current" (* Translate *) diff --git a/lib/flags.mli b/lib/flags.mli index 29a0bbef01..cb92e1462d 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -55,7 +55,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 -- cgit v1.2.3 From 597e5dd737dd235222798153b2342ae609519348 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 16 Dec 2015 20:03:45 +0100 Subject: Getting rid of some hardwired generic arguments. --- lib/genarg.ml | 12 ------------ lib/genarg.mli | 4 ---- 2 files changed, 16 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index 149d872c52..8712eda8e1 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -18,11 +18,7 @@ type argument_type = | GenArgType | ConstrArgType | ConstrMayEvalArgType - | QuantHypArgType | OpenConstrArgType - | ConstrWithBindingsArgType - | BindingsArgType - | RedExprArgType | ListArgType of argument_type | OptArgType of argument_type | PairArgType of argument_type * argument_type @@ -35,11 +31,7 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with | 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) -> @@ -54,11 +46,7 @@ let rec pr_argument_type = function | 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) -> diff --git a/lib/genarg.mli b/lib/genarg.mli index 3a18581d7b..2dcaa789f7 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -190,11 +190,7 @@ type argument_type = | GenArgType | ConstrArgType | ConstrMayEvalArgType - | QuantHypArgType | OpenConstrArgType - | ConstrWithBindingsArgType - | BindingsArgType - | RedExprArgType | ListArgType of argument_type | OptArgType of argument_type | PairArgType of argument_type * argument_type -- cgit v1.2.3 From a17891fdc314d0fe5246ab785268e2005a8c98b2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 17 Dec 2015 18:33:14 +0100 Subject: spawn: fix leak of file descriptors The interesting manifestation of the bug was Unix.select returning no error but the empty list of descriptors, as if a timeout did happen. --- lib/spawn.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/spawn.ml b/lib/spawn.ml index 851c6a2235..01f6a4f8d3 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -175,7 +175,7 @@ let is_alive p = p.alive let uid { pid; } = string_of_int pid let unixpid { pid; } = pid -let kill ({ pid = unixpid; oob_req; cin; cout; alive; watch } as p) = +let kill ({ pid = unixpid; oob_resp; oob_req; cin; cout; alive; watch } as p) = p.alive <- false; if not alive then prerr_endline "This process is already dead" else begin try @@ -183,6 +183,8 @@ let kill ({ pid = unixpid; oob_req; cin; cout; alive; watch } as p) = output_death_sentence (uid p) oob_req; close_in_noerr cin; close_out_noerr cout; + close_in_noerr oob_resp; + close_out_noerr oob_req; if Sys.os_type = "Unix" then Unix.kill unixpid 9; p.watch <- None with e -> prerr_endline ("kill: "^Printexc.to_string e) end @@ -247,13 +249,15 @@ let is_alive p = p.alive let uid { pid; } = string_of_int pid let unixpid { pid = pid; } = pid -let kill ({ pid = unixpid; oob_req; cin; cout; alive } as p) = +let kill ({ pid = unixpid; oob_req; oob_resp; cin; cout; alive } as p) = p.alive <- false; if not alive then prerr_endline "This process is already dead" else begin try output_death_sentence (uid p) oob_req; close_in_noerr cin; close_out_noerr cout; + close_in_noerr oob_resp; + close_out_noerr oob_req; if Sys.os_type = "Unix" then Unix.kill unixpid 9; with e -> prerr_endline ("kill: "^Printexc.to_string e) end -- cgit v1.2.3 From 75d74cd7d124f244882b9c4ed200eac144dcbc43 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 8 Dec 2015 12:49:01 +0100 Subject: COMMENTS: added to the "Predicate" module In the original version, ocamldoc markup wasn't used properly thus ocamldoc output did not in all places make sense. This commit makes sure that the documentation of the Predicate module is as clear as the documentation of the Set module (in the standard library). --- lib/predicate.ml | 9 +++--- lib/predicate.mli | 85 +++++++++++++++++++++++++++++++++---------------------- 2 files changed, 56 insertions(+), 38 deletions(-) (limited to 'lib') diff --git a/lib/predicate.ml b/lib/predicate.ml index a60b3dadd4..1aa7db6af1 100644 --- a/lib/predicate.ml +++ b/lib/predicate.ml @@ -10,8 +10,6 @@ (* *) (************************************************************************) -(* Sets over ordered types *) - module type OrderedType = sig type t @@ -43,9 +41,10 @@ module Make(Ord: OrderedType) = struct module EltSet = Set.Make(Ord) - (* when bool is false, the denoted set is the complement of - the given set *) type elt = Ord.t + + (* (false, s) represents a set which is equal to the set s + (true, s) represents a set which is equal to the complement of set s *) type t = bool * EltSet.t let elements (b,s) = (b, EltSet.elements s) @@ -84,6 +83,7 @@ module Make(Ord: OrderedType) = let diff s1 s2 = inter s1 (complement s2) + (* assumes the set is infinite *) let subset s1 s2 = match (s1,s2) with ((false,p1),(false,p2)) -> EltSet.subset p1 p2 @@ -91,6 +91,7 @@ module Make(Ord: OrderedType) = | ((false,p1),(true,n2)) -> EltSet.is_empty (EltSet.inter p1 n2) | ((true,_),(false,_)) -> false + (* assumes the set is infinite *) let equal (b1,s1) (b2,s2) = b1=b2 && EltSet.equal s1 s2 diff --git a/lib/predicate.mli b/lib/predicate.mli index bcc89e7275..cee3b0bd39 100644 --- a/lib/predicate.mli +++ b/lib/predicate.mli @@ -1,67 +1,84 @@ +(** Infinite sets over a chosen [OrderedType]. -(** Module [Pred]: sets over infinite ordered types with complement. *) - -(** This module implements the set data structure, given a total ordering - function over the set elements. All operations over sets - are purely applicative (no side-effects). - The implementation uses the Set library. *) + All operations over sets are purely applicative (no side-effects). + *) +(** Input signature of the functor [Make]. *) module type OrderedType = sig type t - val compare: t -> t -> int + (** The type of the elements in the set. + + The chosen [t] {b must be infinite}. *) + + val compare : t -> t -> int + (** A total ordering function over the set elements. + This is a two-argument function [f] such that: + - [f e1 e2] is zero if the elements [e1] and [e2] are equal, + - [f e1 e2] is strictly negative if [e1] is smaller than [e2], + - and [f e1 e2] is strictly positive if [e1] is greater than [e2]. + *) end - (** The input signature of the functor [Pred.Make]. - [t] is the type of the set elements. - [compare] is a total ordering function over the set elements. - This is a two-argument function [f] such that - [f e1 e2] is zero if the elements [e1] and [e2] are equal, - [f e1 e2] is strictly negative if [e1] is smaller than [e2], - and [f e1 e2] is strictly positive if [e1] is greater than [e2]. - Example: a suitable ordering function is - the generic structural comparison function [compare]. *) module type S = sig type elt - (** The type of the set elements. *) + (** The type of the elements in the set. *) + type t - (** The type of sets. *) + (** The type of sets. *) + val empty: t - (** The empty set. *) + (** The empty set. *) + val full: t - (** The whole type. *) + (** The set of all elements (of type [elm]). *) + val is_empty: t -> bool - (** Test whether a set is empty or not. *) + (** Test whether a set is empty or not. *) + val is_full: t -> bool - (** Test whether a set contains the whole type or not. *) + (** Test whether a set contains the whole type or not. *) + val mem: elt -> t -> bool - (** [mem x s] tests whether [x] belongs to the set [s]. *) + (** [mem x s] tests whether [x] belongs to the set [s]. *) + val singleton: elt -> t - (** [singleton x] returns the one-element set containing only [x]. *) + (** [singleton x] returns the one-element set containing only [x]. *) + val add: elt -> t -> t - (** [add x s] returns a set containing all elements of [s], - plus [x]. If [x] was already in [s], [s] is returned unchanged. *) + (** [add x s] returns a set containing all elements of [s], + plus [x]. If [x] was already in [s], then [s] is returned unchanged. *) + val remove: elt -> t -> t (** [remove x s] returns a set containing all elements of [s], - except [x]. If [x] was not in [s], [s] is returned unchanged. *) + except [x]. If [x] was not in [s], then [s] is returned unchanged. *) + val union: t -> t -> t + (** Set union. *) + val inter: t -> t -> t + (** Set intersection. *) + val diff: t -> t -> t + (** Set difference. *) + val complement: t -> t - (** Union, intersection, difference and set complement. *) + (** Set complement. *) + val equal: t -> t -> bool - (** [equal s1 s2] tests whether the sets [s1] and [s2] are - equal, that is, contain equal elements. *) + (** [equal s1 s2] tests whether the sets [s1] and [s2] are + equal, that is, contain equal elements. *) + val subset: t -> t -> bool (** [subset s1 s2] tests whether the set [s1] is a subset of - the set [s2]. *) + the set [s2]. *) + val elements: t -> bool * elt list (** Gives a finite representation of the predicate: if the boolean is false, then the predicate is given in extension. if it is true, then the complement is given *) end -module Make(Ord: OrderedType): (S with type elt = Ord.t) - (** Functor building an implementation of the set structure - given a totally ordered type. *) +(** The [Make] functor constructs an implementation for any [OrderedType]. *) +module Make (Ord : OrderedType) : (S with type elt = Ord.t) -- cgit v1.2.3 From ca42472322013714050b98756aeaa222908fbe67 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 12:54:58 +0100 Subject: COMMENTS: updated in the "Option" module. --- lib/option.ml | 4 ++-- lib/option.mli | 16 ++++++++-------- 2 files changed, 10 insertions(+), 10 deletions(-) (limited to 'lib') diff --git a/lib/option.ml b/lib/option.ml index 9ea1a76982..2f6e8365bb 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 d9ad0e119f..4a8114177f 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 -- cgit v1.2.3 From 5174ee7e118d2bc57fc2d8a6619101735af79b16 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 12:55:40 +0100 Subject: COMMENTS: added to the "Unicode" module. --- lib/unicode.ml | 7 ++++++- lib/unicode.mli | 22 ++++++++++++++++------ 2 files changed, 22 insertions(+), 7 deletions(-) (limited to 'lib') diff --git a/lib/unicode.ml b/lib/unicode.ml index 1765e93dcd..05998bb804 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 098f6c919d..eb75f00c28 100644 --- a/lib/unicode.mli +++ b/lib/unicode.mli @@ -10,19 +10,29 @@ 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 -(** For extraction, turn a unicode string into an ascii-only one *) +(** 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. *) val ascii_of_ident : string -> string -- cgit v1.2.3 From 13f014ba37e0af547d57854df8926d633f9ccb7b Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 21 Dec 2015 17:51:38 +0100 Subject: Trust the directory cache in batch mode. When coqtop is a long-lived process (e.g. coqide), the user might be creating files on the fly. So we have to ask the operating system whether a file exists beforehand, so that we know whether the content of the directory cache is outdated. In batch mode, we can assume that the cache is always up-to-date, so we don't need to query the operating system before trusting the content of the cache. On a script doing "Require Import Reals", this brings down the number of stat syscalls from 42k to 2k. The number of syscalls could be further halved if all_subdirs was filling the directory cache. --- lib/system.ml | 26 ++++++++++++++------------ 1 file changed, 14 insertions(+), 12 deletions(-) (limited to 'lib') diff --git a/lib/system.ml b/lib/system.ml index b641aad91b..31e9861d3a 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -56,7 +56,7 @@ let check_unix_dir warn dir = 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 name.[0] <> '.' && ok_dirname name then + 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)) @@ -109,20 +109,22 @@ let make_dir_table dir = Array.fold_left filter_dotfiles StrSet.empty (Sys.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 @@ -132,7 +134,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 -- cgit v1.2.3 From fcf425a4714f0c888b3d670a9a37fe52a6e49bc5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Dec 2015 18:41:50 +0100 Subject: Attaching a dynamic argument to the toplevel type of generic arguments. --- lib/genarg.ml | 46 ++++++++++++++++++++++++++++++++++++++++++---- lib/genarg.mli | 20 ++++++++++++++++++-- 2 files changed, 60 insertions(+), 6 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index 8712eda8e1..b6a2849ad5 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -9,6 +9,8 @@ open Pp open Util +module Val = Dyn.Make(struct end) + type argument_type = (* Basic types *) | IntOrVarArgType @@ -133,13 +135,22 @@ let pair_unpack pack (t, obj) = match t with (** Creating args *) -let (arg0_map : Obj.t option String.Map.t ref) = ref String.Map.empty +type load = { + nil : Obj.t option; + dyn : Obj.t Val.tag; +} + +let (arg0_map : load String.Map.t ref) = ref String.Map.empty -let create_arg opt name = +let cast_tag : 'a Val.tag -> 'b Val.tag = Obj.magic + +let create_arg opt ?dyn name = if String.Map.mem name !arg0_map then Errors.anomaly (str "generic argument already declared: " ++ str name) else - let () = arg0_map := String.Map.add name (Obj.magic opt) !arg0_map in + let dyn = match dyn with None -> Val.create name | Some dyn -> cast_tag dyn in + let obj = { nil = Option.map Obj.repr opt; dyn; } in + let () = arg0_map := String.Map.add name obj !arg0_map in ExtraArgType name let make0 = create_arg @@ -153,12 +164,39 @@ let default_empty_value t = | Some v1, Some v2 -> Some (Obj.repr (v1, v2)) | _ -> None) | ExtraArgType s -> - String.Map.find s !arg0_map + (String.Map.find s !arg0_map).nil | _ -> None in match aux t with | Some v -> Some (Obj.obj v) | None -> None +(** Beware: keep in sync with the corresponding types *) +let int_or_var_T = Val.create "int_or_var" +let ident_T = Val.create "ident" +let var_T = Val.create "var" +let genarg_T = Val.create "genarg" +let constr_T = Val.create "constr" +let constr_may_eval_T = Val.create "constr_may_eval" +let open_constr_T = Val.create "open_constr" + +let option_val = Val.create "option" +let list_val = Val.create "list" +let pair_val = Val.create "pair" + +let val_tag = function +| IntOrVarArgType -> cast_tag int_or_var_T +| IdentArgType -> cast_tag ident_T +| VarArgType -> cast_tag var_T +| GenArgType -> cast_tag genarg_T +| ConstrArgType -> cast_tag constr_T +| ConstrMayEvalArgType -> cast_tag constr_may_eval_T +| OpenConstrArgType -> cast_tag open_constr_T +| ExtraArgType s -> Obj.magic (String.Map.find s !arg0_map).dyn +(** Recursive types have no associated dynamic tag *) +| ListArgType t -> assert false +| OptArgType t -> assert false +| PairArgType (t1, t2) -> assert false + (** Registering genarg-manipulating functions *) module type GenObj = diff --git a/lib/genarg.mli b/lib/genarg.mli index 2dcaa789f7..d52a246107 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -72,14 +72,20 @@ type ('raw, 'glob, 'top) genarg_type (** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized one, and ['top] the internalized one. *) +module Val : Dyn.S +(** 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 -> string -> ('raw, 'glob, 'top) genarg_type +val make0 : 'raw option -> ?dyn:'top Val.tag -> 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 : 'raw option -> ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type (** Alias for [make0]. *) (** {5 Specialized types} *) @@ -179,6 +185,16 @@ type ('r, 'l) pair_unpacker = val pair_unpack : ('r, 'l) pair_unpacker -> 'l generic_argument -> 'r +(** {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. *) + +val option_val : Val.t option Val.tag +val list_val : Val.t list Val.tag +val pair_val : (Val.t * Val.t) Val.tag + (** {6 Type reification} *) type argument_type = -- cgit v1.2.3 From b2beb9087628de23679a831e6273b91816f1ed27 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Dec 2015 19:24:17 +0100 Subject: Using dynamic values in tactic evaluation. --- lib/genarg.ml | 37 +++++++++++++++++++++++++++++++++++++ lib/genarg.mli | 5 +++++ 2 files changed, 42 insertions(+) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index b6a2849ad5..a43a798c46 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -197,6 +197,43 @@ let val_tag = function | OptArgType t -> assert false | PairArgType (t1, t2) -> assert false +exception CastError of argument_type * Val.t + +let prj : type a. a Val.tag -> Val.t -> a option = fun t v -> + let Val.Dyn (t', x) = v in + match Val.eq t t' with + | None -> None + | Some Refl -> Some x + +let try_prj wit v = match prj (val_tag wit) v with +| None -> raise (CastError (wit, v)) +| Some x -> x + +let rec val_cast : type a. a typed_abstract_argument_type -> Val.t -> a = +fun wit v -> match unquote wit with +| IntOrVarArgType | IdentArgType +| VarArgType | GenArgType +| ConstrArgType | ConstrMayEvalArgType +| OpenConstrArgType | ExtraArgType _ -> try_prj wit v +| ListArgType t -> + let v = match prj list_val v with + | None -> raise (CastError (wit, v)) + | Some v -> v + in + Obj.magic (List.map (fun x -> val_cast t x) v) +| OptArgType t -> + let v = match prj option_val v with + | None -> raise (CastError (wit, v)) + | Some v -> v + in + Obj.magic (Option.map (fun x -> val_cast t x) v) +| PairArgType (t1, t2) -> + let (v1, v2) = match prj pair_val v with + | None -> raise (CastError (wit, v)) + | Some v -> v + in + Obj.magic (val_cast t1 v1, val_cast t2 v2) + (** Registering genarg-manipulating functions *) module type GenObj = diff --git a/lib/genarg.mli b/lib/genarg.mli index d52a246107..c431aa619d 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -191,6 +191,8 @@ 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. *) +val val_cast : 'a typed_abstract_argument_type -> Val.t -> 'a + val option_val : Val.t option Val.tag val list_val : Val.t list Val.tag val pair_val : (Val.t * Val.t) Val.tag @@ -212,6 +214,9 @@ type argument_type = | PairArgType of argument_type * argument_type | ExtraArgType of string +exception CastError of argument_type * Val.t +(** Exception raised by {!val_cast} *) + val argument_type_eq : argument_type -> argument_type -> bool val pr_argument_type : argument_type -> Pp.std_ppcmds -- cgit v1.2.3 From 329b5b9ed526d572d7df066dc99486e1dcb9e4cc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 Dec 2015 17:18:06 +0100 Subject: Removing the now useless genarg generic argument. --- lib/genarg.ml | 6 +----- lib/genarg.mli | 1 - 2 files changed, 1 insertion(+), 6 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index a43a798c46..bf223f99e0 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -17,7 +17,6 @@ type argument_type = | IdentArgType | VarArgType (* Specific types *) - | GenArgType | ConstrArgType | ConstrMayEvalArgType | OpenConstrArgType @@ -30,7 +29,6 @@ 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 | OpenConstrArgType, OpenConstrArgType -> true @@ -45,7 +43,6 @@ 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" | OpenConstrArgType -> str "open_constr" @@ -187,7 +184,6 @@ let val_tag = function | IntOrVarArgType -> cast_tag int_or_var_T | IdentArgType -> cast_tag ident_T | VarArgType -> cast_tag var_T -| GenArgType -> cast_tag genarg_T | ConstrArgType -> cast_tag constr_T | ConstrMayEvalArgType -> cast_tag constr_may_eval_T | OpenConstrArgType -> cast_tag open_constr_T @@ -212,7 +208,7 @@ let try_prj wit v = match prj (val_tag wit) v with let rec val_cast : type a. a typed_abstract_argument_type -> Val.t -> a = fun wit v -> match unquote wit with | IntOrVarArgType | IdentArgType -| VarArgType | GenArgType +| VarArgType | ConstrArgType | ConstrMayEvalArgType | OpenConstrArgType | ExtraArgType _ -> try_prj wit v | ListArgType t -> diff --git a/lib/genarg.mli b/lib/genarg.mli index c431aa619d..89ea49ddb5 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -205,7 +205,6 @@ type argument_type = | IdentArgType | VarArgType (** Specific types *) - | GenArgType | ConstrArgType | ConstrMayEvalArgType | OpenConstrArgType -- cgit v1.2.3 From 9b02ddf179b375cb09966b70dd3b119eda0d92c1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 Dec 2015 17:51:53 +0100 Subject: Sharing toplevel representation for several generic types. - int and int_or_var - ident and var - constr and constr_may_eval --- lib/genarg.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index bf223f99e0..3989cf6df8 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -168,12 +168,10 @@ let default_empty_value t = | None -> None (** Beware: keep in sync with the corresponding types *) -let int_or_var_T = Val.create "int_or_var" +let int_or_var_T = Val.create "int" let ident_T = Val.create "ident" -let var_T = Val.create "var" let genarg_T = Val.create "genarg" let constr_T = Val.create "constr" -let constr_may_eval_T = Val.create "constr_may_eval" let open_constr_T = Val.create "open_constr" let option_val = Val.create "option" @@ -183,9 +181,11 @@ let pair_val = Val.create "pair" let val_tag = function | IntOrVarArgType -> cast_tag int_or_var_T | IdentArgType -> cast_tag ident_T -| VarArgType -> cast_tag var_T +| VarArgType -> cast_tag ident_T + (** Must ensure that toplevel types of Var and Ident agree! *) | ConstrArgType -> cast_tag constr_T -| ConstrMayEvalArgType -> cast_tag constr_may_eval_T +| ConstrMayEvalArgType -> cast_tag constr_T + (** Must ensure that toplevel types of Constr and ConstrMayEval agree! *) | OpenConstrArgType -> cast_tag open_constr_T | ExtraArgType s -> Obj.magic (String.Map.find s !arg0_map).dyn (** Recursive types have no associated dynamic tag *) -- cgit v1.2.3 From 5835804bd69a193b9ea29b6d4c8d0cc03530ccdd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 Dec 2015 18:04:14 +0100 Subject: Removing ad-hoc interpretation rules for tactic notations and their genarg. Now that types can share the same dynamic representation, we do not have to transtype the topelvel values dynamically and just take advantage of the standard interpretation function. --- lib/genarg.ml | 14 ++------------ lib/genarg.mli | 2 -- 2 files changed, 2 insertions(+), 14 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index 3989cf6df8..11a0421176 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -13,12 +13,10 @@ module Val = Dyn.Make(struct end) type argument_type = (* Basic types *) - | IntOrVarArgType | IdentArgType | VarArgType (* Specific types *) | ConstrArgType - | ConstrMayEvalArgType | OpenConstrArgType | ListArgType of argument_type | OptArgType of argument_type @@ -26,11 +24,9 @@ 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 | ConstrArgType, ConstrArgType -> true -| ConstrMayEvalArgType, ConstrMayEvalArgType -> true | OpenConstrArgType, OpenConstrArgType -> true | ListArgType arg1, ListArgType arg2 -> argument_type_eq arg1 arg2 | OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2 @@ -40,11 +36,9 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with | _ -> false let rec pr_argument_type = function -| IntOrVarArgType -> str "int_or_var" | IdentArgType -> str "ident" | VarArgType -> str "var" | ConstrArgType -> str "constr" -| ConstrMayEvalArgType -> str "constr_may_eval" | OpenConstrArgType -> str "open_constr" | ListArgType t -> pr_argument_type t ++ spc () ++ str "list" | OptArgType t -> pr_argument_type t ++ spc () ++ str "opt" @@ -168,7 +162,6 @@ let default_empty_value t = | None -> None (** Beware: keep in sync with the corresponding types *) -let int_or_var_T = Val.create "int" let ident_T = Val.create "ident" let genarg_T = Val.create "genarg" let constr_T = Val.create "constr" @@ -179,13 +172,10 @@ let list_val = Val.create "list" let pair_val = Val.create "pair" let val_tag = function -| IntOrVarArgType -> cast_tag int_or_var_T | IdentArgType -> cast_tag ident_T | VarArgType -> cast_tag ident_T (** Must ensure that toplevel types of Var and Ident agree! *) | ConstrArgType -> cast_tag constr_T -| ConstrMayEvalArgType -> cast_tag constr_T - (** Must ensure that toplevel types of Constr and ConstrMayEval agree! *) | OpenConstrArgType -> cast_tag open_constr_T | ExtraArgType s -> Obj.magic (String.Map.find s !arg0_map).dyn (** Recursive types have no associated dynamic tag *) @@ -207,9 +197,9 @@ let try_prj wit v = match prj (val_tag wit) v with let rec val_cast : type a. a typed_abstract_argument_type -> Val.t -> a = fun wit v -> match unquote wit with -| IntOrVarArgType | IdentArgType +| IdentArgType | VarArgType -| ConstrArgType | ConstrMayEvalArgType +| ConstrArgType | OpenConstrArgType | ExtraArgType _ -> try_prj wit v | ListArgType t -> let v = match prj list_val v with diff --git a/lib/genarg.mli b/lib/genarg.mli index 89ea49ddb5..83ba1dd04d 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -201,12 +201,10 @@ val pair_val : (Val.t * Val.t) Val.tag type argument_type = (** Basic types *) - | IntOrVarArgType | IdentArgType | VarArgType (** Specific types *) | ConstrArgType - | ConstrMayEvalArgType | OpenConstrArgType | ListArgType of argument_type | OptArgType of argument_type -- cgit v1.2.3 From 44ac395761d6b46866823b89addaea0ab45f4ebc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Dec 2015 00:38:00 +0100 Subject: Finer-grained types for toplevel values. --- lib/genarg.ml | 110 +++++++++++++++++++++++++++++++++++++++++---------------- lib/genarg.mli | 21 ++++++++--- 2 files changed, 95 insertions(+), 36 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index 11a0421176..2b8e0c9fdd 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -9,7 +9,51 @@ open Pp open Util -module Val = Dyn.Make(struct end) +module Dyn = Dyn.Make(struct end) + +module Val = +struct + + type 'a typ = 'a Dyn.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 -> Dyn.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 (Dyn.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 ")" + +end type argument_type = (* Basic types *) @@ -139,7 +183,7 @@ let create_arg opt ?dyn name = if String.Map.mem name !arg0_map then Errors.anomaly (str "generic argument already declared: " ++ str name) else - let dyn = match dyn with None -> Val.create name | Some dyn -> cast_tag dyn in + let dyn = match dyn with None -> Val.Base (Dyn.create name) | Some dyn -> cast_tag dyn in let obj = { nil = Option.map Obj.repr opt; dyn; } in let () = arg0_map := String.Map.add name obj !arg0_map in ExtraArgType name @@ -162,26 +206,22 @@ let default_empty_value t = | None -> None (** Beware: keep in sync with the corresponding types *) -let ident_T = Val.create "ident" -let genarg_T = Val.create "genarg" -let constr_T = Val.create "constr" -let open_constr_T = Val.create "open_constr" - -let option_val = Val.create "option" -let list_val = Val.create "list" -let pair_val = Val.create "pair" +let base_create n = Val.Base (Dyn.create n) +let ident_T = base_create "ident" +let genarg_T = base_create "genarg" +let constr_T = base_create "constr" +let open_constr_T = base_create "open_constr" -let val_tag = function +let rec val_tag = function | IdentArgType -> cast_tag ident_T | VarArgType -> cast_tag ident_T (** Must ensure that toplevel types of Var and Ident agree! *) | ConstrArgType -> cast_tag constr_T | OpenConstrArgType -> cast_tag open_constr_T -| ExtraArgType s -> Obj.magic (String.Map.find s !arg0_map).dyn -(** Recursive types have no associated dynamic tag *) -| ListArgType t -> assert false -| OptArgType t -> assert false -| PairArgType (t1, t2) -> assert false +| ExtraArgType s -> cast_tag (String.Map.find s !arg0_map).dyn +| ListArgType t -> cast_tag (Val.List (val_tag t)) +| OptArgType t -> cast_tag (Val.Opt (val_tag t)) +| PairArgType (t1, t2) -> cast_tag (Val.Pair (val_tag t1, val_tag t2)) exception CastError of argument_type * Val.t @@ -202,23 +242,31 @@ fun wit v -> match unquote wit with | ConstrArgType | OpenConstrArgType | ExtraArgType _ -> try_prj wit v | ListArgType t -> - let v = match prj list_val v with - | None -> raise (CastError (wit, v)) - | Some v -> v - in - Obj.magic (List.map (fun x -> val_cast t x) v) + let Val.Dyn (tag, v) = v in + begin match tag with + | Val.List tag -> + let map x = val_cast t (Val.Dyn (tag, x)) in + Obj.magic (List.map map v) + | _ -> raise (CastError (wit, Val.Dyn (tag, v))) + end | OptArgType t -> - let v = match prj option_val v with - | None -> raise (CastError (wit, v)) - | Some v -> v - in - Obj.magic (Option.map (fun x -> val_cast t x) v) + let Val.Dyn (tag, v) = v in + begin match tag with + | Val.Opt tag -> + let map x = val_cast t (Val.Dyn (tag, x)) in + Obj.magic (Option.map map v) + | _ -> raise (CastError (wit, Val.Dyn (tag, v))) + end | PairArgType (t1, t2) -> - let (v1, v2) = match prj pair_val v with - | None -> raise (CastError (wit, v)) - | Some v -> v - in - Obj.magic (val_cast t1 v1, val_cast t2 v2) + let Val.Dyn (tag, v) = v in + begin match tag with + | Val.Pair (tag1, tag2) -> + let (v1, v2) = v in + let v1 = Val.Dyn (tag1, v1) in + let v2 = Val.Dyn (tag2, v2) in + Obj.magic (val_cast t1 v1, val_cast t2 v2) + | _ -> raise (CastError (wit, Val.Dyn (tag, v))) + end (** Registering genarg-manipulating functions *) diff --git a/lib/genarg.mli b/lib/genarg.mli index 83ba1dd04d..0904960938 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -72,7 +72,22 @@ type ('raw, 'glob, 'top) genarg_type (** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized one, and ['top] the internalized one. *) -module Val : Dyn.S +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 @@ -193,10 +208,6 @@ val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag val val_cast : 'a typed_abstract_argument_type -> Val.t -> 'a -val option_val : Val.t option Val.tag -val list_val : Val.t list Val.tag -val pair_val : (Val.t * Val.t) Val.tag - (** {6 Type reification} *) type argument_type = -- cgit v1.2.3 From cb2f6a95ee72edb956f419a24f8385c8ae7f96f4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 28 Dec 2015 02:08:42 +0100 Subject: Removing the special status of open_constr generic argument. We also intepret it at toplevel as a true constr and push the resulting evarmap in the current state. --- lib/genarg.ml | 7 +------ lib/genarg.mli | 1 - 2 files changed, 1 insertion(+), 7 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index 2b8e0c9fdd..6108c15555 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -61,7 +61,6 @@ type argument_type = | VarArgType (* Specific types *) | ConstrArgType - | OpenConstrArgType | ListArgType of argument_type | OptArgType of argument_type | PairArgType of argument_type * argument_type @@ -71,7 +70,6 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with | IdentArgType, IdentArgType -> true | VarArgType, VarArgType -> true | ConstrArgType, ConstrArgType -> true -| OpenConstrArgType, OpenConstrArgType -> 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) -> @@ -83,7 +81,6 @@ let rec pr_argument_type = function | IdentArgType -> str "ident" | VarArgType -> str "var" | ConstrArgType -> str "constr" -| OpenConstrArgType -> str "open_constr" | ListArgType t -> pr_argument_type t ++ spc () ++ str "list" | OptArgType t -> pr_argument_type t ++ spc () ++ str "opt" | PairArgType (t1, t2) -> @@ -210,14 +207,12 @@ let base_create n = Val.Base (Dyn.create n) let ident_T = base_create "ident" let genarg_T = base_create "genarg" let constr_T = base_create "constr" -let open_constr_T = base_create "open_constr" let rec val_tag = function | IdentArgType -> cast_tag ident_T | VarArgType -> cast_tag ident_T (** Must ensure that toplevel types of Var and Ident agree! *) | ConstrArgType -> cast_tag constr_T -| OpenConstrArgType -> cast_tag open_constr_T | ExtraArgType s -> cast_tag (String.Map.find s !arg0_map).dyn | ListArgType t -> cast_tag (Val.List (val_tag t)) | OptArgType t -> cast_tag (Val.Opt (val_tag t)) @@ -240,7 +235,7 @@ fun wit v -> match unquote wit with | IdentArgType | VarArgType | ConstrArgType -| OpenConstrArgType | ExtraArgType _ -> try_prj wit v +| ExtraArgType _ -> try_prj wit v | ListArgType t -> let Val.Dyn (tag, v) = v in begin match tag with diff --git a/lib/genarg.mli b/lib/genarg.mli index 0904960938..674ee97ae8 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -216,7 +216,6 @@ type argument_type = | VarArgType (** Specific types *) | ConstrArgType - | OpenConstrArgType | ListArgType of argument_type | OptArgType of argument_type | PairArgType of argument_type * argument_type -- cgit v1.2.3 From d3bc575c498ae09ad1003405d17a9d5cfbcf3cbf Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 31 Dec 2015 17:00:42 +0100 Subject: Do not dump a glob reference when its location is ghost. (Fix bug #4469) This patch also causes the code to finish a bit faster in the NoGlob case by not preparing a string for dump_string. It also optimizes Dumpglob.is_ghost by only checking whether the end position is zero. Note that no ghost locations were part of the glob files of the standard library before the patch. Note also that the html documentation of the standard library is bitwise identical before and after the patch. --- lib/loc.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/loc.ml b/lib/loc.ml index b62677d484..9043bee075 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -31,7 +31,7 @@ let ghost = { fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; bp = 0; ep = 0; } -let is_ghost loc = Pervasives.(=) loc ghost (** FIXME *) +let is_ghost loc = loc.ep = 0 let merge loc1 loc2 = if loc1.bp < loc2.bp then -- cgit v1.2.3 From 1a157442dff4bfa127af467c49280e79889acde7 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 26 Dec 2015 10:07:19 +0100 Subject: Do not compose List.length with List.filter. --- lib/cList.ml | 7 +++++++ lib/cList.mli | 2 ++ 2 files changed, 9 insertions(+) (limited to 'lib') diff --git a/lib/cList.ml b/lib/cList.ml index 0ac372d8d8..72f892a09d 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -48,6 +48,7 @@ sig val filteri : (int -> 'a -> bool) -> 'a list -> 'a list val smartfilter : ('a -> bool) -> '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 +376,12 @@ let rec smartfilter f l = match l with else h :: tl' else tl' +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) diff --git a/lib/cList.mli b/lib/cList.mli index 19eeb2509a..1487f67a37 100644 --- a/lib/cList.mli +++ b/lib/cList.mli @@ -94,6 +94,8 @@ sig (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i [f ai = true], then [smartfilter f l == 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). *) -- cgit v1.2.3 From c671a5cb30db29feda56f008d45789c2fd4928e9 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 1 Jan 2016 23:33:40 +0100 Subject: Do not make it harder on the compiler optimizer by packing arguments. --- lib/cList.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'lib') diff --git a/lib/cList.ml b/lib/cList.ml index 72f892a09d..bd3e09b5b2 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -645,12 +645,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" -- cgit v1.2.3 From 53d109a21d97d073bc6a1f36a6c39b940a55eb69 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 1 Jan 2016 23:42:47 +0100 Subject: Remove unused hashconsing code. --- lib/hashcons.ml | 29 ----------------------------- 1 file changed, 29 deletions(-) (limited to 'lib') diff --git a/lib/hashcons.ml b/lib/hashcons.ml index 46ba0b6285..d927519181 100644 --- a/lib/hashcons.ml +++ b/lib/hashcons.ml @@ -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 equal = 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) -- cgit v1.2.3 From d5b1807e65f7ea29d435c3f894aa551370c5989f Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 1 Jan 2016 23:47:59 +0100 Subject: Fix typos. --- lib/hashcons.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/hashcons.ml b/lib/hashcons.ml index d927519181..eeaaf2f7fc 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. *) -- cgit v1.2.3 From 82ac0604888679bc2fbdeda9ac264d7cd10f7928 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 16:52:33 +0100 Subject: Avoid warnings about loop indices. --- lib/hashset.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/hashset.ml b/lib/hashset.ml index 1ca6cc6418..0009ac6506 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 -- cgit v1.2.3 From 3049b2930ec2bd4adf886fc90bf01a478b318477 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:01:28 +0100 Subject: Remove some useless module opening. --- lib/hMap.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'lib') diff --git a/lib/hMap.ml b/lib/hMap.ml index 8e900cd581..b5fc523150 100644 --- a/lib/hMap.ml +++ b/lib/hMap.ml @@ -333,7 +333,6 @@ struct struct module IntM = Int.Map.Monad(M) module ExtM = Map.Monad(M) - open M let fold f s accu = let ff _ m accu = ExtM.fold f m accu in -- cgit v1.2.3 From 80bbdf335be5657f5ab33b4aa02e21420d341de2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:11:03 +0100 Subject: Remove some unused functions. Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. --- lib/heap.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'lib') diff --git a/lib/heap.ml b/lib/heap.ml index a19bc0d1c3..5682b87bb6 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) -- cgit v1.2.3 From e4a682e2f2c91fac47f55cd8619af2321b2e4c30 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 8 Dec 2015 12:49:01 +0100 Subject: COMMENTS: Predicate In the original version, ocamldoc markup wasn't used properly thus ocamldoc output did not in all places make sense. This commit makes sure that the documentation of the Predicate module is as clear as the documentation of the Set module (in the standard library). --- lib/predicate.ml | 9 +++--- lib/predicate.mli | 85 +++++++++++++++++++++++++++++++++---------------------- 2 files changed, 56 insertions(+), 38 deletions(-) (limited to 'lib') diff --git a/lib/predicate.ml b/lib/predicate.ml index a60b3dadd4..1aa7db6af1 100644 --- a/lib/predicate.ml +++ b/lib/predicate.ml @@ -10,8 +10,6 @@ (* *) (************************************************************************) -(* Sets over ordered types *) - module type OrderedType = sig type t @@ -43,9 +41,10 @@ module Make(Ord: OrderedType) = struct module EltSet = Set.Make(Ord) - (* when bool is false, the denoted set is the complement of - the given set *) type elt = Ord.t + + (* (false, s) represents a set which is equal to the set s + (true, s) represents a set which is equal to the complement of set s *) type t = bool * EltSet.t let elements (b,s) = (b, EltSet.elements s) @@ -84,6 +83,7 @@ module Make(Ord: OrderedType) = let diff s1 s2 = inter s1 (complement s2) + (* assumes the set is infinite *) let subset s1 s2 = match (s1,s2) with ((false,p1),(false,p2)) -> EltSet.subset p1 p2 @@ -91,6 +91,7 @@ module Make(Ord: OrderedType) = | ((false,p1),(true,n2)) -> EltSet.is_empty (EltSet.inter p1 n2) | ((true,_),(false,_)) -> false + (* assumes the set is infinite *) let equal (b1,s1) (b2,s2) = b1=b2 && EltSet.equal s1 s2 diff --git a/lib/predicate.mli b/lib/predicate.mli index bcc89e7275..cee3b0bd39 100644 --- a/lib/predicate.mli +++ b/lib/predicate.mli @@ -1,67 +1,84 @@ +(** Infinite sets over a chosen [OrderedType]. -(** Module [Pred]: sets over infinite ordered types with complement. *) - -(** This module implements the set data structure, given a total ordering - function over the set elements. All operations over sets - are purely applicative (no side-effects). - The implementation uses the Set library. *) + All operations over sets are purely applicative (no side-effects). + *) +(** Input signature of the functor [Make]. *) module type OrderedType = sig type t - val compare: t -> t -> int + (** The type of the elements in the set. + + The chosen [t] {b must be infinite}. *) + + val compare : t -> t -> int + (** A total ordering function over the set elements. + This is a two-argument function [f] such that: + - [f e1 e2] is zero if the elements [e1] and [e2] are equal, + - [f e1 e2] is strictly negative if [e1] is smaller than [e2], + - and [f e1 e2] is strictly positive if [e1] is greater than [e2]. + *) end - (** The input signature of the functor [Pred.Make]. - [t] is the type of the set elements. - [compare] is a total ordering function over the set elements. - This is a two-argument function [f] such that - [f e1 e2] is zero if the elements [e1] and [e2] are equal, - [f e1 e2] is strictly negative if [e1] is smaller than [e2], - and [f e1 e2] is strictly positive if [e1] is greater than [e2]. - Example: a suitable ordering function is - the generic structural comparison function [compare]. *) module type S = sig type elt - (** The type of the set elements. *) + (** The type of the elements in the set. *) + type t - (** The type of sets. *) + (** The type of sets. *) + val empty: t - (** The empty set. *) + (** The empty set. *) + val full: t - (** The whole type. *) + (** The set of all elements (of type [elm]). *) + val is_empty: t -> bool - (** Test whether a set is empty or not. *) + (** Test whether a set is empty or not. *) + val is_full: t -> bool - (** Test whether a set contains the whole type or not. *) + (** Test whether a set contains the whole type or not. *) + val mem: elt -> t -> bool - (** [mem x s] tests whether [x] belongs to the set [s]. *) + (** [mem x s] tests whether [x] belongs to the set [s]. *) + val singleton: elt -> t - (** [singleton x] returns the one-element set containing only [x]. *) + (** [singleton x] returns the one-element set containing only [x]. *) + val add: elt -> t -> t - (** [add x s] returns a set containing all elements of [s], - plus [x]. If [x] was already in [s], [s] is returned unchanged. *) + (** [add x s] returns a set containing all elements of [s], + plus [x]. If [x] was already in [s], then [s] is returned unchanged. *) + val remove: elt -> t -> t (** [remove x s] returns a set containing all elements of [s], - except [x]. If [x] was not in [s], [s] is returned unchanged. *) + except [x]. If [x] was not in [s], then [s] is returned unchanged. *) + val union: t -> t -> t + (** Set union. *) + val inter: t -> t -> t + (** Set intersection. *) + val diff: t -> t -> t + (** Set difference. *) + val complement: t -> t - (** Union, intersection, difference and set complement. *) + (** Set complement. *) + val equal: t -> t -> bool - (** [equal s1 s2] tests whether the sets [s1] and [s2] are - equal, that is, contain equal elements. *) + (** [equal s1 s2] tests whether the sets [s1] and [s2] are + equal, that is, contain equal elements. *) + val subset: t -> t -> bool (** [subset s1 s2] tests whether the set [s1] is a subset of - the set [s2]. *) + the set [s2]. *) + val elements: t -> bool * elt list (** Gives a finite representation of the predicate: if the boolean is false, then the predicate is given in extension. if it is true, then the complement is given *) end -module Make(Ord: OrderedType): (S with type elt = Ord.t) - (** Functor building an implementation of the set structure - given a totally ordered type. *) +(** The [Make] functor constructs an implementation for any [OrderedType]. *) +module Make (Ord : OrderedType) : (S with type elt = Ord.t) -- cgit v1.2.3 From 8a9445fbf65d4ddf2c96348025d487b4d54a5d01 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 5 Jan 2016 19:36:02 +0100 Subject: Fix order of files in mllib. CString was linked after Serialize, although the later was using CString.equal. This had not been noticed so far because OCaml was ignoring functions marked as external in interfaces (which is the case of CString.equal) when considering link dependencies. This was changed on the OCaml side as part of the fix of PR#6956, so linking was now failing in several places. --- lib/clib.mllib | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/clib.mllib b/lib/clib.mllib index 7ff1d29359..9c9607abdb 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -18,11 +18,11 @@ Pp_control Flags Control Loc +CList +CString Serialize Deque CObj -CList -CString CArray CStack Util -- cgit v1.2.3 From 23cbf43f353c50fa72b72d694611c5c14367cea2 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 6 Jan 2016 00:58:42 +0100 Subject: Protect code against changes in Map interface. The Map interface of upcoming OCaml 4.03 includes a new union operator. In order to make our homemade implementation of Maps compatible with OCaml versions from 3.12 to 4.03, we define our own signatures for Maps. --- lib/cMap.ml | 2 +- lib/cMap.mli | 2 +- lib/cSig.mli | 31 +++++++++++++++++++++++++++++++ 3 files changed, 33 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/cMap.ml b/lib/cMap.ml index cf590d96c3..048a690812 100644 --- a/lib/cMap.ml +++ b/lib/cMap.ml @@ -16,7 +16,7 @@ module type S = Map.S module type ExtS = sig - include Map.S + include CSig.MapS module Set : CSig.SetS with type elt = key val update : key -> 'a -> 'a t -> 'a t val modify : key -> (key -> 'a -> 'a) -> 'a t -> 'a t diff --git a/lib/cMap.mli b/lib/cMap.mli index 23d3801e08..9d0fbbad24 100644 --- a/lib/cMap.mli +++ b/lib/cMap.mli @@ -18,7 +18,7 @@ module type S = Map.S module type ExtS = sig - include Map.S + include CSig.MapS (** The underlying Map library *) module Set : CSig.SetS with type elt = key diff --git a/lib/cSig.mli b/lib/cSig.mli index 2a8bda2936..e095c82cb0 100644 --- a/lib/cSig.mli +++ b/lib/cSig.mli @@ -45,3 +45,34 @@ sig end (** Redeclaration of OCaml set signature, to preserve compatibility. See OCaml documentation for more information. *) + +module type MapS = +sig + type key + type (+'a) t + val empty: 'a t + val is_empty: 'a t -> bool + val mem: key -> 'a t -> bool + val add: key -> 'a -> 'a t -> 'a t + val singleton: key -> 'a -> 'a t + val remove: key -> 'a t -> 'a t + val merge: + (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t + val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int + val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool + val iter: (key -> 'a -> unit) -> 'a t -> unit + val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b + val for_all: (key -> 'a -> bool) -> 'a t -> bool + val exists: (key -> 'a -> bool) -> 'a t -> bool + val filter: (key -> 'a -> bool) -> 'a t -> 'a t + val partition: (key -> 'a -> bool) -> 'a t -> 'a t * 'a t + val cardinal: 'a t -> int + val bindings: 'a t -> (key * 'a) list + val min_binding: 'a t -> (key * 'a) + val max_binding: 'a t -> (key * 'a) + val choose: 'a t -> (key * 'a) + val split: key -> 'a t -> 'a t * 'a option * 'a t + val find: key -> 'a t -> 'a + val map: ('a -> 'b) -> 'a t -> 'b t + val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t +end -- cgit v1.2.3 From 67b9b34d409c793dc449104525684852353ee064 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 Jan 2016 21:40:23 +0100 Subject: Removing ident and var generic arguments. --- lib/genarg.ml | 12 ------------ lib/genarg.mli | 4 +--- 2 files changed, 1 insertion(+), 15 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index 6108c15555..af9ea70ec5 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -56,9 +56,6 @@ struct end type argument_type = - (* Basic types *) - | IdentArgType - | VarArgType (* Specific types *) | ConstrArgType | ListArgType of argument_type @@ -67,8 +64,6 @@ type argument_type = | ExtraArgType of string let rec argument_type_eq arg1 arg2 = match arg1, arg2 with -| IdentArgType, IdentArgType -> true -| VarArgType, VarArgType -> true | ConstrArgType, ConstrArgType -> true | ListArgType arg1, ListArgType arg2 -> argument_type_eq arg1 arg2 | OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2 @@ -78,8 +73,6 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with | _ -> false let rec pr_argument_type = function -| IdentArgType -> str "ident" -| VarArgType -> str "var" | ConstrArgType -> str "constr" | ListArgType t -> pr_argument_type t ++ spc () ++ str "list" | OptArgType t -> pr_argument_type t ++ spc () ++ str "opt" @@ -204,13 +197,10 @@ let default_empty_value t = (** Beware: keep in sync with the corresponding types *) let base_create n = Val.Base (Dyn.create n) -let ident_T = base_create "ident" let genarg_T = base_create "genarg" let constr_T = base_create "constr" let rec val_tag = function -| IdentArgType -> cast_tag ident_T -| VarArgType -> cast_tag ident_T (** Must ensure that toplevel types of Var and Ident agree! *) | ConstrArgType -> cast_tag constr_T | ExtraArgType s -> cast_tag (String.Map.find s !arg0_map).dyn @@ -232,8 +222,6 @@ let try_prj wit v = match prj (val_tag wit) v with let rec val_cast : type a. a typed_abstract_argument_type -> Val.t -> a = fun wit v -> match unquote wit with -| IdentArgType -| VarArgType | ConstrArgType | ExtraArgType _ -> try_prj wit v | ListArgType t -> diff --git a/lib/genarg.mli b/lib/genarg.mli index 674ee97ae8..8d929f9f69 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -212,10 +212,8 @@ val val_cast : 'a typed_abstract_argument_type -> Val.t -> 'a type argument_type = (** Basic types *) - | IdentArgType - | VarArgType - (** Specific types *) | ConstrArgType + (** Specific types *) | ListArgType of argument_type | OptArgType of argument_type | PairArgType of argument_type * argument_type -- cgit v1.2.3 From 448866f0ec5291d58677d8fccbefde493ade0ee2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 Jan 2016 22:20:16 +0100 Subject: Removing constr generic argument. --- lib/genarg.ml | 13 +------------ lib/genarg.mli | 2 -- 2 files changed, 1 insertion(+), 14 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index af9ea70ec5..c2c1014f17 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -57,14 +57,12 @@ end type argument_type = (* Specific types *) - | ConstrArgType | 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 -| ConstrArgType, ConstrArgType -> 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) -> @@ -73,7 +71,6 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with | _ -> false let rec pr_argument_type = function -| ConstrArgType -> str "constr" | ListArgType t -> pr_argument_type t ++ spc () ++ str "list" | OptArgType t -> pr_argument_type t ++ spc () ++ str "opt" | PairArgType (t1, t2) -> @@ -190,19 +187,12 @@ let default_empty_value t = | _ -> None) | ExtraArgType s -> (String.Map.find s !arg0_map).nil - | _ -> None in + in match aux t with | Some v -> Some (Obj.obj v) | None -> None -(** Beware: keep in sync with the corresponding types *) -let base_create n = Val.Base (Dyn.create n) -let genarg_T = base_create "genarg" -let constr_T = base_create "constr" - let rec val_tag = function - (** Must ensure that toplevel types of Var and Ident agree! *) -| ConstrArgType -> cast_tag constr_T | ExtraArgType s -> cast_tag (String.Map.find s !arg0_map).dyn | ListArgType t -> cast_tag (Val.List (val_tag t)) | OptArgType t -> cast_tag (Val.Opt (val_tag t)) @@ -222,7 +212,6 @@ let try_prj wit v = match prj (val_tag wit) v with let rec val_cast : type a. a typed_abstract_argument_type -> Val.t -> a = fun wit v -> match unquote wit with -| ConstrArgType | ExtraArgType _ -> try_prj wit v | ListArgType t -> let Val.Dyn (tag, v) = v in diff --git a/lib/genarg.mli b/lib/genarg.mli index 8d929f9f69..56c09f14fc 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -211,8 +211,6 @@ val val_cast : 'a typed_abstract_argument_type -> Val.t -> 'a (** {6 Type reification} *) type argument_type = - (** Basic types *) - | ConstrArgType (** Specific types *) | ListArgType of argument_type | OptArgType of argument_type -- cgit v1.2.3 From 74a5cfa8b2f1a881ebf010160421cf0775c2a084 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 15 Jan 2016 17:49:49 +0100 Subject: Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen. --- lib/flags.ml | 2 ++ lib/flags.mli | 2 ++ 2 files changed, 4 insertions(+) (limited to 'lib') diff --git a/lib/flags.ml b/lib/flags.ml index ab4ac03f80..bdae0adc9a 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -83,6 +83,8 @@ let profile = false let print_emacs = ref false let coqtop_ui = ref false +let xml_export = ref false + let ide_slave = ref false let ideslave_coqtop_flags = ref None diff --git a/lib/flags.mli b/lib/flags.mli index 8e37136560..be2682cbd9 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -44,6 +44,8 @@ val profile : bool val print_emacs : bool ref val coqtop_ui : bool ref +val xml_export : bool ref + val ide_slave : bool ref val ideslave_coqtop_flags : string option ref -- cgit v1.2.3 From 0d1345ea2423fc418a470786b0b33b80df3a67bc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 17 Jan 2016 01:08:21 +0100 Subject: Temporary commit getting rid of Obj.magic unsafety for Genarg. This will allow an easier landing of the rewriting of Genarg. --- lib/genarg.ml | 3 +++ lib/genarg.mli | 3 +++ 2 files changed, 6 insertions(+) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index c2c1014f17..5efb074440 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -117,6 +117,9 @@ 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 +let arg_list wit = ListArgType wit +let arg_opt wit = OptArgType wit + type ('a, 'b, 'c, 'l) cast = Obj.t let raw = Obj.obj diff --git a/lib/genarg.mli b/lib/genarg.mli index 56c09f14fc..8099c062ab 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -265,6 +265,9 @@ val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) gena val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type -> ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type +val arg_list : ('a, 'l) abstract_argument_type -> ('a list, 'l) abstract_argument_type +val arg_opt : ('a, 'l) abstract_argument_type -> ('a option, 'l) abstract_argument_type + (** {5 Magic used by the parser} *) val default_empty_value : ('raw, 'glb, 'top) genarg_type -> 'raw option -- cgit v1.2.3 From 32a18b19f99c82dea5358bdebeb19862d30c4973 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 Jan 2016 22:39:23 +0100 Subject: Adding a structure indexed by tags. --- lib/dyn.ml | 56 +++++++++++++++++++++++++++++++++++++++++++++++++++++++- lib/dyn.mli | 29 +++++++++++++++++++++++++++++ 2 files changed, 84 insertions(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/dyn.ml b/lib/dyn.ml index 826cfaf8db..660ffc44ec 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -6,6 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +module type TParam = +sig + type 'a t +end + module type S = sig type 'a tag @@ -14,6 +19,30 @@ 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 @@ -25,6 +54,8 @@ 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 hash. We ensure unicity of the hash in the [create] function. If ever a @@ -51,6 +82,29 @@ let repr s = let () = Printf.eprintf "Unknown dynamic tag %i\n%!" s in assert false +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 -end \ No newline at end of file +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 diff --git a/lib/dyn.mli b/lib/dyn.mli index 28587859e1..d39acdf5d7 100644 --- a/lib/dyn.mli +++ b/lib/dyn.mli @@ -7,6 +7,10 @@ (************************************************************************) (** Dynamics. Use with extreme care. Not for kids. *) +module type TParam = +sig + type 'a t +end module type S = sig @@ -16,7 +20,32 @@ 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 (** FIXME: use OCaml 4.02 generative functors when available *) -- cgit v1.2.3 From be7f6f003ff4318dbe962ec141060a9daf92a80d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 12 Jan 2016 10:31:48 +0100 Subject: Reimplementing Genarg safely. No more Obj.magic in Genarg. We leverage the expressivity of GADT coupled with dynamic tags to get rid of unsafety. For now the API did not change in order to port the legacy code more easily. --- lib/genarg.ml | 288 +++++++++++++++++++++++++++++++++++++++------------------- 1 file changed, 196 insertions(+), 92 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index 5efb074440..030797da9c 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -9,12 +9,13 @@ open Pp open Util -module Dyn = Dyn.Make(struct end) +module ValT = Dyn.Make(struct end) +module ArgT = Dyn.Make(struct end) module Val = struct - type 'a typ = 'a Dyn.tag + type 'a typ = 'a ValT.tag type _ tag = | Base : 'a typ -> 'a tag @@ -26,7 +27,7 @@ struct 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 -> Dyn.eq t1 t2 + | Base t1, Base t2 -> ValT.eq t1 t2 | List t1, List t2 -> begin match eq t1 t2 with | None -> None @@ -48,7 +49,7 @@ struct | _ -> None let rec repr : type a. a tag -> std_ppcmds = function - | Base t -> str (Dyn.repr t) + | 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 ")" @@ -78,58 +79,147 @@ let rec pr_argument_type = function str "*" ++ spc () ++ pr_argument_type t2 ++ str ")" | ExtraArgType s -> str s -type ('raw, 'glob, 'top) genarg_type = argument_type +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 + +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 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 _ 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 +| 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 rawwit t = Rawwit t +let glbwit t = Glbwit t +let topwit t = Topwit t -let wit_list t = ListArgType t +let wit_list t = ListArg t -let wit_opt t = OptArgType t +let wit_opt t = OptArg t -let wit_pair t1 t2 = PairArgType (t1,t2) +let wit_pair t1 t2 = PairArg (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 in_gen t o = GenArg (t, o) -let has_type (t, v) u = argument_type_eq t u +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 x = x +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 + +let genarg_tag (GenArg (t, _)) = unquote t -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 -let arg_list wit = ListArgType wit -let arg_opt wit = OptArgType wit +let arg_list : type l. (_, l) abstract_argument_type -> (_, l) abstract_argument_type = function +| Rawwit t -> Rawwit (ListArg t) +| Glbwit t -> Glbwit (ListArg t) +| Topwit t -> Topwit (ListArg t) -type ('a, 'b, 'c, 'l) cast = Obj.t +let arg_opt : type l. (_, l) abstract_argument_type -> (_, l) abstract_argument_type = function +| Rawwit t -> Rawwit (OptArg t) +| Glbwit t -> Glbwit (OptArg t) +| Topwit t -> Topwit (OptArg t) -let raw = Obj.obj -let glb = Obj.obj -let top = Obj.obj +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 ('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) +let unpack (type l) (pack : (_, l) unpacker) (GenArg (t, obj) : l generic_argument) = match t with +| Rawwit t -> pack.unpacker t (Rcast obj) +| Glbwit t -> pack.unpacker t (Gcast obj) +| Topwit t -> pack.unpacker t (Tcast obj) (** Type transformers *) @@ -137,16 +227,20 @@ 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) +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 pack (t, obj) = match t with -| OptArgType t -> pack.opt_unpacker t (Obj.obj obj) +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 = @@ -154,52 +248,60 @@ type ('r, 'l) pair_unpacker = ('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) +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 *) -type load = { - nil : Obj.t option; - dyn : Obj.t Val.tag; +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 + +type ('raw, 'glb, 'top) load = { + nil : 'raw option; + dyn : 'top Val.tag; } -let (arg0_map : load String.Map.t ref) = ref String.Map.empty +module LoadMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) load end) -let cast_tag : 'a Val.tag -> 'b Val.tag = Obj.magic +let arg0_map = ref LoadMap.empty let create_arg opt ?dyn name = - if String.Map.mem name !arg0_map then + match ArgT.name name with + | Some _ -> Errors.anomaly (str "generic argument already declared: " ++ str name) - else - let dyn = match dyn with None -> Val.Base (Dyn.create name) | Some dyn -> cast_tag dyn in - let obj = { nil = Option.map Obj.repr opt; dyn; } in - let () = arg0_map := String.Map.add name obj !arg0_map in - ExtraArgType 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 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).nil - in - match aux t with - | Some v -> Some (Obj.obj v) - | None -> None +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 = function -| ExtraArgType s -> cast_tag (String.Map.find s !arg0_map).dyn -| ListArgType t -> cast_tag (Val.List (val_tag t)) -| OptArgType t -> cast_tag (Val.Opt (val_tag t)) -| PairArgType (t1, t2) -> cast_tag (Val.Pair (val_tag t1, val_tag t2)) +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 exception CastError of argument_type * Val.t @@ -210,39 +312,42 @@ let prj : type a. a Val.tag -> Val.t -> a option = fun t v -> | Some Refl -> Some x let try_prj wit v = match prj (val_tag wit) v with -| None -> raise (CastError (wit, v)) +| None -> raise (CastError (untype wit, v)) | Some x -> x -let rec val_cast : type a. a typed_abstract_argument_type -> Val.t -> a = -fun wit v -> match unquote wit with -| ExtraArgType _ -> try_prj wit v -| ListArgType t -> +let rec val_cast : type a b c. (a, b, c) genarg_type -> Val.t -> c = +fun wit v -> match wit with +| ExtraArg _ -> try_prj wit v +| ListArg t -> let Val.Dyn (tag, v) = v in begin match tag with | Val.List tag -> let map x = val_cast t (Val.Dyn (tag, x)) in - Obj.magic (List.map map v) - | _ -> raise (CastError (wit, Val.Dyn (tag, v))) + List.map map v + | _ -> raise (CastError (untype wit, Val.Dyn (tag, v))) end -| OptArgType t -> +| OptArg t -> let Val.Dyn (tag, v) = v in begin match tag with | Val.Opt tag -> let map x = val_cast t (Val.Dyn (tag, x)) in - Obj.magic (Option.map map v) - | _ -> raise (CastError (wit, Val.Dyn (tag, v))) + Option.map map v + | _ -> raise (CastError (untype wit, Val.Dyn (tag, v))) end -| PairArgType (t1, t2) -> +| PairArg (t1, t2) -> let Val.Dyn (tag, v) = v in begin match tag with | Val.Pair (tag1, tag2) -> let (v1, v2) = v in let v1 = Val.Dyn (tag1, v1) in let v2 = Val.Dyn (tag2, v2) in - Obj.magic (val_cast t1 v1, val_cast t2 v2) - | _ -> raise (CastError (wit, Val.Dyn (tag, v))) + (val_cast t1 v1, val_cast t2 v2) + | _ -> raise (CastError (untype wit, Val.Dyn (tag, v))) end +let val_tag = function Topwit t -> val_tag t +let val_cast = function Topwit t -> val_cast t + (** Registering genarg-manipulating functions *) module type GenObj = @@ -254,30 +359,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 @@ -285,12 +391,10 @@ 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 -> +| 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" -- cgit v1.2.3 From 15747cc2aaaeeb5d59ec90cda940c1dc6de01a6a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 17 Jan 2016 01:34:58 +0100 Subject: Exporting Genarg implementation in the API. We can now use the expressivity of GADT to work around historical kludges of generic arguments. --- lib/genarg.mli | 38 ++++++++++++++++++++++++++++++++------ 1 file changed, 32 insertions(+), 6 deletions(-) (limited to 'lib') diff --git a/lib/genarg.mli b/lib/genarg.mli index 8099c062ab..38dc0c684a 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -68,7 +68,21 @@ ExtraArgType of string '_a '_b (** {5 Generic types} *) -type ('raw, 'glob, 'top) genarg_type +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 + 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. *) @@ -112,11 +126,14 @@ val create_arg : 'raw option -> ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'to 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 @@ -141,7 +158,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. *) @@ -220,7 +237,16 @@ type argument_type = exception CastError of argument_type * Val.t (** Exception raised by {!val_cast} *) +(** {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. *) -- cgit v1.2.3 From 88a16f49efd315aa1413da67f6d321a5fe269772 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 17 Jan 2016 01:46:02 +0100 Subject: Simplification and type-safety of Pcoq thanks to GADTs in Genarg. --- lib/genarg.ml | 10 ---------- lib/genarg.mli | 3 --- 2 files changed, 13 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index 030797da9c..6c10dee2ae 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -194,16 +194,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 -let arg_list : type l. (_, l) abstract_argument_type -> (_, l) abstract_argument_type = function -| Rawwit t -> Rawwit (ListArg t) -| Glbwit t -> Glbwit (ListArg t) -| Topwit t -> Topwit (ListArg t) - -let arg_opt : type l. (_, l) abstract_argument_type -> (_, l) abstract_argument_type = function -| Rawwit t -> Rawwit (OptArg t) -| Glbwit t -> Glbwit (OptArg t) -| Topwit t -> Topwit (OptArg t) - type ('a, 'b, 'c, 'l) cast = | Rcast : 'a -> ('a, 'b, 'c, rlevel) cast | Gcast : 'b -> ('a, 'b, 'c, glevel) cast diff --git a/lib/genarg.mli b/lib/genarg.mli index 38dc0c684a..a1b74c6744 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -291,9 +291,6 @@ val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) gena val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type -> ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type -val arg_list : ('a, 'l) abstract_argument_type -> ('a list, 'l) abstract_argument_type -val arg_opt : ('a, 'l) abstract_argument_type -> ('a option, 'l) abstract_argument_type - (** {5 Magic used by the parser} *) val default_empty_value : ('raw, 'glb, 'top) genarg_type -> 'raw option -- cgit v1.2.3 From d3ee6b2fbcd0fbb666af7f1920446e809e8d6e1e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 17 Jan 2016 01:58:05 +0100 Subject: Getting rid of the awkward unpack mechanism from Genarg. --- lib/genarg.ml | 8 -------- lib/genarg.mli | 38 -------------------------------------- 2 files changed, 46 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index 6c10dee2ae..58d83ce7ae 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -203,14 +203,6 @@ 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 ('r, 'l) unpacker = - { unpacker : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> ('a, 'b, 'c, 'l) cast -> 'r } - -let unpack (type l) (pack : (_, l) unpacker) (GenArg (t, obj) : l generic_argument) = match t with -| Rawwit t -> pack.unpacker t (Rcast obj) -| Glbwit t -> pack.unpacker t (Gcast obj) -| Topwit t -> pack.unpacker t (Tcast obj) - (** Type transformers *) type ('r, 'l) list_unpacker = diff --git a/lib/genarg.mli b/lib/genarg.mli index a1b74c6744..8d1a439827 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -179,44 +179,6 @@ 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 Dynamic toplevel values} *) val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag -- cgit v1.2.3 From 820a282fde5cb4233116ce2cda927fda2f36097d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 17 Jan 2016 02:56:14 +0100 Subject: Moving val_cast to Tacinterp. --- lib/genarg.ml | 43 ------------------------------------------- lib/genarg.mli | 5 ----- 2 files changed, 48 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index 58d83ce7ae..37b31a511b 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -285,50 +285,7 @@ let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function | ExtraArg s -> match LoadMap.find s !arg0_map with LoadMap.Pack obj -> obj.dyn -exception CastError of argument_type * Val.t - -let prj : type a. a Val.tag -> Val.t -> a option = fun t v -> - let Val.Dyn (t', x) = v in - match Val.eq t t' with - | None -> None - | Some Refl -> Some x - -let try_prj wit v = match prj (val_tag wit) v with -| None -> raise (CastError (untype wit, v)) -| Some x -> x - -let rec val_cast : type a b c. (a, b, c) genarg_type -> Val.t -> c = -fun wit v -> match wit with -| ExtraArg _ -> try_prj wit v -| ListArg t -> - let Val.Dyn (tag, v) = v in - begin match tag with - | Val.List tag -> - let map x = val_cast t (Val.Dyn (tag, x)) in - List.map map v - | _ -> raise (CastError (untype wit, Val.Dyn (tag, v))) - end -| OptArg t -> - let Val.Dyn (tag, v) = v in - begin match tag with - | Val.Opt tag -> - let map x = val_cast t (Val.Dyn (tag, x)) in - Option.map map v - | _ -> raise (CastError (untype wit, Val.Dyn (tag, v))) - end -| PairArg (t1, t2) -> - let Val.Dyn (tag, v) = v in - begin match tag with - | Val.Pair (tag1, tag2) -> - let (v1, v2) = v in - let v1 = Val.Dyn (tag1, v1) in - let v2 = Val.Dyn (tag2, v2) in - (val_cast t1 v1, val_cast t2 v2) - | _ -> raise (CastError (untype wit, Val.Dyn (tag, v))) - end - let val_tag = function Topwit t -> val_tag t -let val_cast = function Topwit t -> val_cast t (** Registering genarg-manipulating functions *) diff --git a/lib/genarg.mli b/lib/genarg.mli index 8d1a439827..024c7a456e 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -185,8 +185,6 @@ 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. *) -val val_cast : 'a typed_abstract_argument_type -> Val.t -> 'a - (** {6 Type reification} *) type argument_type = @@ -196,9 +194,6 @@ type argument_type = | PairArgType of argument_type * argument_type | ExtraArgType of string -exception CastError of argument_type * Val.t -(** Exception raised by {!val_cast} *) - (** {6 Equalities} *) val argument_type_eq : argument_type -> argument_type -> bool -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- lib/aux_file.ml | 2 +- lib/aux_file.mli | 2 +- lib/bigint.ml | 2 +- lib/bigint.mli | 2 +- lib/cMap.ml | 2 +- lib/cMap.mli | 2 +- lib/cSet.ml | 2 +- lib/cSet.mli | 2 +- lib/cString.ml | 2 +- lib/cString.mli | 2 +- lib/cThread.ml | 2 +- lib/cThread.mli | 2 +- lib/cUnix.ml | 2 +- lib/cUnix.mli | 2 +- lib/canary.ml | 2 +- lib/canary.mli | 2 +- lib/control.ml | 2 +- lib/control.mli | 2 +- lib/deque.ml | 2 +- lib/deque.mli | 2 +- lib/dyn.ml | 2 +- lib/dyn.mli | 2 +- lib/envars.ml | 2 +- lib/envars.mli | 2 +- lib/ephemeron.ml | 2 +- lib/ephemeron.mli | 2 +- lib/explore.ml | 2 +- lib/explore.mli | 2 +- lib/feedback.ml | 2 +- lib/feedback.mli | 2 +- lib/flags.ml | 2 +- lib/flags.mli | 2 +- lib/future.ml | 2 +- lib/future.mli | 2 +- lib/genarg.ml | 2 +- lib/genarg.mli | 2 +- lib/hMap.ml | 2 +- lib/hMap.mli | 2 +- lib/hashcons.ml | 2 +- lib/hashcons.mli | 2 +- lib/hashset.ml | 2 +- lib/hashset.mli | 2 +- lib/heap.ml | 2 +- lib/heap.mli | 2 +- lib/hook.ml | 2 +- lib/hook.mli | 2 +- lib/iStream.ml | 2 +- lib/iStream.mli | 2 +- lib/int.ml | 2 +- lib/int.mli | 2 +- lib/loc.ml | 2 +- lib/loc.mli | 2 +- lib/option.ml | 2 +- lib/option.mli | 2 +- lib/pp.ml | 2 +- lib/pp.mli | 2 +- lib/pp_control.ml | 2 +- lib/pp_control.mli | 2 +- lib/ppstyle.ml | 2 +- lib/ppstyle.mli | 2 +- lib/profile.ml | 2 +- lib/profile.mli | 2 +- lib/remoteCounter.ml | 2 +- lib/remoteCounter.mli | 2 +- lib/richpp.ml | 2 +- lib/richpp.mli | 2 +- lib/rtree.ml | 2 +- lib/rtree.mli | 2 +- lib/serialize.ml | 2 +- lib/serialize.mli | 2 +- lib/spawn.ml | 2 +- lib/spawn.mli | 2 +- lib/system.ml | 2 +- lib/system.mli | 2 +- lib/terminal.ml | 2 +- lib/terminal.mli | 2 +- lib/trie.ml | 2 +- lib/trie.mli | 2 +- lib/unicode.mli | 2 +- lib/unionfind.ml | 2 +- lib/unionfind.mli | 2 +- lib/util.mli | 2 +- lib/xml_datatype.mli | 2 +- lib/xml_printer.ml | 2 +- lib/xml_printer.mli | 2 +- 85 files changed, 85 insertions(+), 85 deletions(-) (limited to 'lib') diff --git a/lib/aux_file.ml b/lib/aux_file.ml index 5dedb0d0ac..f7bd81f85d 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* '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 @@ -376,6 +377,12 @@ 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 diff --git a/lib/cList.mli b/lib/cList.mli index 1487f67a37..9c7b815c15 100644 --- a/lib/cList.mli +++ b/lib/cList.mli @@ -94,6 +94,9 @@ 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 -- cgit v1.2.3 From f65f8d5a4d9ba437fa2d8af03e2781d841e53007 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 21 Jan 2016 09:21:23 +0100 Subject: Restore warnings produced by the interpretation of the command line (e.g. with deprecated options such as -byte, etc.) since I guess this is what we expect. Was probably lost in 81eb133d64ac81cb. --- lib/flags.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'lib') diff --git a/lib/flags.mli b/lib/flags.mli index ab06eda306..69caad5b62 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -90,6 +90,7 @@ val is_universe_polymorphism : unit -> bool val make_polymorphic_flag : bool -> unit val use_polymorphic_flag : unit -> bool +val warn : bool ref val make_warn : bool -> unit val if_warn : ('a -> unit) -> 'a -> unit -- cgit v1.2.3 From e9675e068f9e0e92bab05c030fb4722b146123b8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 3 Feb 2016 16:20:46 +0100 Subject: Adding a "get" primitive to map signature. It is similar to find but raises an assertion failure instead of a Not_found when the element is not encountered. Using it will give stronger invariants. --- lib/cMap.ml | 2 ++ lib/cMap.mli | 3 +++ lib/hMap.ml | 2 ++ 3 files changed, 7 insertions(+) (limited to 'lib') diff --git a/lib/cMap.ml b/lib/cMap.ml index d1a32b7aa5..4b058380c6 100644 --- a/lib/cMap.ml +++ b/lib/cMap.ml @@ -25,6 +25,7 @@ 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 @@ -207,4 +208,5 @@ 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 464dc503be..3ef7fa2c8a 100644 --- a/lib/cMap.mli +++ b/lib/cMap.mli @@ -31,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. *) diff --git a/lib/hMap.ml b/lib/hMap.ml index 220adc28f3..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 = -- cgit v1.2.3 From 5f29a92c0648afd4d9e46de79ab00d0c4b901ff0 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 9 Feb 2016 16:36:05 +0100 Subject: Don't fail fatally if PATH is not set. This fixes micromega in certain environments. --- lib/system.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'lib') diff --git a/lib/system.ml b/lib/system.ml index 9bdcecef19..0ad43a7423 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -149,10 +149,12 @@ let is_in_path lpath filename = with Not_found -> false let is_in_system_path filename = - let path = try Sys.getenv "PATH" - with Not_found -> error "system variable PATH not found" in - let lpath = CUnix.path_to_list path in - is_in_path lpath filename + try + let lpath = CUnix.path_to_list (Sys.getenv "PATH") in + is_in_path lpath filename + with Not_found -> + msg_warning (str "system variable PATH not found"); + false let open_trapping_failure name = try open_out_bin name -- cgit v1.2.3 From 06fa0334047a9400d0b5a144601fca35746a53b8 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 17 Feb 2016 10:32:40 +0100 Subject: CLEANUP: Renaming "Util.compose" function to "%" I propose to change the name of the "Util.compose" function to "%". Reasons: 1. If one wants to express function composition, then the new name enables us to achieve this goal easier. 2. In "Batteries Included" they had made the same choice. --- lib/util.ml | 8 +++++++- lib/util.mli | 10 +++++++++- 2 files changed, 16 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/util.ml b/lib/util.ml index b67539918d..0f79c10df1 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 diff --git a/lib/util.mli b/lib/util.mli index 7923c65a3b..559874bb83 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 -- cgit v1.2.3 From 508d5a99101097948b6de342295eec0d5c8cbe72 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 3 Mar 2016 18:59:51 +0100 Subject: Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop. Printing invalid UTF-8 string startled GTK too much, leading to CoqIDE dying improperly. We now check that all strings outputed by Coq are proper UTF-8. This is not perfect, as CoqIDE will sometimes truncate strings which contains the null character, but at least it should not crash. --- lib/unicode.ml | 7 +++++++ lib/unicode.mli | 3 +++ 2 files changed, 10 insertions(+) (limited to 'lib') diff --git a/lib/unicode.ml b/lib/unicode.ml index 1765e93dcd..cfaa73cc11 100644 --- a/lib/unicode.ml +++ b/lib/unicode.ml @@ -168,6 +168,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 = diff --git a/lib/unicode.mli b/lib/unicode.mli index 520203d435..65e75a20d6 100644 --- a/lib/unicode.mli +++ b/lib/unicode.mli @@ -26,3 +26,6 @@ val lowercase_first_char : string -> string (** For extraction, turn a unicode string into an ascii-only one *) val is_basic_ascii : string -> bool val ascii_of_ident : string -> string + +(** Validate an UTF-8 string *) +val is_utf8 : string -> bool -- cgit v1.2.3 From b98e4857a13a4014c65882af5321ebdb09f41890 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 4 Mar 2016 17:40:10 +0100 Subject: Rename Ephemeron -> CEphemeron. Fixes compilation of Coq with OCaml 4.03 beta 1. --- lib/cEphemeron.ml | 89 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/cEphemeron.mli | 52 +++++++++++++++++++++++++++++++ lib/ephemeron.ml | 89 ------------------------------------------------------ lib/ephemeron.mli | 52 ------------------------------- lib/future.ml | 8 ++--- lib/lib.mllib | 2 +- 6 files changed, 146 insertions(+), 146 deletions(-) create mode 100644 lib/cEphemeron.ml create mode 100644 lib/cEphemeron.mli delete mode 100644 lib/ephemeron.ml delete mode 100644 lib/ephemeron.mli (limited to 'lib') diff --git a/lib/cEphemeron.ml b/lib/cEphemeron.ml new file mode 100644 index 0000000000..a38ea11e10 --- /dev/null +++ b/lib/cEphemeron.ml @@ -0,0 +1,89 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* boxed_key = + (* TODO: take a random value here. Is there a random function in OCaml? *) + let bid = ref 0 in + (* According to OCaml Gc module documentation, Pervasives.ref is one of the + few ways of getting a boxed value the compiler will never alias. *) + fun () -> incr bid; Pervasives.ref (Pervasives.ref !bid) + +(* A phantom type to preserve type safety *) +type 'a key = boxed_key + +(* Comparing keys with == grants that if a key is unmarshalled (in the same + process where it was created or in another one) it is not mistaken for + an already existing one (unmarshal has no right to alias). If the initial + value of bid is taken at random, then one also avoids potential collisions *) +module HT = Hashtbl.Make(struct + type t = key_type ref + let equal k1 k2 = k1 == k2 + let hash id = !id +end) + +(* A key is the (unique) value inside a boxed key, hence it does not + keep its corresponding boxed key reachable (replacing key_type by boxed_key + would make the key always reachable) *) +let values : Obj.t HT.t = HT.create 1001 + +(* To avoid a race contidion between the finalization function and + get/create on the values hashtable, the finalization function just + enqueues in an imperative list the item to be collected. Being the list + imperative, even if the Gc enqueue an item while run_collection is operating, + the tail of the list is eventually set to Empty on completion. + Kudos to the authors of Why3 that came up with this solution for their + implementation of weak hash tables! *) +type imperative_list = cell ref +and cell = Empty | Item of key_type ref * imperative_list + +let collection_queue : imperative_list ref = ref (ref Empty) + +let enqueue x = collection_queue := ref (Item (!x, !collection_queue)) + +let run_collection () = + let rec aux l = match !l with + | Empty -> () + | Item (k, tl) -> HT.remove values k; aux tl in + let l = !collection_queue in + aux l; + l := Empty + +(* The only reference to the boxed key is the one returned, when the user drops + it the value eventually disappears from the values table above *) +let create (v : 'a) : 'a key = + run_collection (); + let k = mk_key () in + HT.add values !k (Obj.repr v); + Gc.finalise enqueue k; + k + +(* Avoid raising Not_found *) +exception InvalidKey +let get (k : 'a key) : 'a = + run_collection (); + try Obj.obj (HT.find values !k) + with Not_found -> raise InvalidKey + +(* Simple utils *) +let default k v = + try get k + with InvalidKey -> v + +let iter_opt k f = + match + try Some (get k) + with InvalidKey -> None + with + | None -> () + | Some v -> f v + +let clear () = run_collection () diff --git a/lib/cEphemeron.mli b/lib/cEphemeron.mli new file mode 100644 index 0000000000..1200e4e208 --- /dev/null +++ b/lib/cEphemeron.mli @@ -0,0 +1,52 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a key + +(* May raise InvalidKey *) +exception InvalidKey +val get : 'a key -> 'a + +(* These never fail. *) +val iter_opt : 'a key -> ('a -> unit) -> unit +val default : 'a key -> 'a -> 'a + +val clear : unit -> unit diff --git a/lib/ephemeron.ml b/lib/ephemeron.ml deleted file mode 100644 index a38ea11e10..0000000000 --- a/lib/ephemeron.ml +++ /dev/null @@ -1,89 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* boxed_key = - (* TODO: take a random value here. Is there a random function in OCaml? *) - let bid = ref 0 in - (* According to OCaml Gc module documentation, Pervasives.ref is one of the - few ways of getting a boxed value the compiler will never alias. *) - fun () -> incr bid; Pervasives.ref (Pervasives.ref !bid) - -(* A phantom type to preserve type safety *) -type 'a key = boxed_key - -(* Comparing keys with == grants that if a key is unmarshalled (in the same - process where it was created or in another one) it is not mistaken for - an already existing one (unmarshal has no right to alias). If the initial - value of bid is taken at random, then one also avoids potential collisions *) -module HT = Hashtbl.Make(struct - type t = key_type ref - let equal k1 k2 = k1 == k2 - let hash id = !id -end) - -(* A key is the (unique) value inside a boxed key, hence it does not - keep its corresponding boxed key reachable (replacing key_type by boxed_key - would make the key always reachable) *) -let values : Obj.t HT.t = HT.create 1001 - -(* To avoid a race contidion between the finalization function and - get/create on the values hashtable, the finalization function just - enqueues in an imperative list the item to be collected. Being the list - imperative, even if the Gc enqueue an item while run_collection is operating, - the tail of the list is eventually set to Empty on completion. - Kudos to the authors of Why3 that came up with this solution for their - implementation of weak hash tables! *) -type imperative_list = cell ref -and cell = Empty | Item of key_type ref * imperative_list - -let collection_queue : imperative_list ref = ref (ref Empty) - -let enqueue x = collection_queue := ref (Item (!x, !collection_queue)) - -let run_collection () = - let rec aux l = match !l with - | Empty -> () - | Item (k, tl) -> HT.remove values k; aux tl in - let l = !collection_queue in - aux l; - l := Empty - -(* The only reference to the boxed key is the one returned, when the user drops - it the value eventually disappears from the values table above *) -let create (v : 'a) : 'a key = - run_collection (); - let k = mk_key () in - HT.add values !k (Obj.repr v); - Gc.finalise enqueue k; - k - -(* Avoid raising Not_found *) -exception InvalidKey -let get (k : 'a key) : 'a = - run_collection (); - try Obj.obj (HT.find values !k) - with Not_found -> raise InvalidKey - -(* Simple utils *) -let default k v = - try get k - with InvalidKey -> v - -let iter_opt k f = - match - try Some (get k) - with InvalidKey -> None - with - | None -> () - | Some v -> f v - -let clear () = run_collection () diff --git a/lib/ephemeron.mli b/lib/ephemeron.mli deleted file mode 100644 index 1200e4e208..0000000000 --- a/lib/ephemeron.mli +++ /dev/null @@ -1,52 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a key - -(* May raise InvalidKey *) -exception InvalidKey -val get : 'a key -> 'a - -(* These never fail. *) -val iter_opt : 'a key -> ('a -> unit) -> unit -val default : 'a key -> 'a -> 'a - -val clear : unit -> unit diff --git a/lib/future.ml b/lib/future.ml index 5cd2beba91..e8f33db5e1 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -62,7 +62,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 @@ -70,13 +70,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/lib.mllib b/lib/lib.mllib index f3f6ad8fc7..6805ce4919 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -15,6 +15,6 @@ Rtree Heap Unionfind Genarg -Ephemeron +CEphemeron Future RemoteCounter -- cgit v1.2.3 From cebc677e01c64c4a3f7081f85e37f3b61a112b68 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 9 Mar 2016 16:23:33 +0100 Subject: Win: kill unreliable hence do not waitpid after kill -9 (Close #4369) This commit also completes 74bd95d10b9f4cccb4bd5b855786c444492b201b --- lib/spawn.ml | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) (limited to 'lib') diff --git a/lib/spawn.ml b/lib/spawn.ml index 4d35ded90f..fda4b4239a 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -220,10 +220,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 +270,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 -- cgit v1.2.3 From 10e3c8e59664ed5137cd650ba6e0704943c511e8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 10 Mar 2016 14:17:48 +0100 Subject: Removing OCaml deprecated function names from the Lazy module. --- lib/iStream.ml | 6 +++--- lib/pp.ml | 18 +++++++++--------- 2 files changed, 12 insertions(+), 12 deletions(-) (limited to 'lib') 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/pp.ml b/lib/pp.ml index 0260f98fa2..9a833ae225 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -261,7 +261,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 +290,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;*) -- cgit v1.2.3 From 0dfd0fb7d7c04eedfb3b161b9b5cfab103c17916 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 13 Mar 2016 17:48:28 +0100 Subject: Adding a few functions on type union. --- lib/util.ml | 33 ++++++++++++++++++++++++++++++--- lib/util.mli | 8 ++++++++ 2 files changed, 38 insertions(+), 3 deletions(-) (limited to 'lib') diff --git a/lib/util.ml b/lib/util.ml index 0f79c10df1..cae996e332 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -132,9 +132,36 @@ 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 + | _ -> a +end + +let map_union = Union.map + +(** Lifting equality onto union types. *) +let equal_union 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_union f g a = function + | Inl y -> f a y + | Inr y -> g a y + | _ -> a 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. *) -- cgit v1.2.3 From 34c467a4e41e20a9bf1318d47fbc09da94c5ad97 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 15 Mar 2016 19:56:52 +0100 Subject: Fix #4591: Uncaught exception in directory browsing. We protect Sys.readdir calls againts any nasty exception. --- lib/system.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/system.ml b/lib/system.ml index 0ad43a7423..36fdf26089 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -26,6 +26,8 @@ let ok_dirname f = not (String.List.mem f !skipped_dirnames) && (match Unicode.ident_refutation f with None -> true | _ -> false) +let readdir dir = try Sys.readdir dir with any -> [||] + let all_subdirs ~unix_path:root = let l = ref [] in let add f rel = l := (f, rel) :: !l in @@ -38,7 +40,7 @@ let all_subdirs ~unix_path:root = add file newrel; traverse file newrel end) - (Sys.readdir dir) + (readdir dir) in if exists_dir root then traverse root []; List.rev !l @@ -58,7 +60,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 contents, cached = -- cgit v1.2.3 From 29f26d380177495a224c3b94d3309a3d23693d8f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 11:01:32 +0100 Subject: Reducing the number of modules linked in grammar.cma. --- lib/ppstyle.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib') diff --git a/lib/ppstyle.ml b/lib/ppstyle.ml index bb73fbdf56..3ecaac0391 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 -- cgit v1.2.3 From 2537e84ba9fa92db6cfd3d7f5e400b1716c31246 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 14:42:51 +0100 Subject: Removing the registering of default values for generic arguments. --- lib/genarg.ml | 16 ++-------------- lib/genarg.mli | 6 ++---- 2 files changed, 4 insertions(+), 18 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index c7273ac93e..7aada461f5 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -246,7 +246,6 @@ struct end type ('raw, 'glb, 'top) load = { - nil : 'raw option; dyn : 'top Val.tag; } @@ -254,30 +253,19 @@ 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 ?dyn name = match ArgT.name name with | 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 obj = LoadMap.Pack { 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) diff --git a/lib/genarg.mli b/lib/genarg.mli index ce0536cf49..d509649f22 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -110,11 +110,11 @@ end 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 : ?dyn:'top Val.tag -> 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 : ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type (** Alias for [make0]. *) (** {5 Specialized types} *) @@ -250,8 +250,6 @@ val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, '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. -- cgit v1.2.3 From 2cf8f76ea6a15d46b57d5c4ecf9513683561e284 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Mar 2016 18:46:54 +0100 Subject: Removing the untyped representation of genargs. --- lib/genarg.ml | 53 +++++++++++++++++++++-------------------------------- lib/genarg.mli | 7 +------ 2 files changed, 22 insertions(+), 38 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index 7aada461f5..27d7b50e52 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -56,29 +56,6 @@ struct 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 | ListArg : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type @@ -86,6 +63,8 @@ type (_, _, _) 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 +90,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 rec 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 rec pr_argument_type (ArgumentType t) = pr_genarg_type t + type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type (** Alias for concision *) @@ -177,16 +172,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 diff --git a/lib/genarg.mli b/lib/genarg.mli index d509649f22..ac13f545ba 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -187,12 +187,7 @@ val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag (** {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} *) -- cgit v1.2.3 From 27d173f94a68367d91def90c6d287138c733054b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Mar 2016 18:55:01 +0100 Subject: Removing dead code in Genarg. --- lib/genarg.ml | 14 -------------- lib/genarg.mli | 10 ---------- 2 files changed, 24 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index 27d7b50e52..0deb34afd7 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -303,17 +303,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 ac13f545ba..30b96c7000 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -242,13 +242,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 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. *) -- cgit v1.2.3 From 2e557589920156fe84335e72c5e765347bcc7c9c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 2 Aug 2015 14:45:24 +0200 Subject: A patch renaming equal into eq in the module dealing with hash-consing, so as to avoid having too many kinds of equalities with same name. --- lib/cSet.ml | 2 +- lib/hashcons.ml | 12 ++++++------ lib/hashcons.mli | 12 ++++++------ lib/hashset.ml | 4 ++-- lib/hashset.mli | 2 +- 5 files changed, 16 insertions(+), 16 deletions(-) (limited to 'lib') 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/hashcons.ml b/lib/hashcons.ml index 144d951303..4a72b015c5 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) @@ -124,7 +124,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 @@ -144,7 +144,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 @@ -191,7 +191,7 @@ 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 6fb78f9a45..04009fdf3c 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 = { -- cgit v1.2.3 From 051c9a8a1112174769670cb0dc8cebb85ccb803c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 30 Mar 2016 12:06:53 +0200 Subject: Removing dead code in Genarg. --- lib/genarg.ml | 51 ++------------------------------------------------- 1 file changed, 2 insertions(+), 49 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index 0deb34afd7..a43466c627 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -98,13 +98,13 @@ let rec pr_genarg_type : type a b c. (a, b, c) genarg_type -> std_ppcmds = funct str "*" ++ spc () ++ pr_genarg_type t2 ++ str ")" | ExtraArg s -> str (ArgT.repr s) -let rec argument_type_eq arg1 arg2 = match arg1, arg2 with +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 rec pr_argument_type (ArgumentType t) = pr_genarg_type t +let pr_argument_type (ArgumentType t) = pr_genarg_type t type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type (** Alias for concision *) @@ -115,11 +115,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 @@ -183,48 +178,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 -- cgit v1.2.3 From c0aefc5323cb4393297adcaffd2967ab93ab815e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 30 Mar 2016 12:09:21 +0200 Subject: Ensuring that the type of base generic arguments contain triples. --- lib/genarg.ml | 17 +++++++++++++++-- lib/genarg.mli | 10 +++++----- 2 files changed, 20 insertions(+), 7 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index a43466c627..5d5b29c99d 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -10,7 +10,20 @@ open Pp open Util module ValT = Dyn.Make(struct end) -module ArgT = Dyn.Make(struct end) +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 module Val = struct @@ -57,7 +70,7 @@ struct end 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 -> diff --git a/lib/genarg.mli b/lib/genarg.mli index 30b96c7000..6cc7893dc4 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -70,15 +70,15 @@ ExtraArgType of string '_a '_b 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 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 -> -- cgit v1.2.3 From b5420538da04984ca42eb4284a9be27f3b5ba021 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 8 Apr 2016 00:58:56 +0200 Subject: Fixing printing of toplevel values. This is not perfect yet, in particular the whole precedence system is a real mess, as there is a real need for tidying up the Pptactic implementation. Nonetheless, printing toplevel values is only used for debugging purposes, where an ugly display is better than none at all. --- lib/genarg.ml | 12 +++++++----- lib/genarg.mli | 3 ++- 2 files changed, 9 insertions(+), 6 deletions(-) (limited to 'lib') diff --git a/lib/genarg.ml b/lib/genarg.ml index 5d5b29c99d..ef0de89afb 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -61,11 +61,13 @@ struct 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 ")" + let repr = ValT.repr + + let rec pr : type a. a tag -> std_ppcmds = function + | Base t -> str (repr t) + | List t -> pr t ++ spc () ++ str "list" + | Opt t -> pr t ++ spc () ++ str "option" + | Pair (t1, t2) -> str "(" ++ pr t1 ++ str " * " ++ pr t2 ++ str ")" end diff --git a/lib/genarg.mli b/lib/genarg.mli index 6cc7893dc4..93665fd45d 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -99,7 +99,8 @@ sig 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 + val repr : 'a typ -> string + val pr : 'a tag -> Pp.std_ppcmds end (** Dynamic types for toplevel values. While the generic types permit to relate -- cgit v1.2.3 From ce71ac17268f11ddd92f4bea85cbdd9c62acbc21 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 9 Apr 2016 11:56:53 +0200 Subject: In pr_clauses, do not print a leading space by default so that it can be used in the generic printer for tactics. Allows e.g. to print "symmetry in H" correctly after its move to TACTIC EXTEND. --- lib/pp.ml | 1 + lib/pp.mli | 3 +++ 2 files changed, 4 insertions(+) (limited to 'lib') diff --git a/lib/pp.ml b/lib/pp.ml index 9a833ae225..c7cf9b8d0e 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -518,6 +518,7 @@ 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 diff --git a/lib/pp.mli b/lib/pp.mli index 015151bc90..2e4d029749 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -199,6 +199,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. *) -- cgit v1.2.3 From 3b3d98acd58e91c960a2e11cd47ac19b2b34f86b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 15 Apr 2016 16:28:33 +0200 Subject: Cleaning unpolished commit 0dfd0fb7d7 on basic functions about union type. --- lib/util.ml | 12 ------------ 1 file changed, 12 deletions(-) (limited to 'lib') diff --git a/lib/util.ml b/lib/util.ml index cae996e332..009dfbe1c1 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -147,22 +147,10 @@ struct let fold_left f g a = function | Inl y -> f a y | Inr y -> g a y - | _ -> a end let map_union = Union.map -(** Lifting equality onto union types. *) -let equal_union 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_union f g a = function - | Inl y -> f a y - | Inr y -> g a y - | _ -> a - type iexn = Exninfo.iexn let iraise = Exninfo.iraise -- cgit v1.2.3