{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
-- | Constraints for /monomorphic types/.
module Language.LOL.Typing.Constraint.Monotype where

import Control.Applicative (Applicative(..))
import Data.Eq (Eq(..))
import Data.Function (on)
import Data.Functor (Functor(..), (<$>))
import qualified Data.List as List
import Data.Monoid ((<>))
import Data.Text.Buildable (Buildable(..))
import Text.Show (Show(..))

import Language.LOL.Typing.Type
import Language.LOL.Typing.Solver

-- * Type 'Constraint_Monotype_Unification'

-- | /monotype constraint/.
data Constraint_Monotype info
 =   Constraint_Monotype_Unification Monotype Monotype info
     -- ^ A /monotype unification constraint/.
 deriving (Show)

-- | Infix alias for 'Constraint_Monotype_Unification'.
(.==.) :: Monotype -> Monotype -> info -> Constraint_Monotype info
(.==.) = Constraint_Monotype_Unification

instance Buildable info => Buildable (Constraint_Monotype info) where
	build (Constraint_Monotype_Unification t1 t2 info) =
		build t1 <> " == " <> build t2 <> build_info
		where
		build_info = " {- " <> build info <> " -}"
instance Functor Constraint_Monotype where
	fmap f (Constraint_Monotype_Unification t1 t2 info) =
		Constraint_Monotype_Unification t1 t2 (f info)
instance Substitutable (Constraint_Monotype info) where
	subvars (Constraint_Monotype_Unification t1 t2 _) = subvars t1 `List.union` subvars t2
	sub `substitute` (Constraint_Monotype_Unification t1 t2 info) =
		Constraint_Monotype_Unification (sub `substitute` t1) (sub `substitute` t2) info
instance
 ( info ~ Info m
 , Show info
 , Buildable info
 , Solver_Constraint m
 , Solver_Monotype m
 , Solver_Polytype m
 ) => Solvable (Constraint_Monotype info) m where
	constraint_solver (Constraint_Monotype_Unification t1 t2 info) =
		monotype_unify
		 (info_insert (Info_Monotype_Unification t1 t2) info)
		 t1 t2
	constraint_checker (Constraint_Monotype_Unification t1 t2 _) = do
		Synotype_Substitution{synotypes} <- synotype_substitution
		((==) `on` synexpand synotypes)
		 <$> monotype_substitute t1
		 <*> monotype_substitute t2