    module Agda.Interaction.Highlighting.Vim where

    import Control.Monad.Trans

    import Data.Function ( on )
    import qualified Data.List as List
    import qualified Data.Map as Map
    import Data.Maybe

    import System.FilePath

    import Agda.Syntax.Scope.Base
    import Agda.Syntax.Common
    import Agda.Syntax.Concrete.Name as CName

    import Agda.TypeChecking.Monad

    import qualified Agda.Utils.IO.UTF8 as UTF8
    import Agda.Utils.Tuple
    import Agda.Utils.Pretty

    vimFile :: FilePath -> FilePath
    vimFile :: [Char] -> [Char]
    vimFile [Char]
    file =
        case [Char] -> ([Char], [Char])
    splitFileName [Char]
    file of
            ([Char]
    path, [Char]
    name) -> [Char]
    path [Char] -> [Char] -> [Char]
    </> [Char]
    "" [Char] -> [Char] -> [Char]
    <.> [Char]
    name [Char] -> [Char] -> [Char]
    <.> [Char]
    "vim"

    escape :: String -> String
    escape :: [Char] -> [Char]
    escape = (Char -> [Char]) -> [Char] -> [Char]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Char -> [Char]
    esc
        where
            escchars :: String
            escchars :: [Char]
    escchars = [Char]
    "$\\^.*~[]"
            esc :: Char -> [Char]
    esc Char
    c   | Char
    c Char -> [Char] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Char]
    escchars = [Char
    '\\',Char
    c]
                    | Bool
    otherwise         = [Char
    c]

    wordBounded :: String -> String
    wordBounded :: [Char] -> [Char]
    wordBounded [Char]
    s0 = [[Char]] -> [Char]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[Char]
    "\\<", [Char]
    s0, [Char]
    "\\>"]

    keyword :: String -> [String] -> String
    keyword :: [Char] -> [[Char]] -> [Char]
    keyword [Char]
    _ [] = [Char]
    ""
    keyword [Char]
    cat [[Char]]
    ws  = [Char]
    "syn keyword " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [[Char]] -> [Char]
    unwords ([Char]
    cat [Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    : [[Char]]
    ws)

    match :: String -> [String] -> String
    match :: [Char] -> [[Char]] -> [Char]
    match [Char]
    _   [] = [Char]
    ""
    match [Char]
    cat [[Char]]
    ws =
      [Char]
    "syn match "
        [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    cat
        [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " \""
        [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    List.intercalate [Char]
    "\\|" (([Char] -> [Char]) -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char] -> [Char]
    wordBounded ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> [Char]
    escape) [[Char]]
    ws)
        [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\""

    matches :: [String] -> [String] -> [String] -> [String] -> [String] -> [String] -> [String]
    matches :: [[Char]]
    -> [[Char]]
    -> [[Char]]
    -> [[Char]]
    -> [[Char]]
    -> [[Char]]
    -> [[Char]]
    matches [[Char]]
    cons [[Char]]
    icons [[Char]]
    defs [[Char]]
    idefs [[Char]]
    flds [[Char]]
    iflds =
        ((Int, [Char]) -> [Char]) -> [(Int, [Char])] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, [Char]) -> [Char]
    forall a b. (a, b) -> b
    snd
        ([(Int, [Char])] -> [[Char]]) -> [(Int, [Char])] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $ ((Int, [Char]) -> (Int, [Char]) -> Ordering)
    -> [(Int, [Char])] -> [(Int, [Char])]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    List.sortBy (Int -> Int -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Int -> Int -> Ordering)
    -> ((Int, [Char]) -> Int)
    -> (Int, [Char])
    -> (Int, [Char])
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (Int, [Char]) -> Int
    forall a b. (a, b) -> a
    fst)
        ([(Int, [Char])] -> [(Int, [Char])])
    -> [(Int, [Char])] -> [(Int, [Char])]
    forall a b. (a -> b) -> a -> b
    $ [(Int, [Char])]
    cons' [(Int, [Char])] -> [(Int, [Char])] -> [(Int, [Char])]
    forall a. [a] -> [a] -> [a]
    ++ [(Int, [Char])]
    defs' [(Int, [Char])] -> [(Int, [Char])] -> [(Int, [Char])]
    forall a. [a] -> [a] -> [a]
    ++ [(Int, [Char])]
    icons' [(Int, [Char])] -> [(Int, [Char])] -> [(Int, [Char])]
    forall a. [a] -> [a] -> [a]
    ++ [(Int, [Char])]
    idefs'
        where
            cons' :: [(Int, [Char])]
    cons'  = [Char] -> [[[Char]]] -> [(Int, [Char])]
    foo [Char]
    "agdaConstructor"      ([[[Char]]] -> [(Int, [Char])]) -> [[[Char]]] -> [(Int, [Char])]
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> Int) -> [[Char]] -> [[[Char]]]
    forall {b} {a}. Ord b => (a -> b) -> [a] -> [[a]]
    classify [Char] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [[Char]]
    cons
            icons' :: [(Int, [Char])]
    icons' = [Char] -> [[[Char]]] -> [(Int, [Char])]
    foo [Char]
    "agdaInfixConstructor" ([[[Char]]] -> [(Int, [Char])]) -> [[[Char]]] -> [(Int, [Char])]
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> Int) -> [[Char]] -> [[[Char]]]
    forall {b} {a}. Ord b => (a -> b) -> [a] -> [[a]]
    classify [Char] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [[Char]]
    icons
            defs' :: [(Int, [Char])]
    defs'  = [Char] -> [[[Char]]] -> [(Int, [Char])]
    foo [Char]
    "agdaFunction"         ([[[Char]]] -> [(Int, [Char])]) -> [[[Char]]] -> [(Int, [Char])]
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> Int) -> [[Char]] -> [[[Char]]]
    forall {b} {a}. Ord b => (a -> b) -> [a] -> [[a]]
    classify [Char] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [[Char]]
    defs
            idefs' :: [(Int, [Char])]
    idefs' = [Char] -> [[[Char]]] -> [(Int, [Char])]
    foo [Char]
    "agdaInfixFunction"    ([[[Char]]] -> [(Int, [Char])]) -> [[[Char]]] -> [(Int, [Char])]
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> Int) -> [[Char]] -> [[[Char]]]
    forall {b} {a}. Ord b => (a -> b) -> [a] -> [[a]]
    classify [Char] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [[Char]]
    idefs

            classify :: (a -> b) -> [a] -> [[a]]
    classify a -> b
    f = (a -> a -> Bool) -> [a] -> [[a]]
    forall a. (a -> a -> Bool) -> [a] -> [[a]]
    List.groupBy (b -> b -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (b -> b -> Bool) -> (a -> b) -> a -> a -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` a -> b
    f)
                         ([a] -> [[a]]) -> ([a] -> [a]) -> [a] -> [[a]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> a -> Ordering) -> [a] -> [a]
    forall a. (a -> a -> Ordering) -> [a] -> [a]
    List.sortBy (b -> b -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (b -> b -> Ordering) -> (a -> b) -> a -> a -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` a -> b
    f)

            foo :: String -> [[String]] -> [(Int, String)]
            foo :: [Char] -> [[[Char]]] -> [(Int, [Char])]
    foo [Char]
    cat = ([[Char]] -> (Int, [Char])) -> [[[Char]]] -> [(Int, [Char])]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length ([Char] -> Int) -> ([[Char]] -> [Char]) -> [[Char]] -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [[Char]] -> [Char]
    forall a. [a] -> a
    head ([[Char]] -> Int)
    -> ([[Char]] -> [Char]) -> [[Char]] -> (Int, [Char])
    forall a b c. (a -> b) -> (a -> c) -> a -> (b, c)
    /\ [Char] -> [[Char]] -> [Char]
    match [Char]
    cat)

    toVim :: NamesInScope -> String
    toVim :: NamesInScope -> [Char]
    toVim NamesInScope
    ns = [[Char]] -> [Char]
    unlines ([[Char]] -> [Char]) -> [[Char]] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [[Char]]
    -> [[Char]]
    -> [[Char]]
    -> [[Char]]
    -> [[Char]]
    -> [[Char]]
    -> [[Char]]
    matches [[Char]]
    mcons [[Char]]
    micons [[Char]]
    mdefs [[Char]]
    midefs [[Char]]
    mflds [[Char]]
    miflds
        where
            cons :: [Name]
    cons = [ Name
    x | (Name
    x, AbstractName
    con:[AbstractName]
    _) <- NamesInScope -> [(Name, [AbstractName])]
    forall k a. Map k a -> [(k, a)]
    Map.toList NamesInScope
    ns, Maybe Induction -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe Induction -> Bool) -> Maybe Induction -> Bool
    forall a b. (a -> b) -> a -> b
    $ KindOfName -> Maybe Induction
    isConName (KindOfName -> Maybe Induction) -> KindOfName -> Maybe Induction
    forall a b. (a -> b) -> a -> b
    $ AbstractName -> KindOfName
    anameKind AbstractName
    con ]
            defs :: [Name]
    defs = [ Name
    x | (Name
    x, AbstractName
    def:[AbstractName]
    _) <- NamesInScope -> [(Name, [AbstractName])]
    forall k a. Map k a -> [(k, a)]
    Map.toList NamesInScope
    ns, KindOfName -> Bool
    isDefName (AbstractName -> KindOfName
    anameKind AbstractName
    def) ]
            flds :: [Name]
    flds = [ Name
    x | (Name
    x, AbstractName
    fld:[AbstractName]
    _) <- NamesInScope -> [(Name, [AbstractName])]
    forall k a. Map k a -> [(k, a)]
    Map.toList NamesInScope
    ns, AbstractName -> KindOfName
    anameKind AbstractName
    fld KindOfName -> KindOfName -> Bool
    forall a. Eq a => a -> a -> Bool
    == KindOfName
    FldName  ]

            mcons :: [[Char]]
    mcons = (Name -> [Char]) -> [Name] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [Name]
    cons
            mdefs :: [[Char]]
    mdefs = (Name -> [Char]) -> [Name] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [Name]
    defs
            mflds :: [[Char]]
    mflds = (Name -> [Char]) -> [Name] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow [Name]
    flds

            micons :: [[Char]]
    micons = (Name -> [[Char]]) -> [Name] -> [[Char]]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Name -> [[Char]]
    parts [Name]
    cons
            midefs :: [[Char]]
    midefs = (Name -> [[Char]]) -> [Name] -> [[Char]]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Name -> [[Char]]
    parts [Name]
    defs
            miflds :: [[Char]]
    miflds = (Name -> [[Char]]) -> [Name] -> [[Char]]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Name -> [[Char]]
    parts [Name]
    flds

            parts :: Name -> [[Char]]
    parts Name
    n
              | Name -> Bool
    isOperator Name
    n = ([Char] -> [Char]) -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map [Char] -> [Char]
    rawNameToString ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $ Name -> [[Char]]
    nameStringParts Name
    n
              | Bool
    otherwise    = []

    generateVimFile :: FilePath -> TCM ()
    generateVimFile :: [Char] -> TCM ()
    generateVimFile [Char]
    file = do
        ScopeInfo
    scope <- TCMT IO ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
        IO () -> TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCM ()) -> IO () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char] -> IO ()
    UTF8.writeFile ([Char] -> [Char]
    vimFile [Char]
    file) ([Char] -> IO ()) -> [Char] -> IO ()
    forall a b. (a -> b) -> a -> b
    $ NamesInScope -> [Char]
    toVim (NamesInScope -> [Char]) -> NamesInScope -> [Char]
    forall a b. (a -> b) -> a -> b
    $ ScopeInfo -> NamesInScope
    names ScopeInfo
    scope
        where
            names :: ScopeInfo -> NamesInScope
    names = NameSpace -> NamesInScope
    nsNames (NameSpace -> NamesInScope)
    -> (ScopeInfo -> NameSpace) -> ScopeInfo -> NamesInScope
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ScopeInfo -> NameSpace
    everythingInScope