Improving abbreviations/notations + backtrack of semantic change in r12439

- Deactivation of short names registration and printing for
  abbreviations to identical names, what avoids printing uselessly
  qualified names binding where the short name is in fact equivalent.
- New treatment of abbreviations to names: don't insert any maximally
  inserted implicit arguments at all at the time of the abbreviation
  and use the regular internalization strategy to have them inserted
  at use time.
- The previous modifications altogether make redirections of
  qualified names easier and avoid the semantic change of r12349 and
  hence allows to keep "Notation b := @a" as it was before, i.e.  as a
  notation for the deactivation of the implicit arguments of a.
- Took benefit of these changes and updated nil/cons/list/app
  redefinition in "List.v".
- Fixed parsing/printing notation bugs (loop on partially applied
  abreviations for constructors in constrintern.ml + bad reverting of
  notations with holes that captured non anonymous variables in
  match_cases_pattern).
- Add support for parsing/printing abbreviations to @-like constructors
  and for reverting printing for abbreviations to constructors applied
  to parameters only (function extern_symbol_pattern).
- Minor error messages fixes and minor APIs cleaning.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12494 85f007b7-540e-0410-9357-904b9bb8a0f7

15 files changed, 194 insertions, 62 deletions

diff --git a/CHANGES b/CHANGES
index d76fe4bc7..0eb237a97 100644
--- a/CHANGES
+++ b/CHANGES
@@ -47,11 +47,13 @@ Tactic Language
 
 - Support for parsing non-empty lists with separators in tactic notations.
 
-Language
+Notations
 
-- Notations to names now behave like the names they refer to wrt implicit
-  arguments and interpretation scopes.
 - Record syntax "{|x=...; y=...|}" now works inside patterns too.
+- Abbreviations from non-imported module now invisible at printing time.
+- Abbreviations now use implicit arguments and arguments scopes for printing.
+- Abbreviations to pure names now strictly behave like the name they refer to
+  (make redirections of qualified names easier).
 
 Vernacular commands
 
diff --git a/dev/printers.mllib b/dev/printers.mllib
index d9f66d7bd..033e0fa60 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -101,6 +101,7 @@ Impargs
 Constrextern
 Syntax_def
 Implicit_quantifiers
+Smartlocate
 Constrintern
 Proof_trees
 Tacexpr
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e948dc6b4..60960754b 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -351,7 +351,6 @@ let bind_env (sigma,sigmalist as fullsigma) var v =
 let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
   | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
   | PatVar (_,Anonymous), AHole _ -> sigma
