author | krauss |
Mon, 30 May 2011 17:07:48 +0200 | |
changeset 43072 | 8aeb7ec8003a |
parent 43068 | ac769b5edd1d |
child 43073 | a4c985fe015d |
permissions | -rw-r--r-- |
33823 | 1 |
(* Title: Tools/WWW_Find/find_theorems.ML |
33817 | 2 |
Author: Timothy Bourke, NICTA |
3 |
||
33823 | 4 |
Simple find_theorems server. |
33817 | 5 |
*) |
6 |
||
7 |
local |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36960
diff
changeset
|
8 |
|
33817 | 9 |
val default_limit = 20; |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36960
diff
changeset
|
10 |
val thy_names = sort string_ord (Thy_Info.get_names ()); |
33817 | 11 |
|
12 |
val find_theorems_url = "find_theorems"; |
|
13 |
||
14 |
fun is_sorry thm = |
|
15 |
Thm.proof_of thm |
|
16 |
|> Proofterm.approximate_proof_body |
|
17 |
|> Proofterm.all_oracles_of |
|
18 |
|> exists (fn (x, _) => x = "Pure.skip_proof"); |
|
19 |
||
20 |
local open Xhtml in |
|
21 |
fun find_theorems_form thy_name (query, limit, withdups) = |
|
22 |
let |
|
23 |
val query_input = |
|
24 |
input (id "query", { |
|
25 |
name = "query", |
|
26 |
itype = TextInput { value = query, maxlength = NONE }}); |
|
27 |
||
28 |
val max_results = divele noid |
|
29 |
[ |
|
30 |
label (noid, { for = "limit" }, "Max. results:"), |
|
31 |
input (id "limit", |
|
32 |
{ name = "limit", |
|
41491 | 33 |
itype = TextInput { value = SOME (string_of_int limit), |
33817 | 34 |
maxlength = NONE }}) |
35 |
]; |
|
36 |
||
37 |
val theories = divele noid |
|
38 |
[ |
|
39 |
label (noid, { for = "theory" }, "Search in:"), |
|
40 |
select (id "theory", { name = "theory", value = SOME thy_name }) |
|
41 |
thy_names |
|
42 |
]; |
|
43 |
||
44 |
val with_dups = divele noid |
|
45 |
[ |
|
46 |
label (noid, { for = "withdups" }, "Allow duplicates:"), |
|
47 |
input (id "withdups", |
|
48 |
{ name = "withdups", |
|
49 |
itype = Checkbox { checked = withdups, value = SOME "true" }}) |
|
50 |
]; |
|
51 |
||
52 |
val help = divele (class "help") |
|
53 |
[ a { href="/pasting_help.html", text="(pasting from proof general)" } ]; |
|
54 |
in |
|
55 |
form (id "findtheorems", { method = "post", action = "/isabelle/find_theorems" }) |
|
56 |
[tag "fieldset" [] |
|
57 |
[tag "legend" [] [text "find_theorems"], |
|
58 |
(add_script (OnKeyPress, "encodequery(this)") |
|
59 |
o add_script (OnChange, "encodequery(this)") |
|
60 |
o add_script (OnMouseUp, "encodequery(this)")) query_input, |
|
61 |
divele (class "settings") [ max_results, theories, with_dups, help ], |
|
62 |
divele (class "mainbuttons") |
|
63 |
[ reset_button (id "reset"), submit_button (id "submit") ] |
|
64 |
] |
|
65 |
] |
|
66 |
end; |
|
67 |
||
68 |
fun html_header thy_name args = |
|
69 |
html { lang = "en" } [ |
|
70 |
head { title = "Find Theorems: results", stylesheet_href = "/basic.css" } |
|
71 |
[script (noid, { script_type="text/javascript", |
|
72 |
src="/find_theorems.js" })], |
|
73 |
add_script (OnLoad, "encodequery(document.getElementById('query'))") |
|
74 |
(body noid [ |
|
75 |
h (noid, 1, "Theory " ^ thy_name), |
|
76 |
find_theorems_form thy_name args, |
|
77 |
divele noid [] |
|
78 |
]) |
|
79 |
]; |
|
80 |
||
81 |
fun html_error msg = p ((class "error"), msg); |
|
82 |
||
83 |
val find_theorems_table = |
|
84 |
table (class "findtheorems") |
|
85 |
[ |
|
86 |
thead noid [tr [th (noid, "name"), th (noid, "theorem")]], |
|
87 |
tbody noid [] |
|
88 |
]; |
|
89 |
||
90 |
fun show_criterion (b, c) = |
|
91 |
let |
|
92 |
fun prfx s = let |
|
93 |
val (c, v) = if b then ("criterion", s) else ("ncriterion", "-" ^ s); |
|
94 |
in span (class c, v) end; |
|
95 |
in |
|
96 |
(case c of |
|
97 |
Find_Theorems.Name name => prfx ("name: " ^ quote name) |
|
98 |
| Find_Theorems.Intro => prfx "intro" |
|
99 |
| Find_Theorems.IntroIff => prfx "introiff" |
|
100 |
| Find_Theorems.Elim => prfx "elim" |
|
101 |
| Find_Theorems.Dest => prfx "dest" |
|
102 |
| Find_Theorems.Solves => prfx "solves" |
|
103 |
| Find_Theorems.Simp pat => prfx ("simp: \"" ^ pat ^ "\"") |
|
104 |
| Find_Theorems.Pattern pat => prfx ("\"" ^ pat ^ "\"")) |
|
105 |
end; |
|
106 |
||
43072
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
107 |
fun find_theorems_summary (othmslen, thmslen, args) = |
33817 | 108 |
let |
109 |
val args = |
|
110 |
(case othmslen of |
|
111 |
NONE => args |
|
41491 | 112 |
| SOME l => Symtab.update ("limit", string_of_int l) args) |
33817 | 113 |
val qargs = HttpUtil.make_query_string args; |
114 |
||
115 |
val num_found_text = |
|
116 |
(case othmslen of |
|
41491 | 117 |
NONE => text (string_of_int thmslen) |
33817 | 118 |
| SOME l => |
119 |
a { href = find_theorems_url ^ |
|
120 |
(if qargs = "" then "" else "?" ^ qargs), |
|
41491 | 121 |
text = string_of_int l }) |
33817 | 122 |
val found = [text "found ", num_found_text, text " theorems"] : tag list; |
123 |
val displayed = |
|
124 |
if is_some othmslen |
|
41491 | 125 |
then " (" ^ string_of_int thmslen ^ " displayed)" |
33817 | 126 |
else ""; |
127 |
in |
|
128 |
table (class "findtheoremsquery") |
|
129 |
[ tr [ th' noid (found @ [text (displayed ^ ":")]) ] ] |
|
130 |
end |
|
131 |
||
132 |
fun sorry_class thm = if is_sorry thm then class "sorried" else noid; |
|
133 |
||
134 |
fun html_thm ctxt (n, (thmref, thm)) = |
|
135 |
let |
|
38980
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
37863
diff
changeset
|
136 |
val output_thm = |
36745 | 137 |
Output.output o Pretty.string_of_margin 100 o |
38980
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
37863
diff
changeset
|
138 |
Display.pretty_thm (Config.put show_question_marks false ctxt); |
33817 | 139 |
in |
41491 | 140 |
tag' "tr" (class ("row" ^ string_of_int (n mod 2))) |
33817 | 141 |
[ |
142 |
tag' "td" (class "name") |
|
143 |
[span' (sorry_class thm) |
|
144 |
[raw_text (Facts.string_of_ref thmref)] |
|
145 |
], |
|
38980
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
37863
diff
changeset
|
146 |
tag' "td" (class "thm") [pre noid (output_thm thm)] |
33817 | 147 |
] |
148 |
end; |
|
149 |
||
150 |
end; |
|
151 |
||
152 |
fun app_index f xs = fold_index (fn x => K (f x)) xs (); |
|
153 |
||
43072
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
154 |
fun parse_request (ScgiReq.Req {request_method, query_string, ...}, content, send) = |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
155 |
(case request_method of |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
156 |
ScgiReq.Get => query_string |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
157 |
| ScgiReq.Post => |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
158 |
content |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
159 |
|> Byte.bytesToString |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
160 |
|> HttpUtil.parse_query_string |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
161 |
| ScgiReq.Head => raise Fail "Cannot handle Head requests.", |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
162 |
send); |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
163 |
|
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
164 |
fun find_theorems (arg_data, send) = |
33817 | 165 |
let |
166 |
val args = Symtab.lookup arg_data; |
|
167 |
||
43072
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
168 |
val query_str = the_default "" (args "query"); |
33817 | 169 |
fun get_query () = |
43072
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
170 |
(query_str ^ ";") |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36959
diff
changeset
|
171 |
|> Outer_Syntax.scan Position.start |
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36745
diff
changeset
|
172 |
|> filter Token.is_proper |
43068
ac769b5edd1d
exported raw query parser; removed inconsistent clone
krauss
parents:
43067
diff
changeset
|
173 |
|> Scan.error Find_Theorems.query_parser |
33817 | 174 |
|> fst; |
175 |
||
43072
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
176 |
val limit = case args "limit" of |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
177 |
NONE => default_limit |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
178 |
| SOME str => the_default default_limit (Int.fromString str); |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
179 |
val thy_name = the_default "Main" (args "theory"); |
33817 | 180 |
val with_dups = is_some (args "with_dups"); |
43072
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
181 |
|
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
182 |
val ctxt = Proof_Context.init_global (Thy_Info.get_theory thy_name); |
33817 | 183 |
|
43072
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
184 |
fun do_find query = |
33817 | 185 |
let |
43072
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
186 |
val (othmslen, thms) = |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
187 |
Find_Theorems.find_theorems_cmd ctxt NONE (SOME limit) with_dups query |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
188 |
||> rev; |
33817 | 189 |
in |
190 |
Xhtml.write send |
|
43072
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
191 |
(find_theorems_summary (othmslen, length thms, arg_data)); |
33817 | 192 |
if null thms then () |
43072
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
193 |
else Xhtml.write_enclosed send find_theorems_table (fn send => |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
194 |
HTML_Unicode.print_mode (app_index (Xhtml.write send o html_thm ctxt)) thms) |
33817 | 195 |
end; |
196 |
in |
|
197 |
send Xhtml.doctype_xhtml1_0_strict; |
|
43072
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
198 |
Xhtml.write_enclosed send |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
199 |
(html_header thy_name (args "query", limit, with_dups)) |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
200 |
(fn send => |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
201 |
if query_str = "" then () |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
202 |
else |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
203 |
do_find (get_query ()) |
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
204 |
handle ERROR msg => Xhtml.write send (html_error msg)) |
33817 | 205 |
end; |
206 |
in |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36960
diff
changeset
|
207 |
|
42289
dafae095d733
discontinued special status of structure Printer;
wenzelm
parents:
41522
diff
changeset
|
208 |
val () = Printer.show_question_marks_default := false; |
43072
8aeb7ec8003a
attempt to clarify code; removed "handle _" and dead code
krauss
parents:
43068
diff
changeset
|
209 |
val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems o parse_request); |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36960
diff
changeset
|
210 |
|
33817 | 211 |
end; |
212 |