{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
module Language.LOL.Typing.Type.Kind where

import Data.Function (($))
import Data.Int (Int)
import Data.List ((++))
import qualified Data.List as List
import Data.String (String)
import qualified Data.Text as Text
import Text.Show (Show(..))

import Language.LOL.Typing.Type.Monotype
import Language.LOL.Typing.Type.Polytype
import Language.LOL.Typing.Type.Substitution
import Language.LOL.Typing.Type.Quantification

-- * Type 'Monokind'

type Monokind = Monotype
type Polykind = Polytype

-- | The kind of all 'Type's.
star :: Monokind
star = Monotype_Const "*"

-- | In traditional /kind inference systems/,
-- a kind cannot contain /kind variables/.
-- At some point in the inference process
-- the /kind variables/ are defaulted to 'star'.
monokind_vars_to_star :: Monokind -> Monokind
monokind_vars_to_star ki = sub `substitute` ki
	where
	sub = substitution_finite
	 [ (v, star)
	 | v <- subvars ki
	 ]

-- | A function to show kinds.
show_Monokind :: Monokind -> String
show_Monokind ki = show (sub `substitute` ki)
	where
	sub = substitution_finite
	 [ (v, Monotype_Const (Text.pack ('k':show v)))
	 | v <- subvars ki
	 ]

show_Polykind :: Polykind -> String
show_Polykind polyki = show (sub `substitute` quantified polyki)
	where
	sub = substitution_finite $
	 [ (v1, Monotype_Const (Text.pack ('k':show v2)))
	 | (v1, v2) <- List.zip (quantifiers polyki) [1 :: Int ..]
	 ] ++
	 [ (v, Monotype_Const (Text.pack ("_k"++show v)))
	 | v <- subvars polyki
	 ]