Parsing and printing of primitive projections, fix buggy behavior when

implicits do not allow to parse as an application and cleanup code.

4 files changed, 100 insertions, 76 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 284bba1b7..ad159bb60 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -437,23 +437,29 @@ let occur_name na aty =
     | Name id -> occur_var_constr_expr id aty
     | Anonymous -> false
 
-let is_projection primproj nargs cf =
-  if primproj then Some 1
-  else 
-    match cf with
-    | Some r when not !in_debugger && not !Flags.raw_print && !print_projections ->
-      (try
-	let n = Recordops.find_projection_nparams r + 1 in
-	  if n <= nargs then
-	  (* For primitive projections, r.(p) and r.(@p) are reserved to the 
-	     non-eta-expanded version of the constant, we disallow printing 
-	     of the eta-expanded projection as a projection *)
-	    if Environ.is_projection (destConstRef r) (Global.env()) then None
-	    else Some n 
-	  else None
-       with Not_found -> None)
-    | _ -> None
-
+let is_projection primprojapp nargs cf =
+  let env = Global.env () in
+    match primprojapp with 
+    | Some r ->
+      let pb = Environ.lookup_projection r env in
+	Some pb.Declarations.proj_npars, Some 1
+    | None ->
+      match cf with
+      | Some (ConstRef p) when Environ.is_projection p (Global.env()) ->
+	let pb = Environ.lookup_projection p env in
+        (* For primitive projections, r.(p) and r.(@p) are reserved to the 
+	   non-eta-expanded version of the constant, we disallow printing 
+	   of the eta-expanded projection as a projection *)
+	  Some pb.Declarations.proj_npars, None
+      | Some r when not !in_debugger && not !Flags.raw_print && !print_projections ->
+	(try
+	   let n = Recordops.find_projection_nparams r + 1 in
+	     if n <= nargs then None, None
+	     else None, Some n
+	 with Not_found -> None, None)
+      | _ -> None, None
+      
+	
 let is_hole = function CHole _ -> true | _ -> false
 
 let is_significant_implicit a =
@@ -464,9 +470,18 @@ let is_needed_for_correct_partial_application tail imp =
 
 exception Expl
 
+let params_implicit n impl = 
+  let rec aux n impl =
+    if n == 0 then true
+    else match impl with
+    | [] -> false
+    | imp :: impl when is_status_implicit imp -> aux (pred n) impl
+    | _ -> false
+  in aux n impl
+
 (* Implicit args indexes are in ascending order *)
 (* inctx is useful only if there is a last argument to be deduced from ctxt *)
-let explicitize loc inctx impl (cf,primproj,f) args =
+let explicitize loc inctx impl (cf,primprojapp,f) args =
   let impl = if !Constrintern.parsing_explicit then [] else impl in
   let n = List.length args in
   let rec exprec q = function
@@ -491,39 +506,36 @@ let explicitize loc inctx impl (cf,primproj,f) args =
       raise Expl
     | [], _ -> []
   in
-  let ip = is_projection primproj (List.length args) cf in
+  let primproj, ip = is_projection primprojapp (List.length args) cf in
   let expl () = 
     match ip with
     | Some i ->
-      if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then
-	if primproj then
-	  let args = exprec 1 (args,impl) in		  
-	    CApp (loc, (None, f), args)
-	else raise Expl
-      else
-	let (args1,args2) = List.chop i args in
-	let (impl1,impl2) = if List.is_empty impl then [],[] else List.chop i impl in
-	let args1 = exprec 1 (args1,impl1) in
-	let args2 = exprec (i+1) (args2,impl2) in
-	let len = List.length args1 in
-	let ip = (* Printing primitive projection as application *) 
-	  if len == 1 && primproj && not !print_projections && not !Flags.raw_print then None
-	  else Some len
-	in
-	  CApp (loc,(ip,f),args1@args2)
+      (match primproj with
+      | Some npars -> (* Primitive projection in projection notation *)
+	let projimpl = CList.skipn_at_least npars impl in
+	  if not !print_projections && not !Flags.raw_print && params_implicit npars impl then
+	    (* Printing primitive projection as application *)
+	    let args = exprec 1 (args,projimpl) in		  
+	      CApp (loc, (None, f), args)
+	  else (** Printing as projection *)
+	    let args = exprec 1 (args,projimpl) in
+	      CApp (loc, (Some i,f),args)
+      | None -> (** Regular constant in projection notation *)
+	if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then
+	  raise Expl
+	else
+	  let (args1,args2) = List.chop i args in
+	  let (impl1,impl2) = if List.is_empty impl then [],[] else List.chop i impl in
+	  let args1 = exprec 1 (args1,impl1) in
+	  let args2 = exprec (i+1) (args2,impl2) in
+	  let ip = Some (List.length args1) in
+	    CApp (loc,(ip,f),args1@args2))
     | None ->
