{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Language.LOL.Typing.Type.Polytype where

import Data.Bool
import qualified Data.Foldable as Foldable
import Data.Functor ((<$>))
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Function ((.), id)
import qualified Data.List as List
import Data.Monoid ((<>))
import Data.Text.Buildable (Buildable(..))
import Text.Show (Show(..))

import Language.LOL.Typing.Type.Monotype
import Language.LOL.Typing.Type.Substitution
import Language.LOL.Typing.Type.Quantification
import Language.LOL.Typing.Type.Qualification
import Language.LOL.Typing.Type.Class
import Language.LOL.Typing.Lib.Data.Default (Default(..))

-- * Type 'Polytype'

-- | A /rank-1 polymorphic type/ (aka. /polytype/), with qualifiers.
type Polytype
 = Forall (Qualification [Class_Qualifier] Monotype)
instance Buildable Polytype where
	build x = build (def::Quantification_Build_Options, x)
instance Has_Monoconsts Polytype where
	monoconsts Quantification{quantified = Qualification quals monoty} =
		Map.unions (monoconsts monoty : (monoconsts <$> quals))

-- | Return a 'Polytype' /generalizing/ the given 'Monotype':
--
-- * quantifying all its 'Monovar's (which thus become /polymorphic/)
--   except the given 'Monovar's (which thus remain /monomorphic/),
-- * and qualifying them by the given 'Class_Qualifier's
--   which use at least one of them.
polytype_but
 :: [Monovar] -> [Class_Qualifier]
 -> Monotype -> Polytype
polytype_but vars_mono quals monoty =
	forall_in vars_poly Qualification
	 { qualifiers = List.filter is_quantified quals
	 , qualified  = monoty
	 }
	where
	vars_poly = subvars monoty List.\\ vars_mono
	is_quantified = Foldable.any (`List.elem` vars_poly) . subvars

-- | A /type with qualifiers/, constructed from a 'Monotype'
-- and some 'Class_Qualifier's (aka. /class context/).
--
-- These 'Class_Qualifier's put restrictions on certain 'Monovar's.
type Qualified_Type
 =   Qualification [Class_Qualifier] Monotype

-- ** Class 'Polytypeable'

-- | A type class to convert something into a 'Polytype'
class Polytypeable a where
	polytype :: a -> Polytype
instance Polytypeable Monotype where
	polytype = quantification . ([] .=>.)
instance Polytypeable (Qualification [Class_Qualifier] Monotype) where
	polytype = quantification
instance Polytypeable Polytype where
	polytype = id

-- | Return the 'Arity' of a 'Polytype'.
polytype_arity :: Polytype -> Arity
polytype_arity = type_arity . qualified . quantified

-- | Return whether the given 'Polytype' contains 'Class_Qualifier's.
is_polytype_qualified :: Polytype -> Bool
is_polytype_qualified = not . Foldable.null . qualifiers . quantified

-- * Type 'Polysub'

-- | A /polymorphic type substitution/.
type Polysub = Map Polyvar Polytype

-- | A /polymorphic type variable/:
-- a place-holder for a 'Polytype' that is not yet known,
-- but that become available at some time during 'Constraint' solving.
--
-- NOTE: is to 'Polytype', what a 'Monovar' is to a 'Monotype'.
type Polyvar = Quantifier

-- * Type 'Polytyref'

data Polytyref
 =   Polytyref     Polytype
 |   Polytyref_Var Polyvar
 deriving (Show)

instance Buildable Polytyref where
	build r =
		case r of
		 Polytyref polyty -> build (def::Quantification_Build_Options, polyty)
		 Polytyref_Var v  -> "p" <> build v
instance Substitutable Polytyref where
	subvars (Polytyref polyty) = subvars polyty
	subvars (Polytyref_Var _)  = []
	
	_   `substitute` r@(Polytyref_Var _) = r
	sub `substitute` (Polytyref s)       = Polytyref (sub `substitute` s)

-- ** Class 'Polytyrefable'

class Polytyrefable a where
	polytyref :: a -> Polytyref

instance Polytyrefable Monotype       where polytyref = Polytyref . polytype
instance Polytyrefable Polytype       where polytyref = Polytyref . polytype
instance Polytyrefable Polytyref      where polytyref = id
instance Polytyrefable Polyvar        where polytyref = Polytyref_Var
instance Polytyrefable Qualified_Type where polytyref = Polytyref . polytype