Merge PR #1103: Take Suggest Proof Using outside the kernel.

18 files changed, 149 insertions, 95 deletions

diff --git a/API/API.mli b/API/API.mli
index 04c69b025..879323a37 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4914,7 +4914,6 @@ module G_proofs :
 sig
 
   val hint : Vernacexpr.hints_expr Pcoq.Gram.entry
-  val hint_proof_using : 'a Pcoq.Gram.entry -> 'a option -> 'a option
 
 end
 
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 4a471d4a2..bc7146884 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -236,6 +236,7 @@ type scheme =
 
 type section_subset_expr =
   | SsEmpty
+  | SsType
   | SsSingl of lident
   | SsCompl of section_subset_expr
   | SsUnion of section_subset_expr * section_subset_expr
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 0c0b910e1..22e109b01 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -367,7 +367,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
       cook_context = None;
     }
 
-let record_aux env s_ty s_bo suggested_expr =
+let record_aux env s_ty s_bo =
   let in_ty = keep_hyps env s_ty in
   let v =
     String.concat " "
@@ -376,10 +376,7 @@ let record_aux env s_ty s_bo suggested_expr =
           if List.exists (NamedDecl.get_id %> Id.equal id) in_ty then None
           else Some (Id.to_string id))
         (keep_hyps env s_bo)) in
-  Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr)
-
-let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
-let set_suggest_proof_using f = suggest_proof_using := f
+  Aux_file.record_in_aux "context_used" v
 
 let build_constant_declaration kn env result =
   let open Cooking in
@@ -425,16 +422,13 @@ let build_constant_declaration kn env result =
                 (Opaqueproof.force_proof (opaque_tables env) lc) in
             (* we force so that cst are added to the env immediately after *)
             ignore(Opaqueproof.force_constraints (opaque_tables env) lc);
-            let expr =
-              !suggest_proof_using (Constant.to_string kn)
-                env vars ids_typ context_ids in
-            if !Flags.record_aux_file then record_aux env ids_typ vars expr;
+            if !Flags.record_aux_file then record_aux env ids_typ vars;
             vars
         in
         keep_hyps env (Idset.union ids_typ ids_def), def
     | None ->
         if !Flags.record_aux_file then
-          record_aux env Id.Set.empty Id.Set.empty "";
+          record_aux env Id.Set.empty Id.Set.empty;
         [], def (* Empty section context: no need to check *)
     | Some declared ->
         (* We use the declared set and chain a check of correctness *)
@@ -618,14 +612,10 @@ let translate_local_def mb env id centry =
     | Undef _ -> ()
     | Def _ -> ()
     | OpaqueDef lc ->
-       let context_ids = List.map NamedDecl.get_id (named_context env) in
        let ids_typ = global_vars_set env typ in
        let ids_def = global_vars_set env
          (Opaqueproof.force_proof (opaque_tables env) lc) in
-       let expr =
-         !suggest_proof_using (Id.to_string id)
-           env ids_def ids_typ context_ids in
-       record_aux env ids_typ ids_def expr
+       record_aux env ids_typ ids_def
   end;
   let univs = match decl.cook_universes with
   | Monomorphic_const ctx -> ctx
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 24153343e..b16f81c5a 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -77,6 +77,3 @@ val infer_declaration : trust:'a trust -> env -> constant option ->
 
 val build_constant_declaration :
   constant -> env -> Cooking.result -> constant_body
-
-val set_suggest_proof_using :
-  (string -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> string) -> unit
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index e2c87bbbf..f10d74677 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -17,12 +17,6 @@ open Pcoq.Vernac_
 
 let thm_token = G_vernac.thm_token
 
-let hint_proof_using e = function
-  | Some _ as x -> x
-  | None -> match Proof_using.get_default_proof_using () with
-     | None -> None
-     | Some s -> Some (Gram.entry_parse e (Gram.parsable (Stream.of_string s)))
-
 let hint = Gram.entry_create "hint"
 
 (* Proof commands *)
