From a51cce369b9c634a93120092d4c7685a242d55b1 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sat, 4 Jul 2015 14:22:08 +0200
Subject: Fix handling of primitive projections in VM.

I'm pushing this patch now because the previous treatment of such projections
in the VM was already unsound. It should however be carefully reviewed.
---
 pretyping/inductiveops.ml  | 9 +++++++++
 pretyping/inductiveops.mli | 2 ++
 pretyping/pretyping.mllib  | 2 +-
 pretyping/retyping.ml      | 9 ++-------
 pretyping/vnorm.ml         | 4 ++++
 5 files changed, 18 insertions(+), 8 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index dfdc24d480..90aa8000a8 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -584,6 +584,15 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
         env evdref scl ar.template_level (ctx,ar.template_param_levels) in
       !evdref, mkArity (List.rev ctx,scl)
 
+let type_of_projection_knowing_arg env sigma p c ty =
+  let IndType(pars,realargs) =
+    try find_rectype env sigma ty
+    with Not_found ->
+      raise (Invalid_argument "type_of_projection_knowing_arg_type: not an inductive type")
+  in
+  let (_,u), pars = dest_ind_family pars in
+  substl (c :: List.rev pars) (Typeops.type_of_projection env (p,u))
+
 (***********************************************)
 (* Guard condition *)
 
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 7959759a3f..757599a3ce 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -126,6 +126,8 @@ val allowed_sorts : env -> inductive -> sorts_family list
 (** Primitive projections *)
 val projection_nparams : projection -> int
 val projection_nparams_env : env -> projection -> int
+val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
+  constr -> types -> types
 
 (** Extract information from an inductive family *)
 
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 25d17c7c9f..a644e3d107 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -3,8 +3,8 @@ Termops
 Namegen
 Evd
 Reductionops
-Vnorm
 Inductiveops
+Vnorm
 Arguments_renaming
 Nativenorm
 Retyping
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index a56861c683..743bc3b19b 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -127,13 +127,8 @@ let retype ?(polyprop=true) sigma =
         strip_outer_cast
           (subst_type env sigma (type_of env f) (Array.to_list args))
     | Proj (p,c) -> 
-       let Inductiveops.IndType(pars,realargs) =
-	 let ty = type_of env c in
-           try Inductiveops.find_rectype env sigma ty
-           with Not_found -> retype_error BadRecursiveType
-       in
-       let (_,u), pars = dest_ind_family pars in
-	 substl (c :: List.rev pars) (Typeops.type_of_projection env (p,u))
+       let ty = type_of env c in
+       Inductiveops.type_of_projection_knowing_arg env sigma p c ty
     | Cast (c,_, t) -> t
     | Sort _ | Prod _ -> mkSort (sort_of env cstr)
 
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 8198db1b8a..af640d7f34 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -216,6 +216,10 @@ and nf_stk env c t stk  =
       let tcase = build_case_type dep p realargs c in
       let ci = case_info sw in
       nf_stk env (mkCase(ci, p, c, branchs)) tcase stk
+  | Zproj p :: stk ->
+     let p' = Projection.make p true in
+     let ty = Inductiveops.type_of_projection_knowing_arg env Evd.empty p' c t in
+     nf_stk env (mkProj(p',c)) ty stk
 
 and nf_predicate env ind mip params v pT =
   match whd_val v, kind_of_term pT with
-- 
cgit v1.2.3