{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
-- | /type class/.
--
-- __Ressources:__
--
-- * /Type classes: exploring the design space/,
--   Simon Peyton Jones, Mark Jones, Erik Meijer, 1997,
--   http://research.microsoft.com/en-us/um/people/simonpj/Papers/type-class-design-space/multi.ps.gz
--
-- * /Implementing, and Understanding Type Classes/,
--   Oleg Kiselyov, 2014,
--   http://okmij.org/ftp/Computation/typeclass.html
module Language.LOL.Typing.Type.Class where

import Control.Arrow (first)
import Control.Monad (mapM)
import Data.Bool
import Data.Either (Either(..))
import Data.Eq (Eq(..))
import qualified Data.Foldable as Foldable
import Data.Function (($), (.), flip)
import Data.Functor ((<$>))
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (Maybe(..), maybe)
import Data.Monoid ((<>))
import Data.Text (Text)
import Data.Text.Buildable (Buildable(..))
import Text.Show (Show(..))

import Language.LOL.Typing.Type.Monotype
import Language.LOL.Typing.Type.Substitution (Substitutable(..))
import Language.LOL.Typing.Type.Synotype
import Language.LOL.Typing.Type.Unification
import Language.LOL.Typing.Type.Qualification

-- * Type 'Class'

data Class
 =   Class
 {   class_supers    :: [Class_Name] -- ^ /adjacent super classes/
 ,   class_instances :: [Class_Instance] -- ^ /class instances/
 } deriving (Eq, Show)

-- ** Type 'Class_Instance'

data Class_Instance
 =   Class_Instance
 {   class_instance_head    :: Class_Qualifier
 ,   class_instance_context :: [Class_Qualifier]
 } deriving (Eq, Show)

-- ** Type 'Class_Qualifier'

data Class_Qualifier
 =   Class_Qualifier
 {   class_qualifier_name :: Class_Name
 ,   class_qualifier_type :: Monotype
 } deriving (Eq, Show)

-- | Right associative alias for 'Qualification'.
(.=>.) :: [Class_Qualifier] -> a -> Qualification [Class_Qualifier] a
(.=>.) = Qualification
infixr 2 .=>.

instance Buildable Class_Qualifier where
	build (Class_Qualifier q ty) =
		build q <> " "  <> build ty
instance Substitutable Class_Qualifier where
	subvars = subvars . class_qualifier_type
	sub `substitute` p = p{class_qualifier_type =
		sub `substitute` class_qualifier_type p}
instance Has_Monoconsts Class_Qualifier where
	monoconsts p = monoconsts (class_qualifier_type p)
instance Has_Monotypes Class_Qualifier where
	monotypes q = [class_qualifier_type q]
	monotypes_map f q = q{class_qualifier_type = f (class_qualifier_type q)}

-- | Return the 'Unification' (when it exists)
-- of two given 'Class_Qualifier's,
-- using given 'Synotype_Substitution'.
class_qualifier_unification
 :: Synotype_Substitution
 -> Class_Qualifier
 -> Class_Qualifier
 -> Maybe Unification
class_qualifier_unification syns
 (Class_Qualifier na1 ty1)
 (Class_Qualifier na2 ty2)
 | na1 == na2 =
	case mgu_with_synotypes syns (constify ty1) ty2 of
	 Left _ -> Nothing
	 Right (_, uni) -> Just (unconstify <$> uni)
 | otherwise = Nothing

-- ** Type 'Class_Env'

type Class_Env  = Map Class_Name Class
type Class_Name = Text
type Class_Path = [Class_Name]

class_env_empty :: Class_Env
class_env_empty = Map.empty

class_env_default :: Class_Env
class_env_default = Map.fromList
	[ ("Num",)
		Class
		 { class_supers    = ["Eq", "Show"]
		 , class_instances =
			 [ Class_Instance (Class_Qualifier "Num" ty) []
			 | ty <- [type_Int, type_Float]
			 ]
		 }
	, ("Enum",)
		Class
		 { class_supers    = []
		 , class_instances =
			 [ Class_Instance (Class_Qualifier "Enum" ty) []
			 | ty <- [type_Unit, type_Int, type_Float, type_Bool, type_Char]
			 ]
		 }
	, ("Eq",)
		Class
		 { class_supers    = []
		 , class_instances =
			Class_Instance
			 { class_instance_head = Class_Qualifier "Eq" "Ordering"
			 , class_instance_context  = []
			 } :
			instances_Eq_Ord_Show "Eq"
		 }
	, ("Ord",)
		Class
		 { class_supers    = ["Eq"]
		 , class_instances = instances_Eq_Ord_Show "Ord"
		 }
	, ("Show",)
		Class
		 { class_supers    = []
		 , class_instances = instances_Eq_Ord_Show "Show"
		 }
	]
	where
	instances_Eq_Ord_Show name =
		Class_Instance -- NOTE: List instance
		 { class_instance_head = Class_Qualifier name (type_List (Monotype_Var 0))
		 , class_instance_context  = [Class_Qualifier name (Monotype_Var 0)]
		 } :
		[ Class_Instance
			 { class_instance_head = Class_Qualifier name ty
			 , class_instance_context  = []
			 }
		| ty <- [type_Bool, type_Char, type_Float, type_Int]
		] <>
		(inst_tuples <$> (0 : [2..10]))
		where
		inst_tuples i =
			Class_Instance
			 { class_instance_head =
				Class_Qualifier name (type_Tuple [ Monotype_Var n | n <- [1..i] ])
			 , class_instance_context =
				[ Class_Qualifier name (Monotype_Var n)
				| n <- [1..i]
				]
			 }

-- | Return given 'Class_Env'
-- with given 'Class_Name'
-- mapping to a 'Class'
-- with given 'Class_Instance'.
class_env_insert_instance
 :: Class_Name
 -> Class_Instance
 -> Class_Env -> Class_Env
class_env_insert_instance name inst =
	Map.insertWith
	 (\_new old -> old{class_instances = inst : class_instances old})
	 name Class
	 { class_supers    = []
	 , class_instances = [inst]
	 }

-- | Return whether given 'Class_Env'
-- has a 'Class' with given 'Class_Name'.
class_env_has :: Class_Env -> Class_Name -> Bool
class_env_has = flip Map.member

-- | Return the 'class_supers'
-- associated to the given 'Class_Name',
-- in given 'Class_Env'.
--
-- Example: @'class_env_supers' 'class_env_default' \"Ord\" '==' [\"Eq\"]@
class_env_supers :: Class_Env -> Class_Name -> [Class_Name]
class_env_supers env name = maybe [] class_supers $ Map.lookup name env

-- | Return the 'Class_Path's
-- between given 'Class_Name's
-- in given 'Class_Env'.
class_env_super_path
 :: Class_Env
 -> Class_Name -> Class_Name
 -> [Class_Path]
class_env_super_path env from to
 | from == to = [[to]]
 | otherwise =
	[ from : path
	| super <- class_env_supers env from
	, path <- class_env_super_path env super to
	]

-- | Return the 'Class_Instance's
-- of given 'Class_Name' within given 'Class_Env'.
class_env_instances
 :: Class_Env -> Class_Name -> [Class_Instance]
class_env_instances env name =
	maybe [] class_instances $
	Map.lookup name env

-- | Return all the 'Class_Qualifier's
-- of all the 'class_supers'
-- of the given 'Class_Qualifier',
-- within given 'Class_Env'.
class_env_supers_all
 :: Class_Env
 -> Class_Qualifier
 -> [Class_Qualifier]
class_env_supers_all env p@(Class_Qualifier name ty) =
	p : List.concat
	 [ class_env_supers_all env (Class_Qualifier supers ty)
	 | supers <- class_env_supers env name
	 ]

-- | Return the 'class_instance_context'
-- 'substitute'd by the 'class_qualifier_unification'
-- of the first 'class_instance_head'
-- unifying with given 'Class_Qualifier',
-- within given 'Class_Env',
-- and using given 'Synotype_Substitution'.
class_env_instance_context
 :: Synotype_Substitution
 -> Class_Env
 -> Class_Qualifier
 -> Maybe [Class_Qualifier]
class_env_instance_context syns env qual@(Class_Qualifier qname _) =
	Foldable.msum
	 [ context inst
	 | inst <- class_env_instances env qname
	 ]
	where
	context :: Class_Instance -> Maybe [Class_Qualifier]
	context Class_Instance{class_instance_head, class_instance_context} = do
		uni <- class_qualifier_unification syns qual class_instance_head
		Just (uni `substitute` class_instance_context)

-- ** Normalization

class_qualifier_normalize
 :: Synotype_Substitution
 -> Class_Env
 -> Class_Qualifier
 -> Maybe [Class_Qualifier]
class_qualifier_normalize syns env p
 | is_class_qualifier_normalized p = Just [p]
 | otherwise = do
	ctx <- class_env_instance_context syns env p
	class_context_normalize syns env ctx

is_class_qualifier_normalized :: Class_Qualifier -> Bool
is_class_qualifier_normalized (Class_Qualifier _ ty) = go ty
	where
	go (Monotype_Var _)   = True
	go (Monotype_Const _) = False
	go (Monotype_App t _) = go t

class_context_normalize
 :: Synotype_Substitution
 -> Class_Env
 -> [Class_Qualifier]
 -> Maybe [Class_Qualifier]
class_context_normalize syns env ps =
	List.concat <$>
	mapM (class_qualifier_normalize syns env) ps

-- ** Entailment

class_entails
 :: Synotype_Substitution
 -> Class_Env
 -> [Class_Qualifier]
 -> Class_Qualifier
 -> Bool
class_entails syns env quals qual =
	class_entails_super_class env quals qual ||
	case class_env_instance_context syns env qual of
	 Nothing -> False
	 Just insts -> Foldable.all (class_entails syns env quals) insts

-- | Return whether a given 'Class'
-- implies another as a 'class_supers'.
class_entails_super_class
 :: Class_Env
 -> [Class_Qualifier]
 -> Class_Qualifier
 -> Bool
class_entails_super_class env ps p =
	Foldable.any
	 (p `List.elem`)
	 (class_env_supers_all env <$> ps)

class_entails_all
 :: Synotype_Substitution
 -> Class_Env
 -> [Class_Qualifier]
 -> [Class_Qualifier]
 -> Bool
class_entails_all syns env ps =
	Foldable.all (class_entails syns env ps)

-- ** Type 'Class_Reduction_Error'

newtype Class_Reduction_Error a
 =      Class_Reduction_Error a
 deriving (Show)

-- | Reduce a 'Class' context by performing:
--
-- 1. Simplification using 'Class_Instance's.
--
--      Example: @Eq (a, b)@ is simplified to @Eq a@ and @Eq b@.
--
--      Example: @Eq Int@ is removed.
--
--      Example: @Num Bool@ (whose 'Class_Instance' does not exist)
--               gives a 'Class_Reduction_Error'.
--
-- 2. Removal of 'Class'es entailed by 'class_supers'.
--
--      Example: Because @Eq@ is the superclass of @Ord@, @Ord a@ 'class_entails' @Eq a@,
--               which therefore can safely be removed when @Ord a@ is present.
--
-- 3. Removal of duplicate 'Class'es.
class_context_reduction
 :: Synotype_Substitution
 -> Class_Env
 -> [Class_Qualifier]
 -> ( [Class_Qualifier]
    , [Class_Reduction_Error Class_Qualifier]
    )
class_context_reduction syns env =
	first (go []) . List.foldr fold ([], [])
	where
	fold qual (quals, errs) =
		case class_qualifier_normalize syns env qual of
		 Just qs -> (qs <> quals, errs)
		 Nothing -> (quals, Class_Reduction_Error qual : errs)
	go rs [] = rs
	go rs (q:qs)
	 | entailed  = go    rs  qs
	 | otherwise = go (q:rs) qs
		where entailed = class_entails_super_class env (rs <> qs) q

{-
context_reduction_associated
 :: Synotype_Substitution
 -> Class_Env
 -> [(Class_Qualifier, a)]
 -> ( [(Class_Qualifier, a)]
    , [Class_Reduction_Error (Class_Qualifier, a)]
    )
context_reduction_associated syns env =
	first (go []) . List.foldr fold ([], [])
	where
	fold (qual, a) (reduced, es) =
		case class_qualifier_normalize syns env qual of
		 Just qs -> ([(p, a) | p <- qs] <> reduced, es)
		 Nothing -> (reduced, Class_Reduction_Error (qual, a) : es)
	go rs [] = rs
	go rs (q:qs)
	 | entailed  = go    rs  qs
	 | otherwise = go (q:rs) qs
		where
		entailed = class_entails_super_class env
			 (fst <$> (rs <> qs)) (fst q)
-}

-- * Type 'Class_Directive'

data Class_Directive info
 =   Class_Directive_Never    Class_Qualifier info
 |   Class_Directive_Close    Class_Name            info
 |   Class_Directive_Disjoint [Class_Name]          info
 |   Class_Directive_Default  Class_Name [Monotype] info
 deriving (Eq, Show)

instance Buildable info => Buildable (Class_Directive info) where
	build _ = "Class_Directive"
	 -- FIXME: write it.