{-# LANGUAGE NamedFieldPuns #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
module Language.LOL.Typing.Type.Unification where

import Data.Bool
import Data.Either (Either(..))
import Data.Eq (Eq(..))
import Data.Function (($))
import Data.Functor ((<$>))
import qualified Data.List as List
import qualified Data.Map as Map
import Data.Maybe (Maybe(..), fromMaybe)
import Data.Monoid (Monoid(..), (<>))
import Data.Tuple (snd)
import Prelude (error)
import Text.Show (Show(..))

import Language.LOL.Typing.Type.Monotype
import Language.LOL.Typing.Type.Substitution
import Language.LOL.Typing.Type.Synotype
import Language.LOL.Typing.Lib.Data.Empty (Empty(..))

-- * Type 'Unification'

type Unification
 =   Substitution_Finite

-- | Like 'mgu_with_synotypes', but with an empty 'Synotype_Substitution'.
mgu :: Monotype -> Monotype -> Either Unification_Error Unification
mgu t1 t2 = snd <$> mgu_with_synotypes empty t1 t2

-- | The /most general unification/ ('Substitution') of two 'Monotype's,
--   expanding 'Synotypes' as lazy as possible.
--
-- Example:
--
-- @
--   if String => [Char]
--   then   v11 -> [v11]  `mgu`  String -> [[v14]]
--   should be:
--      [ v11 := [Char] , v14 := Char ]
-- @
--
-- NOTE: the boolean indicates whether expansions were necessary.
mgu_with_synotypes
 :: Synotype_Substitution
 -> Monotype -> Monotype
 -> Either Unification_Error (Bool, Unification)
mgu_with_synotypes syns = go mempty
	where
	err s = error $ "mgu_with_synotypes: " <> s
	go sub t1 t2 =
		case (app_spine_left t1, app_spine_left t2) of
		 (App_Spine (Monotype_Var v) [], _) -> go_Var sub v t2
		 (_, App_Spine (Monotype_Var v) []) -> go_Var sub v t1
		 (  App_Spine (Monotype_Const c1) s1
		  , App_Spine (Monotype_Const c2) s2 )
		  | c1 == c2 && not (is_panthom_synotype syns c1) ->
			go_List sub s1 s2
		  | otherwise ->
			case synexpand_top_step_ordered syns (t1, t2) of
			 Nothing -> Left $ Unification_Error_Constant_clash c1 c2
			 Just (t1', t2') ->
				case go sub t1' t2' of
				 Left e -> Left e
				 Right (_, sub') -> Right (True, sub')
		 _ -> case (t1, t2) of
			 (Monotype_App l1 r1, Monotype_App l2 r2) ->
				go_List sub [l1, r1] [l2, r2]
			 _ ->  err "illegal type"
	go_Var sub v ty =
		case Map.lookup v sub of
		 Just t2 ->
			case go sub ty t2 of
			 Right (True, sub') ->
				let mgt =
					fromMaybe (err "illegal types") $
					mgt_with_synotypes syns
					 (sub' `substitute` ty)
					 (sub' `substitute` t2) in
				Right
				 ( True
				 , substitution_finite_union
					 (substitution_finite_singleton v mgt)
					 (substitution_domain_remove [v] sub')
				 )
			 e -> e
		 Nothing ->
			case sub `substitute` ty of
			 Monotype_Var v' | v == v' -> Right (False, sub)
			 ty' | v `List.elem` subvars ty' -> Left (Unification_Error_Infinite_type v)
			     | otherwise -> Right (False, substitution_finite_singleton v ty' `substitution_finite_union` sub)
	go_List sub [] [] = Right (False, sub)
	go_List sub (s:ss) (t:tt) =
		case go sub s t of
		 Left e -> Left e
		 Right (b,sub') ->
			case go_List sub' ss tt of
			 Left e -> Left e
			 Right (b', sub'') -> Right (b || b', sub'')
	go_List _ _ _ = err "kinds do not match"

-- | Given a set of 'Synotype_Substitution', can two types be unified?
unifiable :: Synotype_Substitution -> Monotype -> Monotype -> Bool
unifiable syns t1 t2 =
	case mgu_with_synotypes syns t1 t2 of
	 Left  _ -> False
	 Right _ -> True

-- | Same as unifiable, but takes as input a list of 'Monotype's
unifiables :: Synotype_Substitution -> [Monotype] -> Bool
unifiables syns (t1:t2:ts) =
	case mgu_with_synotypes syns t1 t2 of
	 Left _         -> False
	 Right (_, sub) -> unifiables syns (sub `substitute` (t2:ts))
unifiables _ _ = True

-- ** Type 'Unification_Error'

-- | Reasons why two 'Monotype's cannot be unified.
data Unification_Error
 =   Unification_Error_Constant_clash Monoconst Monoconst
     -- ^ Two different 'Monoconst's clash (they should be the same).
 |   Unification_Error_Infinite_type Monovar
     -- ^ A 'Monotype_Var' is unified with a composed 'Monotype'
     --   which contains this same 'Monotype_Var'.
 deriving (Eq, Show)