-- | 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.
{-# LANGUAGE BangPatterns        #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Language.Fixpoint.Solver (
    -- * Invoke Solver on an FInfo
    solve, Solver

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

    -- * Function to determine outcome
  , resultExit
  , resultExitCode

    -- * Parse Qualifiers from File
  , parseFInfo

    -- * Simplified Info
  , simplifyFInfo
) where

import           Control.Concurrent
import           Data.Binary
import           System.Exit                        (ExitCode (..))
import           System.Console.CmdArgs.Verbosity   (whenNormal, whenLoud)
import           Text.PrettyPrint.HughesPJ          (render)
import           Control.Monad                      (when)
import           Control.Exception                  (catch)

import           Language.Fixpoint.Solver.Sanitize  (symbolEnv, sanitize)
import           Language.Fixpoint.Solver.UniqifyBinds (renameAll)
import           Language.Fixpoint.Defunctionalize (defunctionalize)
import           Language.Fixpoint.SortCheck            (Elaborate (..))
import           Language.Fixpoint.Solver.Extensionality (expand)
import           Language.Fixpoint.Solver.UniqifyKVars (wfcUniqify)
import qualified Language.Fixpoint.Solver.Solve     as Sol
import           Language.Fixpoint.Types.Config
import           Language.Fixpoint.Types.Errors
import           Language.Fixpoint.Utils.Files            hiding (Result)
import           Language.Fixpoint.Misc
import           Language.Fixpoint.Utils.Statistics (statistics)
import           Language.Fixpoint.Graph
import           Language.Fixpoint.Parse            (rr')
import           Language.Fixpoint.Types
import           Language.Fixpoint.Minimize (minQuery, minQuals, minKvars)
import           Language.Fixpoint.Solver.Instantiate (instantiate)
import           Control.DeepSeq

---------------------------------------------------------------------------
-- | Solve an .fq file ----------------------------------------------------
---------------------------------------------------------------------------
solveFQ :: Config -> IO ExitCode
solveFQ :: Config -> IO ExitCode
solveFQ Config
cfg = do
    (FInfo ()
fi, [String]
opts) <- String -> IO (FInfo (), [String])
readFInfo String
file
    Config
cfg'       <- Config -> [String] -> IO Config
withPragmas Config
cfg [String]
opts
    let fi' :: FInfo ()
fi'     = Config -> FInfo () -> FInfo ()
forall a. Config -> FInfo a -> FInfo a
ignoreQualifiers Config
cfg' FInfo ()
fi
    Result (Integer, ())
r          <- Solver ()
forall a. (NFData a, Fixpoint a, Show a, Loc a) => Solver a
solve Config
cfg' FInfo ()
fi'
    Result Integer -> IO ExitCode
resultExitCode ((Integer, ()) -> Integer
forall a b. (a, b) -> a
fst ((Integer, ()) -> Integer)
-> Result (Integer, ()) -> Result Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Result (Integer, ())
r)
  where
    file :: String
file    = Config -> String
srcFile      Config
cfg

---------------------------------------------------------------------------
resultExitCode :: Result SubcId -> IO ExitCode 
---------------------------------------------------------------------------
resultExitCode :: Result Integer -> IO ExitCode
resultExitCode Result Integer
r = do 
  -- let str  = render $ resultDoc $!! (const () <$> stat)
  -- putStrLn "\n"
  IO () -> IO ()
whenNormal (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Moods -> String -> IO ()
colorStrLn (FixResult Integer -> Moods
forall a. FixResult a -> Moods
colorResult FixResult Integer
stat) (FixResult Integer -> String
statStr (FixResult Integer -> String) -> FixResult Integer -> String
forall a b. NFData a => (a -> b) -> a -> b
$!! FixResult Integer
stat)
  ExitCode -> IO ExitCode
forall (m :: * -> *) a. Monad m => a -> m a
return (Result Integer -> ExitCode
forall a. Result a -> ExitCode
eCode Result Integer
r)
  where 
    stat :: FixResult Integer
stat    = Result Integer -> FixResult Integer
forall a. Result a -> FixResult a
resStatus (Result Integer -> FixResult Integer)
-> Result Integer -> FixResult Integer
forall a b. NFData a => (a -> b) -> a -> b
$!! Result Integer
r
    eCode :: Result a -> ExitCode
eCode   = FixResult a -> ExitCode
forall a. FixResult a -> ExitCode
resultExit (FixResult a -> ExitCode)
-> (Result a -> FixResult a) -> Result a -> ExitCode
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result a -> FixResult a
forall a. Result a -> FixResult a
resStatus
    statStr :: FixResult Integer -> String
statStr = Doc -> String
render (Doc -> String)
-> (FixResult Integer -> Doc) -> FixResult Integer -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FixResult Integer -> Doc
forall a. Fixpoint a => FixResult a -> Doc
resultDoc 

ignoreQualifiers :: Config -> FInfo a -> FInfo a
ignoreQualifiers :: Config -> FInfo a -> FInfo a
ignoreQualifiers Config
cfg FInfo a
fi
  | Config -> Eliminate
eliminate Config
cfg Eliminate -> Eliminate -> Bool
forall a. Eq a => a -> a -> Bool
== Eliminate
All = FInfo a
fi { quals :: [Qualifier]
quals = [] }
  | Bool
otherwise            = FInfo a
fi


--------------------------------------------------------------------------------
-- | Solve FInfo system of horn-clause constraints -----------------------------
--------------------------------------------------------------------------------
solve :: (NFData a, Fixpoint a, Show a, Loc a) => Solver a
--------------------------------------------------------------------------------
solve :: Solver a
solve Config
cfg FInfo a
q
  | Config -> Bool
parts Config
cfg      = Solver a
forall a (c :: * -> *).
(Fixpoint a, Fixpoint (c a), TaggedC c a) =>
Config -> GInfo c a -> IO (Result (Integer, a))
partition  Config
cfg        (FInfo a -> IO (Result (Integer, a)))
-> FInfo a -> IO (Result (Integer, a))
forall a b. NFData a => (a -> b) -> a -> b
$!! FInfo a
q
  | Config -> Bool
stats Config
cfg      = Solver a
forall a. Config -> FInfo a -> IO (Result (Integer, a))
statistics Config
cfg        (FInfo a -> IO (Result (Integer, a)))
-> FInfo a -> IO (Result (Integer, a))
forall a b. NFData a => (a -> b) -> a -> b
$!! FInfo a
q
  | Config -> Bool
minimize Config
cfg   = Config -> Solver a -> FInfo a -> IO (Result (Integer, a))
forall a.
(NFData a, Fixpoint a) =>
Config -> Solver a -> FInfo a -> IO (Result (Integer, a))
minQuery   Config
cfg Solver a
forall a. (NFData a, Fixpoint a, Show a, Loc a) => Solver a
solve' (FInfo a -> IO (Result (Integer, a)))
-> FInfo a -> IO (Result (Integer, a))
forall a b. NFData a => (a -> b) -> a -> b
$!! FInfo a
q
  | Config -> Bool
minimizeQs Config
cfg = Config -> Solver a -> FInfo a -> IO (Result (Integer, a))
forall a.
(NFData a, Fixpoint a) =>
Config -> Solver a -> FInfo a -> IO (Result (Integer, a))
minQuals Config
cfg Solver a
forall a. (NFData a, Fixpoint a, Show a, Loc a) => Solver a
solve'   (FInfo a -> IO (Result (Integer, a)))
-> FInfo a -> IO (Result (Integer, a))
forall a b. NFData a => (a -> b) -> a -> b
$!! FInfo a
q
  | Config -> Bool
minimizeKs Config
cfg = Config -> Solver a -> FInfo a -> IO (Result (Integer, a))
forall a.
(NFData a, Fixpoint a) =>
Config -> Solver a -> FInfo a -> IO (Result (Integer, a))
minKvars Config
cfg Solver a
forall a. (NFData a, Fixpoint a, Show a, Loc a) => Solver a
solve'   (FInfo a -> IO (Result (Integer, a)))
-> FInfo a -> IO (Result (Integer, a))
forall a b. NFData a => (a -> b) -> a -> b
$!! FInfo a
q
  | Bool
otherwise      = Solver a
forall a. (NFData a, Fixpoint a, Show a, Loc a) => Solver a
solve'     Config
cfg        (FInfo a -> IO (Result (Integer, a)))
-> FInfo a -> IO (Result (Integer, a))
forall a b. NFData a => (a -> b) -> a -> b
$!! FInfo a
q

solve' :: (NFData a, Fixpoint a, Show a, Loc a) => Solver a
solve' :: Solver a
solve' Config
cfg FInfo a
q = do
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
save Config
cfg) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Config -> FInfo a -> IO ()
forall a. Config -> FInfo a -> IO ()
saveQuery   Config
cfg FInfo a
q
  Config -> Solver a -> Solver a
forall a.
(NFData a, Fixpoint a, Show a, Loc a) =>
Config -> Solver a -> Solver a
configSW  Config
cfg     Solver a
forall a. (NFData a, Fixpoint a, Show a, Loc a) => Solver a
solveNative Config
cfg FInfo a
q

configSW :: (NFData a, Fixpoint a, Show a, Loc a) => Config -> Solver a -> Solver a
configSW :: Config -> Solver a -> Solver a
configSW Config
cfg
  | Config -> Bool
multicore Config
cfg = Solver a -> Solver a
forall a. Fixpoint a => Solver a -> Solver a
solveParWith
  | Bool
otherwise     = Solver a -> Solver a
forall a. Fixpoint a => Solver a -> Solver a
solveSeqWith

--------------------------------------------------------------------------------
readFInfo :: FilePath -> IO (FInfo (), [String])
--------------------------------------------------------------------------------
readFInfo :: String -> IO (FInfo (), [String])
readFInfo String
f
  | String -> Bool
isBinary String
f = (,) (FInfo () -> [String] -> (FInfo (), [String]))
-> IO (FInfo ()) -> IO ([String] -> (FInfo (), [String]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO (FInfo ())
readBinFq String
f IO ([String] -> (FInfo (), [String]))
-> IO [String] -> IO (FInfo (), [String])
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return []
  | Bool
otherwise  = String -> IO (FInfo (), [String])
readFq String
f

readFq :: FilePath -> IO (FInfo (), [String])
readFq :: String -> IO (FInfo (), [String])
readFq String
file = do
  String
str   <- String -> IO String
readFile String
file
  let q :: FInfoWithOpts ()
q  = {-# SCC "parsefq" #-} String -> String -> FInfoWithOpts ()
forall a. Inputable a => String -> String -> a
rr' String
file String
str :: FInfoWithOpts ()
  (FInfo (), [String]) -> IO (FInfo (), [String])
forall (m :: * -> *) a. Monad m => a -> m a
return (FInfoWithOpts () -> FInfo ()
forall a. FInfoWithOpts a -> FInfo a
fioFI FInfoWithOpts ()
q, FInfoWithOpts () -> [String]
forall a. FInfoWithOpts a -> [String]
fioOpts FInfoWithOpts ()
q)

readBinFq :: FilePath -> IO (FInfo ())
readBinFq :: String -> IO (FInfo ())
readBinFq String
file = {-# SCC "parseBFq" #-} String -> IO (FInfo ())
forall a. Binary a => String -> IO a
decodeFile String
file

--------------------------------------------------------------------------------
-- | Solve in parallel after partitioning an FInfo to indepdendant parts
--------------------------------------------------------------------------------
solveSeqWith :: (Fixpoint a) => Solver a -> Solver a
solveSeqWith :: Solver a -> Solver a
solveSeqWith Solver a
s Config
c FInfo a
fi0 = {- withProgressFI fi $ -} Solver a
s Config
c FInfo a
fi
  where
    fi :: FInfo a
fi               = Config -> FInfo a -> FInfo a
forall (c :: * -> *) a.
TaggedC c a =>
Config -> GInfo c a -> GInfo c a
slice Config
c FInfo a
fi0

--------------------------------------------------------------------------------
-- | Solve in parallel after partitioning an FInfo to indepdendant parts
--------------------------------------------------------------------------------
solveParWith :: (Fixpoint a) => Solver a -> Solver a
--------------------------------------------------------------------------------
solveParWith :: Solver a -> Solver a
solveParWith Solver a
s Config
c FInfo a
fi0 = do
  -- putStrLn "Using Parallel Solver \n"
  let fi :: FInfo a
fi    = Config -> FInfo a -> FInfo a
forall (c :: * -> *) a.
TaggedC c a =>
Config -> GInfo c a -> GInfo c a
slice Config
c FInfo a
fi0
  MCInfo
mci      <- Config -> IO MCInfo
mcInfo Config
c
  let fis :: [FInfo a]
fis   = Maybe MCInfo -> FInfo a -> [FInfo a]
forall (c :: * -> *) a.
TaggedC c a =>
Maybe MCInfo -> GInfo c a -> [GInfo c a]
partition' (MCInfo -> Maybe MCInfo
forall a. a -> Maybe a
Just MCInfo
mci) FInfo a
fi
  String -> IO ()
writeLoud (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Number of partitions : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([FInfo a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FInfo a]
fis)
  String -> IO ()
writeLoud (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"number of cores      : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Maybe Int -> String
forall a. Show a => a -> String
show (Config -> Maybe Int
cores Config
c)
  String -> IO ()
writeLoud (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"minimum part size    : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Config -> Int
minPartSize Config
c)
  String -> IO ()
writeLoud (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"maximum part size    : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Config -> Int
maxPartSize Config
c)
  case [FInfo a]
fis of
    []        -> String -> IO (Result (Integer, a))
forall a. (?callStack::CallStack) => String -> a
errorstar String
"partiton' returned empty list!"
    [FInfo a
onePart] -> Solver a
s Config
c FInfo a
onePart
    [FInfo a]
_         -> ((Int, FInfo a) -> IO (Result (Integer, a)))
-> [(Int, FInfo a)] -> IO (Result (Integer, a))
forall a b. (a -> IO (Result b)) -> [a] -> IO (Result b)
inParallelUsing (Solver a -> Config -> (Int, FInfo a) -> IO (Result (Integer, a))
forall t t. (Config -> t -> t) -> Config -> (Int, t) -> t
f Solver a
s Config
c) ([(Int, FInfo a)] -> IO (Result (Integer, a)))
-> [(Int, FInfo a)] -> IO (Result (Integer, a))
forall a b. (a -> b) -> a -> b
$ [Int] -> [FInfo a] -> [(Int, FInfo a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] [FInfo a]
fis
    where
      f :: (Config -> t -> t) -> Config -> (Int, t) -> t
f Config -> t -> t
s Config
c (Int
j, t
fi) = Config -> t -> t
s (Config
c {srcFile :: String
srcFile = Ext -> Config -> String
queryFile (Int -> Ext
Part Int
j) Config
c}) t
fi

--------------------------------------------------------------------------------
-- | Solve a list of FInfos using the provided solver function in parallel
--------------------------------------------------------------------------------
inParallelUsing :: (a -> IO (Result b)) -> [a] -> IO (Result b)
--------------------------------------------------------------------------------
inParallelUsing :: (a -> IO (Result b)) -> [a] -> IO (Result b)
inParallelUsing a -> IO (Result b)
f [a]
xs = do
   Int -> IO ()
setNumCapabilities ([a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs)
   [Result b]
rs <- (a -> IO (Result b)) -> [a] -> IO [Result b]
forall a b. (a -> IO b) -> [a] -> IO [b]
asyncMapM a -> IO (Result b)
f [a]
xs
   Result b -> IO (Result b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Result b -> IO (Result b)) -> Result b -> IO (Result b)
forall a b. (a -> b) -> a -> b
$ [Result b] -> Result b
forall a. Monoid a => [a] -> a
mconcat [Result b]
rs

--------------------------------------------------------------------------------
-- | Native Haskell Solver -----------------------------------------------------
--------------------------------------------------------------------------------
solveNative, solveNative' :: (NFData a, Fixpoint a, Show a, Loc a) => Solver a
--------------------------------------------------------------------------------
solveNative :: Solver a
solveNative !Config
cfg !FInfo a
fi0 = (Solver a
forall a. (NFData a, Fixpoint a, Show a, Loc a) => Solver a
solveNative' Config
cfg FInfo a
fi0)
                          IO (Result (Integer, a))
-> (Error -> IO (Result (Integer, a))) -> IO (Result (Integer, a))
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch`
                             (Result (Integer, a) -> IO (Result (Integer, a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Integer, a) -> IO (Result (Integer, a)))
-> (Error -> Result (Integer, a))
-> Error
-> IO (Result (Integer, a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Error -> Result (Integer, a)
forall a. Error -> Result a
result)

result :: Error -> Result a
result :: Error -> Result a
result Error
e = FixResult a -> FixSolution -> GFixSolution -> Result a
forall a. FixResult a -> FixSolution -> GFixSolution -> Result a
Result ([a] -> String -> FixResult a
forall a. [a] -> String -> FixResult a
Crash [] String
msg) FixSolution
forall a. Monoid a => a
mempty GFixSolution
forall a. Monoid a => a
mempty
  where
    msg :: String
msg  = Error -> String
forall a. PPrint a => a -> String
showpp Error
e

loudDump :: (Fixpoint a) => Int -> Config -> SInfo a -> IO ()
loudDump :: Int -> Config -> SInfo a -> IO ()
loudDump Int
i Config
cfg SInfo a
si = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
False (String -> IO ()
writeLoud (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
render (Config -> SInfo a -> Doc
forall a (c :: * -> *).
(Fixpoint a, Fixpoint (c a)) =>
Config -> GInfo c a -> Doc
toFixpoint Config
cfg SInfo a
si))
  where
    msg :: String
msg           = String
"fq file after Uniqify & Rename " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"

simplifyFInfo :: (NFData a, Fixpoint a, Show a, Loc a)
               => Config -> FInfo a -> IO (SInfo a)
simplifyFInfo :: Config -> FInfo a -> IO (SInfo a)
simplifyFInfo !Config
cfg !FInfo a
fi0 = do
  -- writeLoud $ "fq file in: \n" ++ render (toFixpoint cfg fi)
  -- rnf fi0 `seq` donePhase Loud "Read Constraints"
  -- let qs   = quals fi0
  -- whenLoud $ print qs
  -- whenLoud $ putStrLn $ showFix (quals fi1)
  let fi1 :: FInfo a
fi1   = FInfo a
fi0 { quals :: [Qualifier]
quals = Qualifier -> Qualifier
remakeQual (Qualifier -> Qualifier) -> [Qualifier] -> [Qualifier]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FInfo a -> [Qualifier]
forall (c :: * -> *) a. GInfo c a -> [Qualifier]
quals FInfo a
fi0 }
  let si0 :: SInfo a
si0   = {-# SCC "convertFormat" #-} FInfo a -> SInfo a
forall a. Fixpoint a => FInfo a -> SInfo a
convertFormat FInfo a
fi1
  -- writeLoud $ "fq file after format convert: \n" ++ render (toFixpoint cfg si0)
  -- rnf si0 `seq` donePhase Loud "Format Conversion"
  let si1 :: SInfo a
si1   = (Error -> SInfo a)
-> (SInfo a -> SInfo a) -> Either Error (SInfo a) -> SInfo a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Error -> SInfo a
forall a. Error -> a
die SInfo a -> SInfo a
forall a. a -> a
id (Either Error (SInfo a) -> SInfo a)
-> Either Error (SInfo a) -> SInfo a
forall a b. (a -> b) -> a -> b
$ {-# SCC "sanitize" #-} Config -> SInfo a -> Either Error (SInfo a)
forall a. Config -> SInfo a -> SanitizeM (SInfo a)
sanitize Config
cfg (SInfo a -> Either Error (SInfo a))
-> SInfo a -> Either Error (SInfo a)
forall a b. NFData a => (a -> b) -> a -> b
$!! SInfo a
si0
  -- writeLoud $ "fq file after sanitize: \n" ++ render (toFixpoint cfg si1)
  -- rnf si1 `seq` donePhase Loud "Validated Constraints"
  Config -> SInfo a -> IO ()
forall (c :: * -> *) a. TaggedC c a => Config -> GInfo c a -> IO ()
graphStatistics Config
cfg SInfo a
si1
  let si2 :: SInfo a
si2  = {-# SCC "wfcUniqify" #-} SInfo a -> SInfo a
forall a. SInfo a -> SInfo a
wfcUniqify (SInfo a -> SInfo a) -> SInfo a -> SInfo a
forall a b. NFData a => (a -> b) -> a -> b
$!! SInfo a
si1
  let si3 :: SInfo a
si3  = {-# SCC "renameAll"  #-} SInfo a -> SInfo a
forall a. SInfo a -> SInfo a
renameAll  (SInfo a -> SInfo a) -> SInfo a -> SInfo a
forall a b. NFData a => (a -> b) -> a -> b
$!! SInfo a
si2
  SInfo a -> ()
forall a. NFData a => a -> ()
rnf SInfo a
si3 () -> IO () -> IO ()
`seq` IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Moods -> String -> IO ()
donePhase Moods
Loud String
"Uniqify & Rename"
  Int -> Config -> SInfo a -> IO ()
forall a. Fixpoint a => Int -> Config -> SInfo a -> IO ()
loudDump Int
1 Config
cfg SInfo a
si3
  let si4 :: SInfo a
si4  = {-# SCC "defunction" #-} Config -> SInfo a -> SInfo a
forall a. Fixpoint a => Config -> SInfo a -> SInfo a
defunctionalize Config
cfg (SInfo a -> SInfo a) -> SInfo a -> SInfo a
forall a b. NFData a => (a -> b) -> a -> b
$!! SInfo a
si3
  -- putStrLn $ "AXIOMS: " ++ showpp (asserts si4)
  Int -> Config -> SInfo a -> IO ()
forall a. Fixpoint a => Int -> Config -> SInfo a -> IO ()
loudDump Int
2 Config
cfg SInfo a
si4
  let si5 :: SInfo a
si5  = {-# SCC "elaborate"  #-} Located String -> SymEnv -> SInfo a -> SInfo a
forall a. Elaborate a => Located String -> SymEnv -> a -> a
elaborate (SrcSpan -> String -> Located String
forall l b. Loc l => l -> b -> Located b
atLoc SrcSpan
dummySpan String
"solver") (Config -> SInfo a -> SymEnv
forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
si4) SInfo a
si4
  Int -> Config -> SInfo a -> IO ()
forall a. Fixpoint a => Int -> Config -> SInfo a -> IO ()
loudDump Int
3 Config
cfg SInfo a
si5
  let si6 :: SInfo a
si6  = if Config -> Bool
extensionality Config
cfg then {-# SCC "expand"     #-} Config -> SInfo a -> SInfo a
forall a. Config -> SInfo a -> SInfo a
expand Config
cfg SInfo a
si5 else SInfo a
si5
  Config -> SInfo a -> IO (SInfo a)
forall a. Loc a => Config -> SInfo a -> IO (SInfo a)
instantiate Config
cfg (SInfo a -> IO (SInfo a)) -> SInfo a -> IO (SInfo a)
forall a b. NFData a => (a -> b) -> a -> b
$!! SInfo a
si6


solveNative' :: Solver a
solveNative' !Config
cfg !FInfo a
fi0 = do
  SInfo a
si6 <- Config -> FInfo a -> IO (SInfo a)
forall a.
(NFData a, Fixpoint a, Show a, Loc a) =>
Config -> FInfo a -> IO (SInfo a)
simplifyFInfo Config
cfg FInfo a
fi0
  Result (Integer, a)
res <- {-# SCC "Sol.solve" #-} Config -> SInfo a -> IO (Result (Integer, a))
forall a.
(NFData a, Fixpoint a, Show a, Loc a) =>
Config -> SInfo a -> IO (Result (Integer, a))
Sol.solve Config
cfg (SInfo a -> IO (Result (Integer, a)))
-> SInfo a -> IO (Result (Integer, a))
forall a b. NFData a => (a -> b) -> a -> b
$!! SInfo a
si6
  -- rnf soln `seq` donePhase Loud "Solve2"
  --let stat = resStatus res
  Config -> Result (Integer, a) -> IO ()
forall a. Config -> Result a -> IO ()
saveSolution Config
cfg Result (Integer, a)
res
  -- when (save cfg) $ saveSolution cfg
  -- writeLoud $ "\nSolution:\n"  ++ showpp (resSolution res)
  -- colorStrLn (colorResult stat) (show stat)
  Result (Integer, a) -> IO (Result (Integer, a))
forall (m :: * -> *) a. Monad m => a -> m a
return Result (Integer, a)
res

--------------------------------------------------------------------------------
-- | Parse External Qualifiers -------------------------------------------------
--------------------------------------------------------------------------------
parseFInfo :: [FilePath] -> IO (FInfo a)
--------------------------------------------------------------------------------
parseFInfo :: [String] -> IO (FInfo a)
parseFInfo [String]
fs = [FInfo a] -> FInfo a
forall a. Monoid a => [a] -> a
mconcat ([FInfo a] -> FInfo a) -> IO [FInfo a] -> IO (FInfo a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> IO (FInfo a)) -> [String] -> IO [FInfo a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> IO (FInfo a)
forall a. String -> IO (FInfo a)
parseFI [String]
fs

parseFI :: FilePath -> IO (FInfo a)
parseFI :: String -> IO (FInfo a)
parseFI String
f = do
  String
str   <- String -> IO String
readFile String
f
  let fi :: FInfo ()
fi = String -> String -> FInfo ()
forall a. Inputable a => String -> String -> a
rr' String
f String
str :: FInfo ()
  FInfo a -> IO (FInfo a)
forall (m :: * -> *) a. Monad m => a -> m a
return (FInfo a -> IO (FInfo a)) -> FInfo a -> IO (FInfo a)
forall a b. (a -> b) -> a -> b
$ FInfo a
forall a. Monoid a => a
mempty { quals :: [Qualifier]
quals = FInfo () -> [Qualifier]
forall (c :: * -> *) a. GInfo c a -> [Qualifier]
quals  FInfo ()
fi
                  , gLits :: SEnv Sort
gLits = FInfo () -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
gLits  FInfo ()
fi
                  , dLits :: SEnv Sort
dLits = FInfo () -> SEnv Sort
forall (c :: * -> *) a. GInfo c a -> SEnv Sort
dLits  FInfo ()
fi }

saveSolution :: Config -> Result a -> IO ()
saveSolution :: Config -> Result a -> IO ()
saveSolution Config
cfg Result a
res = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
save Config
cfg) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
  let f :: String
f = Ext -> Config -> String
queryFile Ext
Out Config
cfg
  String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Saving Solution: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"
  String -> IO ()
ensurePath String
f
  String -> String -> IO ()
writeFile String
f (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"\nSolution:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FixSolution -> String
forall a. PPrint a => a -> String
showpp (Result a -> FixSolution
forall a. Result a -> FixSolution
resSolution  Result a
res)
                String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if (Config -> Bool
gradual Config
cfg) then (String
"\n\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ GFixSolution -> String
forall a. PPrint a => a -> String
showpp (Result a -> GFixSolution
forall a. Result a -> GFixSolution
gresSolution Result a
res)) else String
forall a. Monoid a => a
mempty)