Revert specific syntax for primitive projections, avoiding ugly

contortions in internalization/externalization. It uses a fully typed
version of detyping, requiring the environment, to move from
primitive projection applications to regular applications of
the eta-expanded version. The kernel is unchanged, and only
constrMatching needs compatibility code now.

6 files changed, 49 insertions, 169 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 2e6ab4354..b774da356 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -437,28 +437,14 @@ let occur_name na aty =
     | Name id -> occur_var_constr_expr id aty
     | Anonymous -> false
 
-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_projection nargs = function
+  | 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
+	 else Some n
+     with Not_found -> None)
+  | _ -> None
 	
 let is_hole = function CHole _ | CEvar _ -> true | _ -> false
 
@@ -481,7 +467,7 @@ let params_implicit 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,primprojapp,f) args =
+let explicitize loc inctx impl (cf,f) args =
   let impl = if !Constrintern.parsing_explicit then [] else impl in
   let n = List.length args in
   let rec exprec q = function
@@ -506,44 +492,27 @@ let explicitize loc inctx impl (cf,primprojapp,f) args =
       raise Expl
     | [], _ -> []
   in
-  let primproj, ip = is_projection primprojapp (List.length args) cf in
+  let ip = is_projection (List.length args) cf in
   let expl () = 
     match ip with
     | Some i ->
-      (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 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. *)
+      if not (List.is_empty impl) && is_status_implicit (List.nth impl (i-1)) then
 	raise Expl
-      | _ -> 
-        let args = exprec 1 (args,impl) in
-	  if List.is_empty args then f else CApp (loc, (None, f), args)
+      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 ->
+      let args = exprec 1 (args,impl) in
+	if List.is_empty args then f else CApp (loc, (None, f), args)
   in
     try expl ()
     with Expl -> 
       let f',us = match f with CRef (f,us) -> f,us | _ -> assert false in
-      let ip = if primprojapp != None || !print_projections then ip else None in
+      let ip = if !print_projections then ip else None in
 	CAppExpl (loc, (ip, f', us), args)
 
 let is_start_implicit = function
@@ -557,7 +526,7 @@ let extern_global loc impl f us =
   else
     CRef (f,us)
 
-let extern_app loc inctx impl (cf,primproj,f) us args =
+let extern_app loc inctx impl (cf,f) us args =
   if List.is_empty args then
     (* If coming from a notation "Notation a := @b" *)
     CAppExpl (loc, (None, f, us), [])
@@ -566,12 +535,9 @@ 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 != None then
-      CAppExpl (loc, (Some 1,f,us), args)
-    else
-      CAppExpl (loc, (snd (is_projection primproj (List.length args) cf),f,us), args)
+    CAppExpl (loc, (is_projection (List.length args) cf,f,us), args)
   else
-    explicitize loc inctx impl (cf,primproj,CRef (f,us)) args
+    explicitize loc inctx impl (cf,CRef (f,us)) args
 
 let rec extern_args extern scopes env args subscopes =
   match args with
@@ -585,12 +551,6 @@ let rec extern_args extern scopes env args subscopes =
 
 let match_coercion_app = function
   | GApp (loc,GRef (_,r,_),args) -> Some (loc, r, 0, args)
-  | GProj (loc, r, arg) -> 
-    let pars = Inductiveops.projection_nparams r in
-      Some (loc, ConstRef r, pars, [arg])
-  | GApp (loc,GProj (_, r, c), args) -> 
-    let pars = Inductiveops.projection_nparams r in
-      Some (loc, ConstRef r, pars, c :: args)
   | _ -> None
 
 let rec remove_coercions inctx c =
@@ -728,27 +688,13 @@ 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,None,extern_reference rloc vars ref) (extern_universes us) args
+		       (Some ref,extern_reference rloc vars ref) (extern_universes us) args
 	     end
-
-	 | GProj (loc,p,c) ->
-	   let ref = ConstRef p in
-	   let subscopes = find_arguments_scope ref in
-	   let args =
-	     extern_args (extern true) (snd scopes) vars (c :: args) subscopes 
-	   in
-	     extern_app loc inctx 
-	     (select_stronger_impargs (implicits_of_global ref))
-	       (Some ref, Some p, extern_reference loc vars ref)
-	       None args
 	       
 	 | _       ->
-	   explicitize loc inctx [] (None,None,sub_extern false scopes vars f)
+	   explicitize loc inctx [] (None,sub_extern false scopes vars f)
              (List.map (sub_extern true scopes vars) args))
 
