-- {-# OPTIONS_GHC -Wunused-imports #-}

-- | Setup up the emacs mode for Agda.

module Agda.Setup.EmacsMode
  ( help
  -- * Locate
  , locateFlag
  , printEmacsModeFile
  -- * Setup
  , setupFlag
  , setupDotEmacs
  -- * Compile
  , compileFlag
  , compileElispFiles
  -- * Utilities
  , inform
  )
where

import Control.Applicative    ( liftA2 )
import Control.Exception as E ( bracket, catch, evaluate, IOException )
import Control.Monad          ( unless )

import Data.Bifunctor         ( first, second )
import Data.Bool              ( bool )
import Data.Char              ( isAscii, isPrint )
import Data.Functor           ( (<&>) )
import Data.List              ( isInfixOf )
import Data.Maybe             ( catMaybes, fromMaybe )

import Numeric                ( showHex )

import System.Directory       ( doesFileExist, findExecutable, getTemporaryDirectory, removeFile )
import System.Exit            ( exitFailure, ExitCode(ExitSuccess) )
import System.FilePath        ( (</>), getSearchPath )
import System.IO              ( IOMode(ReadMode)
                              , hClose, hSetEncoding, hGetContents, hPutStr, hPutStrLn
                              , openTempFile, stderr, stdout, utf8, withFile
                              )
import System.Process         ( rawSystem, showCommandForUser )

import Agda.Setup             ( getDataDir )
import Agda.Setup.DataFiles   ( emacsLispFiles, emacsModeDir )

-- Command line options.

setupFlag :: String
setupFlag :: [Char]
setupFlag   = [Char]
"setup"

locateFlag :: String
locateFlag :: [Char]
locateFlag  = [Char]
"locate"

compileFlag :: String
compileFlag :: [Char]
compileFlag = [Char]
"compile"

-- | Help topic for @--emacs-mode@.

help :: String
help :: [Char]
help = [[Char]] -> [Char]
unlines
  [ [Char]
"Option --emacs-mode allows to administer the Agda Emacs mode."
  , [Char]
"It accepts three commands:"
  , [Char]
""
  , [Char]
setupFlag
  , [Char]
""
  , [Char]
"  This command unpacks Agda's data files, including the Emacs mode,"
  , [Char]
"  into Agda's data directory (see option --print-agda-data-dir)."
  , [Char]
""
  , [Char]
"  It then tries to add setup code for Agda's Emacs mode to the"
  , [Char]
"  current user's .emacs file. It is assumed that the .emacs file"
  , [Char]
"  uses the character encoding specified by the locale."
  , [Char]
""
  , [Char]
compileFlag
  , [Char]
""
  , [Char]
"  This command unpacks Agda's data files, including the Emacs mode,"
  , [Char]
"  into Agda's data directory."
  , [Char]
""
  , [Char]
"  It then tries to compile Agda's Emacs mode's source files."
  , [Char]
""
  , [Char]
"  WARNING: If you reinstall the Agda mode without recompiling the Emacs"
  , [Char]
"  Lisp files, then Emacs may continue using the old, compiled files."
  , [Char]
""
  , [Char]
locateFlag
  , [Char]
""
  , [Char]
"  The path to the Emacs mode's main file is printed on standard"
  , [Char]
"  output (using the UTF-8 character encoding and no trailing"
  , [Char]
"  newline)."
  ]

------------------------------------------------------------------------
-- Locating the Agda mode

-- | Prints out the path to the Agda mode's main file (using UTF-8 and
-- without any trailing newline).

printEmacsModeFile :: IO ()
printEmacsModeFile :: IO ()
printEmacsModeFile = do
  [Char]
dataDir <- IO [Char]
getDataDir
  let path :: [Char]
path = [Char]
dataDir [Char] -> [Char] -> [Char]
</> [Char]
emacsModeDir [Char] -> [Char] -> [Char]
</> [Char]
"agda2.el"
  Handle -> TextEncoding -> IO ()
hSetEncoding Handle
stdout TextEncoding
utf8
  [Char] -> IO ()
putStr [Char]
path

------------------------------------------------------------------------
-- Setting up the .emacs file

-- | Tries to set up the Agda mode in the given .emacs file.

setupDotEmacs :: String -> IO ()
setupDotEmacs :: [Char] -> IO ()
setupDotEmacs [Char]
agda = do
  let cmd :: [Char]
