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

import Control.Monad (liftM, liftM2)
import Data.Proxy
import Data.Ratio (Ratio)
import Data.Type.Equality ((:~:)(Refl))
import qualified Data.Ratio as Ratio

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_Ratio'
class Sym_Ratio term where
	ratio :: Integral a => term a -> term a -> term (Ratio a)
	numerator   :: term (Ratio a) -> term a
	denominator :: term (Ratio a) -> term a
	
	default ratio :: (Trans t term, Integral a) => t term a -> t term a -> t term (Ratio a)
	default numerator   :: Trans t term => t term (Ratio a) -> t term a
	default denominator :: Trans t term => t term (Ratio a) -> t term a
	
	ratio       = trans_map2 ratio
	numerator   = trans_map1 numerator
	denominator = trans_map1 denominator

type instance Sym_of_Iface (Proxy Ratio) = Sym_Ratio
type instance TyConsts_of_Iface (Proxy Ratio) = Proxy Ratio ': TyConsts_imported_by (Proxy Ratio)
type instance TyConsts_imported_by (Proxy Ratio) =
 [ Proxy Enum
 , Proxy Eq
 -- , Proxy Fractional
 , Proxy Integral
 , Proxy Num
 , Proxy Ord
 , Proxy Real
 -- , Proxy RealFrac
 , Proxy Show
 ]

instance Sym_Ratio HostI where
	ratio       = liftM2 (Ratio.%)
	numerator   = liftM  Ratio.numerator
	denominator = liftM  Ratio.denominator
instance Sym_Ratio TextI where
	ratio       = textI_infix "ratio" (infixL 7)
	numerator   = textI1 "numerator"
	denominator = textI1 "denominator"
instance (Sym_Ratio r1, Sym_Ratio r2) => Sym_Ratio (DupI r1 r2) where
	ratio       = dupI2 @Sym_Ratio ratio
	numerator   = dupI1 @Sym_Ratio numerator
	denominator = dupI1 @Sym_Ratio denominator

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

instance Proj_TyFamC cs TyFam_MonoElement Ratio

instance -- Proj_TyConC
 ( Proj_TyConst cs Ratio
 , Proj_TyConsts cs (TyConsts_imported_by (Proxy Ratio))
 , Proj_TyCon cs
 , Inj_TyConst cs Integral
 ) => Proj_TyConC cs (Proxy Ratio) where
	proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ a))
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @Ratio)
	 = case () of
		 _ | Just Refl  <- proj_TyConst q (Proxy @Eq)
		   , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
		   | Just Refl  <- proj_TyConst q (Proxy @Show)
		   , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
		   | Just Refl  <- proj_TyConst q (Proxy @Real)
		   , Just TyCon  <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
		   | Just Refl  <- proj_TyConst q (Proxy @Ord)
		   {-
		   , Just TyCon  <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
		   | Just Refl  <- proj_TyConst q (Proxy @Fractional)
		   -}
		   , Just TyCon  <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
		   | Just Refl  <- proj_TyConst q (Proxy @Num)
		   , Just TyCon  <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
		   {-
		   | Just Refl  <- proj_TyConst q (Proxy @RealFrac)
		   , Just TyCon  <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
		   -}
		 _ -> Nothing
	proj_TyConC _c _q = Nothing

data instance TokenT meta (ts::[*]) (Proxy Ratio)
 = Token_Term_Ratio             (EToken meta ts) (EToken meta ts)
 | Token_Term_Ratio_numerator   (EToken meta ts)
 | Token_Term_Ratio_denominator (EToken meta ts)
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Ratio))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Ratio))

instance -- CompileI
 ( Inj_TyConst cs Ratio
 , Inj_TyConst cs Integral
 , Proj_TyCon  cs
 , Compile cs is
 ) => CompileI cs is (Proxy Ratio) where
	compileI tok ctx k =
		case tok of
		 Token_Term_Ratio tok_n tok_d ->
			-- (%) :: a -> a -> (a, a)
			compileO tok_n ctx $ \ty_n (TermO n) ->
			compileO tok_d ctx $ \ty_d (TermO d) ->
			check_TyEq
			 (At (Just tok_n) ty_n)
			 (At (Just tok_d) ty_d) $ \Refl ->
			check_TyCon (At (Just tok_n) (ty @Integral :$ ty_n)) $ \TyCon ->
			k (ty @Ratio :$ ty_n) $ TermO $
			 \c -> ratio (n c) (d c)
		 Token_Term_Ratio_numerator tok_r ->
			-- numerator :: Ratio a -> a
			compileO tok_r ctx $ \ty_r (TermO r) ->
			check_TyEq1 (ty @Ratio) (At (Just tok_r) ty_r) $ \Refl ty_a ->
			k ty_a $ TermO $
			 \c -> numerator (r c)
		 Token_Term_Ratio_denominator tok_r ->
			-- denominator :: Ratio a -> a
			compileO tok_r ctx $ \ty_r (TermO r) ->
			check_TyEq1 (ty @Ratio) (At (Just tok_r) ty_r) $ \Refl ty_a ->
			k ty_a $ TermO $
			 \c -> denominator (r c)
instance -- TokenizeT
 -- Inj_Token meta ts Ratio =>
 TokenizeT meta ts (Proxy Ratio)
instance Gram_Term_AtomsT meta ts (Proxy Ratio) g