-      match cf with
-      | Some (ConstRef p) when not !in_debugger && not primproj 
-	  && Environ.is_projection p (Global.env ()) -> 
+      match primproj with
+      | Some npars when List.length args > npars && params_implicit npars impl ->
         (* Eta-expanded version of projection, print explicited if the implicit 
 	   application would be parsed as a primitive projection application. *)
-        let proj = Environ.lookup_projection p (Global.env ()) in
-	  if List.length args > proj.Declarations.proj_npars &&
-	    List.for_all is_status_implicit (List.firstn proj.Declarations.proj_npars impl)
-	  then raise Expl
-	  else
-            let args = exprec 1 (args,impl) in
-              CApp (loc, (None, f), args)
+	raise Expl
       | _ -> 
         let args = exprec 1 (args,impl) in
 	  if List.is_empty args then f else CApp (loc, (None, f), args)
@@ -531,7 +543,7 @@ let explicitize loc inctx impl (cf,primproj,f) args =
     try expl ()
     with Expl -> 
       let f',us = match f with CRef (f,us) -> f,us | _ -> assert false in
-      let ip = if primproj || !print_projections then ip else None in
+      let ip = if primprojapp != None || !print_projections then ip else None in
 	CAppExpl (loc, (ip, f', us), args)
 
 let is_start_implicit = function
@@ -554,10 +566,10 @@ let extern_app loc inctx impl (cf,primproj,f) us args =
       (!print_implicits && not !print_implicits_explicit_args)) &&
      List.exists is_status_implicit impl)
   then
-    if primproj then
+    if primproj != None then
       CAppExpl (loc, (Some 1,f,us), args)
     else
-      CAppExpl (loc, (is_projection primproj (List.length args) cf,f,us), args)
+      CAppExpl (loc, (snd (is_projection primproj (List.length args) cf),f,us), args)
   else
     explicitize loc inctx impl (cf,primproj,CRef (f,us)) args
 
@@ -715,7 +727,7 @@ let rec extern inctx scopes vars r =
 		 | Not_found | No_match | Exit ->
 		     extern_app loc inctx
 		       (select_stronger_impargs (implicits_of_global ref))
-		       (Some ref,false,extern_reference rloc vars ref) (extern_universes us) args
+		       (Some ref,None,extern_reference rloc vars ref) (extern_universes us) args
 	     end
 
 	 | GProj (loc,p,c) ->
@@ -725,13 +737,12 @@ let rec extern inctx scopes vars r =
 	     extern_args (extern true) (snd scopes) vars (c :: args) subscopes 
 	   in
 	     extern_app loc inctx 
-	     (projection_implicits (Global.env ()) p
-	      (select_stronger_impargs (implicits_of_global ref)))
-	       (Some ref, true, extern_reference loc vars ref)
+	     (select_stronger_impargs (implicits_of_global ref))
+	       (Some ref, Some p, extern_reference loc vars ref)
 	       None args
 	       
 	 | _       ->
-	   explicitize loc inctx [] (None,false,sub_extern false scopes vars f)
+	   explicitize loc inctx [] (None,None,sub_extern false scopes vars f)
              (List.map (sub_extern true scopes vars) args))
 
   | GProj (loc,p,c) ->
@@ -955,7 +966,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
  	if List.is_empty args then e
 	else
 	  let args = extern_args (extern true) scopes vars args argsscopes in
