Issue23 (#37)

This closes #23 * added --cpu-password flag and --debug flag * [ test-suite ] fixed basic.test
jonaprieto · Jan 26, 2017 · 8d83f2d · 8d83f2d
1 parent e496351
commit 8d83f2d
Show file tree

Hide file tree

Showing 6 changed files with 115 additions and 15 deletions.
diff --git a/online-atps.cabal b/online-atps.cabal
@@ -52,6 +52,7 @@ executable online-atps
                 , mtl >= 2.2.1 && < 2.3
                 , network >= 2.6.0 && < 3.0
                 , pretty >= 1.1.1.0 && < 1.1.1.2 || >= 1.1.2 && < 1.2
+                , pretty-show >= 1.6.12 && <= 2.0
                 --, safe >= 0.3.5 && < 0.4
                 , split >= 0.2 && < 1.0
                 , tagsoup >= 0.14 && < 1.0

diff --git a/src/Main.hs b/src/Main.hs
@@ -31,6 +31,7 @@ import OnlineATPs.Options
   , Options
     ( optATP
     , optATPList
+    , optDebug
     , optHelp
     , optInputFile
     , optOnlyCheck
@@ -54,6 +55,8 @@ import System.Directory           ( doesFileExist )
 import System.Environment         ( getArgs )
 import System.Exit                ( exitFailure, exitSuccess )
 
+import qualified Text.Show.Pretty as Pr
+
 -- | Main function.
 main ∷ IO ()
 main = do
@@ -95,16 +98,19 @@ main = do
 
           form ∷ Either Msg SystemOnTPTP ← getSystemOnTPTP opts
 
-          case form of
-            Left msg   → putStrLn msg >> exitFailure
-            Right spec →
-              if optOnlyCheck opts
-                then do
+          if optDebug opts then
+            putStrLn $ Pr.ppShow opts
+          else
+            case form of
+              Left msg   → putStrLn msg >> exitFailure
+              Right spec →
+                if optOnlyCheck opts
+                  then do
 
-                  answer ∷ String ← checkTheoremSync spec
-                  putStrLn answer >> exitSuccess
+                    answer ∷ String ← checkTheoremSync spec
+                    putStrLn answer >> exitSuccess
 
-                else do
+                  else do
 
-                  response ∷ L.ByteString ← getResponseSystemOnTPTP spec
-                  C.putStrLn response >> exitSuccess
+                    response ∷ L.ByteString ← getResponseSystemOnTPTP spec
+                    C.putStrLn response >> exitSuccess
diff --git a/src/OnlineATPs/Consult.hs b/src/OnlineATPs/Consult.hs
@@ -53,7 +53,30 @@ import OnlineATPs.Defaults      ( getDefaults )
 import OnlineATPs.Options       ( getManageOpt, Options (..) )
 import OnlineATPs.SystemATP     ( SystemATP (..), isFOFATP, setTimeLimit )
 import OnlineATPs.SystemOnTPTP
-  ( SystemOnTPTP (..)
+  ( SystemOnTPTP
+    ( optAutoMode
+    , optAutoModeSystemsLimit
+    , optAutoModeTimeLimit
+    , optCompleteness
+    , optCorrectness
+    , optCPUPassword
+    , optFORMULAEProblem
+    , optFormulaURL
+    , optIDV
+    , optNoHTML
+    , optProblemSource
+    , optQuietFlag
+    , optReportFlag
+    , optSoundness
+    , optSubmitButton
+    , optSystemInfo
+    , optSystemOnTSTP
+    , optSystems
+    , optTPTPProblem
+    , optTSTPData
+    , optUPLOADProblem
+    , optX2TPTP
+    )
   , getDataSystemOnTPTP
   , setFORMULAEProblem
   , setSystems
@@ -195,7 +218,8 @@ getSystemATPWith atps name =
         Just atp → atp
         _        → NoSystemATP
 
--- | The function 'getSystemATP' tries to find an ATP given the specification -- from its input.
+-- | The function 'getSystemATP' tries to find an ATP given the specification
+-- from its input.
 getSystemATP ∷ Options → IO SystemATP
 getSystemATP opts =
   let name = optVersionATP opts in
@@ -237,7 +261,8 @@ getResponseSystemOnTPTP spec = withSocketsDo $ do
     let response = responseBody res
     return response
 
--- | The function 'getSystemOnTPTP' reads some options including the problem file and it sends all this information to TPTP World.
+-- | The function 'getSystemOnTPTP' reads some options including the problem
+-- file and it sends all this information to TPTP World.
 getSystemOnTPTP ∷ Options → IO (Either Msg SystemOnTPTP)
 getSystemOnTPTP opts = do
 
@@ -257,6 +282,19 @@ getSystemOnTPTP opts = do
 
   defaults ∷ SystemOnTPTP ← getDefaults
 
+  -- ---------------------------------------------------------------------------
+  -- Update defaults info for SystemOnTPTP based on arguments
+  -- given on the command-line.
+
+  let finals ∷ SystemOnTPTP
+      finals = defaults {
+          optCPUPassword = case optCPUPassword (optSystemOnTPTP opts) of
+            []   → optCPUPassword defaults
+            pass → pass
+    }
+
+  -- ---------------------------------------------------------------------------
+
   let file ∷ Maybe FilePath
       file = optInputFile opts
 
@@ -267,6 +305,6 @@ getSystemOnTPTP opts = do
       contentFile ∷ String ← readFile $ fromJust file
 
       let form ∷ SystemOnTPTP
-          form  = setFORMULAEProblem (setSystems defaults setATPs) contentFile
+          form  = setFORMULAEProblem (setSystems finals setATPs) contentFile
 
       return $ Right form
diff --git a/src/OnlineATPs/Options.hs b/src/OnlineATPs/Options.hs
@@ -13,9 +13,11 @@ module OnlineATPs.Options
     ( Options --Improve Haddock information.
     , optATP
     , optATPList
+    , optDebug
     , optFOF
     , optHelp
     , optInputFile
+    , optSystemOnTPTP
     , optOnlyCheck
     , optTime
     , optVersion
@@ -29,6 +31,33 @@ module OnlineATPs.Options
 import Data.Char ( isDigit )
 import Data.List ( foldl', nub )
 
+import OnlineATPs.Defaults ( defaultSystemOnTPTP )
+import OnlineATPs.SystemOnTPTP
+  ( SystemOnTPTP
+    ( optAutoMode
+    , optAutoModeSystemsLimit
+    , optAutoModeTimeLimit
+    , optCompleteness
+    , optCorrectness
+    , optCPUPassword
+    , optFORMULAEProblem
+    , optFormulaURL
+    , optIDV
+    , optNoHTML
+    , optProblemSource
+    , optQuietFlag
+    , optReportFlag
+    , optSoundness
+    , optSubmitButton
+    , optSystemInfo
+    , optSystemOnTSTP
+    , optSystems
+    , optTPTPProblem
+    , optTSTPData
+    , optUPLOADProblem
+    , optX2TPTP
+    )
+  )
 import OnlineATPs.Utils.PrettyPrint
   ( Doc
   , Pretty ( pretty )
@@ -49,6 +78,7 @@ import System.Environment ( getProgName )
 -- | 'ManageOption' handles the options from the defaults and the command
 -- line.
 data ManageOption a = DefaultOpt a | CommandOpt a
+                    deriving Show
 
 -- | The function 'getManageOpt' extracts the value from the
 -- 'Options.ManageOption' data type.
@@ -61,24 +91,29 @@ getManageOpt (CommandOpt val) = val
 data Options = Options
   { optATP            ∷ ManageOption [String]
   , optATPList        ∷ Bool
+  , optDebug          ∷ Bool
   , optFOF            ∷ Bool
   , optHelp           ∷ Bool
   , optInputFile      ∷ Maybe FilePath
+  , optSystemOnTPTP   ∷ SystemOnTPTP
   , optOnlyCheck      ∷ Bool
   , optTime           ∷ Int
   , optVersion        ∷ Bool
   , optVersionATP     ∷ String
   , optWithAll        ∷ Bool
   }
+  deriving Show
 
 
 defaultOptions ∷ Options
 defaultOptions = Options
   { optATP            = DefaultOpt []
   , optATPList        = False
+  , optDebug          = False
   , optFOF            = False
   , optHelp           = False
   , optInputFile      = Nothing
+  , optSystemOnTPTP   = defaultSystemOnTPTP
   , optOnlyCheck      = False
   , optTime           = 240
   , optVersion        = False
@@ -103,6 +138,20 @@ atpOpt name opts = Right opts { optATP = CommandOpt atps }
 atpListOpt ∷ MOptions
 atpListOpt opts = Right opts { optATPList = True }
 
+cpuPasswordOpt ∷ String → MOptions
+cpuPasswordOpt [] _ = Left $
+  pretty "option " <> squotes "--cpu-password" <> pretty " requires an argument KEY"
+cpuPasswordOpt pass opts = Right opts { optSystemOnTPTP = newTPTP }
+  where
+    sTPTP ∷ SystemOnTPTP
+    sTPTP = optSystemOnTPTP opts
+
+    newTPTP ∷ SystemOnTPTP
+    newTPTP = sTPTP { optCPUPassword = pass }
+
+debugOpt ∷ MOptions
+debugOpt opts = Right opts { optDebug = True }
+
 fofOpt ∷ MOptions
 fofOpt opts = Right opts { optFOF = True }
 
@@ -115,7 +164,6 @@ inputFileOpt file opts =
     Nothing → Right opts { optInputFile = Just file }
     Just _  → Left $ pretty "only one input file allowed"
 
-
 onlyCheckOpt ∷ MOptions
 onlyCheckOpt opts = Right opts { optOnlyCheck = True }
 
@@ -144,6 +192,10 @@ options ∷ [OptDescr MOptions]
 options =
   [ Option []  ["atp"] (ReqArg atpOpt "NAME")
                "Set the ATP (online-e, online-vampire, online-z3, ...)\n"
+  , Option []  ["cpu-password"] (ReqArg cpuPasswordOpt "KEY")
+                "Set the CPU Password on SystemOnTPTP\n"
+  , Option []  ["debug"] (NoArg debugOpt)
+                "Prints out debug information to check the form for SystemOnTPTP"
   , Option []  ["fof"] (NoArg fofOpt)
                "Only use ATP for FOF"
   , Option []  ["help"] (NoArg helpOpt)

diff --git a/src/OnlineATPs/SystemOnTPTP.hs b/src/OnlineATPs/SystemOnTPTP.hs
@@ -243,6 +243,7 @@ getters = [
 getDataSystemOnTPTP ∷ SystemOnTPTP → [(String, String)]
 getDataSystemOnTPTP spec = concatMap ($ spec) getters
 
+
 -- | The function 'setFORMULAEProblem' sets the problem in the format TSTP.
 setFORMULAEProblem ∷ SystemOnTPTP → String → SystemOnTPTP
 setFORMULAEProblem spec problemText = spec { optFORMULAEProblem = problemText }

diff --git a/test/basics/basics.test b/test/basics/basics.test
@@ -5,6 +5,8 @@
 Usage: online-atps [OPTIONS] FILE
 
     --atp=NAME          Set the ATP (online-e, online-vampire, online-z3, ...)
+    --cpu-password=KEY  Set the CPU Password on SystemOnTPTP
+    --debug             Prints out debug information to check the form for SystemOnTPTP
     --fof               Only use ATP for FOF
     --help              Show this help
     --list-atps         Consult all ATPs available in TPTP World