author | wenzelm |
Tue, 06 Oct 2015 11:29:00 +0200 | |
changeset 61335 | 43848476063c |
parent 61223 | dfccf6c06201 |
child 62848 | e4140efe699e |
permissions | -rw-r--r-- |
30143 | 1 |
(* Title: Pure/Tools/find_consts.ML |
29884 | 2 |
Author: Timothy Bourke and Gerwin Klein, NICTA |
3 |
||
30143 | 4 |
Hoogle-like (http://www-users.cs.york.ac.uk/~ndm/hoogle) searching by |
5 |
type over constants, but matching is not fuzzy. |
|
29884 | 6 |
*) |
7 |
||
8 |
signature FIND_CONSTS = |
|
9 |
sig |
|
30143 | 10 |
datatype criterion = |
11 |
Strict of string |
|
12 |
| Loose of string |
|
13 |
| Name of string |
|
56758 | 14 |
val read_query: Position.T -> string -> (bool * criterion) list |
29884 | 15 |
val find_consts : Proof.context -> (bool * criterion) list -> unit |
16 |
end; |
|
17 |
||
33301 | 18 |
structure Find_Consts : FIND_CONSTS = |
29884 | 19 |
struct |
20 |
||
30143 | 21 |
(* search criteria *) |
22 |
||
23 |
datatype criterion = |
|
24 |
Strict of string |
|
25 |
| Loose of string |
|
26 |
| Name of string; |
|
29884 | 27 |
|
31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset
|
28 |
|
30143 | 29 |
(* matching types/consts *) |
29884 | 30 |
|
30143 | 31 |
fun matches_subtype thy typat = |
38335 | 32 |
Term.exists_subtype (fn ty => Sign.typ_instance thy (ty, typat)); |
29884 | 33 |
|
61335 | 34 |
fun check_const pred (c, (ty, _)) = |
35 |
if pred (c, ty) then SOME (Term.size_of_typ ty) else NONE; |
|
29884 | 36 |
|
30143 | 37 |
fun opt_not f (c as (_, (ty, _))) = |
38335 | 38 |
if is_some (f c) then NONE else SOME (Term.size_of_typ ty); |
29884 | 39 |
|
46979
ef4b0d6b2fb6
sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
wenzelm
parents:
46961
diff
changeset
|
40 |
fun filter_const _ _ NONE = NONE |
ef4b0d6b2fb6
sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
wenzelm
parents:
46961
diff
changeset
|
41 |
| filter_const c f (SOME rank) = |
31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset
|
42 |
(case f c of |
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset
|
43 |
NONE => NONE |
46979
ef4b0d6b2fb6
sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
wenzelm
parents:
46961
diff
changeset
|
44 |
| SOME i => SOME (Int.min (rank, i))); |
30143 | 45 |
|
46 |
||
47 |
(* pretty results *) |
|
29895
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
48 |
|
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
49 |
fun pretty_criterion (b, c) = |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
50 |
let |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
51 |
fun prfx s = if b then s else "-" ^ s; |
60667
d86c449d30ba
plain string output, without funny control chars;
wenzelm
parents:
60664
diff
changeset
|
52 |
val show_pat = quote o Input.source_content o Syntax.read_input; |
29895
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
53 |
in |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
54 |
(case c of |
60667
d86c449d30ba
plain string output, without funny control chars;
wenzelm
parents:
60664
diff
changeset
|
55 |
Strict pat => Pretty.str (prfx "strict: " ^ show_pat pat) |
d86c449d30ba
plain string output, without funny control chars;
wenzelm
parents:
60664
diff
changeset
|
56 |
| Loose pat => Pretty.str (prfx (show_pat pat)) |
29895
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
57 |
| Name name => Pretty.str (prfx "name: " ^ quote name)) |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
58 |
end; |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
59 |
|
49886 | 60 |
fun pretty_const ctxt (c, ty) = |
30143 | 61 |
let |
35845
e5980f0ad025
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
wenzelm
parents:
33301
diff
changeset
|
62 |
val ty' = Logic.unvarifyT_global ty; |
61335 | 63 |
val markup = Name_Space.markup (Proof_Context.const_space ctxt) c; |
29895
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
64 |
in |
30143 | 65 |
Pretty.block |
49886 | 66 |
[Pretty.mark markup (Pretty.str c), Pretty.str " ::", Pretty.brk 1, |
30143 | 67 |
Pretty.quote (Syntax.pretty_typ ctxt ty')] |
29895
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
68 |
end; |
0e70a29d3e02
find_consts: display the search criteria. (by Timothy Bourke)
kleing
parents:
29884
diff
changeset
|
69 |
|
31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset
|
70 |
|
30143 | 71 |
(* find_consts *) |
72 |
||
56758 | 73 |
fun pretty_consts ctxt raw_criteria = |
30143 | 74 |
let |
42360 | 75 |
val thy = Proof_Context.theory_of ctxt; |
29884 | 76 |
val low_ranking = 10000; |
77 |
||
30207
c56d27155041
Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents:
30206
diff
changeset
|
78 |
fun make_pattern crit = |
c56d27155041
Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents:
30206
diff
changeset
|
79 |
let |
c56d27155041
Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents:
30206
diff
changeset
|
80 |
val raw_T = Syntax.parse_typ ctxt crit; |
31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset
|
81 |
val t = |
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset
|
82 |
Syntax.check_term |
42360 | 83 |
(Proof_Context.set_mode Proof_Context.mode_pattern ctxt) |
31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset
|
84 |
(Term.dummy_pattern raw_T); |
30207
c56d27155041
Implement Makarius's suggestion for improved type pattern parsing.
Timothy Bourke
parents:
30206
diff
changeset
|
85 |
in Term.type_of t end; |
29884 | 86 |
|
87 |
fun make_match (Strict arg) = |
|
88 |
let val qty = make_pattern arg; in |
|
30143 | 89 |
fn (_, (ty, _)) => |
90 |
let |
|
29884 | 91 |
val tye = Sign.typ_match thy (qty, ty) Vartab.empty; |
31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset
|
92 |
val sub_size = |
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset
|
93 |
Vartab.fold (fn (_, (_, t)) => fn n => Term.size_of_typ t + n) tye 0; |
32790
a7b92f98180b
handle Type.TYPE_MATCH, not arbitrary exceptions;
wenzelm
parents:
31687
diff
changeset
|
94 |
in SOME sub_size end handle Type.TYPE_MATCH => NONE |
29884 | 95 |
end |
96 |
| make_match (Loose arg) = |
|
97 |
check_const (matches_subtype thy (make_pattern arg) o snd) |
|
98 |
| make_match (Name arg) = check_const (match_string arg o fst); |
|
99 |
||
100 |
fun make_criterion (b, crit) = (if b then I else opt_not) (make_match crit); |
|
30206
48507466d9d2
find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
Timothy Bourke
parents:
30190
diff
changeset
|
101 |
val criteria = map make_criterion raw_criteria; |
29884 | 102 |
|
61335 | 103 |
fun user_visible (c, _) = |
104 |
if Consts.is_concealed (Proof_Context.consts_of ctxt) c |
|
105 |
then NONE else SOME low_ranking; |
|
106 |
||
31684
d5d830979a54
minor tuning according to Isabelle/ML conventions;
wenzelm
parents:
30207
diff
changeset
|
107 |
fun eval_entry c = |
61335 | 108 |
fold (filter_const c) (user_visible :: criteria) (SOME low_ranking); |
29884 | 109 |
|
61335 | 110 |
val {constants, ...} = Consts.dest (Sign.consts_of thy); |
30143 | 111 |
val matches = |
56062 | 112 |
fold (fn c => (case eval_entry c of NONE => I | SOME rank => cons (rank, c))) constants [] |
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58928
diff
changeset
|
113 |
|> sort (prod_ord (rev_order o int_ord) (string_ord o apply2 fst)) |
46979
ef4b0d6b2fb6
sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold;
wenzelm
parents:
46961
diff
changeset
|
114 |
|> map (apsnd fst o snd); |
56912
293cd4dcfebc
some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56908
diff
changeset
|
115 |
|
293cd4dcfebc
some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56908
diff
changeset
|
116 |
val position_markup = Position.markup (Position.thread_data ()) Markup.position; |
29884 | 117 |
in |
56891
48899c43b07d
tuned message -- more context for detached window etc.;
wenzelm
parents:
56763
diff
changeset
|
118 |
Pretty.block |
56912
293cd4dcfebc
some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56908
diff
changeset
|
119 |
(Pretty.fbreaks |
293cd4dcfebc
some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56908
diff
changeset
|
120 |
(Pretty.mark position_markup (Pretty.keyword1 "find_consts") :: |
293cd4dcfebc
some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56908
diff
changeset
|
121 |
map pretty_criterion raw_criteria)) :: |
38335 | 122 |
Pretty.str "" :: |
56908
734f7e6151c9
tuned message: more compact, imitate actual command line;
wenzelm
parents:
56891
diff
changeset
|
123 |
(if null matches then [Pretty.str "found nothing"] |
734f7e6151c9
tuned message: more compact, imitate actual command line;
wenzelm
parents:
56891
diff
changeset
|
124 |
else |
734f7e6151c9
tuned message: more compact, imitate actual command line;
wenzelm
parents:
56891
diff
changeset
|
125 |
Pretty.str ("found " ^ string_of_int (length matches) ^ " constant(s):") :: |
734f7e6151c9
tuned message: more compact, imitate actual command line;
wenzelm
parents:
56891
diff
changeset
|
126 |
grouped 10 Par_List.map (Pretty.item o single o pretty_const ctxt) matches) |
61335 | 127 |
end |> Pretty.chunks; |
56758 | 128 |
|
129 |
fun find_consts ctxt args = Pretty.writeln (pretty_consts ctxt args); |
|
29884 | 130 |
|
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset
|
131 |
|
30143 | 132 |
(* command syntax *) |
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset
|
133 |
|
38334 | 134 |
local |
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset
|
135 |
|
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset
|
136 |
val criterion = |
36950 | 137 |
Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name || |
60664
263a8f15faf3
proper outer syntax category, e.g. relevant for PIDE markup;
wenzelm
parents:
60610
diff
changeset
|
138 |
Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.typ) >> Strict || |
263a8f15faf3
proper outer syntax category, e.g. relevant for PIDE markup;
wenzelm
parents:
60610
diff
changeset
|
139 |
Parse.typ >> Loose; |
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset
|
140 |
|
56758 | 141 |
val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion); |
142 |
||
59934
b65c4370f831
more position information and PIDE markup for command keywords;
wenzelm
parents:
59083
diff
changeset
|
143 |
val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords; |
58905 | 144 |
|
38334 | 145 |
in |
146 |
||
56758 | 147 |
fun read_query pos str = |
59083 | 148 |
Token.explode query_keywords pos str |
56758 | 149 |
|> filter Token.is_proper |
150 |
|> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof))) |
|
151 |
|> #1; |
|
152 |
||
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset
|
153 |
val _ = |
59936
b8ffc3dc9e24
@{command_spec} is superseded by @{command_keyword};
wenzelm
parents:
59934
diff
changeset
|
154 |
Outer_Syntax.command @{command_keyword find_consts} |
56758 | 155 |
"find constants by name / type patterns" |
156 |
(query >> (fn spec => |
|
157 |
Toplevel.keep (fn st => |
|
158 |
Pretty.writeln (pretty_consts (Toplevel.context_of st) spec)))); |
|
30142
8d6145694bb5
moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents:
29895
diff
changeset
|
159 |
|
29884 | 160 |
end; |
161 |
||
56758 | 162 |
|
163 |
(* PIDE query operation *) |
|
164 |
||
165 |
val _ = |
|
60610
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
59936
diff
changeset
|
166 |
Query_Operation.register {name = "find_consts", pri = Task_Queue.urgent_pri} |
61223 | 167 |
(fn {state, args, writeln_result, ...} => |
60610
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
59936
diff
changeset
|
168 |
(case try Toplevel.context_of state of |
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
59936
diff
changeset
|
169 |
SOME ctxt => |
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
59936
diff
changeset
|
170 |
let |
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
59936
diff
changeset
|
171 |
val [query_arg] = args; |
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
59936
diff
changeset
|
172 |
val query = read_query Position.none query_arg; |
61223 | 173 |
in writeln_result (Pretty.string_of (pretty_consts ctxt query)) end |
60610
f52b4b0c10c4
improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
wenzelm
parents:
59936
diff
changeset
|
174 |
| NONE => error "Unknown context")); |
56758 | 175 |
|
38334 | 176 |
end; |