{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
-- | Type inference for /monomorphic types/.
module Language.LOL.Typing.Solver.Monotype where

import Control.Monad (Monad(..), mapM)
import qualified Control.Monad.Classes as MC
import Data.Bool
import Data.Either (Either(..))
import Data.Eq (Eq(..))
import Data.Function (($), (.), id)
import Data.Int (Int)
import qualified Data.List as List
import qualified Data.Map.Strict as Map
import Data.Maybe (Maybe(..), fromMaybe)
import Data.Monoid (Monoid(..), (<>))
import Data.Text (Text)
import Data.Text.Buildable (Buildable(..))
import Data.Tuple (uncurry)
import Prelude (error)
import Text.Show (Show(..))

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

-- * Type 'State_Monotype'

data State_Monotype sub
 =   State_Monotype
 {   state_monotype_substitution :: sub
     -- ^ Known 'Monovar's.
 ,   state_monotype_synotypes :: Synotype_Substitution
     -- ^ Known 'Synotype's.
 } deriving (Show)

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

instance Buildable sub => Buildable (State_Monotype sub) where
	build State_Monotype
	 { state_monotype_substitution = sub
	 , state_monotype_synotypes    = synotys
	 } =
		Build.unlines
		 [ "monotypes: "
		 , Build.indent "  " sub
		 , "synotypes: " <> build synotys
		 ]
instance Buildable sub => State (State_Monotype sub) where
	state_name _ = "State_Monotype"
	state_show = Build.text
instance Empty sub => Empty (State_Monotype sub) where
	empty = State_Monotype
		 { state_monotype_substitution = empty
		 , state_monotype_synotypes    = empty
		 }

-- * Class 'Solver_Monotype'

-- | A type class for 'Monad's containing a 'Substitution',
-- that may be in an inconsistent state.
class
 ( Solver_Constraint m
 , Monad m
 , MC.MonadState (State_Monotype (Solver_Monotype_Sub m)) m
 , Solver_Monotype_Substitution (Solver_Monotype_Sub m)
 , Infoable Info_Monotype (Info m)
 ) => Solver_Monotype (m :: * -> *) where
	error_monotype :: Error_Monotype -> Error m
	type Solver_Monotype_Sub m
	
	monotype_substitution :: m Substitution_Fixpoint
	monotype_substitution = MC.gets $
	 \(s::State_Monotype (Solver_Monotype_Sub m)) ->
		monotype_substitution_fixpoint $
		state_monotype_substitution s
	
	-- | Lookup the value of a 'Monotype_Var' in the substitution.
	monotype_lookup :: Monovar -> m Monotype
	monotype_lookup v = MC.gets $
	 \(s::State_Monotype (Solver_Monotype_Sub m)) ->
		fromMaybe (Monotype_Var v) $
		substitution_lookup v $
		state_monotype_substitution s
	
	-- | Apply the 'Substitution' to any instance of 'Substitutable'.
	monotype_substitute :: Substitutable a => a -> m a
	monotype_substitute a = do
		let subvars_a = subvars a
		monotys <- monotype_lookup `mapM` subvars_a
		let sub = substitution_finite (List.zip subvars_a monotys)
		return (sub `substitute` a)
	
	-- | Unify two 'Monotype's.
	--
	-- NOTE: In the end, the two 'Monotype's should be equivalent
	-- under 'monotype_substitution'. However, unifying two 'Monotype's
	-- may bring the substitution into an /inconsistent state/.
	monotype_unify :: Info m -> Monotype -> Monotype -> m ()
	monotype_unify info ty1 ty2 = do
		synotys <- synotype_substitution
		subty1 <- monotype_substitute ty1
		subty2 <- monotype_substitute ty2
		case monotype_substitution_unify
		 synotys (ty1, subty1) (ty2, subty2) of
		 Left err ->
			constraint_error_insert
			 (error_monotype $ Error_Monotype_Unification err)
			 info
		 Right (_log, uni) -> -- do
			-- constraint_log "monotype_unify" log
			MC.modify $ \(s::State_Monotype (Solver_Monotype_Sub m)) ->
				s{state_monotype_substitution =
					uni $ state_monotype_substitution s }
	-- | Make 'state_monotype_substitution' consistent.
	--
	-- NOTE: Only relevant for 'Substitution' states
	-- that can be inconsistent
	-- (eg. the /type graph/ substitution state).
	monotype_substitution_consistentify :: m ()
	monotype_substitution_consistentify = return ()
	
	synotype_substitution :: m Synotype_Substitution
	synotype_substitution = MC.gets $
	 \(s::State_Monotype (Solver_Monotype_Sub m)) ->
		state_monotype_synotypes s
	synotype_substitution_set :: Synotype_Substitution -> m ()
	synotype_substitution_set state_monotype_synotypes =
		MC.modify $ \(s::State_Monotype (Solver_Monotype_Sub m)) ->
			s{ state_monotype_synotypes }

-- ** Class 'Solver_Monotype_Substitution'

class
 ( Buildable sub
 , Show sub
 , Monoid sub
 , Substitution sub
 ) => Solver_Monotype_Substitution sub where
	monotype_substitution_fixpoint :: sub -> Substitution_Fixpoint
	monotype_substitution_unify
	 :: Synotype_Substitution
	 -> (Monotype, Monotype)
	 -> (Monotype, Monotype)
	 -> Either Unification_Error (Text, sub -> sub)

instance Solver_Monotype_Substitution Substitution_Finite where
	monotype_substitution_fixpoint = Substitution_Fixpoint
	monotype_substitution_unify synotys (_origty1, ty1) (_origty2, ty2) =
		case mgu_with_synotypes synotys ty1 ty2 of
		 Left err -> Left err
		 Right (_, uni) -> Right $ (Build.text uni,) $ substitution_finite_union uni
instance Solver_Monotype_Substitution Substitution_Fixpoint where
	monotype_substitution_fixpoint = id
	monotype_substitution_unify synotys (origty1, ty1) (origty2, ty2) =
		case mgu_with_synotypes synotys ty1 ty2 of
		 Left err -> Left err
		 Right (was_synexpanded, uni) ->
			Right $ (Build.text uni,) $
				(if was_synexpanded then subexpand else id) .
				subunion uni
			where
			subunion x (Substitution_Fixpoint y) =
				Substitution_Fixpoint $
				(`Map.union` y) $
				Map.fromList
				 [ (v, fromMaybe (Monotype_Var v) $ substitution_lookup v x)
				 | v <- substitution_domain x
				 ]
			subexpand =
				substitution_fixpoint_synexpand synotys origty2 unity .
				substitution_fixpoint_synexpand synotys origty1 unity
			unity =
				fromMaybe (error "monotype_substitution_unify: types not unifiable") $
				mgt_with_synotypes synotys
				 (uni `substitute` ty1)
				 (uni `substitute` ty2)

-- TODO: understand and test this code better…

-- NOTE: Top: The key idea is as follows:
-- try to minimize the number of expansions by 'Synotype's.
-- If a type is expanded, then this should be recorded in the substitution.
-- Invariant of this function should be that "atp" (the first type) can be
-- made equal to "utp" (the second type) with a number of 'Synotype' expansions
substitution_fixpoint_synexpand
 :: Synotype_Substitution
 -> Monotype
 -> Monotype
 -> Substitution_Fixpoint
 -> Substitution_Fixpoint
substitution_fixpoint_synexpand syns =
	go
	where
	go :: Monotype -> Monotype -> Substitution_Fixpoint -> Substitution_Fixpoint
	go atp utp original =
		case (app_spine_left atp, app_spine_left utp) of
		 (App_Spine (Monotype_Var i) [], _) -> writeIntType i utp original
		 (  App_Spine (Monotype_Const s) as
		  , App_Spine (Monotype_Const t) bs
		  ) | s == t && not (is_panthom_synotype syns s) ->
			List.foldr (uncurry go) original (List.zip as bs)
		 (App_Spine (Monotype_Const _) _, _) ->
			case synexpand_top_step (synotypes syns) atp of
			 Just atp' -> go atp' utp original
			 Nothing -> error $ "substitution_fixpoint_synexpand: inconsistent types(1)" <> show (atp, utp)
		 _ -> error $ "substitution_fixpoint_synexpand: inconsistent types(2)" <> show (atp, utp)
	
	writeIntType :: Int -> Monotype -> Substitution_Fixpoint -> Substitution_Fixpoint
	writeIntType i utp original@(Substitution_Fixpoint fm) =
		case Map.lookup i fm of
		 Nothing ->
			case utp of
			 Monotype_Var j | i == j -> original
			 _ -> Substitution_Fixpoint (Map.insert i utp fm)
		 Just atp ->
			case (app_spine_left atp, app_spine_left utp) of
			 (App_Spine (Monotype_Var j) [], _) -> writeIntType j utp original
			 (  App_Spine (Monotype_Const s) as
			  , App_Spine (Monotype_Const t) bs
			  ) | s == t ->
				List.foldr (uncurry go) original (List.zip as bs)
			 (App_Spine (Monotype_Const _) _, _) ->
				case synexpand_top_step (synotypes syns) atp of
				 Just atp' -> writeIntType i utp (Substitution_Fixpoint (Map.insert i atp' fm))
				 Nothing ->
					-- NOTE: Top: FIX!!!   HERSCHRIJVEN!
					-- de volgende situatie trad op:
					--    utp=Categorie, atp = [Char]
					--  met type Categorie = String
					case synexpand_top_step (synotypes syns) utp of
					 Just utp' -> writeIntType i atp (Substitution_Fixpoint (Map.insert i utp' fm))
					 Nothing -> error $ "substitution_fixpoint_synexpand: inconsistent types(1)" <> show (i, utp, atp)
			 _ -> error "substitution_fixpoint_synexpand: inconsistent types(2)"

-- ** Class 'Info_Monotype'

data Info_Monotype
 =   Info_Monotype_Unification Monotype Monotype
 deriving (Eq, Show)

instance Buildable Info_Monotype where
	build x =
		case x of
		 Info_Monotype_Unification m1 m2 ->
			"Info_Monotype_Unification " <> Build.tuple [m1, m2]

-- ** Type 'Error_Monotype'

data Error_Monotype
 =   Error_Monotype_Unification Unification_Error
 deriving (Eq, Show)