Use r.(p) syntax to print primitive projections.

There is no way today to distinguish primitive projections from
compatibility constants, at least in the case of a record without
parameters.

We remedy to this by always using the r.(p) syntax when printing
primitive projections, even with Set Printing All.

The input syntax r.(p) is still elaborated to GApp, so that we can preserve
the compatibility layer. Hopefully we can make up a plan to get rid of that
layer, but it will require fixing a few problems.

5 files changed, 27 insertions, 9 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 23993243f..754e88139 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -581,12 +581,7 @@ and detype_r d flags avoid env sigma t =
     | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u)
     | Proj (p,c) ->
       let noparams () = 
-	let pb = Environ.lookup_projection p (snd env) in
-	let pars = pb.Declarations.proj_npars in
-	let hole = DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in
-	let args = List.make pars hole in
- 	  GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None),
-		(args @ [detype d flags avoid env sigma c]))
+    GProj (p, detype d flags avoid env sigma c)
       in
       if fst flags || !Flags.in_debugger || !Flags.in_toplevel then
 	try noparams ()
@@ -1002,6 +997,13 @@ let rec subst_glob_constr subst = DAst.map (function
       let r1' = subst_glob_constr subst r1 in
       let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in
       if r1' == r1 && k' == k then raw else GCast (r1',k')
+
+  | GProj (p,c) as raw ->
+    let kn = Projection.constant p in
+    let b = Projection.unfolded p in
+    let kn' = subst_constant subst kn in
+    let c' = subst_glob_constr subst c in
+    if kn' == kn && c' == c then raw else GProj(Projection.make kn' b, c')
   )
 
 (* Utilities to transform kernel cases to simple pattern-matching problem *)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 093f1f0b6..a21137a05 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -133,8 +133,10 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
     Miscops.intro_pattern_naming_eq nam1 nam2
   | GCast (c1, t1), GCast (c2, t2) ->
     f c1 c2 && cast_type_eq f t1 t2
+  | GProj (p1, t1), GProj (p2, t2) ->
+    Projection.equal p1 p2 && f t1 t2
   | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ |
-     GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _), _ -> false
+     GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ | GProj _), _ -> false
 
 let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c
 
@@ -180,6 +182,8 @@ let map_glob_constr_left_to_right f = DAst.map (function
       let comp1 = f c in
       let comp2 = Miscops.map_cast_type f k in
       GCast (comp1,comp2)
+  | GProj (p,c) ->
+    GProj (p, f c)
   | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x
   )
 
@@ -212,6 +216,8 @@ let fold_glob_constr f acc = DAst.with_val (function
     let acc = match k with
       | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in
     f acc c
+  | GProj(_,c) ->
+    f acc c
   | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
   )
 
@@ -253,6 +259,8 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
     let acc = match k with
       | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in
     f v acc c
+  | GProj(_,c) ->
+    f v acc c
   | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc))
 
 let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 41e09004c..1bec4a6f1 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -137,8 +137,7 @@ let rec head_pattern_bound t =
     | PCase (_,p,c,br) -> head_pattern_bound c
     | PRef r         -> r
     | PVar id        -> VarRef id
-    | PProj (p,c)    -> ConstRef (Projection.constant p)
-    | PEvar _ | PRel _ | PMeta _ | PSoApp _  | PSort _ | PFix _
+    | PEvar _ | PRel _ | PMeta _ | PSoApp _  | PSort _ | PFix _ | PProj _
 	-> raise BoundPattern
     (* Perhaps they were arguments, but we don't beta-reduce *)
     | PLambda _ -> raise BoundPattern
@@ -446,6 +445,9 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
 	 one non-trivial branch. These facts are used in [Constrextern]. *)
       PCase (info, pred, pat_of_raw metas vars c, brs)
 
+  | GProj(p,c) ->
+    PProj(p, pat_of_raw metas vars c)
+
   | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ ->
       err ?loc (Pp.str "Non supported pattern."))
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b930c5db8..33dd1344f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -738,6 +738,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     let j = pretype_sort ?loc evdref s in
       inh_conv_coerce_to_tycon ?loc env evdref j tycon
 
+  | GProj (p, c) ->
+    (* TODO: once GProj is used as an input syntax, use bidirectional typing here *)
+    let cj = pretype empty_tycon env evdref lvar c in
+    judge_of_projection env.ExtraEnv.env !evdref p cj
+
   | GApp (f,args) ->
     let fj = pretype empty_tycon env evdref lvar f in
     let floc = loc_of_glob_constr f in
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 9f084ae8d..153a48a71 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -53,3 +53,4 @@ val judge_of_abstraction : Environ.env -> Name.t ->
   unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment
 val judge_of_product : Environ.env -> Name.t ->
   unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment
+val judge_of_projection : env -> evar_map -> projection -> unsafe_judgment -> unsafe_judgment