{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
-- {-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

module Hcompta.Expr.Bool where

import Data.Bool
-- import Data.Either (Either(..))
-- import Data.Function (($), (.))
-- import Data.Maybe (Maybe(..))
-- import Data.Monoid ((<>))
-- import Data.Proxy (Proxy(..))
-- import Data.String (String)
-- import Data.Type.Equality ((:~:)(Refl))
-- import Text.Show (Show(..))

import Hcompta.Expr.Dup
-- import Hcompta.Expr.Fun
-- import Hcompta.Expr.Lit

-- * Class 'Expr_Bool'

-- | /Tagless-final symantics/ for usual logical boolean operators.
class Expr_Bool repr where
	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)

instance -- Expr_Bool Dup
 ( Expr_Bool r1
 , Expr_Bool r2
 ) => Expr_Bool (Dup r1 r2) where
	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

{-
instance -- Expr_from Tree
 ( Expr_Bool repr
 , Type_from Tree next
 , Expr_from Tree repr next (Type_Lit Bool repr next)
 ) => Expr_from Tree repr   (Type_Lit Bool repr next)
                            (Type_Fun_Lit Bool repr next) where
	expr_from _pty pvar ctx (Raw "And" [raw_x, raw_y]) k =
		expr_from pvar pvar ctx raw_x $ \ty_x (x::Repr_HO repr _ctx _h_x) ->
		expr_from pvar pvar ctx raw_y $ \ty_y (y::Repr_HO repr _ctx _h_y) ->
			case (ty_x, ty_y) of
			 (  Type_Fun_Next Type_Int
			  , Type_Fun_Next Type_Int ) ->
				k (Type_Fun_Next Type_Int) $ \c -> and (x c) (y c)
			 _ -> Left "Error: And: at least one operand is not an Int"
	expr_from _pty pvar ctx raw k =
		expr_from (Proxy::Proxy next) pvar ctx raw k
-}

{-
-- * Type 'Type_Bool'

-- | GADT for boolean type:
--
-- * singleton (bijective mapping between Haskell type @h@ and the GADT's terms),
-- * and extensible (through @next@).
data Type_Bool (next:: * -> *) h where
	Type_Bool      :: Type_Bool next Bool
	Type_Bool_Next :: next h -> Type_Bool next h
type Type_Fun_Lit_Bool repr next = Type_Fun repr (Type_Bool next)
type Type_Fun_Lit_Bool_End repr  = Type_Fun_Lit_Bool repr Type_Bool_End

instance -- Type_Eq
 Type_Eq next =>
 Type_Eq (Type_Bool next) where
	type_eq Type_Bool
	        Type_Bool = Just Refl
	type_eq (Type_Bool_Next x)
	        (Type_Bool_Next y) = x `type_eq` y
	type_eq _ _ = Nothing
instance -- Type_from Tree
 Type_from Tree next =>
 Type_from Tree (Type_Bool next) where
	type_from (Tree "Bool" []) k = k Type_Bool
	type_from raw k = type_from raw $ k . Type_Bool_Next
instance -- From_Type String
 From_Type String next =>
 From_Type String (Type_Bool next) where
	from_type Type_Bool = "Bool"
	from_type (Type_Bool_Next t) = from_type t
--instance -- Show
-- From_Type String next =>
-- Show (Type_Bool next h) where
--	show = from_type

-- ** Type 'Type_Bool_End'

data Type_Bool_End h where
	Type_Bool_End :: Type_Bool_End ()

instance -- Type_Eq
 Type_Eq Type_Bool_End where
	type_eq Type_Bool_End
	        Type_Bool_End = Just Refl
instance -- Type_from Tree
 Type_from Tree Type_Bool_End where
	type_from _ k = k Type_Bool_End
instance -- Expr_from Tree
 Show raw =>
 Expr_from raw repr Type_Bool_End (Type_Fun_Lit_Bool repr Type_Bool_End) where
	expr_from _pty _pvar _ctx raw _k =
		Left $ "Error: invalid: " <> show raw


fun_lit_bool_from
 :: forall next raw repr ret.
 ( Expr_from raw repr (Type_Fun_Lit_Bool repr next) (Type_Fun_Lit_Bool repr next)
 -- , Expr_from raw repr next (Type_Fun_Lit_Bool repr next)
 , Expr_Fun repr
 , Expr_Lit repr
 , Type_from raw next
 )
 => Proxy next
 -> raw
 -> (forall h. Type_Fun_Lit_Bool repr next h -> repr h -> Either Error_Type ret)
 -> Either Error_Type ret
fun_lit_bool_from _pty raw k =
	expr_from
	 (Proxy::Proxy (Type_Fun_Lit_Bool repr next))
	 (Proxy::Proxy (Type_Fun_Lit_Bool repr next))
	 Context_Type_Empty raw $ \ty repr ->
		k ty $ repr Context_Type_Empty
-}