1structure OpenTheoryIO :> OpenTheoryIO = struct
2
3open Opentheory Logging HolKernel
4
5val ERR = Feedback.mk_HOL_ERR "OpenTheoryIO"
6
7fun thm_to_article out th = let
8  val _ = raw_start_logging out
9  val th = th()
10  val _ = export_thm th
11  val _ = stop_logging()
12in () end
13
14fun term_to_article out t = thm_to_article out
15  (fn()=>mk_thm([],list_mk_comb(inst[alpha|->bool,beta|->type_of t]``combin$K``,[boolSyntax.F,t])))
16
17val article_to_thm = let
18  val ERR = ERR "article_to_thm"
19in fn inp => let
20  val thms = raw_read_article inp {
21    define_tyop = fn _ => raise ERR "define_tyop",
22    define_const = fn _ => raise ERR "define_const",
23    axiom = axiom_in_db,
24    const_name = const_name_in_map,
25    tyop_name = tyop_name_in_map}
26in hd (Net.listItems thms) end end
27
28val article_to_term = let
29  exception E of term
30  val ERR = ERR "article_to_term"
31in fn inp =>
32  ( raw_read_article inp {
33    define_tyop = fn _ => raise ERR "define_tyop",
34    define_const = fn _ => raise ERR "define_const",
35    axiom = fn _ => fn (_,c) => raise (E (rand c)),
36    const_name = const_name_in_map,
37    tyop_name = tyop_name_in_map } ; raise ERR "no theorem" )
38  handle E t => boolSyntax.rhs(concl(NUMERAL_conv t)) handle UNCHANGED => t
39end
40
41fun url_conv url tm = let
42  val t = OS.FileSys.tmpName()
43  val _ = term_to_article (TextIO.openOut t) tm
44  val t = Curl.submitFile {url=url,field="article",file=t}
45in article_to_thm t end
46
47end
48