{-# 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 'Bool'.
module Language.Symantic.Compiling.Bool where

import Control.Monad
import qualified Data.Bool as Bool
import Data.Monoid
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import qualified Data.Text as Text
import Prelude hiding ((&&), not, (||))

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

-- * Class 'Sym_Bool'
-- | Symantic.
class Sym_Bool term where
	bool ::      Bool -> term Bool
	not  :: term Bool -> term Bool
	(&&) :: term Bool -> term Bool -> term Bool
	(||) :: term Bool -> term Bool -> term Bool
	xor  :: term Bool -> term Bool -> term Bool
	xor x y = (x || y) && not (x && y)
	
	default bool :: Trans t term =>        Bool -> t term Bool
	default not  :: Trans t term => t term Bool -> t term Bool
	default (&&) :: Trans t term => t term Bool -> t term Bool -> t term Bool
	default (||) :: Trans t term => t term Bool -> t term Bool -> t term Bool
	
	bool = trans_lift . bool
	not  = trans_map1 not
	(&&) = trans_map2 (&&)
	(||) = trans_map2 (||)

infixr 2 ||
infixr 2 `xor`
infixr 3 &&

type instance Sym_of_Iface (Proxy Bool) = Sym_Bool

instance Sym_Bool HostI where
	bool = HostI
	not  = liftM Bool.not
	(&&) = liftM2 (Bool.&&)
	(||) = liftM2 (Bool.||)
instance Sym_Bool TextI where
	bool a = TextI $ \_p _v ->
		Text.pack (show a)
	not (TextI x) =
		TextI $ \p v ->
			let p' = Precedence 9 in
			paren p p' $ "not " <> x p' v
	(&&) = textI_infix "&&"    (Precedence 6)
	(||) = textI_infix "||"    (Precedence 5)
	xor  = textI_infix "`xor`" (Precedence 5)
instance (Sym_Bool r1, Sym_Bool r2) => Sym_Bool (DupI r1 r2) where
	bool x = bool x `DupI` bool x
	not  = dupI1 sym_Bool not
	(&&) = dupI2 sym_Bool (&&)
	(||) = dupI2 sym_Bool (||)
	xor  = dupI2 sym_Bool xor

sym_Bool :: Proxy Sym_Bool
sym_Bool = Proxy

instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Inj_Const (Consts_of_Ifaces is) Bool
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Term_from is ast
 ) => Term_fromI is (Proxy Bool) ast where
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "True"  -> k tyBool $ Term_of_LamCtx $ \_c -> bool True
		 "False" -> k tyBool $ Term_of_LamCtx $ \_c -> bool False
		 "not" -> op1_from not
		 "&&"  -> op2_from (&&)
		 "||"  -> op2_from (||)
		 "xor" -> op2_from xor
		 _ -> Left $ Error_Term_unsupported
		where
		op1_from (op::forall term. Sym_Bool term => term Bool -> term Bool) =
			case ast_nodes ast of
			 [] -> k (tyBool ~> tyBool) $ Term_of_LamCtx $
				 \_c -> lam op
			 [ast_x] ->
				term_from ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
				check_type (At Nothing tyBool) (At (Just ast_x) ty_x) $ \Refl ->
				k tyBool $ Term_of_LamCtx $
				 \c -> op (x c)
			 _ -> Left $ Error_Term_Syntax $
				Error_Syntax_too_many_arguments $ At (Just ast) 1
		op2_from (op::forall term. Sym_Bool term => term Bool -> term Bool -> term Bool) =
			case ast_nodes ast of
			 [] -> k (tyBool ~> tyBool ~> tyBool) $ Term_of_LamCtx $
				 \_c -> lam $ lam . op
			 [ast_x] ->
				term_from ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
				check_type (At Nothing tyBool) (At (Just ast_x) ty_x) $ \Refl ->
				k (tyBool ~> tyBool) $ Term_of_LamCtx $
				 \c -> lam $ op (x c)
			 [ast_x, ast_y] ->
				term_from ast_x ctx $ \ty_x (Term_of_LamCtx x) ->
				term_from ast_y ctx $ \ty_y (Term_of_LamCtx y) ->
				check_type (At Nothing tyBool) (At (Just ast_x) ty_x) $ \Refl ->
				check_type (At Nothing tyBool) (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