{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# OPTIONS_HADDOCK show-extensions #-}

-- |
-- Module      :  Yi.Mode.Abella
-- License     :  GPL-2
-- Maintainer  :  yi-devel@googlegroups.com
-- Stability   :  experimental
-- Portability :  portable
--
-- 'Mode's and utility function for working with the Abella
-- interactive theorem prover.

module Yi.Mode.Abella
  ( abellaModeEmacs
  , abella
  , abellaEval
  , abellaEvalFromProofPoint
  , abellaUndo
  , abellaGet
  , abellaSend
  ) where

import           Lens.Micro.Platform (use, (%~), (&), (.=), (.~))
import           Control.Monad       (join, when)
import           Data.Binary         (Binary)
import           Data.Char           (isSpace)
import           Data.Default        (Default)
import           Data.Maybe          (isJust)
import qualified Data.Text           as T (isInfixOf, snoc, unpack)
import           Data.Typeable       (Typeable)
import           Yi.Buffer
import           Yi.Core             (sendToProcess)
import           Yi.Editor
import           Yi.Keymap           (YiM, topKeymapA)
import           Yi.Keymap.Keys      (Event, choice, ctrlCh, (<||), (?*>>!))
import qualified Yi.Lexer.Abella     as Abella (Token, lexer)
import           Yi.MiniBuffer       (CommandArguments (..))
import qualified Yi.Mode.Interactive as Interactive (spawnProcess)
import           Yi.Mode.Common      (TokenBasedMode, anyExtension, styleMode)
import qualified Yi.Rope             as R (YiString, toText)
import           Yi.Types            (YiVariable)

abellaModeGen :: (Char -> [Event]) -> TokenBasedMode Abella.Token
abellaModeGen :: (Char -> [Event]) -> TokenBasedMode Token
abellaModeGen Char -> [Event]
abellaBinding = StyleLexer AlexState HlState Token AlexInput
-> TokenBasedMode Token
forall (l :: * -> *) s t i.
Show (l s) =>
StyleLexer l s t i -> TokenBasedMode t
styleMode StyleLexer AlexState HlState Token AlexInput
Abella.lexer
  TokenBasedMode Token
-> (TokenBasedMode Token -> TokenBasedMode Token)
-> TokenBasedMode Token
forall a b. a -> (a -> b) -> b
& (Text -> Identity Text)
-> TokenBasedMode Token -> Identity (TokenBasedMode Token)
forall syntax (f :: * -> *).
Functor f =>
(Text -> f Text) -> Mode syntax -> f (Mode syntax)
modeNameA ((Text -> Identity Text)
 -> TokenBasedMode Token -> Identity (TokenBasedMode Token))
-> Text -> TokenBasedMode Token -> TokenBasedMode Token
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Text
"abella"
  TokenBasedMode Token
-> (TokenBasedMode Token -> TokenBasedMode Token)
-> TokenBasedMode Token
forall a b. a -> (a -> b) -> b
& ((String -> YiString -> Bool)
 -> Identity (String -> YiString -> Bool))
-> TokenBasedMode Token -> Identity (TokenBasedMode Token)
forall syntax (f :: * -> *).
Functor f =>
((String -> YiString -> Bool) -> f (String -> YiString -> Bool))
-> Mode syntax -> f (Mode syntax)
modeAppliesA (((String -> YiString -> Bool)
  -> Identity (String -> YiString -> Bool))
 -> TokenBasedMode Token -> Identity (TokenBasedMode Token))
-> (String -> YiString -> Bool)
-> TokenBasedMode Token
-> TokenBasedMode Token
forall s t a b. ASetter s t a b -> b -> s -> t
.~ [String] -> String -> YiString -> Bool
forall a. [String] -> String -> a -> Bool
anyExtension [String
"thm"]
  TokenBasedMode Token
-> (TokenBasedMode Token -> TokenBasedMode Token)
-> TokenBasedMode Token
forall a b. a -> (a -> b) -> b
& (Maybe (BufferM ()) -> Identity (Maybe (BufferM ())))
-> TokenBasedMode Token -> Identity (TokenBasedMode Token)
forall syntax (f :: * -> *).
Functor f =>
(Maybe (BufferM ()) -> f (Maybe (BufferM ())))
-> Mode syntax -> f (Mode syntax)
modeToggleCommentSelectionA ((Maybe (BufferM ()) -> Identity (Maybe (BufferM ())))
 -> TokenBasedMode Token -> Identity (TokenBasedMode Token))
-> Maybe (BufferM ())
-> TokenBasedMode Token
-> TokenBasedMode Token
forall s t a b. ASetter s t a b -> b -> s -> t
.~ BufferM () -> Maybe (BufferM ())
forall a. a -> Maybe a
Just (YiString -> BufferM ()
toggleCommentB YiString
"%")
  TokenBasedMode Token
-> (TokenBasedMode Token -> TokenBasedMode Token)
-> TokenBasedMode Token
forall a b. a -> (a -> b) -> b
& ((KeymapSet -> KeymapSet) -> Identity (KeymapSet -> KeymapSet))
-> TokenBasedMode Token -> Identity (TokenBasedMode Token)
forall syntax (f :: * -> *).
Functor f =>
((KeymapSet -> KeymapSet) -> f (KeymapSet -> KeymapSet))
-> Mode syntax -> f (Mode syntax)
modeKeymapA (((KeymapSet -> KeymapSet) -> Identity (KeymapSet -> KeymapSet))
 -> TokenBasedMode Token -> Identity (TokenBasedMode Token))
-> (KeymapSet -> KeymapSet)
-> TokenBasedMode Token
-> TokenBasedMode Token
forall s t a b. ASetter s t a b -> b -> s -> t
.~ (Keymap -> Identity Keymap) -> KeymapSet -> Identity KeymapSet
Lens' KeymapSet Keymap
topKeymapA ((Keymap -> Identity Keymap) -> KeymapSet -> Identity KeymapSet)
-> (Keymap -> Keymap) -> KeymapSet -> KeymapSet
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ Keymap -> Keymap -> Keymap
forall (f :: * -> *) w e a.
MonadInteract f w e =>
f a -> f a -> f a
(<||)
     ([Keymap] -> Keymap
forall (m :: * -> *) w e a.
(MonadInteract m w e, MonadFail m) =>
[m a] -> m a
choice
      [ Char -> [Event]
abellaBinding Char
'p' [Event] -> YiM () -> Keymap
forall (m :: * -> *) a x.
(MonadInteract m Action Event, YiAction a x, Show x) =>
[Event] -> a -> m ()
?*>>! YiM ()
abellaUndo
      , Char -> [Event]
abellaBinding Char
'e' [Event] -> YiM () -> Keymap
forall (m :: * -> *) a x.
(MonadInteract m Action Event, YiAction a x, Show x) =>
[Event] -> a -> m ()
?*>>! YiM ()
abellaEval
      , Char -> [Event]
abellaBinding Char
'n' [Event] -> YiM () -> Keymap
forall (m :: * -> *) a x.
(MonadInteract m Action Event, YiAction a x, Show x) =>
[Event] -> a -> m ()
?*>>! YiM ()
abellaNext
      , Char -> [Event]
abellaBinding Char
'a' [Event] -> YiM () -> Keymap
forall (m :: * -> *) a x.
(MonadInteract m Action Event, YiAction a x, Show x) =>
[Event] -> a -> m ()
?*>>! YiM ()
abellaAbort
      , Char -> [Event]
abellaBinding Char
'\r' [Event] -> YiM () -> Keymap
forall (m :: * -> *) a x.
(MonadInteract m Action Event, YiAction a x, Show x) =>
[Event] -> a -> m ()
?*>>! YiM ()
abellaEvalFromProofPoint
      ])

abellaModeEmacs :: TokenBasedMode Abella.Token
abellaModeEmacs :: TokenBasedMode Token
abellaModeEmacs = (Char -> [Event]) -> TokenBasedMode Token
abellaModeGen (\Char
ch -> [Char -> Event
ctrlCh Char
'c', Char -> Event
ctrlCh Char
ch])

newtype AbellaBuffer = AbellaBuffer {AbellaBuffer -> Maybe BufferRef
_abellaBuffer :: Maybe BufferRef}
    deriving (AbellaBuffer
AbellaBuffer -> Default AbellaBuffer
forall a. a -> Default a
$cdef :: AbellaBuffer
def :: AbellaBuffer
Default, Typeable, Get AbellaBuffer
[AbellaBuffer] -> Put
AbellaBuffer -> Put
(AbellaBuffer -> Put)
-> Get AbellaBuffer
-> ([AbellaBuffer] -> Put)
-> Binary AbellaBuffer
forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
$cput :: AbellaBuffer -> Put
put :: AbellaBuffer -> Put
$cget :: Get AbellaBuffer
get :: Get AbellaBuffer
$cputList :: [AbellaBuffer] -> Put
putList :: [AbellaBuffer] -> Put
Binary)
instance YiVariable AbellaBuffer

getProofPointMark :: BufferM Mark
getProofPointMark :: BufferM Mark
getProofPointMark = Maybe String -> BufferM Mark
getMarkB (Maybe String -> BufferM Mark) -> Maybe String -> BufferM Mark
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"p"

getTheoremPointMark :: BufferM Mark
getTheoremPointMark :: BufferM Mark
getTheoremPointMark = Maybe String -> BufferM Mark
getMarkB (Maybe String -> BufferM Mark) -> Maybe String -> BufferM Mark
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
"t"

abellaEval :: YiM ()
abellaEval :: YiM ()
abellaEval = do
  YiString
reg <- BufferM YiString -> YiM YiString
forall (m :: * -> *) a. MonadEditor m => BufferM a -> m a
withCurrentBuffer (BufferM YiString -> YiM YiString)
-> (BufferM YiString -> BufferM YiString)
-> BufferM YiString
-> YiM YiString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BufferM YiString -> BufferM YiString
forall a. BufferM a -> BufferM a
savingPointB (BufferM YiString -> YiM YiString)
-> BufferM YiString -> YiM YiString
forall a b. (a -> b) -> a -> b
$ do
    BufferM (BufferM ()) -> BufferM ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
(.=) (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ())
-> (Mark -> ASetter FBuffer FBuffer Point Point)
-> Mark
-> Point
-> BufferM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mark -> ASetter FBuffer FBuffer Point Point
forall (f :: * -> *).
Functor f =>
Mark -> (Point -> f Point) -> FBuffer -> f FBuffer
markPointA (Mark -> Point -> BufferM ())
-> BufferM Mark -> BufferM (Point -> BufferM ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BufferM Mark
getProofPointMark BufferM (Point -> BufferM ())
-> BufferM Point -> BufferM (BufferM ())
forall a b. BufferM (a -> b) -> BufferM a -> BufferM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BufferM Point
pointB)
    BufferM ()
leftB
    Region -> BufferM YiString
readRegionB (Region -> BufferM YiString) -> BufferM Region -> BufferM YiString
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TextUnit -> BufferM Region
regionOfNonEmptyB TextUnit
unitSentence
  YiString -> YiM ()
abellaSend YiString
reg

abellaEvalFromProofPoint :: YiM ()
abellaEvalFromProofPoint :: YiM ()
abellaEvalFromProofPoint = YiString -> YiM ()
abellaSend (YiString -> YiM ()) -> YiM YiString -> YiM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< BufferM YiString -> YiM YiString
forall (m :: * -> *) a. MonadEditor m => BufferM a -> m a
withCurrentBuffer BufferM YiString
f
  where f :: BufferM YiString
f = do Mark
mark <- BufferM Mark
getProofPointMark
               Point
p <- Getting Point FBuffer Point -> BufferM Point
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use (Getting Point FBuffer Point -> BufferM Point)
-> Getting Point FBuffer Point -> BufferM Point
forall a b. (a -> b) -> a -> b
$ Mark -> Getting Point FBuffer Point
forall (f :: * -> *).
Functor f =>
Mark -> (Point -> f Point) -> FBuffer -> f FBuffer
markPointA Mark
mark
               Point
cur <- BufferM Point
pointB
               Mark -> ASetter FBuffer FBuffer Point Point
forall (f :: * -> *).
Functor f =>
Mark -> (Point -> f Point) -> FBuffer -> f FBuffer
markPointA Mark
mark ASetter FBuffer FBuffer Point Point -> Point -> BufferM ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Point
cur
               Region -> BufferM YiString
readRegionB (Region -> BufferM YiString) -> Region -> BufferM YiString
forall a b. (a -> b) -> a -> b
$ Point -> Point -> Region
mkRegion Point
p Point
cur

abellaNext :: YiM ()
abellaNext :: YiM ()
abellaNext = do
  YiString
reg <- BufferM YiString -> YiM YiString
forall (m :: * -> *) a. MonadEditor m => BufferM a -> m a
withCurrentBuffer (BufferM YiString -> YiM YiString)
-> BufferM YiString -> YiM YiString
forall a b. (a -> b) -> a -> b
$ BufferM ()
rightB BufferM () -> BufferM YiString -> BufferM YiString
forall a b. BufferM a -> BufferM b -> BufferM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Region -> BufferM YiString
readRegionB (Region -> BufferM YiString) -> BufferM Region -> BufferM YiString
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TextUnit -> BufferM Region
regionOfNonEmptyB TextUnit
unitSentence)
  YiString -> YiM ()
