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

import Data.Ratio (Ratio)
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 FixityOf Ratio
instance ClassInstancesFor Ratio where
	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ 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