{-# 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 = 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 -> List1 String -> String
match :: [Char] -> List1 [Char] -> [Char]
match [Char]
cat ([Char]
w :| [[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) forall a b. (a -> b) -> a -> b
$ [Char]
wforall a. a -> [a] -> [a]
:[[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] -> [List1 [Char]] -> [(Int, [Char])]
foo [Char]
"agdaConstructor"      forall a b. (a -> b) -> a -> b
$ forall {b} {a}. Ord b => (a -> b) -> [a] -> [NonEmpty a]
classify forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Char]]
cons
        icons' :: [(Int, [Char])]
icons' = [Char] -> [List1 [Char]] -> [(Int, [Char])]
foo [Char]
"agdaInfixConstructor" forall a b. (a -> b) -> a -> b
$ forall {b} {a}. Ord b => (a -> b) -> [a] -> [NonEmpty a]
classify forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Char]]
icons
        defs' :: [(Int, [Char])]
defs'  = [Char] -> [List1 [Char]] -> [(Int, [Char])]
foo [Char]
"agdaFunction"         forall a b. (a -> b) -> a -> b
$ forall {b} {a}. Ord b => (a -> b) -> [a] -> [NonEmpty a]
classify forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Char]]
defs
        idefs' :: [(Int, [Char])]
idefs' = [Char] -> [List1 [Char]] -> [(Int, [Char])]
foo [Char]
"agdaInfixFunction"    forall a b. (a -> b) -> a -> b
$ forall {b} {a}. Ord b => (a -> b) -> [a] -> [NonEmpty a]
classify forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Char]]
idefs

        classify :: (a -> b) -> [a] -> [NonEmpty a]
classify a -> b
f = forall (f :: * -> *) a.
Foldable f =>
(a -> a -> Bool) -> f a -> [NonEmpty a]
List1.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 -> [List1 String] -> [(Int, String)]
        foo :: [Char] -> [List1 [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. NonEmpty a -> a
List1.head 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 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