abellaSend YiString
reg
  BufferM () -> YiM ()
forall (m :: * -> *) a. MonadEditor m => BufferM a -> m a
withCurrentBuffer (BufferM () -> YiM ()) -> BufferM () -> YiM ()
forall a b. (a -> b) -> a -> b
$ do
    TextUnit -> Direction -> BufferM ()
moveB TextUnit
unitSentence Direction
Forward
    BufferM ()
rightB
    BufferM Bool -> BufferM () -> BufferM ()
forall a. BufferM Bool -> BufferM a -> BufferM ()
untilB_ (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isSpace (Char -> Bool) -> BufferM Char -> BufferM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BufferM Char
readB) BufferM ()
rightB
    BufferM Bool -> BufferM () -> BufferM ()
forall a. BufferM Bool -> BufferM a -> BufferM ()
untilB_ ((Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'%') (Char -> Bool) -> BufferM Char -> BufferM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BufferM Char
readB) (BufferM () -> BufferM ()) -> BufferM () -> BufferM ()
forall a b. (a -> b) -> a -> b
$ BufferM ()
moveToEol BufferM () -> BufferM () -> BufferM ()
forall a b. BufferM a -> BufferM b -> BufferM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BufferM ()
rightB BufferM () -> BufferM () -> BufferM ()
forall a b. BufferM a -> BufferM b -> BufferM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> BufferM ()
firstNonSpaceB
    BufferM (BufferM ()) -> BufferM ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
