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