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

import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import Prelude as Bounded (Bounded)
import Prelude hiding (Bounded(..))
import qualified Data.Function as Fun
import qualified Prelude as Bounded

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

-- * Class 'Sym_Bounded'
class Sym_Bounded term where
	minBound :: Bounded a => term a
	maxBound :: Bounded a => term a
	default minBound :: (Trans t term, Bounded a) => t term a
	default maxBound :: (Trans t term, Bounded a) => t term a
	minBound = trans_lift minBound
	maxBound = trans_lift maxBound

type instance Sym_of_Iface (Proxy Bounded) = Sym_Bounded
type instance TyConsts_of_Iface (Proxy Bounded) = Proxy Bounded ': TyConsts_imported_by (Proxy Bounded)
type instance TyConsts_imported_by (Proxy Bounded) = '[]

instance Sym_Bounded HostI where
	minBound = HostI Bounded.minBound
	maxBound = HostI Bounded.maxBound
instance Sym_Bounded TextI where
	minBound = textI0 "minBound"
	maxBound = textI0 "maxBound"
instance (Sym_Bounded r1, Sym_Bounded r2) => Sym_Bounded (DupI r1 r2) where
	minBound = dupI0 @Sym_Bounded minBound
	maxBound = dupI0 @Sym_Bounded maxBound

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

instance Proj_TyConC cs (Proxy Bounded)
data instance TokenT meta (ts::[*]) (Proxy Bounded)
 = Token_Term_Bounded_minBound (EToken meta '[Proxy Token_Type])
 | Token_Term_Bounded_maxBound (EToken meta '[Proxy Token_Type])
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Bounded))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Bounded))

instance -- CompileI
 ( Read_TyName TyName cs
 , Inj_TyConst        cs Bounded
 , Proj_TyCon         cs
 , Compile cs is
 ) => CompileI cs is (Proxy Bounded) where
	compileI tok _ctx k =
		case tok of
		 Token_Term_Bounded_minBound tok_ty_a -> bound minBound tok_ty_a
		 Token_Term_Bounded_maxBound tok_ty_a -> bound maxBound tok_ty_a
		where
		bound (bnd::forall term a. (Sym_Bounded term, Bounded a) => term a) tok_ty_a =
		 -- minBound :: Bounded a => a
		 -- maxBound :: Bounded a => 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 @Bounded :$ ty_a)) $ \TyCon ->
			k ty_a $ Term $ Fun.const bnd
instance -- TokenizeT
 Inj_Token meta ts Bounded =>
 TokenizeT meta ts (Proxy Bounded) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ (TeName "minBound",) ProTok_Term
			 { protok_term = \meta -> ProTokPi $ \a ->
				ProTokTe $ inj_EToken meta $ Token_Term_Bounded_minBound a
			 , protok_fixity = infixN5
			 }
		 , (TeName "maxBound",) ProTok_Term
			 { protok_term = \meta -> ProTokPi $ \a ->
				ProTokTe $ inj_EToken meta $ Token_Term_Bounded_maxBound a
			 , protok_fixity = infixN5
			 }
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Bounded) g