Merge branch 'v8.5'

5 files changed, 121 insertions, 107 deletions

diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 4aa3c3bfd..b1fba132d 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -117,7 +117,8 @@ val set_end_tac : Tacexpr.raw_tactic_expr -> unit
 (** {6 ... } *)
 (** [set_used_variables l] declares that section variables [l] will be
     used in the proof *)
-val set_used_variables : Id.t list -> Context.section_context
+val set_used_variables :
+  Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list
 val get_used_variables : unit -> Context.section_context option
 
 (** {6 ... } *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index b5e25cc7c..96c80f263 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -253,17 +253,43 @@ let start_dependent_proof id str goals terminator =
 
 let get_used_variables () = (cur_pstate ()).section_vars
 
+let proof_using_auto_clear = ref true
+let _ = Goptions.declare_bool_option
+    { Goptions.optsync  = true;
+      Goptions.optdepr  = false;
+      Goptions.optname  = "Proof using Clear Unused";
+      Goptions.optkey   = ["Proof";"Using";"Clear";"Unused"];
+      Goptions.optread  = (fun () -> !proof_using_auto_clear);
+      Goptions.optwrite = (fun b -> proof_using_auto_clear := b) }
+
 let set_used_variables l =
   let env = Global.env () in
   let ids = List.fold_right Id.Set.add l Id.Set.empty in
   let ctx = Environ.keep_hyps env ids in
+  let ctx_set =
+    List.fold_right Id.Set.add (List.map pi1 ctx) Id.Set.empty in
+  let vars_of = Environ.global_vars_set in
+  let aux env entry (ctx, all_safe, to_clear as orig) =
+    match entry with
+    | (x,None,_) ->
+       if Id.Set.mem x all_safe then orig
+       else (ctx, all_safe, (Loc.ghost,x)::to_clear) 
+    | (x,Some bo, ty) as decl ->
+       if Id.Set.mem x all_safe then orig else
+       let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
+       if Id.Set.subset vars all_safe
+       then (decl :: ctx, Id.Set.add x all_safe, to_clear)
+       else (ctx, all_safe, (Loc.ghost,x) :: to_clear) in
+  let ctx, _, to_clear =
+    Environ.fold_named_context aux env ~init:(ctx,ctx_set,[]) in
+  let to_clear = if !proof_using_auto_clear then to_clear else [] in
   match !pstates with
   | [] -> raise NoCurrentProof
   | p :: rest ->
       if not (Option.is_empty p.section_vars) then
         Errors.error "Used section variables can be declared only once";
       pstates := { p with section_vars = Some ctx} :: rest;
-      ctx
+      ctx, to_clear
 
 let get_open_goals () =
   let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in
@@ -342,10 +368,6 @@ type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.ev
 let return_proof ?(allow_partial=false) () =
  let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
  if allow_partial then begin
-  if Proof.is_complete proof then begin
-    msg_warning (str"The proof of " ++ str (Names.Id.to_string pid) ++
-     str" is complete, no need to end it with Admitted");
-  end;
   let proofs = Proof.partial_proof proof in
   let _,_,_,_, evd = Proof.proof proof in
   let eff = Evd.eval_side_effects evd in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 995e90efc..a11c7b4e0 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -132,8 +132,10 @@ val set_interp_tac :
     -> unit
 
 (** Sets the section variables assumed by the proof, returns its closure
- * (w.r.t. type dependencies *)
-val set_used_variables : Names.Id.t list -> Context.section_context
+ * (w.r.t. type dependencies and let-ins covered by it) + a list of
+ * ids to be cleared *)
+val set_used_variables :
+  Names.Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list
 val get_used_variables : unit -> Context.section_context option
 
 (**********************************************************)
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index f66e96571..7eed1cb31 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -11,20 +11,15 @@ open Environ
 open Util
 open Vernacexpr
 
-let to_string = function
-  | SsAll -> "All"
-  | SsType -> "Type"
-  | SsExpr(SsSet l)-> String.concat " " (List.map Id.to_string (List.map snd l))
-  | SsExpr e ->
-      let rec aux = function
-        | SsSet [] -> "( )"
-        | SsSet [_,x] -> Id.to_string x
-        | SsSet l ->
-          "(" ^ String.concat " " (List.map Id.to_string (List.map snd l)) ^ ")"
-        | SsCompl e -> "-" ^ aux e^""
-        | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")"
-        | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")"
-      in aux e
+let to_string e =
+  let rec aux = function
+    | SsEmpty -> "()"
+    | SsSingl (_,id) -> "("^Id.to_string id^")"
+    | SsCompl e -> "-" ^ aux e^""
+    | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")"
+    | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")"
+    | SsFwdClose e -> "("^aux e^")*"
+  in aux e
 
 let known_names = Summary.ref [] ~name:"proofusing-nameset"
 
@@ -36,30 +31,48 @@ let in_nameset =
     discharge_function = (fun _ -> None)
   }
 
