symantic-lib/Language/Symantic/Lib/Ratio.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Ratio'.
   4 module Language.Symantic.Lib.Ratio where
   5
   6 import Data.Eq (Eq)
   7 import Data.Function (($))
   8 import Data.Maybe (Maybe(..))
   9 import Data.Ord (Ord)
  10 import Data.Ratio (Ratio)
  11 import Prelude (Fractional, Integral, Num, Real, RealFrac)
  12 import Text.Show (Show)
  13 import qualified Data.Ratio as Ratio
  14
  15 import Language.Symantic
  16 import Language.Symantic.Lib.Function (a0)
  17 import Language.Symantic.Lib.Integral (tyIntegral)
  18
  19 -- * Class 'Sym_Ratio'
  20 type instance Sym Ratio = Sym_Ratio
  21 class Sym_Ratio term where
  22         ratio       :: Integral a => term a -> term a -> term (Ratio a)
  23         numerator   :: term (Ratio a) -> term a
  24         denominator :: term (Ratio a) -> term a
  25
  26         default ratio       :: Sym_Ratio (UnT term) => Trans term => Integral a => term a -> term a -> term (Ratio a)
  27         default numerator   :: Sym_Ratio (UnT term) => Trans term               => term (Ratio a) -> term a
  28         default denominator :: Sym_Ratio (UnT term) => Trans term               => term (Ratio a) -> term a
  29
  30         ratio       = trans2 ratio
  31         numerator   = trans1 numerator
  32         denominator = trans1 denominator
  33
  34 -- Interpreting
  35 instance Sym_Ratio Eval where
  36         ratio       = eval2 (Ratio.%)
  37         numerator   = eval1 Ratio.numerator
  38         denominator = eval1 Ratio.denominator
  39 instance Sym_Ratio View where
  40         ratio       = viewInfix "ratio" (infixL 7)
  41         numerator   = view1 "numerator"
  42         denominator = view1 "denominator"
  43 instance (Sym_Ratio r1, Sym_Ratio r2) => Sym_Ratio (Dup r1 r2) where
  44         ratio       = dup2 @Sym_Ratio ratio
  45         numerator   = dup1 @Sym_Ratio numerator
  46         denominator = dup1 @Sym_Ratio denominator
  47
  48 -- Transforming
  49 instance (Sym_Ratio term, Sym_Lambda term) => Sym_Ratio (BetaT term)
  50
  51 -- Typing
  52 instance NameTyOf Ratio where
  53         nameTyOf _c = ["Ratio"] `Mod` "Ratio"
  54 instance FixityOf Ratio
  55 instance ClassInstancesFor Ratio where
  56         proveConstraintFor _ (tq@(TyConst _ _ q) :$ c:@a)
  57          | Just HRefl <- proj_ConstKiTy @_ @Ratio c
  58          = case () of
  59                  _ | Just Refl <- proj_Const @Eq q
  60                    , Just Dict <- proveConstraint (tq`tyApp`a)   -> Just Dict
  61                    | Just Refl <- proj_Const @Show q
  62                    , Just Dict <- proveConstraint (tq`tyApp`a)   -> Just Dict
  63                    | Just Refl <- proj_Const @Real q
  64                    , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict
  65                    | Just Refl <- proj_Const @Ord q
  66                    , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict
  67                    | Just Refl <- proj_Const @Fractional q
  68                    , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict
  69                    | Just Refl <- proj_Const @Num q
  70                    , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict
  71                    | Just Refl <- proj_Const @RealFrac q
  72                    , Just Dict <- proveConstraint (tyIntegral a) -> Just Dict
  73                  _ -> Nothing
  74         proveConstraintFor _c _q = Nothing
  75 instance TypeInstancesFor Ratio
  76
  77 -- Compiling
  78 instance Gram_Term_AtomsFor src ss g Ratio
  79 instance (Source src, SymInj ss Ratio) => ModuleFor src ss Ratio where
  80         moduleFor = ["Ratio"] `moduleWhere`
  81          [ "ratio"       := teRatio
  82          , "numerator"   := teRatio_numerator
  83          , "denominator" := teRatio_denominator
  84          ]
  85
  86 -- ** 'Type's
  87 tyRatio :: Source src => Type src vs a -> Type src vs (Ratio a)
  88 tyRatio a = tyConstLen @(K Ratio) @Ratio (lenVars a) `tyApp` a
  89
  90 -- ** 'Term's
  91 teRatio :: TermDef Ratio '[Proxy a] (Integral a #> (a -> a -> Ratio a))
  92 teRatio = Term (tyIntegral a0) (a0 ~> a0 ~> tyRatio a0) $ teSym @Ratio $ lam2 ratio
  93
  94 teRatio_numerator, teRatio_denominator :: TermDef Ratio '[Proxy a] (() #> (Ratio a -> a))
  95 teRatio_numerator   = Term noConstraint (tyRatio a0 ~> a0) $ teSym @Ratio $ lam1 numerator
  96 teRatio_denominator = Term noConstraint (tyRatio a0 ~> a0) $ teSym @Ratio $ lam1 denominator