-  | a, AHole _ -> sigma
   | PatCstr (loc,(ind,_ as r1),args1,_), _ ->
       let nparams =
 	(fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
@@ -361,7 +360,10 @@ let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
 	  | AApp (ARef (ConstructRef r2),l2)  when r1 = r2 -> l2
           | _ -> raise No_match in
       if List.length l2 <> nparams + List.length args1
-      then raise No_match
+      then
+	(* TODO: revert partially applied notations of the form 
+           "Notation P x := (@pair _ _ x)." *)
+	raise No_match
       else
         let (p2,args2) = list_chop nparams l2 in
         (* All parameters must be _ *)
@@ -425,13 +427,26 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
-      try
-	(* Check the number of arguments expected by the notation *)
-	let loc,na = match t,n with
-	  | PatCstr (_,f,l,_), Some n when List.length l > n ->
-	      raise No_match
-	  | PatCstr (loc,_,_,na),_ -> loc,na
-	  | PatVar (loc,na),_ -> loc,na in
+    try
+      match t,n with
+      | PatCstr (loc,(ind,_),l,na), n when n = Some 0 or n = None or 
+	 n = Some(fst(Global.lookup_inductive ind)).Declarations.mind_nparams ->
+        (* Abbreviation for the constructor name only *)
+	(match keyrule with
+        | NotationRule (sc,ntn) -> raise No_match
+        | SynDefRule kn ->
+	    let p =
+	      let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
+	      if l = [] then
+		CPatAtom (loc,Some qid)
+	      else
+		let l =
+		  List.map (extern_cases_pattern_in_scope allscopes vars) l in
+		CPatCstr (loc,qid,l) in
+	    insert_pat_alias loc p na)
+      | PatCstr (_,f,l,_), Some n when List.length l > n ->
+	  raise No_match
+      | PatCstr (loc,_,_,na),_ ->
 	(* Try matching ... *)
 	let subst,substlist = match_aconstr_cases_pattern t pat in
 	(* Try availability of interpretation ... *)
@@ -458,8 +473,10 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
 	      let qid = shortest_qualid_of_syndef vars kn in
               CPatAtom (loc,Some (Qualid (loc, qid))) in
 	insert_pat_alias loc p na
-      with
-	  No_match -> extern_symbol_pattern allscopes vars t rules
+      | PatVar (loc,Anonymous),_ -> CPatAtom (loc, None)
+      | PatVar (loc,Name id),_ -> CPatAtom (loc, Some (Ident (loc,id)))
+    with
+	No_match -> extern_symbol_pattern allscopes vars t rules
 
 let extern_cases_pattern vars p =
   extern_cases_pattern_in_scope (None,[]) vars p
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d8cb8c715..cfce96521 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -68,12 +68,7 @@ let for_grammar f x =
 (* Locating reference, possibly via an abbreviation *)
 
 let locate_reference qid =
-  match Nametab.locate_extended qid with
-    | TrueGlobal ref -> ref
-    | SynDef kn ->
-	match Syntax_def.search_syntactic_definition dummy_loc kn with
-	  | [],ARef ref -> ref
-	  | _ -> raise Not_found
+  Smartlocate.global_of_extended_global (Nametab.locate_extended qid)
 
 let is_global id =
   try
@@ -429,25 +424,31 @@ let check_no_explicitation l =
     user_err_loc
      (loc,"",str"Unexpected explicitation of the argument of an abbreviation.")
 
+let dump_extended_global loc = function
+  | TrueGlobal ref -> Dumpglob.add_glob loc ref
+  | SynDef sp -> Dumpglob.add_glob_kn loc sp
+
+let intern_extended_global_of_qualid (loc,qid) =
+  try let r = Nametab.locate_extended qid in dump_extended_global loc r; r
+  with Not_found -> error_global_not_found_loc loc qid
+
+let intern_reference ref =
+  Smartlocate.global_of_extended_global
+    (intern_extended_global_of_qualid (qualid_of_reference ref))
+
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid loc qid intern env args =
-  try match Nametab.locate_extended qid with
+  match intern_extended_global_of_qualid (loc,qid) with
   | TrueGlobal ref ->
-      Dumpglob.add_glob loc ref;
       RRef (loc, ref), args
   | SynDef sp ->
-      Dumpglob.add_glob_kn loc sp;
-      match Syntax_def.search_syntactic_definition loc sp with
-      | [],ARef ref -> RRef (loc, ref), args
-      | (ids,c) ->
+      let (ids,c) = Syntax_def.search_syntactic_definition sp in
       let nids = List.length ids in
       if List.length args < nids then error_not_enough_arguments loc;
       let args1,args2 = list_chop nids args in
       check_no_explicitation args1;
       let subst = List.map2 (fun (id,scl) a -> (id,(fst a,scl))) ids args1 in
       subst_aconstr_in_rawconstr loc intern (subst,[]) ([],env) c, args2
-  with Not_found ->
-    error_global_not_found_loc loc qid
 
 (* Rule out section vars since these should have been found by intern_var *)
 let intern_non_secvar_qualid loc qid intern env args =
@@ -489,8 +490,8 @@ let rec simple_adjust_scopes n = function
 let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) =
   let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
   let npar = mib.Declarations.mind_nparams in
