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

import Data.Function (id)
import Data.Map.Strict (Map)
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 Language.Symantic.Document as D
import Language.Symantic.Grammar
import Language.Symantic.Typing.Kind
import Language.Symantic.Typing.Variable
import Language.Symantic.Typing.Type

-- * Type 'Config_Doc_Type'
newtype 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 :: Config_Doc_Type
config_doc_type =
	Config_Doc_Type
	 { config_Doc_Type_vars_numbering = True }

docType ::
 forall src vs t d.
 Semigroup d =>
 D.Doc_Text d =>
 D.Doc_Color d =>
 Config_Doc_Type ->
 Precedence ->
 Type src vs t -> d
docType conf pr ty =
	let (v2n, _) = var2Name conf mempty ty in
	go v2n (infixB SideL pr, SideL) ty
	where
	go ::
	 forall x.
	 (Map IndexVar Name) -> -- names of variables
	 (Infix, Side) ->
	 Type src vs x -> d
	go _v2n _po c
	 | Just HRefl <- proj_ConstKiTy @Constraint @() c = D.textH "()"
	go _v2n _po (TyConst _src _vs c) = D.stringH $ show c
	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 -> D.textH n
	go v2n _po (TyApp _ (TyConst _ _ f@Const{}) a)
	 | Just HRefl <- proj_ConstKi @(K []) @[] f =
		"[" <> go v2n (infixB SideL 0, SideL) a <> "]"
	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 needsParenInfix po op then D.paren else id) $
		go v2n (op, SideL) a <>
		prettyConst f <>
		go v2n (op, SideR) b
		where
		d_op = D.yellower
		unParen ('(':s) | ')':s' <- reverse s = reverse s'
		unParen s = s
		prettyConst :: forall k c. Const src (c::k) -> d
		prettyConst c | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c = D.space <> d_op "=>" <> D.space
		prettyConst c | Just HRefl <- proj_ConstKi @(K (#))  @(#)  c = d_op "," <> D.space
		prettyConst c | Just HRefl <- proj_ConstKi @(K (,))  @(,)  c = d_op "," <> D.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.
		 = D.space <> d_op "~" <> D.space
		 | otherwise = D.space <> d_op (D.stringH $ unParen $ show c) <> D.space
	go v2n po (TyApp _src f a) =
		let op = infixL 11 in
		(if needsParenInfix po op then D.paren else id) $
		go v2n (op, SideL) f <>
		D.space <>
		go v2n (op, SideR) a
	go v2n po (TyFam _src _len fam args) =
		let op = infixL 11 in
		(if needsParenInfix po op then D.paren else id) $
		D.stringH (show fam) <>
		foldlTys (\t acc ->
			D.space <> go v2n (op, SideL) t <> acc
		 ) args D.empty

docTypes ::
 forall src vs ts d.
 Semigroup d =>
 D.Doc_Text d =>
 D.Doc_Color d =>
 Config_Doc_Type ->
 Types src vs ts -> d
docTypes conf tys =
	d_op (D.charH '[') <> go tys <> d_op (D.charH ']')
	where
	d_op = D.yellower
	go :: forall xs. Types src vs xs -> d
	go TypesZ = D.empty
	go (TypesS t0 (TypesS t1 ts)) =
		docType conf 10 t0 <>
		d_op (D.charH ',') <> D.space <>
		docType conf 10 t1 <>
		go ts
	go (TypesS t ts) = docType conf 10 t <> go ts

-- | 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 'Name'
type Name     = Text
type NameHint = Name
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 ..] ]