src/Tools/WWW_Find/find_theorems.ML
author krauss
Mon May 30 17:07:48 2011 +0200 (2011-05-30)
changeset 43067 76e1d25c6357
parent 42361 23f352990944
child 43068 ac769b5edd1d
permissions -rw-r--r--
separate query parsing from actual search
     1 (*  Title:      Tools/WWW_Find/find_theorems.ML
     2     Author:     Timothy Bourke, NICTA
     3 
     4 Simple find_theorems server.
     5 *)
     6 
     7 local
     8 
     9 val default_limit = 20;
    10 val thy_names = sort string_ord (Thy_Info.get_names ());
    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",
    33             itype = TextInput { value = SOME (string_of_int limit),
    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 
    96     fun prfxwith s = let
    97         val (c, v) =
    98           if b
    99           then ("criterion", "with " ^ s)
   100           else ("ncriterion", "without " ^ s);
   101       in span (class c, v) end;
   102   in
   103     (case c of
   104       Find_Theorems.Name name => prfx ("name: " ^ quote name)
   105     | Find_Theorems.Intro => prfx "intro"
   106     | Find_Theorems.IntroIff => prfx "introiff"
   107     | Find_Theorems.Elim => prfx "elim"
   108     | Find_Theorems.Dest => prfx "dest"
   109     | Find_Theorems.Solves => prfx "solves"
   110     | Find_Theorems.Simp pat => prfx ("simp: \"" ^ pat ^ "\"")
   111     | Find_Theorems.Pattern pat => prfx ("\"" ^ pat ^ "\""))
   112   end;
   113 
   114 fun find_theorems_summary (othmslen, thmslen, query, args) =
   115   let
   116     val args =
   117       (case othmslen of
   118          NONE => args
   119        | SOME l => Symtab.update ("limit", string_of_int l) args)
   120     val qargs = HttpUtil.make_query_string args;
   121 
   122     val num_found_text =
   123       (case othmslen of
   124          NONE => text (string_of_int thmslen)
   125        | SOME l =>
   126            a { href = find_theorems_url ^
   127                (if qargs = "" then "" else "?" ^ qargs),
   128            text = string_of_int l })
   129     val found = [text "found ", num_found_text, text " theorems"] : tag list;
   130     val displayed =
   131       if is_some othmslen
   132       then " (" ^ string_of_int thmslen ^ " displayed)"
   133       else "";
   134     fun show_search c = tr [ td' noid [show_criterion c] ];
   135   in
   136     table (class "findtheoremsquery")
   137     (* [ tr [ th (noid, "searched for:") ] ]
   138        @ map show_search query @ *)
   139       [ tr [ th' noid (found @ [text (displayed ^ ":")]) ] ]
   140   end
   141 
   142 fun sorry_class thm = if is_sorry thm then class "sorried" else noid;
   143 
   144 fun html_thm ctxt (n, (thmref, thm)) =
   145   let
   146     val output_thm =
   147       Output.output o Pretty.string_of_margin 100 o
   148         Display.pretty_thm (Config.put show_question_marks false ctxt);
   149   in
   150     tag' "tr" (class ("row" ^ string_of_int (n mod 2)))
   151       [
   152         tag' "td" (class "name")
   153           [span' (sorry_class thm)
   154              [raw_text (Facts.string_of_ref thmref)]
   155           ],
   156         tag' "td" (class "thm") [pre noid (output_thm thm)]
   157       ]
   158   end;
   159 
   160 end;
   161 
   162 val criterion =
   163   Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Find_Theorems.Name ||
   164   Parse.reserved "intro" >> K Find_Theorems.Intro ||
   165   Parse.reserved "elim" >> K Find_Theorems.Elim ||
   166   Parse.reserved "dest" >> K Find_Theorems.Dest ||
   167   Parse.reserved "solves" >> K Find_Theorems.Solves ||
   168   Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Find_Theorems.Simp ||
   169   Parse.term >> Find_Theorems.Pattern;
   170 
   171 val parse_query =
   172   Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
   173 
   174 fun app_index f xs = fold_index (fn x => K (f x)) xs ();
   175 
   176 fun find_theorems (req as ScgiReq.Req {request_method, query_string, ...},
   177                    content, send) =
   178   let
   179     val arg_data =
   180       (case request_method of
   181          ScgiReq.Get => query_string
   182        | ScgiReq.Post =>
   183           content
   184           |> Byte.bytesToString
   185           |> HttpUtil.parse_query_string
   186        | ScgiReq.Head => raise Fail "Cannot handle Head requests.");
   187 
   188     val args = Symtab.lookup arg_data;
   189 
   190     val query = the_default "" (args "query");
   191     fun get_query () =
   192       query
   193       |> (fn s => s ^ ";")
   194       |> Outer_Syntax.scan Position.start
   195       |> filter Token.is_proper
   196       |> Scan.error parse_query
   197       |> fst;
   198 
   199     val limit =
   200       args "limit"
   201       |> Option.mapPartial Int.fromString
   202       |> the_default default_limit;
   203     val thy_name =
   204       args "theory"
   205       |> the_default "Main";
   206     val with_dups = is_some (args "with_dups");
   207 
   208     fun do_find () =
   209       let
   210         val ctxt = Proof_Context.init_global (Thy_Info.get_theory thy_name);
   211         val query = get_query ();
   212         val (othmslen, thms) = apsnd rev
   213           (Find_Theorems.find_theorems_cmd ctxt NONE (SOME limit) with_dups query);
   214         val thmslen = length thms;
   215         fun thm_row args = Xhtml.write send (html_thm ctxt args);
   216       in
   217         Xhtml.write send
   218           (find_theorems_summary (othmslen, thmslen, query, arg_data));
   219         if null thms then ()
   220         else (Xhtml.write_open send find_theorems_table;
   221               HTML_Unicode.print_mode (app_index thm_row) thms;
   222               Xhtml.write_close send find_theorems_table)
   223       end;
   224 
   225     val header = (html_header thy_name (args "query", limit, with_dups));
   226   in
   227     send Xhtml.doctype_xhtml1_0_strict;
   228     Xhtml.write_open send header;
   229     if query = "" then ()
   230     else
   231       do_find ()
   232         handle
   233           ERROR msg => Xhtml.write send (html_error msg)
   234         | e => Xhtml.write send (html_error ("Server error: " ^ exnMessage e)); (* FIXME avoid handle e *)
   235     Xhtml.write_close send header
   236   end;
   237 in
   238 
   239 val () = Printer.show_question_marks_default := false;
   240 val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems);
   241 
   242 end;
   243