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

import Data.Map.Strict (Map)
import Data.Semigroup ((<>))
import Data.Set (Set)
import Data.Text (Text)
import Data.Typeable
import qualified Data.List as List
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import qualified Data.Text as Text

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

-- * Type 'Config_showType'
data Config_showType
 =   Config_showType
 {   config_showType_vars_numbering :: Bool
 }

config_showType :: Config_showType
config_showType =
	Config_showType
	 { config_showType_vars_numbering = True }

showType :: Config_showType -> Int -> Type src vs t -> String
showType conf pr ty = showTypeS conf pr ty ""

showTypeS :: forall src vs t. Config_showType -> Int -> Type src vs t -> ShowS
showTypeS conf pr ty =
	let (v2n, _) = varNames 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 ->
	 ShowS
	go _v2n _po c
	 | Just HRefl <- proj_ConstKiTy @Constraint @() c = showString "()"
	go _v2n _po (TyConst _src _vs c) = showsPrec 11 c
	go v2n _po (TyVar _src _n v) =
		let iv = indexVar v in
		case Map.lookup iv v2n of
		 Nothing -> error "[BUG] showsPrec @Type: variable name missing"
		 Just n -> showString $ Text.unpack n
	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
	 | Fixity2 op <- fixityOf f =
		showParen (needsParenInfix po op) $
		go v2n (op, SideL) a .
		showString (prettyConst f) .
		go v2n (op, SideR) b
		where
		prettyConst :: forall k c. Const src (c::k) -> String
		prettyConst c | Just HRefl <- proj_ConstKi @(K (#>)) @(#>) c = " => "
		prettyConst c | Just HRefl <- proj_ConstKi @(K (#)) @(#) c = ", "
		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.
		 = " ~ "
		 | otherwise = ' ' : unParen (show c) ++ " "
		unParen ('(':s) | ')':s' <- reverse s = reverse s'
		unParen s = s
	go v2n po (TyApp _src f a) =
		let op = infixR 11 in
		showParen (needsParenInfix po op) $
		go v2n (op, SideL) f .
		showChar ' ' .
		go v2n (op, SideR) a
	go v2n po (TyFam _src _len fam args) =
		let op = infixL 11 in
		showParen (needsParenInfix po op) $
		showsPrec 11 fam .
		foldlTys (\t acc ->
			showChar ' ' . go v2n (op, SideL) t . acc
		 ) args id
	
	-- | Return a 'Map' associating a distinct 'Name'
	-- for all the variables of the given 'Type'.
	varNames ::
	 forall x.
	 Config_showType ->
	 (Map IndexVar Name, Names) ->
	 Type src vs x ->
	 (Map IndexVar Name, Names)
	varNames _cfg st TyConst{} = st
	varNames 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_showType_vars_numbering cfg
				then n <> Text.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')
	varNames cfg st (TyApp _src f a) = varNames cfg (varNames cfg st f) a
	varNames cfg st (TyFam _src _len _fam as) = foldlTys (flip $ varNames cfg) as st

instance Source src => Show (Type src vs t) where
	showsPrec = showTypeS config_showType
instance Source src => Show (TypeK src vs kt) where
	showsPrec p (TypeK t) = showsPrec p t
instance Source src => Show (TypeVT src) where
	showsPrec p (TypeVT t) = showsPrec p t
instance Source src => Show (TypeT src vs) where
	showsPrec p (TypeT t) = showsPrec p t
instance Source src => Show (Types src vs ts) where
	showsPrec _p tys = showString "[" . go tys . showString "]"
		where
		go :: forall xs. Types src vs xs -> ShowS
		go TypesZ = showString ""
		go (TypesS t0 (TypesS t1 ts)) = showsPrec 10 t0 . showString ", " . showsPrec 10 t1 . go ts
		go (TypesS t ts) = showsPrec 10 t . go ts

showBracket :: Bool -> ShowS -> ShowS
showBracket b p =  if b then showChar '{' . p . showChar '}' else p

-- ** 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
	List.head
	 [ fresh
	 | suffix <- "" : (show <$> ints)
	 , fresh <- [n <> Text.pack suffix]
	 , fresh `Set.notMember` ns
	 ]

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

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