Correct implementation of discharging of implicit arguments and add new

setting "Set Manual Implicit Arguments" for manual-only implicits.
Fix test-suite script. This removes the discharge_info argument of
"dynamic" object's rebuild function.


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

8 files changed, 157 insertions, 64 deletions

diff --git a/library/declare.ml b/library/declare.ml
index b524639ef..e250ec282 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -57,10 +57,12 @@ let cache_variable ((sp,_),o) =
   let impl,opaq,cst,keep = match d with (* Fails if not well-typed *)
     | SectionLocalAssum (ty, impl, keep) ->
         let cst = Global.push_named_assum (id,ty) in
-        impl, true, cst, (if keep then Some ty else None)
+	let impl = if impl then Rawterm.Implicit else Rawterm.Explicit in
+	let keep = if keep then Some ty else None in
+	impl, true, cst, keep
     | SectionLocalDef (c,t,opaq) -> 
         let cst = Global.push_named_def (id,c,t) in
-        false, opaq, cst, None in
+        Rawterm.Explicit, opaq, cst, None in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
   add_section_variable id impl keep;
   Dischargedhypsmap.set_discharged_hyps sp [];
@@ -116,7 +118,7 @@ let cache_constant ((sp,kn),(cdt,dhyps,kind)) =
 
 let discharged_hyps kn sechyps =
   let (_,dir,_) = repr_kn kn in
-  let args = array_map_to_list destVar (instance_from_named_context sechyps) in
+  let args = Array.to_list (instance_from_variable_context sechyps) in
   List.rev (List.map (Libnames.make_path dir) args)
 
 let discharge_constant ((sp,kn),(cdt,dhyps,kind)) =
@@ -124,7 +126,7 @@ let discharge_constant ((sp,kn),(cdt,dhyps,kind)) =
   let cb = Global.lookup_constant con in
   let repl = replacement_context () in
   let sechyps = section_segment_of_constant con in
