{-# 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 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.Constant
import Language.Symantic.Typing.Type
import Language.Symantic.Typing.Quantification

showTy :: forall src ctx ss cs h.
 Show_TyConst cs
 => Fixity_TyConst cs
 => Int -> Type src ctx ss cs h -> ShowS
showTy pr typ =
	go Nothing
	 (infixB L pr, L)
	 (freeTyVar typ)
	 (Map.empty, namesTy typ) typ
	where
	go :: forall p x.
	    Maybe (Type src ctx ss cs p) -- parent Type, used to prettify
	 -> (Infix, LR)    -- fixity and associativity
	 -> Var            -- variable counter (DeBruijn)
	 -> ( Map Var Name -- names of bound variables
	    , Names        -- used names : bound variables', free variables' and constants'
	    )
	 -> Type src ctx ss cs x
	 -> ShowS
	go _prev _po _v _vs (TyConst _src c) = showsPrec 11 c
	go _prev po v vs t@(TyApp _ (TyApp _ (TyConst _ f) a) b)
	 | FixityInfix op <- fixity_TyConst f =
		showParen (parenInfix po op) $
		go (Just t) (op, L) v vs a .
		showChar ' ' .
		showString (unParen $ show_TyConst f) .
		showChar ' ' .
		go (Just t) (op, R) v vs b
		where
		unParen ('(':s) | ')':s' <- reverse s = reverse s'
		unParen s = s
	go _prev po v vs t@(TyApp _src f a) =
		let op = infixR 11 in
		showParen (parenInfix po op) $
		go (Just t) (op, L) v vs f .
		showChar ' ' .
		go (Just t) (op, R) v vs a
	go prev po v (vs, ns) t@(TyQuant src nv kv f) =
		let op  = infixR 0 in
		let var = TyVar src kv v in
		let n   = freshifyName ns nv in
		let vs' = Map.insert v n vs in
		let ns' = Set.insert n ns in
		case f var of
		 KT x ->
			showParen (parenInfix po op) $
			(case prev of
			 Just TyQuant{} -> id
			 _ -> showString "forall") .
			showChar ' ' .
			go Nothing po v (vs', ns') var .
			(case x of
			 TyQuant{} -> id
			 _ -> showString ". ") .
			go (Just t) (op, R) (v + 1) (vs', ns') x
	go _prev _po _v (vs, _ns) (TyVar _src _kv v) =
		case Map.lookup v vs of
		 Nothing -> showChar '#' . showsPrec 0 v
		 Just n  -> showString $ Text.unpack n
	go _prev po v vs t@(Term x _te) =
		showBracket True $
		go (Just t) po v vs x
	go _prev po v vs (TyFam _src fam args) =
		let op = infixL 11 in
		showParen (parenInfix po op) $
		showsPrec 11 fam .
		foldlTys (\h acc ->
			showChar ' ' . go Nothing (op, L) v vs h . acc
		 ) args id

instance -- T
 ( Show_TyConst cs
 , Fixity_TyConst cs
 ) => Show (T src ctx ss cs h) where
	showsPrec = showTy
instance -- EType
 ( Show_TyConst cs
 , Fixity_TyConst cs
 ) => Show (EType src ctx ss cs) where
	showsPrec p (EType t) = showsPrec p t
instance -- KT
 ( Show_TyConst cs
 , Fixity_TyConst cs
 ) => Show (KT src ctx ss cs ki) where
	showsPrec p (KT t) = showTy p t

showTys
 :: forall src ctx ss cs hs.
    Show_TyConst cs
 => Fixity_TyConst cs
 => Types src ctx ss cs hs -> ShowS
showTys ts = showString "[" . go ts . showString "]"
	where
	go :: forall xs. Types src ctx ss cs xs -> ShowS
	go TypesZ = showString ""
	go (TypesS h0 (TypesS h1 hs)) = showTy 10 h0 . showString ", " . showTy 10 h1 . go hs
	go (TypesS h hs) = showTy 10 h . go hs

instance
 ( Show_TyConst cs
 , Fixity_TyConst cs
 ) => Show (Types src ctx ss cs hs) where
	showsPrec _p = showTys

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

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

namesTy :: Show_TyConst cs => Type src ctx ss cs h -> Names
namesTy (TyConst _src c)      = Set.singleton $ Text.pack $ show_TyConst c
namesTy (TyApp   _src f x)    = namesTy f `Set.union` namesTy x
namesTy (TyQuant src _n kv f) = namesTy `ofKT` f (TyVar src kv (-1))
namesTy (TyVar   _src _kv v)  | v < 0     = Set.empty
                              | otherwise = Set.singleton $ "#" <> Text.pack (show v)
namesTy (Term x _te) = namesTy x
namesTy (TyFam _src _f as) = foldrTys (\h acc -> Set.union (namesTy h) acc) as Set.empty

-- | 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 ..] ]

-- | 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