diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cWarnings.ml | 8 | ||||
| -rw-r--r-- | lib/coqProject_file.ml4 | 2 | ||||
| -rw-r--r-- | lib/envars.ml | 1 | ||||
| -rw-r--r-- | lib/feedback.ml | 22 | ||||
| -rw-r--r-- | lib/feedback.mli | 16 | ||||
| -rw-r--r-- | lib/flags.ml | 6 | ||||
| -rw-r--r-- | lib/flags.mli | 10 | ||||
| -rw-r--r-- | lib/future.ml | 82 | ||||
| -rw-r--r-- | lib/future.mli | 69 | ||||
| -rw-r--r-- | lib/minisys.ml | 14 | ||||
| -rw-r--r-- | lib/pp.ml | 19 | ||||
| -rw-r--r-- | lib/segmenttree.ml | 8 | ||||
| -rw-r--r-- | lib/segmenttree.mli | 8 | ||||
| -rw-r--r-- | lib/system.ml | 10 | ||||
| -rw-r--r-- | lib/system.mli | 6 | ||||
| -rw-r--r-- | lib/unicode.ml | 140 | ||||
| -rw-r--r-- | lib/unicode.mli | 18 | ||||
| -rw-r--r-- | lib/util.ml | 9 | ||||
| -rw-r--r-- | lib/util.mli | 5 |
19 files changed, 256 insertions, 197 deletions
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index ff7145267..3699b1c61 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -93,8 +93,12 @@ let split_flags s = "all" flag, and reverses the list. *) let rec cut_before_all_rev acc = function | [] -> acc - | (_status,name as w) :: warnings -> - cut_before_all_rev (w :: if is_all_keyword name then [] else acc) warnings + | (status,name as w) :: warnings -> + let acc = + if is_all_keyword name then [w] + else if is_none_keyword name then [(Disabled,"all")] + else w :: acc in + cut_before_all_rev acc warnings let cut_before_all_rev warnings = cut_before_all_rev [] warnings diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4 index 13de731f5..970666638 100644 --- a/lib/coqProject_file.ml4 +++ b/lib/coqProject_file.ml4 @@ -206,7 +206,7 @@ let rec find_project_file ~from ~projfile_name = if Sys.file_exists fname then Some fname else let newdir = Filename.dirname from in - if newdir = "" || newdir = "/" then None + if newdir = from then None else find_project_file ~from:newdir ~projfile_name ;; diff --git a/lib/envars.ml b/lib/envars.ml index 68604ae6c..206d75033 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -213,6 +213,7 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs = fprintf f "%sCAMLP4BIN=%s/\n" prefix_var_name (camlp4bin ()); fprintf f "%sCAMLP4LIB=%s\n" prefix_var_name (camlp4lib ()); fprintf f "%sCAMLP4OPTIONS=%s\n" prefix_var_name Coq_config.camlp4compat; + fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags; fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name (if Coq_config.has_natdynlink then "true" else "false"); fprintf f "%sCOQ_SRC_SUBDIRS=%s\n" prefix_var_name (String.concat " " coq_src_subdirs) diff --git a/lib/feedback.ml b/lib/feedback.ml index 54d16a9be..7a126363c 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -15,6 +15,7 @@ type level = | Warning | Error +type doc_id = int type route_id = int type feedback_content = @@ -35,7 +36,8 @@ type feedback_content = | Message of level * Loc.t option * Pp.t type feedback = { - id : Stateid.t; + doc_id : doc_id; (* The document being concerned *) + span_id : Stateid.t; route : route_id; contents : feedback_content; } @@ -52,23 +54,27 @@ let add_feeder = let del_feeder fid = Hashtbl.remove feeders fid let default_route = 0 -let feedback_id = ref Stateid.dummy +let span_id = ref Stateid.dummy +let doc_id = ref 0 let feedback_route = ref default_route -let set_id_for_feedback ?(route=default_route) i = - feedback_id := i; feedback_route := route +let set_id_for_feedback ?(route=default_route) d i = + doc_id := d; + span_id := i; + feedback_route := route -let feedback ?id ?route what = +let feedback ?did ?id ?route what = let m = { contents = what; - route = Option.default !feedback_route route; - id = Option.default !feedback_id id; + route = Option.default !feedback_route route; + doc_id = Option.default !doc_id did; + span_id = Option.default !span_id id; } in Hashtbl.iter (fun _ f -> f m) feeders (* Logging messages *) let feedback_logger ?loc lvl msg = - feedback ~route:!feedback_route ~id:!feedback_id (Message (lvl, loc, msg)) + feedback ~route:!feedback_route ~id:!span_id (Message (lvl, loc, msg)) let msg_info ?loc x = feedback_logger ?loc Info x let msg_notice ?loc x = feedback_logger ?loc Notice x diff --git a/lib/feedback.mli b/lib/feedback.mli index 45a02d384..73b84614f 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -17,6 +17,9 @@ type level = | Error +(** Document unique identifier for serialization *) +type doc_id = int + (** Coq "semantic" infos obtained during execution *) type route_id = int @@ -43,7 +46,8 @@ type feedback_content = | Message of level * Loc.t option * Pp.t type feedback = { - id : Stateid.t; (* The document part concerned *) + doc_id : doc_id; (* The document being concerned *) + span_id : Stateid.t; (* The document part concerned *) route : route_id; (* Extra routing info *) contents : feedback_content; (* The payload *) } @@ -60,13 +64,13 @@ val add_feeder : (feedback -> unit) -> int (** [del_feeder fid] removes the feeder with id [fid] *) val del_feeder : int -> unit -(** [feedback ?id ?route fb] produces feedback fb, with [route] and - [id] set appropiatedly, if absent, it will use the defaults set by - [set_id_for_feedback] *) -val feedback : ?id:Stateid.t -> ?route:route_id -> feedback_content -> unit +(** [feedback ?did ?sid ?route fb] produces feedback [fb], with + [route] and [did, sid] set appropiatedly, if absent, it will use + the defaults set by [set_id_for_feedback] *) +val feedback : ?did:doc_id -> ?id:Stateid.t -> ?route:route_id -> feedback_content -> unit (** [set_id_for_feedback route id] Set the defaults for feedback *) -val set_id_for_feedback : ?route:route_id -> Stateid.t -> unit +val set_id_for_feedback : ?route:route_id -> doc_id -> Stateid.t -> unit (** {6 output functions} diff --git a/lib/flags.ml b/lib/flags.ml index d4be81c61..a53a866ab 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -42,12 +42,8 @@ let with_extra_values o l f x = Exninfo.iraise reraise let boot = ref false -let load_init = ref true -let batch_mode = ref false -type compilation_mode = BuildVo | BuildVio | Vio2Vo -let compilation_mode = ref BuildVo -let compilation_output_name = ref None +let record_aux_file = ref false let test_mode = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 3024c6039..5233e72a2 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -11,14 +11,10 @@ (** Command-line flags *) val boot : bool ref -val load_init : bool ref -(* Will affect STM caching *) -val batch_mode : bool ref - -type compilation_mode = BuildVo | BuildVio | Vio2Vo -val compilation_mode : compilation_mode ref -val compilation_output_name : string option ref +(** Set by coqtop to tell the kernel to output to the aux file; will + be eventually removed by cleanups such as PR#1103 *) +val record_aux_file : bool ref (* Flag set when the test-suite is called. Its only effect to display verbose information for `Fail` *) diff --git a/lib/future.ml b/lib/future.ml index d9463aa0f..09285ea27 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -6,12 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* To deal with side effects we have to save/restore the system state *) -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 -> Pp.strbrk("The value you are asking for ("^name^") is not ready yet. "^ "Please wait or pass "^ @@ -30,6 +24,7 @@ let customize_not_here_msg f = not_here_msg := f exception NotReady of string exception NotHere of string + let _ = CErrors.register_handler (function | NotReady name -> !not_ready_msg name | NotHere name -> !not_here_msg name @@ -59,7 +54,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 * freeze option + | Val of 'a | Exn of Exninfo.iexn (* Invariant: this exception is always "fixed" as in fix_exn *) and 'a comput = @@ -74,7 +69,7 @@ let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f 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)) + | Finished v -> unnamed, UUID.invalid, id, ref (Val v) | Ongoing (name, x) -> try let uuid, fix, c = CEphemeron.get x in name, uuid, fix, c with CEphemeron.InvalidKey -> @@ -95,13 +90,13 @@ let is_exn kx = let _, _, _, x = get kx in match !x with | Val _ | Closure _ | Delegated _ -> false let peek_val kx = let _, _, _, x = get kx in match !x with - | Val (v, _) -> Some v + | Val v -> Some v | Exn _ | Closure _ | Delegated _ -> None let uuid kx = let _, id, _, _ = get kx in id -let from_val ?(fix_exn=id) v = create fix_exn (Val (v, None)) -let from_here ?(fix_exn=id) v = create fix_exn (Val (v, Some (!freeze ()))) +let from_val ?(fix_exn=id) v = create fix_exn (Val v) +let from_here ?(fix_exn=id) v = create fix_exn (Val v) let fix_exn_of ck = let _, _, fix_exn, _ = get ck in fix_exn @@ -110,7 +105,7 @@ let create_delegate ?(blocking=true) ~name fix_exn = let _, _, fix_exn, c = get ck in assert (match !c with Delegated _ -> true | _ -> false); begin match v with - | `Val v -> c := Val (v, None) + | `Val v -> c := Val v | `Exn e -> c := Exn (fix_exn e) | `Comp f -> let _, _, _, comp = get f in c := !comp end; signal () in @@ -124,17 +119,16 @@ let create_delegate ?(blocking=true) ~name fix_exn = ck, assignement signal ck (* TODO: get rid of try/catch to be stackless *) -let rec compute ~pure ck : 'a value = +let rec compute ck : 'a value = let _, _, fix_exn, c = get ck in match !c with - | Val (x, _) -> `Val x + | Val x -> `Val x | Exn (e, info) -> `Exn (e, info) - | Delegated wait -> wait (); compute ~pure ck + | Delegated wait -> wait (); compute ck | Closure f -> try let data = f () in - let state = if pure then None else Some (!freeze ()) in - c := Val (data, state); `Val data + c := Val data; `Val data with e -> let e = CErrors.push e in let e = fix_exn e in @@ -142,60 +136,30 @@ let rec compute ~pure ck : 'a value = | (NotReady _, _) -> `Exn e | _ -> c := Exn e; `Exn e -let force ~pure x = match compute ~pure x with +let force x = match compute x with | `Val v -> v | `Exn e -> Exninfo.iraise e -let chain ~pure ck f = +let chain ck f = let name, uuid, fix_exn, c = get ck in create ~uuid ~name fix_exn (match !c with - | Closure _ | Delegated _ -> Closure (fun () -> f (force ~pure ck)) + | Closure _ | Delegated _ -> Closure (fun () -> f (force ck)) | Exn _ as x -> x - | Val (v, None) when pure -> Val (f v, None) - | Val (v, Some _) when pure -> Val (f v, None) - | Val (v, Some state) -> Closure (fun () -> !unfreeze state; f v) - | Val (v, None) -> - match !ck with - | Finished _ -> CErrors.anomaly(Pp.str - "Future.chain ~pure:false call on an already joined computation.") - | Ongoing _ -> CErrors.anomaly(Pp.strbrk( - "Future.chain ~pure:false call on a pure computation. "^ - "This can happen if the computation was initial created with "^ - "Future.from_val or if it was Future.chain ~pure:true with a "^ - "function and later forced."))) + | Val v -> Val (f v)) let create fix_exn f = create fix_exn (Closure f) let replace kx y = let _, _, _, x = get kx in match !x with - | Exn _ -> x := Closure (fun () -> force ~pure:false y) + | Exn _ -> x := Closure (fun () -> force y) | _ -> CErrors.anomaly (Pp.str "A computation can be replaced only if is_exn holds.") -let purify f x = - let state = !freeze () in - try - let v = f x in - !unfreeze state; - v - with e -> - let e = CErrors.push e in !unfreeze state; Exninfo.iraise e - -let transactify f x = - let state = !freeze () in - try f x - with e -> - let e = CErrors.push e in !unfreeze state; Exninfo.iraise e - -let purify_future f x = if is_over x then f x else purify f x -let compute x = purify_future (compute ~pure:false) x -let force ~pure x = purify_future (force ~pure) x -let chain ~pure x f = - let y = chain ~pure x f in - if is_over x then ignore(force ~pure y); +let chain x f = + let y = chain x f in + if is_over x then ignore(force y); y -let force x = force ~pure:false x let join kx = let v = force kx in @@ -205,12 +169,11 @@ let join kx = let sink kx = if is_val kx then ignore(join kx) let split2 x = - chain ~pure:true x (fun x -> fst x), - chain ~pure:true x (fun x -> snd x) + chain x (fun x -> fst x), chain x (fun x -> snd x) let map2 f x l = CList.map_i (fun i y -> - let xi = chain ~pure:true x (fun x -> + let xi = chain x (fun x -> try List.nth x i with Failure _ | Invalid_argument _ -> CErrors.anomaly (Pp.str "Future.map2 length mismatch.")) in @@ -226,6 +189,5 @@ let print f kx = match !x with | Delegated _ -> str "Delegated" ++ uid | Closure _ -> str "Closure" ++ uid - | Val (x, None) -> str "PureVal" ++ uid ++ spc () ++ hov 0 (f x) - | Val (x, Some _) -> str "StateVal" ++ uid ++ spc () ++ hov 0 (f x) + | Val x -> str "PureVal" ++ uid ++ spc () ++ hov 0 (f x) | Exn (e, _) -> str "Exn" ++ uid ++ spc () ++ hov 0 (str (Printexc.to_string e)) diff --git a/lib/future.mli b/lib/future.mli index acfce51a0..853f81cea 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -6,42 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Futures: asynchronous computations with some purity enforcing +(* Futures: asynchronous computations. * * A Future.computation is like a lazy_t but with some extra bells and whistles - * to deal with imperative code and eventual delegation to a slave process. + * to deal with eventual delegation to a slave process. * - * Example of a simple scenario taken into account: - * - * let f = Future.from_here (number_of_constants (Global.env())) in - * let g = Future.chain ~pure:false f (fun n -> - * n = number_of_constants (Global.env())) in - * ... - * Lemmas.save_named ...; - * ... - * let b = Future.force g in - * - * The Future.computation f holds a (immediate, no lazy here) value. - * We then chain to obtain g that (will) hold false if (when it will be - * run) the global environment has a different number of constants, true - * if nothing changed. - * Before forcing g, we add to the global environment one more constant. - * When finally we force g. Its value is going to be *true*. - * This because Future.from_here stores in the computation not only the initial - * value but the entire system state. When g is forced the state is restored, - * hence Global.env() returns the environment that was actual when f was - * created. - * Last, forcing g is run protecting the system state, hence when g finishes, - * the actual system state is restored. - * - * If you compare this with lazy_t, you see that the value returned is *false*, - * that is counter intuitive and error prone. - * - * Still not all computations are impure and access/alter the system state. - * This class can be optimized by using ~pure:true, but there is no way to - * statically check if this flag is misused, hence use it with care. - * - * Other differences with lazy_t is that a future computation that produces + * One difference with lazy_t is that a future computation that produces * and exception can be substituted for another computation of the same type. * Moreover a future computation can be delegated to another execution entity * that will be allowed to set the result. Finally future computations can @@ -113,27 +83,17 @@ val is_exn : 'a computation -> bool val peek_val : 'a computation -> 'a option val uuid : 'a computation -> UUID.t -(* [chain pure c f] chains computation [c] with [f]. - * [chain] forces immediately the new computation if the old one is_over (Exn or Val). - * The [pure] parameter is tricky: - * [pure]: - * When pure is true, the returned computation will not keep a copy - * of the global state. - * [let c' = chain ~pure:true c f in let c'' = chain ~pure:false c' g in] - * is invalid. It works if one forces [c''] since the whole computation - * will be executed in one go. It will not work, and raise an anomaly, if - * one forces c' and then c''. - * [join c; chain ~pure:false c g] is invalid and fails at runtime. - * [force c; chain ~pure:false c g] is correct. - *) -val chain : pure:bool -> - 'a computation -> ('a -> 'b) -> 'b computation +(* [chain c f] chains computation [c] with [f]. + * [chain] is eager, that is to say, it won't suspend the new computation + * if the old one is_over (Exn or Val). +*) +val chain : 'a computation -> ('a -> 'b) -> 'b computation (* Forcing a computation *) val force : 'a computation -> 'a val compute : 'a computation -> 'a value -(* Final call, no more *inpure* chain allowed since the state is lost. +(* Final call. * Also the fix_exn function is lost, hence error reporting can be incomplete * in a computation obtained by chaining on a joined future. *) val join : 'a computation -> 'a @@ -148,19 +108,8 @@ val map2 : ('a computation -> 'b -> 'c) -> 'a list computation -> 'b list -> 'c list -(* Once set_freeze is called we can purify a computation *) -val purify : ('a -> 'b) -> 'a -> 'b -(* And also let a function alter the state but backtrack if it raises exn *) -val transactify : ('a -> 'b) -> 'a -> 'b - (** Debug: print a computation given an inner printing function. *) val print : ('a -> Pp.t) -> 'a computation -> Pp.t -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 -> freeze) -> (freeze -> unit) -> unit - val customize_not_ready_msg : (string -> Pp.t) -> unit val customize_not_here_msg : (string -> Pp.t) -> unit diff --git a/lib/minisys.ml b/lib/minisys.ml index 706f0430c..389b18ad4 100644 --- a/lib/minisys.ml +++ b/lib/minisys.ml @@ -36,10 +36,15 @@ let skipped_dirnames = ref ["CVS"; "_darcs"] let exclude_directory f = skipped_dirnames := f :: !skipped_dirnames +(* Note: this test is possibly used for Coq module/file names but also for + OCaml filenames, whose syntax as of today is more restrictive for + module names (only initial letter then letter, digits, _ or quote), + but more permissive (though disadvised) for file names *) + let ok_dirname f = not (f = "") && f.[0] != '.' && - not (List.mem f !skipped_dirnames) (*&& - (match Unicode.ident_refutation f with None -> true | _ -> false)*) + not (List.mem f !skipped_dirnames) && + match Unicode.ident_refutation f with None -> true | _ -> false (* Check directory can be opened *) @@ -55,10 +60,11 @@ let exists_dir 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 ok_dirname name then + let base = try Filename.chop_extension name with Invalid_argument _ -> name in + if ok_dirname base then let path = if path = "." then name else path//name in match try (Unix.stat path).Unix.st_kind with Unix.Unix_error _ -> Unix.S_BLK with - | Unix.S_DIR -> f (FileDir (path,name)) + | Unix.S_DIR when name = base -> f (FileDir (path,name)) | Unix.S_REG -> f (FileRegular name) | _ -> () @@ -82,10 +82,21 @@ let utf8_length s = done ; !cnt -let app s1 s2 = match s1, s2 with - | Ppcmd_empty, s - | s, Ppcmd_empty -> s - | s1, s2 -> Ppcmd_glue [s1; s2] +let rec app d1 d2 = match d1, d2 with + | Ppcmd_empty, d + | d, Ppcmd_empty -> d + + (* Optimizations *) + | Ppcmd_glue [l1;l2], Ppcmd_glue l3 -> Ppcmd_glue (l1 :: l2 :: l3) + | Ppcmd_glue [l1;l2], d2 -> Ppcmd_glue [l1 ; l2 ; d2] + | d1, Ppcmd_glue l2 -> Ppcmd_glue (d1 :: l2) + + | Ppcmd_tag(t1,d1), Ppcmd_tag(t2,d2) + when t1 = t2 -> Ppcmd_tag(t1,app d1 d2) + | d1, d2 -> Ppcmd_glue [d1; d2] + (* Optimizations deemed too costly *) + (* | Ppcmd_glue l1, Ppcmd_glue l2 -> Ppcmd_glue (l1 @ l2) *) + (* | Ppcmd_string s1, Ppcmd_string s2 -> Ppcmd_string (s1 ^ s2) *) let seq s = Ppcmd_glue s diff --git a/lib/segmenttree.ml b/lib/segmenttree.ml index 9ce348a0b..d0ded4cb5 100644 --- a/lib/segmenttree.ml +++ b/lib/segmenttree.ml @@ -1,3 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + (** This module is a very simple implementation of "segment trees". A segment tree of type ['a t] represents a mapping from a union of diff --git a/lib/segmenttree.mli b/lib/segmenttree.mli index 3258537b9..e274a6fdc 100644 --- a/lib/segmenttree.mli +++ b/lib/segmenttree.mli @@ -1,3 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + (** This module is a very simple implementation of "segment trees". A segment tree of type ['a t] represents a mapping from a union of diff --git a/lib/system.ml b/lib/system.ml index 12eacf2ea..4b5066ef4 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -52,7 +52,9 @@ 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 (readdir dir) + Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir) + +let trust_file_cache = ref true let exists_in_dir_respecting_case dir bf = let cache_dir dir = @@ -62,10 +64,10 @@ let exists_in_dir_respecting_case dir bf = let contents, fresh = try (* in batch mode, assume the directory content is still fresh *) - StrMap.find dir !dirmap, !Flags.batch_mode + StrMap.find dir !dirmap, !trust_file_cache 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 + if !trust_file_cache && not (exists_dir dir) then StrSet.empty, true else cache_dir dir, true in StrSet.mem bf contents || not fresh && @@ -80,7 +82,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 (!Flags.batch_mode || Sys.file_exists (Filename.concat path f)) && aux f + in (!trust_file_cache || Sys.file_exists (Filename.concat path f)) && aux f let rec search paths test = match paths with diff --git a/lib/system.mli b/lib/system.mli index 7281de97c..aa964abeb 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -54,6 +54,12 @@ val where_in_path_rex : val find_file_in_path : ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string +val trust_file_cache : bool ref +(** [trust_file_cache] indicates whether we trust the underlying + mapped file-system not to change along the execution of Coq. This + assumption greatly speds up file search, but it is often + inconvenient in interactive mode *) + val file_exists_respecting_case : string -> string -> bool (** {6 I/O functions } *) diff --git a/lib/unicode.ml b/lib/unicode.ml index 959ccaf73..f193c4e0f 100644 --- a/lib/unicode.ml +++ b/lib/unicode.ml @@ -8,13 +8,14 @@ (** Unicode utilities *) -type status = Letter | IdentPart | Symbol | Unknown +type status = Letter | IdentPart | Symbol | IdentSep | Unknown (* The following table stores classes of Unicode characters that - are used by the lexer. There are 3 different classes so 2 bits are - allocated for each character. We only use 16 bits over the 31 bits - to simplify the masking process. (This choice seems to be a good - trade-off between speed and space after some benchmarks.) *) + are used by the lexer. There are 5 different classes so 3 bits + are allocated for each character. We encode the masks of 8 + characters per word, thus using 24 bits over the 31 available + bits. (This choice seems to be a good trade-off between speed + and space after some benchmarks.) *) (* A 256 KiB table, initially filled with zeros. *) let table = Array.make (1 lsl 17) 0 @@ -24,14 +25,15 @@ let table = Array.make (1 lsl 17) 0 define the position of the pattern in the word. Notice that pattern "00" means "undefined". *) let mask i = function - | Letter -> 1 lsl ((i land 7) lsl 1) (* 01 *) - | IdentPart -> 2 lsl ((i land 7) lsl 1) (* 10 *) - | Symbol -> 3 lsl ((i land 7) lsl 1) (* 11 *) - | Unknown -> 0 lsl ((i land 7) lsl 1) (* 00 *) + | Letter -> 1 lsl ((i land 7) * 3) (* 001 *) + | IdentPart -> 2 lsl ((i land 7) * 3) (* 010 *) + | Symbol -> 3 lsl ((i land 7) * 3) (* 011 *) + | IdentSep -> 4 lsl ((i land 7) * 3) (* 100 *) + | Unknown -> 0 lsl ((i land 7) * 3) (* 000 *) -(* Helper to reset 2 bits in a word. *) +(* Helper to reset 3 bits in a word. *) let reset_mask i = - lnot (3 lsl ((i land 7) lsl 1)) + lnot (7 lsl ((i land 7) * 3)) (* Initialize the lookup table from a list of segments, assigning a status to every character of each segment. The order of these @@ -50,13 +52,14 @@ let mk_lookup_table_from_unicode_tables_for status tables = (* Look up into the table and interpret the found pattern. *) let lookup x = - let v = (table.(x lsr 3) lsr ((x land 7) lsl 1)) land 3 in + let v = (table.(x lsr 3) lsr ((x land 7) * 3)) land 7 in if v = 1 then Letter else if v = 2 then IdentPart else if v = 3 then Symbol + else if v = 4 then IdentSep else Unknown -(* [classify] discriminates between 3 different kinds of +(* [classify] discriminates between 5 different kinds of symbols based on the standard unicode classification (extracted from Camomile). *) let classify = @@ -67,13 +70,13 @@ let classify = Unicodetable.sm; (* Symbol, maths. *) Unicodetable.sc; (* Symbol, currency. *) Unicodetable.so; (* Symbol, modifier. *) - Unicodetable.pd; (* Punctation, dash. *) - Unicodetable.pc; (* Punctation, connector. *) - Unicodetable.pe; (* Punctation, open. *) - Unicodetable.ps; (* Punctation, close. *) - Unicodetable.pi; (* Punctation, initial quote. *) - Unicodetable.pf; (* Punctation, final quote. *) - Unicodetable.po; (* Punctation, other. *) + Unicodetable.pd; (* Punctuation, dash. *) + Unicodetable.pc; (* Punctuation, connector. *) + Unicodetable.pe; (* Punctuation, open. *) + Unicodetable.ps; (* Punctution, close. *) + Unicodetable.pi; (* Punctuation, initial quote. *) + Unicodetable.pf; (* Punctuation, final quote. *) + Unicodetable.po; (* Punctuation, other. *) ]; mk_lookup_table_from_unicode_tables_for Letter [ @@ -107,14 +110,14 @@ let classify = [(0x02074, 0x02079)]; (* Superscript 4-9. *) single 0x0002E; (* Dot. *) ]; - mk_lookup_table_from_unicode_tables_for Letter + mk_lookup_table_from_unicode_tables_for IdentSep [ single 0x005F; (* Underscore. *) single 0x00A0; (* Non breaking space. *) ]; mk_lookup_table_from_unicode_tables_for IdentPart [ - single 0x0027; (* Special space. *) + single 0x0027; (* Single quote. *) ]; (* Lookup *) lookup @@ -163,24 +166,75 @@ let is_utf8 s = in try check 0 with End_of_input -> true | Invalid_argument _ -> false +(* Escape string if it contains non-utf8 characters *) + +let escaped_non_utf8 s = + let mk_escape x = Printf.sprintf "%%%X" x in + let buff = Buffer.create (String.length s * 3) in + let rec process_trailing_aux i j = + if i = j then i else + match String.unsafe_get s i with + | '\128'..'\191' -> process_trailing_aux (i+1) j + | _ -> i in + let process_trailing i n = + let j = if i+n-1 >= String.length s then i+1 else process_trailing_aux (i+1) (i+n) in + (if j = i+n then + Buffer.add_string buff (String.sub s i n) + else + let v = Array.init (j-i) (fun k -> mk_escape (Char.code s.[i+k])) in + Buffer.add_string buff (String.concat "" (Array.to_list v))); + j in + let rec process i = + if i >= String.length s then Buffer.contents buff else + let c = String.unsafe_get s i in + match c with + | '\000'..'\127' -> Buffer.add_char buff c; process (i+1) + | '\128'..'\191' | '\248'..'\255' -> Buffer.add_string buff (mk_escape (Char.code c)); process (i+1) + | '\192'..'\223' -> process (process_trailing i 2) + | '\224'..'\239' -> process (process_trailing i 3) + | '\240'..'\247' -> process (process_trailing i 4) + in + process 0 + +let escaped_if_non_utf8 s = + if is_utf8 s then s else escaped_non_utf8 s + (* Check the well-formedness of an identifier *) +let is_valid_ident_initial = function + | Letter | IdentSep -> true + | IdentPart | Symbol | Unknown -> false + let initial_refutation j n s = - match classify n with - | Letter -> None - | _ -> + if is_valid_ident_initial (classify n) then None + else let c = String.sub s 0 j in Some (false, "Invalid character '"^c^"' at beginning of identifier \""^s^"\".") +let is_valid_ident_trailing = function + | Letter | IdentSep | IdentPart -> true + | Symbol | Unknown -> false + let trailing_refutation i j n s = - match classify n with - | Letter | IdentPart -> None - | _ -> + if is_valid_ident_trailing (classify n) then None + else let c = String.sub s i j in Some (false, "Invalid character '"^c^"' in identifier \""^s^"\".") +let is_unknown = function + | Unknown -> true + | Letter | IdentSep | IdentPart | Symbol -> false + +let is_ident_part = function + | IdentPart -> true + | Letter | IdentSep | Symbol | Unknown -> false + +let is_ident_sep = function + | IdentSep -> true + | Letter | IdentPart | Symbol | Unknown -> false + let ident_refutation s = if s = ".." then None else try let j, n = next_utf8 s 0 in @@ -198,7 +252,7 @@ let ident_refutation s = |x -> x with | End_of_input -> Some (true,"The empty string is not an identifier.") - | Invalid_argument _ -> Some (true,s^": invalid utf8 sequence.") + | Invalid_argument _ -> Some (true,escaped_non_utf8 s^": invalid utf8 sequence.") let lowercase_unicode = let tree = Segmenttree.make Unicodetable.to_lower in @@ -214,6 +268,26 @@ let lowercase_first_char s = let j, n = next_utf8 s 0 in utf8_of_unicode (lowercase_unicode n) +let split_at_first_letter s = + let n, v = next_utf8 s 0 in + if ((* optim *) n = 1 && s.[0] != '_') || not (is_ident_sep (classify v)) then None + else begin + let n = ref n in + let p = ref 0 in + while !n < String.length s && + let n', v = next_utf8 s !n in + p := n'; + (* Test if not letter *) + ((* optim *) n' = 1 && (s.[!n] = '_' || s.[!n] = '\'')) + || let st = classify v in + is_ident_sep st || is_ident_part st + do n := !n + !p + done; + let s1 = String.sub s 0 !n in + let s2 = String.sub s !n (String.length s - !n) in + Some (s1,s2) + end + (** For extraction, we need to encode unicode character into ascii ones *) let is_basic_ascii s = @@ -268,9 +342,7 @@ let utf8_length s = | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *) | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *) | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *) - | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *) - | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *) - | '\254'..'\255' -> nc := 0 (* invalid byte *) + | '\248'..'\255' -> nc := 0 (* invalid byte *) end ; incr p ; while !p < len && !nc > 0 do @@ -299,9 +371,7 @@ let utf8_sub s start_u len_u = | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *) | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *) | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *) - | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *) - | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *) - | '\254'..'\255' -> nc := 0 (* invalid byte *) + | '\248'..'\255' -> nc := 0 (* invalid byte *) end ; incr p ; while !p < len_b && !nc > 0 do diff --git a/lib/unicode.mli b/lib/unicode.mli index c7d742480..32ffbb8e9 100644 --- a/lib/unicode.mli +++ b/lib/unicode.mli @@ -8,7 +8,7 @@ (** Unicode utilities *) -type status = Letter | IdentPart | Symbol | Unknown +type status (** Classify a unicode char into 3 classes or unknown. *) val classify : int -> status @@ -17,10 +17,23 @@ val classify : int -> status Return [Some (b,s)] otherwise, where [s] is an explanation and [b] is severity. *) val ident_refutation : string -> (bool * string) option +(** Tells if a valid initial character for an identifier *) +val is_valid_ident_initial : status -> bool + +(** Tells if a valid non-initial character for an identifier *) +val is_valid_ident_trailing : status -> bool + +(** Tells if a character is unclassified *) +val is_unknown : status -> bool + (** First char of a string, converted to lowercase @raise Assert_failure if the input string is empty. *) val lowercase_first_char : string -> string +(** Split a string supposed to be an ident at the first letter; + as an optimization, return None if the first character is a letter *) +val split_at_first_letter : string -> (string * string) option + (** 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 @@ -40,3 +53,6 @@ val utf8_length : string -> int (** Variant of {!String.sub} for UTF-8 strings. *) val utf8_sub : string -> int -> int -> string + +(** Return a "%XX"-escaped string if it contains non UTF-8 characters. *) +val escaped_if_non_utf8 : string -> string diff --git a/lib/util.ml b/lib/util.ml index 36282b2da..6de012da0 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -171,3 +171,12 @@ let open_utf8_file_in fname = let s = Bytes.make 3 ' ' in if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0; in_chan + +(** A trick which can typically be used to store on the fly the + computation of values in the "when" clause of a "match" then + retrieve the evaluated result in the r.h.s of the clause *) + +let set_temporary_memory () = + let a = ref None in + (fun x -> assert (!a = None); a := Some x; x), + (fun () -> match !a with Some x -> x | None -> assert false) diff --git a/lib/util.mli b/lib/util.mli index d910e7e28..c54f5825c 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -137,3 +137,8 @@ val sym : ('a, 'b) eq -> ('b, 'a) eq val open_utf8_file_in : string -> in_channel (** Open an utf-8 encoded file and skip the byte-order mark if any. *) + +val set_temporary_memory : unit -> ('a -> 'a) * (unit -> 'a) +(** A trick which can typically be used to store on the fly the + computation of values in the "when" clause of a "match" then + retrieve the evaluated result in the r.h.s of the clause *) |