diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-30 10:01:50 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-30 10:01:50 +0100 |
| commit | 879ebad4d0b39fda275a72ba44c1f4dfbb9282e5 (patch) | |
| tree | b2775e675b9b82acd5fd8a34b99b7b33af782d91 | |
| parent | ae2429e6cf0e4faa0e57bd3b1393efc3b532920a (diff) | |
| parent | 4be607ec6c0b89e85566b4a6952bdf41e40fae7b (diff) | |
Merge PR #6666: Fix reduction of primitive projections on coinductive records for cbv and native_compute
| -rw-r--r-- | kernel/nativecode.ml | 6 | ||||
| -rw-r--r-- | pretyping/cbv.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5286.v | 9 |
3 files changed, 14 insertions, 3 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 diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 192eca63b..e42576d95 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -171,7 +171,7 @@ let fixp_reducible flgs ((reci,i),_) stk = let cofixp_reducible flgs _ stk = if red_set flgs fCOFIX then match stk with - | (CASE _ | APP(_,CASE _)) -> true + | (CASE _ | PROJ _ | APP(_,CASE _) | APP(_,PROJ _)) -> true | _ -> false else false diff --git a/test-suite/bugs/closed/5286.v b/test-suite/bugs/closed/5286.v new file mode 100644 index 000000000..98d4e5c96 --- /dev/null +++ b/test-suite/bugs/closed/5286.v @@ -0,0 +1,9 @@ +Set Primitive Projections. + +CoInductive R := mkR { p : unit }. + +CoFixpoint foo := mkR tt. + +Check (eq_refl tt : p foo = tt). +Check (eq_refl tt <: p foo = tt). +Check (eq_refl tt <<: p foo = tt). |