Merge PR #984: Handling primitive projections in canonical structures.

5 files changed, 89 insertions, 14 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index cb76df4e8a..0f1a508c8d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -176,6 +176,12 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
         let s = ESorts.kind sigma s in
 	lookup_canonical_conversion
 	  (proji, Sort_cs (family_of_sort s)),[]
+      | Proj (p, c) ->
+        let c2 = Globnames.ConstRef (Projection.constant p) in
+        let c = Retyping.expand_projection env sigma p c [] in
+        let _, args = destApp sigma c in
+        let sk2 = Stack.append_app args sk2 in
+        lookup_canonical_conversion (proji, Const_cs c2), sk2
       | _ ->
 	let (c2, _) = Termops.global_of_constr sigma t2 in
 	  lookup_canonical_conversion (proji, Const_cs c2),sk2
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index a23579609a..e970a1db90 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -171,7 +171,7 @@ let keep_true_projections projs kinds =
   let filter (p, (_, b)) = if b then Some p else None in
   List.map_filter filter (List.combine projs kinds)
 
-let cs_pattern_of_constr t =
+let cs_pattern_of_constr env t =
   match kind_of_term t with
       App (f,vargs) ->
 	begin
@@ -180,6 +180,10 @@ let cs_pattern_of_constr t =
 	end
     | Rel n -> Default_cs, Some n, []
     | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b]
+    | Proj (p, c) ->
+      let { Environ.uj_type = ty } = Typeops.infer env c in
+      let _, params = Inductive.find_rectype env ty in
+      Const_cs (ConstRef (Projection.constant p)), None, params @ [c]
     | Sort s -> Sort_cs (family_of_sort s), None, []
     | _ ->
 	begin
@@ -190,7 +194,6 @@ let cs_pattern_of_constr t =
 let warn_projection_no_head_constant =
   CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker"
          (fun (sign,env,t,con,proji_sp) ->
-          let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
           let env = Termops.push_rels_assum sign env in
           let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in
           let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
@@ -207,14 +210,16 @@ let compute_canonical_projections warn (con,ind) =
   let v = (mkConstU (con,u)) in
   let c = Environ.constant_value_in env (con,u) in
   let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in
+  let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in
   let t = EConstr.Unsafe.to_constr t in
-  let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) sign in
+  let lt = List.rev_map snd sign in
   let args = snd (decompose_app t) in
   let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } =
     lookup_structure ind in
   let params, projs = List.chop p args in
   let lpj = keep_true_projections lpj kl in
   let lps = List.combine lpj projs in
