added experimental yxml_find_theorems web service (but no client yet)
authorkrauss
Mon May 30 17:07:48 2011 +0200 (2011-05-30)
changeset 430756fde0c323c15
parent 43074 8b566f0d226c
child 43076 7b06cd71792c
added experimental yxml_find_theorems web service (but no client yet)
src/Tools/WWW_Find/IsaMakefile
src/Tools/WWW_Find/ROOT.ML
src/Tools/WWW_Find/lib/Tools/wwwfind
src/Tools/WWW_Find/scgi_server.ML
src/Tools/WWW_Find/yxml_find_theorems.ML
     1.1 --- a/src/Tools/WWW_Find/IsaMakefile	Mon May 30 17:07:48 2011 +0200
     1.2 +++ b/src/Tools/WWW_Find/IsaMakefile	Mon May 30 17:07:48 2011 +0200
     1.3 @@ -30,7 +30,8 @@
     1.4  
     1.5  $(LOGFILE): $(OUT)/Pure echo.ML find_theorems.ML html_unicode.ML \
     1.6    html_templates.ML http_status.ML http_util.ML mime.ML scgi_req.ML \
     1.7 -  scgi_server.ML socket_util.ML unicode_symbols.ML xhtml.ML ROOT.ML
     1.8 +  scgi_server.ML socket_util.ML unicode_symbols.ML xhtml.ML yxml_find_theorems.ML \
     1.9 +  ROOT.ML
    1.10  	@cd ..; $(ISABELLE_TOOL) usedir Pure WWW_Find
    1.11  
    1.12  
     2.1 --- a/src/Tools/WWW_Find/ROOT.ML	Mon May 30 17:07:48 2011 +0200
     2.2 +++ b/src/Tools/WWW_Find/ROOT.ML	Mon May 30 17:07:48 2011 +0200
     2.3 @@ -11,5 +11,6 @@
     2.4    use "scgi_server.ML";
     2.5    use "echo.ML";
     2.6    use "html_templates.ML";
     2.7 -  use "find_theorems.ML")
     2.8 +  use "find_theorems.ML";
     2.9 +  use "yxml_find_theorems.ML")
    2.10  else ()
     3.1 --- a/src/Tools/WWW_Find/lib/Tools/wwwfind	Mon May 30 17:07:48 2011 +0200
     3.2 +++ b/src/Tools/WWW_Find/lib/Tools/wwwfind	Mon May 30 17:07:48 2011 +0200
     3.3 @@ -124,7 +124,7 @@
     3.4  
     3.5  WWWPORT=`sed -e 's/[ 	]*//g' -ne 's/server.port=\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
     3.6  SCGIPORT=`sed -e 's/[ 	]*//g' -ne 's/"port"=>\([0-9][0-9]*\),\?/\1/p' "$WWWCONFIG"`
     3.7 -MLSTARTSERVER="ScgiServer.server' 10 \"/\" $SCGIPORT;"
     3.8 +MLSTARTSERVER="YXML_Find_Theorems.init (); ScgiServer.server' 10 \"/\" $SCGIPORT;"
     3.9  
    3.10  case "$COMMAND" in
    3.11    start)
     4.1 --- a/src/Tools/WWW_Find/scgi_server.ML	Mon May 30 17:07:48 2011 +0200
     4.2 +++ b/src/Tools/WWW_Find/scgi_server.ML	Mon May 30 17:07:48 2011 +0200
     4.3 @@ -12,6 +12,7 @@
     4.4    val server : string -> int -> unit
     4.5    val server' : int -> string -> int -> unit (* keeps trying for port *)
     4.6    val simple_handler : (string Symtab.table -> (string -> unit) -> unit) -> handler
     4.7 +  val raw_post_handler : (string -> string) -> handler
     4.8  end;
     4.9  
    4.10  structure ScgiServer : SCGI_SERVER =
    4.11 @@ -132,5 +133,9 @@
    4.12     | ScgiReq.Head => raise Fail "Cannot handle Head requests.")
    4.13    send;
    4.14  
    4.15 +fun raw_post_handler h (ScgiReq.Req {request_method=ScgiReq.Post, ...}, content, send) =
    4.16 +      send (h (Byte.bytesToString content))
    4.17 +  | raw_post_handler _ _ = raise Fail "Can only handle POST request.";
    4.18 +
    4.19  end;
    4.20  
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Tools/WWW_Find/yxml_find_theorems.ML	Mon May 30 17:07:48 2011 +0200
     5.3 @@ -0,0 +1,47 @@
     5.4 +(*  Title:      src/Pure/Tools/yxml_find_theorems.ML
     5.5 +    Author:     Sree Harsha Totakura, TUM
     5.6 +                Lars Noschinski, TUM
     5.7 +                Alexander Krauss, TUM
     5.8 +
     5.9 +Simple find theorems web service with yxml interface for programmatic
    5.10 +invocation.
    5.11 +*)
    5.12 +
    5.13 +signature YXML_FIND_THEOREMS =
    5.14 +sig
    5.15 +  val init: unit -> unit
    5.16 +end
    5.17 +
    5.18 +
    5.19 +structure YXML_Find_Theorems : YXML_FIND_THEOREMS =
    5.20 +struct
    5.21 +
    5.22 +val the_theory = "Main"; (* FIXME!!! EXPERIMENTAL *)
    5.23 +
    5.24 +fun yxml_find_theorems theorem_list yxml_query =
    5.25 +  let
    5.26 +    val ctxt = Proof_Context.init_global (Thy_Info.get_theory the_theory);
    5.27 +  in
    5.28 +    Find_Theorems.query_of_xml (YXML.parse yxml_query)
    5.29 +    |> Find_Theorems.filter_theorems ctxt theorem_list
    5.30 +    ||> rev o (filter (fn Find_Theorems.External x => true | _ => false))
    5.31 +    |> Find_Theorems.xml_of_result |> YXML.string_of
    5.32 +  end;
    5.33 +
    5.34 +fun visible_facts facts =
    5.35 +  Facts.dest_static [] facts
    5.36 +  |> filter_out (Facts.is_concealed facts o #1);
    5.37 +
    5.38 +fun init () = 
    5.39 +  let
    5.40 +    val all_facts =
    5.41 +      maps Facts.selections
    5.42 +        (visible_facts (Global_Theory.facts_of (Thy_Info.get_theory the_theory)))
    5.43 +      |> map (Find_Theorems.External o apsnd prop_of);
    5.44 +  in
    5.45 +    ScgiServer.register ("yxml_find_theorems", SOME Mime.html (*FIXME?*),
    5.46 +      ScgiServer.raw_post_handler (yxml_find_theorems all_facts))
    5.47 +  end;
    5.48 +
    5.49 +end;
    5.50 +