-  | GProj (loc,p,c) ->
-    extern inctx scopes vars (GApp (loc,r',[]))
-
   | GLetIn (loc,na,t,c) ->
       CLetIn (loc,(loc,na),sub_extern false scopes vars t,
               extern inctx scopes (add_vname vars na) c)
@@ -967,7 +913,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,None,e) args
+	  explicitize loc false argsimpls (None,e) args
       with
 	  No_match -> extern_symbol allscopes vars t rules
 
@@ -989,7 +935,7 @@ let extern_glob_type vars c =
 
 let loc = Loc.ghost (* for constr and pattern, locations are lost *)
 
-let extern_constr_gen goal_concl_style scopt env sigma t =
+let extern_constr_gen lax goal_concl_style scopt env sigma t =
   (* "goal_concl_style" means do alpha-conversion using the "goal" convention *)
   (* i.e.: avoid using the names of goal/section/rel variables and the short *)
   (* names of global definitions of current module when computing names for *)
@@ -998,21 +944,19 @@ let extern_constr_gen goal_concl_style scopt env sigma t =
   (* those goal/section/rel variables that occurs in the subterm under *)
   (* consideration; see namegen.ml for further details *)
   let avoid = if goal_concl_style then ids_of_context env else [] in
-  let rel_env_names = names_of_rel_context env in
-  let r = Detyping.detype goal_concl_style avoid rel_env_names sigma t in
+  let r = Detyping.detype ~lax goal_concl_style avoid env sigma t in
   let vars = vars_of_env env in
   extern false (scopt,[]) vars r
 
 let extern_constr_in_scope goal_concl_style scope env sigma t =
-  extern_constr_gen goal_concl_style (Some scope) env sigma t
+  extern_constr_gen false goal_concl_style (Some scope) env sigma t
 
-let extern_constr goal_concl_style env sigma t =
-  extern_constr_gen goal_concl_style None env sigma t
+let extern_constr ?(lax=false) goal_concl_style env sigma t =
+  extern_constr_gen lax goal_concl_style None env sigma t
 
 let extern_type goal_concl_style env sigma t =
   let avoid = if goal_concl_style then ids_of_context env else [] in
-  let rel_env_names = names_of_rel_context env in
-  let r = Detyping.detype goal_concl_style avoid rel_env_names sigma t in
+  let r = Detyping.detype goal_concl_style avoid env sigma t in
   extern_glob_type (vars_of_env env) r
 
 let extern_sort s = extern_glob_sort (detype_sort s)
@@ -1076,14 +1020,14 @@ let rec glob_of_pat env sigma = function
 	| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive")
       in
       GCases (loc,RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat)
-  | PFix f -> Detyping.detype false [] env sigma (mkFix f)
-  | PCoFix c -> Detyping.detype false [] env sigma (mkCoFix c)
+  | PFix f -> Detyping.detype_names false [] env (Global.env()) sigma (mkFix f) (** FIXME bad env *)
+  | PCoFix c -> Detyping.detype_names false [] env (Global.env()) sigma (mkCoFix c)
   | PSort s -> GSort (loc,s)
 
 let extern_constr_pattern env sigma pat =
   extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat)
 
 let extern_rel_context where env sigma sign =
-  let a = detype_rel_context where [] (names_of_rel_context env) sigma sign in
+  let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in
   let vars = vars_of_env env in
   pi3 (extern_local_binder (None,[]) vars a)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index a994d8693..023c5be22 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -30,9 +30,12 @@ val extern_constr_pattern : names_context -> Evd.evar_map ->
   constr_pattern -> constr_expr
 
 (** If [b=true] in [extern_constr b env c] then the variables in the first
-   level of quantification clashing with the variables in [env] are renamed *)
+   level of quantification clashing with the variables in [env] are renamed.
+    ~lax is for debug printing, when the constr might not be well typed in 
+    env, sigma
+*)
 
-val extern_constr : bool -> env -> Evd.evar_map -> constr -> constr_expr
+val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr
 val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
 val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference
 val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 66f51b19e..56780e240 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1312,7 +1312,6 @@ let get_implicit_name n imps =
 
 let set_hole_implicit i b = function
   | GRef (loc,r,_) | GApp (_,GRef (loc,r,_),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b),None)
-  | GProj (loc,p,_) -> (loc,Evar_kinds.ImplicitArg (ConstRef p,i,b),None)
   | GVar (loc,id) -> (loc,Evar_kinds.ImplicitArg (VarRef id,i,b),None)
   | _ -> anomaly (Pp.str "Only refs have implicits")
 
@@ -1463,14 +1462,8 @@ let internalize globalenv env allow_patvar lvar c =
 	  intern_applied_reference intern env (Environ.named_context globalenv) 
 	    lvar us args ref 
 	in
-	  (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 scopes (List.map fst args) in
-	      GApp (loc, GProj (loc, r, List.hd args), List.tl args)
-	  | _ ->
-	    (* Rem: GApp(_,f,[]) stands for @f *)
-	    GApp (loc, f, intern_args env args_scopes (List.map fst args)))
+	  (* Rem: GApp(_,f,[]) stands for @f *)
+	  GApp (loc, f, intern_args env args_scopes (List.map fst args))
 
     | CApp (loc, (isproj,f), args) ->
         let isproj,f,args = match f with
@@ -1726,58 +1719,10 @@ let internalize globalenv env allow_patvar lvar c =
 	  intern_args env subscopes rargs
     in aux 1 l subscopes eargs rargs
 
