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

import Control.Monad (liftM)
import Data.Proxy
import qualified Prelude
import Data.Ratio (Ratio)
import Prelude (Real)
import Prelude hiding (Real(..))

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

-- * Class 'Sym_Real'
class Sym_Real term where
	toRational :: Real a => term a -> term Rational
	default toRational :: (Trans t term, Real a) => t term a -> t term Rational
	toRational = trans_map1 toRational

type instance Sym_of_Iface (Proxy Real) = Sym_Real
type instance TyConsts_of_Iface (Proxy Real) = Proxy Real ': TyConsts_imported_by Real
type instance TyConsts_imported_by Real =
 [ Proxy Ratio
 , Proxy Integer
 ]

instance Sym_Real HostI where
	toRational = liftM  Prelude.toRational
instance Sym_Real TextI where
	toRational = textI1 "toRational"
instance (Sym_Real r1, Sym_Real r2) => Sym_Real (DupI r1 r2) where
	toRational = dupI1 @Sym_Real toRational

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

instance Proj_TyConC cs (Proxy Real)
data instance TokenT meta (ts::[*]) (Proxy Real)
 =  Token_Term_Real (EToken meta ts)
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy Real))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy Real))
instance -- CompileI
 ( Read_TyName TyName cs
 , Inj_TyConst cs Real
 , Inj_TyConst cs Ratio
 , Inj_TyConst cs Integer
 , Proj_TyCon  cs
 , Compile cs is
 ) => CompileI cs is (Proxy Real) where
	compileI tok ctx k =
		case tok of
		 Token_Term_Real tok_a ->
			-- toRational :: a -> Rational
			compileO tok_a ctx $ \ty_a (TermO a) ->
			check_TyCon (At (Just tok_a) (ty @Real :$ ty_a)) $ \TyCon ->
			k (ty @Ratio :$ ty @Integer) $ TermO $
			 \c -> toRational (a c)
instance -- TokenizeT
 Inj_Token meta ts Real =>
 TokenizeT meta ts (Proxy Real) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize1 "toRational" infixN5 Token_Term_Real
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy Real) g