(.=) (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ())
-> (Mark -> ASetter FBuffer FBuffer Point Point)
-> Mark
-> Point
-> BufferM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mark -> ASetter FBuffer FBuffer Point Point
forall (f :: * -> *).
Functor f =>
Mark -> (Point -> f Point) -> FBuffer -> f FBuffer
markPointA (Mark -> Point -> BufferM ())
-> BufferM Mark -> BufferM (Point -> BufferM ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BufferM Mark
getProofPointMark BufferM (Point -> BufferM ())
-> BufferM Point -> BufferM (BufferM ())
forall a b. BufferM (a -> b) -> BufferM a -> BufferM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BufferM Point
pointB)

abellaUndo :: YiM ()
abellaUndo :: YiM ()
abellaUndo = do
  YiString -> YiM ()
abellaSend YiString
"undo."
  BufferM () -> YiM ()
forall (m :: * -> *) a. MonadEditor m => BufferM a -> m a
withCurrentBuffer (BufferM () -> YiM ()) -> BufferM () -> YiM ()
forall a b. (a -> b) -> a -> b
$ do
    TextUnit -> Direction -> BufferM ()
moveB TextUnit
unitSentence Direction
Backward
    BufferM (BufferM ()) -> BufferM ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
(.=) (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ())
-> (Mark -> ASetter FBuffer FBuffer Point Point)
-> Mark
-> Point
-> BufferM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mark -> ASetter FBuffer FBuffer Point Point
forall (f :: * -> *).
Functor f =>
Mark -> (Point -> f Point) -> FBuffer -> f FBuffer
markPointA (Mark -> Point -> BufferM ())
-> BufferM Mark -> BufferM (Point -> BufferM ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BufferM Mark
getProofPointMark BufferM (Point -> BufferM ())
-> BufferM Point -> BufferM (BufferM ())
forall a b. BufferM (a -> b) -> BufferM a -> BufferM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BufferM Point
pointB)