-  snd (list_chop (List.length pl1 + npar)
-    (simple_adjust_scopes (npar + List.length pl2)
+  snd (list_chop (npar + List.length pl1)
+    (simple_adjust_scopes (npar + List.length pl1 + List.length pl2)
       (find_arguments_scope (ConstructRef cstr))))
 
 (**********************************************************************)
@@ -564,11 +565,16 @@ let error_invalid_pattern_notation loc =
   user_err_loc (loc,"",str "Invalid notation for pattern.")
 
 let chop_aconstr_constructor loc (ind,k) args =
-  let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
-  let params,args = list_chop nparams args in
-  List.iter (function AHole _ -> ()
-    | _ -> error_invalid_pattern_notation loc) params;
-  args
+  if List.length args = 0 then (* Tolerance for a @id notation *) args else
+    begin
+      let mib,_ = Global.lookup_inductive ind in
+      let nparams = mib.Declarations.mind_nparams in
+      if nparams > List.length args then error_invalid_pattern_notation loc;
+      let params,args = list_chop nparams args in
+      List.iter (function AHole _ -> ()
+	| _ -> error_invalid_pattern_notation loc) params;
+      args
+    end
 
 let rec subst_pat_iterator y t (subst,p) = match p with
   | PatVar (_,id) as x ->
@@ -637,7 +643,7 @@ let find_constructor ref f aliases pats scopes =
     with Not_found -> raise (InternalisationError (loc,NotAConstructor ref)) in
   match gref with
   | SynDef sp ->
-      let (vars,a) = Syntax_def.search_syntactic_definition loc sp in
+      let (vars,a) = Syntax_def.search_syntactic_definition sp in
       (match a with
        | ARef (ConstructRef cstr) ->
 	   assert (vars=[]);
@@ -1123,7 +1129,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	  let args = List.map (fun a -> (a,None)) args in
 	  intern_applied_reference intern env lvar args ref in
 	check_projection isproj (List.length args) f;
-	if args = [] then f else
+	(* Rem: RApp(_,f,[]) stands for @f *)
 	RApp (loc, f, intern_args env args_scopes (List.map fst args))
     | CApp (loc, (isproj,f), args) ->
         let isproj,f,args = match f with
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index b08b8dd1f..ee677e80a 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -144,6 +144,10 @@ val intern_constr_pattern :
   evar_map -> env -> ?as_type:bool -> ?ltacvars:ltac_sign ->
     constr_pattern_expr -> patvar list * constr_pattern
 
+(* Raise Not_found if syndef not bound to a name and error if unexisting ref *)
+val intern_reference : reference -> global_reference
+
+(* Expands abbreviations (syndef); raise an error if not existing *)
 val interp_reference : ltac_sign -> reference -> rawconstr
 
 (* Interpret binders *)
@@ -161,8 +165,8 @@ val interp_context_evars : ?fail_anonymous:bool ->
   evar_defs ref -> env -> local_binder list -> (env * rel_context) * manual_implicits
 
 (* Locating references of constructions, possibly via a syntactic definition *)
+(* (these functions do not modify the glob file) *)
 
-val locate_reference : qualid -> global_reference
 val is_global : identifier -> bool
 val construct_reference : named_context -> identifier -> constr
 val global_reference : identifier -> constr
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 9b4ff860c..faad3c50a 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -25,7 +25,7 @@ open Topconstr
 let global_of_extended_global = function
   | TrueGlobal ref -> ref
   | SynDef kn ->
-  match search_syntactic_definition dummy_loc kn with
+  match search_syntactic_definition kn with
   | [],ARef ref -> ref
   | _ -> raise Not_found
 
@@ -34,7 +34,7 @@ let locate_global_with_alias (loc,qid) =
   try global_of_extended_global ref
   with Not_found ->
     user_err_loc (loc,"",pr_qualid qid ++
-      str " is bound to a notation that does not denote a reference")
+      str " is bound to a notation that does not denote a reference.")
 
 let global_inductive_with_alias r =
   let (loc,qid as lqid) = qualid_of_reference r in
@@ -42,7 +42,7 @@ let global_inductive_with_alias r =
   | IndRef ind -> ind
   | ref ->
       user_err_loc (loc_of_reference r,"global_inductive",
-        pr_reference r ++ spc () ++ str "is not an inductive type")
+        pr_reference r ++ spc () ++ str "is not an inductive type.")
   with Not_found -> Nametab.error_global_not_found_loc loc qid
 
 let global_with_alias r =
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index b0e27f04e..245ed0f50 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -38,15 +38,25 @@ let load_syntax_constant i ((sp,kn),(local,pat,onlyparse)) =
   add_syntax_constant kn pat;
   Nametab.push_syndef (Nametab.Until i) sp kn
 
+let is_alias_of_already_visible_name sp = function
+  | _,ARef ref ->
+      let (dir,id) = repr_qualid (shortest_qualid_of_global Idset.empty ref) in
+      dir = empty_dirpath && id = basename sp
+  | _ ->
+      false
+
 let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
-  Nametab.push_syndef (Nametab.Exactly i) sp kn;
-  if not onlyparse then
-    (* Redeclare it to be used as (short) name in case an other (distfix)
-       notation was declared inbetween *)
-    Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
+  if not (is_alias_of_already_visible_name sp pat) then begin
+    Nametab.push_syndef (Nametab.Exactly i) sp kn;
+    if not onlyparse then
+      (* Redeclare it to be used as (short) name in case an other (distfix)
+	 notation was declared inbetween *)
+      Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
+  end
 
 let cache_syntax_constant d =
-  load_syntax_constant 1 d
+  load_syntax_constant 1 d;
+  open_syntax_constant 1 d
 
 let subst_syntax_constant (subst,(local,pat,onlyparse)) =
   (local,subst_interpretation subst pat,onlyparse)
@@ -72,5 +82,5 @@ let out_pat ((ids,idsl),ac) = assert (idsl=[]); (ids,ac)
 let declare_syntactic_definition local id onlyparse pat =
   let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
 
-let search_syntactic_definition loc kn =
+let search_syntactic_definition kn =
   out_pat (KNmap.find kn !syntax_table)
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 747f7b9da..b4da6dd7a 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -24,4 +24,4 @@ type syndef_interpretation = (identifier * subscopes) list * aconstr
 val declare_syntactic_definition : bool -> identifier -> bool ->
   syndef_interpretation -> unit
 
-val search_syntactic_definition : loc -> kernel_name -> syndef_interpretation
+val search_syntactic_definition : kernel_name -> syndef_interpretation
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index b7e218719..98c93f897 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -408,7 +408,7 @@ let gallina_print_constant_with_infos sp =
 let gallina_print_syntactic_def kn =
   let sep = " := "
   and qid = Nametab.shortest_qualid_of_syndef Idset.empty kn
-  and (vars,a) = Syntax_def.search_syntactic_definition dummy_loc kn in
+  and (vars,a) = Syntax_def.search_syntactic_definition kn in
   let c = Topconstr.rawconstr_of_aconstr dummy_loc a in
   str "Notation " ++ pr_qualid qid ++
   prlist_with_sep spc pr_id (List.map fst vars) ++ str sep ++
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 428583047..01eef8082 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -46,6 +46,10 @@ fun x : nat => ifn x is succ n then n else 0
      : bool
 -4
      : Z
+SUM (nat * nat) nat
+     : Set
+FST (0; 1)
+     : Z
 Nil
      : forall A : Type, list A
 NIL:list nat
@@ -57,3 +61,34 @@ Defining 'I' as keyword
      : Z * Z * Z * (Z * Z * Z)
 fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z
      : (Z -> Z -> Z -> Z) -> Z
+plus
+     : nat -> nat -> nat
+S
+     : nat -> nat
+mult
+     : nat -> nat -> nat
+le
+     : nat -> nat -> Prop
+plus
+     : nat -> nat -> nat
+succ
+     : nat -> nat
+mult
+     : nat -> nat -> nat
+le
+     : nat -> nat -> Prop
+fun x : option Z => match x with
+                    | SOME x0 => x0
+                    | NONE => 0
+                    end
+     : option Z -> Z
+fun x : option Z => match x with
+                    | SOME2 x0 => x0
+                    | NONE2 => 0
+                    end
+     : option Z -> Z
+fun x : option Z => match x with
+                    | SOME3 x0 => x0
+                    | NONE3 => 0
+                    end
+     : option Z -> Z
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 8d16dff5b..f041b9b71 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -121,6 +121,18 @@ Notation "- 4" := (-2 + -2).
 Check -4.
 
 (**********************************************************************)
+(* Check preservation of scopes at printing time *)
+
+Notation SUM := sum.
+Check SUM (nat*nat) nat.
+
+(**********************************************************************)
+(* Check preservation of implicit arguments at printing time *)
+
+Notation FST := fst.
+Check FST (0;1).
+
+(**********************************************************************)
 (* Check notations for references with activated or deactivated       *)
 (* implicit arguments                                                 *)
 
@@ -159,3 +171,38 @@ Check [|1,2,3;4,5,6|].
 
 Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y).
 Check fun f => {| f; 0; 1; 2 |} : Z.
