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

import Data.Eq (Eq)
import Data.Function (($))
import Data.Maybe (Maybe(..))
import Data.Ord (Ord)
import Data.Ratio (Ratio)
import Prelude (Fractional, Integral, Num, Real, RealFrac)
import Text.Show (Show)
import qualified Data.Ratio as Ratio

import Language.Symantic
import Language.Symantic.Lib.Function (a0)
import Language.Symantic.Lib.Integral (tyIntegral)

-- * Class 'Sym_Ratio'
type instance Sym Ratio = 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       :: Sym_Ratio (UnT term) => Trans term => Integral a => term a -> term a -> term (Ratio a)
	default numerator   :: Sym_Ratio (UnT term) => Trans term               => term (Ratio a) -> term a
	default denominator :: Sym_Ratio (UnT term) => Trans term               => term (Ratio a) -> term a
	
	ratio       = trans2 ratio
	numerator   = trans1 numerator
	denominator = trans1 denominator

-- Interpreting
instance Sym_Ratio Eval where
	ratio       = eval2 (Ratio.%)
	numerator   = eval1 Ratio.numerator
	denominator = eval1 Ratio.denominator
instance Sym_Ratio View where
	ratio       = viewInfix "ratio" (infixL 7)
	numerator   = view1 "numerator"
	denominator = view1 "denominator"
instance (Sym_Ratio r1, Sym_Ratio r2) => Sym_Ratio (Dup r1 r2) where
	ratio       = dup2 @Sym_Ratio ratio
	numerator   = dup1 @Sym_Ratio numerator
	denominator = dup1 @Sym_Ratio denominator

-- Transforming
instance (Sym_Ratio term, Sym_Lambda term) => Sym_Ratio (BetaT term)

-- Typing
instance NameTyOf Ratio where
	nameTyOf _c = ["Ratio"] `Mod` "Ratio"
instance FixityOf Ratio
instance ClassInstancesFor Ratio where
	proveConstraintFor _ (tq@(TyConst _ _ q) :$ c:@a)
	 | Just HRefl <- proj_ConstKiTy @_ @Ratio c
	 = case () of
		 _ | Just Refl <- proj_Const @Eq q
		   , Just Dict <- proveConstraint (tq`tyApp`a)   -> Just Dict
		   | Just Refl <- proj_Const @Show q
		   , Just Dict <- proveConstraint (tq`tyApp`a)   -> Just Dict
		   | Just Refl <- proj_Const @Real q
		   , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict
		   | Just Refl <- proj_Const @Ord q
		   , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict
		   | Just Refl <- proj_Const @Fractional q
		   , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict
		   | Just Refl <- proj_Const @Num q
		   , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict
		   | Just Refl <- proj_Const @RealFrac q
		   , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Ratio

-- Compiling
instance Gram_Term_AtomsFor src ss g Ratio
instance (Source src, SymInj ss Ratio) => ModuleFor src ss Ratio where
	moduleFor = ["Ratio"] `moduleWhere`
	 [ "ratio"       := teRatio
	 , "numerator"   := teRatio_numerator
	 , "denominator" := teRatio_denominator
	 ]

-- ** 'Type's
tyRatio :: Source src => Type src vs a -> Type src vs (Ratio a)
tyRatio a = tyConstLen @(K Ratio) @Ratio (lenVars a) `tyApp` a

-- ** 'Term's
teRatio :: TermDef Ratio '[Proxy a] (Integral a #> (a -> a -> Ratio a))
teRatio = Term (tyIntegral a0) (a0 ~> a0 ~> tyRatio a0) $ teSym @Ratio $ lam2 ratio

teRatio_numerator, teRatio_denominator :: TermDef Ratio '[Proxy a] (() #> (Ratio a -> a))
teRatio_numerator   = Term noConstraint (tyRatio a0 ~> a0) $ teSym @Ratio $ lam1 numerator
teRatio_denominator = Term noConstraint (tyRatio a0 ~> a0) $ teSym @Ratio $ lam1 denominator