Fix bug 3662 by actually reducing primitive projections in cbv/compute.

3 files changed, 73 insertions, 14 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index d491ded72..4db9cf066 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -59,6 +59,8 @@ type cbv_value =
  *      the subs S, pat is information on the patterns of the Case
  *      (Weak reduction: we propagate the sub only when the selected branch
  *      is determined)
+ *   PROJ(p,pb,stk) means the term is in a primitive projection p, itself in stk.
+ *      pb is the associated projection body
  *
  * Important remark: the APPs should be collapsed:
  *    (APP (l,(APP ...))) forbidden
@@ -176,9 +178,9 @@ let cofixp_reducible flgs _ stk =
 
 (* The main recursive functions
  *
- * Go under applications and cases (pushed in the stack), expand head
- * constants or substitued de Bruijn, and try to make appear a
- * constructor, a lambda or a fixp in the head. If not, it is a value
+ * Go under applications and cases/projections (pushed in the stack), 
+ * expand head constants or substitued de Bruijn, and try to a make a
+ * constructor, a lambda or a fixp appear in the head. If not, it is a value
  * and is completely computed here. The head redexes are NOT reduced:
  * the function returns the pair of a cbv_value and its stack.  *
  * Invariant: if the result of norm_head is CONSTR or (CO)FIXP, it last
@@ -197,9 +199,14 @@ let rec norm_head info env t stack =
   | Cast (ct,_,_) -> norm_head info env ct stack
   
   | Proj (p, c) -> 
+    let p' =
+      if red_set (info_flags info) (fCONST (Projection.constant p)) then
+	Projection.unfold p
+      else p
+    in 
     let pinfo = Environ.lookup_projection p (info_env info) in
-    norm_head info env c (PROJ (p, pinfo, stack))
-
+      norm_head info env c (PROJ (p', pinfo, stack))
+	
   (* constants, axioms
    * the first pattern is CRUCIAL, n=0 happens very often:
    * when reducing closed terms, n is always 0 *)
@@ -257,12 +264,14 @@ and norm_head_ref k info env stack normt =
  * we build a value.
  *)
 and cbv_stack_term info stack env t =
-  match norm_head info env t stack with
-    (* a lambda meets an application -> BETA *)
-    | (LAM (nlams,ctxt,b,env), APP (args, stk))
+  cbv_stack_value info env (norm_head info env t stack)
+
+and cbv_stack_value info env = function
+  (* a lambda meets an application -> BETA *)
+  | (LAM (nlams,ctxt,b,env), APP (args, stk))
       when red_set (info_flags info) fBETA ->
-        let nargs = Array.length args in
-        if nargs == nlams then
+    let nargs = Array.length args in
+      if nargs == nlams then
           cbv_stack_term info stk (subs_cons(args,env)) b
         else if nlams < nargs then
           let env' = subs_cons(Array.sub args 0 nlams, env) in
@@ -296,11 +305,17 @@ and cbv_stack_term info stack env t =
             when red_set (info_flags info) fIOTA ->
                     cbv_stack_term info stk env br.(n-1)
 
+    (* constructor in a Projection -> IOTA *)
+    | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk)))
+        when red_set (info_flags info) fIOTA && Projection.unfolded p ->
+      let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in
+	cbv_stack_value info env (arg, stk)
+
     (* may be reduced later by application *)
     | (FIXP(fix,env,[||]), APP(appl,TOP)) -> FIXP(fix,env,appl)
     | (COFIXP(cofix,env,[||]), APP(appl,TOP)) -> COFIXP(cofix,env,appl)
     | (CONSTR(c,[||]), APP(appl,TOP)) -> CONSTR(c,appl)
-
+      
     (* definitely a value *)
     | (head,stk) -> mkSTACK(head, stk)
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index a2584571d..ab04a9045 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1070,9 +1070,6 @@ let is_projection env = function
  * at the occurrences of occ_list. If occ_list is empty, unfold all occurences.
  * Performs a betaiota reduction after unfolding. *)
 let unfoldoccs env sigma (occs,name) c =
-  if is_projection env name then
-    error ("Cannot unfold primitive projection " ^ string_of_evaluable_ref env name)
-  else
   let unfo nowhere_except_in locs =
     let (nbocc,uc) = substlin env sigma name 1 (nowhere_except_in,locs) c in
     if Int.equal nbocc 1 then
diff --git a/test-suite/bugs/closed/3662.v b/test-suite/bugs/closed/3662.v
new file mode 100644
index 000000000..0de92b131
--- /dev/null
+++ b/test-suite/bugs/closed/3662.v
@@ -0,0 +1,47 @@
+Set Primitive Projections.
+Set Implicit Arguments.
+Set Record Elimination Schemes.
+Record prod A B := pair { fst : A ; snd : B }.
+Definition f : Set -> Type := fun x => x.
+
+Goal (fst (pair (fun x => x + 1) nat) 0) = 0.
+compute.
+Undo.
+cbv.
+Undo.
+Opaque fst.
+cbn.
+Transparent fst.
+cbn.
+Undo.
+simpl.
+Undo.
+Abort.
+
+Goal f (fst (pair nat nat)) = nat.
+compute.
+  match goal with
+    | [ |- fst ?x = nat ] => fail 1 "compute failed"
+    | [ |- nat = nat ] => idtac
+  end.
+  reflexivity.
+Defined.
+
+Goal fst (pair nat nat) = nat.
+  unfold fst. 
+  match goal with
+    | [ |- fst ?x = nat ] => fail 1 "compute failed"
+    | [ |- nat = nat ] => idtac
+  end.
+  reflexivity.
+Defined.
+
+Lemma eta A B : forall x : prod A B, x = pair (fst x) (snd x). reflexivity. Qed.
+
+Goal forall x : prod nat nat, fst x = 0.
+  intros. unfold fst. rewrite (eta x). cbv iota. cbv delta. cbv iota.
+  cbv delta. 
+  match goal with
+    | [ |- fst ?x = 0 ] => idtac
+  end.
+Abort.
\ No newline at end of file