abellaAbort :: YiM ()
abellaAbort :: YiM ()
abellaAbort = do
  YiString -> YiM ()
abellaSend YiString
"abort."
  BufferM () -> YiM ()
forall (m :: * -> *) a. MonadEditor m => BufferM a -> m a
withCurrentBuffer (BufferM () -> YiM ()) -> BufferM () -> YiM ()
forall a b. (a -> b) -> a -> b
$ do
    Point -> BufferM ()
moveTo (Point -> BufferM ()) -> BufferM Point -> BufferM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Getting Point FBuffer Point -> BufferM Point
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use (Getting Point FBuffer Point -> BufferM Point)
-> (Mark -> Getting Point FBuffer Point) -> Mark -> BufferM Point
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mark -> Getting Point FBuffer Point
forall (f :: * -> *).
Functor f =>
Mark -> (Point -> f Point) -> FBuffer -> f FBuffer
markPointA (Mark -> BufferM Point) -> BufferM Mark -> BufferM Point
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< BufferM Mark
getTheoremPointMark
    BufferM (BufferM ()) -> BufferM ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
(.=) (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ())
-> (Mark -> ASetter FBuffer FBuffer Point Point)
-> Mark
-> Point
-> BufferM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mark -> ASetter FBuffer FBuffer Point Point
forall (f :: * -> *).
Functor f =>
Mark -> (Point -> f Point) -> FBuffer -> f FBuffer
markPointA (Mark -> Point -> BufferM ())
-> BufferM Mark -> BufferM (Point -> BufferM ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BufferM Mark
getProofPointMark BufferM (Point -> BufferM ())
-> BufferM Point -> BufferM (BufferM ())
forall a b. BufferM (a -> b) -> BufferM a -> BufferM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BufferM Point
pointB)

