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

import Data.Proxy (Proxy(..))

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

-- * Class 'Expr_Int'

-- | Symantics combinable with 'Type_Int'.
class Expr_Int repr where
	int :: Int -> repr Int
	add :: repr Int -> repr Int -> repr Int

type instance Expr_from_Type (Type_Int next) repr
 = ( Expr_Int repr
   , Expr_from_Type next repr )

instance -- Expr_Int Dup
 ( Expr_Int r1
 , Expr_Int r2
 ) => Expr_Int (Dup r1 r2) where
	int x = int x `Dup` int x
	add (x1 `Dup` x2) (y1 `Dup` y2) = add x1 y1 `Dup` add x2 y2
instance -- Expr_from Raw
 ( Type_from Raw next
 , Expr_from Raw next (Type_Fun_Bool_Int fun next)
 ) => Expr_from Raw (Type_Int next)
                    (Type_Fun_Bool_Int fun next) where
	expr_from _px_ty _px_ty_end _ctx (Raw "int" [Raw raw_int []]) k = do
		(i::Int) <- read_safe raw_int
		k (Type_Fun_Next $ Type_Bool_Next Type_Int) $ Forall_Repr_with_Context $
		 \_c -> int i
	expr_from _px_ty px_ty_end ctx (Raw "add" [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_Next Type_Int)
			  , Type_Fun_Next (Type_Bool_Next Type_Int) ) ->
				k ty_x $ Forall_Repr_with_Context $
				 \c -> x c `add` y c
			 _ -> Left "Error: add: at least one operand is not an Int"
	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_Int repr Type_End) where
	expr_from _px_ty _px_ty_end _ctx raw _k =
		Left $ "Error: invalid Type_Fun_Bool_Int: " ++ show raw

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