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 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

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

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

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

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

match :: String -> [String] -> String
match :: FilePath -> [FilePath] -> FilePath
match FilePath
_ [] = FilePath
""
match FilePath
cat [FilePath]
ws    = FilePath
"syn match " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
cat FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
" \"" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                    [FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
List.intersperse FilePath
"\\|" ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ (FilePath -> FilePath) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath -> FilePath
wordBounded (FilePath -> FilePath)
-> (FilePath -> FilePath) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> FilePath
escape) [FilePath]
ws) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\""

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

        classify :: (a -> a) -> [a] -> [[a]]
classify a -> a
f = (a -> a -> Bool) -> [a] -> [[a]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
List.groupBy (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==) (a -> a -> Bool) -> (a -> a) -> a -> a -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> a
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 (a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (a -> a -> Ordering) -> (a -> a) -> a -> a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> a
f)

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

toVim :: NamesInScope -> String
toVim :: NamesInScope -> FilePath
toVim NamesInScope
ns = [FilePath] -> FilePath
unlines ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$ [FilePath]
-> [FilePath]
-> [FilePath]
-> [FilePath]
-> [FilePath]
-> [FilePath]
-> [FilePath]
matches [FilePath]
mcons [FilePath]
micons [FilePath]
mdefs [FilePath]
midefs [FilePath]
mflds [FilePath]
miflds
    where
        cons :: [Name]
cons = [ Name
x | (Name
x, AbstractName
def:[AbstractName]
_) <- NamesInScope -> [(Name, [AbstractName])]
forall k a. Map k a -> [(k, a)]
Map.toList NamesInScope
ns, AbstractName -> KindOfName
anameKind AbstractName
def KindOfName -> KindOfName -> Bool
forall a. Eq a => a -> a -> Bool
== KindOfName
ConName ]
        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 :: [FilePath]
mcons = (Name -> FilePath) -> [Name] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map Name -> FilePath
forall a. Show a => a -> FilePath
show [Name]
cons
        mdefs :: [FilePath]
mdefs = (Name -> FilePath) -> [Name] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map Name -> FilePath
forall a. Show a => a -> FilePath
show [Name]
defs
        mflds :: [FilePath]
mflds = (Name -> FilePath) -> [Name] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map Name -> FilePath
forall a. Show a => a -> FilePath
show [Name]
flds

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

        parts :: Name -> [FilePath]
parts (NoName Range
_ NameId
_)    = []
        parts (Name Range
_ NameInScope
_ [NamePart
_])  = []
        parts (Name Range
_ NameInScope
_ [NamePart]
ps)   = [ FilePath -> FilePath
rawNameToString FilePath
x | Id FilePath
x <- [NamePart]
ps ]

generateVimFile :: FilePath -> TCM ()
generateVimFile :: FilePath -> TCM ()
generateVimFile FilePath
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
$ FilePath -> FilePath -> IO ()
UTF8.writeFile (FilePath -> FilePath
vimFile FilePath
file) (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ NamesInScope -> FilePath
toVim (NamesInScope -> FilePath) -> NamesInScope -> FilePath
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