Skip to content
This repository
Browse code

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...
commit 5927c967031a9d5836f654043d4ff3c7fde5a43d 1 parent 833362a
Ramana Kumar xrchz authored
3  src/opentheory/logging/Curl.sig
... ... @@ -0,0 +1,3 @@
  1 +signature Curl = sig
  2 + val submitFile : {url : string, field : string, file : string} -> TextIO.instream
  3 +end
8 src/opentheory/logging/Curl.sml
... ... @@ -0,0 +1,8 @@
  1 +structure Curl :> Curl = struct
  2 + fun submitFile {url,field,file} = let
  3 + open OS.Process
  4 + val t = OS.FileSys.tmpName()
  5 + val _ = if isSuccess(system("curl -F '"^field^"=@"^file^"' '"^url^"' >"^t)) then ()
  6 + else raise mk_HOL_ERR "Curl" "submitFile" "curl call failed"
  7 + in TextIO.openIn t end
  8 +end
1  src/opentheory/logging/OpenTheoryIO.sig
@@ -3,4 +3,5 @@ signature OpenTheoryIO = sig
3 3 val term_to_article : TextIO.outstream -> term -> unit
4 4 val article_to_thm : TextIO.instream -> thm
5 5 val article_to_term : TextIO.instream -> term
  6 + val url_conv : string -> conv
6 7 end
6 src/opentheory/logging/OpenTheoryIO.sml
@@ -37,4 +37,10 @@ in fn inp =>
37 37 handle E t => t
38 38 end
39 39
  40 +fun url_conv url tm = let
  41 + val t = OS.FileSys.tmpName()
  42 + val _ = term_to_article (TextIO.openOut t) tm
  43 + val t = Curl.submitFile {url=url,field="article",file=t}
  44 +in article_to_thm t end
  45 +
40 46 end

0 comments on commit 5927c96

Please sign in to comment.
Something went wrong with that request. Please try again.