{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeInType #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.Symantic.Typing.Document where

import Data.Function (id)
import Data.Map.Strict (Map)
import Data.Maybe (fromMaybe)
import Data.Monoid (Monoid(..))
import Data.Semigroup (Semigroup(..))
import Data.Set (Set)
import Data.Text (Text)
import Data.Typeable
import qualified Data.List as L
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import qualified Data.Text as T
import qualified Symantic.Document as Doc

import Language.Symantic.Grammar
import Language.Symantic.Typing.Kind
import Language.Symantic.Typing.Variable
import Language.Symantic.Typing.Module
import Language.Symantic.Typing.Type

-- * Type 'Config_Doc_Type'
data Config_Doc_Type
 =   Config_Doc_Type
 {   config_Doc_Type_vars_numbering :: Bool
     -- ^ Style of /type variables/:
     --
     -- * if 'True': use name and position (as in @a0@ then @a1@)
     -- * if 'False': use name, and a counter when names collide (as in @a@ then @a1@)
     --
     -- NOTE: if the name is empty, a 'freshName' is taken from 'poolNames'.
 ,   config_Doc_Type_imports :: Imports NameTy
 }

config_Doc_Type :: Config_Doc_Type
config_Doc_Type =
        Config_Doc_Type
         { config_Doc_Type_vars_numbering = True
         , config_Doc_Type_imports        = mempty
         }

-- * Document 'Type'
docType ::
 forall src vs t d.
 Semigroup d =>
 Doc.From (Doc.Word Char) d =>
 Doc.From (Doc.Word Text) d =>
 Doc.Spaceable d =>
 Doc.Colorable16 d =>
 Config_Doc_Type ->
 Precedence ->
 Type src vs t -> d
docType conf@Config_Doc_Type{config_Doc_Type_imports=imps} pr ty =
        let (v2n, _) = var2Name conf mempty ty in
        go v2n (infixB SideL pr, SideL) ty
        where
        go ::
         forall kx (x::kx).
         Map IndexVar Name -> -- names of variables
         (Infix, Side) ->
         Type src vs x -> d
        -- Var
        go v2n _po (TyVar _src _n v) =
                let iv = indexVar v in
                case Map.lookup iv v2n of
                 Nothing -> error "[BUG] docType: variable name missing"
                 Just n -> Doc.from (Doc.Word n)
        -- Const
        go _v2n _po (TyConst _src _vs c@Const{}) =
                (if isNameTyOp c then docParen else id) $
                docConst imps c
        -- [] Const
        go v2n _po (TyApp _ (TyConst _ _ f@Const{}) a)
         | Just HRefl <- proj_ConstKi @(K []) @[] f =
                Doc.between (Doc.from (Doc.Word '[')) (Doc.from (Doc.Word ']')) $
                go v2n (infixB SideL 0, SideL) a
        -- Infix Const
        go v2n po (TyApp _ (TyApp _ (TyConst _ _ f@Const{}) a) b)
         -- () =>
         | Just HRefl <- proj_ConstKiTy @Constraint @(()::Constraint) a
         , Just HRefl <- proj_ConstKi @(K (#>)) @(#>) f =
                go v2n po b
         | Just (Fixity2 op) <- fixityOf f =
                (if isPairNeeded po op then docParen else id) $
                go v2n (op, SideL) a <>
                prettyConst f <>
                go v2n (op, SideR) b
                where
                d_op :: Text -> d
                d_op = Doc.yellower . Doc.from . Doc.Word
                prettyConst :: forall k c. Const src (c::k) -> d
                prettyConst c | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c = Doc.space <> d_op "=>" <> Doc.space
                prettyConst c | Just HRefl <- proj_ConstKi @(K (#))  @(#)  c = d_op "," <> Doc.space
                prettyConst c | Just HRefl <- proj_ConstKi @(K (,))  @(,)  c = d_op "," <> Doc.space
                prettyConst c@Const{}
                 | r <- typeRepTyCon (typeRep c)
                 , tyConName   r =="#~"
                 , tyConModule r =="Language.Symantic.Typing.Type"
                 -- XXX: module name must be in sync with where (#~) is defined.
                 -- NOTE: cannot use 'proj_ConstKi' here
                 -- because (#~) has a polymorphic kind.
                 = Doc.space <> d_op "~" <> Doc.space
                 | otherwise = Doc.space <> d_op (docConst imps c) <> Doc.space
        -- TyApp
        go v2n po (TyApp _src f a) =
                let op = infixL 11 in
                (if isPairNeeded po op then docParen else id) $
                go v2n (op, SideL) f <>
                Doc.space <>
                go v2n (op, SideR) a
        -- TyFam
        go v2n po (TyFam _src _len fam args) =
                let op = infixL 11 in
                (if isPairNeeded po op then docParen else id) $
                docConst imps fam <>
                foldlTys (\t acc ->
                        Doc.space <> go v2n (op, SideL) t <> acc
                 ) args mempty

-- | Return a 'Map' associating a distinct 'Name'
-- for all the variables of the given 'Type'.
var2Name ::
 Config_Doc_Type ->
 (Map IndexVar Name, Names) ->
 Type src vs t ->
 (Map IndexVar Name, Names)
var2Name _cfg st TyConst{} = st
var2Name cfg st@(v2n, ns) (TyVar _src (NameVar n) v) =
        let iv = indexVar v in
        case Map.lookup iv v2n of
         Just{} -> st
         Nothing ->
                let n' =
                        if config_Doc_Type_vars_numbering cfg && not (T.null n)
                        then n <> T.pack (show iv)
                        else freshifyName ns n in
                let v2n' = Map.insert iv n' v2n in
                let ns'  = Set.insert n' ns in
                (v2n', ns')
var2Name cfg st (TyApp _src f a) = var2Name cfg (var2Name cfg st f) a
var2Name cfg st (TyFam _src _len _fam as) = foldlTys (flip $ var2Name cfg) as st

-- ** Type 'Names'
type Names = Set Name

-- | Return given 'Name' renamed a bit to avoid
-- conflicting with any given 'Names'.
freshifyName :: Names -> Name -> Name
freshifyName ns "" = freshName ns
freshifyName ns n =
        let ints = [1..] :: [Int] in
        L.head
         [ fresh
         | suffix <- "" : (show <$> ints)
         , fresh <- [n <> T.pack suffix]
         , fresh `Set.notMember` ns
         ]

freshName :: Names -> Name
freshName ns = L.head $ poolNames L.\\ Set.toList ns

-- | Infinite list of unique 'Name's:
-- @a, b, .., z, a1, b1 .., z1, a2, ..@
poolNames :: [Name]
poolNames =
        [ T.singleton n     | n <- ['a'..'z'] ] <>
        [ T.pack (n:show i) | n <- ['a'..'z']
                            , i <- [1 :: Int ..] ]

-- * Document 'Types'
docTypes ::
 forall src vs ts d.
 Semigroup d =>
 Doc.From (Doc.Word Char) d =>
 Doc.From (Doc.Word Text) d =>
 Doc.Spaceable d =>
 Doc.Colorable16 d =>
 Config_Doc_Type ->
 Types src vs ts -> d
docTypes conf tys =
        d_op (Doc.from (Doc.Word '[')) <> go tys <> d_op (Doc.from (Doc.Word ']'))
        where
        d_op = Doc.yellower
        go :: forall xs. Types src vs xs -> d
        go TypesZ = mempty
        go (TypesS t0 (TypesS t1 ts)) =
                docType conf 10 t0 <>
                d_op (Doc.from (Doc.Word ',')) <> Doc.space <>
                docType conf 10 t1 <>
                go ts
        go (TypesS t ts) = docType conf 10 t <> go ts

-- * Document 'Const'
docConst ::
 Monoid d =>
 Doc.From (Doc.Word Char) d =>
 Doc.From (Doc.Word Text) d =>
 Imports NameTy -> Const src c -> d
docConst imps c@Const{} =
        docMod docNameTy $
        maybe mn (`Mod` n) $
        revlookupImports f (m `Mod` n) imps
        where
        f = fixyOfFixity $ Fixity2 infixN5 `fromMaybe` fixityOf c
        mn@(m `Mod` n) = nameTyOf c

-- * Document 'NameTy'
docNameTy :: Doc.From (Doc.Word Text) d => NameTy -> d
docNameTy (NameTy t) = Doc.from (Doc.Word t)

-- * Document 'Mod'
docMod ::
 Monoid d =>
 Doc.From (Doc.Word Char) d =>
 Doc.From (Doc.Word Text) d =>
 (a -> d) -> Mod a -> d
docMod a2d ([] `Mod` a) = a2d a
docMod a2d (m `Mod`  a) = docPathMod m <> (Doc.from (Doc.Word '.')) <> a2d a

-- * Document 'PathMod'
docPathMod ::
 Monoid d =>
 Doc.From (Doc.Word Char) d =>
 Doc.From (Doc.Word Text) d =>
 PathMod -> d
docPathMod (p::PathMod) =
        mconcat $
        L.intersperse (Doc.from (Doc.Word '.')) $
        (\(NameMod n) -> Doc.from (Doc.Word n)) <$> p

docParen :: Doc.Spaceable d => Doc.From (Doc.Word Char) d => d -> d
docParen = Doc.between (Doc.from (Doc.Word '(')) (Doc.from (Doc.Word ')'))

{-
docModules ::
 Source src =>
 Doc.Textable d =>
 Doc.Colorable16 d =>
 Doc.Decorationable d =>
 ReadTe src ss =>
 Sym.Modules src ss -> d
docModules (Sym.Modules mods) =
	Map.foldrWithKey
	 (\p m doc -> docModule p m <> doc)
	 mempty
	 mods

docModule ::
 forall src ss d.
 Source src =>
 Doc.Textable d =>
 Doc.Colorable16 d =>
 Doc.Decorationable d =>
 ReadTe src ss =>
 Sym.PathMod -> Sym.Module src ss -> d
docModule m Sym.Module
 { Sym.module_infix
 , Sym.module_prefix
 , Sym.module_postfix
 } =
	go docFixityInfix   module_infix <>
	go docFixityPrefix  module_prefix <>
	go docFixityPostfix module_postfix
	where
	go :: (fixy -> d) -> ModuleFixy src ss fixy -> d
	go docFixy =
		Map.foldrWithKey
		 (\n Sym.Tokenizer
			 { Sym.token_fixity
			 , Sym.token_term = t
			 } doc ->
			docPathTe m n <>
			docFixy token_fixity <>
			Doc.space <> Doc.bold (Doc.yellower "::") <> Doc.space <>
			docTokenTerm (t Sym.noSource) <>
			Doc.eol <> doc)
		 mempty

docTokenTerm ::
 forall src ss d.
 Source src =>
 Doc.Textable d =>
 Doc.Colorable16 d =>
 ReadTe src ss =>
 Sym.Token_Term src ss -> d
docTokenTerm t =
	let n2t = name2typeInj @ss in
	case Sym.readTerm n2t CtxTyZ (G.BinTree0 t) of
	 Left{} -> error "[BUG] docTokenTerm: readTerm failed"
	 Right (Sym.TermVT te) ->
		Sym.docType Sym.config_doc_type
		 { config_Doc_Type_vars_numbering = False
		 } 0 $ Sym.typeOfTerm te

docFixityInfix :: (Doc.Decorationable t, Doc.Colorable16 t, Doc.Textable t) => Infix -> t
docFixityInfix = \case
	 Sym.Infix Nothing 5 -> mempty
	 Sym.Infix a p ->
		let docAssoc = \case
			 Sym.AssocL -> "l"
			 Sym.AssocR -> "r"
			 Sym.AssocB Sym.SideL -> "l"
			 Sym.AssocB Sym.SideR -> "r" in
		Doc.magenta $ " infix" <> maybe mempty docAssoc a <>
		Doc.space <> Doc.bold (Doc.bluer (Doc.int p))
docFixityPrefix :: (Doc.Decorationable t, Doc.Colorable16 t, Doc.Textable t) => Unifix -> t
docFixityPrefix p = Doc.magenta $ " prefix "  <> Doc.bold (Doc.bluer (Doc.int $ Sym.unifix_prece p))
docFixityPostfix :: (Doc.Decorationable t, Doc.Colorable16 t, Doc.Textable t) => Unifix -> t
docFixityPostfix p = Doc.magenta $ " postfix " <> Doc.bold (Doc.bluer (Doc.int $ Sym.unifix_prece p))

docPathTe ::
 Doc.Textable d =>
 Doc.Colorable16 d =>
 Sym.PathMod -> Sym.NameTe -> d
docPathTe (ms::Sym.PathMod) (Sym.NameTe n) =
	Doc.catH $
	L.intersperse (Doc.charH '.') $
	((\(Sym.NameMod m) -> Doc.textH m) <$> ms) <>
	[(if isOp n then id else Doc.yellower) $ Doc.text n]
	where
	isOp = T.all $ \case '_' -> True; '\'' -> True; c -> Char.isAlphaNum c
-}