{-# 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.Type.Equality ((:~:)(Refl))
import Prelude hiding ((==), (/=))

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

-- * Class 'Sym_Eq'
-- | Symantic.
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

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 (/=)

sym_Eq :: Proxy Sym_Eq
sym_Eq = Proxy

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 (Term_of_LamCtx x) ->
				check_constraint (At (Just ast_x) (tyEq :$ ty_x)) $ \Con ->
				k (ty_x ~> tyBool) $ Term_of_LamCtx $
				 \c -> lam $ op (x c)
			 [ast_x, ast_y] ->
				term_from ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
				check_constraint (At (Just ast_x) (tyEq :$ ty_x)) $ \Con ->
				term_from ast_y ctx $ \ty_y (Term_of_LamCtx y) ->
				check_type (At (Just ast_x) ty_x) (At (Just ast_y) ty_y) $ \Refl ->
				k tyBool $ Term_of_LamCtx $
				 \c -> op (x c) (y c)
			 _ -> Left $ Error_Term_Syntax $
				Error_Syntax_too_many_arguments $ At (Just ast) 2