]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Ratio.hs
Clarify a few names in Grammar.Fixity.
[haskell/symantic.git] / 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