{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
module Language.LOL.Typing.Solver.Monad where

import Control.Applicative (Applicative(..))
import Control.Monad (Monad(..))
import qualified Control.Monad.Classes as MC
import qualified Control.Monad.Classes.Run as MC
import qualified Control.Monad.Trans.State.Lazy as SL
import Data.Bool
import Data.Eq (Eq(..))
import Data.Function (($), (.))
import Data.Functor ((<$>))
import qualified Data.List as List
import Data.Map.Strict (Map)
import Data.Monoid (Monoid(..), (<>))
import Data.Ord (Ord(..), max)
import Data.Sequence (Seq)
import Data.Text.Buildable (Buildable(..))
import Prelude (Num(..))
import Text.Show (Show(..))

import Language.LOL.Typing.Type
import Language.LOL.Typing.Solver.Common
import Language.LOL.Typing.Solver.Constraint
import Language.LOL.Typing.Solver.Monotype
import Language.LOL.Typing.Solver.Polytype
import Language.LOL.Typing.Solver.Class
import Language.LOL.Typing.Lib.Data.Empty (Empty(..))
import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.Instance as MC
import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.StateFix as MC
import qualified Language.LOL.Typing.Lib.Control.Monad.Classes.StateInstance as MC
import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build

-- * Type 'Solver'

-- | A 'Monad' stack gathering all the @Solver_*@.
--
-- * @m@ is a base 'Monad'
--   (for instance within which 'Solver_Log's
--   can be handled during the solving).
-- * @info@ is a polymorphic type to hold informations
--   about the origin of the 'Constraint's.
-- * @monotype_substitution@ is a for accumulating known 'Monotype's
--   (for example it can be: 'Substitution_Finite' or 'Substitution_Fixpoint').
type Solver info m monotype_substitution =
	MC.StateLazyFixT State_Constraint
	(SL.StateT (State_Monotype monotype_substitution)
	(SL.StateT (State_Polytype info)
	(SL.StateT (State_Class info)
	(WriterT Solver_Log
	m))))

-- * Type 'Solver_Log'

data Solver_Log
 =   Solver_Log_States [MC.Instance State]
     -- ^ Logs summarizing the 'State's.
 |   Solver_Log_Constraint Log_Constraint
     -- ^ Log of 'Constraint' handling.
 |   Solver_Log_Class Log_Class
     -- ^ Log of 'Class' handling.
 |   Solver_Log_Polytype Log_Polytype
     -- ^ Log of 'Polytype' handling.

instance Monad m
 => Solver_Logable Log_Constraint (Solver info m sub) where
	log = MC.tell . Solver_Log_Constraint
instance Monad m
 => Solver_Logable Log_Class (Solver info m sub) where
	log = MC.tell . Solver_Log_Class
instance Monad m
 => Solver_Logable Log_Polytype (Solver info m sub) where
	log = MC.tell . Solver_Log_Polytype

log_states
 :: forall m.
 ( MC.MonadWriter Solver_Log m
 , MC.MonadStateInstance State m
 , Solver_Constraint m
 ) => m ()
log_states = do
	(states::[MC.Instance State]) <- MC.getInstance
	MC.tell $ Solver_Log_States states

-- | Type synonym to 'MC.CustomWriterT',
-- /eta-reduced/ to fit in 'Solver'.
type WriterT w m = MC.CustomWriterT' w m m

-- * Type 'Solver_Info'

data Solver_Info info
 =   Solver_Info_Class    (Info_Class info)
 |   Solver_Info_Monotype Info_Monotype
 |   Solver_Info_Polytype Info_Polytype
 deriving (Eq, Show)
instance Buildable info => Buildable (Solver_Info info) where
	build x =
		case x of
		 Solver_Info_Class    i -> build i
		 Solver_Info_Monotype i -> build i
		 Solver_Info_Polytype i -> build i
instance Buildable info => Buildable [Solver_Info info] where
	build = Build.list

instance
 ( Monad m
 , Buildable info
 ) =>  Information (Solver info m sub) where
	type Info        (Solver info m sub) = info

data instance Error (Solver info m sub)
 = Solver_Error_Class    Error_Class
 | Solver_Error_Monotype Error_Monotype
 | Solver_Error_Polytype Error_Polytype
 deriving (Eq, Show)

instance
 ( Monad m
 , Buildable info
 ) => Solver_Constraint (Solver info m sub)
instance
 ( Monad m
 , Buildable info
 , Solver_Monotype_Substitution sub
 , Infoable Info_Monotype info
 ) =>  Solver_Monotype     (Solver info m sub) where
	type Solver_Monotype_Sub (Solver info m sub) = sub
	error_monotype = Solver_Error_Monotype
instance
 ( Monad m
 , Buildable info
 , info ~ Info (Solver info m sub)
 , Infoable Info_Polytype info
 ) => Solver_Polytype (Solver info m sub) where
	error_polytype = Solver_Error_Polytype
instance
 ( Monad m
 , Buildable info
 , info ~ Info (Solver info m sub)
 , Infoable Info_Monotype info
 , Infoable Info_Polytype info
 , Infoable (Info_Class info) info
 , Solver_Monotype_Substitution sub
 ) => Solver_Class (Solver info m sub) where
	error_class = Solver_Error_Class

-- | Return within base 'Monad' @m@.
-- the 'Solver_Result' produced
-- by evaluating the given 'Solver',
-- while using the given 'Solver_Log' handler.
solve ::
 ( sol ~ Solver info m sub
 , res ~ Solver_Result (Info sol) (Error sol)
 , Monad m
 , Empty sub
 ) => (Solver_Log -> m ())
 -> sol res -> m res
solve writer_log =
	MC.evalWriterWith writer_log .
	MC.evalStateLazy    empty .
	MC.evalStateLazy    empty .
	MC.evalStateLazy    empty .
	MC.evalStateLazyFix empty

-- | Return the 'Solver' produced
-- by the given 'Solver_Config' and 'Contraint's.
solver ::
 ( sol ~ Solver info m sub
 , res ~ Solver_Result (Info sol) (Error sol)
 , Monad m
 , Solver_Monotype_Substitution sub
 , Solvable constraint sol
 , MC.CansMonadStateInstance State (MC.EffState ()) m ~ '[ 'False ]
   -- NOTE: require that the inner 'Monad' does not have 'State' instances.
 , Buildable info
 , Infoable Info_Monotype info
 , Infoable Info_Polytype info
 , Infoable (Info_Class info) info
 ) => Solver_Config -> Seq constraint -> sol res