cmd   = [Char]
agda [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" --emacs-mode"
  let elisp :: [Char]
elisp = [Char] -> [Char]
setupString [Char]
cmd

  [Char]
dotEmacs <- IO [Char]
findDotEmacs
  [Char] -> IO ()
informLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"The .emacs file used: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
dotEmacs

  [Char] -> [Char] -> IO Bool
alreadyInstalled [Char]
cmd [Char]
dotEmacs IO Bool -> (Bool -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Bool
True  -> do
      [Char] -> IO ()
informLn [Char]
"It seems as if setup has already been performed."
    Bool
False -> do
      [Char] -> [Char] -> IO ()
appendFile [Char]
dotEmacs [Char]
elisp
      [Char] -> IO ()
inform ([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]
"Setup done. Try to (re)start Emacs and open an Agda file."
        , [Char]
"The following text was appended to the .emacs file:"
        ] [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]]
lines [Char]
elisp

-- | Tries to find the user's .emacs file by querying Emacs.

findDotEmacs :: IO FilePath
findDotEmacs :: IO [Char]
findDotEmacs = [Char] -> IO [Char]
askEmacs [Char]
"(expand-file-name user-init-file)"

-- | Has the Agda mode already been set up?

alreadyInstalled :: String -> FilePath -> IO Bool
alreadyInstalled :: [Char] -> [Char] -> IO Bool
alreadyInstalled [Char]
cmd [Char]
dotEmacs = do
  [Char] -> IO Bool
doesFileExist [Char]
dotEmacs IO Bool -> (Bool -> IO Bool) -> IO Bool
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Bool
False -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Bool
True  -> [Char] -> IOMode -> (Handle -> IO Bool) -> IO Bool
forall r. [Char] -> IOMode -> (Handle -> IO r) -> IO r
withFile [Char]
dotEmacs IOMode
ReadMode \ Handle
f -> do
      [Char]
txt <- Handle -> IO [Char]
hGetContents Handle
f
      Bool -> IO Bool
forall a. a -> IO a
evaluate (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
identifier [Char]
cmd [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` [Char]
txt
        -- Uses evaluate to ensure that the file is not closed prematurely.

-- | If this string occurs in the .emacs file, then it is assumed that
-- setup has already been performed.

identifier :: String -> String
identifier :: [Char] -> [Char]
identifier [Char]
cmd = [Char]
cmd [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
locateFlag

-- | The string appended to the end of the .emacs file.

setupString :: String -> String
setupString :: [Char] -> [Char]
setupString [Char]
cmd = [[Char]] -> [Char]
unlines
  [ [Char]
""
  , [Char]
"(load-file (let ((coding-system-for-read 'utf-8))"
  , [Char]
"                (shell-command-to-string \""
                        [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
identifier [Char]
cmd [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\")))"
  ]

------------------------------------------------------------------------
-- Querying Emacs

-- | Evaluates the given Elisp command using Emacs. The output of the
-- command (whatever was written into the current buffer) is returned.
--
-- Note: The input is not checked. The input is assumed to come from a
-- trusted source.

askEmacs :: String -> IO String
askEmacs :: [Char] -> IO [Char]
askEmacs [Char]
query = do
  [Char]
tempDir <- IO [Char]
getTemporaryDirectory
  IO ([Char], Handle)
-> (([Char], Handle) -> IO ())
-> (([Char], Handle) -> IO [Char])
-> IO [Char]
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracket ([Char] -> [Char] -> IO ([Char], Handle)
openTempFile [Char]
tempDir [Char]
"askEmacs")
          ([Char] -> IO ()
removeFile ([Char] -> IO ())
-> (([Char], Handle) -> [Char]) -> ([Char], Handle) -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char], Handle) -> [Char]
forall a b. (a, b) -> a
fst) ((([Char], Handle) -> IO [Char]) -> IO [Char])
-> (([Char], Handle) -> IO [Char]) -> IO [Char]
forall a b. (a -> b) -> a -> b
$ \ ([Char]
file, Handle
h) -> do
    Handle -> IO ()
hClose Handle
h
    ExitCode
exit <- [Char] -> [[Char]] -> IO ExitCode
rawSystemWithDiagnostics [Char]
"emacs"
      [ [Char]
"--batch"
          -- Andreas, 2022-10-15, issue #5901, suggested by Spencer Baugh (catern):
          -- Use Emacs batch mode so that it can run without a terminal.
      , [Char]
"--user", [Char]
""
          -- The flag --user is necessary with --batch so that user-init-file is defined.
          -- The empty user is the default user.
          -- (Option --batch includes --no-init-file, this is reverted by supplying --user.)
      -- Andreas, 2022-05-25, issue #5901 reloaded:
      -- Loading the init file without loading the site fails for some users:
      -- , "--quick"
      --     -- Option --quick includes --no-site-file.
      , [Char]
"--eval"
      , [[Char]] -> [Char]
apply [ [Char]
"with-temp-file", [Char] -> [Char]
escape [Char]
file, [[Char]] -> [Char]
apply [ [Char]
"insert", [Char]
query ] ]
          -- Short cutting the temp file via just [ "princ", query ]
          -- does not work if the loading of the user-init-file prints extra stuff.
          -- Going via the temp file we can let this stuff go to stdout without
          -- affecting the output we care about.
      ]
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (ExitCode
exit ExitCode -> ExitCode -> Bool
forall a. Eq a => a -> a -> Bool
== ExitCode
ExitSuccess) do
      [Char] -> IO ()
informLn [Char]
"Unable to query Emacs."
      IO ()
forall a. IO a
exitFailure
    [Char] -> IOMode -> (Handle -> IO [Char]) -> IO [Char]
forall r. [Char] -> IOMode -> (Handle -> IO r) -> IO r
withFile [Char]
file IOMode
ReadMode \ Handle
h -> do
      [Char]
result <- Handle -> IO [Char]
hGetContents Handle
h
      Int
_ <- Int -> IO Int
forall a. a -> IO a
evaluate ([Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
result)
        -- Uses evaluate to ensure that the file is not closed prematurely.
      [Char] -> IO [Char]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Char]
result

-- | Like 'rawSystem' but handles 'IOException' by printing diagnostics
-- (@PATH@) before 'exitFailure'.

rawSystemWithDiagnostics
  :: FilePath  -- ^ Command to run.
  -> [String]  -- ^ Arguments to command.
  -> IO ExitCode
rawSystemWithDiagnostics :: [Char] -> [[Char]] -> IO ExitCode
rawSystemWithDiagnostics [Char]
cmd [[Char]]
args =
    [Char] -> [[Char]] -> IO ExitCode
rawSystem [Char]
cmd [[Char]]
args
  IO ExitCode -> (IOException -> IO ExitCode) -> IO ExitCode
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`E.catch` \ (IOException
e :: IOException) -> do
     [Char] -> IO ()
informLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords [ [Char]
"FAILED:", [Char] -> [[Char]] -> [Char]
showCommandForUser [Char]
cmd [[Char]]
args ]
     [Char] -> IO ()
informLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords [ [Char]
"Exception:", IOException -> [Char]
forall a. Show a => a -> [Char]
show IOException
e ]
     -- The PATH might be useful in other exceptions, like "permission denied".
     [Char]
path <- [Char] -> Maybe [Char] -> [Char]
forall a. a -> Maybe a -> a
fromMaybe [Char]
"(not found)" (Maybe [Char] -> [Char]) -> IO (Maybe [Char]) -> IO [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> IO (Maybe [Char])
findExecutable [Char]
cmd
     [Char] -> IO ()
informLn ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords [ [Char]
"Executable", [Char]
cmd, [Char]
"at:", [Char]
path ]
     [Char] -> IO ()
informLn [Char]
"PATH:"
     ([Char] -> IO ()) -> [[Char]] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Char] -> IO ()
informLn ([Char] -> IO ()) -> ([Char] -> [Char]) -> [Char] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char]
"  - " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++)) ([[Char]] -> IO ()) -> IO [[Char]] -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO [[Char]]
getSearchPath
     IO ExitCode
forall a. IO a
exitFailure

-- | Escapes the string so that Emacs can parse it as an Elisp string.

escape :: FilePath -> FilePath
escape :: [Char] -> [Char]
escape [Char]
s = [Char]
"\"" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Char -> [Char]) -> [Char] -> [Char]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> [Char]
esc [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\""
  where
  esc :: Char -> [Char]
esc Char
c | Char
c Char -> [Char] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Char
'\\', Char
'"']   = Char
'\\' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char
c]
        | Char -> Bool
isAscii Char
c Bool -> Bool -> Bool
&& Char -> Bool
isPrint Char
c = [Char
c]
        | Bool
otherwise              = [Char]
"\\x" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char] -> [Char]
forall a. Integral a => a -> [Char] -> [Char]
showHex (Char -> Int
forall a. Enum a => a -> Int
fromEnum Char
c) [Char]
"\\ "

------------------------------------------------------------------------
-- Compiling Emacs Lisp files

-- | Tries to compile the Agda mode's Emacs Lisp files.

compileElispFiles :: IO ()
compileElispFiles :: IO ()
compileElispFiles = do
  [Char]
dataDir <- IO [Char]
getDataDir IO [Char] -> ([Char] -> [Char]) -> IO [Char]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> ([Char] -> [Char] -> [Char]
</> [Char]
emacsModeDir)
  let elFiles :: [[Char]]
elFiles = ([Char] -> [Char]) -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char]
dataDir [Char] -> [Char] -> [Char]
</>) [[Char]]
emacsLispFiles
  ([[Char]]
existing, [[Char]]
missing) <- ([Char] -> IO Bool) -> [[Char]] -> IO ([[Char]], [[Char]])
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m ([a], [a])
partitionM [Char] -> IO Bool
doesFileExist [[Char]]
elFiles
  [[Char]]
failed <- [Maybe [Char]] -> [[Char]]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe [Char]] -> [[Char]]) -> IO [Maybe [Char]] -> IO [[Char]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> IO (Maybe [Char])) -> [[Char]] -> IO [Maybe [Char]]
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] -> [Char] -> IO (Maybe [Char])
compile [Char]
dataDir) [[Char]]
existing

  -- If any of the .el files was missing or failed to compile, fail execution.
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([[Char]] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Char]]
missing) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    [Char] -> IO ()
informLn [Char]
"Missing Emacs Lisp files:"
    ([Char] -> IO ()) -> [[Char]] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Char] -> IO ()
informLn ([Char] -> IO ()) -> ([Char] -> [Char]) -> [Char] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++)) [[Char]]
missing
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([[Char]] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Char]]
failed) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    [Char] -> IO ()
informLn [Char]
"Unable to compile the following Emacs Lisp files:"
    ([Char] -> IO ()) -> [[Char]] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Char] -> IO ()
informLn ([Char] -> IO ()) -> ([Char] -> [Char]) -> [Char] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char]
"  " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++)) [[Char]]
failed
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([[Char]] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Char]]
missing Bool -> Bool -> Bool
&& [[Char]] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Char]]
failed) IO ()
forall a. IO a
exitFailure

  where
  compile :: [Char] -> [Char] -> IO (Maybe [Char])
compile [Char]
dataDir [Char]
f = do
    ExitCode
exit <- [Char] -> [[Char]] -> IO ExitCode
rawSystemWithDiagnostics [Char]
"emacs" ([[Char]] -> IO ExitCode) -> [[Char]] -> IO ExitCode
forall a b. (a -> b) -> a -> b
$
      [ [Char]
"--quick"                -- 'quick' implies 'no-site-file'
      , [Char]
"--directory", [Char]
dataDir
      , [Char]
"--batch"                -- 'batch' implies 'no-init-file' but not 'no-site-file'.
      , [Char]
"--eval"
      , [Char]
"(progn \
           \(setq byte-compile-error-on-warn t) \
           \(byte-compile-disable-warning 'cl-functions) \
           \(batch-byte-compile))"
      , [Char]
f
      ]
    Maybe [Char] -> IO (Maybe [Char])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [Char] -> IO (Maybe [Char]))
-> Maybe [Char] -> IO (Maybe [Char])
forall a b. (a -> b) -> a -> b
$ if ExitCode
exit ExitCode -> ExitCode -> Bool
forall a. Eq a => a -> a -> Bool
== ExitCode
ExitSuccess then Maybe [Char]
forall a. Maybe a
Nothing else [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
f

------------------------------------------------------------------------
-- Helper functions

-- These functions inform the user about something by printing on
-- stderr.

inform :: String -> IO ()
inform :: [Char] -> IO ()
inform   = Handle -> [Char] -> IO ()
hPutStr   Handle
stderr

informLn :: String -> IO ()
informLn :: [Char] -> IO ()
informLn = Handle -> [Char] -> IO ()
hPutStrLn Handle
stderr

parens :: String -> String
parens :: [Char] -> [Char]
parens [Char]
s = [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
"(", [Char]
s, [Char]
")" ]

-- LISP application
apply :: [String] -> String
apply :: [[Char]] -> [Char]
apply = [Char] -> [Char]
parens ([Char] -> [Char]) -> ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Char]] -> [Char]
unwords

-- Utilities

-- | A ``monadic'' version of @'partition' :: (a -> Bool) -> [a] -> ([a],[a])
partitionM :: Applicative m => (a -> m Bool) -> [a] -> m ([a], [a])
partitionM :: forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m ([a], [a])
partitionM a -> m Bool
f =
  (a -> m ([a], [a]) -> m ([a], [a]))
-> m ([a], [a]) -> [a] -> m ([a], [a])
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ a
x -> (Bool -> ([a], [a]) -> ([a], [a]))
-> m Bool -> m ([a], [a]) -> m ([a], [a])
forall a b c. (a -> b -> c) -> m a -> m b -> m c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 ((([a], [a]) -> ([a], [a]))
-> (([a], [a]) -> ([a], [a])) -> Bool -> ([a], [a]) -> ([a], [a])
forall a. a -> a -> Bool -> a
bool (([a] -> [a]) -> ([a], [a]) -> ([a], [a])
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:)) (([a] -> [a]) -> ([a], [a]) -> ([a], [a])
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:))) (m Bool -> m ([a], [a]) -> m ([a], [a]))
-> m Bool -> m ([a], [a]) -> m ([a], [a])
forall a b. (a -> b) -> a -> b
$ a -> m Bool
f a
x)
        (([a], [a]) -> m ([a], [a])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], []))