-- | 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 DoAndIfThenElse     #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE ScopedTypeVariables #-}

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

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                 (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 hiding (GInfo(..), fi)
import qualified Language.Fixpoint.Types as Types (GInfo(..))
import           Language.Fixpoint.Minimize (minQuery, minQuals, minKvars)
import           Language.Fixpoint.Solver.Instantiate (instantiate)
import           Control.DeepSeq
import qualified Data.ByteString as B
import Data.Maybe (catMaybes)

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

---------------------------------------------------------------------------
resultExitCode :: (Fixpoint a, NFData a, ToJSON a) => Config -> Result a
               -> IO ExitCode
---------------------------------------------------------------------------
resultExitCode :: forall a.
(Fixpoint a, NFData a, ToJSON a) =>
Config -> Result a -> IO ExitCode
resultExitCode Config
cfg Result a
r = do
  IO () -> IO ()
whenNormal forall a b. (a -> b) -> a -> b
$ Moods -> [Char] -> IO ()
colorStrLn (forall a. FixResult a -> Moods
colorResult FixResult a
stat) (FixResult a -> [Char]
statStr forall a b. NFData a => (a -> b) -> a -> b
$!! FixResult a
stat)
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
json Config
cfg) forall a b. (a -> b) -> a -> b
$ Text -> IO ()
LT.putStrLn Text
jStr
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall {a}. Result a -> ExitCode
eCode Result a
r)
  where
    jStr :: Text
jStr    = ByteString -> Text
LT.decodeUtf8 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ToJSON a => a -> ByteString
encode forall a b. (a -> b) -> a -> b
$ Result a
r
    stat :: FixResult a
stat    = forall a. Result a -> FixResult a
resStatus forall a b. NFData a => (a -> b) -> a -> b
$!! Result a
r
    eCode :: Result a -> ExitCode
eCode   = forall a. FixResult a -> ExitCode
resultExit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Result a -> FixResult a
resStatus
    statStr :: FixResult a -> [Char]
statStr = Doc -> [Char]
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Fixpoint a => FixResult a -> Doc
resultDoc

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


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

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

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

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

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

readBinFq :: FilePath -> IO (FInfo ())
readBinFq :: [Char] -> IO (FInfo ())
readBinFq [Char]
file = {-# SCC "parseBFq" #-} do
  ByteString
bs <- [Char] -> IO ByteString
B.readFile [Char]
file
  case forall a. Store a => ByteString -> Either PeekException a
S.decode ByteString
bs of
    Right FInfo ()
fi -> forall (m :: * -> *) a. Monad m => a -> m a
return FInfo ()
fi
    Left PeekException
err' -> forall a. HasCallStack => [Char] -> a
error ([Char]
"Error decoding .bfq: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show PeekException
err')

--------------------------------------------------------------------------------
-- | Solve in parallel after partitioning an FInfo to indepdendant parts
--------------------------------------------------------------------------------
solveSeqWith :: (Fixpoint a) => Solver a -> Solver a
solveSeqWith :: forall a. Fixpoint a => 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               = 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 :: forall a. Fixpoint a => Solver a -> Solver a
solveParWith Solver a
s Config
c FInfo a
fi0 = do
  -- putStrLn "Using Parallel Solver \n"
  let fi :: FInfo a
fi    = 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   = forall (c :: * -> *) a.
TaggedC c a =>
Maybe MCInfo -> GInfo c a -> [GInfo c a]
partition' (forall a. a -> Maybe a
Just MCInfo
mci) FInfo a
fi
  [Char] -> IO ()
writeLoud forall a b. (a -> b) -> a -> b
$ [Char]
"Number of partitions : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [FInfo a]
fis)
  [Char] -> IO ()
writeLoud forall a b. (a -> b) -> a -> b
$ [Char]
"number of cores      : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Config -> Maybe Int
cores Config
c)
  [Char] -> IO ()
writeLoud forall a b. (a -> b) -> a -> b
$ [Char]
"minimum part size    : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Config -> Int
minPartSize Config
c)
  [Char] -> IO ()
writeLoud forall a b. (a -> b) -> a -> b
$ [Char]
"maximum part size    : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Config -> Int
maxPartSize Config
c)
  case [FInfo a]
fis of
    []        -> forall a. HasCallStack => [Char] -> a
errorstar [Char]
"partiton' returned empty list!"
    [FInfo a
onePart] -> Solver a
s Config
c FInfo a
onePart
    [FInfo a]
_         -> forall a b. (a -> IO (Result b)) -> [a] -> IO (Result b)
inParallelUsing (forall {t} {t}. (Config -> t -> t) -> Config -> (Int, t) -> t
f Solver a
s Config
c) forall a b. (a -> b) -> a -> b
$ 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 :: [Char]
srcFile = Ext -> Config -> [Char]
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 :: forall a b. (a -> IO (Result b)) -> [a] -> IO (Result b)
inParallelUsing a -> IO (Result b)
f [a]
xs = do
   Int -> IO ()