solver cfg cs = do
	solver_init cs cfg
	solver_run cs
	solver_result

-- | Run the solvers of a 'Monad' over the given 'Constraint's.
solver_run ::
 ( Solvable constraint m
 , Solver_Constraint m
 , Solver_Monotype m
 , Solver_Polytype m
 , Solver_Class m
 , MC.MonadWriter Solver_Log m
 , MC.MonadStateInstance State m
 ) => Seq constraint -> m ()
solver_run cs = do
	constraint_push_many $ constraints cs
	log_states
	constraint_solve
	monotype_substitution_consistentify
	polytype_rigids_check
	class_ambiguities
	log_states

-- ** Type 'Solver_Config'

data Solver_Config
 =   Solver_Config
 {   solver_config_class_env :: Class_Env
 ,   solver_config_freshvar  :: Freshvar
 ,   solver_config_synotypes :: Synotype_Substitution
 ,   solver_config_check     :: Bool
 ,   solver_config_stop      :: Bool
 }

-- | Return a 'Solver_Config'.
solver_config :: Solver_Config
solver_config =
	Solver_Config
	 { solver_config_class_env = class_env_default
	 , solver_config_freshvar  = -1
	 , solver_config_synotypes = empty
	 , solver_config_check     = option_current $ state_constraint_option_check empty
	 , solver_config_stop      = option_current $ state_constraint_option_stop  empty
	 }

-- | Initialize a solver 'Monad' with given 'Solver_Config'.
solver_init ::
 forall m constraints.
 ( Substitutable constraints
 , Solver_Constraint m
 , Solver_Polytype m
 , Solver_Class m
 ) => constraints -> Solver_Config -> m ()
solver_init cs cfg = do
	polytype_freshvar_set freshvar
	synotype_substitution_set $
		solver_config_synotypes cfg
	class_env_set $
		solver_config_class_env cfg
	MC.modifyFix $ \(s::State_Constraint m) ->
		s{ state_constraint_option_check =
			(state_constraint_option_check s)
			 { option_current = solver_config_check cfg }
		 , state_constraint_option_stop =
			(state_constraint_option_stop s)
			 { option_current = solver_config_stop cfg }
		 }
	where
	freshvar
	 | solver_config_freshvar cfg < 0 = 1 + List.maximum (-1 : subvars cs)
	 | otherwise                      = solver_config_freshvar cfg

-- ** Type 'Solver_Result'

data Solver_Result info err
 =   Solver_Result
 {   solver_result_freshvar    :: Freshvar
 ,   solver_result_monotypes   :: Substitution_Fixpoint
 ,   solver_result_polytypes   :: Polysub
 ,   solver_result_quantifiers :: Map Monovar [Quantifier]
 ,   solver_result_qualifiers  :: [Class_Qualifier]
     -- ^ 'Class_Qualifier's assumed to hold.
 ,   solver_result_errors      :: [(info, err)]
 }

instance Empty (Solver_Result info err) where
	empty = mempty
instance Monoid (Solver_Result info err) where
	mempty = Solver_Result 0 mempty mempty mempty mempty mempty
	mappend
	 (Solver_Result fr1 ms1 ps1 qts1 qls1 es1)
	 (Solver_Result fr2 ms2 ps2 qts2 qls2 es2) =
		Solver_Result
		 (fr1 `max` fr2)
		 (ms1 <> ms2)
		 (ps1 <> ps2)
		 (qts1 <> qts2)
		 (qls1 <> qls2)
		 (es1 <> es2)

-- | Return a 'Solver_Result' from a solver 'Monad'.
solver_result ::
 ( Solver_Constraint m
 , Solver_Monotype m
 , Solver_Polytype m
 , Solver_Class m
 ) => m (Solver_Result (Info m) (Error m))
solver_result =
	Solver_Result
	 <$> polytype_freshvar
	 <*> monotype_substitution
	 <*> polytype_substitution
	 <*> polytype_quantifiers
	 <*> class_qualifiers_reduced
	 <*> constraint_errors