aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/acyclicGraph.ml171
-rw-r--r--lib/cWarnings.ml6
-rw-r--r--lib/cWarnings.mli7
-rw-r--r--lib/control.ml11
-rw-r--r--lib/control.mli4
-rw-r--r--lib/stateid.ml3
-rw-r--r--lib/stateid.mli7
-rw-r--r--lib/util.ml7
-rw-r--r--lib/util.mli9
9 files changed, 171 insertions, 54 deletions
diff --git a/lib/acyclicGraph.ml b/lib/acyclicGraph.ml
index 14c08da35d..17299c72eb 100644
--- a/lib/acyclicGraph.ml
+++ b/lib/acyclicGraph.ml
@@ -58,15 +58,59 @@ module Make (Point:Point) = struct
*)
- module PMap = Point.Map
- module PSet = Point.Set
+ module Index :
+ sig
+ type t
+ val equal : t -> t -> bool
+ module Set : CSig.SetS with type elt = t
+ module Map : CMap.ExtS with type key = t and module Set := Set
+ type table
+ val empty : table
+ val fresh : Point.t -> table -> t * table
+ val mem : Point.t -> table -> bool
+ val find : Point.t -> table -> t
+ val repr : t -> table -> Point.t
+ end =
+ struct
+ type t = int
+ let equal = Int.equal
+ module Set = Int.Set
+ module Map = Int.Map
+
+ type table = {
+ tab_len : int;
+ tab_fwd : Point.t Int.Map.t;
+ tab_bwd : int Point.Map.t
+ }
+
+ let empty = {
+ tab_len = 0;
+ tab_fwd = Int.Map.empty;
+ tab_bwd = Point.Map.empty;
+ }
+ let mem x t = Point.Map.mem x t.tab_bwd
+ let find x t = Point.Map.find x t.tab_bwd
+ let repr n t = Int.Map.find n t.tab_fwd
+
+ let fresh x t =
+ let () = assert (not @@ mem x t) in
+ let n = t.tab_len in
+ n, {
+ tab_len = n + 1;
+ tab_fwd = Int.Map.add n x t.tab_fwd;
+ tab_bwd = Point.Map.add x n t.tab_bwd;
+ }
+ end
+
+ module PMap = Index.Map
+ module PSet = Index.Set
module Constraint = Point.Constraint
type status = NoMark | Visited | WeakVisited | ToMerge
(* Comparison on this type is pointer equality *)
type canonical_node =
- { canon: Point.t;
+ { canon: Index.t;
ltle: bool PMap.t; (* true: strict (lt) constraint.
false: weak (le) constraint. *)
gtge: PSet.t;
@@ -81,12 +125,13 @@ module Make (Point:Point) = struct
type entry =
| Canonical of canonical_node
- | Equiv of Point.t
+ | Equiv of Index.t
type t =
{ entries : entry PMap.t;
index : int;
- n_nodes : int; n_edges : int }
+ n_nodes : int; n_edges : int;
+ table : Index.table }
(** Used to cleanup mutable marks if a traversal function is
interrupted before it has the opportunity to do it itself. *)
@@ -121,7 +166,8 @@ module Make (Point:Point) = struct
| _ -> assert false) g.entries;
index = g.index;
n_nodes = g.n_nodes - 1;
- n_edges = g.n_edges }
+ n_edges = g.n_edges;
+ table = g.table }
(* Low-level function : changes data associated with a canonical node.
Resets the mutable fields in the old record, in order to avoid breaking
@@ -145,7 +191,10 @@ module Make (Point:Point) = struct
| Canonical arc -> arc
| exception Not_found ->
CErrors.anomaly ~label:"Univ.repr"
- Pp.(str"Universe " ++ Point.pr u ++ str" undefined.")
+ Pp.(str"Universe " ++ Point.pr (Index.repr u g.table) ++ str" undefined.")
+
+ let repr_node g u =
+ repr g (Index.find u g.table)
exception AlreadyDeclared
@@ -168,6 +217,7 @@ module Make (Point:Point) = struct
(* Checks most of the invariants of the graph. For debugging purposes. *)
let check_invariants ~required_canonical g =
+ let required_canonical u = required_canonical (Index.repr u g.table) in
let n_edges = ref 0 in
let n_nodes = ref 0 in
PMap.iter (fun l u ->
@@ -188,7 +238,7 @@ module Make (Point:Point) = struct
PMap.exists (fun l _ -> u == repr g l) v.ltle))
) u.gtge;
assert (u.status = NoMark);
- assert (Point.equal l u.canon);
+ assert (Index.equal l u.canon);
assert (u.ilvl > g.index);
assert (not (PMap.mem u.canon u.ltle));
incr n_nodes
@@ -200,7 +250,7 @@ module Make (Point:Point) = struct
let clean_ltle g ltle =
PMap.fold (fun u strict acc ->
let uu = (repr g u).canon in
- if Point.equal uu u then acc
+ if Index.equal uu u then acc
else (
let acc = PMap.remove u (fst acc) in
if not strict && PMap.mem uu acc then (acc, true)
@@ -210,7 +260,7 @@ module Make (Point:Point) = struct
let clean_gtge g gtge =
PSet.fold (fun u acc ->
let uu = (repr g u).canon in
- if Point.equal uu u then acc
+ if Index.equal uu u then acc
else PSet.add uu (PSet.remove u (fst acc)), true)
gtge (gtge, false)
@@ -314,7 +364,7 @@ module Make (Point:Point) = struct
| Visited -> false, to_revert | ToMerge -> true, to_revert
| NoMark ->
let to_revert = x::to_revert in
- if Point.equal x.canon v then
+ if Index.equal x.canon v then
begin x.status <- ToMerge; true, to_revert end
else
begin
@@ -425,7 +475,7 @@ module Make (Point:Point) = struct
(* Inserting shortcuts for old nodes. *)
let g = List.fold_left (fun g n ->
- if Point.equal n.canon root.canon then g else enter_equiv g n.canon root.canon)
+ if Index.equal n.canon root.canon then g else enter_equiv g n.canon root.canon)
g to_merge
in
@@ -481,11 +531,10 @@ module Make (Point:Point) = struct
raise e
let add ?(rank=0) v g =
- try
- let _arcv = PMap.find v g.entries in
- raise AlreadyDeclared
- with Not_found ->
- assert (g.index > min_int);
+ if Index.mem v g.table then raise AlreadyDeclared
+ else
+ let () = assert (g.index > min_int) in
+ let v, table = Index.fresh v g.table in
let node = {
canon = v;
ltle = PMap.empty;
@@ -497,17 +546,18 @@ module Make (Point:Point) = struct
}
in
let entries = PMap.add v (Canonical node) g.entries in
- { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges }
+ { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges; table }
exception Undeclared of Point.t
let check_declared g us =
- let check l = if not (PMap.mem l g.entries) then raise (Undeclared l) in
- PSet.iter check us
+ let check l = if not (Index.mem l g.table) then raise (Undeclared l) in
+ Point.Set.iter check us
exception Found_explanation of (constraint_type * Point.t) list
let get_explanation strict u v g =
- let v = repr g v in
+ let u = Index.find u g.table in
+ let v = repr_node g v in
let visited_strict = ref PMap.empty in
let rec traverse strict u =
if u == v then
@@ -527,6 +577,7 @@ module Make (Point:Point) = struct
| None -> ()
| Some exp ->
let typ = if strictu' then Lt else Le in
+ let u' = Index.repr u' g.table in
raise (Found_explanation ((typ, u') :: exp)))
u.ltle;
None
@@ -534,7 +585,7 @@ module Make (Point:Point) = struct
end
in
let u = repr g u in
- if u == v then [(Eq, v.canon)]
+ if u == v then [(Eq, Index.repr v.canon g.table)]
else match traverse strict u with Some exp -> exp | None -> assert false
let get_explanation strict u v g =
@@ -608,21 +659,27 @@ module Make (Point:Point) = struct
let check_eq g u v =
u == v ||
- let arcu = repr g u and arcv = repr g v in
+ let arcu = repr_node g u and arcv = repr_node g v in
arcu == arcv
let check_smaller g strict u v =
- search_path strict (repr g u) (repr g v) g
+ search_path strict (repr_node g u) (repr_node g v) g
let check_leq g u v = check_smaller g false u v
let check_lt g u v = check_smaller g true u v
(* enforce_eq g u v will force u=v if possible, will fail otherwise *)
- let rec enforce_eq u v g =
- let ucan = repr g u in
- let vcan = repr g v in
- if topo_compare ucan vcan = 1 then enforce_eq v u g
+ let enforce_eq u v g =
+ let ucan = repr_node g u in
+ let vcan = repr_node g v in
+ if ucan == vcan then g
+ else if topo_compare ucan vcan = 1 then
+ let ucan = vcan and vcan = ucan in
+ let g = insert_edge false ucan vcan g in (* Cannot fail *)
+ try insert_edge false vcan ucan g
+ with CycleDetected ->
+ Point.error_inconsistency Eq v u (get_explanation true v u g)
else
let g = insert_edge false ucan vcan g in (* Cannot fail *)
try insert_edge false vcan ucan g
@@ -631,35 +688,40 @@ module Make (Point:Point) = struct
(* enforce_leq g u v will force u<=v if possible, will fail otherwise *)
let enforce_leq u v g =
- let ucan = repr g u in
- let vcan = repr g v in
+ let ucan = repr_node g u in
+ let vcan = repr_node g v in
try insert_edge false ucan vcan g
with CycleDetected ->
Point.error_inconsistency Le u v (get_explanation true v u g)
(* enforce_lt u v will force u<v if possible, will fail otherwise *)
let enforce_lt u v g =
- let ucan = repr g u in
- let vcan = repr g v in
+ let ucan = repr_node g u in
+ let vcan = repr_node g v in
try insert_edge true ucan vcan g
with CycleDetected ->
Point.error_inconsistency Lt u v (get_explanation false v u g)
let empty =
- { entries = PMap.empty; index = 0; n_nodes = 0; n_edges = 0 }
+ { entries = PMap.empty; index = 0; n_nodes = 0; n_edges = 0; table = Index.empty }
(* Normalization *)
let constraints_of g =
- let module UF = Unionfind.Make (PSet) (PMap) in
+ let module UF = Unionfind.Make (Point.Set) (Point.Map) in
let uf = UF.create () in
let constraints_of u v acc =
match v with
| Canonical {canon=u; ltle; _} ->
PMap.fold (fun v strict acc->
let typ = if strict then Lt else Le in
+ let u = Index.repr u g.table in
+ let v = Index.repr v g.table in
Constraint.add (u,typ,v) acc) ltle acc
- | Equiv v -> UF.union u v uf; acc
+ | Equiv v ->
+ let u = Index.repr u g.table in
+ let v = Index.repr v g.table in
+ UF.union u v uf; acc
in
let csts = PMap.fold constraints_of g.entries Constraint.empty in
csts, UF.partition uf
@@ -667,16 +729,20 @@ module Make (Point:Point) = struct
(* domain g.entries = kept + removed *)
let constraints_for ~kept g =
(* rmap: partial map from canonical points to kept points *)
+ let add_cst u knd v cst =
+ Constraint.add (Index.repr u g.table, knd, Index.repr v g.table) cst
+ in
+ let kept = Point.Set.fold (fun u accu -> PSet.add (Index.find u g.table) accu) kept PSet.empty in
let rmap, csts = PSet.fold (fun u (rmap,csts) ->
let arcu = repr g u in
if PSet.mem arcu.canon kept then
- let csts = if Point.equal u arcu.canon then csts
- else Constraint.add (u,Eq,arcu.canon) csts
+ let csts = if Index.equal u arcu.canon then csts
+ else add_cst u Eq arcu.canon csts
in
PMap.add arcu.canon arcu.canon rmap, csts
else
match PMap.find arcu.canon rmap with
- | v -> rmap, Constraint.add (u,Eq,v) csts
+ | v -> rmap, add_cst u Eq v csts
| exception Not_found -> PMap.add arcu.canon u rmap, csts)
kept (PMap.empty,Constraint.empty)
in
@@ -687,7 +753,7 @@ module Make (Point:Point) = struct
(match PMap.find v.canon rmap with
| v ->
let d = if strict then Lt else Le in
- let csts = Constraint.add (u,d,v) csts in
+ let csts = add_cst u d v csts in
add_from u csts todo
| exception Not_found ->
(* v is not equal to any kept point *)
@@ -703,18 +769,23 @@ module Make (Point:Point) = struct
arc.ltle csts)
kept csts
- let domain g = PMap.domain g.entries
+ let domain g =
+ let fold u _ accu = Point.Set.add (Index.repr u g.table) accu in
+ PMap.fold fold g.entries Point.Set.empty
let choose p g u =
let exception Found of Point.t in
- let ru = (repr g u).canon in
- if p ru then Some ru
+ let ru = (repr_node g u).canon in
+ let ruv = Index.repr ru g.table in
+ if p ruv then Some ruv
else
try PMap.iter (fun v -> function
| Canonical _ -> () (* we already tried [p ru] *)
| Equiv v' ->
let rv = (repr g v').canon in
- if rv == ru && p v then raise (Found v)
+ if rv == ru then
+ let v = Index.repr v g.table in
+ if p v then raise (Found v)
(* NB: we could also try [p v'] but it will come up in the
rest of the iteration regardless. *)
) g.entries; None
@@ -724,10 +795,16 @@ module Make (Point:Point) = struct
type repr = node Point.Map.t
let repr g =
- let map n = match n with
- | Canonical n -> Node n.ltle
- | Equiv u -> Alias u
+ let fold u n accu =
+ let n = match n with
+ | Canonical n ->
+ let fold u lt accu = Point.Map.add (Index.repr u g.table) lt accu in
+ let ltle = PMap.fold fold n.ltle Point.Map.empty in
+ Node ltle
+ | Equiv u -> Alias (Index.repr u g.table)
+ in
+ Point.Map.add (Index.repr u g.table) n accu
in
- Point.Map.map map g.entries
+ PMap.fold fold g.entries Point.Map.empty
end
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index cc1fa647f9..ee7dab92bc 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -173,3 +173,9 @@ let create ~name ~category ?(default=Enabled) pp =
| Disabled -> ()
| AsError -> CErrors.user_err ?loc (pp x)
| Enabled -> Feedback.msg_warning ?loc (pp x)
+
+(* Remark: [warn] does not need to start with a comma, but if present
+ it won't hurt (",," is normalized into ","). *)
+let with_warn warn (f:'b -> 'a) x =
+ let s = get_flags () in
+ Util.try_finally (fun x -> set_flags (s^","^warn);f x) x set_flags s
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
index ded1f9be3b..b63eed09d0 100644
--- a/lib/cWarnings.mli
+++ b/lib/cWarnings.mli
@@ -19,3 +19,10 @@ val set_flags : string -> unit
(** Cleans up a user provided warnings status string, e.g. removing unknown
warnings (in which case a warning is emitted) or subsumed warnings . *)
val normalize_flags_string : string -> string
+
+(** [with_warn "-xxx,+yyy..." f x] calls [f x] after setting the
+ warnings as specified in the string (keeping other previously set
+ warnings), and restores current warnings after [f()] returns or
+ raises an exception. If both f and restoring the warnings raise
+ exceptions, the latter is raised. *)
+val with_warn: string -> ('b -> 'a) -> 'b -> 'a
diff --git a/lib/control.ml b/lib/control.ml
index 7da95ff3dd..ea94bda064 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -30,11 +30,12 @@ let check_for_interrupt () =
(** This function does not work on windows, sigh... *)
let unix_timeout n f x =
+ let open Unix in
let timeout_handler _ = raise Timeout in
let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
- let _ = Unix.alarm n in
+ let _ = setitimer ITIMER_REAL {it_interval = 0.; it_value = n} in
let restore_timeout () =
- let _ = Unix.alarm 0 in
+ let _ = setitimer ITIMER_REAL { it_interval = 0.; it_value = 0. } in
Sys.set_signal Sys.sigalrm psh
in
try
@@ -52,7 +53,7 @@ let windows_timeout n f x =
let thread init =
while not !killed do
let cur = Unix.gettimeofday () in
- if float_of_int n <= cur -. init then begin
+ if n <= cur -. init then begin
interrupt := true;
exited := true;
Thread.exit ()
@@ -68,7 +69,7 @@ let windows_timeout n f x =
let cur = Unix.gettimeofday () in
(* The thread did not interrupt, but the computation took longer than
expected. *)
- let () = if float_of_int n <= cur -. init then begin
+ let () = if n <= cur -. init then begin
exited := true;
raise Sys.Break
end in
@@ -83,7 +84,7 @@ let windows_timeout n f x =
let () = killed := true in
Exninfo.iraise e
-type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> 'b option }
+type timeout = { timeout : 'a 'b. float -> ('a -> 'b) -> 'a -> 'b option }
let timeout_fun = match Sys.os_type with
| "Unix" | "Cygwin" -> { timeout = unix_timeout }
diff --git a/lib/control.mli b/lib/control.mli
index 9465d8f0d5..f992d8e8d0 100644
--- a/lib/control.mli
+++ b/lib/control.mli
@@ -24,13 +24,13 @@ 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 -> ('a -> 'b) -> 'a -> 'b option
+val timeout : float -> ('a -> 'b) -> 'a -> 'b option
(** [timeout n f x] tries to compute [Some (f x)], and if it fails to do so
before [n] seconds, returns [None] instead. *)
(** Set a particular timeout function; warning, this is an internal
API and it is scheduled to go away. *)
-type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> 'b option }
+type timeout = { timeout : 'a 'b. float -> ('a -> 'b) -> 'a -> 'b option }
val set_timeout : timeout -> unit
(** [protect_sigalrm f x] computes [f x], but if SIGALRM is received during that
diff --git a/lib/stateid.ml b/lib/stateid.ml
index a1328f156c..2a41cb7866 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -45,3 +45,6 @@ type ('a,'b) request = {
name : string
}
+let is_valid_ref = ref (fun ~doc:_ (_ : t) -> true)
+let is_valid ~doc id = !is_valid_ref ~doc id
+let set_is_valid f = is_valid_ref := f
diff --git a/lib/stateid.mli b/lib/stateid.mli
index 9b2de9c894..00acc962a2 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -42,3 +42,10 @@ type ('a,'b) request = {
name : string
}
+(* Asks the document manager if the given state is valid (or belongs to an
+ old version of the document) *)
+val is_valid : doc:int -> t -> bool
+
+(* By default [is_valid] always answers true, but a document manager supporting
+ undo operations like the STM can override this. *)
+val set_is_valid : (doc:int -> t -> bool) -> unit
diff --git a/lib/util.ml b/lib/util.ml
index 87cc30e557..e8aa0f3e48 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -135,6 +135,13 @@ type 'a delayed = unit -> 'a
let delayed_force f = f ()
+(* finalize - Credit X.Leroy, D.Remy. *)
+let try_finally f x finally y =
+ let res = try f x with exn -> finally y; raise exn in
+ finally y;
+ res
+
+
(* Misc *)
type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
diff --git a/lib/util.mli b/lib/util.mli
index fe34525671..aefb015c38 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -112,6 +112,15 @@ type 'a delayed = unit -> 'a
val delayed_force : 'a delayed -> 'a
+(** [try_finally f x g y] applies the main code [f] to [x] and
+ returns the result after having applied the finalization
+ code [g] to [y]. If the main code raises the exception
+ [exn], the finalization code is executed and [exn] is raised.
+ If the finalization code itself fails, the exception
+ returned is always the one from the finalization code.
+ Credit X.Leroy, D.Remy. *)
+val try_finally: ('a -> 'b) -> 'a -> ('c -> unit) -> 'c -> 'b
+
(** {6 Enriched exceptions} *)
type iexn = Exninfo.iexn
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 15:02:19 +0000