src/Tools/WWW_Find/find_theorems.ML
author wenzelm
Wed Jan 12 15:15:51 2011 +0100 (2011-01-12)
changeset 41522 42d13d00ccfb
parent 41491 a2ad5b824051
child 42289 dafae095d733
permissions -rw-r--r--
more FIXMEs concerning bad catch-all exception handlers;
wenzelm@33823
     1
(*  Title:      Tools/WWW_Find/find_theorems.ML
kleing@33817
     2
    Author:     Timothy Bourke, NICTA
kleing@33817
     3
wenzelm@33823
     4
Simple find_theorems server.
kleing@33817
     5
*)
kleing@33817
     6
kleing@33817
     7
local
wenzelm@37216
     8
kleing@33817
     9
val default_limit = 20;
wenzelm@37216
    10
val thy_names = sort string_ord (Thy_Info.get_names ());
kleing@33817
    11
kleing@33817
    12
val find_theorems_url = "find_theorems";
kleing@33817
    13
kleing@33817
    14
fun is_sorry thm =
kleing@33817
    15
  Thm.proof_of thm
kleing@33817
    16
  |> Proofterm.approximate_proof_body
kleing@33817
    17
  |> Proofterm.all_oracles_of
kleing@33817
    18
  |> exists (fn (x, _) => x = "Pure.skip_proof");
kleing@33817
    19
kleing@33817
    20
local open Xhtml in
kleing@33817
    21
fun find_theorems_form thy_name (query, limit, withdups) =
kleing@33817
    22
  let
kleing@33817
    23
    val query_input =
kleing@33817
    24
      input (id "query", {
kleing@33817
    25
        name = "query",
kleing@33817
    26
        itype = TextInput { value = query, maxlength = NONE }});
kleing@33817
    27
kleing@33817
    28
    val max_results = divele noid
kleing@33817
    29
      [
kleing@33817
    30
        label (noid, { for = "limit" }, "Max. results:"),
kleing@33817
    31
        input (id "limit",
kleing@33817
    32
          { name = "limit",
wenzelm@41491
    33
            itype = TextInput { value = SOME (string_of_int limit),
kleing@33817
    34
                                maxlength = NONE }})
kleing@33817
    35
      ];
kleing@33817
    36
kleing@33817
    37
    val theories = divele noid
kleing@33817
    38
      [
kleing@33817
    39
        label (noid, { for = "theory" }, "Search in:"),
kleing@33817
    40
        select (id "theory", { name = "theory", value = SOME thy_name })
kleing@33817
    41
               thy_names
kleing@33817
    42
      ];
kleing@33817
    43
kleing@33817
    44
    val with_dups = divele noid
kleing@33817
    45
      [
kleing@33817
    46
        label (noid, { for = "withdups" }, "Allow duplicates:"),
kleing@33817
    47
        input (id "withdups",
kleing@33817
    48
          { name = "withdups",
kleing@33817
    49
            itype = Checkbox { checked = withdups, value = SOME "true" }})
kleing@33817
    50
      ];
kleing@33817
    51
kleing@33817
    52
    val help = divele (class "help")
kleing@33817
    53
      [ a { href="/pasting_help.html", text="(pasting from proof general)" } ];
kleing@33817
    54
  in
kleing@33817
    55
    form (id "findtheorems", { method = "post", action = "/isabelle/find_theorems" })
kleing@33817
    56
      [tag "fieldset" []
kleing@33817
    57
        [tag "legend" [] [text "find_theorems"],
kleing@33817
    58
         (add_script (OnKeyPress, "encodequery(this)")
kleing@33817
    59
          o add_script (OnChange, "encodequery(this)")
kleing@33817
    60
          o add_script (OnMouseUp, "encodequery(this)")) query_input,
kleing@33817
    61
         divele (class "settings") [ max_results, theories, with_dups, help ],
kleing@33817
    62
         divele (class "mainbuttons")
kleing@33817
    63
           [ reset_button (id "reset"), submit_button (id "submit") ]
kleing@33817
    64
        ]
kleing@33817
    65
      ]
kleing@33817
    66
  end;
kleing@33817
    67
kleing@33817
    68
fun html_header thy_name args =
kleing@33817
    69
  html { lang = "en" } [
kleing@33817
    70
    head { title = "Find Theorems: results", stylesheet_href = "/basic.css" }
kleing@33817
    71
         [script (noid, { script_type="text/javascript",
kleing@33817
    72
                          src="/find_theorems.js" })],
kleing@33817
    73
    add_script (OnLoad, "encodequery(document.getElementById('query'))")
kleing@33817
    74
      (body noid [
kleing@33817
    75
          h (noid, 1, "Theory " ^ thy_name),
kleing@33817
    76
          find_theorems_form thy_name args,
kleing@33817
    77
          divele noid []
kleing@33817
    78
         ])
kleing@33817
    79
  ];
