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)
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
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
instance (Sym_Ratio term, Sym_Lambda term) => Sym_Ratio (BetaT term)
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
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
]
tyRatio :: Source src => Type src vs a -> Type src vs (Ratio a)
tyRatio a = tyConstLen @(K Ratio) @Ratio (lenVars a) `tyApp` a
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