{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
-- {-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module TFHOE.Expr.Bool where

import Data.Proxy (Proxy(..))
import Prelude hiding (and, or)

import TFHOE.Raw
import TFHOE.Type
import TFHOE.Expr.Common
import TFHOE.Expr.Fun ()
import TFHOE.Repr.Dup

-- * Class 'Expr_Bool'

-- | Symantics combinable with 'Type_Bool'.
class Expr_Bool repr where
	bool :: Bool -> repr Bool
	neg :: repr Bool -> repr Bool
	and :: repr Bool -> repr Bool -> repr Bool
	or  :: repr Bool -> repr Bool -> repr Bool
	xor :: repr Bool -> repr Bool -> repr Bool
	xor x y = (x `or` y) `and` neg (x `and` y)

type instance Expr_from_Type (Type_Bool next) repr
 = ( Expr_Bool repr
   , Expr_from_Type next repr )

instance -- Expr_Bool Dup
 ( Expr_Bool r1
 , Expr_Bool r2
 ) => Expr_Bool (Dup r1 r2) where
	bool x = bool x `Dup` bool x
	neg (x1 `Dup` x2)               = neg x1    `Dup` neg x2
	and (x1 `Dup` x2) (y1 `Dup` y2) = and x1 y1 `Dup` and x2 y2
	or  (x1 `Dup` x2) (y1 `Dup` y2) = or  x1 y1 `Dup` or  x2 y2
	xor (x1 `Dup` x2) (y1 `Dup` y2) = xor x1 y1 `Dup` xor x2 y2
instance -- Expr_from Raw Type_Bool Type_Fun_Bool
 ( Type_from Raw next
 , Expr_from Raw next (Type_Fun_Bool fun next)
 ) => Expr_from Raw (Type_Bool next) (Type_Fun_Bool fun next) where
	expr_from _px_ty _px_ty_end _ctx (Raw "bool" [Raw raw_bool []]) k = do
		(i::Bool) <- read_safe raw_bool
		k (Type_Fun_Next Type_Bool) $ Forall_Repr_with_Context $
			const $ bool i
	expr_from _px_ty px_ty_end ctx (Raw "neg" [raw_x]) k =
		expr_from px_ty_end px_ty_end ctx raw_x $ \ty_x (Forall_Repr_with_Context x) ->
			case ty_x of
			 Type_Fun_Next Type_Bool ->
				k ty_x $ Forall_Repr_with_Context $
					neg . x
			 _ -> Left "Error: neg: the operand is not a Bool"
	expr_from _px_ty px_ty_end ctx (Raw op_name@"and" [raw_x, raw_y]) k =
		expr_from px_ty_end px_ty_end ctx raw_x $ \ty_x (Forall_Repr_with_Context x) ->
		expr_from px_ty_end px_ty_end ctx raw_y $ \ty_y (Forall_Repr_with_Context y) ->
			case (ty_x, ty_y) of
			 (  Type_Fun_Next Type_Bool
			  , Type_Fun_Next Type_Bool ) ->
				k ty_x $ Forall_Repr_with_Context $
				 \c -> x c `and` y c
			 _ -> Left $ "Error: "++op_name++": at least one operand is not a Bool"
	expr_from _px_ty px_ty_end ctx (Raw op_name@"or" [raw_x, raw_y]) k =
		expr_from px_ty_end px_ty_end ctx raw_x $ \ty_x (Forall_Repr_with_Context x) ->
		expr_from px_ty_end px_ty_end ctx raw_y $ \ty_y (Forall_Repr_with_Context y) ->
			case (ty_x, ty_y) of
			 (  Type_Fun_Next Type_Bool
			  , Type_Fun_Next Type_Bool ) ->
				k ty_x $ Forall_Repr_with_Context $
				 \c -> x c `or` y c
			 _ -> Left $ "Error: "++op_name++": at least one operand is not a Bool"
	expr_from _px_ty px_ty_end ctx (Raw op_name@"xor" [raw_x, raw_y]) k =
		expr_from px_ty_end px_ty_end ctx raw_x $ \ty_x (Forall_Repr_with_Context x) ->
		expr_from px_ty_end px_ty_end ctx raw_y $ \ty_y (Forall_Repr_with_Context y) ->
			case (ty_x, ty_y) of
			 (  Type_Fun_Next Type_Bool
			  , Type_Fun_Next Type_Bool ) ->
				k ty_x $ Forall_Repr_with_Context $
				 \c -> x c `xor` y c
			 _ -> Left $ "Error: "++op_name++": at least one operand is not a Bool"
	expr_from _px_ty px_ty_end ctx raw k =
		expr_from (Proxy::Proxy next) px_ty_end ctx raw k
instance Expr_from Raw Type_End (Type_Fun_Bool fun Type_End) where
	expr_from _px_ty _px_ty_end _ctx raw _k =
		Left $ "Error: invalid Type_Fun_Bool: " ++ show raw

expr_fun_bool_from
 :: forall fun raw next.
 ( Expr_from raw (Type_Fun_Bool fun next)
                 (Type_Fun_Bool fun next)
 )
 => Proxy fun
 -> Proxy next
 -> raw
 -> Either Error_Type
           (Exists_Type_and_Repr
            (Type_Fun_Bool fun next)
            (Forall_Repr (Type_Fun_Bool fun next)))
expr_fun_bool_from _px_call _px_next raw =
	expr_from
	 (Proxy::Proxy (Type_Fun_Bool fun next))
	 (Proxy::Proxy (Type_Fun_Bool fun next))
	 Context_Empty raw $ \ty (Forall_Repr_with_Context repr) ->
		Right $ Exists_Type_and_Repr ty $
			Forall_Repr $ repr Context_Empty