-------------------------------------------------------------------------------
-- | 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.SMTParse   as SH

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 qualified Data.Aeson as Aeson
-- import Debug.Trace (traceM)

----------------------------------------------------------------------------------
solveHorn :: F.Config -> IO ExitCode
----------------------------------------------------------------------------------
solveHorn :: Config -> IO ExitCode
solveHorn Config
baseCfg = do
  Query Tag
q <- Config -> IO (Query Tag)
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 (Query Tag -> [String]
forall a. Query a -> [String]
H.qOpts Query Tag
q)

  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.TagQuery
parseQuery :: Config -> IO (Query Tag)
parseQuery Config
cfg
  | Config -> Bool
F.stdin Config
cfg = Parser (Query Tag) -> IO (Query Tag)
forall a. Parser a -> IO a
Parse.parseFromStdIn Parser (Query Tag)
hornP
  | Bool
json        = String -> IO (Query Tag)
loadFromJSON String
file
  | Bool
otherwise   = Parser (Query Tag) -> String -> IO (Query Tag)
forall b. Parser b -> String -> IO b
Parse.parseFromFile Parser (Query Tag)
hornP String
file
  where
    json :: Bool
json  = Ext -> String -> Bool
Files.isExtFile Ext
Files.Json String
file
    file :: String
file  = Config -> String
F.srcFile Config
cfg
    hornP :: Parser (Query Tag)
hornP = if Config -> Bool
F.noSmtHorn Config
cfg then Parser (Query Tag)
H.hornP else Parser (Query Tag)
SH.hornP

loadFromJSON :: FilePath -> IO H.TagQuery
loadFromJSON :: String -> IO (Query Tag)
loadFromJSON String
f = do
  Either String (Query Tag)
r <- String -> IO (Either String (Query Tag))
forall a. FromJSON a => String -> IO (Either String a)
Aeson.eitherDecodeFileStrict String
f
  case Either String (Query Tag)
r of
    Right Query Tag
v -> Query Tag -> IO (Query Tag)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Query Tag
v
    Left String
err -> String -> IO (Query Tag)
forall a. HasCallStack => String -> a
error (String
"Error in loadFromJSON: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
err)

saveHornQuery :: F.Config -> H.Query H.Tag -> IO ()
saveHornQuery :: Config -> Query Tag -> IO ()
saveHornQuery Config
cfg Query Tag
q = do
  Config -> Query Tag -> IO ()
forall a. ToHornSMT a => Config -> a -> IO ()
saveHornSMT2 Config
cfg Query Tag
q
  Config -> Query Tag -> IO ()
saveHornJSON Config
cfg Query Tag
q

saveHornSMT2 :: H.ToHornSMT a => F.Config -> a -> IO ()
saveHornSMT2 :: forall a. ToHornSMT a => Config -> a -> IO ()
saveHornSMT2 Config
cfg a
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 ({- F.pprint -} a -> Doc
forall a. ToHornSMT a => a -> Doc
H.toHornSMT a
q)

saveHornJSON :: F.Config -> H.Query H.Tag -> IO ()
saveHornJSON :: Config -> Query Tag -> IO ()
saveHornJSON Config
cfg Query Tag
q = do
  let hjson :: String
hjson   = Ext -> Config -> String
F.queryFile Ext
Files.HJSON 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
hjson String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"
  String -> IO ()
Misc.ensurePath String
hjson
  String -> Query Tag -> IO ()
forall a. ToJSON a => String -> a -> IO ()
Aeson.encodeFile String
hjson Query Tag
q

----------------------------------------------------------------------------------
eliminate :: (F.Fixpoint a, F.PPrint a) => F.Config -> H.Query a -> IO (H.Query a)
----------------------------------------------------------------------------------
eliminate :: forall a.
(Fixpoint 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.
(Fixpoint 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.
(Fixpoint 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. (Fixpoint a, PPrint a) => Config -> Query a -> FInfo a
hornFInfo Config
cfg Query a
q)