    {-# OPTIONS_GHC -Wunused-imports #-}

    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 Agda.Utils.List1             ( List1, pattern (:|) )
    import qualified Agda.Utils.List1   as List1
    import qualified Agda.Utils.IO.UTF8 as UTF8
    import Agda.Utils.Tuple
    import Agda.Syntax.Common.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 a. Eq a => a -> [a] -> 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 -> List1 String -> String
    match :: [Char] -> List1 [Char] -> [Char]
    match [Char]
    cat ([Char]
    w :| [[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]] -> [[Char]]) -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $ [Char]
    w[Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    :[[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] -> [List1 [Char]] -> [(Int, [Char])]
    foo [Char]
    "agdaConstructor"      ([List1 [Char]] -> [(Int, [Char])])
    -> [List1 [Char]] -> [(Int, [Char])]
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> Int) -> [[Char]] -> [List1 [Char]]
    forall {b} {a}. Ord b => (a -> b) -> [a] -> [NonEmpty a]
    classify [Char] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [[Char]]
    cons
            icons' :: [(Int, [Char])]
    icons' = [Char] -> [List1 [Char]] -> [(Int, [Char])]
    foo [Char]
    "agdaInfixConstructor" ([List1 [Char]] -> [(Int, [Char])])
    -> [List1 [Char]] -> [(Int, [Char])]
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> Int) -> [[Char]] -> [List1 [Char]]
    forall {b} {a}. Ord b => (a -> b) -> [a] -> [NonEmpty a]
    classify [Char] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [[Char]]
    icons
            defs' :: [(Int, [Char])]
    defs'  = [Char] -> [List1 [Char]] -> [(Int, [Char])]
    foo [Char]
    "agdaFunction"         ([List1 [Char]] -> [(Int, [Char])])
    -> [List1 [Char]] -> [(Int, [Char])]
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> Int) -> [[Char]] -> [List1 [Char]]
    forall {b} {a}. Ord b => (a -> b) -> [a] -> [NonEmpty a]
    classify [Char] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [[Char]]
    defs
            idefs' :: [(Int, [Char])]
    idefs' = [Char] -> [List1 [Char]] -> [(Int, [Char])]
    foo [Char]
    "agdaInfixFunction"    ([List1 [Char]] -> [(Int, [Char])])
    -> [List1 [Char]] -> [(Int, [Char])]
    forall a b. (a -> b) -> a -> b
    $ ([Char] -> Int) -> [[Char]] -> [List1 [Char]]
    forall {b} {a}. Ord b => (a -> b) -> [a] -> [NonEmpty a]
    classify [Char] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [[Char]]
    idefs

            classify :: (a -> b) -> [a] -> [NonEmpty a]
    classify a -> b
    f = (a -> a -> Bool) -> [a] -> [NonEmpty a]
    forall (f :: * -> *) a.
    Foldable f =>
    (a -> a -> Bool) -> f a -> [NonEmpty a]
    List1.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] -> [NonEmpty a]) -> ([a] -> [a]) -> [a] -> [NonEmpty 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 -> [List1 String] -> [(Int, String)]
            foo :: [Char] -> [List1 [Char]] -> [(Int, [Char])]
    foo [Char]
    cat = (List1 [Char] -> (Int, [Char]))
    -> [List1 [Char]] -> [(Int, [Char])]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Char] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length ([Char] -> Int) -> (List1 [Char] -> [Char]) -> List1 [Char] -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 [Char] -> [Char]
    forall a. NonEmpty a -> a
    List1.head (List1 [Char] -> Int)
    -> (List1 [Char] -> [Char]) -> List1 [Char] -> (Int, [Char])
    forall a b c. (a -> b) -> (a -> c) -> a -> (b, c)
    /\ [Char] -> List1 [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, List1 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, List1 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, List1 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
        scope <- TCMT IO ScopeInfo
    forall (m :: * -> *). ReadTCState m => m ScopeInfo
    getScope
        liftIO $ UTF8.writeFile (vimFile file) $ toVim $ names 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