{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
module Language.Fixpoint.Solver (
solve, Solver
, solveFQ
, resultExit
, resultExitCode
, parseFInfo
, simplifyFInfo
) where
import Control.Concurrent (setNumCapabilities)
import qualified Data.HashMap.Strict as HashMap
import qualified Data.Store as S
import Data.Aeson (ToJSON, encode)
import qualified Data.Text.Lazy.IO as LT
import qualified Data.Text.Lazy.Encoding as LT
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.EnvironmentReduction
(reduceEnvironments, simplifyBindings)
import Language.Fixpoint.Solver.Sanitize (symbolEnv, sanitize)
import Language.Fixpoint.Solver.UniqifyBinds (renameAll)
import Language.Fixpoint.Defunctionalize (defunctionalize)
import Language.Fixpoint.SortCheck (Elaborate (..), unElab)
import Language.Fixpoint.Solver.Extensionality (expand)
import Language.Fixpoint.Solver.Prettify (savePrettifiedQuery)
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
import qualified Data.ByteString as B
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'
Config -> Result Integer -> IO ExitCode
forall a.
(Fixpoint a, NFData a, ToJSON a) =>
Config -> Result a -> IO ExitCode
resultExitCode Config
cfg ((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 :: (Fixpoint a, NFData a, ToJSON a) => Config -> Result a
-> IO ExitCode
resultExitCode :: Config -> Result a -> IO ExitCode
resultExitCode Config
cfg Result a
r = do
IO () -> IO ()
whenNormal (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Moods -> String -> IO ()
colorStrLn (FixResult a -> Moods
forall a. FixResult a -> Moods
colorResult FixResult a
stat) (FixResult a -> String
statStr (FixResult a -> String) -> FixResult a -> String
forall a b. NFData a => (a -> b) -> a -> b
$!! FixResult a
stat)
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
json Config
cfg) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Text -> IO ()
LT.putStrLn Text
jStr
ExitCode -> IO ExitCode
forall (m :: * -> *) a. Monad m => a -> m a
return (Result a -> ExitCode
forall a. Result a -> ExitCode
eCode Result a
r)
where
jStr :: Text
jStr = ByteString -> Text
LT.decodeUtf8 (ByteString -> Text)
-> (Result a -> ByteString) -> Result a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result a -> ByteString
forall a. ToJSON a => a -> ByteString
encode (Result a -> Text) -> Result a -> Text
forall a b. (a -> b) -> a -> b
$ Result a
r
stat :: FixResult a
stat = Result a -> FixResult a
forall a. Result a -> FixResult a
resStatus (Result a -> FixResult a) -> Result a -> FixResult a
forall a b. NFData a => (a -> b) -> a -> b
$!! Result a
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 a -> String
statStr = Doc -> String
render (Doc -> String) -> (FixResult a -> Doc) -> FixResult a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FixResult a -> 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 :: (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. Fixpoint 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 = 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" #-} do
ByteString
bs <- String -> IO ByteString
B.readFile String
file
case ByteString -> Either PeekException (FInfo ())
forall a. Store a => ByteString -> Either PeekException a
S.decode ByteString
bs of
Right FInfo ()
fi -> FInfo () -> IO (FInfo ())
forall (m :: * -> *) a. Monad m => a -> m a
return FInfo ()
fi
Left PeekException
err -> String -> IO (FInfo ())
forall a. HasCallStack => String -> a
error (String
"Error decoding .bfq: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PeekException -> String
forall a. Show a => a -> String
show PeekException
err)
solveSeqWith :: (Fixpoint a) => Solver a -> Solver a
solveSeqWith :: Solver a -> Solver a
solveSeqWith Solver a
s Config
c FInfo a
fi0 = 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
solveParWith :: (Fixpoint a) => Solver a -> Solver a
solveParWith :: Solver a -> Solver a
solveParWith Solver a
s Config
c FInfo a
fi0 = do
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. HasCallStack => 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
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
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 -> FixSolution -> GFixSolution -> Result a
forall a.
FixResult a
-> FixSolution -> 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 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"
{-# SCC simplifyFInfo #-}
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
FInfo a
reducedFi <- Config -> FInfo a -> IO (FInfo a)
forall a. Fixpoint a => Config -> FInfo a -> IO (FInfo a)
reduceFInfo Config
cfg FInfo a
fi0
let fi1 :: FInfo a
fi1 = FInfo a
reducedFi { 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
reducedFi }
let si0 :: SInfo a
si0 = FInfo a -> SInfo a
forall a. Fixpoint a => FInfo a -> SInfo a
convertFormat FInfo a
fi1
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
$ ( 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)
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 = 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 = 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 = 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
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 = 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 Config -> SInfo a -> SInfo a
forall a. Config -> SInfo a -> SInfo a
expand Config
cfg SInfo a
si5 else SInfo a
si5
if Config -> Bool
rewriteAxioms Config
cfg Bool -> Bool -> Bool
&& Config -> Bool
noLazyPLE Config
cfg
then Config -> SInfo a -> Maybe [Integer] -> IO (SInfo a)
forall a.
Loc a =>
Config -> SInfo a -> Maybe [Integer] -> IO (SInfo a)
instantiate Config
cfg SInfo a
si6 (Maybe [Integer] -> IO (SInfo a))
-> Maybe [Integer] -> IO (SInfo a)
forall a b. NFData a => (a -> b) -> a -> b
$!! Maybe [Integer]
forall a. Maybe a
Nothing
else SInfo a -> IO (SInfo a)
forall (m :: * -> *) a. Monad m => a -> m a
return SInfo a
si6
reduceFInfo :: Fixpoint a => Config -> FInfo a -> IO (FInfo a)
reduceFInfo :: Config -> FInfo a -> IO (FInfo a)
reduceFInfo Config
cfg FInfo a
fi = do
let simplifiedFi :: FInfo a
simplifiedFi = Config -> FInfo a -> FInfo a
forall a. Config -> FInfo a -> FInfo a
simplifyBindings Config
cfg FInfo a
fi
reducedFi :: FInfo a
reducedFi = FInfo a -> FInfo a
forall a. FInfo a -> FInfo a
reduceEnvironments FInfo a
simplifiedFi
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. Fixpoint a => Config -> FInfo a -> IO ()
savePrettifiedQuery Config
cfg FInfo a
reducedFi
if Config -> Bool
noEnvironmentReduction Config
cfg then
FInfo a -> IO (FInfo a)
forall (m :: * -> *) a. Monad m => a -> m a
return FInfo a
fi
else
FInfo a -> IO (FInfo a)
forall (m :: * -> *) a. Monad m => a -> m a
return FInfo a
reducedFi
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 <- 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
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 -> Result (Integer, a) -> IO ()
forall a. Config -> Result a -> IO ()
saveSolution Config
cfg Result (Integer, a)
res
Result (Integer, a) -> IO (Result (Integer, a))
forall (m :: * -> *) a. Monad m => a -> m a
return Result (Integer, a)
res
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] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
[ String
""
, String
"Solution:"
, 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
"", String
"", GFixSolution -> String
forall a. PPrint a => a -> String
showpp (Result a -> GFixSolution
forall a. Result a -> GFixSolution
gresSolution Result a
res)]
else []
) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[ String
""
, String
""
, String
"Non-cut kvars:"
, String
""
, FixSolution -> String
forall a. PPrint a => a -> String
showpp ((Expr -> Expr) -> FixSolution -> FixSolution
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map Expr -> Expr
unElab (FixSolution -> FixSolution) -> FixSolution -> FixSolution
forall a b. (a -> b) -> a -> b
$ Result a -> FixSolution
forall a. Result a -> FixSolution
resNonCutsSolution Result a
res)
]