+
+(**********************************************************************)
+(* Check printing of notations from other modules *)
+
+(* 1- Non imported case *)
+
+Require make_notation.
+
+Check plus.
+Check S.
+Check mult.
+Check le.
+
+(* 2- Imported case *)
+
+Import make_notation.
+
+Check plus.
+Check S.
+Check mult.
+Check le.
+
+(* Check notations in cases patterns *)
+
+Notation SOME := Some.
+Notation NONE := None.
+Check (fun x => match x with SOME x => x | NONE => 0 end).
+
+Notation NONE2 := (@None _).
+Notation SOME2 := (@Some _).     
+Check (fun x => match x with SOME2 x => x | NONE2 => 0 end).
+
+Notation NONE3 := @None.
+Notation SOME3 := @Some.     
+Check (fun x => match x with SOME3 x => x | NONE3 => 0 end).
diff --git a/test-suite/prerequisite/make_notation.v b/test-suite/prerequisite/make_notation.v
index 4a75713d1..c93d102a2 100644
--- a/test-suite/prerequisite/make_notation.v
+++ b/test-suite/prerequisite/make_notation.v
@@ -1,3 +1,8 @@
 (* Used in Notation.v to test import of notations from files in sections *)
 
 Notation "'Z'" := O (at level 9).
+Notation plus := plus.
+Notation succ := S.
+Notation mult := mult (only parsing).
+Notation less := le (only parsing).
+
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 316bede93..7ddb6146d 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -49,8 +49,7 @@ Definition foo P := let '(exists x, Q) := P in x = Q :> nat.
 Notation "'exists' x >= y , P" := (exists x, x >= y /\ P)%nat
    (at level 200, x ident, right associativity, y at level 69).
 
