diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cMap.ml | 10 | ||||
| -rw-r--r-- | lib/cMap.mli | 2 | ||||
| -rw-r--r-- | lib/cSig.mli | 6 | ||||
| -rw-r--r-- | lib/cUnix.ml | 5 | ||||
| -rw-r--r-- | lib/cUnix.mli | 7 | ||||
| -rw-r--r-- | lib/control.ml | 18 | ||||
| -rw-r--r-- | lib/control.mli | 11 | ||||
| -rw-r--r-- | lib/hMap.ml | 26 |
8 files changed, 50 insertions, 35 deletions
diff --git a/lib/cMap.ml b/lib/cMap.ml index 0ecb40209c..b4c4aedd0e 100644 --- a/lib/cMap.ml +++ b/lib/cMap.ml @@ -26,7 +26,7 @@ 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 set : key -> 'a -> 'a t -> 'a t val modify : key -> (key -> 'a -> 'a) -> 'a t -> 'a t val domain : 'a t -> Set.t val bind : (key -> 'a) -> Set.t -> 'a t @@ -50,7 +50,7 @@ end module MapExt (M : Map.OrderedType) : sig type 'a map = 'a Map.Make(M).t - val update : M.t -> 'a -> 'a map -> 'a map + val set : M.t -> 'a -> 'a map -> 'a map val modify : M.t -> (M.t -> 'a -> 'a) -> 'a map -> 'a map val domain : 'a map -> Set.Make(M).t val bind : (M.t -> 'a) -> Set.Make(M).t -> 'a map @@ -93,19 +93,19 @@ struct let set_prj : set -> _set = Obj.magic let set_inj : _set -> set = Obj.magic - let rec update k v (s : 'a map) : 'a map = match map_prj s with + let rec set k v (s : 'a map) : 'a map = match map_prj s with | MEmpty -> raise Not_found | MNode (l, k', v', r, h) -> let c = M.compare k k' in if c < 0 then - let l' = update k v l in + let l' = set k v l in if l == l' then s else map_inj (MNode (l', k', v', r, h)) else if c = 0 then if v' == v then s else map_inj (MNode (l, k', v, r, h)) else - let r' = update k v r in + let r' = set k v r in if r == r' then s else map_inj (MNode (l, k', v', r', h)) diff --git a/lib/cMap.mli b/lib/cMap.mli index f65036139b..5e65bd200a 100644 --- a/lib/cMap.mli +++ b/lib/cMap.mli @@ -34,7 +34,7 @@ sig 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 + val set : 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/cSig.mli b/lib/cSig.mli index 6910cbbf03..32e9d2af0c 100644 --- a/lib/cSig.mli +++ b/lib/cSig.mli @@ -56,6 +56,12 @@ sig val is_empty: 'a t -> bool val mem: key -> 'a t -> bool val add: key -> 'a -> 'a t -> 'a t + (* when Coq requires OCaml 4.06 or later, can add: + + val update : key -> ('a option -> 'a option) -> 'a t -> 'a t + + allowing Coq to use OCaml's "update" + *) val singleton: key -> 'a -> 'a t val remove: key -> 'a t -> 'a t val merge: diff --git a/lib/cUnix.ml b/lib/cUnix.ml index 867f86a746..34fb660db4 100644 --- a/lib/cUnix.ml +++ b/lib/cUnix.ml @@ -14,6 +14,11 @@ type load_path = physical_path list let physical_path_of_string s = s let string_of_physical_path p = p +let escaped_string_of_physical_path p = + (* We assume a reasonable-enough path (typically utf8) and prevents + the presence of space; other escapings might be useful... *) + if String.contains p ' ' then "\"" ^ p ^ "\"" else p + let path_to_list p = let sep = Str.regexp (if Sys.os_type = "Win32" then ";" else ":") in Str.split sep p diff --git a/lib/cUnix.mli b/lib/cUnix.mli index a394814041..d08dc4c403 100644 --- a/lib/cUnix.mli +++ b/lib/cUnix.mli @@ -14,9 +14,12 @@ type load_path = physical_path list val physical_path_of_string : string -> physical_path val string_of_physical_path : physical_path -> string +(** Escape what has to be escaped (e.g. surround with quotes if with spaces) *) +val escaped_string_of_physical_path : physical_path -> string + val canonical_path_name : string -> string -(** remove all initial "./" in a path *) +(** Remove all initial "./" in a path *) val remove_path_dot : string -> string (** If a path [p] starts with the current directory $PWD then @@ -61,6 +64,6 @@ val sys_command : string -> string list -> Unix.process_status val waitpid_non_intr : int -> Unix.process_status -(** checks if two file names refer to the same (existing) file *) +(** Check if two file names refer to the same (existing) file *) val same_file : string -> string -> bool diff --git a/lib/control.ml b/lib/control.ml index f5d7df204e..d936d7557b 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -26,7 +26,7 @@ let check_for_interrupt () = end (** This function does not work on windows, sigh... *) -let unix_timeout n f e = +let unix_timeout n f x e = let timeout_handler _ = raise e in let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in let _ = Unix.alarm n in @@ -35,7 +35,7 @@ let unix_timeout n f e = Sys.set_signal Sys.sigalrm psh in try - let res = f () in + let res = f x in restore_timeout (); res with e -> @@ -43,7 +43,7 @@ let unix_timeout n f e = restore_timeout (); Exninfo.iraise e -let windows_timeout n f e = +let windows_timeout n f x e = let killed = ref false in let exited = ref false in let thread init = @@ -60,7 +60,7 @@ let windows_timeout n f e = let init = Unix.gettimeofday () in let _id = Thread.create thread init in try - let res = f () in + let res = f x in let () = killed := true in let cur = Unix.gettimeofday () in (** The thread did not interrupt, but the computation took longer than @@ -80,12 +80,10 @@ let windows_timeout n f e = let e = Backtrace.add_backtrace e in Exninfo.iraise e -type timeout = { timeout : 'a. int -> (unit -> 'a) -> exn -> 'a } +type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b } let timeout_fun = match Sys.os_type with -| "Unix" | "Cygwin" -> ref { timeout = unix_timeout } -| _ -> ref { timeout = windows_timeout } +| "Unix" | "Cygwin" -> { timeout = unix_timeout } +| _ -> { timeout = windows_timeout } -let set_timeout f = timeout_fun := f - -let timeout n f e = !timeout_fun.timeout n f e +let timeout n f e = timeout_fun.timeout n f e diff --git a/lib/control.mli b/lib/control.mli index 337cdf67b0..f6c63ffb34 100644 --- a/lib/control.mli +++ b/lib/control.mli @@ -16,11 +16,6 @@ val check_for_interrupt : unit -> unit (** Use this function as a potential yield function. If {!interrupt} has been set, il will raise [Sys.Break]. *) -val timeout : int -> (unit -> 'a) -> exn -> 'a -(** [timeout n f e] tries to compute [f], and if it fails to do so before [n] - seconds, it raises [e] instead. *) - -type timeout = { timeout : 'a. int -> (unit -> 'a) -> exn -> 'a } - -val set_timeout : timeout -> unit -(** Set a particular timeout function. *) +val timeout : int -> ('a -> 'b) -> 'a -> exn -> 'b +(** [timeout n f x e] tries to compute [f x], and if it fails to do so + before [n] seconds, it raises [e] instead. *) diff --git a/lib/hMap.ml b/lib/hMap.ml index c69efdb711..37079af783 100644 --- a/lib/hMap.ml +++ b/lib/hMap.ml @@ -47,7 +47,7 @@ struct try let m = Int.Map.find h s in let m = Set.add x m in - Int.Map.update h m s + Int.Map.set h m s with Not_found -> let m = Set.singleton x in Int.Map.add h m s @@ -65,7 +65,7 @@ struct if Set.is_empty m then Int.Map.remove h s else - Int.Map.update h m s + Int.Map.set h m s with Not_found -> s let height s = Int.Map.height s @@ -135,7 +135,7 @@ struct let s' = Int.Map.find h accu in let si = Set.filter (fun e -> not (Set.mem e s)) s' in if Set.is_empty si then Int.Map.remove h accu - else Int.Map.update h si accu + else Int.Map.set h si accu with Not_found -> accu in Int.Map.fold fold s2 s1 @@ -242,11 +242,19 @@ struct try let m = Int.Map.find h s in let m = Map.add k x m in - Int.Map.update h m s + Int.Map.set h m s with Not_found -> let m = Map.singleton k x in Int.Map.add h m s + (* when Coq requires OCaml 4.06 or later, the module type + CSig.MapS may include the signature of OCaml's "update", + requiring an implementation here, which could be just: + + let update k f s = assert false (* not implemented *) + + *) + let singleton k x = let h = M.hash k in Int.Map.singleton h (Map.singleton k x) @@ -259,7 +267,7 @@ struct if Map.is_empty m then Int.Map.remove h s else - Int.Map.update h m s + Int.Map.set h m s with Not_found -> s let merge f s1 s2 = @@ -359,7 +367,7 @@ struct let h = M.hash k in let m = Int.Map.find h s in let m = Map.modify k f m in - Int.Map.update h m s + Int.Map.set h m s let bind f s = let fb m = Map.bind f m in @@ -367,11 +375,11 @@ struct let domain s = Int.Map.map Map.domain s - let update k x s = + let set k x s = let h = M.hash k in let m = Int.Map.find h s in - let m = Map.update k x m in - Int.Map.update h m s + let m = Map.set k x m in + Int.Map.set h m s let smartmap f s = let fs m = Map.smartmap f m in |