-  and make_first_explicit l =
-    match l with
-    | hd :: tl -> None :: tl
-    | [] -> []
-
-  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_application_implicits (pred n) noargs tl
-      else None
-    | _ -> None
-
   and apply_impargs (isproj,isprojf) c env imp subscopes l loc = 
     let imp = select_impargs_size (List.length l) imp in
-    let default () =
-      let l = intern_impargs c env imp subscopes l in
-	smart_gapp c loc l
-    in
-      match isprojf with
-      | 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 ->
-	      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
-	    | _ -> 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 ()
+    let l = intern_impargs c env imp subscopes l in
+      smart_gapp c loc l
 
   and smart_gapp f loc = function
     | [] -> f
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index c69eb629d..90303cc92 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -127,7 +127,6 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp
 	  else (id, loc) :: vs
 	else vs
     | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args)
-    | GProj (loc,p,c) -> vars bound vs c
     | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) ->
 	let vs' = vars bound vs ty in
 	let bound' = add_name_to_ids bound na in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 1aac1c53d..81e2ac810 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -55,7 +55,6 @@ let ldots_var = Id.of_string ".."
 let glob_constr_of_notation_constr_with_binders loc g f e = function
   | NVar id -> GVar (loc,id)
   | NApp (a,args) -> GApp (loc,f e a, List.map (f e) args)
-  | NProj (p,c) -> GProj (loc,p,f e c)
   | NList (x,y,iter,tail,swap) ->
       let t = f e tail in let it = f e iter in
       let innerl = (ldots_var,t)::(if swap then [] else [x,GVar(loc,y)]) in
@@ -150,7 +149,6 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
   | GRef (_,r1,_), GRef (_,r2,_) -> eq_gr r1 r2
   | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1)
   | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2
-  | GProj (_,p1,c1), GProj (_, p2, c2) -> eq_constant p1 p2 && f c1 c2
   | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2)
     when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
     on_true_do (f ty1 ty2 && f c1 c2) add na1
@@ -166,7 +164,7 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
   | _,(GCases _ | GRec _
       | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _)
       -> error "Unsupported construction in recursive notations."
-  | (GRef _ | GVar _ | GApp _ | GProj _ | GLambda _ | GProd _
+  | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _
     | GHole _ | GSort _ | GLetIn _), _
       -> false
 
@@ -261,7 +259,6 @@ let notation_constr_and_vars_of_glob_constr a =
   and aux' = function
   | GVar (_,id) -> add_id found id; NVar id
   | GApp (_,g,args) -> NApp (aux g, List.map aux args)
-  | GProj (_,p,c) -> NProj (p, aux c)
   | GLambda (_,na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c)
   | GProd (_,na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c)
   | GLetIn (_,na,b,c) -> add_name found na; NLetIn (na,aux b,aux c)
@@ -356,7 +353,7 @@ let notation_constr_of_glob_constr nenv a =
 (* Substitution of kernel names, avoiding a list of bound identifiers *)
 
 let notation_constr_of_constr avoiding t =
-  let t = Detyping.detype false avoiding [] Evd.empty t in
+  let t = Detyping.detype false avoiding (Global.env()) Evd.empty t in
   let nenv = {
     ninterp_var_type = Id.Map.empty;
     ninterp_rec_vars = Id.Map.empty;
@@ -388,12 +385,6 @@ let rec subst_notation_constr subst bound raw =
 	if r' == r && rl' == rl then raw else
 	  NApp(r',rl')
 
-  | NProj (p,c) ->
-      let p' = subst_constant subst p in
-      let c' = subst_notation_constr subst bound c in
-	if p == p' && c == c' then raw else
-	  NProj (p',c')
-
   | NList (id1,id2,r1,r2,b) ->
       let r1' = subst_notation_constr subst bound r1
       and r2' = subst_notation_constr subst bound r2 in
@@ -669,8 +660,6 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
   | GVar (_,id1), NVar id2 when alpha_var id1 id2 alp -> sigma
   | GRef (_,r1,_), NRef r2 when (eq_gr r1 r2) -> sigma
   | GPatVar (_,(_,n1)), NPatVar n2 when Id.equal n1 n2 -> sigma
-  | GProj (loc,f1,c1), NProj (f2,c2) when Constant.equal f1 f2 -> 
-     match_in u alp metas sigma c1 c2
   | GApp (loc,f1,l1), NApp (f2,l2) ->
       let n1 = List.length l1 and n2 = List.length l2 in
       let f1,l1,f2,l2 =
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 33c21eea5..bb4109009 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -108,7 +108,7 @@ let constr_key c =
 let revert_reserved_type t =
   try
     let reserved = KeyMap.find (constr_key t) !reserve_revtable in
-    let t = Detyping.detype false [] [] Evd.empty t in
+    let t = Detyping.detype false [] (Global.env()) Evd.empty t in
     (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _]
         then I've introduced a bug... *)
     let filter _ pat =