Des critères plus fins d'analyse des implicites automatiques; meilleur affichage des implicites en cas d'application partielle ou inférence via une position flexible; gestion des implicites en positions terminales pour anticiper sur un implicite dans nil et cie

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

5 files changed, 58 insertions, 44 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index e1efe655a7..bbd9b49e6d 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -433,10 +433,23 @@ let set_hole_implicit i = function
   | RVar (loc,id) -> (loc,ImplicitArg (VarRef id,i))
   | _ -> anomaly "Only refs have implicits"
 
+(*
+let check_only_implicits t imp =
+  let rec aux env n t =
+    match kind_of_term (whd_betadeltaiota env t) with
+      | Prod (x,a,b) -> (aux (push_rel (x,None,a) env) (n+1) b)
+      | _ -> n
+  in 
+  let env = Global.env () in
+  imp = interval 1 (aux env 0 (get_type_of env Evd.empty t))
+*)
+
 let build_expression loc1 loc2 (ref,impls) args =
   let rec add_args n = function
-    | true::impls,args -> (RHole (set_hole_implicit n (RRef (loc2,ref))))::add_args (n+1) (impls,args)
-    | false::impls,a::args -> a::add_args (n+1) (impls,args)
+    | imp::impls,args when is_status_implicit imp ->
+        (RHole (set_hole_implicit n (RRef (loc2,ref))))
+        ::add_args (n+1) (impls,args)
+    | _::impls,a::args -> a::add_args (n+1) (impls,args)
     | [], args -> args
     | _ -> anomalylabstrm "astterm"
       (str "Incorrect signature " ++ pr_global_env None ref ++ str " as an infix") in
@@ -448,7 +461,12 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	rawconstr_of_var env lvar loc s
 
     | Node(loc,"QUALID", l) ->
-        rawconstr_of_qualid env lvar loc (interp_qualid l)
+        let (c,imp,subscopes) =
+          rawconstr_of_qualid_gen env lvar loc (interp_qualid l)
+        in
+        (match ast_to_impargs c env imp subscopes [] with
+            [] -> c
+          | l -> RApp (loc, c, l))
   
     | Node(loc,"FIX", (Nvar (locid,iddef))::ldecl) ->
 	let (lf,ln,lA,lt) = ast_to_fix ldecl in
