diff options
| author | Pierre-Marie Pédrot | 2018-07-19 15:05:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-05 19:11:40 +0200 |
| commit | 943da5e6fb2412a63d1ea67dfeee635b0b5001f4 (patch) | |
| tree | d93adfe64b62d8f667703dbfe77efa5ed836c57c /kernel/nativevalues.ml | |
| parent | 579f30a53809f9cf73aa3d7c69960b50fc51c7fc (diff) | |
Use more efficient accu check for cofix unfolding in native compilation.
Diffstat (limited to 'kernel/nativevalues.ml')
| -rw-r--r-- | kernel/nativevalues.ml | 28 |
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 |
