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