-------------------------------------------------------------------------------
-- | This module defines a function to solve NNF constraints,
--   by reducing them to the standard FInfo.
-------------------------------------------------------------------------------

module Language.Fixpoint.Horn.Solve (solveHorn, solve) where

import System.Exit ( ExitCode )
import Control.DeepSeq ( NFData )
import Control.Monad (when)
import qualified Language.Fixpoint.Misc         as Misc
import qualified Language.Fixpoint.Utils.Files  as Files
import qualified Language.Fixpoint.Solver       as Solver
import qualified Language.Fixpoint.Parse        as Parse
import qualified Language.Fixpoint.Types        as F
import qualified Language.Fixpoint.Types.Config as F
import qualified Language.Fixpoint.Horn.Types   as H
import qualified Language.Fixpoint.Horn.Parse   as H
import qualified Language.Fixpoint.Horn.Transformations as Tx
import Text.PrettyPrint.HughesPJ.Compat ( render )
import Language.Fixpoint.Horn.Info ( hornFInfo )

import System.Console.CmdArgs.Verbosity ( whenLoud )

-- import Debug.Trace (traceM)

----------------------------------------------------------------------------------
solveHorn :: F.Config -> IO ExitCode
----------------------------------------------------------------------------------
solveHorn :: Config -> IO ExitCode
solveHorn Config
baseCfg = do
  (Query Tag
q, [String]
opts) <- Config -> IO (Query Tag, [String])
parseQuery Config
baseCfg

  -- If you want to set --eliminate=none, you better make it a pragma
  Config
cfgElim <- if Config -> Eliminate
F.eliminate Config
baseCfg Eliminate -> Eliminate -> Bool
forall a. Eq a => a -> a -> Bool
== Eliminate
F.None
           then Config -> IO Config
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Config
baseCfg { F.eliminate =  F.Some })
           else Config -> IO Config
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Config
baseCfg

  Config
cfgPragmas <- Config -> [String] -> IO Config
F.withPragmas Config
cfgElim [String]
opts

  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
F.save Config
cfgPragmas) (Config -> Query Tag -> IO ()
saveHornQuery Config
cfgPragmas Query Tag
q)

  Result (Integer, Tag)
r <- Config -> Query Tag -> IO (Result (Integer, Tag))
forall a.
(PPrint a, NFData a, Loc a, Show a, Fixpoint a) =>
Config -> Query a -> IO (Result (Integer, a))
solve Config
cfgPragmas Query Tag
q
  Config -> Result (Integer, Tag) -> IO ExitCode
forall a.
(Fixpoint a, NFData a, ToJSON a) =>
Config -> Result a -> IO ExitCode
Solver.resultExitCode Config
cfgPragmas Result (Integer, Tag)
r

parseQuery :: F.Config -> IO (H.Query H.Tag, [String])
parseQuery :: Config -> IO (Query Tag, [String])
parseQuery Config
cfg
  | Config -> Bool
F.stdin Config
cfg = Parser (Query Tag, [String]) -> IO (Query Tag, [String])
forall a. Parser a -> IO a
Parse.parseFromStdIn Parser (Query Tag, [String])
H.hornP
  | Bool
otherwise   = Parser (Query Tag, [String]) -> String -> IO (Query Tag, [String])
forall b. Parser b -> String -> IO b
Parse.parseFromFile Parser (Query Tag, [String])
H.hornP (Config -> String
F.srcFile Config
cfg)

saveHornQuery :: F.Config -> H.Query H.Tag -> IO ()
saveHornQuery :: Config -> Query Tag -> IO ()
saveHornQuery Config
cfg Query Tag
q = do
  let hq :: String
hq   = Ext -> Config -> String
F.queryFile Ext
Files.HSmt2 Config
cfg
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Saving Horn Query: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
hq String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"
  String -> IO ()
Misc.ensurePath String
hq
  String -> String -> IO ()
writeFile String
hq (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> String
render (Query Tag -> Doc
forall a. PPrint a => a -> Doc
F.pprint Query Tag
q)

----------------------------------------------------------------------------------
eliminate :: (F.PPrint a) => F.Config -> H.Query a -> IO (H.Query a)
----------------------------------------------------------------------------------
eliminate :: forall a. PPrint a => Config -> Query a -> IO (Query a)
eliminate Config
cfg Query a
q
  | Config -> Eliminate
F.eliminate Config
cfg Eliminate -> Eliminate -> Bool
forall a. Eq a => a -> a -> Bool
== Eliminate
F.Existentials = do
    Config -> Query a -> IO (Query a)
forall a. PPrint a => Config -> Query a -> IO (Query a)
Tx.solveEbs Config
cfg Query a
q
  | Config -> Eliminate
F.eliminate Config
cfg Eliminate -> Eliminate -> Bool
forall a. Eq a => a -> a -> Bool
== Eliminate
F.Horn = do
    let c :: Cstr a
c = Cstr a -> Cstr a
forall a. Cstr a -> Cstr a
Tx.elim (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ Query a -> Cstr a
forall a. Query a -> Cstr a
H.qCstr Query a
q
    IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Horn Elim:"
    IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Cstr a -> String
forall a. PPrint a => a -> String
F.showpp Cstr a
c
    Query a -> IO (Query a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Query a -> IO (Query a)) -> Query a -> IO (Query a)
forall a b. (a -> b) -> a -> b
$ Query a
q { H.qCstr = c }
  | Bool
otherwise = Query a -> IO (Query a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Query a
q

----------------------------------------------------------------------------------
solve :: (F.PPrint a, NFData a, F.Loc a, Show a, F.Fixpoint a) => F.Config -> H.Query a
       -> IO (F.Result (Integer, a))
----------------------------------------------------------------------------------
solve :: forall a.
(PPrint a, NFData a, Loc a, Show a, Fixpoint a) =>
Config -> Query a -> IO (Result (Integer, a))
solve Config
cfg Query a
qry = do
  let c :: Cstr a
c = Cstr a -> Cstr a
forall a. Cstr a -> Cstr a
Tx.uniq (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ Cstr a -> Cstr a
forall a. Flatten a => a -> a
Tx.flatten (Cstr a -> Cstr a) -> Cstr a -> Cstr a
forall a b. (a -> b) -> a -> b
$ Query a -> Cstr a
forall a. Query a -> Cstr a
H.qCstr Query a
qry
  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Horn Uniq:"
  IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Cstr a -> String
forall a. PPrint a => a -> String
F.showpp Cstr a
c
  Query a
q <- Config -> Query a -> IO (Query a)
forall a. PPrint a => Config -> Query a -> IO (Query a)
eliminate Config
cfg ({- void $ -} Query a
qry { H.qCstr = c })
  Solver a
forall a.
(PPrint a, NFData a, Fixpoint a, Show a, Loc a) =>
Solver a
Solver.solve Config
cfg (Config -> Query a -> FInfo a
forall a. Config -> Query a -> FInfo a
hornFInfo Config
cfg Query a
q)