module Yi.Mode.Abella
( abellaModeEmacs
, abella
, abellaEval
, abellaEvalFromProofPoint
, abellaUndo
, abellaGet
, abellaSend
) where
import Control.Applicative
import Control.Lens
import Control.Monad
import Data.Binary
import Data.Char (isSpace)
import Data.Default
import Data.Maybe (isJust)
import qualified Data.Text as T
import Data.Typeable
import Yi.Buffer
import Yi.Core (sendToProcess)
import Yi.Types (YiVariable)
import Yi.Editor
import Yi.Keymap
import Yi.Keymap.Keys
import qualified Yi.Lexer.Abella as Abella
import Yi.MiniBuffer (CommandArguments(..))
import qualified Yi.Mode.Interactive as Interactive
import Yi.Modes (TokenBasedMode, styleMode, anyExtension)
import qualified Yi.Rope as R
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'