{-# 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 = (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 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 ([[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
    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