{-# 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.Abstract.Name (AbstractName(..), KindOfName (FldName))
import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty
import Agda.Syntax.Concrete.Name as CName
import Agda.Syntax.Scope.Base

import Agda.TypeChecking.Monad

import Agda.Utils.IO.UTF8 qualified as UTF8
import Agda.Utils.List1 ( List1, pattern (:|) )
import Agda.Utils.List1 qualified as List1
import Agda.Utils.Tuple

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

        classify :: (a -> b) -> [a] -> [NonEmpty a]
classify a -> b
f = (a -> a -> Bool) -> [a] -> [NonEmpty a]
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> Bool) -> f a -> [NonEmpty a]
List1.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] -> [NonEmpty a]) -> ([a] -> [a]) -> [a] -> [NonEmpty 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 -> [List1 String] -> [(Int, String)]
        foo :: [Char] -> [List1 [Char]] -> [(Int, [Char])]
foo [Char]
cat = (List1 [Char] -> (Int, [Char]))
-> [List1 [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) -> (List1 [Char] -> [Char]) -> List1 [Char] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. List1 [Char] -> [Char]
forall a. NonEmpty a -> a
List1.head (List1 [Char] -> Int)
-> (List1 [Char] -> [Char]) -> List1 [Char] -> (Int, [Char])
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& [Char] -> List1 [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, List1 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, List1 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, List1 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
    scope <- TCMT IO ScopeInfo
forall (m :: * -> *). ReadTCState m => m ScopeInfo
getScope
    liftIO $ UTF8.writeFile (vimFile file) $ toVim $ names 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