@@ -35,8 +29,7 @@ GEXTEND Gram
   ;
   command:
     [ [ IDENT "Goal"; c = lconstr -> VernacGoal c
-      | IDENT "Proof" ->
-          VernacProof (None,hint_proof_using G_vernac.section_subset_expr None)
+      | IDENT "Proof" -> VernacProof (None,None)
       | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
       | IDENT "Proof"; c = lconstr -> VernacExactProof c
       | IDENT "Abort" -> VernacAbort None
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3e0b85b54..a5b58b855 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -580,8 +580,8 @@ GEXTEND Gram
   starredidentref:
     [ [ i = identref -> SsSingl i
       | i = identref; "*" -> SsFwdClose(SsSingl i)
-      | "Type" -> SsSingl (Loc.tag ~loc:!@loc @@ Id.of_string "Type")
-      | "Type"; "*" -> SsFwdClose (SsSingl (Loc.tag ~loc:!@loc @@ Id.of_string "Type")) ]]
+      | "Type" -> SsType
+      | "Type"; "*" -> SsFwdClose SsType ]]
   ;
   ssexpr:
     [ "35" 
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index d639dd0e1..c577cb219 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -340,7 +340,7 @@ GEXTEND Gram
   command:
     [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; 
         l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] ->
-          Vernacexpr.VernacProof (Some (in_tac ta), G_proofs.hint_proof_using G_vernac.section_subset_expr l)
+          Vernacexpr.VernacProof (Some (in_tac ta), l)
       | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
         ta = OPT [ "with"; ta = Pltac.tactic -> in_tac ta ] ->
           Vernacexpr.VernacProof (ta,Some l) ] ]
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index a1cdfdbaa..d1158b3d6 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -524,7 +524,16 @@ open Decl_kinds
     | PrintStrategy (Some qid) ->
       keyword "Print Strategy" ++ pr_smart_global qid
 
-  let pr_using e = str (Proof_using.to_string e)
+  let pr_using e =
+    let rec aux = function
+      | SsEmpty -> "()"
+      | SsType -> "(Type)"
+      | 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 Pp.str (aux e)
 
   let rec pr_vernac_body v =
     let return = tag_vernac v in
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index b88eed484..cf27b413c 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -15,5 +15,8 @@ val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation lis
 (** Prints a vernac expression *)
 val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.t
 
+(** Prints a "proof using X" clause. *)
+val pr_using : Vernacexpr.section_subset_expr -> Pp.t
+
 (** Prints a vernac expression and closes it with a dot. *)
 val pr_vernac : Vernacexpr.vernac_expr -> Pp.t
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index eaf0c693e..058e839b4 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -1,7 +1,6 @@
 Miscprint
 Goal
 Evar_refiner
-Proof_using
 Proof_type
 Logic
 Refine
diff --git a/stm/stm.ml b/stm/stm.ml
index 770ccf22d..d1693519d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1167,16 +1167,12 @@ let set_compilation_hints file =
 
 let get_hint_ctx loc =
   let s = Aux_file.get ?loc !hints "context_used" in
-  match Str.split (Str.regexp ";") s with
-  | ids :: _ ->
-      let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") ids) in
-      let ids = List.map (fun id -> Loc.tag id) ids in
-      begin match ids with
-      | [] -> SsEmpty
-      | x :: xs ->
-          List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs
-      end
-  | _ -> raise Not_found
+  let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in
+  let ids = List.map (fun id -> Loc.tag id) ids in
+  match ids with
+  | [] -> SsEmpty
+  | x :: xs ->
+    List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs
 
 let get_hint_bp_time proof_name =
   try float_of_string (Aux_file.get !hints proof_name)
