diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-01-29 10:55:16 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-29 10:55:16 +0100 |
commit | 46b59c60152148c122ee6ac26cddca42ae4f8430 (patch) | |
tree | 8925338d14c56dbd53afbc6c837bb7905f1c5f49 /kernel/nativecode.ml | |
parent | d0e05a1964fb2af093ac2a15a75bb84d342bf1ad (diff) |
[native_compute] Fix evaluation of cofixpoints under primitive projections.
Diffstat (limited to 'kernel/nativecode.ml')
-rw-r--r-- | kernel/nativecode.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index ffe19510a..613b2f2ec 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1919,15 +1919,17 @@ let compile_constant env sigma prefix ~interactive con cb = let asw = { asw_ind = ind; asw_prefix = prefix; asw_ci = ci; asw_reloc = tbl; asw_finite = true } in let c_uid = fresh_lname Anonymous in + let cf_uid = fresh_lname Anonymous in let _, arity = tbl.(0) in let ci_uid = fresh_lname Anonymous in let cargs = Array.init arity (fun i -> if Int.equal i pb.proj_arg then Some ci_uid else None) in let i = push_symbol (SymbConst con) in - let accu = MLapp (MLprimitive Cast_accu, [|MLlocal c_uid|]) in + let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in let accu_br = MLapp (MLprimitive Mk_proj, [|get_const_code i;accu|]) in - let code = MLmatch(asw,MLlocal c_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) 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 gn = Gproj ("",con) in let fargs = Array.init (pb.proj_npars + 1) (fun _ -> fresh_lname Anonymous) in let arg = fargs.(pb.proj_npars) in |