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 = 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 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 = 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 " forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
unwords ([Char]
cat 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 "
    forall a. [a] -> [a] -> [a]
++ [Char]
cat
    forall a. [a] -> [a] -> [a]
++ [Char]
" \""
    forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"\\|" (forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> [Char]
wordBounded forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [Char]
escape) [[Char]]
ws)
    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 =
    forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd
    forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst)
    forall a b. (a -> b) -> a -> b
$ [(Int, [Char])]
cons' forall a. [a] -> [a] -> [a]
++ [(Int, [Char])]
defs' forall a. [a] -> [a] -> [a]
++ [(Int, [Char])]
icons' forall a. [a] -> [a] -> [a]
++ [(Int, [Char])]
idefs'
    where
        cons' :: [(Int, [Char])]
cons'  = [Char] -> [[[Char]]] -> [(Int, [Char])]
foo [Char]
"agdaConstructor"      forall a b. (a -> b) -> a -> b
$ forall {b} {a}. Ord b => (a -> b) -> [a] -> [[a]]
classify forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Char]]
cons
        icons' :: [(Int, [Char])]
icons' = [Char] -> [[[Char]]] -> [(Int, [Char])]
foo [Char]
"agdaInfixConstructor" forall a b. (a -> b) -> a -> b
$ forall {b} {a}. Ord b => (a -> b) -> [a] -> [[a]]
classify forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Char]]
icons
        defs' :: [(Int, [Char])]
defs'  = [Char] -> [[[Char]]] -> [(Int, [Char])]
foo [Char]
"agdaFunction"         forall a b. (a -> b) -> a -> b
$ forall {b} {a}. Ord b => (a -> b) -> [a] -> [[a]]
classify forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Char]]
defs
        idefs' :: [(Int, [Char])]
idefs' = [Char] -> [[[Char]]] -> [(Int, [Char])]
foo [Char]
"agdaInfixFunction"    forall a b. (a -> b) -> a -> b
$ forall {b} {a}. Ord b => (a -> b) -> [a] -> [[a]]
classify forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Char]]
idefs

        classify :: (a -> b) -> [a] -> [[a]]
classify a -> b
f = forall a. (a -> a -> Bool) -> [a] -> [[a]]
List.groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> b
f)
                     forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy (forall a. Ord a => a -> a -> Ordering
compare 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 = forall a b. (a -> b) -> [a] -> [b]
map (forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
head 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 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]
_) <- forall k a. Map k a -> [(k, a)]
Map.toList NamesInScope
ns, forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ KindOfName -> Maybe Induction
isConName forall a b. (a -> b) -> a -> b
$ AbstractName -> KindOfName
anameKind AbstractName
con ]
        defs :: [Name]
defs = [ Name
x | (Name
x, AbstractName
def:[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]
_) <- forall k a. Map k a -> [(k, a)]
Map.toList NamesInScope
ns, AbstractName -> KindOfName
anameKind AbstractName
fld forall a. Eq a => a -> a -> Bool
== KindOfName
FldName  ]

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

        micons :: [[Char]]
micons = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Name -> [[Char]]
parts [Name]
cons
        midefs :: [[Char]]
midefs = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Name -> [[Char]]
parts [Name]
defs
        miflds :: [[Char]]
miflds = 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 = forall a b. (a -> b) -> [a] -> [b]
map [Char] -> [Char]
rawNameToString 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 <- forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> IO ()
UTF8.writeFile ([Char] -> [Char]
vimFile [Char]
file) forall a b. (a -> b) -> a -> b
$ NamesInScope -> [Char]
toVim forall a b. (a -> b) -> a -> b
$ ScopeInfo -> NamesInScope
names ScopeInfo
scope
    where
        names :: ScopeInfo -> NamesInScope
names = NameSpace -> NamesInScope
nsNames forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeInfo -> NameSpace
everythingInScope