diff --git a/test-suite/output/SuggestProofUsing.out b/test-suite/output/SuggestProofUsing.out
new file mode 100644
index 000000000..8d67a4a4b
--- /dev/null
+++ b/test-suite/output/SuggestProofUsing.out
@@ -0,0 +1,7 @@
+The proof of nat should start with one of the following commands:
+Proof using . 
+Proof using Type*. 
+Proof using Type. 
+The proof of foo should start with one of the following commands:
+Proof using A B. 
+Proof using All. 
diff --git a/test-suite/output/SuggestProofUsing.v b/test-suite/output/SuggestProofUsing.v
new file mode 100644
index 000000000..00b6f8e18
--- /dev/null
+++ b/test-suite/output/SuggestProofUsing.v
@@ -0,0 +1,31 @@
+Set Suggest Proof Using.
+
+Section Sec.
+  Variables A B : Type.
+
+  (* Some normal lemma. *)
+  Lemma nat : Set.
+  Proof.
+    exact nat.
+  Qed.
+
+  (* Make sure All is suggested even though we add an unused variable
+  to the context. *)
+  Let foo : Type.
+  Proof.
+    exact (A -> B).
+  Qed.
+
+  (* Having a [Proof using] disables the suggestion message. *)
+  Definition bar : Type.
+  Proof using A.
+    exact A.
+  Qed.
+
+  (* Transparent definitions don't get a suggestion message. *)
+  Definition baz : Type.
+  Proof.
+    exact A.
+  Defined.
+
+End Sec.
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 2c8f6ec9d..d45665dd4 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -180,10 +180,14 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
   try
     let const = adjust_guardness_conditions const do_guard in
     let k = Kindops.logical_kind_of_goal_kind kind in
+    let should_suggest = const.const_entry_opaque && Option.is_empty const.const_entry_secctx in
     let l,r = match locality with
       | Discharge when Lib.sections_are_opened () ->
           let c = SectionLocalDef const in
           let _ = declare_variable id (Lib.cwd(), c, k) in
+          let () = if should_suggest
+            then Proof_using.suggest_variable (Global.env ()) id
+          in
           (Local, VarRef id)
       | Local | Global | Discharge ->
           let local = match locality with
@@ -192,7 +196,11 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
           in
           let kn =
            declare_constant ?export_seff id ~local (DefinitionEntry const, k) in
-          (locality, ConstRef kn) in
+          let () = if should_suggest
+            then Proof_using.suggest_constant (Global.env ()) kn
+          in
+          (locality, ConstRef kn)
+    in
     definition_message id;
     Option.iter (Universes.register_universe_binders r) pl;
     call_hook (fun exn -> exn) hook l r
diff --git a/proofs/proof_using.ml b/vernac/proof_using.ml
index 1a321120c..ffe99cfd8 100644
--- a/proofs/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -14,16 +14,6 @@ open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
 
-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"
 
 let in_nameset =
@@ -48,12 +38,20 @@ let rec close_fwd e s =
     s (named_context e)
     in
   if Id.Set.equal s s' then s else close_fwd e s'
-;;
+
+let set_of_type env ty =
+  List.fold_left (fun acc ty ->
+      Id.Set.union (global_vars_set env ty) acc)
+    Id.Set.empty ty
+
+let full_set env =
+  List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
 
 let rec process_expr env e ty =
   let rec aux = function
     | SsEmpty -> Id.Set.empty
-    | SsSingl (_,id) -> set_of_id env ty id
+    | SsType -> set_of_type env ty
+    | SsSingl (_,id) -> set_of_id env 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)
@@ -61,23 +59,15 @@ let rec process_expr env e ty =
   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
-  else if Id.to_string id = "All" then
+and set_of_id env id =
+  if Id.to_string id = "All" then
     List.fold_right Id.Set.add (List.map NamedDecl.get_id (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 NamedDecl.get_id (named_context env)) Id.Set.empty
-
 let process_expr env e ty =
-  let ty_expr = SsSingl(Loc.tag @@ Id.of_string "Type") in
-  let v_ty = process_expr env ty_expr ty in
+  let v_ty = set_of_type env ty in
   let s = Id.Set.union v_ty (process_expr env e ty) in
   Id.Set.elements s
 
@@ -105,7 +95,13 @@ let remove_ids_and_lets env s ids =
      (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 record_proof_using expr =
+  Aux_file.record_in_aux "suggest_proof_using" expr
+
+(* Variables in [skip] come from after the definition, so don't count
+   for "All". Used in the variable case since the env contains the
+   variable itself. *)
+let suggest_common env ppid used ids_typ skip =
   let module S = Id.Set in
   let open Pp in
   let print x = Feedback.msg_debug x in
@@ -114,10 +110,13 @@ let suggest_Proof_using name env vars ids_typ context_ids =
       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 all = List.fold_left (fun all d -> S.add (NamedDecl.get_id d) all)
+      S.empty (named_context env)
+  in
+  let all = S.diff all skip in
   let fwd_typ = close_fwd env ids_typ in
   if !Flags.debug then begin
     print (str "All "        ++ pr_set false all);
@@ -133,36 +132,59 @@ let suggest_Proof_using name env vars ids_typ context_ids =
   if S.equal all all_needed then valid(str "All");
   valid (pr_set false needed);
   Feedback.msg_info (
-    str"The proof of "++ str name ++ spc() ++
+    str"The proof of "++ ppid ++ 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)
-;;
+  if !Flags.record_aux_file
+  then
+    let s = string_of_ppcmds (prlist_with_sep (fun _ -> str";")  (fun x->x) !valid_exprs) in
+    record_proof_using s
 
-let value = ref false
+let suggest_proof_using = ref false
 
 let _ =
   Goptions.declare_bool_option
     { Goptions.optdepr  = false;
       Goptions.optname  = "suggest Proof using";
       Goptions.optkey   = ["Suggest";"Proof";"Using"];
-      Goptions.optread  = (fun () -> !value);
-      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 _ _ _ _ _ -> "")
-      ) }
+      Goptions.optread  = (fun () -> !suggest_proof_using);
+      Goptions.optwrite = ((:=) suggest_proof_using) }
+
+let suggest_constant env kn =
+  if !suggest_proof_using
+  then begin
+    let open Declarations in
+    let body = lookup_constant kn env in
+    let used = Id.Set.of_list @@ List.map NamedDecl.get_id body.const_hyps in
+    let ids_typ = global_vars_set env body.const_type in
+    suggest_common env (Printer.pr_constant env kn) used ids_typ Id.Set.empty
+  end
+
+let suggest_variable env id =
+  if !suggest_proof_using
+  then begin
+    match lookup_named id env with
+    | LocalDef (_,body,typ) ->
+      let ids_typ = global_vars_set env typ in
+      let ids_body = global_vars_set env body in
+      let used = Id.Set.union ids_body ids_typ in
+      suggest_common env (Id.print id) used ids_typ (Id.Set.singleton id)
+    | LocalAssum _ -> assert false
+  end
 
 let value = ref None
 