setNumCapabilities (forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs)
   [Result b]
rs <- forall a b. (a -> IO b) -> [a] -> IO [b]
asyncMapM a -> IO (Result b)
f [a]
xs
   forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => [a] -> a
mconcat [Result b]
rs


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

crashResult :: (PPrint a) => ErrorMap a -> Error -> Result (Integer, a)
crashResult :: forall a. PPrint a => ErrorMap a -> Error -> Result (Integer, a)
crashResult ErrorMap a
m Error
e = forall a.
FixResult a
-> FixSolution -> FixSolution -> GFixSolution -> Result a
Result FixResult (Integer, a)
res forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
  where
    res :: FixResult (Integer, a)
res           = forall a. [(a, Maybe [Char])] -> [Char] -> FixResult a
Crash [((Integer, a), Maybe [Char])]
es [Char]
msg
    es :: [((Integer, a), Maybe [Char])]
es            = forall a. [Maybe a] -> [a]
catMaybes [ forall a.
ErrorMap a -> Error1 -> Maybe ((Integer, a), Maybe [Char])
findError ErrorMap a
m Error1
e | Error1
e <- Error -> [Error1]
errs Error
e ]
    msg :: [Char]
msg | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((Integer, a), Maybe [Char])]
es = forall a. PPrint a => a -> [Char]
showpp Error
e
        | Bool
otherwise = [Char]
"Sorry, unexpected panic in liquid-fixpoint!" -- ++ showpp e

-- | Unpleasant hack to save meta-data that can be recovered from SrcSpan
type ErrorMap a = HashMap.HashMap SrcSpan a

findError :: ErrorMap a -> Error1 -> Maybe ((Integer, a), Maybe String)
findError :: forall a.
ErrorMap a -> Error1 -> Maybe ((Integer, a), Maybe [Char])
findError ErrorMap a
m Error1
e = do
  a
ann <- forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup (Error1 -> SrcSpan
errLoc Error1
e) ErrorMap a
m
  let str :: [Char]
str = Doc -> [Char]
render (Error1 -> Doc
errMsg Error1
e)
  forall (m :: * -> *) a. Monad m => a -> m a
return ((-Integer
1, a
ann), forall a. a -> Maybe a
Just [Char]
str)

-- The order is important here: we want the "binders" to get the "precedence"
errorMap :: (Loc a) => FInfo a -> ErrorMap a
errorMap :: forall a. Loc a => FInfo a -> ErrorMap a
errorMap FInfo a
fi = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList [ (forall a. Loc a => a -> SrcSpan
srcSpan a
a, a
a) | a
a <- [a]
anns ]
  where
    anns :: [a]
anns    =  [ forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SubC a
c | (Integer
_, SubC a
c) <- forall k v. HashMap k v -> [(k, v)]
HashMap.toList (forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
Types.cm FInfo a
fi) ]
            forall a. [a] -> [a] -> [a]
++ [ forall a. WfC a -> a
winfo WfC a
w | (KVar
_, WfC a
w) <- forall k v. HashMap k v -> [(k, v)]
HashMap.toList (forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
Types.ws FInfo a
fi) ]
            forall a. [a] -> [a] -> [a]
++ [ a
a | (Int
_, (Symbol
_,SortedReft
_, a
a)) <- forall a. BindEnv a -> [(Int, (Symbol, SortedReft, a))]
bindEnvToList (forall (c :: * -> *) a. GInfo c a -> BindEnv a
Types.bs FInfo a
fi) ]

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

{-# SCC simplifyFInfo #-}
simplifyFInfo :: (NFData a, Fixpoint a, Show a, Loc a)
               => Config -> FInfo a -> IO (SInfo a)
simplifyFInfo :: forall a.
(NFData a, Fixpoint a, Show a, Loc a) =>
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)
  FInfo a
reducedFi <- 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]
Types.quals = Qualifier -> Qualifier
remakeQual forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (c :: * -> *) a. GInfo c a -> [Qualifier]
Types.quals FInfo a
reducedFi }
  let si0 :: SInfo a