-(* Check that notations to atomic references preserve implicit arguments *)
+(* This used to loop at some time before r12491 *)
 
-Notation eq := @eq.
-
-Check (eq 0 0).
+Notation R x := (@pair _ _ x).
+Check (fun x:nat*nat => match x with R x y => (x,y) end).
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index f520c4fd6..d6b4c1354 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1973,13 +1973,10 @@ Notation list := list (only parsing).
 Notation list_rect := list_rect (only parsing).
 Notation list_rec := list_rec (only parsing).
 Notation list_ind := list_ind (only parsing).
-Notation nil := @nil (only parsing).
-Notation cons := @cons (only parsing).
-Notation length := @length (only parsing).
-Notation app := @app (only parsing).
-(* We hide these compatibility notations behind the true definitions
-   that are in [Datatypes]: *)
-Export Datatypes.
+Notation nil := nil (only parsing).
+Notation cons := cons (only parsing).
+Notation length := length (only parsing).
+Notation app := app (only parsing).
 (* Compatibility Names *)
 Notation ass_app := app_assoc (only parsing).
 Notation app_ass := app_assoc_reverse (only parsing).
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index b3fbeb655..63f653eda 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1049,8 +1049,17 @@ let add_delimiters scope key =
 let add_class_scope scope cl =
   Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl))
 
+(* Check if abbreviation to a name and avoid early insertion of
+   maximal implicit arguments *)
+let try_interp_name_alias = function
+  | [], CRef ref -> intern_reference ref
+  | _ -> raise Not_found
+
 let add_syntactic_definition ident (vars,c) local onlyparse =
-  let ((vars,_),pat) = interp_aconstr (vars,[]) c in
+  let vars,pat =
+    try [], ARef (try_interp_name_alias (vars,c))
+    with Not_found -> let (vars,_),pat = interp_aconstr (vars,[]) c in vars,pat
+  in
   let onlyparse = onlyparse or is_not_printable pat in
   Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)