Do not match on record types with mutable fields in function arguments.

This tends to confuse the OCaml compiler, for good reasons. Indeed, if
there are mutable fields, the generated code cannot wait for the function
to be fully applied. It needs to recover the value of the mutable fields
as early as possible, and thus to create a closure.

Example:

    let foo {bar} x = ...

is compiled as

    let foo y = match y with {bar} -> fun x -> ...

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;