Merge PR #13978: Do not match on record types with mutable fields in function arguments.

Reviewed-by: gares

4 files changed, 28 insertions, 22 deletions

diff --git a/lib/cProfile.ml b/lib/cProfile.ml
index a4f2da7080..b68d35d2d4 100644
--- a/lib/cProfile.ml
+++ b/lib/cProfile.ml
@@ -285,7 +285,7 @@ let format_profile (table, outside, total) =
   Printf.printf
     "%-23s  %9s %9s %10s %10s %10s\n"
     "Function name" "Own time" "Tot. time" "Own alloc" "Tot. alloc" "Calls ";
-  let l = List.sort (fun (_,{tottime=p}) (_,{tottime=p'}) -> p' - p) table in
+  let l = List.sort (fun p p' -> (snd p').tottime - (snd p).tottime) table in
   List.iter (fun (name,e) ->
     Printf.printf
       "%-23s %9.2f %9.2f %10.0f %10.0f %6d %6d\n"
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index da4a50b674..cfdaac710b 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -217,13 +217,13 @@ module Mlenv = struct
 
   (* Adding a type with no [Tvar], hence no generalization needed. *)
 
-  let push_type {env=e;free=f} t =
-    { env = (0,t) :: e; free = find_free f t}
+  let push_type mle t =
+    { env = (0,t) :: mle.env; free = find_free mle.free t}
 
   (* Adding a type with no [Tvar] nor [Tmeta]. *)
 
-  let push_std_type {env=e;free=f} t =
-    { env = (0,t) :: e; free = f}
+  let push_std_type mle t =
+    { env = (0,t) :: mle.env; free = mle.free}
 
 end
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 5ed6adbd63..9480bbdc2e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2565,8 +2565,8 @@ let get_allow_nested_proofs =
     ~value:false
 
 (** [process_transaction] adds a node in the document *)
-let process_transaction ~doc ?(newtip=Stateid.fresh ())
-  ({ verbose; expr } as x) c =
+let process_transaction ~doc ?(newtip=Stateid.fresh ()) x c =
+  let { verbose; expr } = x in
   stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x);
   let vcs = VCS.backup () in
   try
diff --git a/stm/tQueue.ml b/stm/tQueue.ml
index e17c3a2f88..2aaca85582 100644
--- a/stm/tQueue.ml
+++ b/stm/tQueue.ml
@@ -27,21 +27,23 @@ end = struct
   let create () = ref ([],sort_timestamp)
   let is_empty t = fst !t = []
   let exists p t = List.exists (fun (_,x) -> p x) (fst !t)
-  let pop ?(picky=(fun _ -> true)) ({ contents = (l, rel) } as t) =
+  let pop ?(picky=(fun _ -> true)) t =
+    let (l, rel) = !t in
     let rec aux acc = function
       | [] -> raise Queue.Empty
       | (_,x) :: xs when picky x -> t := (List.rev acc @ xs, rel); x
       | (_,x) as hd :: xs -> aux (hd :: acc) xs in
     aux [] l
-  let push ({ contents = (xs, rel) } as t) x =
+  let push t x =
+    let (xs, rel) = !t in
     incr age;
     (* re-roting the whole list is not the most efficient way... *)
     t := (List.sort rel (xs @ [!age,x]), rel)
-  let clear ({ contents = (l, rel) } as t) = t := ([], rel)
-  let set_rel rel ({ contents = (xs, _) } as t) =
+  let clear t = t := ([], snd !t)
+  let set_rel rel t =
     let rel (_,x) (_,y) = rel x y in
-    t := (List.sort rel xs, rel)
-  let length ({ contents = (l, _) }) = List.length l
+    t := (List.sort rel (fst !t), rel)
+  let length t = List.length (fst !t)
 end
 
 type 'a t = {
@@ -64,9 +66,8 @@ let create () = {
   release = false;
 }
 
-let pop ?(picky=(fun _ -> true)) ?(destroy=ref false)
-  ({ queue = q; lock = m; cond = c; cond_waiting = cn } as tq)
-=
+let pop ?(picky=(fun _ -> true)) ?(destroy=ref false) tq =
+  let { queue = q; lock = m; cond = c; cond_waiting = cn } = tq in
   Mutex.lock m;
   if tq.release then (Mutex.unlock m; raise BeingDestroyed);
   while not (PriorityQueue.exists picky q || !destroy) do
@@ -83,12 +84,14 @@ let pop ?(picky=(fun _ -> true)) ?(destroy=ref false)
   Mutex.unlock m;
   x
 
-let broadcast { lock = m; cond = c } =
+let broadcast tq =
+  let { lock = m; cond = c } = tq in
   Mutex.lock m;
   Condition.broadcast c;
   Mutex.unlock m
 
-let push { queue = q; lock = m; cond = c; release } x =
+let push tq x =
+  let { queue = q; lock = m; cond = c; release } = tq in
   if release then CErrors.anomaly(Pp.str
     "TQueue.push while being destroyed! Only 1 producer/destroyer allowed.");
   Mutex.lock m;
@@ -96,18 +99,21 @@ let push { queue = q; lock = m; cond = c; release } x =
   Condition.broadcast c;
   Mutex.unlock m
 
-let length { queue = q; lock = m } =
+let length tq =
+  let { queue = q; lock = m } = tq in
   Mutex.lock m;
   let n = PriorityQueue.length q in
   Mutex.unlock m;
   n
 
-let clear { queue = q; lock = m; cond = c } =
+let clear tq =
+  let { queue = q; lock = m; cond = c } = tq in
   Mutex.lock m;
   PriorityQueue.clear q;
   Mutex.unlock m
 
-let clear_saving { queue = q; lock = m; cond = c } f =
+let clear_saving tq f =
+  let { queue = q; lock = m; cond = c } = tq in
   Mutex.lock m;
   let saved = ref [] in
   while not (PriorityQueue.is_empty q) do
@@ -119,7 +125,7 @@ let clear_saving { queue = q; lock = m; cond = c } f =
   Mutex.unlock m;
   List.rev !saved
 
-let is_empty { queue = q } = PriorityQueue.is_empty q
+let is_empty tq = PriorityQueue.is_empty tq.queue
 
 let destroy tq =
   tq.release <- true;