+let rec close_fwd e s =
+  let s' =
+    List.fold_left (fun s (id,b,ty) ->      
+      let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in
+      let vty = global_vars_set e ty in
+      let vbty = Id.Set.union vb vty in
+      if Id.Set.exists (fun v -> Id.Set.mem v s) vbty
+      then Id.Set.add id (Id.Set.union s vbty) else s)
+    s (named_context e)
+    in
+  if Id.Set.equal s s' then s else close_fwd e s'
+;;
+
 let rec process_expr env e ty =
-  match e with
-  | SsAll ->
-      List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty
-  | SsExpr e ->
-      let rec aux = function
-        | SsSet l -> set_of_list env (List.map snd l)
-        | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
-        | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
-        | SsCompl e -> Id.Set.diff (full_set env) (aux e)
-      in
-        aux e
-  | SsType ->
-      List.fold_left (fun acc ty ->
+  let rec aux = function
+    | SsEmpty -> Id.Set.empty
+    | SsSingl (_,id) -> set_of_id env ty id
+    | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2)
+    | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2)
+    | SsCompl e -> Id.Set.diff (full_set env) (aux e)
+    | SsFwdClose e -> close_fwd env (aux e)
+  in
+    aux e
+
+and set_of_id env ty id =
+  if Id.to_string id = "Type" then
+    List.fold_left (fun acc ty ->
         Id.Set.union (global_vars_set env ty) acc)
       Id.Set.empty ty
-and set_of_list env = function
-  | [x] when CList.mem_assoc_f Id.equal x !known_names ->
-      process_expr env (CList.assoc_f Id.equal x !known_names) []
-  | l -> List.fold_right Id.Set.add l Id.Set.empty
-and full_set env = set_of_list env (List.map pi1 (named_context env))
+  else if Id.to_string id = "All" then
+    List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty
+  else if CList.mem_assoc_f Id.equal id !known_names then
+    process_expr env (CList.assoc_f Id.equal id !known_names) []
+  else Id.Set.singleton id
+
+and full_set env =
+  List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty
 
 let process_expr env e ty =
-  let s = Id.Set.union (process_expr env SsType ty) (process_expr env e []) in
+  let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in
+  let v_ty = process_expr env ty_expr ty in
+  let s = Id.Set.union v_ty (process_expr env e ty) in
   Id.Set.elements s
 
 let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr))
@@ -77,62 +90,49 @@ let minimize_hyps env ids =
   in
     aux ids
 
-let minimize_unused_hyps env ids =
-  let all_ids = List.map pi1 (named_context env) in
-  let deps_of =
-    let cache =
-      List.map (fun id -> id,really_needed env (Id.Set.singleton id)) all_ids in
-    fun id -> List.assoc id cache in
-  let inv_dep_of =
-    let cache_sum cache id stuff =
-      try Id.Map.add id (Id.Set.add stuff (Id.Map.find id cache)) cache
-      with Not_found -> Id.Map.add id (Id.Set.singleton stuff) cache in
-    let cache =
-      List.fold_left (fun cache id ->
-        Id.Set.fold (fun d cache -> cache_sum cache d id)
-          (Id.Set.remove id (deps_of id)) cache)
-        Id.Map.empty all_ids in
-    fun id -> try Id.Map.find id cache with Not_found -> Id.Set.empty in
-  let rec aux s =
-    let s' =
-      Id.Set.fold (fun id s ->
-        if Id.Set.subset (inv_dep_of id) s then Id.Set.diff s (inv_dep_of id)
-        else s)
-      s s in
-    if Id.Set.equal s s' then s else aux s' in
-  aux ids
-
-let suggest_Proof_using kn env vars ids_typ context_ids =
+let remove_ids_and_lets env s ids =
+  let not_ids id = not (Id.Set.mem id ids) in
+  let no_body id = named_body id env = None in
+  let deps id = really_needed env (Id.Set.singleton id) in
+    (Id.Set.filter (fun id ->
+      not_ids id &&
+     (no_body id ||
+       Id.Set.exists not_ids (Id.Set.filter no_body (deps id)))) s)
+
+let suggest_Proof_using name env vars ids_typ context_ids =
   let module S = Id.Set in
   let open Pp in
-  let used = S.union vars ids_typ in
-  let needed = minimize_hyps env used in
-  let all_needed = really_needed env needed in
-  let all = List.fold_right S.add context_ids S.empty in
-  let unneeded = minimize_unused_hyps env (S.diff all needed) in
-  let pr_set s =
+  let print x = prerr_endline (string_of_ppcmds x) in
+  let pr_set parens s =
     let wrap ppcmds =
