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 :: 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] -> FilePath
forall a. [a] -> [[a]] -> [a]
List.intercalate FilePath
"\\|" ((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

        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
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 :: [FilePath]
mcons = (Name -> FilePath) -> [Name] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map Name -> FilePath
forall a. Pretty a => a -> FilePath
prettyShow [Name]
cons
        mdefs :: [FilePath]
mdefs = (Name -> FilePath) -> [Name] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map Name -> FilePath
forall a. Pretty a => a -> FilePath
prettyShow [Name]
defs
        mflds :: [FilePath]
mflds = (Name -> FilePath) -> [Name] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map Name -> FilePath
forall a. Pretty a => a -> FilePath
prettyShow [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 Name
n
          | Name -> Bool
isOperator Name
n = (FilePath -> FilePath) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> FilePath
rawNameToString ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ Name -> [FilePath]
nameStringParts Name
n
          | Bool
otherwise    = []

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