kleing@33817
    80
kleing@33817
    81
fun html_error msg = p ((class "error"), msg);
kleing@33817
    82
kleing@33817
    83
val find_theorems_table =
kleing@33817
    84
  table (class "findtheorems")
kleing@33817
    85
    [
kleing@33817
    86
      thead noid [tr [th (noid, "name"), th (noid, "theorem")]],
kleing@33817
    87
      tbody noid []
kleing@33817
    88
    ];
kleing@33817
    89
kleing@33817
    90
fun show_criterion (b, c) =
kleing@33817
    91
  let
kleing@33817
    92
    fun prfx s = let
kleing@33817
    93
        val (c, v) = if b then ("criterion", s) else ("ncriterion", "-" ^ s);
kleing@33817
    94
      in span (class c, v) end;
kleing@33817
    95
kleing@33817
    96
    fun prfxwith s = let
kleing@33817
    97
        val (c, v) =
kleing@33817
    98
          if b
kleing@33817
    99
          then ("criterion", "with " ^ s)
kleing@33817
   100
          else ("ncriterion", "without " ^ s);
kleing@33817
   101
      in span (class c, v) end;
kleing@33817
   102
  in
kleing@33817
   103
    (case c of
kleing@33817
   104
      Find_Theorems.Name name => prfx ("name: " ^ quote name)
kleing@33817
   105
    | Find_Theorems.Intro => prfx "intro"
kleing@33817
   106
    | Find_Theorems.IntroIff => prfx "introiff"
kleing@33817
   107
    | Find_Theorems.Elim => prfx "elim"
kleing@33817
   108
    | Find_Theorems.Dest => prfx "dest"
kleing@33817
   109
    | Find_Theorems.Solves => prfx "solves"
kleing@33817
   110
    | Find_Theorems.Simp pat => prfx ("simp: \"" ^ pat ^ "\"")
kleing@33817
   111
    | Find_Theorems.Pattern pat => prfx ("\"" ^ pat ^ "\""))
kleing@33817
   112
  end;
kleing@33817
   113
kleing@33817
   114
fun find_theorems_summary (othmslen, thmslen, query, args) =
kleing@33817
   115
  let
kleing@33817
   116
    val args =
kleing@33817
   117
      (case othmslen of
kleing@33817
   118
         NONE => args
wenzelm@41491
   119
       | SOME l => Symtab.update ("limit", string_of_int l) args)
kleing@33817
   120
    val qargs = HttpUtil.make_query_string args;
kleing@33817
   121
kleing@33817
   122
    val num_found_text =
kleing@33817
   123
      (case othmslen of
wenzelm@41491
   124
         NONE => text (string_of_int thmslen)
kleing@33817
   125
       | SOME l =>
kleing@33817
   126
           a { href = find_theorems_url ^
kleing@33817
   127
               (if qargs = "" then "" else "?" ^ qargs),
wenzelm@41491
   128
           text = string_of_int l })
kleing@33817
   129
    val found = [text "found ", num_found_text, text " theorems"] : tag list;
kleing@33817
   130
    val displayed =
kleing@33817
   131
      if is_some othmslen
wenzelm@41491
   132
      then " (" ^ string_of_int thmslen ^ " displayed)"
kleing@33817
   133
      else "";
