fixes

Author: c-cube

dune-project

@@ -19,7 +19,7 @@
     sqlite3)
   (depends
     (containers (and (>= 3.3) (< 4.0)))
-    (pp_loc (and (>= 1.0) (< 2.0)))
+    (pp_loc (and (>= 2.0) (< 3.0)))
     (iter (>= 1.0))
     (ocaml (>= 4.08.0))
     sha
@@ -58,7 +58,6 @@
   (synopsis "Trustee-powered interactive theorem prover")
   (depends
     (containers (and (>= 3.0) (< 4.0)))
-    containers-thread
     logs
     cmdliner
     (ocaml (>= 4.08.0))

src/itp/dune

@@ -2,5 +2,5 @@
  (name trustee_itp)
  (public_name trustee-itp)
  (flags :standard -open Trustee_core.Sigs)
- (libraries trustee.core trustee.syntax pp_loc containers containers-thread
+ (libraries trustee.core trustee.syntax pp_loc containers
    threads.posix logs))

src/itp/lock.ml

@@ -0,0 +1,81 @@
+type 'a t = {
+  mutex: Mutex.t;
+  mutable content: 'a;
+}
+
+let create content = { mutex = Mutex.create (); content }
+
+let with_lock l f =
+  Mutex.lock l.mutex;
+  try
+    let x = f l.content in
+    Mutex.unlock l.mutex;
+    x
+  with exn ->
+    let bt = Printexc.get_raw_backtrace () in
+    (match Mutex.unlock l.mutex with
+    | () -> Printexc.raise_with_backtrace exn bt
+    | exception _ ->
+      (* this should only happen if [f …] switched thread *)
+      Printf.eprintf "mutex.unlock failed during `with_lock` cleanup\n%!";
+      Printexc.raise_with_backtrace (Fun.Finally_raised exn) bt)
+
+let mutex l = l.mutex
+let update l f = with_lock l (fun x -> l.content <- f x)
+
+let update_map l f =
+  with_lock l (fun x ->
+      let x', y = f x in
+      l.content <- x';
+      y)
+
+let get l =
+  Mutex.lock l.mutex;
+  let x = l.content in
+  Mutex.unlock l.mutex;
+  x
+
+let set l x =
+  Mutex.lock l.mutex;
+  l.content <- x;
+  Mutex.unlock l.mutex
+
+let exchange l x =
+  Mutex.lock l.mutex;
+  let old = l.content in
+  l.content <- x;
+  Mutex.unlock l.mutex;
+  old
+
+module LockRef = struct
+  type nonrec 'a t = {
+    l: 'a ref;
+    mutable usable: bool;
+  }
+
+  let as_ref self = self.l
+  let get self = !(self.l)
+
+  let set self x =
+    assert self.usable;
+    self.l := x
+end
+
+let with_lock_as_ref l f =
+  Mutex.lock l.mutex;
+  let lref = { LockRef.l = ref l.content; usable = true } in
+  try
+    let x = f lref in
+    l.content <- !(lref.l);
+    lref.usable <- false;
+    Mutex.unlock l.mutex;
+    x
+  with e ->
+    l.content <- !(lref.l);
+    lref.usable <- false;
+    Mutex.unlock l.mutex;
+    raise e
+
+let pp ppx out self =
+  let x = get self in
+  Fmt.fprintf out "(@[lock@ %a@])" ppx x

src/itp/lock.mli

