diff options
| -rw-r--r-- | kernel/nativecode.ml | 12 | ||||
| -rw-r--r-- | kernel/nativevalues.ml | 28 |
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 |