aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativevalues.ml
diff options
context:
space:
mode:
authorMaxime Dénès2018-09-12 17:25:46 +0200
committerMaxime Dénès2018-09-12 17:25:46 +0200
commit26936e66c7c16f72fd1a7978505c95af9899ddc0 (patch)
treeb82a055010d31fd79c7f3b6c69d08011d7b813c0 /kernel/nativevalues.ml
parent60103f4af881485c0f905ebcb6710b31744466d0 (diff)
parent943da5e6fb2412a63d1ea67dfeee635b0b5001f4 (diff)
Merge PR #8097: Use more efficient accu check for cofix unfolding in native compilation.
Diffstat (limited to 'kernel/nativevalues.ml')
-rw-r--r--kernel/nativevalues.ml28
1 files changed, 11 insertions, 17 deletions
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