-  let recipe = { d_from=cb; d_modlist=repl; d_abstract=sechyps } in
+  let recipe = { d_from=cb; d_modlist=repl; d_abstract=named_of_variable_context sechyps } in
   Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,kind)
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
@@ -235,7 +237,7 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) =
   let repl = replacement_context () in
   let sechyps = section_segment_of_mutual_inductive kn in
   Some (discharged_hyps kn sechyps,
-        Discharge.process_inductive sechyps repl mie)
+        Discharge.process_inductive (named_of_variable_context sechyps) repl mie)
 
 let dummy_one_inductive_entry mie = {
   mind_entry_typename = mie.mind_entry_typename;
diff --git a/library/heads.ml b/library/heads.ml
index ca1f1014f..1b1dba43f 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -158,7 +158,7 @@ let discharge_head (_,(ref,k)) =
   | EvalConstRef cst -> Some (EvalConstRef (pop_con cst), k)
   | EvalVarRef id -> None
 
-let rebuild_head (info,(ref,k)) =
+let rebuild_head (ref,k) =
   (ref, compute_head ref)
 
 let export_head o = Some o
diff --git a/library/impargs.ml b/library/impargs.ml
index b5c27f430..4759ced46 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -27,6 +27,7 @@ open Topconstr
 
 type implicits_flags = {
   main : bool;
+  manual : bool;                     (* automatic or manual only *)
   strict : bool;                   (* true = strict *)
   strongly_strict : bool;            (* true = strongly strict *)
   reversible_pattern : bool;
@@ -38,6 +39,7 @@ type implicits_flags = {
 
 let implicit_args = ref { 
   main = false;
+  manual = false;
   strict = true;
   strongly_strict = false;
   reversible_pattern = false;
@@ -48,6 +50,10 @@ let implicit_args = ref {
 let make_implicit_args flag =
   implicit_args := { !implicit_args with main = flag }
 
+let make_manual_implicit_args flag =
+  implicit_args := { !implicit_args with main = if flag then true else !implicit_args.main;
+    manual = flag }
+
 let make_strict_implicit_args flag =
   implicit_args := { !implicit_args with strict = flag }
 
@@ -64,6 +70,7 @@ let make_maximal_implicit_args flag =
   implicit_args := { !implicit_args with maximal = flag }
 
 let is_implicit_args () = !implicit_args.main
+let is_manual_implicit_args () = !implicit_args.manual
 let is_strict_implicit_args () = !implicit_args.strict
 let is_strongly_strict_implicit_args () = !implicit_args.strongly_strict
 let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern
@@ -245,10 +252,6 @@ let compute_implicits_flags env f all t =
 let set_implicit id imp insmax =
   (id,(match imp with None -> Manual | Some imp -> imp),insmax)
 
-let merge_imps f = function 
-    None -> Some Manual
-  | x -> x
-
 let rec assoc_by_pos k = function
     (ExplByPos (k', x), b) :: tl when k = k' -> (x,b), tl
   | hd :: tl -> let (x, tl) = assoc_by_pos k tl in x, hd :: tl
@@ -307,11 +310,15 @@ let compute_manual_implicits env flags t enriching l =
   in
   merge 1 l autoimps
 
+let const v _ = v
+
 let compute_implicits_auto env f manual t =
   match manual with
-      [] -> let l = compute_implicits_flags env f false t in
-	      prepare_implicits f l
-    | _ -> compute_manual_implicits env f t true manual
+  | [] -> 
+      let l = compute_implicits_flags env f false t in
+	if f.manual then List.map (const None) l
+	else prepare_implicits f l
+  | _ -> compute_manual_implicits env f t (not f.manual) manual
 	
 let compute_implicits env t = compute_implicits_auto env !implicit_args [] t
 
@@ -415,12 +422,18 @@ let list_split_at index l =
     | [] -> failwith "list_split_at: Invalid argument"
   in aux 0 [] l
     
-let merge_impls newimpls oldimpls =
-  let before, after = list_split_at (List.length newimpls - List.length oldimpls) newimpls in
+let merge_impls oldimpls newimpls =
+  let (before, news), olds = 
+    let len = List.length newimpls - List.length oldimpls in
+      if len >= 0 then list_split_at len newimpls, oldimpls
+      else 
+	let before, after = list_split_at (-len) oldimpls in
+	  (before, newimpls), after
+  in
     before @ (List.map2 (fun orig ni ->
       match orig with
       | Some (_, Manual, _) -> orig
-      | _ -> ni) oldimpls after)
+      | _ -> ni) olds news)
 
 (* Caching implicits *)
 
@@ -454,34 +467,67 @@ let subst_implicits_decl subst (r,imps as o) =
 let subst_implicits (_,subst,(req,l)) =
   (ImplLocal,list_smartmap (subst_implicits_decl subst) l)
 
+let impls_of_context ctx =
+  List.rev_map (fun (id,impl,_,_) -> if impl = Rawterm.Implicit then Some (id, Manual, true) else None)
+    (List.filter (fun (_,_,b,_) -> b = None) ctx)
+
+let section_segment_of_reference = function
+  | ConstRef con -> section_segment_of_constant con
+  | IndRef (kn,_) | ConstructRef ((kn,_),_) ->
+      section_segment_of_mutual_inductive kn
+  | _ -> []
+
 let discharge_implicits (_,(req,l)) =
   match req with
   | ImplLocal -> None
   | ImplInteractive (ref,flags,exp) -> 
-      Some (ImplInteractive (pop_global_reference ref,flags,exp),l)
+      let vars = section_segment_of_reference ref in
+      let ref' = pop_global_reference ref in
+      let l' = [ref', impls_of_context vars @ snd (List.hd l)] in
+      Some (ImplInteractive (ref',flags,exp),l')
   | ImplConstant (con,flags) ->
-      Some (ImplConstant (pop_con con,flags),l)
+      let con' = pop_con con in
+      let l' = [ConstRef con',impls_of_context (section_segment_of_constant con) @ snd (List.hd l)] in
+	Some (ImplConstant (con',flags),l')
   | ImplMutualInductive (kn,flags) ->
-      Some (ImplMutualInductive (pop_kn kn,flags),l)
+      let l' = List.map (fun (gr, l) -> 
+	let vars = section_segment_of_reference gr in
+	  (pop_global_reference gr, impls_of_context vars @ l)) l 
+      in
+	Some (ImplMutualInductive (pop_kn kn,flags),l')
 
-let rebuild_implicits (info,(req,l)) =
-  let manual = List.fold_left (fun acc (id, impl, keep) -> 
-    if impl then (ExplByName id, (true, true)) :: acc else acc)
-    [] info
-  in
+let rebuild_implicits (req,l) =
   let l' = match req with
   | ImplLocal -> assert false
   | ImplConstant (con,flags) -> 
-      [ConstRef con, compute_constant_implicits flags manual con]
+      let oldimpls = snd (List.hd l) in
+      let newimpls = compute_constant_implicits flags [] con in
+      [ConstRef con, merge_impls oldimpls newimpls]
   | ImplMutualInductive (kn,flags) ->
-      compute_all_mib_implicits flags manual kn
+      let newimpls = compute_all_mib_implicits flags [] kn in
+      let rec aux olds news = 
+	match olds, news with
+	| (_, oldimpls) :: old, (gr, newimpls) :: tl ->
+	    (gr, merge_impls oldimpls newimpls) :: aux old tl
+	| [], [] -> []
+	| _, _ -> assert false
+      in aux l newimpls
+
   | ImplInteractive (ref,flags,o) ->
       match o with
-      | ImplAuto -> [ref,compute_global_implicits flags manual ref]
-      | ImplManual l -> 
-	  let auto = compute_global_implicits flags manual ref in
-(* 	  let auto = if flags.main then auto else List.map (fun _ -> None) auto in *)
-	  let l' = merge_impls auto l in [ref,l']
+      | ImplAuto -> 
+	  let oldimpls = snd (List.hd l) in
+	  let newimpls = compute_global_implicits flags [] ref in
+	    [ref,merge_impls oldimpls newimpls]
+      | ImplManual m -> 
+	  let oldimpls = snd (List.hd l) in
+	  let auto = 
+	    if flags.main then
+	      let newimpls = compute_global_implicits flags [] ref in
+		merge_impls oldimpls newimpls
+	    else oldimpls
+	  in
+	  let l' = merge_impls auto m in [ref,l']
   in (req,l')
 
 let export_implicits (req,_ as x) = 
diff --git a/library/impargs.mli b/library/impargs.mli
index 5bfa0470d..353f657c6 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -20,6 +20,7 @@ open Nametab
     are outside the kernel, which knows nothing about implicit arguments. *)
 
 val make_implicit_args : bool -> unit
+val make_manual_implicit_args : bool -> unit
 val make_strict_implicit_args : bool -> unit
 val make_strongly_strict_implicit_args : bool -> unit
 val make_reversible_pattern_implicit_args : bool -> unit
@@ -27,6 +28,7 @@ val make_contextual_implicit_args : bool -> unit
 val make_maximal_implicit_args : bool -> unit
 
 val is_implicit_args : unit -> bool
+val is_manual_implicit_args : unit -> bool
 val is_strict_implicit_args : unit -> bool
 val is_strongly_strict_implicit_args : unit -> bool
 val is_reversible_pattern_implicit_args : unit -> bool
@@ -38,10 +40,20 @@ val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b
 
 (*s An [implicits_list] is a list of positions telling which arguments
     of a reference can be automatically infered *)
-type implicit_status
-type implicits_list = implicit_status list
 
-type implicit_explanation
+
+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
+
+type implicit_status = (identifier * implicit_explanation * bool) option
+type implicits_list = implicit_status list
 
 val is_status_implicit : implicit_status -> bool
 val is_inferable_implicit : bool -> int -> implicit_status -> bool
@@ -84,3 +96,28 @@ val maybe_declare_manual_implicits : bool -> global_reference -> bool ->
 val implicits_of_global : global_reference -> implicits_list
 
 val lift_implicits : int -> manual_explicitation list -> manual_explicitation list
+
+val merge_impls : implicits_list -> implicits_list -> implicits_list
+
+type implicit_interactive_request =
+  | ImplAuto
+  | ImplManual of implicit_status list
+
+type implicit_discharge_request =
+  | ImplLocal
+  | ImplConstant of constant * implicits_flags
+  | ImplMutualInductive of kernel_name * implicits_flags
+  | ImplInteractive of global_reference * implicits_flags * 
+      implicit_interactive_request
+
+val discharge_implicits :     'a *
+    (implicit_discharge_request *
+     (Libnames.global_reference *
+      (Names.identifier * implicit_explanation * bool) option list)
+     list) ->
+    (implicit_discharge_request *
+     (Libnames.global_reference *
+      (Names.identifier * implicit_explanation * bool) option list)
+     list)
+    option
+
diff --git a/library/lib.ml b/library/lib.ml
index 4743290ae..31b94cc96 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -216,9 +216,9 @@ let add_leaf id obj =
   add_entry oname (Leaf obj);
   oname
 
-let add_discharged_leaf id varinfo obj =
+let add_discharged_leaf id obj =
   let oname = make_oname id in
-  let newobj = rebuild_object (varinfo, obj) in
+  let newobj = rebuild_object obj in
   cache_object (oname,newobj);
   add_entry oname (Leaf newobj)
 
@@ -439,10 +439,12 @@ let what_is_opened () = find_entry_p is_something_opened
    - the list of substitution to do at section closing 
 *)
 
-type abstr_list = Sign.named_context Names.Cmap.t * Sign.named_context Names.KNmap.t
+type variable_info = Names.identifier * Rawterm.binding_kind * Term.constr option * Term.types
+type variable_context = variable_info list
+type abstr_list = variable_context Names.Cmap.t * variable_context Names.KNmap.t
 
 let sectab =
-  ref ([] : ((Names.identifier * bool * Term.types option) list * Cooking.work_list * abstr_list) list)
+  ref ([] : ((Names.identifier * Rawterm.binding_kind * Term.types option) list * Cooking.work_list * abstr_list) list)
 
 let add_section () =
   sectab := ([],(Names.Cmap.empty,Names.KNmap.empty),(Names.Cmap.empty,Names.KNmap.empty)) :: !sectab
@@ -453,25 +455,34 @@ let add_section_variable id impl keep =
     | (vars,repl,abs)::sl -> sectab := ((id,impl,keep)::vars,repl,abs)::sl
 
 let rec extract_hyps = function
-  | ((id,impl,keep)::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps)
-  | ((id,impl,Some ty)::idl,hyps) -> (id,None,ty) :: extract_hyps (idl,hyps)
+  | ((id,impl,keep)::idl,(id',b,t)::hyps) when id=id' -> (id',impl,b,t) :: extract_hyps (idl,hyps)
+  | ((id,impl,Some ty)::idl,hyps) -> (id,impl,None,ty) :: extract_hyps (idl,hyps)
   | (id::idl,hyps) -> extract_hyps (idl,hyps)
   | [], _ -> []
 
+let instance_from_variable_context sign =
+  let rec inst_rec = function
+    | (id,b,None,_) :: sign -> id :: inst_rec sign
+    | _ :: sign -> inst_rec sign
+    | [] -> [] in
+  Array.of_list (inst_rec sign)
+
+let named_of_variable_context = List.map (fun (id,_,b,t) -> (id,b,t))
+
 let add_section_replacement f g hyps =
   match !sectab with
   | [] -> ()
   | (vars,exps,abs)::sl ->
     let sechyps = extract_hyps (vars,hyps) in
-    let args = Sign.instance_from_named_context (List.rev sechyps) in
-    sectab := (vars,f (Array.map Term.destVar args) exps,g sechyps abs)::sl
+    let args = instance_from_variable_context (List.rev sechyps) in
+    sectab := (vars,f args exps,g sechyps abs)::sl
 	
 let add_section_kn kn =
-  let f = (fun x (l1,l2) -> (l1,Names.KNmap.add kn x l2)) in
+  let f x (l1,l2) = (l1,Names.KNmap.add kn x l2) in
   add_section_replacement f f
 
 let add_section_constant kn =
-  let f = (fun x (l1,l2) -> (Names.Cmap.add kn x l1,l2)) in
+  let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
   add_section_replacement f f
 
 let replacement_context () = pi2 (List.hd !sectab)
@@ -562,10 +573,6 @@ let close_section id =
     with Not_found ->
       error "no opened section"
   in
-  let var_info = List.map
-    (fun (x, y, z) -> (x, y, match z with Some _ -> true | None -> false))
-    (variables_context ())
-  in
   let (secdecls,secopening,before) = split_lib oname in
   lib_stk := before;
   let full_olddir = fst !path_prefix in
@@ -574,7 +581,7 @@ let close_section id =
   if !Flags.xml_export then !xml_close_section id;
   let newdecls = List.map discharge_item secdecls in
   Summary.section_unfreeze_summaries fs;
-  List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id var_info o)) newdecls;
+  List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
   Cooking.clear_cooking_sharing ();
   Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir)
 
diff --git a/library/lib.mli b/library/lib.mli
index c13f7f62d..42a68f0ed 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -168,14 +168,19 @@ val set_xml_close_section : (Names.identifier -> unit) -> unit
 
 
 (*s Section management for discharge *)
+type variable_info = Names.identifier * Rawterm.binding_kind * Term.constr option * Term.types
+type variable_context = variable_info list
 
-val section_segment_of_constant : Names.constant -> Sign.named_context
-val section_segment_of_mutual_inductive: Names.mutual_inductive -> Sign.named_context
+val instance_from_variable_context : variable_context -> Names.identifier array
+val named_of_variable_context : variable_context -> Sign.named_context
+
+val section_segment_of_constant : Names.constant -> variable_context
+val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_context
 
 val section_instance : Libnames.global_reference -> Names.identifier array
 val is_in_section : Libnames.global_reference -> bool
 
-val add_section_variable : Names.identifier -> bool -> Term.types option -> unit
+val add_section_variable : Names.identifier -> Rawterm.binding_kind -> Term.types option -> unit
 val add_section_constant : Names.constant -> Sign.named_context -> unit
 val add_section_kn : Names.kernel_name -> Sign.named_context -> unit
 val replacement_context : unit ->
diff --git a/library/libobject.ml b/library/libobject.ml
index b24a46e38..684607b4b 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -28,8 +28,6 @@ let relax b = relax_flag := b;;
 type 'a substitutivity = 
     Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
 
-type discharge_info = (identifier * bool * bool) list
-
 type 'a object_declaration = {
   object_name : string;
   cache_function : object_name * 'a -> unit;
@@ -38,7 +36,7 @@ type 'a object_declaration = {
   classify_function : object_name * 'a -> 'a substitutivity;
   subst_function : object_name * substitution * 'a -> 'a;
   discharge_function : object_name * 'a -> 'a option;
-  rebuild_function : discharge_info * 'a -> 'a;
+  rebuild_function : 'a -> 'a;
   export_function : 'a -> 'a option }
 
 let yell s = anomaly s
@@ -52,7 +50,7 @@ let default_object s = {
     yell ("The object "^s^" does not know how to substitute!"));
   classify_function = (fun (_,obj) -> Keep obj);
   discharge_function = (fun _ -> None);
-  rebuild_function = (fun (_,x) -> x);
+  rebuild_function = (fun x -> x);
   export_function = (fun _ -> None)} 
 
 
