{-# OPTIONS_GHC -Wunused-imports #-}

module Mikan.Interaction.Highlighting.Vim where

import Control.Monad.Trans

import Data.Function ( on )
import Data.List qualified as List
import Data.Map qualified as Map
import Data.Maybe
import Data.Text.Short qualified as TS

import System.FilePath

import Mikan.Syntax.Abstract.Name (AbstractName(..), KindOfName (FldName))
import Mikan.Syntax.Common
import Mikan.Syntax.Common.Pretty
import Mikan.Syntax.Concrete.Name as CName
import Mikan.Syntax.Scope.Base

import Mikan.TypeChecking.Monad

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

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 (ShortText -> [Char]
TS.unpack (ShortText -> [Char]) -> [ShortText] -> [[Char]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ShortText]
micons) [[Char]]
mdefs (ShortText -> [Char]
TS.unpack (ShortText -> [Char]) -> [ShortText] -> [[Char]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ShortText]
midefs) [[Char]]
mflds (ShortText -> [Char]
TS.unpack (ShortText -> [Char]) -> [ShortText] -> [[Char]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ShortText]
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 :: [ShortText]
micons = (Name -> [ShortText]) -> [Name] -> [ShortText]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Name -> [ShortText]
parts [Name]
cons
        midefs :: [ShortText]
midefs = (Name -> [ShortText]) -> [Name] -> [ShortText]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Name -> [ShortText]
parts [Name]
defs
        miflds :: [ShortText]
miflds = (Name -> [ShortText]) -> [Name] -> [ShortText]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Name -> [ShortText]
parts [Name]
flds

        parts :: Name -> [ShortText]
parts Name
n
          | Name -> Bool
isOperator Name
n = (ShortText -> ShortText) -> [ShortText] -> [ShortText]
forall a b. (a -> b) -> [a] -> [b]
map ShortText -> ShortText
rawNameToString ([ShortText] -> [ShortText]) -> [ShortText] -> [ShortText]
forall a b. (a -> b) -> a -> b
$ Name -> [ShortText]
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