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 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 -> [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 a. [a] -> 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 a. [a] -> 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 a. [a] -> 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 a. [a] -> 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 a. [a] -> 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. HasCallStack => [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 a. IO a -> TCMT IO a
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