-- | Start Abella in a buffer
abella :: CommandArguments -> YiM BufferRef
abella :: CommandArguments -> YiM BufferRef
abella (CommandArguments [Text]
args) = do
    BufferRef
b <- String -> [String] -> YiM BufferRef
Interactive.spawnProcess String
"abella" (Text -> String
T.unpack (Text -> String) -> [Text] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Text]
args)
    EditorM () -> YiM ()
forall a. EditorM a -> YiM a
forall (m :: * -> *) a. MonadEditor m => EditorM a -> m a
withEditor (EditorM () -> YiM ())
-> (Maybe BufferRef -> EditorM ()) -> Maybe BufferRef -> YiM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbellaBuffer -> EditorM ()
forall (m :: * -> *) a.
(MonadEditor m, YiVariable a, Functor m) =>
a -> m ()
putEditorDyn (AbellaBuffer -> EditorM ())
-> (Maybe BufferRef -> AbellaBuffer)
-> Maybe BufferRef
-> EditorM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe BufferRef -> AbellaBuffer
AbellaBuffer (Maybe BufferRef -> YiM ()) -> Maybe BufferRef -> YiM ()
forall a b. (a -> b) -> a -> b
$ BufferRef -> Maybe BufferRef
forall a. a -> Maybe a
Just BufferRef
b
    BufferRef -> YiM BufferRef
forall a. a -> YiM a
forall (m :: * -> *) a. Monad m => a -> m a
return BufferRef
b

-- | Return Abella's buffer; create it if necessary.
-- Show it in another window.
abellaGet :: YiM BufferRef
abellaGet :: YiM BufferRef
abellaGet = YiM BufferRef -> YiM BufferRef
forall (m :: * -> *) a. MonadEditor m => m a -> m a
withOtherWindow (YiM BufferRef -> YiM BufferRef) -> YiM BufferRef -> YiM BufferRef
forall a b. (a -> b) -> a -> b
$ do
    AbellaBuffer Maybe BufferRef