kleing@33817
   134
    fun show_search c = tr [ td' noid [show_criterion c] ];
kleing@33817
   135
  in
kleing@33817
   136
    table (class "findtheoremsquery")
kleing@33817
   137
    (* [ tr [ th (noid, "searched for:") ] ]
kleing@33817
   138
       @ map show_search query @ *)
kleing@33817
   139
      [ tr [ th' noid (found @ [text (displayed ^ ":")]) ] ]
kleing@33817
   140
  end
kleing@33817
   141
kleing@33817
   142
fun sorry_class thm = if is_sorry thm then class "sorried" else noid;
kleing@33817
   143
kleing@33817
   144
fun html_thm ctxt (n, (thmref, thm)) =
kleing@33817
   145
  let
wenzelm@38980
   146
    val output_thm =
wenzelm@36745
   147
      Output.output o Pretty.string_of_margin 100 o
wenzelm@38980
   148
        Display.pretty_thm (Config.put show_question_marks false ctxt);
kleing@33817
   149
  in
wenzelm@41491
   150
    tag' "tr" (class ("row" ^ string_of_int (n mod 2)))
kleing@33817
   151
      [
kleing@33817
   152
        tag' "td" (class "name")
kleing@33817
   153
          [span' (sorry_class thm)
kleing@33817
   154
             [raw_text (Facts.string_of_ref thmref)]
kleing@33817
   155
          ],
wenzelm@38980
   156
        tag' "td" (class "thm") [pre noid (output_thm thm)]
kleing@33817
   157
      ]
kleing@33817
   158
  end;
kleing@33817
   159
kleing@33817
   160
end;
kleing@33817
   161
kleing@33817
   162
val criterion =
wenzelm@36960
   163
  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Find_Theorems.Name ||
wenzelm@36960
   164
  Parse.reserved "intro" >> K Find_Theorems.Intro ||
wenzelm@36960
   165
  Parse.reserved "elim" >> K Find_Theorems.Elim ||
wenzelm@36960
   166
  Parse.reserved "dest" >> K Find_Theorems.Dest ||
wenzelm@36960
   167
  Parse.reserved "solves" >> K Find_Theorems.Solves ||
wenzelm@36960
   168
  Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Find_Theorems.Simp ||
wenzelm@36960
   169
  Parse.term >> Find_Theorems.Pattern;
kleing@33817
   170
kleing@33817
   171
val parse_query =
wenzelm@36960
   172
  Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
kleing@33817
   173
kleing@33817
   174
fun app_index f xs = fold_index (fn x => K (f x)) xs ();
kleing@33817
   175
kleing@33817
   176
fun find_theorems (req as ScgiReq.Req {request_method, query_string, ...},
kleing@33817
   177
                   content, send) =
kleing@33817
   178
  let
kleing@33817
   179
    val arg_data =
kleing@33817
   180
      (case request_method of
kleing@33817
   181
         ScgiReq.Get => query_string
kleing@33817
   182
       | ScgiReq.Post =>
kleing@33817
   183
          content
kleing@33817
   184
          |> Byte.bytesToString
kleing@33817
   185
          |> HttpUtil.parse_query_string
kleing@33817
   186
       | ScgiReq.Head => raise Fail "Cannot handle Head requests.");
kleing@33817
   187
kleing@33817
   188
    val args = Symtab.lookup arg_data;
kleing@33817
   189
kleing@33817
   190
    val query = the_default "" (args "query");
kleing@33817
   191
    fun get_query () =
kleing@33817
   192
      query
kleing@33817
   193
      |> (fn s => s ^ ";")
wenzelm@36960
   194
      |> Outer_Syntax.scan Position.start
wenzelm@36959
   195
      |> filter Token.is_proper
kleing@33817
   196
      |> Scan.error parse_query
kleing@33817
   197
      |> fst;
kleing@33817
   198
kleing@33817
   199
    val limit =
kleing@33817
   200
      args "limit"
kleing@33817
   201
      |> Option.mapPartial Int.fromString
kleing@33817
   202
      |> the_default default_limit;
kleing@33817
   203
    val thy_name =
kleing@33817
   204
      args "theory"
kleing@33817
   205
      |> the_default "Main";
kleing@33817
   206
    val with_dups = is_some (args "with_dups");
kleing@33817
   207
kleing@33817
   208
    fun do_find () =
kleing@33817
   209
      let
wenzelm@37863
   210
        val ctxt = ProofContext.init_global (Thy_Info.get_theory thy_name);
kleing@33817
   211
        val query = get_query ();
kleing@33817
   212
        val (othmslen, thms) = apsnd rev
kleing@33817
   213
          (Find_Theorems.find_theorems ctxt NONE (SOME limit) with_dups query);
kleing@33817
   214
        val thmslen = length thms;
kleing@33817
   215
        fun thm_row args = Xhtml.write send (html_thm ctxt args);
kleing@33817
   216
      in
kleing@33817
   217
        Xhtml.write send
kleing@33817
   218
          (find_theorems_summary (othmslen, thmslen, query, arg_data));
kleing@33817
   219
        if null thms then ()
kleing@33817
   220
        else (Xhtml.write_open send find_theorems_table;
kleing@33817
   221
              HTML_Unicode.print_mode (app_index thm_row) thms;
kleing@33817
   222
              Xhtml.write_close send find_theorems_table)
kleing@33817
   223
      end;
kleing@33817
   224
kleing@33817
   225
    val header = (html_header thy_name (args "query", limit, with_dups));
kleing@33817
   226
  in
kleing@33817
   227
    send Xhtml.doctype_xhtml1_0_strict;
kleing@33817
   228
    Xhtml.write_open send header;
kleing@33817
   229
    if query = "" then ()
kleing@33817
   230
    else
kleing@33817
   231
      do_find ()
kleing@33817
   232
        handle
kleing@33817
   233
          ERROR msg => Xhtml.write send (html_error msg)
wenzelm@41522
   234
        | e => Xhtml.write send (html_error ("Server error: " ^ exnMessage e)); (* FIXME avoid handle e *)
kleing@33817
   235
    Xhtml.write_close send header
kleing@33817
   236
  end;
kleing@33817
   237
in
wenzelm@37216
   238
wenzelm@38980
   239
val () = show_question_marks_default := false;
kleing@33817
   240
val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems);
wenzelm@37216
   241
kleing@33817
   242
end;
kleing@33817
   243