+let using_to_string us = Pp.string_of_ppcmds (Ppvernac.pr_using us)
+let using_from_string us = Pcoq.Gram.(entry_parse G_vernac.section_subset_expr (parsable (Stream.of_string us)))
+
 let _ =
   Goptions.declare_stringopt_option
     { Goptions.optdepr  = false;
       Goptions.optname  = "default value for Proof using";
       Goptions.optkey   = ["Default";"Proof";"Using"];
-      Goptions.optread  = (fun () -> !value);
-      Goptions.optwrite = (fun b -> value := b;) }
-
+      Goptions.optread  = (fun () -> Option.map using_to_string !value);
+      Goptions.optwrite = (fun b -> value := Option.map using_from_string b);
+    }
 
 let get_default_proof_using () = !value
diff --git a/proofs/proof_using.mli b/vernac/proof_using.mli
index c882b1827..f63c8e242 100644
--- a/proofs/proof_using.mli
+++ b/vernac/proof_using.mli
@@ -14,6 +14,8 @@ val process_expr :
 
 val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit
 
-val to_string : Vernacexpr.section_subset_expr -> string
+val suggest_constant : Environ.env -> Names.Constant.t -> unit
 
-val get_default_proof_using : unit -> string option
+val suggest_variable : Environ.env -> Names.Id.t -> unit
+
+val get_default_proof_using : unit -> Vernacexpr.section_subset_expr option
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index f74073e1f..850902d6b 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -1,4 +1,5 @@
 Vernacprop
+Proof_using
 Lemmas
 Himsg
 ExplainErr
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 203d913db..66427b709 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2060,17 +2060,13 @@ let interp ?proof ?loc locality poly c =
   | VernacEndSubproof -> vernac_end_subproof ()
   | VernacShow s -> vernac_show s
   | VernacCheckGuard -> vernac_check_guard ()
-  | VernacProof (None, None) ->
-      Aux_file.record_in_aux_at ?loc "VernacProof" "tac:no using:no"
-  | VernacProof (Some tac, None) ->
-      Aux_file.record_in_aux_at ?loc "VernacProof" "tac:yes using:no";
-      vernac_set_end_tac tac
-  | VernacProof (None, Some l) ->
-      Aux_file.record_in_aux_at ?loc "VernacProof" "tac:no using:yes";
-      vernac_set_used_variables l
-  | VernacProof (Some tac, Some l) -> 
-      Aux_file.record_in_aux_at ?loc "VernacProof" "tac:yes using:yes";
-      vernac_set_end_tac tac; vernac_set_used_variables l
+  | VernacProof (tac, using) ->
+    let using = Option.append using (Proof_using.get_default_proof_using ()) in
+    let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in
+    let usings = if Option.is_empty using then "using:no" else "using:yes" in
+    Aux_file.record_in_aux_at ?loc "VernacProof" (tacs^" "^usings);
+    Option.iter vernac_set_end_tac tac;
+    Option.iter vernac_set_used_variables using
   | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
 
   (* Extensions *)