Mise en place d'implicites par noms en v8

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

5 files changed, 53 insertions, 10 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 16e1a63881..43879c3b63 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -217,7 +217,7 @@ GEXTEND Gram
   ;
   constr91:
     [ [ test_int_bang; n = INT; "!"; c = operconstr LEVEL "9" ->
-        (c, Some (int_of_string n))
+        (c, Some (loc,ExplByPos (int_of_string n)))
       | c = operconstr LEVEL "9" -> (c, None) ] ]
   ;
   (* annot and product_annot_tail are hacks to forbid concrete syntax *)
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 6e279218ef..c3a7c27b3a 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -132,10 +132,27 @@ let rec mkCLambdaN loc bll c =
   | [] -> c
   | LocalRawAssum ([],_) :: bll -> mkCLambdaN loc bll c
 
+(* Hack to parse "(n)" as nat without conflicts with the (useless) *)
+(* admissible notation "(n)" *)
+let test_lpar_id_coloneq =
+  Gram.Entry.of_parser "test_lpar_id_coloneq"
+    (fun strm ->
+      match Stream.npeek 1 strm with
+        | [("", "(")] ->
+            begin match Stream.npeek 2 strm with
+              | [_; ("IDENT", _)] ->
+		  begin match Stream.npeek 3 strm with
+		    | [_; _; ("", ":=")] -> ()
+		    | _ -> raise Stream.Failure
+		  end
+	      | _ -> raise Stream.Failure
+            end
+        | _ -> raise Stream.Failure)
+
 if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr sort global
-  constr_pattern Constr.ident binder_let tuple_constr;
+  constr_pattern lconstr_pattern Constr.ident binder_let tuple_constr;
   Constr.ident:
     [ [ id = Prim.ident -> id
 
@@ -151,6 +168,9 @@ GEXTEND Gram
   constr_pattern:
     [ [ c = constr -> c ] ]
   ;
+  lconstr_pattern:
+    [ [ c = lconstr -> c ] ]
+  ;
   sort:
     [ [ "Set"  -> RProp Pos
       | "Prop" -> RProp Null
@@ -218,7 +238,11 @@ GEXTEND Gram
       | c=fix_constr -> c ] ]
   ;
   appl_arg:
-    [ [ "@"; n=INT; ":="; c=constr -> (c,Some(int_of_string n))
+    [ [ _ = test_lpar_id_coloneq; "("; id = ident; ":="; c=lconstr; ")" ->
+	  (c,Some (loc,ExplByName id))
+(*
+      | "@"; n=INT; ":="; c=constr -> (c,Some(loc,ExplByPos (int_of_string n)))
+*)
       | c=constr -> (c,None) ] ]
   ;
   atomic_constr:
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index af651a4f20..4afdf55f41 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -81,7 +81,8 @@ let pr_sort = function
 
 let pr_explicitation = function
   | None -> mt ()
-  | Some n -> int n ++ str "!"
+  | Some (_,ExplByPos n) -> int n ++ str "!"
+  | Some (_,ExplByName n) -> anomaly "Argument made explicit by name"
 
 let pr_expl_args pr (a,expl) =
   pr_explicitation expl ++ pr (lapp,L) a
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index bf26f02ecf..d39be39190 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -47,7 +47,19 @@ let print_impl_args_by_pos = function
       prlist_with_sep (fun () -> str "; ") int l ++
       str"] are implicit" ++ fnl()
 
-let print_impl_args l = print_impl_args_by_pos (positions_of_implicits l)
+let print_impl_args_by_name = function
+  | []  -> mt ()
+  | [i] -> str"Argument " ++ pr_id (name_of_implicit i) ++ str" is implicit" ++
+      fnl()
+  | l   -> 
+      str"Arguments " ++ 
+      prlist_with_sep (fun () -> str ", ")
+        (fun imp -> pr_id (name_of_implicit imp)) l ++
+      str" are implicit" ++ fnl()
+
+let print_impl_args l = 
+  if !Options.v7 then print_impl_args_by_pos (positions_of_implicits l)
+  else print_impl_args_by_name (List.filter is_status_implicit l)
 
 let print_argument_scopes = function
   | [Some sc] -> str"Argument scope is [" ++ str sc ++ str"]" ++ fnl()
@@ -58,6 +70,10 @@ let print_argument_scopes = function
       str "]") ++ fnl()
   | _  -> mt()
 
+let print_name_infos ref =
+  print_impl_args (implicits_of_global ref) ++
+  print_argument_scopes (Symbols.find_arguments_scope ref)
+
 (* To be improved; the type should be used to provide the types in the
    abstractions. This should be done recursively inside prterm, so that
    the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u)
@@ -163,8 +179,7 @@ let print_mutual sp =
 let print_section_variable sp =
   let d = get_variable sp in
   print_named_decl d ++ 
-  print_impl_args (implicits_of_global (VarRef sp)) ++
-  print_argument_scopes (Symbols.find_arguments_scope (VarRef sp))
+  print_name_infos (VarRef sp)
 
 let print_body = function
   | Some lc  -> prterm (Declarations.force lc)
@@ -187,8 +202,7 @@ let print_constant with_values sep sp =
 	print_basename sp ++ str sep ++ cut () ++
 	(if with_values then print_typed_body (val_0,typ) else prtype typ) ++
 	fnl ()) ++ 
-  print_impl_args (implicits_of_global (ConstRef sp)) ++
-  print_argument_scopes (Symbols.find_arguments_scope (ConstRef sp))
+  print_name_infos (ConstRef sp)
 
 let print_inductive sp = (print_mutual sp)
 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 9326ff5382..6b89169b5c 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -183,6 +183,10 @@ let mlexpr_of_red_flags {
   Rawterm.rConst = $mlexpr_of_list mlexpr_of_reference l$
 } >>
 
+let mlexpr_of_explicitation = function
+  | Topconstr.ExplByName id -> <:expr< Topconstr.ExplByName $mlexpr_of_ident id$ >>
+  | Topconstr.ExplByPos n -> <:expr< Topconstr.ExplByPos $mlexpr_of_int n$ >>
+ 
 let rec mlexpr_of_constr = function
   | Topconstr.CRef (Libnames.Ident (loc,id)) when is_meta (string_of_id id) ->
       anti loc (string_of_id id)
@@ -195,7 +199,7 @@ let rec mlexpr_of_constr = function
   | Topconstr.CLambdaN (loc,l,a) -> <:expr< Topconstr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_pair (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
   | Topconstr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
-  | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option mlexpr_of_int)) l$ >>
+  | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option (mlexpr_of_located mlexpr_of_explicitation))) l$ >>
   | Topconstr.CCases (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.COrderedCase (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.CHole loc -> <:expr< Topconstr.CHole $dloc$ >>