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

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

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

-- * Class 'Sym_Int'
class Sym_Int term where
	int :: Int -> term Int
	default int :: Trans t term => Int -> t term Int
	int = trans_lift . int

type instance Sym_of_Iface (Proxy Int) = Sym_Int
type instance Consts_of_Iface (Proxy Int) = Proxy Int ': Consts_imported_by Int
type instance Consts_imported_by Int =
 [ Proxy Bounded
 , Proxy Enum
 , Proxy Eq
 , Proxy Integral
 , Proxy Num
 , Proxy Ord
 , Proxy Real
 , Proxy Show
 ]

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

instance
 ( Read_TypeNameR Type_Name cs rs
 , Inj_Const cs Int
 ) => Read_TypeNameR Type_Name cs (Proxy Int ': rs) where
	read_typenameR _cs (Type_Name "Int") k = k (ty @Int)
	read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy Int ': cs) where
	show_const ConstZ{} = "Int"
	show_const (ConstS c) = show_const c

instance -- Proj_ConC
 ( Proj_Const cs Int
 , Proj_Consts cs (Consts_imported_by Int)
 ) => Proj_ConC cs (Proxy Int) where
	proj_conC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_const c) SKiType
	 , Just Refl <- proj_const c (Proxy @Int)
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy @Bounded)  -> Just Con
		   | Just Refl <- proj_const q (Proxy @Enum)     -> Just Con
		   | Just Refl <- proj_const q (Proxy @Eq)       -> Just Con
		   | Just Refl <- proj_const q (Proxy @Integral) -> Just Con
		   | Just Refl <- proj_const q (Proxy @Num)      -> Just Con
		   | Just Refl <- proj_const q (Proxy @Ord)      -> Just Con
		   | Just Refl <- proj_const q (Proxy @Real)     -> Just Con
		   | Just Refl <- proj_const q (Proxy @Show)     -> Just Con
		 _ -> Nothing
	proj_conC _c _q = Nothing
data instance TokenT meta (ts::[*]) (Proxy Int)
 = Token_Term_Int Int
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Int))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Int))
instance -- CompileI
 Inj_Const (Consts_of_Ifaces is) Int =>
 CompileI is (Proxy Int) where
	compileI tok _ctx k =
		case tok of
		 Token_Term_Int i -> k (ty @Int) $ TermO $ \_c -> int i
instance TokenizeT meta ts (Proxy Int)
instance Gram_Term_AtomsT meta ts (Proxy Int) g