]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Ord.hs
Fix comment typo.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Ord.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Ord'.
4 module Language.Symantic.Lib.Ord where
5
6 import Control.Monad
7 import Data.Ord (Ord)
8 import qualified Data.Ord as Ord
9 import Data.Proxy (Proxy(..))
10 import qualified Data.Text as Text
11 import Data.Type.Equality ((:~:)(Refl))
12 import qualified Data.Kind as Kind
13 import Prelude hiding (Ord(..))
14
15 import Language.Symantic.Parsing
16 import Language.Symantic.Typing
17 import Language.Symantic.Compiling
18 import Language.Symantic.Interpreting
19 import Language.Symantic.Transforming
20 import Language.Symantic.Lib.Lambda
21 import Language.Symantic.Lib.Eq (Sym_Eq)
22
23 -- * Class 'Sym_Ord'
24 class Sym_Eq term => Sym_Ord term where
25 compare :: Ord a => term a -> term a -> term Ordering
26 (<) :: Ord a => term a -> term a -> term Bool; infix 4 <
27 (<=) :: Ord a => term a -> term a -> term Bool; infix 4 <=
28 (>) :: Ord a => term a -> term a -> term Bool; infix 4 >
29 (>=) :: Ord a => term a -> term a -> term Bool; infix 4 >=
30 max :: Ord a => term a -> term a -> term a
31 min :: Ord a => term a -> term a -> term a
32
33 default compare :: (Trans t term, Ord a) => t term a -> t term a -> t term Ordering
34 default (<) :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
35 default (<=) :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
36 default (>) :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
37 default (>=) :: (Trans t term, Ord a) => t term a -> t term a -> t term Bool
38 default max :: (Trans t term, Ord a) => t term a -> t term a -> t term a
39 default min :: (Trans t term, Ord a) => t term a -> t term a -> t term a
40
41 compare = trans_map2 compare
42 (<) = trans_map2 (<)
43 (<=) = trans_map2 (<=)
44 (>) = trans_map2 (>)
45 (>=) = trans_map2 (>=)
46 min = trans_map2 min
47 max = trans_map2 max
48
49 -- * Class 'Sym_Ordering'
50 class Sym_Eq term => Sym_Ordering term where
51 ordering :: Ordering -> term Ordering
52 default ordering :: Trans t term => Ordering -> t term Ordering
53 ordering = trans_lift . ordering
54
55 type instance Sym_of_Iface (Proxy Ord) = Sym_Ord
56 type instance Sym_of_Iface (Proxy Ordering) = Sym_Ordering
57 type instance TyConsts_of_Iface (Proxy Ord) = Proxy Ord ': TyConsts_imported_by Ord
58 type instance TyConsts_of_Iface (Proxy Ordering) = Proxy Ordering ': TyConsts_imported_by Ordering
59 type instance TyConsts_imported_by Ord = '[]
60 type instance TyConsts_imported_by Ordering =
61 [ Proxy Bounded
62 , Proxy Enum
63 , Proxy Eq
64 , Proxy Ord
65 , Proxy Show
66 ]
67
68 instance Sym_Ord HostI where
69 compare = liftM2 Ord.compare
70 (<) = liftM2 (Ord.<)
71 (<=) = liftM2 (Ord.<=)
72 (>) = liftM2 (Ord.>)
73 (>=) = liftM2 (Ord.>=)
74 min = liftM2 Ord.min
75 max = liftM2 Ord.max
76 instance Sym_Ordering HostI where
77 ordering = HostI
78 instance Sym_Ord TextI where
79 compare = textI2 "compare"
80 (<) = textI_infix "<" (infixN 4)
81 (<=) = textI_infix "<=" (infixN 4)
82 (>) = textI_infix ">" (infixN 4)
83 (>=) = textI_infix ">=" (infixN 4)
84 min = textI2 "min"
85 max = textI2 "max"
86 instance Sym_Ordering TextI where
87 ordering o = TextI $ \_p _v ->
88 Text.pack (show o)
89 instance (Sym_Ord r1, Sym_Ord r2) => Sym_Ord (DupI r1 r2) where
90 compare = dupI2 @Sym_Ord compare
91 (<) = dupI2 @Sym_Ord (<)
92 (<=) = dupI2 @Sym_Ord (<=)
93 (>) = dupI2 @Sym_Ord (>)
94 (>=) = dupI2 @Sym_Ord (>=)
95 min = dupI2 @Sym_Ord min
96 max = dupI2 @Sym_Ord max
97 instance (Sym_Ordering r1, Sym_Ordering r2) => Sym_Ordering (DupI r1 r2) where
98 ordering o = ordering o `DupI` ordering o
99
100 instance
101 ( Read_TyNameR TyName cs rs
102 , Inj_TyConst cs Ord
103 ) => Read_TyNameR TyName cs (Proxy Ord ': rs) where
104 read_TyNameR _cs (TyName "Ord") k = k (ty @Ord)
105 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
106 instance
107 ( Read_TyNameR TyName cs rs
108 , Inj_TyConst cs Ordering
109 ) => Read_TyNameR TyName cs (Proxy Ordering ': rs) where
110 read_TyNameR _cs (TyName "Ordering") k = k (ty @Ordering)
111 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
112 instance Show_TyConst cs => Show_TyConst (Proxy Ord ': cs) where
113 show_TyConst TyConstZ{} = "Ord"
114 show_TyConst (TyConstS c) = show_TyConst c
115 instance Show_TyConst cs => Show_TyConst (Proxy Ordering ': cs) where
116 show_TyConst TyConstZ{} = "Ordering"
117 show_TyConst (TyConstS c) = show_TyConst c
118
119 instance Proj_TyConC cs (Proxy Ord)
120 instance -- Proj_TyConC
121 ( Proj_TyConst cs Ordering
122 , Proj_TyConsts cs (TyConsts_imported_by Ordering)
123 ) => Proj_TyConC cs (Proxy Ordering) where
124 proj_TyConC _ (TyConst q :$ TyConst c)
125 | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
126 , Just Refl <- proj_TyConst c (Proxy @Ordering)
127 = case () of
128 _ | Just Refl <- proj_TyConst q (Proxy @Bounded) -> Just TyCon
129 | Just Refl <- proj_TyConst q (Proxy @Enum) -> Just TyCon
130 | Just Refl <- proj_TyConst q (Proxy @Eq) -> Just TyCon
131 | Just Refl <- proj_TyConst q (Proxy @Ord) -> Just TyCon
132 | Just Refl <- proj_TyConst q (Proxy @Show) -> Just TyCon
133 _ -> Nothing
134 proj_TyConC _c _q = Nothing
135 data instance TokenT meta (ts::[*]) (Proxy Ord)
136 = Token_Term_Ord_compare (EToken meta ts)
137 | Token_Term_Ord_le (EToken meta ts)
138 | Token_Term_Ord_lt (EToken meta ts)
139 | Token_Term_Ord_ge (EToken meta ts)
140 | Token_Term_Ord_gt (EToken meta ts)
141 | Token_Term_Ord_min (EToken meta ts)
142 | Token_Term_Ord_max (EToken meta ts)
143 data instance TokenT meta (ts::[*]) (Proxy Ordering)
144 = Token_Term_Ordering Ordering
145 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Ord))
146 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Ordering))
147 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Ord))
148 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Ordering))
149 instance -- CompileI
150 ( Inj_TyConst (TyConsts_of_Ifaces is) Bool
151 , Inj_TyConst (TyConsts_of_Ifaces is) (->)
152 , Inj_TyConst (TyConsts_of_Ifaces is) Ord
153 , Inj_TyConst (TyConsts_of_Ifaces is) Ordering
154 , Proj_TyCon (TyConsts_of_Ifaces is)
155 , Compile is
156 ) => CompileI is (Proxy Ord) where
157 compileI
158 :: forall meta ctx ret ls rs.
159 TokenT meta is (Proxy Ord)
160 -> CompileT meta ctx ret is ls (Proxy Ord ': rs)
161 compileI tok ctx k =
162 case tok of
163 Token_Term_Ord_compare tok_a -> compare_from tok_a (ty @Ordering) compare
164 Token_Term_Ord_le tok_a -> compare_from tok_a (ty @Bool) (<=)
165 Token_Term_Ord_lt tok_a -> compare_from tok_a (ty @Bool) (<)
166 Token_Term_Ord_ge tok_a -> compare_from tok_a (ty @Bool) (>=)
167 Token_Term_Ord_gt tok_a -> compare_from tok_a (ty @Bool) (>)
168 Token_Term_Ord_min tok_a -> op2_from tok_a min
169 Token_Term_Ord_max tok_a -> op2_from tok_a max
170 where
171 compare_from
172 :: EToken meta is
173 -> Type (TyConsts_of_Ifaces is) (res::Kind.Type)
174 -> (forall term a. (Sym_Ord term, Ord a) => term a -> term a -> term res)
175 -> Either (Error_Term meta is) ret
176 compare_from tok_a ty_res op =
177 -- compare :: Ord a => a -> a -> Ordering
178 -- (<=) :: Ord a => a -> a -> Bool
179 -- (<) :: Ord a => a -> a -> Bool
180 -- (>=) :: Ord a => a -> a -> Bool
181 -- (>) :: Ord a => a -> a -> Bool
182 compileO tok_a ctx $ \ty_a (TermO x) ->
183 check_TyCon (At (Just tok_a) (ty @Ord :$ ty_a)) $ \TyCon ->
184 k (ty_a ~> ty_res) $ TermO $
185 \c -> lam $ op (x c)
186 op2_from tok_a
187 (op::forall term a. (Sym_Ord term, Ord a)
188 => term a -> term a -> term a) =
189 -- min :: Ord a => a -> a -> a
190 -- max :: Ord a => a -> a -> a
191 compileO tok_a ctx $ \ty_a (TermO x) ->
192 check_TyCon (At (Just tok_a) (ty @Ord :$ ty_a)) $ \TyCon ->
193 k (ty_a ~> ty_a) $ TermO $
194 \c -> lam $ \y -> op (x c) y
195 instance -- CompileI
196 ( Inj_TyConst (TyConsts_of_Ifaces is) Ordering
197 ) => CompileI is (Proxy Ordering) where
198 compileI tok _ctx k =
199 case tok of
200 Token_Term_Ordering o -> k (ty @Ordering) $ TermO $ \_c -> ordering o
201 instance -- TokenizeT
202 Inj_Token meta ts Ord =>
203 TokenizeT meta ts (Proxy Ord) where
204 tokenizeT _t = mempty
205 { tokenizers_infix = tokenizeTMod []
206 [ tokenize1 "compare" infixN5 Token_Term_Ord_compare
207 , tokenize1 "<" (infixN 4) Token_Term_Ord_lt
208 , tokenize1 "<=" (infixN 4) Token_Term_Ord_le
209 , tokenize1 ">" (infixN 4) Token_Term_Ord_gt
210 , tokenize1 ">=" (infixN 4) Token_Term_Ord_ge
211 ]
212 }
213 instance -- TokenizeT
214 Inj_Token meta ts Ordering =>
215 TokenizeT meta ts (Proxy Ordering) where
216 tokenizeT _t = mempty
217 { tokenizers_infix = tokenizeTMod []
218 [ tokenize0 "LT" infixN5 $ Token_Term_Ordering LT
219 , tokenize0 "EQ" infixN5 $ Token_Term_Ordering EQ
220 , tokenize0 "GT" infixN5 $ Token_Term_Ordering GT
221 ]
222 }
223 instance Gram_Term_AtomsT meta ts (Proxy Ordering) g
224 instance Gram_Term_AtomsT meta ts (Proxy Ord) g