@@ -614,26 +632,29 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
     let rec aux n l subscopes args =
       let (enva,subscopes') = apply_scope_env env subscopes in
       match (l,args) with 
-      | (i::l',Node(loc, "EXPL", [Num(_,j);a])::args') ->
-	  if i=n & j>=i then
-	    if j=i then
+      | (imp::l',Node(loc, "EXPL", [Num(_,j);a])::args') ->
+	  if is_status_implicit imp & j>=n then
+	    if j=n then
 	      (dbrec enva a)::(aux (n+1) l' subscopes' args')
 	    else 
-	      (RHole (set_hole_implicit i c))::(aux (n+1) l' subscopes' args)
+	      (RHole (set_hole_implicit n c))::(aux (n+1) l' subscopes' args)
 	  else 
-	    if i<>n then
+	    if not (is_status_implicit imp) then
 	      error ("Bad explicitation number: found "^
 		   (string_of_int j)^" but was expecting a regular argument")
 	    else
 	      error ("Bad explicitation number: found "^
-		   (string_of_int j)^" but was expecting "^(string_of_int i))
-      | (i::l',a::args') -> 
-	  if i=n then 
-	    (RHole (set_hole_implicit i c))::(aux (n+1) l' subscopes' args)
+		   (string_of_int j)^" but was expecting "^(string_of_int n))
+      | (imp::l',a::args') -> 
+	  if is_status_implicit imp then 
+	    (RHole (set_hole_implicit n c))::(aux (n+1) l' subscopes' args)
 	  else 
-	    (dbrec enva a)::(aux (n+1) l subscopes' args')
+	    (dbrec enva a)::(aux (n+1) l' subscopes' args')
       | ([],args) -> ast_to_args env subscopes args
-      | (_,[]) -> []
+      | (_::l',[]) ->
+          if List.for_all is_status_implicit l then
+            (RHole (set_hole_implicit n c))::(aux (n+1) l' subscopes args)
+          else []
     in 
     aux 1 l subscopes args
 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 4f8cbaa8c7..55aa143376 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -194,11 +194,11 @@ GEXTEND Gram
           <:ast<(IMPLICITBINDINGS $c1 ($LIST $bl))>> ] ]
   ;
   constr10:
-    [ [ "!"; f = global; args = ne_constr9_list ->
+    [ [ "!"; f = global; args = LIST0 constr9 ->
           <:ast< (APPLISTEXPL $f ($LIST $args)) >>
       | "!"; f = global; "with"; b = binding_list ->
 	  <:ast< (APPLISTWITH $f $b) >>
-      | f = constr9; args = ne_constr91_list ->
+      | f = constr9; args = LIST1 constr91 ->
           <:ast< (APPLIST $f ($LIST $args)) >>
       | f = constr9 -> f ] ]
   ;
@@ -247,14 +247,6 @@ GEXTEND Gram
 	  let n = Coqast.Str (loc,n) in <:ast< (NUMERAL $n) >>
       | c1 = constr9 -> c1 ] ]
   ;
-  ne_constr91_list:
-    [ [ c1 = constr91; cl = ne_constr91_list -> c1::cl
-      | c1 = constr91 -> [c1] ] ]
-  ;
-  ne_constr9_list:
-    [ [ c1 = constr9; cl = ne_constr9_list -> c1::cl
-      | c1 = constr9 -> [c1] ] ]
-  ;
   fixbinder:
     [ [ id = ident; "/"; recarg = Prim.natural; ":"; type_ = constr;
         ":="; def = constr ->
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 8a241aced3..55611ec28f 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -39,7 +39,7 @@ let print_typed_value_in_env env (trm,typ) =
 
 let print_typed_value x = print_typed_value_in_env (Global.env ()) x
 			  		  
-let print_impl_args = function
+let print_impl_args_by_pos = function
   | []  -> mt ()
   | [i] -> str"Position [" ++ int i ++ str"] is implicit"
   | l   -> 
@@ -47,6 +47,8 @@ let print_impl_args = function
       prlist_with_sep (fun () -> str "; ") int l ++
       str"] are implicit"
 
+let print_impl_args l = print_impl_args_by_pos (positions_of_implicits l)
+
 (* 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)
@@ -72,11 +74,11 @@ let print_named_decl (id,c,typ) =
 let assumptions_for_print lna =
   List.fold_right (fun na env -> add_name na env) lna empty_names_context
 
-let implicit_args_id id l = 
-  if l = [] then 
-    (mt ())
-  else 
+let implicit_args_id id l =
+  if List.exists is_status_implicit l then 
     (str"For " ++ pr_id id ++ str": " ++ print_impl_args l ++ fnl ())
+  else 
+    (mt ())
 
 let implicit_args_msg sp mipv = 
   (prvecti
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index 4f3c1269e7..2d175f1f96 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -25,7 +25,7 @@ open Nametab
 val assumptions_for_print : name list -> Termops.names_context
 
 val print_closed_sections : bool ref
-val print_impl_args : int list -> std_ppcmds
+val print_impl_args : Impargs.implicits_list -> std_ppcmds
 val print_context : bool -> Lib.library_segment -> std_ppcmds
 val print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds
 val print_full_context : unit -> std_ppcmds
diff --git a/parsing/termast.ml b/parsing/termast.ml
index d30e03903b..1b9c387582 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -144,20 +144,19 @@ let decompose_binder = function
   | _ -> None
 
 (* Implicit args indexes are in ascending order *)
-let explicitize =
-  let rec exprec n lastimplargs impl = function
-    | a::args ->
-	(match impl with
-	   | i::l when i=n ->
-	       exprec (n+1) (ope("EXPL", [num i; a])::lastimplargs) l args
-	   | _ ->
-	       let tail = a::(exprec (n+1) [] impl args) in
-	       if (!print_implicits & !print_implicits_explicit_args) then
-		 List.rev_append lastimplargs tail
-	       else tail)
-    (* Tail impl args are always printed even if implicit printing is off *)
-    | [] -> List.rev lastimplargs
-  in exprec 1 []
+let explicitize impl args =
+  let n = List.length args in
+  let rec exprec q = function
+    | a::args, imp::impl when is_status_implicit imp ->
+        let tail = exprec (q+1) (args,impl) in
+        let visible =
+          (!print_implicits & !print_implicits_explicit_args)
+          or not (is_inferable_implicit n imp) in
+        if visible then ope("EXPL", [num q; a]) :: tail else tail
+    | a::args, _::impl -> a :: exprec (q+1) (args,impl)
+    | args, [] -> args  (* In case of polymorphism *)
+    | [], _ -> []
+  in exprec 1 (args,impl)
 
 let rec skip_coercion dest_ref (f,args as app) =
   if !print_coercions then app