]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Ratio.hs
Fix Mono{Foldable,Functor} and {Semi,Is}Sequence constraints.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Ratio.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 {-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
4 -- | Symantic for 'Ratio'.
5 module Language.Symantic.Lib.Ratio where
6
7 import Control.Monad (liftM, liftM2)
8 import Data.Proxy
9 import Data.Ratio (Ratio)
10 import Data.Type.Equality ((:~:)(Refl))
11 import qualified Data.Ratio as Ratio
12
13 import Language.Symantic.Parsing
14 import Language.Symantic.Typing
15 import Language.Symantic.Compiling
16 import Language.Symantic.Interpreting
17 import Language.Symantic.Transforming
18 import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))
19
20 -- * Class '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 :: (Trans t term, Integral a) => t term a -> t term a -> t term (Ratio a)
27 default numerator :: Trans t term => t term (Ratio a) -> t term a
28 default denominator :: Trans t term => t term (Ratio a) -> t term a
29
30 ratio = trans_map2 ratio
31 numerator = trans_map1 numerator
32 denominator = trans_map1 denominator
33
34 type instance Sym_of_Iface (Proxy Ratio) = Sym_Ratio
35 type instance TyConsts_of_Iface (Proxy Ratio) = Proxy Ratio ': TyConsts_imported_by (Proxy Ratio)
36 type instance TyConsts_imported_by (Proxy Ratio) =
37 [ Proxy Enum
38 , Proxy Eq
39 -- , Proxy Fractional
40 , Proxy Integral
41 , Proxy Num
42 , Proxy Ord
43 , Proxy Real
44 -- , Proxy RealFrac
45 , Proxy Show
46 ]
47
48 instance Sym_Ratio HostI where
49 ratio = liftM2 (Ratio.%)
50 numerator = liftM Ratio.numerator
51 denominator = liftM Ratio.denominator
52 instance Sym_Ratio TextI where
53 ratio = textI_infix "ratio" (infixL 7)
54 numerator = textI1 "numerator"
55 denominator = textI1 "denominator"
56 instance (Sym_Ratio r1, Sym_Ratio r2) => Sym_Ratio (DupI r1 r2) where
57 ratio = dupI2 @Sym_Ratio ratio
58 numerator = dupI1 @Sym_Ratio numerator
59 denominator = dupI1 @Sym_Ratio denominator
60
61 instance
62 ( Read_TyNameR TyName cs rs
63 , Inj_TyConst cs Ratio
64 ) => Read_TyNameR TyName cs (Proxy Ratio ': rs) where
65 read_TyNameR _cs (TyName "Ratio") k = k (ty @Ratio)
66 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
67 instance Show_TyConst cs => Show_TyConst (Proxy Ratio ': cs) where
68 show_TyConst TyConstZ{} = "Ratio"
69 show_TyConst (TyConstS c) = show_TyConst c
70
71 instance Proj_TyFamC cs TyFam_MonoElement Ratio
72
73 instance -- Proj_TyConC
74 ( Proj_TyConst cs Ratio
75 , Proj_TyConsts cs (TyConsts_imported_by (Proxy Ratio))
76 , Proj_TyCon cs
77 , Inj_TyConst cs Integral
78 ) => Proj_TyConC cs (Proxy Ratio) where
79 proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ a))
80 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
81 , Just Refl <- proj_TyConst c (Proxy @Ratio)
82 = case () of
83 _ | Just Refl <- proj_TyConst q (Proxy @Eq)
84 , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
85 | Just Refl <- proj_TyConst q (Proxy @Show)
86 , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
87 | Just Refl <- proj_TyConst q (Proxy @Real)
88 , Just TyCon <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
89 | Just Refl <- proj_TyConst q (Proxy @Ord)
90 {-
91 , Just TyCon <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
92 | Just Refl <- proj_TyConst q (Proxy @Fractional)
93 -}
94 , Just TyCon <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
95 | Just Refl <- proj_TyConst q (Proxy @Num)
96 , Just TyCon <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
97 {-
98 | Just Refl <- proj_TyConst q (Proxy @RealFrac)
99 , Just TyCon <- proj_TyCon (ty @Integral :$ a) -> Just TyCon
100 -}
101 _ -> Nothing
102 proj_TyConC _c _q = Nothing
103
104 data instance TokenT meta (ts::[*]) (Proxy Ratio)
105 = Token_Term_Ratio (EToken meta ts) (EToken meta ts)
106 | Token_Term_Ratio_numerator (EToken meta ts)
107 | Token_Term_Ratio_denominator (EToken meta ts)
108 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Ratio))
109 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Ratio))
110
111 instance -- CompileI
112 ( Inj_TyConst cs Ratio
113 , Inj_TyConst cs Integral
114 , Proj_TyCon cs
115 , Compile cs is
116 ) => CompileI cs is (Proxy Ratio) where
117 compileI tok ctx k =
118 case tok of
119 Token_Term_Ratio tok_n tok_d ->
120 -- (%) :: a -> a -> (a, a)
121 compileO tok_n ctx $ \ty_n (TermO n) ->
122 compileO tok_d ctx $ \ty_d (TermO d) ->
123 check_TyEq
124 (At (Just tok_n) ty_n)
125 (At (Just tok_d) ty_d) $ \Refl ->
126 check_TyCon (At (Just tok_n) (ty @Integral :$ ty_n)) $ \TyCon ->
127 k (ty @Ratio :$ ty_n) $ TermO $
128 \c -> ratio (n c) (d c)
129 Token_Term_Ratio_numerator tok_r ->
130 -- numerator :: Ratio a -> a
131 compileO tok_r ctx $ \ty_r (TermO r) ->
132 check_TyEq1 (ty @Ratio) (At (Just tok_r) ty_r) $ \Refl ty_a ->
133 k ty_a $ TermO $
134 \c -> numerator (r c)
135 Token_Term_Ratio_denominator tok_r ->
136 -- denominator :: Ratio a -> a
137 compileO tok_r ctx $ \ty_r (TermO r) ->
138 check_TyEq1 (ty @Ratio) (At (Just tok_r) ty_r) $ \Refl ty_a ->
139 k ty_a $ TermO $
140 \c -> denominator (r c)
141 instance -- TokenizeT
142 -- Inj_Token meta ts Ratio =>
143 TokenizeT meta ts (Proxy Ratio)
144 instance Gram_Term_AtomsT meta ts (Proxy Ratio) g