-	  explicitize loc false argsimpls (None,false,e) args
+	  explicitize loc false argsimpls (None,None,e) args
       with
 	  No_match -> extern_symbol allscopes vars t rules
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8f250e890..d34c43d3d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1466,7 +1466,7 @@ let internalize globalenv env allow_patvar lvar c =
 	  (match isproj, isprojf with
 	  | Some i, Some (r, n) -> (* Explicit application of primitive projection *)
 	    let scopes = proj_scopes n args_scopes in
-	    let args = intern_args env args_scopes (List.map fst args) in
+	    let args = intern_args env scopes (List.map fst args) in
 	      GApp (loc, GProj (loc, r, List.hd args), List.tl args)
 	  | _ ->
 	    (* Rem: GApp(_,f,[]) stands for @f *)
@@ -1725,12 +1725,12 @@ let internalize globalenv env allow_patvar lvar c =
     | hd :: tl -> None :: tl
     | [] -> []
 
-  and projection_implicits n noargs l = 
+  and projection_application_implicits n noargs l = 
     if n == 0 then Some l
     else match l with 
     | hd :: tl when is_status_implicit hd ->
       if maximal_insertion_of hd || not noargs then
-	projection_implicits (pred n) noargs tl
+	projection_application_implicits (pred n) noargs tl
       else None
     | _ -> None
 
@@ -1741,16 +1741,11 @@ let internalize globalenv env allow_patvar lvar c =
 	smart_gapp c loc l
     in
       match isprojf with
-      | Some (r, n) ->
-	(match projection_implicits n (List.is_empty l) imp with
-	| Some imp -> (* A primitive projection *)
-	  let subscopes = proj_scopes n subscopes in
-	  let imp = 
-	    if isproj != None then
-	      (* Drop first implicit which corresponds to record given in c.(p) notation *)
-	      make_first_explicit imp
-	    else imp
-	  in
+      | Some (r, n) -> (* A primitive projection *)
+	let subscopes = proj_scopes n subscopes in
+	if isproj != None then (* In projection notation: we remove the parameters *)
+	  let imp = projection_implicits (Global.env()) r imp in
+	  let imp = make_first_explicit imp in (* For the record argument *)
 	  let l = intern_impargs c env imp subscopes l in
 	    (match c, l with
 	    | GApp (loc', GRef (loc'', ConstRef f, _), hd :: tl), rest ->
@@ -1760,8 +1755,22 @@ let internalize globalenv env allow_patvar lvar c =
 	    | GRef (loc', ConstRef f, _), hd :: tl -> 
 	      let proj = GProj (Loc.merge loc' (loc_of_glob_constr hd), f, hd) in
 		smart_gapp proj loc tl
-	    | _ -> default ())
-	| None -> default ())
+	    | _ -> assert false)
+	else (* Not in projection notation, parse as primitive only if the implicits
+		allow *)
+	  (match projection_application_implicits n (List.is_empty l) imp with
+	  | Some imp ->
+	    let l = intern_impargs c env imp subscopes l in
+	      (match c, l with
+	      | GApp (loc', GRef (loc'', ConstRef f, _), hd :: tl), rest ->
+		let proj = GProj (Loc.merge loc'' (loc_of_glob_constr hd), f, hd) in
+		  if List.is_empty tl then smart_gapp proj loc rest
+		  else GApp (loc, proj, tl @ rest)
+	      | GRef (loc', ConstRef f, _), hd :: tl -> 
+		let proj = GProj (Loc.merge loc' (loc_of_glob_constr hd), f, hd) in
+		  smart_gapp proj loc tl
+	      | _ -> default ())
+	  | None -> default ())
       | None -> default ()
 
   and smart_gapp f loc = function
diff --git a/library/impargs.ml b/library/impargs.ml
index 355cbe1fa..cbbb2cea9 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -410,10 +410,6 @@ let compute_constant_implicits flags manual cst =
   let ty = Typeops.type_of_constant_type env cb.const_type in
   let impls = compute_semi_auto_implicits env flags manual ty in
     impls
-    (* match cb.const_proj with *)
-    (* | None -> impls *)
-    (* | Some {proj_npars = n} ->  *)
-    (* List.map (fun (x,args) -> x, CList.skipn_at_least n args) impls *)
 
 (*s Inductives and constructors. Their implicit arguments are stored
    in an array, indexed by the inductive number, of pairs $(i,v)$ where
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 02cb43db0..74083ac89 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -103,6 +103,14 @@ Set Printing All.
 Check p r.
 Unset Printing All.
 
+Check p r (X:=nat).
+Set Printing Projections.
+Check p r (X:=nat).
+Unset Printing Projections.
+Set Printing All.
+Check p r (X:=nat).
+Unset Printing All.
+
 (* Same elaboration, printing for p r *)
 
 (** Explicit version of the primitive projection, under applied w.r.t implicit arguments
@@ -116,7 +124,7 @@ Check r.(@p).
 Unset Printing All.
   
 (** Explicit version of the primitive projection, applied to its implicit arguments
-      can be printed only using projection notation r.(p), r.(@p) in fully explicit form *)
+      can be printed using application notation r.(p), r.(@p) in fully explicit form *)
 Check r.(@p) nat.
 Set Printing Projections.
 Check r.(@p) nat. 
@@ -129,7 +137,7 @@ Parameter r' : R' nat.
 
 Check (r'.(p')).
 Set Printing Projections.
-Check (r'.(p')).
+Check (r'.(p')). 
 Unset Printing Projections.
 Set Printing All.
 Check (r'.(p')).
@@ -140,7 +148,7 @@ Unset Printing All.
    Of type forall X : Set, nat * X
    No Printing All: p' r'
    Set Printing Projections.: r'.(p')
-   Printing All: r'.(p')
+   Printing All: r'.(@p')
  *)
 
 Check p' r'.