This module contains the code for stand-alone use. 
Module declaration: 

\begin{code}
module Main

where 

import Form
import Hylotab
import System
import Exception
import Concurrent
import Dynamic
import Unique
\end{code}

The imports \verb^Exception^, \verb^Concurrent^, 
\verb^Dynamic^, \verb^Unique^ are used by the function \verb^timeout^. 

\begin{code}
data TimeOut = TimeOut Unique

timeOutTc = mkTyCon "TimeOut"
instance Typeable TimeOut where { typeOf _ = mkAppTy timeOutTc [] }

timeout :: Integer -> IO () -> IO () -> IO ()
timeout secs action on_timeout =
    let {
         timeout_thread secs parent i =
         do {
             threadDelay ((fromInteger secs) * 1000000);
             throwTo parent (DynException (toDyn (TimeOut i)))
            }
        } in
   do {
       parent  <- myThreadId;
       i       <- newUnique;
       block (do
          timeout <- forkIO (timeout_thread secs parent i);
          Exception.catchDyn
            ( unblock (
                do {
                   result <- action;
                   killThread timeout;
                   return result;
                   }
              )
            )
            ( \exception ->
                case exception of
                    TimeOut u | u == i -> unblock on_timeout
                    other -> do {
                                killThread timeout;
                                throwDyn exception
                                }
            )
         )
	}
\end{code}

Information banner for cases where the {\em hylotab}\/ command is
invoked without command line arguments.

\begin{code}
showInfo :: IO ()
showInfo = putStrLn ("HyLoTab 1.00: no input file.\n" ++
		     "Usage: `--help' option gives basic information.\n")
\end{code}

Help on usage: 

\begin{code}
showHelp :: IO ()
showHelp = putStrLn ("Usage: \n" ++
 "  hylotab [SATOPTION] [FRAMEOPTION] ... FILE\n\n" ++
 "  satoption   : --help (print this help information)\n" ++
 "                --min  (search for minimal models)\n" ++
 "  frameoptions: -trans -k4 -intrans -refl -kt -irrefl -symm\n" ++
 "                -kb -asymm -s4 -kt4 -s5 -serial -kd -euclid\n" ++
 "                -k5 -kdb -kd4 -kd5 -k45 -kd45 -kb4 -ktb -antisymm\n\n" ++
 "  Examples of use:\n\n" ++
 "  hylotab -s4 form1           (satisfy form1 in s4 model)\n" ++
 "  hylotab -refl -trans form1  (idem) \n" ++
 "  hylotab --min -kt form1     (satisfy form1 in minimal refl model)\n" ++
 "  hylotab --min -refl form1   (idem)\n\n")
\end{code}

List of frame options: 

\begin{code}
frameOptions :: [String] 
frameOptions = ["-trans", "-k4", "-intrans", "-refl", "-kt", "-irrefl", 
                "-symm", "-kb", "-asymm", "-s4", "-kt4", "-s5", 
                "-serial", "-kd", "-euclid", "-k5", "-kdb", "-kd4", 
                "-kd5", "-k45", "-kd45", "-kb4", "-ktb", "-antisymm"]
\end{code}

Converting an option to the corresponding formula: 

\begin{code}
option2form :: String -> Form 
option2form "-trans"    = trans
option2form "-k4"       = k4 
option2form "-intrans"  = intrans 
option2form "-refl"     = refl
option2form "-kt"       = kt
option2form "-irrefl"   = irrefl
option2form "-symm"     = symm
option2form "-kb"       = kb
option2form "-asymm"    = asymm
option2form "-s4"       = s4
option2form "-kt4"      = kt4
option2form "-s5"       = s5
option2form "-serial"   = serial
option2form "-kd"       = kd
option2form "-euclid"   = euclid
option2form "-k5"       = k5
option2form "-kdb"      = kdb
option2form "-kd4"      = kd4
option2form "-kd5"      = kd5
option2form "-k45"      = k45
option2form "-kd45"     = kd45
option2form "-kb4"      = kb4
option2form "-ktb"      = ktb
option2form "-antisymm" = antisymm
\end{code}

Parse the command line arguments. Return of \verb^[]^ indicates error.
If no error occurs, the return is of the form \verb^[(md,fs,name)]^, 
where \verb^md^ indicates the mode in which the satisfaction engine 
gets called, the value of \verb^fs^ lists the frame conditions, and the 
value of \verb^name^ gives the filename. 

\begin{code}
parseArgs :: [String] -> [(Mode,[Form],String)]
parseArgs args = parseArgs' args (Extend,[])

parseArgs' :: [String] -> (Mode,[Form]) -> [(Mode,[Form],String)]
parseArgs' [] (md,flist) = []
parseArgs' [name] (md,flist) = if (head name == '-') then [] 
                               else [(md,flist,name)]
parseArgs' (arg:args) (md,flist) 
  | arg == "--help"       = []
  | arg == "--min"        = parseArgs' args (Try,flist)
  | elem arg frameOptions = parseArgs' args (md,((option2form arg):flist))
  | otherwise             = []
\end{code}

Set a treshold for the number of seconds that the prover should run. 

\begin{code}
treshold :: Integer
treshold = 100
\end{code}

The function \verb^main^ parses the command line and, if all goes well, 
calls the generic satisfaction function in the appropriate way for the 
formula read from the named file. 

\begin{code}
main :: IO ()
main = do { 
	   args <- getArgs;
	   if null args then showInfo
           else if parseArgs args == [] then showHelp
           else let [(md,fs,name)] = parseArgs args in 
                     do {
                          fstring <- readFile name; 
                          let { form = str2form fstring;  };
                          putStr ("Formula: " ++ show form ++ "\n");
                          timeout treshold 
                           (genSat md fs form)           -- call to prover
                           (putStr "Timeout reached.\n") -- exit by timeout
                        }
          }
\end{code}