Did that adding a rule for printing applications as "f(x)" works.

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

4 files changed, 37 insertions, 14 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fa0e18915..08db24dba 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -747,16 +747,22 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
       try
 	(* Adjusts to the number of arguments expected by the notation *)
 	let (t,args,argsscopes,argsimpls) = match t,n with
-	  | GApp (_,(GRef (_,ref) as f),args), Some n
+	  | GApp (_,f,args), Some n
 	      when List.length args >= n ->
 	      let args1, args2 = list_chop n args in
-	      let subscopes =
-		try list_skipn n (find_arguments_scope ref) with _ -> [] in
-	      let impls =
-		let impls =
-		  select_impargs_size
-		    (List.length args) (implicits_of_global ref) in
-		try list_skipn n impls with _ -> [] in
+              let subscopes, impls =
+                match f with
+                | GRef (_,ref) ->
+	          let subscopes =
+		    try list_skipn n (find_arguments_scope ref) with _ -> [] in
+	          let impls =
+		    let impls =
+		      select_impargs_size
+		        (List.length args) (implicits_of_global ref) in
+		    try list_skipn n impls with _ -> [] in
+                  subscopes,impls
+                | _ ->
+                  [], [] in
 	      (if n = 0 then f else GApp (dummy_loc,f,args1)),
 	      args2, subscopes, impls
 	  | GApp (_,(GRef (_,ref) as f),args), None ->
diff --git a/interp/notation.ml b/interp/notation.ml
index 771e85692..ae14cd5ca 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -187,11 +187,15 @@ type key =
 let notations_key_table = ref Gmapl.empty
 let prim_token_key_table = Hashtbl.create 7
 
-let glob_constr_key = function
-  | GApp (_,GRef (_,ref),_) -> RefKey (canonical_gr ref)
-  | GRef (_,ref) -> RefKey (canonical_gr ref)
+let glob_prim_constr_key = function
+  | GApp (_,GRef (_,ref),_) | GRef (_,ref) -> RefKey (canonical_gr ref)
   | _ -> Oth
 
+let glob_constr_keys = function
+  | GApp (_,GRef (_,ref),_) -> [RefKey (canonical_gr ref); Oth]
+  | GRef (_,ref) -> [RefKey (canonical_gr ref)]
+  | _ -> [Oth]
+
 let cases_pattern_key = function
   | PatCstr (_,ref,_,_) -> RefKey (canonical_gr (ConstructRef ref))
   | _ -> Oth
@@ -201,6 +205,7 @@ let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
   | AList (_,_,AApp (ARef ref,args),_,_)
   | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args)
   | ARef ref -> RefKey(canonical_gr ref), None
+  | AApp (_,args) -> Oth, Some (List.length args)
   | _ -> Oth, None
 
 (**********************************************************************)
@@ -234,7 +239,8 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
   declare_scope sc;
   add_prim_token_interpreter sc interp;
   List.iter (fun pat ->
-      Hashtbl.add prim_token_key_table (glob_constr_key pat) (sc,uninterp,b))
+      Hashtbl.add prim_token_key_table
+        (glob_prim_constr_key pat) (sc,uninterp,b))
     patl
 
 let mkNumeral n = Numeral n
@@ -369,8 +375,11 @@ let rec interp_notation loc ntn local_scopes =
     user_err_loc
     (loc,"",str ("Unknown interpretation for notation \""^ntn^"\"."))
 
+let isGApp = function GApp _ -> true | _ -> false
+
 let uninterp_notations c =
-  Gmapl.find (glob_constr_key c) !notations_key_table
+  list_map_append (fun key -> Gmapl.find key !notations_key_table)
+    (glob_constr_keys c)
 
 let uninterp_cases_pattern_notations c =
   Gmapl.find (cases_pattern_key c) !notations_key_table
@@ -382,7 +391,8 @@ let availability_of_notation (ntn_scope,ntn) scopes =
 
 let uninterp_prim_token c =
   try
-    let (sc,numpr,_) = Hashtbl.find prim_token_key_table (glob_constr_key c) in
+    let (sc,numpr,_) =
+      Hashtbl.find prim_token_key_table (glob_prim_constr_key c) in
     match numpr c with
       | None -> raise No_match
       | Some n -> (sc,n)
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 6731d5054..444d6b091 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -25,3 +25,5 @@ let '(a, _, _) := (2, 3, 4) in a
 Defining 'let'' as keyword
 let' f (x y z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2
      : bool -> nat
+λ (f : nat -> nat) (x : nat), f(x) + S(x)
+     : (nat -> nat) -> nat -> nat
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index a78088bad..e7b0b9754 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -55,6 +55,11 @@ Notation "'let'' f x .. y  :=  t 'in' u":=
 
 Check let' f x y z (a:bool) := x+y+z+1 in f 0 1 2.
 
+(* In practice, only the printing rule is used here *)
+(* Note: does not work for pattern *)
+Notation "f ( x )" := (f x) (at level 10, format "f ( x )").
+Check fun f x => f x + S x.
+
 (* This one is not fully satisfactory because binders in the same type
    are re-factorized and parentheses are needed even for atomic binder