src/Tools/WWW_Find/yxml_find_theorems.ML
author wenzelm
Sat, 09 Jul 2011 21:53:27 +0200
changeset 43721 fad8634cee62
parent 43275 327b91364464
permissions -rw-r--r--
echo prover input via raw_messages, for improved protocol tracing;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43275
327b91364464 standardized header;
wenzelm
parents: 43075
diff changeset
     1
(*  Title:      Tools/WWW_Find/yxml_find_theorems.ML
43075
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
     2
    Author:     Sree Harsha Totakura, TUM
43275
327b91364464 standardized header;
wenzelm
parents: 43075
diff changeset
     3
    Author:     Lars Noschinski, TUM
327b91364464 standardized header;
wenzelm
parents: 43075
diff changeset
     4
    Author:     Alexander Krauss, TUM
43075
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
     5
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
     6
Simple find theorems web service with yxml interface for programmatic
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
     7
invocation.
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
     8
*)
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
     9
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    10
signature YXML_FIND_THEOREMS =
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    11
sig
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    12
  val init: unit -> unit
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    13
end
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    14
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    15
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    16
structure YXML_Find_Theorems : YXML_FIND_THEOREMS =
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    17
struct
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    18
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    19
val the_theory = "Main"; (* FIXME!!! EXPERIMENTAL *)
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    20
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    21
fun yxml_find_theorems theorem_list yxml_query =
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    22
  let
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    23
    val ctxt = Proof_Context.init_global (Thy_Info.get_theory the_theory);
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    24
  in
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    25
    Find_Theorems.query_of_xml (YXML.parse yxml_query)
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    26
    |> Find_Theorems.filter_theorems ctxt theorem_list
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    27
    ||> rev o (filter (fn Find_Theorems.External x => true | _ => false))
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    28
    |> Find_Theorems.xml_of_result |> YXML.string_of
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    29
  end;
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    30
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    31
fun visible_facts facts =
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    32
  Facts.dest_static [] facts
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    33
  |> filter_out (Facts.is_concealed facts o #1);
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    34
43275
327b91364464 standardized header;
wenzelm
parents: 43075
diff changeset
    35
fun init () =
43075
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    36
  let
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    37
    val all_facts =
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    38
      maps Facts.selections
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    39
        (visible_facts (Global_Theory.facts_of (Thy_Info.get_theory the_theory)))
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    40
      |> map (Find_Theorems.External o apsnd prop_of);
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    41
  in
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    42
    ScgiServer.register ("yxml_find_theorems", SOME Mime.html (*FIXME?*),
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    43
      ScgiServer.raw_post_handler (yxml_find_theorems all_facts))
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    44
  end;
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    45
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    46
end;
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
diff changeset
    47