import Language.Fixpoint.Interface (solveFile)
import System.Environment (getArgs)
-- import System.Console.GetOpt
import Language.Fixpoint.Config hiding (config)
import Data.Maybe (fromMaybe, listToMaybe)
import System.Console.CmdArgs
import System.Console.CmdArgs.Verbosity (whenLoud)
import Control.Applicative ((<$>))
import Language.Fixpoint.Parse
import Language.Fixpoint.Types
import Text.PrettyPrint.HughesPJ
main = do cfg <- getOpts
whenLoud $ putStrLn $ "Options: " ++ show cfg
if (native cfg)
then solveNative (inFile cfg)
else solveFile cfg
config = Config {
inFile = def &= typ "TARGET" &= args &= typFile
, outFile = "out" &= help "Output file"
, solver = def &= help "Name of SMT Solver"
, genSorts = def &= help "Generalize qualifier sorts"
, ueqAllSorts = def &= help "use UEq on all sorts"
, native = False &= help "Use (new, non-working) Haskell Solver"
, real = False &= help "Experimental support for the theory of real numbers"
}
&= verbosity
&= program "fixpoint"
&= help "Predicate Abstraction Based Horn-Clause Solver"
&= summary "fixpoint Copyright 2009-13 Regents of the University of California."
&= details [ "Predicate Abstraction Based Horn-Clause Solver"
, ""
, "To check a file foo.fq type:"
, " fixpoint foo.fq"
]
getOpts :: IO Config
getOpts = do md <- cmdArgs config
putStrLn $ banner md
return md
banner args = "Liquid-Fixpoint Copyright 2009-13 Regents of the University of California.\n"
++ "All Rights Reserved.\n"
---------------------------------------------------------------------------------
-- Hook for Haskell Solver ------------------------------------------------------
---------------------------------------------------------------------------------
solveNative file
= do str <- readFile file
let q = rr' file str :: FInfo ()
res <- solveQuery q
putStrLn $ "Result: " ++ show res
error "TODO: enzo"
--------------------------------------------------------------
solveQuery :: FInfo a -> IO (FixResult a)
--------------------------------------------------------------
solveQuery q
= do putStrLn $ "Query Was: " ++ (render $ toFixpoint q)
return Safe
-- error "TODO: Enzo"