{-# 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 Symantic.Document (DocFrom(..))
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 =>
 DocFrom (Doc.Word Char) d =>
 DocFrom (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 -> docFrom (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 (docFrom (Doc.Word '[')) (docFrom (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 . docFrom . 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 =>
 DocFrom (Doc.Word Char) d =>
 DocFrom (Doc.Word Text) d =>
 Doc.Spaceable d =>
 Doc.Colorable16 d =>
 Config_Doc_Type ->
 Types src vs ts -> d
docTypes conf tys =
	d_op (docFrom (Doc.Word '[')) <> go tys <> d_op (docFrom (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 (docFrom (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 =>
 DocFrom (Doc.Word Char) d =>
 DocFrom (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 :: DocFrom (Doc.Word Text) d => NameTy -> d
docNameTy (NameTy t) = docFrom (Doc.Word t)

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

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

docParen :: Doc.Spaceable d => DocFrom (Doc.Word Char) d => d -> d
docParen = Doc.between (docFrom (Doc.Word '(')) (docFrom (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
-}