theoremquest-client (empty) → 0.0.0

raw patch · 4 files changed

+183/−0 lines, 4 filesdep +HTTPdep +basedep +networksetup-changed

Dependencies added: HTTP, base, network, theoremquest

Files

• LICENSE +27/−0
• Setup.lhs +8/−0
• TheoremQuestClient.hs +117/−0
• theoremquest-client.cabal +31/−0

@@ -0,0 +1,27 @@+Copyright (c) Tom Hawkins 2011++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:+1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.+2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.+3. Neither the name of the author nor the names of his contributors+   may be used to endorse or promote products derived from this software+   without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE+ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF+SUCH DAMAGE.

@@ -0,0 +1,8 @@+#! /usr/bin/env runhaskell++> module Main (main) where+>+> import Distribution.Simple (defaultMain)+>+> main :: IO ()+> main = defaultMain

@@ -0,0 +1,117 @@+module Main (main) where++import Data.Maybe+import Network.HTTP+import Network.URI+import System.Environment++import TheoremQuest++help :: IO ()+help = putStrLn $ unlines+  [ ""+  , "NAME"+  , "  tq -- a simple TheoremQuest client"+  , ""+  , "SYNOPSYS"+  , "  tq COMMAND { ARGUMENT }"+  , ""+  , "COMMANDS"+  , "  tq help"+  , "    Print this information."+  , ""+  , "  tq ping"+  , "    Ping the server."+  , ""+  , "  tq newuser <username> <email>"+  , "    Create a new user."+  , ""+  , "  tq infer <inference-rule>"+  , "    Apply an inference rule to create a new theorem."+  , ""+  , "  tq theorem <theorem-id>"+  , "    Print the assumptions and proposition of a theorem."+  , ""+  , "  tq check-term <term>"+  , "    Check the syntax (parsing) of a term."+  , ""+  , "  tq check-variable <variable>"+  , "    Check the syntax (parsing) of a variable."+  , ""+  , "  tq check-inference <inference>"+  , "    Check the syntax (parsing) of an inference rule."+  , ""+  , "ENVIRONMENT VARIABLES"+  , "  THEOREMQUEST_USER"+  , "    The TheoremQuest username to use for transactions.  Required for infer commands."+  , ""+  , "  THEOREMQUEST_SERVER"+  , "    URI of the TheoremQuest server.  Default: http://theoremquest.org/cgi-bin/tqcgi"+  , ""+  ]++main :: IO ()+main = getArgs >>= go++-- | Conduct a transaction with the server.+transact :: Req -> IO Rsp+transact req = do+  server <- server+  r <- simpleHTTP $ formatReq server req+  case r of+    Left e -> error $ "failed transaction: " ++ show e+    Right r -> case maybeRead $ rspBody r of+      Just a -> return a+      Nothing -> error $ "response parse error: " ++ show (rspHeaders r) ++ "  " ++ rspBody r+  where+  formatReq uri a = Request+    { rqURI = uri+    , rqMethod = POST+    , rqHeaders = headers+    , rqBody = body+    }+    where+    (headers, body) = formatHaskell a++username :: IO String+username = do+  env <- getEnvironment+  case lookup "THEOREMQUEST_USER" env of+    Just user -> return user+    Nothing -> error "environment variable THEOREMQUEST_USER not set"++server :: IO URI+server = do+  env <- getEnvironment+  return $ fromJust $ parseURI $ case lookup "THEOREMQUEST_SERVER" env of+    Nothing -> "http://theoremquest.org/cgi-bin/tqcgi"+    Just a  -> a++go :: [String] -> IO ()+go args = case args of+  ["newuser", name, email] -> transact (NewUser name email) >>= print+  ["ping"] -> transact Ping >>= print+  ["theorem", n] -> do+    r1 <- transact (TheoremAssumptions theorem)+    case r1 of+      Terms a -> do+        r2 <- transact (TheoremConclusion theorem)+        case r2 of+          Term b -> do+            putStrLn "assumptions:"+            mapM_ print a+            putStrLn "conclusion:"+            print b+          _ -> print r2+      _ -> print r1+    where+    theorem = read n+  ["infer", a] -> do+    user <- username+    r <- transact $ Inference user $ read a+    print r+  ["check-term", a] -> print (read a :: Term)+  ["check-variable", a] -> print (read a :: Variable)+  ["check-inference", a] -> print (read a :: Inference TheoremId)+  _ -> help+

@@ -0,0 +1,31 @@+name:    theoremquest-client+version: 0.0.0++category: Game, Formal Methods, Theorem Provers++synopsis: A simple client for the TheoremQuest theorem proving game.++description:+  TODO++author:     Tom Hawkins <tomahawkins@gmail.com>+maintainer: Tom Hawkins <tomahawkins@gmail.com>++build-type:    Simple+cabal-version: >= 1.6++license:      BSD3+license-file: LICENSE++executable tq+  main-is:           TheoremQuestClient.hs+  build-depends:     base         >= 4.0    && < 5,+                     network      >= 2.3    && < 2.4,+                     HTTP         >= 4000.1 && < 4000.2,+                     theoremquest >= 0.0.0+  ghc-options:       -W++source-repository head+  type:     git+  location: git://github.com/tomahawkins/theoremquest.git+