{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Enum'.
module Language.Symantic.Lib.Enum where

import Control.Monad (liftM)
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import Prelude (Enum)
import Prelude hiding (Enum(..))
import qualified Data.Function as Fun
import qualified Prelude

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming
import Language.Symantic.Lib.Lambda

-- * Class 'Sym_Enum'
class Sym_Enum term where
	toEnum   :: Enum a => term Int -> term a
	fromEnum :: Enum a => term a -> term Int
	succ     :: Enum a => term a -> term a
	pred     :: Enum a => term a -> term a
	
	default succ     :: (Trans t term, Enum a) => t term a -> t term a
	default pred     :: (Trans t term, Enum a) => t term a -> t term a
	default toEnum   :: (Trans t term, Enum a) => t term Int -> t term a
	default fromEnum :: (Trans t term, Enum a) => t term a -> t term Int
	
	toEnum   = trans_map1 toEnum
	fromEnum = trans_map1 fromEnum
	succ     = trans_map1 succ
	pred     = trans_map1 pred

type instance Sym_of_Iface (Proxy Enum) = Sym_Enum
type instance TyConsts_of_Iface (Proxy Enum) = Proxy Enum ': TyConsts_imported_by (Proxy Enum)
type instance TyConsts_imported_by (Proxy Enum) =
 '[ Proxy Int
 ]

instance Sym_Enum HostI where
	toEnum   = liftM Prelude.toEnum
	fromEnum = liftM Prelude.fromEnum
	succ     = liftM Prelude.succ
	pred     = liftM Prelude.pred
instance Sym_Enum TextI where
	toEnum   = textI1 "toEnum"
	fromEnum = textI1 "fromEnum"
	succ     = textI1 "succ"
	pred     = textI1 "pred"
instance (Sym_Enum r1, Sym_Enum r2) => Sym_Enum (DupI r1 r2) where
	toEnum   = dupI1 @Sym_Enum toEnum
	fromEnum = dupI1 @Sym_Enum fromEnum
	succ     = dupI1 @Sym_Enum succ
	pred     = dupI1 @Sym_Enum pred

instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs Enum
 ) => Read_TyNameR TyName cs (Proxy Enum ': rs) where
	read_TyNameR _cs (TyName "Enum") k = k (ty @Enum)
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy Enum ': cs) where
	show_TyConst TyConstZ{} = "Enum"
	show_TyConst (TyConstS c) = show_TyConst c

instance Proj_TyConC cs (Proxy Enum)
data instance TokenT meta (ts::[*]) (Proxy Enum)
 = Token_Term_Enum_fromEnum (EToken meta ts)
 | Token_Term_Enum_toEnum   (EToken meta '[Proxy Token_Type])
 | Token_Term_Enum_succ     (EToken meta ts)
 | Token_Term_Enum_pred     (EToken meta ts)
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Enum))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Enum))

instance -- CompileI
 ( Read_TyName TyName cs
 , Inj_TyConst        cs Enum
 , Inj_TyConst        cs (->)
 , Inj_TyConst        cs Int
 , Proj_TyCon         cs
 , Compile cs is
 ) => CompileI cs is (Proxy Enum) where
	compileI tok ctx k =
		case tok of
		 Token_Term_Enum_toEnum tok_ty_a ->
			-- toEnum :: Enum a => Int -> a
			compile_Type tok_ty_a $ \(ty_a::Type cs a) ->
			check_Kind
			 (At Nothing SKiType)
			 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
			check_TyCon (At (Just tok_ty_a) (ty @Enum :$ ty_a)) $ \TyCon ->
			k (ty @Int ~> ty_a) $ Term $
				Fun.const $ lam toEnum
		 Token_Term_Enum_fromEnum tok_a ->
			-- fromEnum :: Enum a => a -> Int
			compile tok_a ctx $ \ty_a (Term a) ->
			check_TyCon (At (Just tok_a) (ty @Enum :$ ty_a)) $ \TyCon ->
			k (ty @Int) $ Term $
				\c -> fromEnum (a c)
		 Token_Term_Enum_succ tok_a -> op1_from tok_a succ
		 Token_Term_Enum_pred tok_a -> op1_from tok_a pred
		where
		op1_from tok_a
		 (op::forall term a. (Sym_Enum term, Enum a)
			 => term a -> term a) =
		 -- succ :: Enum a => a -> a
		 -- pred :: Enum a => a -> a
			compile tok_a ctx $ \ty_a (Term x) ->
			check_TyCon (At (Just tok_a) (ty @Enum :$ ty_a)) $ \TyCon ->
			k ty_a $ Term $
			 \c -> op (x c)
instance -- TokenizeT
 Inj_Token meta ts Enum =>
 TokenizeT meta ts (Proxy Enum) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize1 "succ" infixN5 Token_Term_Enum_succ
		 , tokenize1 "pred" infixN5 Token_Term_Enum_pred
		 , (TeName "toEnum",) ProTok_Term
			 { protok_term = \meta -> ProTokPi $ \a ->
				ProTok $ inj_EToken meta $ Token_Term_Enum_toEnum a
			 , protok_fixity = infixN5
			 }
		 , tokenize1 "fromEnum" infixN5 Token_Term_Enum_fromEnum
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Enum) g