    {-# 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
      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
      abellaSend 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 <- BufferM Mark
    getProofPointMark
                   p <- use $ markPointA mark
                   cur <- pointB
                   markPointA mark .= cur
                   readRegionB $ mkRegion p cur

    abellaNext :: YiM ()
    abellaNext :: YiM ()
    abellaNext = do
      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)
      abellaSend reg
      withCurrentBuffer $ do
        moveB unitSentence Forward
        rightB
        untilB_ (not . isSpace <$> readB) rightB
        untilB_ ((/= '%') <$> readB) $ moveToEol >> rightB >> firstNonSpaceB
        join ((.=) . markPointA <$> getProofPointMark <*> 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
        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)
        withEditor . putEditorDyn . AbellaBuffer $ Just b
        return 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 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 mb of
            Maybe BufferRef
    Nothing -> CommandArguments -> YiM BufferRef
    abella ([Text] -> CommandArguments
    CommandArguments [])
            Just BufferRef
    b -> do
                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 stillExists
                    then do withEditor $ switchToBufferE b
                            return b
                    else abella (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)
      b <- YiM BufferRef
    abellaGet
      withGivenBuffer b botB
      sendToProcess b . T.unpack $ cmd `T.snoc` '\n'