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

import Control.Monad (Monad(..), filterM, forM_, mapM, unless, when)
import Data.Bool
import qualified Data.Foldable as Foldable
import Data.Function (($), (.))
import Data.Functor (Functor(..), (<$>))
import qualified Data.List as List
import Data.Maybe (Maybe(..))
import Data.Monoid (Monoid(..), (<>))
import Data.Sequence (Seq, (<|))
import qualified Data.Sequence as Seq
import Data.String (String)
import qualified Data.Text as Text
import Data.Text.Buildable (Buildable(..))
import Data.Tuple (fst, snd)
import Prelude (error)
import Text.Show (Show(..))

import Language.LOL.Typing.Type
import Language.LOL.Typing.Solver.Common
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 Language.LOL.Typing.Lib.Data.Empty (Empty(..))
import qualified Language.LOL.Typing.Lib.Data.Text.Buildable as Build

-- * Type 'Constraint'

data Constraint m =
	forall c. (Show c, Buildable c, Substitutable c)
	 => Constraint c
	 (c -> m ()) -- solving strategy
	 (c -> m Bool) -- semantic check

instance Show (Constraint m) where
	show (Constraint c _ _) = show c
instance Buildable (Constraint m) where
	build (Constraint c _ _) = build c
instance Substitutable (Constraint m) where
	subvars (Constraint c _ _) = subvars c
	sub `substitute` (Constraint c f g) =
		Constraint (sub `substitute` c) f g
instance Monad m => Solvable (Constraint m) m where
	constraint_solver  (Constraint c f _) = f c
	constraint_checker (Constraint c _ f) = f c

-- | Return a 'Constraint' from a 'Solvable' instance.
constraint :: Solvable c m => c -> Constraint m
constraint c = Constraint c constraint_solver constraint_checker

constraints :: (Solvable c m, Functor f) => f c -> f (Constraint m)
constraints = (constraint <$>)

constraint_map :: (forall a. m1 a -> m2 a) -> Constraint m1 -> Constraint m2
constraint_map t (Constraint c f g) = Constraint c (t . f) (t . g)

-- ** Class 'Solvable'

-- | A type class for 'Constraint's solvable within a 'Monad'.
class (Show c, Buildable c, Substitutable c, Monad m) => Solvable c m where
	constraint_solver  :: c -> m ()
	constraint_checker :: c -> m Bool
	constraint_checker _ = return True

-- * Type 'State_Constraint'

-- | A 'State_Constraint' is parameterized over the 'Monad'
-- in which the 'Constraint's can be solved.
data State_Constraint m
 =   State_Constraint
 {   state_constraint_constraints  :: Seq (Constraint m)
     -- ^ A stack of 'Constraint's to solve.
 ,   state_constraint_checks       :: [(m Bool, String)]
     -- ^ Conditions to check (for the solved 'Constraint's).
 ,   state_constraint_errors       :: [(Info m, Error m)]
     -- ^ The detected errors.
 ,   state_constraint_option_stop  :: Option Bool
     -- ^ Whether to discard all remaining 'Constraint's after the first error.
 ,   state_constraint_option_check :: Option Bool
     -- ^ Whether to check constraint satisfaction afterwards.
 }

-- | Make 'State_Constraint' collectable as a 'State' instance
-- out of a 'Monad' stack.
type instance MC.Class State (State_Constraint m) = 'True

instance Show (State_Constraint m) where
	show = Build.string
instance Buildable (State_Constraint m) where
	build State_Constraint
	 { state_constraint_constraints
	 , state_constraint_errors
	 , state_constraint_checks } =
		Build.unlines $
		 [ "constraints: " <> Build.tuple
			 [ show (List.length state_constraint_constraints) <> " constraints"
			 , show (List.length state_constraint_errors) <> " errors"
			 , show (List.length state_constraint_checks) <> " checks"
			 ]
		 ] <> (("  " <>) . build <$>
			Foldable.toList state_constraint_constraints)
instance State (State_Constraint m) where
	state_name _ = "State_Constraint"
	state_show = Build.text
	state_options s =
	 [ Text.pack $ show $ state_constraint_option_stop  s
	 , Text.pack $ show $ state_constraint_option_check s
	 ]
instance Empty (State_Constraint m) where
	empty = State_Constraint
	 { state_constraint_constraints  = mempty
	 , state_constraint_errors       = mempty
	 , state_constraint_checks       = mempty
	 , state_constraint_option_stop  = option False "Stop solving at first error"
	 , state_constraint_option_check = option False "Check the solution"
	 }

-- * Class 'Solver_Constraint'