@@ -0,0 +1,50 @@
+(** Value protected by a mutex *)
+
+type 'a t
+(** A value surrounded with a lock *)
+
+val create : 'a -> 'a t
+(** Create a new protected value. *)
+
+val with_lock : 'a t -> ('a -> 'b) -> 'b
+(** [with_lock l f] runs [f x] where [x] is the value protected with the lock
+    [l], in a critical section. If [f x] fails, [with_lock l f] fails too but
+    the lock is released. *)
+
+val update : 'a t -> ('a -> 'a) -> unit
+(** [update l f] replaces the content [x] of [l] with [f x], atomically. *)
+
+val update_map : 'a t -> ('a -> 'a * 'b) -> 'b
+(** [update_map l f] computes [x', y = f (get l)], then puts [x'] in [l] and
+    returns [y]. *)
+
+val mutex : _ t -> Mutex.t
+(** Underlying mutex. *)
+
+val get : 'a t -> 'a
+(** Atomically get the value in the lock. The value that is returned isn't
+    protected! *)
+
+val set : 'a t -> 'a -> unit
+(** Atomically set the value. *)
+
+val exchange : 'a t -> 'a -> 'a
+(** [exchange lock x] atomically sets [lock := x] and returns the previous value
+*)
+
+(** Type allowing to manipulate the lock as a reference when one is holding it.
+*)
+module LockRef : sig
+  type 'a t
+
+  val as_ref : 'a t -> 'a ref
+  val get : 'a t -> 'a
+  val set : 'a t -> 'a -> unit
+end
+
+val with_lock_as_ref : 'a t -> ('a LockRef.t -> 'b) -> 'b
+(** [with_lock_as_ref l f] calls [f] with a reference-like object that allows to
+    manipulate the value of [l] safely. The object passed to [f] must not escape
+    the function call. *)
+
+val pp : 'a Fmt.printer -> 'a t Fmt.printer

src/loc/local_loc.ml

@@ -88,20 +88,21 @@ let positions ~ctx self =
   let off1, off2 = offsets self in
   pos_of_offset ~ctx off1, pos_of_offset ~ctx off2
 
-let tr_position ~ctx ~left ~offset : Lexing.position =
+let tr_position ~ctx ~left ~offset : Pp_loc.Position.t =
   let line, col = tr_offset ctx offset in
-  {
-    Lexing.pos_fname = ctx.filename;
-    pos_lnum = line;
-    pos_cnum =
-      (offset
-      +
-      if left then
-        0
-      else
-        1);
-    pos_bol = offset - col;
-  }
+  Pp_loc.Position.of_lexing
+  @@ {
+       Lexing.pos_fname = ctx.filename;
+       pos_lnum = line;
+       pos_cnum =
+         (offset
+         +
+         if left then
+           0
+         else
+           1);
+       pos_bol = offset - col;
+     }
 
 let line_cols_ ~ctx self =
   let off1, off2 = offsets self in

src/loc/local_loc.mli

@@ -22,7 +22,7 @@ val make : ctx:ctx -> off1:int -> off2:int -> t
 val make_pos : ctx:ctx -> Position.t -> Position.t -> t
 val of_lexbuf : ctx:ctx -> Lexing.lexbuf -> t
 val of_lex_pos : ctx:ctx -> Lexing.position -> Lexing.position -> t
-val tr_position : ctx:ctx -> left:bool -> offset:int -> Lexing.position
+val tr_position : ctx:ctx -> left:bool -> offset:int -> Pp_loc.Position.t
 val offset_of_pos : ctx:ctx -> Position.t -> int
 val pos_of_offset : ctx:ctx -> int -> Position.t
 val offsets : t -> int * int

trustee-itp.opam

@@ -9,7 +9,6 @@ bug-reports: "https://github.com/c-cube/trustee/issues"
 depends: [
   "dune" {>= "2.0"}
   "containers" {>= "3.0" & < "4.0"}
-  "containers-thread"
   "logs"
   "cmdliner"
   "ocaml" {>= "4.08.0"}

trustee.opam

@@ -11,7 +11,7 @@ bug-reports: "https://github.com/c-cube/trustee/issues"
 depends: [
   "dune" {>= "2.0"}
   "containers" {>= "3.3" & < "4.0"}
-  "pp_loc" {>= "1.0" & < "2.0"}
+  "pp_loc" {>= "2.0" & < "3.0"}
   "iter" {>= "1.0"}
   "ocaml" {>= "4.08.0"}
   "sha"