+  let nenv = Termops.push_rels_assum sign env in
   let comp =
     List.fold_left
       (fun l (spopt,t) -> (* comp=components *)
@@ -222,7 +227,7 @@ let compute_canonical_projections warn (con,ind) =
            | Some proji_sp ->
 	       begin
 		 try
-		   let patt, n , args = cs_pattern_of_constr t in
+		   let patt, n , args = cs_pattern_of_constr nenv t in
 		     ((ConstRef proji_sp, patt, t, n, args) :: l)
 		 with Not_found ->
                    if warn then warn_projection_no_head_constant (sign,env,t,con,proji_sp);
@@ -324,15 +329,25 @@ let declare_canonical_structure ref =
 let lookup_canonical_conversion (proj,pat) =
   assoc_pat pat (Refmap.find proj !object_table)
 
+let decompose_projection sigma c args =
+  match EConstr.kind sigma c with
+  | Const (c, u) ->
+     let n = find_projection_nparams (ConstRef c) in
+     (** Check if there is some canonical projection attached to this structure *)
+     let _ = Refmap.find (ConstRef c) !object_table in
+     let arg = Stack.nth args n in
+     arg
+  | Proj (p, c) ->
+     let _ = Refmap.find (ConstRef (Projection.constant p)) !object_table in
+     c
+  | _ -> raise Not_found
+
 let is_open_canonical_projection env sigma (c,args) =
   let open EConstr in
   try
-    let (ref, _) = Termops.global_of_constr sigma c in
-    let n = find_projection_nparams ref in
-    (** Check if there is some canonical projection attached to this structure *)
-    let _ = Refmap.find ref !object_table in
+    let arg = decompose_projection sigma c args in
     try
-      let arg = whd_all env sigma (Stack.nth args n) in
+      let arg = whd_all env sigma arg in
       let hd = match EConstr.kind sigma arg with App (hd, _) -> hd | _ -> arg in
       not (isConstruct sigma hd)
     with Failure _ -> false
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 5480b14af0..8e2333b349 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -65,7 +65,7 @@ type obj_typ = {
   o_TCOMPS : constr list } (** ordered *)
 
 (** Return the form of the component of a canonical structure *)
-val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list
+val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * constr list
 
 val pr_cs_pattern : cs_pattern -> Pp.t
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d52c3932df..e8f7e2bbaf 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -501,6 +501,10 @@ let expand_key ts env sigma = function
     in if EConstr.eq_constr sigma (EConstr.mkProj (p, c)) red then None else Some red
   | None -> None
 
+let isApp_or_Proj sigma c =
+  match kind sigma c with
+  | App _ | Proj _ -> true
+  | _ -> false
   
 type unirec_flags = {
   at_top: bool;
@@ -1020,7 +1024,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 
   and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) =
     let f1 () =
-      if isApp sigma cM then
+      if isApp_or_Proj sigma cM then
 	let f1l1 = whd_nored_state sigma (cM,Stack.empty) in
 	  if is_open_canonical_projection curenv sigma f1l1 then
 	    let f2l2 = whd_nored_state sigma (cN,Stack.empty) in
@@ -1036,7 +1040,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	error_cannot_unify (fst curenvnb) sigma (cM,cN)
       else
 	try f1 () with e when precatchable_exception e ->
-	  if isApp sigma cN then
+	  if isApp_or_Proj sigma cN then
 	    let f2l2 = whd_nored_state sigma (cN, Stack.empty) in
 	      if is_open_canonical_projection curenv sigma f2l2 then
 		let f1l1 = whd_nored_state sigma (cM, Stack.empty) in
diff --git a/test-suite/bugs/closed/5692.v b/test-suite/bugs/closed/5692.v
index 55ef7abe40..4c8d464f19 100644
--- a/test-suite/bugs/closed/5692.v
+++ b/test-suite/bugs/closed/5692.v
@@ -1,9 +1,59 @@
 Set Primitive Projections.
 Require Import ZArith ssreflect.
 
-Module Test3.
+Module Test1.
 
-Set Primitive Projections.
+Structure semigroup := SemiGroup {
+  sg_car :> Type;
+  sg_op : sg_car -> sg_car -> sg_car;
+}.
+
+Structure monoid := Monoid {
+  monoid_car :> Type;
+  monoid_op : monoid_car -> monoid_car -> monoid_car;
+  monoid_unit : monoid_car;
+}.
+
+Coercion monoid_sg (X : monoid) : semigroup :=
+  SemiGroup (monoid_car X) (monoid_op X).
+Canonical Structure monoid_sg.
+
+Parameter X : monoid.
+Parameter x y : X.
+
+Check (sg_op _ x y).
+
+End Test1.
+
+Module Test2.
+
+Structure semigroup := SemiGroup {
+  sg_car :> Type;
+  sg_op : sg_car -> sg_car -> sg_car;
+}.
+
+Structure monoid := Monoid {
+  monoid_car :> Type;
+  monoid_op : monoid_car -> monoid_car -> monoid_car;
+  monoid_unit : monoid_car;
+  monoid_left_id x : monoid_op monoid_unit x = x;
+}.
+
+Coercion monoid_sg (X : monoid) : semigroup :=
+  SemiGroup (monoid_car X) (monoid_op X).
+Canonical Structure monoid_sg.
+
+Canonical Structure nat_sg := SemiGroup nat plus.
+Canonical Structure nat_monoid := Monoid nat plus 0 plus_O_n.
+
+Lemma foo (x : nat) : 0 + x = x.
+Proof.
+apply monoid_left_id.
+Qed.
+
+End Test2.
+
+Module Test3.
 
 Structure semigroup := SemiGroup {
   sg_car :> Type;