diff options
Diffstat (limited to 'proofs/proof_using.ml')
| -rw-r--r-- | proofs/proof_using.ml | 166 |
1 files changed, 166 insertions, 0 deletions
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml new file mode 100644 index 00000000..f66e9657 --- /dev/null +++ b/proofs/proof_using.ml @@ -0,0 +1,166 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \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 known_names = Summary.ref [] ~name:"proofusing-nameset" + +let in_nameset = + let open Libobject in + declare_object { (default_object "proofusing-nameset") with + cache_function = (fun (_,x) -> known_names := x :: !known_names); + classify_function = (fun _ -> Dispose); + discharge_function = (fun _ -> None) + } + +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 -> + 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)) + +let process_expr env e ty = + let s = Id.Set.union (process_expr env SsType ty) (process_expr env e []) in + Id.Set.elements s + +let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr)) + +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 |