mb <- EditorM AbellaBuffer -> YiM AbellaBuffer
forall a. EditorM a -> YiM a
forall (m :: * -> *) a. MonadEditor m => EditorM a -> m a
withEditor EditorM AbellaBuffer
forall (m :: * -> *) a.
(MonadEditor m, YiVariable a, Default a, Functor m) =>
m a
getEditorDyn
    case Maybe BufferRef
mb of
        Maybe BufferRef
Nothing -> CommandArguments -> YiM BufferRef
abella ([Text] -> CommandArguments
CommandArguments [])
        Just BufferRef
b -> do
            Bool
stillExists <- Maybe FBuffer -> Bool
forall a. Maybe a -> Bool
isJust (Maybe FBuffer -> Bool) -> YiM (Maybe FBuffer) -> YiM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BufferRef -> YiM (Maybe FBuffer)
forall (m :: * -> *).
MonadEditor m =>
BufferRef -> m (Maybe FBuffer)
findBuffer BufferRef
b
            if Bool
stillExists
                then do EditorM () -> YiM ()
forall a. EditorM a -> YiM a
forall (m :: * -> *) a. MonadEditor m => EditorM a -> m a
withEditor (EditorM () -> YiM ()) -> EditorM () -> YiM ()
forall a b. (a -> b) -> a -> b
$ BufferRef -> EditorM ()
switchToBufferE BufferRef
b
                        BufferRef -> YiM BufferRef
forall a. a -> YiM a
forall (m :: * -> *) a. Monad m => a -> m a
return BufferRef
b
                else CommandArguments -> YiM BufferRef
abella ([Text] -> CommandArguments
CommandArguments [])

-- | Send a command to Abella
abellaSend :: R.YiString -> YiM ()
abellaSend :: YiString -> YiM ()
abellaSend YiString
cmd' = do
  let cmd :: Text
cmd = YiString -> Text
R.toText YiString
cmd'
  Bool -> YiM () -> YiM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Text
"Theorem" Text -> Text -> Bool
`T.isInfixOf` Text
cmd) (YiM () -> YiM ()) -> YiM () -> YiM ()
forall a b. (a -> b) -> a -> b
$
    BufferM () -> YiM ()
forall (m :: * -> *) a. MonadEditor m => BufferM a -> m a
withCurrentBuffer (BufferM () -> YiM ()) -> BufferM () -> YiM ()
forall a b. (a -> b) -> a -> b
$ BufferM (BufferM ()) -> BufferM ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
(.=) (ASetter FBuffer FBuffer Point Point -> Point -> BufferM ())
-> (Mark -> ASetter FBuffer FBuffer Point Point)
-> Mark
-> Point
-> BufferM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mark -> ASetter FBuffer FBuffer Point Point
forall (f :: * -> *).
Functor f =>
Mark -> (Point -> f Point) -> FBuffer -> f FBuffer
markPointA (Mark -> Point -> BufferM ())
-> BufferM Mark -> BufferM (Point -> BufferM ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BufferM Mark
getTheoremPointMark BufferM (Point -> BufferM ())
-> BufferM Point -> BufferM (BufferM ())
forall a b. BufferM (a -> b) -> BufferM a -> BufferM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BufferM Point
pointB)
  BufferRef
b <- YiM BufferRef
abellaGet
  BufferRef -> BufferM () -> YiM ()
forall (m :: * -> *) a.
MonadEditor m =>
BufferRef -> BufferM a -> m a
withGivenBuffer BufferRef
b BufferM ()
botB
  BufferRef -> String -> YiM ()
sendToProcess BufferRef
b (String -> YiM ()) -> (Text -> String) -> Text -> YiM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack (Text -> YiM ()) -> Text -> YiM ()
forall a b. (a -> b) -> a -> b
$ Text
cmd Text -> Char -> Text
`T.snoc` Char
'\n'