]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Ratio.hs
Add TyApp pattern synonyms (:$) and (:@).
[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.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