-      if S.cardinal s > 1 || S.equal s (S.singleton (Id.of_string "All"))
-      then str "(" ++ ppcmds ++ str ")"
+      if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")"
       else ppcmds in
     wrap (prlist_with_sep (fun _ -> str" ") Id.print (S.elements s)) in
+  let used = S.union vars ids_typ in
+  let needed = minimize_hyps env (remove_ids_and_lets env used ids_typ) in
+  let all_needed = really_needed env needed in
+  let all = List.fold_right S.add context_ids S.empty in
+  let fwd_typ = close_fwd env ids_typ in
   if !Flags.debug then begin
-    prerr_endline (string_of_ppcmds (str "All " ++ pr_set all));
-    prerr_endline (string_of_ppcmds (str "Type" ++ pr_set ids_typ));
-    prerr_endline (string_of_ppcmds (str "needed " ++ pr_set needed));
-    prerr_endline (string_of_ppcmds (str "unneeded " ++ pr_set unneeded));
+    print (str "All "        ++ pr_set false all);
+    print (str "Type "       ++ pr_set false ids_typ);
+    print (str "needed "     ++ pr_set false needed);
+    print (str "all_needed " ++ pr_set false all_needed);
+    print (str "Type* "      ++ pr_set false fwd_typ);
   end;
+  let valid_exprs = ref [] in
+  let valid e = valid_exprs := e :: !valid_exprs in
+  if S.is_empty needed then valid (str "Type");
+  if S.equal all_needed fwd_typ then valid (str "Type*");
+  if S.equal all all_needed then valid(str "All");
+  valid (pr_set false needed);
   msg_info (
-    str"The proof of "++
-    Names.Constant.print kn ++ spc() ++ str "should start with:"++spc()++
-    str"Proof using " ++
-    if S.is_empty needed then str "."
-    else if S.subset needed ids_typ then str "Type."
-    else if S.equal all all_needed then str "All."
-    else 
-      let s1 = string_of_ppcmds (str "-" ++ pr_set unneeded ++ str".") in
-      let s2 = string_of_ppcmds (pr_set needed ++ str".") in
-      if String.length s1 < String.length s2 then str s1 else str s2)
+    str"The proof of "++ str name ++ spc() ++
+    str "should start with one of the following commands:"++spc()++
+    v 0 (
+    prlist_with_sep cut (fun x->str"Proof using " ++x++ str". ") !valid_exprs));
+  string_of_ppcmds (prlist_with_sep (fun _ -> str";")  (fun x->x) !valid_exprs)
+;;
 
 let value = ref false
 
@@ -146,13 +146,13 @@ let _ =
       Goptions.optwrite = (fun b ->
         value := b;
         if b then Term_typing.set_suggest_proof_using suggest_Proof_using
-        else Term_typing.set_suggest_proof_using (fun _ _ _ _ _ -> ())
+        else Term_typing.set_suggest_proof_using (fun _ _ _ _ _ -> "")
       ) }
 
-let value = ref "_unset_"
+let value = ref None
 
 let _ =
-  Goptions.declare_string_option
+  Goptions.declare_stringopt_option
     { Goptions.optsync  = true;
       Goptions.optdepr  = false;
       Goptions.optname  = "default value for Proof using";
@@ -161,6 +161,4 @@ let _ =
       Goptions.optwrite = (fun b -> value := b;) }
 
 
-let get_default_proof_using () =
-  if !value = "_unset_" then None
-  else Some !value
+let get_default_proof_using () = !value
diff --git a/proofs/proof_using.mli b/proofs/proof_using.mli
index fb3497f10..dcf8a0fcd 100644
--- a/proofs/proof_using.mli
+++ b/proofs/proof_using.mli
@@ -6,21 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-
-(* [minimize_hyps e s1] gives [s2] s.t. [Id.Set.subset s2 s1] is [true]
- * and [keep_hyps e s1] is equal to [keep_hyps e s2].  Inefficient. *)
-val minimize_hyps : Environ.env -> Names.Id.Set.t -> Names.Id.Set.t
-
-(* [minimize_unused_hyps e s1] gives [s2] s.t. [Id.Set.subset s2 s1] is [true]
- * and s.t. calling [clear s1] would do the same as [clear s2].  Inefficient. *)
-val minimize_unused_hyps : Environ.env -> Names.Id.Set.t -> Names.Id.Set.t
-
 val process_expr :
-  Environ.env -> Vernacexpr.section_subset_descr -> Constr.types list ->
+  Environ.env -> Vernacexpr.section_subset_expr -> Constr.types list ->
     Names.Id.t list
 
-val name_set : Names.Id.t -> Vernacexpr.section_subset_descr -> unit
+val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit
 
-val to_string : Vernacexpr.section_subset_descr -> string
+val to_string : Vernacexpr.section_subset_expr -> string
 
 val get_default_proof_using : unit -> string option