{-# OPTIONS_GHC -Wno-name-shadowing #-}

-------------------------------------------------------------------------------
-- | 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
cfg = do
  (Query Tag
q, [String]
opts) <- Config -> IO (Query Tag, [String])
parseQuery Config
cfg

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

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

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

  Result (Integer, Tag)
r <- forall a.
(PPrint a, NFData a, Loc a, Show a, Fixpoint a) =>
Config -> Query a -> IO (Result (Integer, a))
solve Config
cfg Query Tag
q
  forall a.
(Fixpoint a, NFData a, ToJSON a) =>
Config -> Result a -> IO ExitCode
Solver.resultExitCode Config
cfg 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 = forall a. Parser a -> IO a
Parse.parseFromStdIn Parser (Query Tag, [String])
H.hornP
  | Bool
otherwise   = 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 forall a b. (a -> b) -> a -> b
$ String
"Saving Horn Query: " forall a. [a] -> [a] -> [a]
++ String
hq forall a. [a] -> [a] -> [a]
++ String
"\n"
  String -> IO ()
Misc.ensurePath String
hq
  String -> String -> IO ()
writeFile String
hq forall a b. (a -> b) -> a -> b
$ Doc -> String
render (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 forall a. Eq a => a -> a -> Bool
== Eliminate
F.Existentials = do
    forall a. PPrint a => Config -> Query a -> IO (Query a)
Tx.solveEbs Config
cfg Query a
q
  | Config -> Eliminate
F.eliminate Config
cfg forall a. Eq a => a -> a -> Bool
== Eliminate
F.Horn = do
    let c :: Cstr a
c = forall a. Cstr a -> Cstr a
Tx.elim forall a b. (a -> b) -> a -> b
$ forall a. Query a -> Cstr a
H.qCstr Query a
q
    IO () -> IO ()
whenLoud forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Horn Elim:"
    IO () -> IO ()
whenLoud forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => a -> String
F.showpp Cstr a
c
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Query a
q { qCstr :: Cstr a
H.qCstr = Cstr a
c }
  | Bool
otherwise = 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
q = do
  let c :: Cstr a
c = forall a. Cstr a -> Cstr a
Tx.uniq forall a b. (a -> b) -> a -> b
$ forall a. Flatten a => a -> a
Tx.flatten forall a b. (a -> b) -> a -> b
$ forall a. Query a -> Cstr a
H.qCstr Query a
q
  IO () -> IO ()
whenLoud forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Horn Uniq:"
  IO () -> IO ()
whenLoud forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => a -> String
F.showpp Cstr a
c
  Query a
q <- forall a. PPrint a => Config -> Query a -> IO (Query a)
eliminate Config
cfg ({- void $ -} Query a
q { qCstr :: Cstr a
H.qCstr = Cstr a
c })
  forall a.
(PPrint a, NFData a, Fixpoint a, Show a, Loc a) =>
Solver a
Solver.solve Config
cfg (forall a. Config -> Query a -> FInfo a
hornFInfo Config
cfg Query a
q)