class
 ( MC.MonadStateFix State_Constraint m
 , Information m
 , Solver_Logable Log_Constraint m
 ) => Solver_Constraint m where
	constraint_push :: Constraint m -> m ()
	constraint_push c = do
		log $ Log_Constraint_Push c
		MC.modifyFix $ \(s::State_Constraint m) ->
			s{ state_constraint_constraints =
				c <| state_constraint_constraints s }
	
	constraint_push_many :: Seq (Constraint m) -> m ()
	constraint_push_many cs = do
		forM_ cs $ log . Log_Constraint_Push
		MC.modifyFix $ \(s::State_Constraint m) ->
			s{ state_constraint_constraints =
				cs <> state_constraint_constraints s }
	
	constraint_pop :: m (Maybe (Constraint m))
	constraint_pop = do
		cs <- MC.getsFix $ \(s::State_Constraint m) ->
			state_constraint_constraints s
		case Seq.viewl cs of
		 Seq.EmptyL -> return Nothing
		 (c Seq.:< state_constraint_constraints) -> do
			log $ Log_Constraint_Pop c
			MC.modifyFix (\(s::State_Constraint m) ->
				s{ state_constraint_constraints })
			return (Just c)
	
	constraint_discard :: m ()
	constraint_discard =
		MC.modifyFix $ \(s::State_Constraint m) ->
			s{ state_constraint_constraints = mempty }
	
	constraint_error_insert :: Error m -> Info m -> m ()
	constraint_error_insert err info = do
		MC.modifyFix (\(s::State_Constraint m) ->
			s{ state_constraint_errors =
				(info, err) : state_constraint_errors s })
		stop <- constraint_option_stop
		when (option_current stop)
			constraint_discard
	
	constraint_errors :: m [(Info m, Error m)]
	constraint_errors =
		MC.getsFix $ \(s::State_Constraint m) ->
			state_constraint_errors s
	
	constraint_error_info_update
	 :: (Info m -> m (Info m)) -> m ()
	constraint_error_info_update f = do
		errs <- constraint_errors
		state_constraint_errors <- do
			let g (info, err) = do
				info' <- f info
				return (info', err)
			g `mapM` errs
		MC.modifyFix $ \(s::State_Constraint m) ->
			s{ state_constraint_errors }
	
	-- | Add sanity checks for the solved 'Constraint's,
	-- performed when all 'Constraint's have been solved.
	--
	-- The first argument of 'constraint_check_insert' is
	-- a message, which is reported
	-- when the second argument evaluates
	-- to 'False' (in the 'Monad' @m@).
	constraint_check_insert :: String -> m Bool -> m ()
	constraint_check_insert text check =
		MC.modifyFix $ \(s::State_Constraint m) ->
			s{ state_constraint_checks =
				(check, text) : state_constraint_checks s}
	
	constraint_check_get :: m [(m Bool, String)]
	constraint_check_get =
		MC.getsFix $ \(s::State_Constraint m) ->
			state_constraint_checks s
	
	constraint_option_stop :: m (Option Bool)
	constraint_option_stop =
		MC.getsFix $ \(s::State_Constraint m) ->
			state_constraint_option_stop s
	
	constraint_option_check :: m (Option Bool)
	constraint_option_check =
		MC.getsFix (\(s::State_Constraint m) ->
			state_constraint_option_check s)
	
	constraint_solve :: m ()
	constraint_solve = do
		mc <- constraint_pop
		case mc of
		 Just c -> do
			constraint_solver c
			constraint_check_insert (show c) (constraint_checker c)
			constraint_solve
		 Nothing -> do
			check <- option_current <$> constraint_option_check
			errs <- fmap fst <$> constraint_errors
			when (check && List.null errs)
				constraint_check
	
	constraint_check :: m ()
	constraint_check = do
		ms <- constraint_check_get
		bs <- filterM ((not <$>) . fst) ms
		unless (List.null bs) $
			let err =
				"\n\n  Constraints violated:\n"
				 <> List.unlines (fmap (("  - " <>) . snd) bs) in
			error $ "constraint_check: " <> err

-- ** Type 'Log_Constraint'

data Log_Constraint
 =   forall c. (Show c, Buildable c) => Log_Constraint_Pop  c
 |   forall c. (Show c, Buildable c) => Log_Constraint_Push c
deriving instance Show Log_Constraint
instance Buildable Log_Constraint where
	build x =
		case x of
		 Log_Constraint_Pop  c -> "constraint_pop : " <> build c
		 Log_Constraint_Push c -> "constraint_push: " <> build c