{-# 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