-- | 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 #-}

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.List as L
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                      (mplus, 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            (ElabParam (..), 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, mapMaybe)

---------------------------------------------------------------------------
-- | 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'     = Config -> FInfo () -> FInfo ()
forall a. Config -> FInfo a -> FInfo a
ignoreQualifiers Config
cfg' FInfo ()
fi
    Result (Integer, ())
r          <- Solver ()
forall a.
(PPrint 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 :: [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 (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Moods -> [Char] -> IO ()
colorStrLn (FixResult a -> Moods
forall a. FixResult a -> Moods
colorResult FixResult a
stat) (FixResult a -> [Char]
statStr (FixResult a -> [Char]) -> FixResult a -> [Char]
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 a. a -> IO a
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 -> [Char]
statStr = Doc -> [Char]
render (Doc -> [Char]) -> (FixResult a -> Doc) -> FixResult a -> [Char]
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 :: forall a. 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 { 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      = Config -> GInfo SubC a -> IO (Result (Integer, a))
forall a (c :: * -> *).
(Fixpoint a, Fixpoint (c a), TaggedC c a) =>
Config -> GInfo c a -> IO (Result (Integer, a))
partition  Config
cfg        (GInfo SubC a -> IO (Result (Integer, a)))
-> GInfo SubC a -> IO (Result (Integer, a))
forall a b. NFData a => (a -> b) -> a -> b
$!! GInfo SubC a
q
  | Config -> Bool
stats Config
cfg      = Config -> GInfo SubC a -> IO (Result (Integer, a))
forall a. Config -> FInfo a -> IO (Result (Integer, a))
statistics Config
cfg        (GInfo SubC a -> IO (Result (Integer, a)))
-> GInfo SubC a -> IO (Result (Integer, a))
forall a b. NFData a => (a -> b) -> a -> b
$!! GInfo SubC a
q
  | Config -> Bool
minimize Config
cfg   = Config
-> (Config -> GInfo SubC a -> IO (Result (Integer, a)))
-> GInfo SubC a
-> IO (Result (Integer, a))
forall a.
(NFData a, Fixpoint a) =>
Config -> Solver a -> FInfo a -> IO (Result (Integer, a))
minQuery   Config
cfg Config -> GInfo SubC a -> IO (Result (Integer, a))
forall a.
(PPrint a, NFData a, Fixpoint a, Show a, Loc a) =>
Solver a
solve' (GInfo SubC a -> IO (Result (Integer, a)))
-> GInfo SubC a -> IO (Result (Integer, a))
forall a b. NFData a => (a -> b) -> a -> b
$!! GInfo SubC a
q
  | Config -> Bool
minimizeQs Config
cfg = Config
-> (Config -> GInfo SubC a -> IO (Result (Integer, a)))
-> GInfo SubC a
-> IO (Result (Integer, a))
forall a.
(NFData a, Fixpoint a) =>
Config -> Solver a -> FInfo a -> IO (Result (Integer, a))
minQuals Config
cfg Config -> GInfo SubC a -> IO (Result (Integer, a))
forall a.
(PPrint a, NFData a, Fixpoint a, Show a, Loc a) =>
Solver a
solve'   (GInfo SubC a -> IO (Result (Integer, a)))
-> GInfo SubC a -> IO (Result (Integer, a))
forall a b. NFData a => (a -> b) -> a -> b
$!! GInfo SubC a
q
  | Config -> Bool
minimizeKs Config
cfg = Config
-> (Config -> GInfo SubC a -> IO (Result (Integer, a)))
-> GInfo SubC a
-> IO (Result (Integer, a))
forall a.
(NFData a, Fixpoint a) =>
Config -> Solver a -> FInfo a -> IO (Result (Integer, a))
minKvars Config
cfg Config -> GInfo SubC a -> IO (Result (Integer, a))
forall a.
(PPrint a, NFData a, Fixpoint a, Show a, Loc a) =>
Solver a
solve'   (GInfo SubC a -> IO (Result (Integer, a)))
-> GInfo SubC a -> IO (Result (Integer, a))
forall a b. NFData a => (a -> b) -> a -> b
$!! GInfo SubC a
q
  | Bool
otherwise      = Config -> GInfo SubC a -> IO (Result (Integer, a))
forall a.
(PPrint a, NFData a, Fixpoint a, Show a, Loc a) =>
Solver a
solve'     Config
cfg        (GInfo SubC a -> IO (Result (Integer, a)))
-> GInfo SubC a -> IO (Result (Integer, a))
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
  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, 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 = 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 :: [Char] -> IO (FInfo (), [[Char]])
readFInfo [Char]
f
  | [Char] -> Bool
isBinary [Char]
f = (,) (FInfo () -> [[Char]] -> (FInfo (), [[Char]]))
-> IO (FInfo ()) -> IO ([[Char]] -> (FInfo (), [[Char]]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> IO (FInfo ())
readBinFq [Char]
f IO ([[Char]] -> (FInfo (), [[Char]]))
-> IO [[Char]] -> IO (FInfo (), [[Char]])
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [[Char]] -> IO [[Char]]
forall a. a -> IO a
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" -} [Char] -> [Char] -> FInfoWithOpts ()
forall a. Inputable a => [Char] -> [Char] -> a
rr' [Char]
file [Char]
str :: FInfoWithOpts ()
  (FInfo (), [[Char]]) -> IO (FInfo (), [[Char]])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (FInfoWithOpts () -> FInfo ()
forall a. FInfoWithOpts a -> FInfo a
fioFI FInfoWithOpts ()
q, FInfoWithOpts () -> [[Char]]
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 ByteString -> Either PeekException (FInfo ())
forall a. Store a => ByteString -> Either PeekException a
S.decode ByteString
bs of
    Right FInfo ()
fi -> FInfo () -> IO (FInfo ())
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return FInfo ()
fi
    Left PeekException
err' -> [Char] -> IO (FInfo ())
forall a. HasCallStack => [Char] -> a
error ([Char]
"Error decoding .bfq: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ PeekException -> [Char]
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               = 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 :: 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    = 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
  [Char] -> IO ()
writeLoud ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Number of partitions : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show ([FInfo a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FInfo a]
fis)
  [Char] -> IO ()
writeLoud ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"number of cores      : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Maybe Int -> [Char]
forall a. Show a => a -> [Char]
show (Config -> Maybe Int
cores Config
c)
  [Char] -> IO ()
writeLoud ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"minimum part size    : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Config -> Int
minPartSize Config
c)
  [Char] -> IO ()
writeLoud ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"maximum part size    : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Config -> Int
maxPartSize Config
c)
  case [FInfo a]
fis of
    []        -> [Char] -> IO (Result (Integer, a))
forall a. HasCallStack => [Char] -> a
errorstar [Char]
"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 = queryFile (Part j) 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 ([a] -> Int
forall a. [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 a. a -> IO a
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, 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 = Solver a
forall a.
(NFData a, Fixpoint a, Show a, Loc a, PPrint 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 a. a -> IO 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
. ErrorMap a -> Error -> Result (Integer, a)
forall a. PPrint a => ErrorMap a -> Error -> Result (Integer, a)
crashResult (FInfo a -> ErrorMap a
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
err' = FixResult (Integer, a)
-> FixSolution
-> FixSolution
-> GFixSolution
-> Result (Integer, a)
forall a.
FixResult a
-> FixSolution -> FixSolution -> GFixSolution -> Result a
Result FixResult (Integer, a)
res FixSolution
forall a. Monoid a => a
mempty FixSolution
forall a. Monoid a => a
mempty GFixSolution
forall a. Monoid a => a
mempty
  where
    res :: FixResult (Integer, a)
res           = [((Integer, a), Maybe [Char])] -> [Char] -> FixResult (Integer, a)
forall a. [(a, Maybe [Char])] -> [Char] -> FixResult a
Crash [((Integer, a), Maybe [Char])]
es [Char]
msg
    es :: [((Integer, a), Maybe [Char])]
es            = [Maybe ((Integer, a), Maybe [Char])]
-> [((Integer, a), Maybe [Char])]
forall a. [Maybe a] -> [a]
catMaybes [ ErrorMap a -> Error1 -> Maybe ((Integer, a), Maybe [Char])
forall a.
ErrorMap a -> Error1 -> Maybe ((Integer, a), Maybe [Char])
findError ErrorMap a
m Error1
e | Error1
e <- [Error1]
ers ]
    ers :: [Error1]
ers           = Error -> [Error1]
errs Error
err'
    msg :: [Char]
msg | [Error1] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Error1]
ers = [Char]
"Sorry, unexpected panic in liquid-fixpoint!"
        --  {-dbgFalse-} True  = "Sorry, unexpected panic in liquid-fixpoint!\n" ++ crashMessage es
        | Bool
otherwise = Error -> [Char]
forall a. PPrint a => a -> [Char]
showpp Error
err'

_crashMessage :: [((Integer, a), Maybe String) ] -> String
_crashMessage :: forall a. [((Integer, a), Maybe [Char])] -> [Char]
_crashMessage [((Integer, a), Maybe [Char])]
es = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
L.intercalate [Char]
"\n" [ Integer -> [Char] -> [Char]
forall {a}. Show a => a -> [Char] -> [Char]
msg Integer
i [Char]
s | ((Integer
i,a
_), Just [Char]
s) <- [((Integer, a), Maybe [Char])]
es ]
  where
    msg :: a -> [Char] -> [Char]
msg a
i [Char]
s = [Char]
"Error in constraint " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
i [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
":\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s

-- | 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 <- SrcSpan -> ErrorMap a -> Maybe a
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)
  ((Integer, a), Maybe [Char]) -> Maybe ((Integer, a), Maybe [Char])
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((-Integer
1, a
ann), [Char] -> Maybe [Char]
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 = [(SrcSpan, a)] -> HashMap SrcSpan a
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HashMap.fromList [ (a -> SrcSpan
forall a. Loc a => a -> SrcSpan
srcSpan a
a, a
a) | a
a <- [a]
anns ]
  where
    anns :: [a]
anns    =  [ SubC a -> a
forall (c :: * -> *) a. TaggedC c a => c a -> a
sinfo SubC a
c | (Integer
_, SubC a
c) <- HashMap Integer (SubC a) -> [(Integer, SubC a)]
forall k v. HashMap k v -> [(k, v)]
HashMap.toList (FInfo a -> HashMap Integer (SubC a)
forall (c :: * -> *) a. GInfo c a -> HashMap Integer (c a)
Types.cm FInfo a
fi) ]
            [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [ WfC a -> a
forall a. WfC a -> a
winfo WfC a
w | (KVar
_, WfC a
w) <- HashMap KVar (WfC a) -> [(KVar, WfC a)]
forall k v. HashMap k v -> [(k, v)]
HashMap.toList (FInfo a -> HashMap KVar (WfC a)
forall (c :: * -> *) a. GInfo c a -> HashMap KVar (WfC a)
Types.ws FInfo a
fi) ]
            [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [ a
a | (Int
_, (Symbol
_,SortedReft
_, a
a)) <- BindEnv a -> [(Int, (Symbol, SortedReft, a))]
forall a. BindEnv a -> [(Int, (Symbol, SortedReft, a))]
bindEnvToList (FInfo a -> BindEnv a
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 = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
False ([Char] -> IO ()
writeLoud ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Doc -> [Char]
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 :: [Char]
msg           = [Char]
"fq file after Uniqify & Rename " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i [Char] -> [Char] -> [Char]
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 <- 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 { Types.quals = remakeQual <$> Types.quals reducedFi }
  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 ({- SCC "sanitize" -} Config -> SInfo a -> Either Error (SInfo a)
forall a. Show 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
  -- writeLoud $ "fq file after wfcUniqify: \n" ++ render (toFixpoint cfg si2)
  let si3 :: SInfo a
si3  = {- SCC "renameAll"  -} SInfo a -> SInfo a
forall a. NFData 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 ()
forall a b. a -> b -> b
`seq` IO () -> IO ()
whenLoud (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Moods -> [Char] -> IO ()
donePhase Moods
Loud [Char]
"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
  -- writeLoud $ "fq file after defunc: \n" ++ render (toFixpoint cfg si4)
  -- 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" -} ElabParam -> SInfo a -> SInfo a
forall a. Elaborate a => ElabParam -> a -> a
elaborate (ElabFlags -> Located [Char] -> SymEnv -> ElabParam
ElabParam (SMTSolver -> ElabFlags
solverFlags (SMTSolver -> ElabFlags) -> SMTSolver -> ElabFlags
forall a b. (a -> b) -> a -> b
$ Config -> SMTSolver
solver Config
cfg) (SrcSpan -> [Char] -> Located [Char]
forall l b. Loc l => l -> b -> Located b
atLoc SrcSpan
dummySpan [Char]
"solver") (Config -> SInfo a -> SymEnv
forall a. Config -> SInfo a -> SymEnv
symbolEnv Config
cfg SInfo a
si4)) SInfo a
si4
  -- writeLoud $ "fq file after elaborate: \n" ++ render (toFixpoint cfg si5)
  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
  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 a. a -> IO a
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" -} Config -> FInfo a -> FInfo a
forall a. Config -> FInfo a -> FInfo a
simplifyBindings Config
cfg FInfo a
fi
      reducedFi :: FInfo a
reducedFi = {- SCC "reduceEnvironments" -} 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 a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return FInfo a
fi
  else
    FInfo a -> IO (FInfo a)
forall a. a -> IO a
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 <- 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)
res0 <- {- 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
  let res :: Result (Integer, a)
res = Result (Integer, a) -> Result (Integer, a)
forall a. Result a -> Result a
simplifyResult Result (Integer, a)
res0
  -- rnf soln `seq` donePhase Loud "Solve2"
  --let stat = resStatus res
  -- saveSolution cfg 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
$ Config -> Result (Integer, a) -> IO ()
forall a. Config -> Result a -> IO ()
saveSolution Config
cfg Result (Integer, a)
res
  -- writeLoud $ "\nSolution:\n"  ++ showpp (resSolution res)
  -- colorStrLn (colorResult stat) (show stat)
  Result (Integer, a) -> IO (Result (Integer, a))
forall a. a -> IO a
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 = [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
<$> ([Char] -> IO (FInfo a)) -> [[Char]] -> IO [FInfo a]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM [Char] -> IO (FInfo a)
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 = [Char] -> [Char] -> FInfo ()
forall a. Inputable a => [Char] -> [Char] -> a
rr' [Char]
f [Char]
str :: FInfo ()
  GInfo SubC a -> IO (GInfo SubC a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (GInfo SubC a -> IO (GInfo SubC a))
-> GInfo SubC a -> IO (GInfo SubC a)
forall a b. (a -> b) -> a -> b
$ GInfo SubC a
forall a. Monoid a => a
mempty { Types.quals = Types.quals  fi
                  , Types.gLits = Types.gLits  fi
                  , Types.dLits = Types.dLits  fi }

saveSolution :: Config -> Result a -> IO ()
saveSolution :: forall a. 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 :: [Char]
f = Ext -> Config -> [Char]
queryFile Ext
Out Config
cfg
  [Char] -> IO ()
putStrLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Saving Solution: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
f [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
  [Char] -> IO ()
ensurePath [Char]
f
  [Char] -> [Char] -> IO ()
writeFile [Char]
f ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$
    [ [Char]
""
    , [Char]
"Solution:"
    , FixSolution -> [Char]
forall a. PPrint a => a -> [Char]
showpp (Result a -> FixSolution
forall a. Result a -> FixSolution
resSolution  Result a
res)
    ] [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++
    ( if Config -> Bool
gradual Config
cfg then
        [[Char]
"", [Char]
"", GFixSolution -> [Char]
forall a. PPrint a => a -> [Char]
showpp (GFixSolution -> [Char]) -> GFixSolution -> [Char]
forall a b. (a -> b) -> a -> b
$ Result a -> GFixSolution
forall a. Result a -> GFixSolution
gresSolution Result a
res]
      else
        []
    ) [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++
    [ [Char]
""
    , [Char]
""
    , [Char]
"Non-cut kvars:"
    , [Char]
""
    , FixSolution -> [Char]
forall a. PPrint a => a -> [Char]
showpp ((ExprV Symbol -> ExprV Symbol) -> FixSolution -> FixSolution
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map ExprV Symbol -> ExprV Symbol
unElab (FixSolution -> FixSolution) -> FixSolution -> FixSolution
forall a b. (a -> b) -> a -> b
$ Result a -> FixSolution
forall a. Result a -> FixSolution
resNonCutsSolution Result a
res)
    ]

simplifyResult :: Result a -> Result a
simplifyResult :: forall a. Result a -> Result a
simplifyResult Result a
res =
    Result a
res
      { resSolution = HashMap.map simplifyKVar (resSolution res)
      , resNonCutsSolution = HashMap.map simplifyKVar (resNonCutsSolution res)
      }

-- | Simplifies existential expressions with unused or inconsequential bindings.
--
-- For instance, in the following example, "x" is not used at all.
--
-- > simplifyKVar "exists x y. y == z && y == C" == "exists y. y == z && y == C"
--
-- And in the following example, @x@ is used but in a way that doesn't
-- contribute any useful knowledge.
--
-- > simplifyKVar "exists x y. x == C && y == z && y == C"
-- >   ==
-- > "exists y. y == z && y == C"
--
-- We require that relevant variables occur more than once, or that
-- they occur in some other place than as an argument to @==@.
--
simplifyKVar :: Expr -> Expr
simplifyKVar :: ExprV Symbol -> ExprV Symbol
simplifyKVar (POr [ExprV Symbol]
es) = [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
POr ([ExprV Symbol] -> ExprV Symbol) -> [ExprV Symbol] -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ (ExprV Symbol -> ExprV Symbol) -> [ExprV Symbol] -> [ExprV Symbol]
forall a b. (a -> b) -> [a] -> [b]
map ExprV Symbol -> ExprV Symbol
simplifyKVar [ExprV Symbol]
es
simplifyKVar (PExist [(Symbol, Sort)]
bs e :: ExprV Symbol
e@(PAnd [ExprV Symbol]
es)) =
    let fvs :: [[Symbol]]
fvs = [Symbol] -> [[Symbol]]
forall a. Eq a => [a] -> [[a]]
L.group ([Symbol] -> [[Symbol]]) -> [Symbol] -> [[Symbol]]
forall a b. (a -> b) -> a -> b
$ [Symbol] -> [Symbol]
forall a. Ord a => [a] -> [a]
L.sort ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ ExprV Symbol -> [Symbol]
collectFreeVarOccurrences ExprV Symbol
e
        esv :: [(Maybe Symbol, ExprV Symbol)]
esv = (ExprV Symbol -> (Maybe Symbol, ExprV Symbol))
-> [ExprV Symbol] -> [(Maybe Symbol, ExprV Symbol)]
forall a b. (a -> b) -> [a] -> [b]
map ([[Symbol]] -> ExprV Symbol -> (Maybe Symbol, ExprV Symbol)
isUniqueEq [[Symbol]]
fvs) [ExprV Symbol]
es
        removed :: [Symbol]
removed = ((Maybe Symbol, ExprV Symbol) -> Maybe Symbol)
-> [(Maybe Symbol, ExprV Symbol)] -> [Symbol]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Maybe Symbol, ExprV Symbol) -> Maybe Symbol
forall a b. (a, b) -> a
fst [(Maybe Symbol, ExprV Symbol)]
esv
        needed :: [Symbol]
needed = ([Symbol] -> Symbol) -> [[Symbol]] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map [Symbol] -> Symbol
forall a. HasCallStack => [a] -> a
head [[Symbol]]
fvs [Symbol] -> [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a] -> [a]
L.\\ [Symbol]
removed
        bs' :: [(Symbol, Sort)]
bs' = ((Symbol, Sort) -> Bool) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol]
needed) (Symbol -> Bool)
-> ((Symbol, Sort) -> Symbol) -> (Symbol, Sort) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, Sort) -> Symbol
forall a b. (a, b) -> a
fst) [(Symbol, Sort)]
bs
     in
        [(Symbol, Sort)] -> ExprV Symbol -> ExprV Symbol
forall v. [(Symbol, Sort)] -> ExprV v -> ExprV v
PExist [(Symbol, Sort)]
bs' (ExprV Symbol -> ExprV Symbol) -> ExprV Symbol -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ [ExprV Symbol] -> ExprV Symbol
forall v. [ExprV v] -> ExprV v
PAnd ([ExprV Symbol] -> ExprV Symbol) -> [ExprV Symbol] -> ExprV Symbol
forall a b. (a -> b) -> a -> b
$ [ExprV Symbol
ei | (Maybe Symbol
Nothing, ExprV Symbol
ei) <- [(Maybe Symbol, ExprV Symbol)]
esv]
  where
    -- | Determine if the expression is an equality that sets the value of
    -- a variable that doesn't occur elsewhere.
    --
    -- In @isUniqueEq fvs e@, @fvs@ contains the occurrences of the free
    -- variables, so we can infer if there is more than one occurrence
    -- of a given free variable, and @e@ is the equality to analyze.
    --
    -- Yields @(Just v, e)@ if @v@ doesn't occur elsewhere, and @e@ has
    -- the form @v == e'@.
    isUniqueEq :: [[Symbol]] -> Expr -> (Maybe Symbol, Expr)
    isUniqueEq :: [[Symbol]] -> ExprV Symbol -> (Maybe Symbol, ExprV Symbol)
isUniqueEq [[Symbol]]
fvs ExprV Symbol
er = case ExprV Symbol -> ExprV Symbol
unElab ExprV Symbol
er of
      PAtom Brel
brel ExprV Symbol
e0 ExprV Symbol
e1
        | Brel -> Bool
isEqRel Brel
brel ->
          let m :: Maybe Symbol
m = [[Symbol]] -> ExprV Symbol -> Maybe Symbol
forall {a} {t :: * -> *}.
(Eq a, IsString a, Foldable t) =>
t [a] -> ExprV a -> Maybe a
isVarToDrop [[Symbol]]
fvs ExprV Symbol
e0 Maybe Symbol -> Maybe Symbol -> Maybe Symbol
forall a. Maybe a -> Maybe a -> Maybe a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` [[Symbol]] -> ExprV Symbol -> Maybe Symbol
forall {a} {t :: * -> *}.
(Eq a, IsString a, Foldable t) =>
t [a] -> ExprV a -> Maybe a
isVarToDrop [[Symbol]]
fvs ExprV Symbol
e1
           in (Maybe Symbol
m, ExprV Symbol
er)
      ExprV Symbol
_ ->
        (Maybe Symbol
forall a. Maybe a
Nothing, ExprV Symbol
er)

    -- | Tells if the binary relation is an equality.
    isEqRel :: Brel -> Bool
isEqRel Brel
Eq = Bool
True
    isEqRel Brel
Ueq = Bool
True
    isEqRel Brel
_ = Bool
False

    -- | @isVarToDrop fvs s@ yields @Just s@ if the variable @s@ doesn't occur
    -- elsewhere according to @fvs@.
    --
    -- > isVarToDrop fvs (cast_as_int s) == isVarToDrop fvs s
    --
    isVarToDrop :: t [a] -> ExprV a -> Maybe a
isVarToDrop t [a]
fvs (EApp (EVar a
"cast_as_int") ExprV a
ei) = t [a] -> ExprV a -> Maybe a
isVarToDrop t [a]
fvs ExprV a
ei
    isVarToDrop t [a]
fvs (EVar a
s)
      | [a] -> t [a] -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem [a
s] t [a]
fvs = a -> Maybe a
forall a. a -> Maybe a
Just a
s
    isVarToDrop t [a]
_fvs ExprV a
_ = Maybe a
forall a. Maybe a
Nothing

simplifyKVar ExprV Symbol
e = ExprV Symbol
e

-- | Produces the free variables of an expressions as many times as they occur.
--
-- There are no guarantees on the order in which the variables are produced. For
-- instance,
--
-- > collectFreeVarOccurrences "z (y x) (y x)" == ["z", "y", "x", "y", "x"]
--
collectFreeVarOccurrences :: Expr -> [Symbol]
collectFreeVarOccurrences :: ExprV Symbol -> [Symbol]
collectFreeVarOccurrences = [Symbol] -> ExprV Symbol -> [Symbol]
go []
  where
    go :: [Symbol] -> ExprV Symbol -> [Symbol]
go [Symbol]
acc ExprV Symbol
e0 = case ExprV Symbol
e0 of
      ESym SymConst
_ -> [Symbol]
acc
      ECon Constant
_ -> [Symbol]
acc
      EVar Symbol
v -> Symbol
v Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
acc
      PKVar KVar
_ (Su HashMap Symbol (ExprV Symbol)
m) -> (ExprV Symbol -> [Symbol] -> [Symbol])
-> [Symbol] -> [ExprV Symbol] -> [Symbol]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (([Symbol] -> ExprV Symbol -> [Symbol])
-> ExprV Symbol -> [Symbol] -> [Symbol]
forall a b c. (a -> b -> c) -> b -> a -> c
flip [Symbol] -> ExprV Symbol -> [Symbol]
go) [Symbol]
acc ([ExprV Symbol] -> [Symbol]) -> [ExprV Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ HashMap Symbol (ExprV Symbol) -> [ExprV Symbol]
forall k v. HashMap k v -> [v]
HashMap.elems HashMap Symbol (ExprV Symbol)
m
      PGrad KVar
_ (Su HashMap Symbol (ExprV Symbol)
m) GradInfo
_ ExprV Symbol
e -> (ExprV Symbol -> [Symbol] -> [Symbol])
-> [Symbol] -> [ExprV Symbol] -> [Symbol]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (([Symbol] -> ExprV Symbol -> [Symbol])
-> ExprV Symbol -> [Symbol] -> [Symbol]
forall a b c. (a -> b -> c) -> b -> a -> c
flip [Symbol] -> ExprV Symbol -> [Symbol]
go) [Symbol]
acc ([ExprV Symbol] -> [Symbol]) -> [ExprV Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ ExprV Symbol
e ExprV Symbol -> [ExprV Symbol] -> [ExprV Symbol]
forall a. a -> [a] -> [a]
: HashMap Symbol (ExprV Symbol) -> [ExprV Symbol]
forall k v. HashMap k v -> [v]
HashMap.elems HashMap Symbol (ExprV Symbol)
m
      ENeg ExprV Symbol
e -> [Symbol] -> ExprV Symbol -> [Symbol]
go [Symbol]
acc ExprV Symbol
e
      PNot ExprV Symbol
p -> [Symbol] -> ExprV Symbol -> [Symbol]
go [Symbol]
acc ExprV Symbol
p
      ECst ExprV Symbol
e Sort
_t -> [Symbol] -> ExprV Symbol -> [Symbol]
go [Symbol]
acc ExprV Symbol
e
      PAll [(Symbol, Sort)]
_xts ExprV Symbol
p -> [Symbol] -> ExprV Symbol -> [Symbol]
go [Symbol]
acc ExprV Symbol
p
      ELam (Symbol
b, Sort
_) ExprV Symbol
e -> [Symbol] -> ExprV Symbol -> [Symbol]
go [Symbol]
acc ExprV Symbol
e [Symbol] -> [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a] -> [a]
L.\\ [Symbol
b]
      ECoerc Sort
_a Sort
_t ExprV Symbol
e -> [Symbol] -> ExprV Symbol -> [Symbol]
go [Symbol]
acc ExprV Symbol
e
      PExist [(Symbol, Sort)]
_xts ExprV Symbol
p -> [Symbol] -> ExprV Symbol -> [Symbol]
go [Symbol]
acc ExprV Symbol
p
      ETApp ExprV Symbol
e Sort
_s -> [Symbol] -> ExprV Symbol -> [Symbol]
go [Symbol]
acc ExprV Symbol
e
      ETAbs ExprV Symbol
e Symbol
_s -> [Symbol] -> ExprV Symbol -> [Symbol]
go [Symbol]
acc ExprV Symbol
e
      EApp ExprV Symbol
g ExprV Symbol
e -> [Symbol] -> ExprV Symbol -> [Symbol]
go ([Symbol] -> ExprV Symbol -> [Symbol]
go [Symbol]
acc ExprV Symbol
e) ExprV Symbol
g
      EBin Bop
_o ExprV Symbol
e1 ExprV Symbol
e2 -> [Symbol] -> ExprV Symbol -> [Symbol]
go ([Symbol] -> ExprV Symbol -> [Symbol]
go [Symbol]
acc ExprV Symbol
e2) ExprV Symbol
e1
      PImp ExprV Symbol
p1 ExprV Symbol
p2 -> [Symbol] -> ExprV Symbol -> [Symbol]
go ([Symbol] -> ExprV Symbol -> [Symbol]
go [Symbol]
acc ExprV Symbol
p2) ExprV Symbol
p1
      PIff ExprV Symbol
p1 ExprV Symbol
p2 -> [Symbol] -> ExprV Symbol -> [Symbol]
go ([Symbol] -> ExprV Symbol -> [Symbol]
go [Symbol]
acc ExprV Symbol
p2) ExprV Symbol
p1
      PAtom Brel
_r ExprV Symbol
e1 ExprV Symbol
e2 -> [Symbol] -> ExprV Symbol -> [Symbol]
go ([Symbol] -> ExprV Symbol -> [Symbol]
go [Symbol]
acc ExprV Symbol
e2) ExprV Symbol
e1
      EIte ExprV Symbol
p ExprV Symbol
e1 ExprV Symbol
e2 -> [Symbol] -> ExprV Symbol -> [Symbol]
go ([Symbol] -> ExprV Symbol -> [Symbol]
go ([Symbol] -> ExprV Symbol -> [Symbol]
go [Symbol]
acc ExprV Symbol
e2) ExprV Symbol
e1) ExprV Symbol
p
      PAnd [ExprV Symbol]
ps -> (ExprV Symbol -> [Symbol] -> [Symbol])
-> [Symbol] -> [ExprV Symbol] -> [Symbol]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (([Symbol] -> ExprV Symbol -> [Symbol])
-> ExprV Symbol -> [Symbol] -> [Symbol]
forall a b c. (a -> b -> c) -> b -> a -> c
flip [Symbol] -> ExprV Symbol -> [Symbol]
go) [Symbol]
acc [ExprV Symbol]
ps
      POr [ExprV Symbol]
ps -> (ExprV Symbol -> [Symbol] -> [Symbol])
-> [Symbol] -> [ExprV Symbol] -> [Symbol]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (([Symbol] -> ExprV Symbol -> [Symbol])
-> ExprV Symbol -> [Symbol] -> [Symbol]
forall a b c. (a -> b -> c) -> b -> a -> c
flip [Symbol] -> ExprV Symbol -> [Symbol]
go) [Symbol]
acc [ExprV Symbol]
ps