--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/find_theorems.ML Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,244 @@
+(* Title: find_theorems.ML
+ Author: Timothy Bourke, NICTA
+
+ Simple find_theorems server
+*)
+
+local
+val default_limit = 20;
+val thy_names = sort string_ord (ThyInfo.get_names ());
+
+val find_theorems_url = "find_theorems";
+
+fun is_sorry thm =
+ Thm.proof_of thm
+ |> Proofterm.approximate_proof_body
+ |> Proofterm.all_oracles_of
+ |> exists (fn (x, _) => x = "Pure.skip_proof");
+
+local open Xhtml in
+fun find_theorems_form thy_name (query, limit, withdups) =
+ let
+ val query_input =
+ input (id "query", {
+ name = "query",
+ itype = TextInput { value = query, maxlength = NONE }});
+
+ val max_results = divele noid
+ [
+ label (noid, { for = "limit" }, "Max. results:"),
+ input (id "limit",
+ { name = "limit",
+ itype = TextInput { value = SOME (Int.toString limit),
+ maxlength = NONE }})
+ ];
+
+ val theories = divele noid
+ [
+ label (noid, { for = "theory" }, "Search in:"),
+ select (id "theory", { name = "theory", value = SOME thy_name })
+ thy_names
+ ];
+
+ val with_dups = divele noid
+ [
+ label (noid, { for = "withdups" }, "Allow duplicates:"),
+ input (id "withdups",
+ { name = "withdups",
+ itype = Checkbox { checked = withdups, value = SOME "true" }})
+ ];
+
+ val help = divele (class "help")
+ [ a { href="/pasting_help.html", text="(pasting from proof general)" } ];
+ in
+ form (id "findtheorems", { method = "post", action = "/isabelle/find_theorems" })
+ [tag "fieldset" []
+ [tag "legend" [] [text "find_theorems"],
+ (add_script (OnKeyPress, "encodequery(this)")
+ o add_script (OnChange, "encodequery(this)")
+ o add_script (OnMouseUp, "encodequery(this)")) query_input,
+ divele (class "settings") [ max_results, theories, with_dups, help ],
+ divele (class "mainbuttons")
+ [ reset_button (id "reset"), submit_button (id "submit") ]
+ ]
+ ]
+ end;
+
+fun html_header thy_name args =
+ html { lang = "en" } [
+ head { title = "Find Theorems: results", stylesheet_href = "/basic.css" }
+ [script (noid, { script_type="text/javascript",
+ src="/find_theorems.js" })],
+ add_script (OnLoad, "encodequery(document.getElementById('query'))")
+ (body noid [
+ h (noid, 1, "Theory " ^ thy_name),
+ find_theorems_form thy_name args,
+ divele noid []
+ ])
+ ];
+
+fun html_error msg = p ((class "error"), msg);
+
+val find_theorems_table =
+ table (class "findtheorems")
+ [
+ thead noid [tr [th (noid, "name"), th (noid, "theorem")]],
+ tbody noid []
+ ];
+
+fun show_criterion (b, c) =
+ let
+ fun prfx s = let
+ val (c, v) = if b then ("criterion", s) else ("ncriterion", "-" ^ s);
+ in span (class c, v) end;
+
+ fun prfxwith s = let
+ val (c, v) =
+ if b
+ then ("criterion", "with " ^ s)
+ else ("ncriterion", "without " ^ s);
+ in span (class c, v) end;
+ in
+ (case c of
+ Find_Theorems.Name name => prfx ("name: " ^ quote name)
+ | Find_Theorems.Intro => prfx "intro"
+ | Find_Theorems.IntroIff => prfx "introiff"
+ | Find_Theorems.Elim => prfx "elim"
+ | Find_Theorems.Dest => prfx "dest"
+ | Find_Theorems.Solves => prfx "solves"
+ | Find_Theorems.Simp pat => prfx ("simp: \"" ^ pat ^ "\"")
+ | Find_Theorems.Pattern pat => prfx ("\"" ^ pat ^ "\""))
+ end;
+
+fun find_theorems_summary (othmslen, thmslen, query, args) =
+ let
+ val args =
+ (case othmslen of
+ NONE => args
+ | SOME l => Symtab.update ("limit", Int.toString l) args)
+ val qargs = HttpUtil.make_query_string args;
+
+ val num_found_text =
+ (case othmslen of
+ NONE => text (Int.toString thmslen)
+ | SOME l =>
+ a { href = find_theorems_url ^
+ (if qargs = "" then "" else "?" ^ qargs),
+ text = Int.toString l })
+ val found = [text "found ", num_found_text, text " theorems"] : tag list;
+ val displayed =
+ if is_some othmslen
+ then " (" ^ Int.toString thmslen ^ " displayed)"
+ else "";
+ fun show_search c = tr [ td' noid [show_criterion c] ];
+ in
+ table (class "findtheoremsquery")
+ (* [ tr [ th (noid, "searched for:") ] ]
+ @ map show_search query @ *)
+ [ tr [ th' noid (found @ [text (displayed ^ ":")]) ] ]
+ end
+
+fun sorry_class thm = if is_sorry thm then class "sorried" else noid;
+
+fun html_thm ctxt (n, (thmref, thm)) =
+ let
+ val string_of_thm =
+ Output.output o Pretty.setmp_margin_CRITICAL 100 Pretty.string_of o
+ setmp_CRITICAL show_question_marks false (Display.pretty_thm ctxt);
+ in
+ tag' "tr" (class ("row" ^ Int.toString (n mod 2)))
+ [
+ tag' "td" (class "name")
+ [span' (sorry_class thm)
+ [raw_text (Facts.string_of_ref thmref)]
+ ],
+ tag' "td" (class "thm") [pre noid (string_of_thm thm)]
+ ]
+ end;
+
+end;
+
+structure P = OuterParse
+ and K = OuterKeyword
+ and FT = Find_Theorems;
+
+val criterion =
+ P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Find_Theorems.Name ||
+ P.reserved "intro" >> K Find_Theorems.Intro ||
+ P.reserved "elim" >> K Find_Theorems.Elim ||
+ P.reserved "dest" >> K Find_Theorems.Dest ||
+ P.reserved "solves" >> K Find_Theorems.Solves ||
+ P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> Find_Theorems.Simp ||
+ P.term >> Find_Theorems.Pattern;
+
+val parse_query =
+ Scan.repeat (((Scan.option P.minus >> is_none) -- criterion));
+
+fun app_index f xs = fold_index (fn x => K (f x)) xs ();
+
+fun find_theorems (req as ScgiReq.Req {request_method, query_string, ...},
+ content, send) =
+ let
+ val arg_data =
+ (case request_method of
+ ScgiReq.Get => query_string
+ | ScgiReq.Post =>
+ content
+ |> Byte.bytesToString
+ |> HttpUtil.parse_query_string
+ | ScgiReq.Head => raise Fail "Cannot handle Head requests.");
+
+ val args = Symtab.lookup arg_data;
+
+ val query = the_default "" (args "query");
+ fun get_query () =
+ query
+ |> (fn s => s ^ ";")
+ |> OuterSyntax.scan Position.start
+ |> filter OuterLex.is_proper
+ |> Scan.error parse_query
+ |> fst;
+
+ val limit =
+ args "limit"
+ |> Option.mapPartial Int.fromString
+ |> the_default default_limit;
+ val thy_name =
+ args "theory"
+ |> the_default "Main";
+ val with_dups = is_some (args "with_dups");
+
+ fun do_find () =
+ let
+ val ctxt = ProofContext.init (theory thy_name);
+ val query = get_query ();
+ val (othmslen, thms) = apsnd rev
+ (Find_Theorems.find_theorems ctxt NONE (SOME limit) with_dups query);
+ val thmslen = length thms;
+ fun thm_row args = Xhtml.write send (html_thm ctxt args);
+ in
+ Xhtml.write send
+ (find_theorems_summary (othmslen, thmslen, query, arg_data));
+ if null thms then ()
+ else (Xhtml.write_open send find_theorems_table;
+ HTML_Unicode.print_mode (app_index thm_row) thms;
+ Xhtml.write_close send find_theorems_table)
+ end;
+
+ val header = (html_header thy_name (args "query", limit, with_dups));
+ in
+ send Xhtml.doctype_xhtml1_0_strict;
+ Xhtml.write_open send header;
+ if query = "" then ()
+ else
+ do_find ()
+ handle
+ ERROR msg => Xhtml.write send (html_error msg)
+ | e => Xhtml.write send (html_error ("Server error: " ^ exnMessage e));
+ Xhtml.write_close send header
+ end;
+in
+val () = show_question_marks := false;
+val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems);
+end;
+