Browse files

a generic conv-from-a-URL function

calling [url_conv "www.example.com/tactic.cgi" some_term] hopefully
returns a theorem. Uses a system call to curl - don't think there are
libcurl bindings for SML.
  • Loading branch information...
1 parent 833362a commit 5927c967031a9d5836f654043d4ff3c7fde5a43d @xrchz xrchz committed Oct 26, 2011
View
3 src/opentheory/logging/Curl.sig
@@ -0,0 +1,3 @@
+signature Curl = sig
+ val submitFile : {url : string, field : string, file : string} -> TextIO.instream
+end
View
8 src/opentheory/logging/Curl.sml
@@ -0,0 +1,8 @@
+structure Curl :> Curl = struct
+ fun submitFile {url,field,file} = let
+ open OS.Process
+ val t = OS.FileSys.tmpName()
+ val _ = if isSuccess(system("curl -F '"^field^"=@"^file^"' '"^url^"' >"^t)) then ()
+ else raise mk_HOL_ERR "Curl" "submitFile" "curl call failed"
+ in TextIO.openIn t end
+end
View
1 src/opentheory/logging/OpenTheoryIO.sig
@@ -3,4 +3,5 @@ signature OpenTheoryIO = sig
val term_to_article : TextIO.outstream -> term -> unit
val article_to_thm : TextIO.instream -> thm
val article_to_term : TextIO.instream -> term
+ val url_conv : string -> conv
end
View
6 src/opentheory/logging/OpenTheoryIO.sml
@@ -37,4 +37,10 @@ in fn inp =>
handle E t => t
end
+fun url_conv url tm = let
+ val t = OS.FileSys.tmpName()
+ val _ = term_to_article (TextIO.openOut t) tm
+ val t = Curl.submitFile {url=url,field="article",file=t}
+in article_to_thm t end
+
end

0 comments on commit 5927c96

Please sign in to comment.