-- | This module implements the top-level API for interfacing with Fixpoint
--   In particular it exports the functions that solve constraints supplied
--   either as .fq files or as FInfo.

module Language.Fixpoint.Interface (

    -- * Containing Constraints
    FInfo (..)

    -- * Invoke Solver on an FInfo
  , solve

    -- * Invoke Solver on a .fq file
  , solveFQ

    -- * Function to determine outcome
  , resultExit

    -- * Parse Qualifiers from File
  , parseFInfo
) where

import           Data.Functor
-- import           Data.Hashable
import qualified Data.HashMap.Strict              as M
import           Data.List
import           Data.Monoid (mconcat, mempty)
-- import           System.Directory                 (getTemporaryDirectory)
import           System.Exit
-- import           System.FilePath                  ((</>))
import           System.IO                        (IOMode (..), hPutStr,
                                                   withFile)
import           Text.Printf

import           Language.Fixpoint.Solver.Eliminate (eliminateAll)
import qualified Language.Fixpoint.Solver.Solve  as S
import           Language.Fixpoint.Config
import           Language.Fixpoint.Files
import           Language.Fixpoint.Misc
import           Language.Fixpoint.Parse          (rr, rr')
import           Language.Fixpoint.Types          hiding (kuts, lits)
import           Language.Fixpoint.Errors (exit)
import           Language.Fixpoint.PrettyPrint (showpp)
-- import           System.Console.CmdArgs.Default
import           System.Console.CmdArgs.Verbosity
import           Text.PrettyPrint.HughesPJ


---------------------------------------------------------------------------
-- | Solve FInfo system of horn-clause constraints ------------------------
---------------------------------------------------------------------------
solve :: Config -> FInfo a -> IO (Result a)
solve cfg
  | native cfg = S.solve  cfg
  | otherwise  = solveExt cfg

---------------------------------------------------------------------------
-- | Solve .fq File -------------------------------------------------------
---------------------------------------------------------------------------
solveFQ :: Config -> IO ExitCode
---------------------------------------------------------------------------
solveFQ cfg
  | native cfg = solveNative' cfg
  | otherwise  = solveFile    cfg


---------------------------------------------------------------------------
-- | Fake Dependencies Harness Solver
---------------------------------------------------------------------------
solveNative :: Config -> IO ExitCode
solveNative cfg
  = do let file = inFile cfg
       str     <- readFile file
       let fi   = rr' file str :: FInfo ()
       let res  = eliminateAll fi
       putStrLn $ "Result: \n" ++ (render $ toFixpoint res)
       error "TODO: solveNative"

---------------------------------------------------------------------------
-- | Native Haskell Solver
---------------------------------------------------------------------------
solveNative' :: Config -> IO ExitCode
solveNative' cfg = exit (ExitFailure 2) $ do
  let file  = inFile cfg
  str      <- readFile file
  let fi    = rr' file str :: FInfo ()
  let fi'   = if eliminate cfg then eliminateAll fi else fi
  (res, s) <- S.solve cfg fi'
  let res'  = sid <$> res
  putStrLn  $ "Solution:\n" ++ showpp s
  putStrLn  $ "Result: "    ++ show res'
  return    $ resultExit res'

---------------------------------------------------------------------------
-- | External Ocaml Solver
---------------------------------------------------------------------------
solveExt :: Config -> FInfo a -> IO (Result a)
solveExt cfg fi =   {-# SCC "Solve"  #-} execFq cfg fn fi
                >>= {-# SCC "exitFq" #-} exitFq fn (cm fi)
  where
    fn          = srcFile cfg

execFq cfg fn fi
  = do writeFile fq qstr
       withFile fq AppendMode (\h -> {-# SCC "HPrintDump" #-} hPutStr h (render d))
       solveFile $ cfg `withTarget` fq
    where
       fq   = extFileName Fq fn
       d    = {-# SCC "FixPointify" #-} toFixpoint fi
       qstr = render ((vcat $ toFix <$> quals fi) $$ text "\n")

solveFile :: Config -> IO ExitCode
solveFile cfg
  = do fp  <- getFixpointPath
       z3  <- getZ3LibPath
       v   <- (\b -> if b then "-v 1" else "") <$> isLoud
       {-# SCC "sysCall:Fixpoint" #-} executeShellCommand "fixpoint" $ fixCommand cfg fp z3 v

fixCommand cfg fp z3 verbosity
  = printf "LD_LIBRARY_PATH=%s %s %s %s -notruekvars -refinesort -nosimple -strictsortcheck -sortedquals %s"
           z3 fp verbosity rf (command cfg)
  where
     rf  = if real cfg then realFlags else ""

realFlags =  "-no-uif-multiply "
          ++ "-no-uif-divide "

exitFq _ _ (ExitFailure n) | n /= 1
  = return (Crash [] "Unknown Error", M.empty)
exitFq fn cm _
  = do str <- {-# SCC "readOut" #-} readFile (extFileName Out fn)
       let (x, y) = parseFixpointOutput str -- {-# SCC "parseFixOut" #-} rr ({-# SCC "sanitizeFixpointOutput" #-} sanitizeFixpointOutput str)
       return  $ (plugC cm x, y)
    where
       plugC = fmap . mlookup

parseFixpointOutput :: String -> (FixResult Integer, FixSolution)
parseFixpointOutput str = {-# SCC "parseFixOut" #-} rr ({-# SCC "sanitizeFixpointOutput" #-} sanitizeFixpointOutput str)

sanitizeFixpointOutput
  = unlines
  . filter (not . ("//"     `isPrefixOf`))
  . chopAfter ("//QUALIFIERS" `isPrefixOf`)
  . lines

---------------------------------------------------------------------------
resultExit :: FixResult a -> ExitCode
---------------------------------------------------------------------------
resultExit Safe        = ExitSuccess
resultExit (Unsafe _)  = ExitFailure 1
resultExit _           = ExitFailure 2


---------------------------------------------------------------------------
-- | Parse External Qualifiers --------------------------------------------
---------------------------------------------------------------------------
parseFInfo :: [FilePath] -> IO (FInfo a) -- [Qualifier]
---------------------------------------------------------------------------
parseFInfo fs = mconcat <$> mapM parseFI fs

parseFI :: FilePath -> IO (FInfo a) --[Qualifier]
parseFI f = do
  str   <- readFile f
  let fi = rr' f str :: FInfo ()
  return $ mempty { quals = quals  fi
                  , gs    = gs     fi }

-- OLD CUT USE NEW SMTLIB INTERFACE ---------------------------------------------------------------------------
-- OLD CUT USE NEW SMTLIB INTERFACE -- | One Shot validity query ----------------------------------------------
-- OLD CUT USE NEW SMTLIB INTERFACE ---------------------------------------------------------------------------
-- OLD CUT USE NEW SMTLIB INTERFACE 
-- OLD CUT USE NEW SMTLIB INTERFACE ---------------------------------------------------------------------------
-- OLD CUT USE NEW SMTLIB INTERFACE checkValid :: (Hashable a) => a -> [(Symbol, Sort)] -> Pred -> IO (FixResult a)
-- OLD CUT USE NEW SMTLIB INTERFACE ---------------------------------------------------------------------------
-- OLD CUT USE NEW SMTLIB INTERFACE checkValid n xts p
-- OLD CUT USE NEW SMTLIB INTERFACE   = do file   <- (</> show (hash n)) <$> getTemporaryDirectory
-- OLD CUT USE NEW SMTLIB INTERFACE        (r, _) <- solve def file [] $ validFInfo n xts p
-- OLD CUT USE NEW SMTLIB INTERFACE        return (sinfo <$> r)
-- OLD CUT USE NEW SMTLIB INTERFACE 
-- OLD CUT USE NEW SMTLIB INTERFACE validFInfo         :: a -> [(Symbol, Sort)] -> Pred -> FInfo a
-- OLD CUT USE NEW SMTLIB INTERFACE validFInfo l xts p = FI constrm [] benv emptySEnv [] ksEmpty []
-- OLD CUT USE NEW SMTLIB INTERFACE   where
-- OLD CUT USE NEW SMTLIB INTERFACE     constrm        = M.singleton 0 $ validSubc l ibenv p
-- OLD CUT USE NEW SMTLIB INTERFACE     binds          = [(x, trueSortedReft t) | (x, t) <- xts]
-- OLD CUT USE NEW SMTLIB INTERFACE     ibenv          = insertsIBindEnv bids emptyIBindEnv
-- OLD CUT USE NEW SMTLIB INTERFACE     (bids, benv)   = foldlMap (\e (x,t) -> insertBindEnv x t e) emptyBindEnv binds
-- OLD CUT USE NEW SMTLIB INTERFACE 
-- OLD CUT USE NEW SMTLIB INTERFACE validSubc         :: a -> IBindEnv -> Pred -> SubC a
-- OLD CUT USE NEW SMTLIB INTERFACE validSubc l env p = safeHead "Interface.validSubC" $ subC env PTrue lhs rhs i t l
-- OLD CUT USE NEW SMTLIB INTERFACE   where
-- OLD CUT USE NEW SMTLIB INTERFACE     lhs           = mempty
-- OLD CUT USE NEW SMTLIB INTERFACE     rhs           = RR mempty (predReft p)
-- OLD CUT USE NEW SMTLIB INTERFACE     i             = Just 0
-- OLD CUT USE NEW SMTLIB INTERFACE     t             = []
-- OLD CUT USE NEW SMTLIB INTERFACE 
-- OLD CUT USE NEW SMTLIB INTERFACE result         :: a -> Bool -> FixResult a
-- OLD CUT USE NEW SMTLIB INTERFACE result _ True  = Safe
-- OLD CUT USE NEW SMTLIB INTERFACE result x False = Unsafe [x]
-- OLD CUT USE NEW SMTLIB INTERFACE