@@ -78,7 +76,7 @@ type dynamic_object_declaration = {
   dyn_subst_function : object_name * substitution * obj -> obj;
   dyn_classify_function : object_name * obj -> obj substitutivity;
   dyn_discharge_function : object_name * obj -> obj option;
-  dyn_rebuild_function : discharge_info * obj -> obj;
+  dyn_rebuild_function : obj -> obj;
   dyn_export_function : obj -> obj option }
 
 let object_tag lobj = Dyn.tag lobj
@@ -116,8 +114,8 @@ let declare_object odecl =
       Option.map infun (odecl.discharge_function (oname,outfun lobj))
     else 
       anomaly "somehow we got the wrong dynamic object in the dischargefun"
-  and rebuild (varinfo,lobj) = 
-    if Dyn.tag lobj = na then infun (odecl.rebuild_function (varinfo,outfun lobj))
+  and rebuild lobj = 
+    if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj))
     else anomaly "somehow we got the wrong dynamic object in the rebuildfun"
   and exporter lobj = 
     if Dyn.tag lobj = na then 
@@ -174,7 +172,7 @@ let classify_object ((_,lobj) as node) =
 let discharge_object ((_,lobj) as node) = 
   apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj
 
-let rebuild_object ((_,lobj) as node) =
+let rebuild_object (lobj as node) =
   apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function node) lobj
 
 let export_object lobj =
diff --git a/library/libobject.mli b/library/libobject.mli
index 33ad67c84..61e650e6b 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -71,8 +71,6 @@ open Mod_subst
 type 'a substitutivity = 
     Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
 
-type discharge_info = (identifier * bool * bool) list
-
 type 'a object_declaration = {
   object_name : string;
   cache_function : object_name * 'a -> unit;
@@ -81,7 +79,7 @@ type 'a object_declaration = {
   classify_function : object_name * 'a -> 'a substitutivity;
   subst_function : object_name * substitution * 'a -> 'a;
   discharge_function : object_name * 'a -> 'a option;
-  rebuild_function : discharge_info * 'a -> 'a;
+  rebuild_function : 'a -> 'a;
   export_function : 'a -> 'a option }
 
 (* The default object is a "Keep" object with empty methods. 
@@ -116,5 +114,5 @@ val subst_object : object_name * substitution * obj -> obj
 val classify_object : object_name * obj -> obj substitutivity
 val export_object : obj -> obj option
 val discharge_object : object_name * obj -> obj option
-val rebuild_object : discharge_info * obj -> obj
+val rebuild_object : obj -> obj
 val relax : bool -> unit