module Yi.Mode.Abella
( abellaModeEmacs
, abella
, abellaEval
, abellaEvalFromProofPoint
, abellaUndo
, abellaGet
, abellaSend
) where
import Control.Applicative (Applicative ((<*>)), (<$>))
import Control.Lens (assign, 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.Modes (TokenBasedMode, anyExtension, styleMode)
import qualified Yi.Rope as R (YiString, toText)
import Yi.Types (YiVariable)
abellaModeGen :: (Char -> [Event]) -> TokenBasedMode Abella.Token
abellaModeGen abellaBinding = styleMode Abella.lexer
& modeNameA .~ "abella"
& modeAppliesA .~ anyExtension ["thm"]
& modeToggleCommentSelectionA .~ Just (toggleCommentB "%")
& modeKeymapA .~ topKeymapA %~ (<||)
(choice
[ abellaBinding 'p' ?*>>! abellaUndo
, abellaBinding 'e' ?*>>! abellaEval
, abellaBinding 'n' ?*>>! abellaNext
, abellaBinding 'a' ?*>>! abellaAbort
, abellaBinding '\r' ?*>>! abellaEvalFromProofPoint
])
abellaModeEmacs :: TokenBasedMode Abella.Token
abellaModeEmacs = abellaModeGen (\ch -> [ctrlCh 'c', ctrlCh ch])
newtype AbellaBuffer = AbellaBuffer {_abellaBuffer :: Maybe BufferRef}
deriving (Default, Typeable, Binary)
instance YiVariable AbellaBuffer
getProofPointMark :: BufferM Mark
getProofPointMark = getMarkB $ Just "p"
getTheoremPointMark :: BufferM Mark
getTheoremPointMark = getMarkB $ Just "t"
abellaEval :: YiM ()
abellaEval = do
reg <- withCurrentBuffer . savingPointB $ do
join (assign . markPointA <$> getProofPointMark <*> pointB)
leftB
readRegionB =<< regionOfNonEmptyB unitSentence
abellaSend reg
abellaEvalFromProofPoint :: YiM ()
abellaEvalFromProofPoint = abellaSend =<< withCurrentBuffer f
where f = do mark <- getProofPointMark
p <- use $ markPointA mark
cur <- pointB
markPointA mark .= cur
readRegionB $ mkRegion p cur
abellaNext :: YiM ()
abellaNext = do
reg <- withCurrentBuffer $ rightB >> (readRegionB =<< regionOfNonEmptyB unitSentence)
abellaSend reg
withCurrentBuffer $ do
moveB unitSentence Forward
rightB
untilB_ (not . isSpace <$> readB) rightB
untilB_ ((/= '%') <$> readB) $ moveToEol >> rightB >> firstNonSpaceB
join (assign . markPointA <$> getProofPointMark <*> pointB)
abellaUndo :: YiM ()
abellaUndo = do
abellaSend "undo."
withCurrentBuffer $ do
moveB unitSentence Backward
join (assign . markPointA <$> getProofPointMark <*> pointB)
abellaAbort :: YiM ()
abellaAbort = do
abellaSend "abort."
withCurrentBuffer $ do
moveTo =<< use . markPointA =<< getTheoremPointMark
join (assign . markPointA <$> getProofPointMark <*> pointB)
abella :: CommandArguments -> YiM BufferRef
abella (CommandArguments args) = do
b <- Interactive.spawnProcess "abella" (T.unpack <$> args)
withEditor . putEditorDyn . AbellaBuffer $ Just b
return b
abellaGet :: YiM BufferRef
abellaGet = withOtherWindow $ do
AbellaBuffer mb <- withEditor getEditorDyn
case mb of
Nothing -> abella (CommandArguments [])
Just b -> do
stillExists <- isJust <$> findBuffer b
if stillExists
then do withEditor $ switchToBufferE b
return b
else abella (CommandArguments [])
abellaSend :: R.YiString -> YiM ()
abellaSend cmd' = do
let cmd = R.toText cmd'
when ("Theorem" `T.isInfixOf` cmd) $
withCurrentBuffer $ join (assign . markPointA <$> getTheoremPointMark <*> pointB)
b <- abellaGet
withGivenBuffer b botB
sendToProcess b . T.unpack $ cmd `T.snoc` '\n'