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

10 files changed, 215 insertions, 78 deletions

diff --git a/CHANGES b/CHANGES
index eb0738d116..0900445c97 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,10 +1,17 @@
 Changes from V7.3.1 to ????
 -------------------------
 
+TODO: unification 2eme ordre avec NewDestruct
+
 Symbolic notations
 
 - Introduction of a notion of scope gathering notations in a consistent set;
   set a notation sets has been developped for nat, Z and R
+- Declarations with only implicit arguments now handled (e.g. the
+  argument of nil can be set implicit; use !nil to refer to nil
+  without arguments)
+- New defensive strategy for printing or not implicit arguments to ensure
+  re-type-checkability of the printed term
 
 Library
 
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 0ae3b2d821..ef232d0dca 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -42,7 +42,7 @@ let convert_env =
 
 (* This function is directly inspired by print_impl_args in pretty.ml *)
 
-let impl_args_to_string = function
+let impl_args_to_string_by_pos = function
     [] -> None
   | [i] -> Some(" position " ^ (string_of_int i) ^ " is implicit.")
   | l -> Some (" positions " ^
@@ -52,6 +52,9 @@ let impl_args_to_string = function
 
 (* This function is directly inspired by implicit_args_id in pretty.ml *)
 
+let impl_args_to_string l = 
+  impl_args_to_string_by_pos (positions_of_implicits l)
+
 let implicit_args_id_to_ast_list id l ast_list = 
     (match impl_args_to_string l with
            None -> ast_list
diff --git a/library/impargs.ml b/library/impargs.ml
index 86535370ae..cc9d3f8cae 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -20,41 +20,144 @@ open Libobject
 open Lib
 open Nametab
 
-(* calcul des arguments implicites *)
-
-(* la seconde liste est ordonne'e *)
-
-let ord_add x l =
-  let rec aux l = match l with 
-    | []    -> [x]
-    | y::l' -> if y > x then x::l else if x = y then l else y::(aux l')
-  in 
-  aux l
-    
-let add_free_rels_until bound m acc =
-  let rec frec depth acc c = match kind_of_term c with
+(*s Calcul arguments implicites *)
+
+(* We remember various information about why an argument is (automatically)
+   inferable as implicit
+
+- [DepRigid] means that the implicit argument can be found by
+  unification along a rigid path (we do not print the arguments of
+  this kind if there is enough arguments to infer them)
+
+- [DepFlex] means that the implicit argument can be found by unification
+  along a collapsable path only (e.g. as x in (P x) where P is another
+  argument) (we do (defensively) print the arguments of this kind)
+
+- [DepFlexAndRigid] means that the least argument from which the
+  implicit argument can be inferred is following a collapsable path
+  but there is a greater argument from where the implicit argument is
+  inferable following a rigid path (useful to know how to print a
+  partial application)
+
+  We also consider arguments inferable from the conclusion but it is
+  operational only if [conclusion_matters] is true.
+*)
+
+type argument_position =
+  | Conclusion
+  | Hyp of int
+
+type implicit_explanation =
+  | DepRigid of argument_position
+  | DepFlex of argument_position
+  | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position
+  | Manual
+
+(* Set this to true to have arguments inferable from conclusion only implicit*)
+let conclusion_matters = false
+
+let argument_less = function
+  | Hyp n, Hyp n' -> n<n'
+  | Hyp _, Conclusion -> true
+  | Conclusion, _ -> false
+
+let update pos rig st =
+  let e =
+  if rig then
+    match st with
+      | None -> DepRigid pos
+      | Some (DepRigid n as x) ->
+          if argument_less (pos,n) then DepRigid pos else x
+      | Some (DepFlexAndRigid (fpos,rpos) as x) ->
+          if argument_less (pos,fpos) or pos=fpos then DepRigid pos else
+          if argument_less (pos,rpos) then DepFlexAndRigid (fpos,pos) else x
+      | Some (DepFlex fpos as x) ->
+          if argument_less (pos,fpos) or pos=fpos then DepRigid pos
+          else DepFlexAndRigid (fpos,pos)
+      | Some Manual -> assert false
+  else
+    match st with
+      | None -> DepFlex pos
+      | Some (DepRigid rpos as x) ->
+          if argument_less (pos,rpos) then DepFlexAndRigid (pos,rpos) else x
+      | Some (DepFlexAndRigid (fpos,rpos) as x) ->
+          if argument_less (pos,fpos) then DepFlexAndRigid (pos,rpos) else x
+      | Some (DepFlex fpos as x) ->
+          if argument_less (pos,fpos) then DepFlex pos else x
+      | Some Manual -> assert false
+  in Some e
+
+(* modified is_rigid_reference with a truncated env *)
+let is_flexible_reference env bound depth f =
+  match kind_of_term f with
+    | Rel n when n >= bound+depth -> (* inductive type *) false
+    | Rel n when n >= depth -> (* previous argument *) true
+    | Rel n -> (* internal variable [TODO: deal local definitions] *) false
+    | Const kn ->
+        let cb = Environ.lookup_constant kn env in
+        cb.const_body <> None & not cb.const_opaque
+    | Var id ->
+        let (_,value,_) = Environ.lookup_named id env in value <> None
+    | Ind _ | Construct _ -> false
+    |  _ -> true
+
+(* Precondition: rels in env are for inductive types only *)
+let add_free_rels_until bound env m pos acc =
+  let rec frec rig depth c = match kind_of_term c with
     | Rel n when (n < bound+depth) & (n >= depth) ->
-	Intset.add (bound+depth-n) acc
-    | _ -> fold_constr_with_binders succ frec depth acc c
+        acc.(bound+depth-n-1) <- update pos rig (acc.(bound+depth-n-1))
+    | App (f,_) when rig & is_flexible_reference env bound depth f ->
+        iter_constr_with_binders succ (frec false) depth c
+    | Case _ ->
+        iter_constr_with_binders succ (frec false) depth c
+    | _ ->
+        iter_constr_with_binders succ (frec rig) depth c
   in 
-  frec 1 acc m 
+  frec true 1 m; acc
 
 (* calcule la liste des arguments implicites *)
 
 let compute_implicits env t =
   let rec aux env n t =
-    match kind_of_term (whd_betadeltaiota env t) with
+    let t = whd_betadeltaiota env t in
+    match kind_of_term t with
       | Prod (x,a,b) ->
-	  add_free_rels_until n a
-	    (aux (push_rel (x,None,a) env) (n+1) b)
-      | _ -> Intset.empty
+	  add_free_rels_until n env a (Hyp (n+1))
+            (aux (push_rel (x,None,a) env) (n+1) b)
+      | _ -> 
+          add_free_rels_until n env t Conclusion (Array.create n None)
   in 
   match kind_of_term (whd_betadeltaiota env t) with 
     | Prod (x,a,b) ->
-	Intset.elements (aux (push_rel (x,None,a) env) 1 b)
+	Array.to_list (aux (push_rel (x,None,a) env) 1 b)
     | _ -> []
 
-type implicits_list = int list
+type implicit_status = implicit_explanation option (* None = Not implicit *)
+
+type implicits_list = implicit_status list
+
+let is_status_implicit = function
+  | None -> false
+  | Some (DepRigid Conclusion) -> conclusion_matters
+  | Some (DepFlex Conclusion) -> conclusion_matters
+  | _ -> true
+
+let is_inferable_implicit n = function
+  | None -> false
+  | Some (DepRigid (Hyp p)) -> n >= p
+  | Some (DepFlex (Hyp p)) -> false
+  | Some (DepFlexAndRigid (_,Hyp q)) -> n >= q
+  | Some (DepRigid Conclusion) -> conclusion_matters
+  | Some (DepFlex Conclusion) -> false
+  | Some (DepFlexAndRigid (_,Conclusion)) -> false
+  | Some Manual -> true
+
+let positions_of_implicits =
+  let rec aux n = function
+      [] -> []
+    | Some _::l -> n :: aux (n+1) l
+    | None::l -> aux (n+1) l
+  in aux 1
 
 type implicits =
   | Impl_auto of implicits_list
@@ -301,15 +404,20 @@ let declare_manual_implicits r l =
   if not (list_distinct l) then error ("Some numbers occur several time");
   List.iter (check_range n) l;
   let l = List.sort (-) l in
+  let rec aux k = function
+    | [] -> if k>n then [] else None :: aux (k+1) []
+    | p::l as l' ->
+        if k=p then Some Manual :: aux (k+1) l else None :: aux (k+1) l'
+  in let l = Impl_manual (aux 1 l) in
   match r with
   | VarRef id -> 
-      add_anonymous_leaf (in_var_implicits (id,Impl_manual l))
+      add_anonymous_leaf (in_var_implicits (id,l))
   | ConstRef sp ->
-      add_anonymous_leaf (in_constant_implicits (sp,Impl_manual l))
+      add_anonymous_leaf (in_constant_implicits (sp,l))
   | IndRef indp ->
-      add_anonymous_leaf (in_inductive_implicits (indp,Impl_manual l))
+      add_anonymous_leaf (in_inductive_implicits (indp,l))
   | ConstructRef consp -> 
-      add_anonymous_leaf (in_constructor_implicits (consp,Impl_manual l))
+      add_anonymous_leaf (in_constructor_implicits (consp,l))
 
 (*s Tests if declared implicit *)
 
diff --git a/library/impargs.mli b/library/impargs.mli
index 751d968447..bf8e1b3852 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -26,7 +26,12 @@ val with_implicits : bool -> ('a -> 'b) -> 'a -> 'b
 
 (*s An [implicits_list] is a list of positions telling which arguments
     of a reference can be automatically infered *)
-type implicits_list = int list
+type implicit_status
+type implicits_list = implicit_status list
+
+val is_status_implicit : implicit_status -> bool
+val is_inferable_implicit : int -> implicit_status -> bool
+val positions_of_implicits : implicits_list -> int list
 
 (* Computation of the positions of arguments automatically inferable
    for an object of the given type in the given env *)
@@ -40,7 +45,7 @@ val declare_mib_implicits : mutual_inductive -> unit
 val declare_implicits : global_reference -> unit
 
 (* Manual declaration of which arguments are expected implicit *)
-val declare_manual_implicits : global_reference -> implicits_list -> unit
+val declare_manual_implicits : global_reference -> int list -> unit
 
 (*s Access to already computed implicits. *)
 
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
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v
index 4b91f8c7b7..ddfbceb835 100755
--- a/syntax/PPConstr.v
+++ b/syntax/PPConstr.v
@@ -181,18 +181,18 @@ Syntax constr
   | apptailcons [ << (APPTAIL $H ($LIST $T)) >> ]
 	 -> [ [1 1] $H:L  (APPTAIL ($LIST $T)):E ]
   | apptailnil [ << (APPTAIL) >> ] -> [ ]
-  | apptailcons1  [ << (APPTAIL (EXPL "!" $n $c1) ($LIST $T)) >> ]
-         -> [ [1 1] (EXPL $n $c1):L  (APPTAIL ($LIST $T)):E ]
-
-  ;
 
 (* Implicits *)
+  | apptailcons1  [ << (APPTAIL (EXPL $n $c1) ($LIST $T)) >> ]
+         -> [ [1 1] $n "!" $c1:E  (APPTAIL ($LIST $T)):E ]
+  ;
+(*
   level 8:
     arg_implicit [ << (EXPL ($NUM $n) $c1) >> ] -> [ $n "!" $c1:L ]
 (*  | arg_implicit1 [(EXPL "EX" ($NUM $n) $c1)] -> [ $n "!" $c1:L ]
   | fun_explicit [ << (EXPL $f) >> ] -> [ $f ]*)
   ;
-
+*)
 
   level 8:
   recterm [ << (MATCH $P $c ($LIST $BL)) >> ] ->