{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Eq'.
module Language.Symantic.Compiling.Eq where

import Control.Monad
import qualified Data.Eq as Eq
import Data.Proxy (Proxy(..))
import Data.String (IsString)
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding ((==), (/=))

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Compiling.Bool
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * Class 'Sym_Eq'
class Sym_Eq term where
	(==) :: Eq a => term a -> term a -> term Bool
	(/=) :: Eq a => term a -> term a -> term Bool
	
	default (==) :: (Trans t term, Eq a) => t term a -> t term a -> t term Bool
	default (/=) :: (Trans t term, Eq a) => t term a -> t term a -> t term Bool
	
	(==) = trans_map2 (==)
	(/=) = trans_map2 (/=)

infix 4 ==
infix 4 /=

type instance Sym_of_Iface (Proxy Eq) = Sym_Eq
type instance Consts_of_Iface (Proxy Eq) = Proxy Eq ': Consts_imported_by Eq
type instance Consts_imported_by Eq = '[]

instance Sym_Eq HostI where
	(==) = liftM2 (Eq.==)
	(/=) = liftM2 (Eq./=)
instance Sym_Eq TextI where
	(==) = textI_infix "==" (Precedence 4)
	(/=) = textI_infix "/=" (Precedence 4)
instance (Sym_Eq r1, Sym_Eq r2) => Sym_Eq (DupI r1 r2) where
	(==) = dupI2 sym_Eq (==)
	(/=) = dupI2 sym_Eq (/=)

instance Const_from Text cs => Const_from Text (Proxy Eq ': cs) where
	const_from "Eq" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Show_Const cs => Show_Const (Proxy Eq ': cs) where
	show_const ConstZ{} = "Eq"
	show_const (ConstS c) = show_const c

instance -- Proj_ConC
 Proj_ConC cs (Proxy Eq)
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Inj_Const (Consts_of_Ifaces is) Bool
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Inj_Const (Consts_of_Ifaces is) Eq
 , Proj_Con (Consts_of_Ifaces is)
 , Term_from is ast
 ) => Term_fromI is (Proxy Eq) ast where
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "=="  -> op2_from (==)
		 "/="  -> op2_from (/=)
		 _ -> Left $ Error_Term_unsupported
		where
		op2_from (op::forall term a. (Sym_Eq term, Eq a) => term a -> term a -> term Bool) =
			case ast_nodes ast of
			 [] -> Left $ Error_Term_Syntax $
				Error_Syntax_more_arguments_needed $ At (Just ast) 1
			 [ast_x] ->
				term_from ast_x ctx $ \ty_x (TermLC x) ->
				check_constraint (At (Just ast_x) (tyEq :$ ty_x)) $ \Con ->
				k (ty_x ~> tyBool) $ TermLC $
				 \c -> lam $ op (x c)
			 [ast_x, ast_y] ->
				term_from ast_x ctx $ \ty_x (TermLC x) ->
				check_constraint (At (Just ast_x) (tyEq :$ ty_x)) $ \Con ->
				term_from ast_y ctx $ \ty_y (TermLC y) ->
				check_type (At (Just ast_x) ty_x) (At (Just ast_y) ty_y) $ \Refl ->
				k tyBool $ TermLC $
				 \c -> op (x c) (y c)
			 _ -> Left $ Error_Term_Syntax $
				Error_Syntax_too_many_arguments $ At (Just ast) 2

-- | The 'Eq' 'Type'
tyEq :: Inj_Const cs Eq => Type cs Eq
tyEq = TyConst inj_const

sym_Eq :: Proxy Sym_Eq
sym_Eq = Proxy

syEq :: IsString a => [Syntax a] -> Syntax a
syEq = Syntax "Eq"