Merge PR #8097: Use more efficient accu check for cofix unfolding in native compilation.

2 files changed, 21 insertions, 19 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index ad10c86945..eed25a4ca4 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -632,6 +632,14 @@ let mkMLapp f args =
     | MLapp(f,args') -> MLapp(f,Array.append args' args)
     | _ -> MLapp(f,args)
 
+let mkForceCofix prefix ind arg =
+  let name = fresh_lname Anonymous in
+  MLlet (name, arg,
+    MLif (
+      MLisaccu (prefix, ind, MLlocal name),
+      MLapp (MLprimitive Force_cofix, [|MLlocal name|]),
+      MLlocal name))
+
 let empty_params = [||]
 
 let decompose_MLlam c =
@@ -1143,7 +1151,7 @@ let ml_of_instance instance u =
       let arg = ml_of_lam env l a in
       let force =
 	if annot.asw_finite then arg
-	else MLapp(MLprimitive Force_cofix, [|arg|]) in
+        else mkForceCofix annot.asw_prefix annot.asw_ind arg in
       mkMLapp (MLapp (MLglobal cn, fv_args env fvn fvr)) [|force|]
   | Lif(t,bt,bf) -> 
       MLif(ml_of_lam env l t, ml_of_lam env l bt, ml_of_lam env l bf)
@@ -1999,7 +2007,7 @@ let compile_mind mb mind stack =
       let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in
       let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in
       let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in
-      let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in
+      let code = MLlet(cf_uid, mkForceCofix "" ind (MLlocal c_uid), code) in
       let gn = Gproj ("", ind, proj_arg) in
       Glet (gn, mkMLlam [|c_uid|] code) :: acc
     in
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 3bf23f1468..93e74af845 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -154,10 +154,6 @@ let args_of_accu (k:accumulator) =
   let acc = (get_accu k).acc_arg in
   (Obj.magic (Array.of_list acc) : t array)
 
-let is_accu x =
-  let o = Obj.repr x in
-  Obj.is_block o && Int.equal (Obj.tag o) accumulate_tag
-
 let mk_fix_accu rec_pos pos types bodies =
   mk_accu (Afix(types,bodies,rec_pos, pos))
 
@@ -172,19 +168,17 @@ let upd_cofix (cofix :t) (cofix_fun : t) =
   | _ -> assert false
   
 let force_cofix (cofix : t) = 
-  if is_accu cofix then
-    let accu = (Obj.magic cofix : accumulator) in
-    let atom = atom_of_accu accu in
-    match atom with
-    | Acofix(typ,norm,pos,f) ->
-      let args = args_of_accu accu in
-      let f = Array.fold_right (fun arg f -> f arg) args f in
-      let v = f (Obj.magic ()) in
-      set_atom_of_accu accu (Acofixe(typ,norm,pos,v));
-	v
-    | Acofixe(_,_,_,v) -> v 
-    | _ -> cofix
-  else cofix
+  let accu = (Obj.magic cofix : accumulator) in
+  let atom = atom_of_accu accu in
+  match atom with
+  | Acofix(typ,norm,pos,f) ->
+    let args = args_of_accu accu in
+    let f = Array.fold_right (fun arg f -> f arg) args f in
+    let v = f (Obj.magic ()) in
+    set_atom_of_accu accu (Acofixe(typ,norm,pos,v));
+      v
+  | Acofixe(_,_,_,v) -> v
+  | _ -> cofix
 
 let mk_const tag = Obj.magic tag