si0   = {- SCC "convertFormat" -} 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   = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. Error -> a
die forall a. a -> a
id ({- SCC "sanitize" -} forall a. Config -> SInfo a -> SanitizeM (SInfo a)
sanitize Config
cfg 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"
  forall (c :: * -> *) a. TaggedC c a => Config -> GInfo c a -> IO ()
graphStatistics Config
cfg SInfo a
si1
  let si2 :: SInfo a
si2  = {- SCC "wfcUniqify" -} forall a. SInfo a -> SInfo a
wfcUniqify forall a b. NFData a => (a -> b) -> a -> b
$!! SInfo a
si1
  let si3 :: SInfo a
si3  = {- SCC "renameAll"  -} forall a. NFData a => SInfo a -> SInfo a
renameAll  forall a b. NFData a => (a -> b) -> a -> b
$!! SInfo a
si2
  forall a. NFData a => a -> ()
rnf SInfo a
si3 seq :: forall a b. a -> b -> b
`seq` IO () -> IO ()
whenLoud forall a b. (a -> b) -> a -> b
$ Moods -> [Char] -> IO ()
donePhase Moods
Loud [Char]
"Uniqify & Rename"
  forall a. Fixpoint a => Int -> Config -> SInfo a -> IO ()
loudDump Int
1 Config
cfg SInfo a
si3
  let si4 :: SInfo a
si4  = {- SCC "defunction" -} forall a. Fixpoint a => Config -> SInfo a -> SInfo a
defunctionalize Config
cfg forall a b. NFData a => (a -> b) -> a -> b
$!! SInfo a
si3
  -- putStrLn $ "AXIOMS: " ++ showpp (asserts si4)
  forall a. Fixpoint a => Int -> Config -> SInfo a -> IO ()
loudDump Int
2 Config
cfg SInfo a
si4
  let si5 :: SInfo a
si5  = {- SCC "elaborate" -} forall a. Elaborate a => Located [Char] -> SymEnv -> a -> a
elaborate (forall l b. Loc l => l -> b -> Located b
atLoc SrcSpan
dummySpan [Char]
"solver") (forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
si4) SInfo a
si4
  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" -} 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 forall a.
Loc a =>
Config -> SInfo a -> Maybe [Integer] -> IO (SInfo a)
instantiate Config
cfg SInfo a
si6 forall a b. NFData a => (a -> b) -> a -> b
$!! forall a. Maybe a
Nothing
    else forall (m :: * -> *) a. Monad m => a -> m a
return SInfo a
si6

reduceFInfo :: Fixpoint a => Config -> FInfo a -> IO (FInfo a)
reduceFInfo :: forall a. Fixpoint a => Config -> FInfo a -> IO (FInfo a)
reduceFInfo Config
cfg FInfo a
fi = do
  let simplifiedFi :: FInfo a
simplifiedFi = {- SCC "simplifyFInfo" -} forall a. Config -> FInfo a -> FInfo a
simplifyBindings Config
cfg FInfo a
fi
      reducedFi :: FInfo a
reducedFi = {- SCC "reduceEnvironments" -} forall a. FInfo a -> FInfo a
reduceEnvironments FInfo a
simplifiedFi
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
save Config
cfg) forall a b. (a -> b) -> a -> b
$
    forall a. Fixpoint a => Config -> FInfo a -> IO ()
savePrettifiedQuery Config
cfg FInfo a
reducedFi
  if Config -> Bool
noEnvironmentReduction Config
cfg then
    forall (m :: * -> *) a. Monad m => a -> m a
return FInfo a
fi
  else
    forall (m :: * -> *) a. Monad m => a -> m a
return FInfo a
reducedFi

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

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

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

saveSolution :: Config -> Result a -> IO ()
saveSolution :: forall a. Config -> Result a -> IO ()
saveSolution Config
cfg Result a
res = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Config -> Bool
save Config
cfg) forall a b. (a -> b) -> a -> b
$ do
  let f :: [Char]
f = Ext -> Config -> [Char]
queryFile Ext
Out Config
cfg
  [Char] -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ [Char]
"Saving Solution: " forall a. [a] -> [a] -> [a]
++ [Char]
f forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
  [Char] -> IO ()
ensurePath [Char]
f
  [Char] -> [Char] -> IO ()
writeFile [Char]
f forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines forall a b. (a -> b) -> a -> b
$
    [ [Char]
""
    , [Char]
"Solution:"
    , forall a. PPrint a => a -> [Char]
showpp (forall a. Result a -> FixSolution
resSolution  Result a
res)
    ] forall a. [a] -> [a] -> [a]
++
    ( if Config -> Bool
gradual Config
cfg then [[Char]
"", [Char]
"", forall a. PPrint a => a -> [Char]
showpp (forall a. Result a -> GFixSolution
gresSolution Result a
res)]
      else []
    ) forall a. [a] -> [a] -> [a]
++
    [ [Char]
""
    , [Char]
""
    , [Char]
"Non-cut kvars:"
    , [Char]
""
    , forall a. PPrint a => a -> [Char]
showpp (forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map Expr -> Expr
unElab forall a b. (a -> b) -> a -> b
$ forall a. Result a -> FixSolution
resNonCutsSolution Result a
res)
    ]