{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=6 #-}
-- | Symantic for 'Integer'.
module Language.Symantic.Lib.Integer where

import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import qualified Data.Text as Text

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming
import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))

-- * Class 'Sym_Integer'
class Sym_Integer term where
	integer :: Integer -> term Integer
	default integer :: Trans t term => Integer -> t term Integer
	integer = trans_lift . integer

type instance Sym_of_Iface (Proxy Integer) = Sym_Integer
type instance TyConsts_of_Iface (Proxy Integer) = Proxy Integer ': TyConsts_imported_by (Proxy Integer)
type instance TyConsts_imported_by (Proxy Integer) =
 [ Proxy Enum
 , Proxy Eq
 , Proxy Integral
 , Proxy Num
 , Proxy Ord
 , Proxy Real
 , Proxy Show
 ]

instance Sym_Integer HostI where
	integer = HostI
instance Sym_Integer TextI where
	integer a = TextI $ \_p _v ->
		Text.pack (show a)
instance (Sym_Integer r1, Sym_Integer r2) => Sym_Integer (DupI r1 r2) where
	integer x = integer x `DupI` integer x

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

instance Proj_TyFamC cs TyFam_MonoElement Integer

instance -- Proj_TyConC
 ( Proj_TyConst cs Integer
 , Proj_TyConsts cs (TyConsts_imported_by (Proxy Integer))
 ) => Proj_TyConC cs (Proxy Integer) where
	proj_TyConC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
	 , Just Refl <- proj_TyConst c (Proxy @Integer)
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Enum)     -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Eq)       -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Integral) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Num)      -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Ord)      -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Real)     -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Show)     -> Just TyCon
		 _ -> Nothing
	proj_TyConC _c _q = Nothing
data instance TokenT meta (ts::[*]) (Proxy Integer)
 = Token_Term_Integer Integer
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Integer))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Integer))

instance -- CompileI
 Inj_TyConst cs Integer =>
 CompileI cs is (Proxy Integer) where
	compileI tok _ctx k =
		case tok of
		 Token_Term_Integer i -> k (ty @Integer) $ TermO $ \_c -> integer i
instance -- TokenizeT
 -- Inj_Token meta ts Integer =>
 TokenizeT meta ts (Proxy Integer)
instance -- Gram_Term_AtomsT
 ( Alt g
 , Alter g
 , Gram_Rule g
 , Gram_Lexer g
 , Gram_Meta meta g
 , Inj_Token meta ts Integer
 ) => Gram_Term_AtomsT meta ts (Proxy Integer) g where
	gs_term_atomsT _t =
	 [ rule "term_integer" $
		lexeme $ metaG $
		(\i meta -> ProTok $ inj_EToken meta $ Token_Term_Integer $ read i)
		 <$> some (choice $ char <$> ['0'..'9'])
	 ]