blob: f66e9657128a17c020a0505f5f0464993cf05b5c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
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
|
