Proof_using: new syntax + suggestion

Proof using can be followed by:
- All : all variables
- Type : all variables occurring in the type
- expr:
    - (a b .. c) : set
    - expr + expr : set union
    - expr - expr : set difference
    - -expr : set complement (All - expr)
Exceptions:
- a singleton set can be written without parentheses. This also allows
  the implementation of named sets sharing the same name space of
  section hyps ans write
  - bla - x : where bla is defined as (a b .. x y) elsewhere.
- if expr is just a set, then parentheses can be omitted

This module also implements some AI to tell the user how he could
decorate "Proof" with a "using BLA" clause.

Finally, one can Set Default Proof Using "str" to any string that is
used whenever the "using ..." part is missing.  The coding of this
sucks a little since it is the parser that applies the default.

1 files changed, 148 insertions, 0 deletions

diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
new file mode 100644
index 0000000000..746daf273a
--- /dev/null
+++ b/proofs/proof_using.ml
@@ -0,0 +1,148 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+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 set_of_list l = List.fold_right Id.Set.add l Id.Set.empty
+
+let full_set env = set_of_list (List.map pi1 (named_context env))
+
+let process_expr env e ty =
+  match e with
+  | SsAll -> List.map pi1 (named_context env)
+  | SsExpr e ->
+      let rec aux = function
+        | SsSet l -> set_of_list (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
+        Id.Set.elements (aux e)
+  | SsType ->
+      match ty with
+      | [ty] -> Id.Set.elements (global_vars_set env ty)
+      | _ -> Errors.error"Proof using on a multiple lemma is not supported"
+
+let minimize_hyps env ids =
+  let rec aux ids =
+    let ids' =
+      Id.Set.fold (fun id alive ->
+        let impl_by_id =
+          Id.Set.remove id (really_needed env (Id.Set.singleton id)) in
+        if Id.Set.is_empty impl_by_id then alive
+        else Id.Set.diff alive impl_by_id)
+      ids ids in
+    if Id.Set.equal ids ids' then ids else aux 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 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 wrap ppcmds =
+      if S.cardinal s > 1 || S.equal s (S.singleton (Id.of_string "All"))
+      then str "(" ++ ppcmds ++ str ")"
+      else ppcmds in
+    wrap (prlist_with_sep (fun _ -> str" ") Id.print (S.elements s)) 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));
+  end;
+  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)
+
+let value = ref false
+
+let _ =
+  Goptions.declare_bool_option
+    { Goptions.optsync  = true;
+      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 _ _ _ _ _ -> ())
+      ) }
+
+let value = ref "_unset_"
+
+let _ =
+  Goptions.declare_string_option
+    { Goptions.optsync  = true;
+      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;) }
+
+
+let get_default_proof_using () =
+  if !value = "_unset_" then None
+  else Some !value