]> Git — Sourcephile - haskell/symantic-parser.git/blob - src/Symantic/Univariant/Data.hs
remove useless benchmarks
[haskell/symantic-parser.git] / src / Symantic / Univariant / Data.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE DataKinds #-}
3 --{-# LANGUAGE RoleAnnotations #-}
4 {-# LANGUAGE FlexibleContexts #-}
5 {-# LANGUAGE FlexibleInstances #-}
6 {-# LANGUAGE GADTs #-}
7 {-# LANGUAGE KindSignatures #-}
8 {-# LANGUAGE LambdaCase #-}
9 {-# LANGUAGE MultiParamTypeClasses #-}
10 {-# LANGUAGE PatternSynonyms #-}
11 {-# LANGUAGE RankNTypes #-}
12 --{-# LANGUAGE QuantifiedConstraints #-}
13 {-# LANGUAGE ScopedTypeVariables #-}
14 {-# LANGUAGE StandaloneDeriving #-}
15 {-# LANGUAGE TypeApplications #-}
16 {-# LANGUAGE TypeFamilies #-}
17 {-# LANGUAGE UndecidableInstances #-} -- For Abstractable (SomeData repr)
18 {-# LANGUAGE ViewPatterns #-}
19 module Symantic.Univariant.Data where
20
21 import Data.Kind
22 import Type.Reflection
23 import Data.Char (Char)
24 import Data.Bool (Bool)
25 import Data.Either (Either)
26 import Data.Maybe (Maybe)
27 import Data.Functor.Identity (Identity(..))
28 import Data.String (String)
29 import Prelude (undefined)
30 import Text.Show (Show(..))
31 import qualified Data.Eq as Eq
32 import qualified Data.Maybe as Maybe
33 import qualified Data.Function as Fun
34 import Data.Coerce
35
36 import Symantic.Univariant.Lang
37 import Symantic.Univariant.Trans
38
39 data SomeData repr a =
40 forall able.
41 ( Trans (Data able repr) repr
42 , Typeable able
43 ) => SomeData (Data able repr a)
44
45 instance Trans (SomeData repr) repr where
46 trans (SomeData x) = trans x
47
48 type UnivariantRepr = Type -> Type
49
50 -- TODO: neither data families nor data instances
51 -- can have phantom roles with GHC-9's RoleAnnotations,
52 -- hence 'Data.Coerce.coerce' cannot be used on them for now.
53 -- https://gitlab.haskell.org/ghc/ghc/-/issues/8177
54 -- https://gitlab.haskell.org/ghc/ghc/-/wikis/roles#proposal-roles-for-type-families
55 -- Would be useful for @Trans (Data able repr) (Data able repr')@ instances.
56 data family Data
57 (able :: UnivariantRepr -> Constraint)
58 :: UnivariantRepr -> UnivariantRepr
59 --instance Trans (Data able repr) (Data able repr) where
60 -- trans = Fun.id
61
62 -- | Convenient utility to pattern-match a 'SomeData'.
63 pattern Data :: Typeable able => Data able repr a -> SomeData repr a
64 pattern Data x <- (unSomeData -> Maybe.Just x)
65
66 {-
67 class TransUnit able where
68 -- | The 'Bottomable' constraint is needed when a @(repr)@ value
69 -- has to be constructed.
70 reprFromUnit :: Bottomable repr => Data able Unit a -> SomeData repr a
71 -- | The 'Bottomable' constraint is also needed here
72 -- to call 'reprFromUnit' in the 'Lam' case.
73 unitFromRepr :: Bottomable repr => Data able repr a -> SomeData Unit a
74
75 coerceRepr ::
76 Bottomable repr => Bottomable repr' =>
77 SomeData repr a -> SomeData repr' a
78 coerceRepr (SomeData r) =
79 case unitFromRepr r of
80 SomeData d -> reprFromUnit d
81 -}
82
83 -- | @(unSomeData c :: 'Maybe' ('Data' able repr a))@
84 -- extract the data-constructor from the given 'SomeData'
85 -- iif. it belongs to the @('Data' able repr a)@ data-instance.
86 unSomeData ::
87 forall able repr a.
88 Typeable able =>
89 SomeData repr a -> Maybe (Data able repr a)
90 unSomeData (SomeData (c::Data c repr a)) =
91 case typeRep @able `eqTypeRep` typeRep @c of
92 Maybe.Just HRefl -> Maybe.Just c
93 Maybe.Nothing -> Maybe.Nothing
94
95 -- Abstractable
96 data instance Data Abstractable repr a where
97 (:@) :: SomeData repr (a->b) -> SomeData repr a -> Data Abstractable repr b
98 Lam :: (SomeData repr a -> SomeData repr b) -> Data Abstractable repr (a->b)
99 Lam1 :: (SomeData repr a -> SomeData repr b) -> Data Abstractable repr (a->b)
100 Var :: repr a -> Data Abstractable repr a
101 -- FIXME: add constructors
102 instance
103 ( Abstractable repr
104 --, Trans (SomeData repr) repr
105 --, Trans repr (SomeData repr)
106 ) => Trans (Data Abstractable repr) repr where
107 trans = \case
108 f :@ x -> trans f .@ trans x
109 Lam f -> lam (\x -> trans (f (SomeData (Var x))))
110 Lam1 f -> lam1 (\x -> trans (f (SomeData (Var x))))
111 Var x -> var x
112 instance
113 ( Abstractable repr
114 --, Trans (SomeData repr) repr
115 --, Trans repr (SomeData repr)
116 ) => Abstractable (SomeData repr) where
117 f .@ x = SomeData (f :@ x)
118 lam f = SomeData (Lam f)
119 lam1 f = SomeData (Lam1 f)
120 var = Fun.id
121 ($) = lam1 (\f -> lam1 (\x -> f .@ x))
122 (.) = lam1 (\f -> lam1 (\g -> lam1 (\x -> f .@ (g .@ x))))
123 const = lam1 (\x -> lam1 (\_y -> x))
124 flip = lam1 (\f -> lam1 (\x -> lam1 (\y -> f .@ y .@ x)))
125 id = lam1 (\x -> x)
126
127 {-
128 instance
129 ( Abstractable repr
130 ) =>
131 Abstractable (Data Abstractable repr) where
132 var = Var Fun.. SomeData
133 f .@ x = SomeData f :@ SomeData x
134 lam f = Lam (SomeData Fun.. f Fun.. Var)
135 lam1 f = Lam1 (SomeData Fun.. f Fun.. Var)
136 ($) = lam1 (\f -> lam1 (\x -> f .@ x))
137 (.) = lam1 (\f -> lam1 (\g -> lam1 (\x -> f .@ (g .@ x))))
138 const = lam1 (\x -> lam1 (\_y -> x))
139 flip = lam1 (\f -> lam1 (\x -> lam1 (\y -> f .@ y .@ x)))
140 id = lam1 (\x -> x)
141 -}
142 {-
143 instance Bottomable repr => Morph (SomeData repr) (SomeData Unit) where
144 morph (SomeData x) = morph x
145 instance Bottomable repr => Morph (SomeData Unit) (SomeData repr) where
146 morph (SomeData x) = morph x
147 instance Abstractable Unit where
148 (.@) _f _x = Unit
149 lam _f = Unit
150 lam1 _f = Unit
151 ($) = Unit
152 (.) = Unit
153 const = Unit
154 flip = Unit
155 id = Unit
156 instance Abstractable (Data Abstractable Unit) where
157 f .@ x = SomeData f :@ SomeData x
158 lam f = Lam (\(SomeData x) -> SomeData (f (trans x)))
159 lam1 f = Lam1 (\(SomeData x) -> SomeData (f (trans x)))
160 ($) = ($)
161 (.) = (.)
162 const = const
163 flip = flip
164 id = id
165 -}
166
167 -- Anythingable
168 data instance Data Anythingable repr a where
169 Anything :: repr a -> Data Anythingable repr a
170 instance
171 ( Anythingable repr
172 ) =>
173 Trans (Data Anythingable repr) repr where
174 trans = \case
175 Anything x -> anything x
176 instance Anythingable (SomeData repr)
177 instance Anythingable (Data Anythingable repr)
178
179 -- Bottomable
180 class Bottomable repr where
181 bottom :: repr a
182 data instance Data Bottomable repr a where
183 Bottom :: Data Bottomable repr a
184 instance Bottomable repr => Trans (Data Bottomable repr) repr where
185 trans Bottom{} = bottom
186
187 -- Constantable
188 data instance Data (Constantable c) repr a where
189 Constant :: c -> Data (Constantable c) repr c
190 instance Constantable c repr => Trans (Data (Constantable c) repr) repr where
191 trans = \case
192 Constant x -> constant x
193 instance
194 ( Constantable c repr
195 , Typeable c
196 ) => Constantable c (SomeData repr) where
197 constant c = SomeData (Constant c)
198 instance Constantable c (Data (Constantable c) repr) where
199 constant = Constant
200
201 -- Eitherable
202 data instance Data Eitherable repr a where
203 Left :: Data Eitherable repr (l -> Either l r)
204 Right :: Data Eitherable repr (r -> Either l r)
205 instance Eitherable repr => Trans (Data Eitherable repr) repr where
206 trans = \case
207 Left -> left
208 Right -> right
209 instance
210 ( Eitherable repr
211 ) => Eitherable (SomeData repr) where
212 left = SomeData Left
213 right = SomeData Right
214 instance Eitherable (Data Eitherable repr) where
215 left = Left
216 right = Right
217
218 -- Equalable
219 data instance Data Equalable repr a where
220 Equal :: Eq.Eq a => Data Equalable repr (a -> a -> Bool)
221 instance Equalable repr => Trans (Data Equalable repr) repr where
222 trans = \case
223 Equal -> equal
224 instance
225 ( Equalable repr
226 ) => Equalable (SomeData repr) where
227 equal = SomeData Equal
228 instance Equalable (Data Equalable repr) where
229 equal = Equal
230
231 -- Listable
232 data instance Data Listable repr a where
233 Cons :: Data Listable repr (a -> [a] -> [a])
234 Nil :: Data Listable repr [a]
235 infixr 4 `Cons`
236 instance Listable repr => Trans (Data Listable repr) repr where
237 trans = \case
238 Cons -> cons
239 Nil -> nil
240 instance
241 ( Listable repr
242 ) => Listable (SomeData repr) where
243 cons = SomeData Cons
244 nil = SomeData Nil
245 instance Listable (Data Listable repr) where
246 cons = Cons
247 nil = Nil
248
249 -- Maybeable
250 data instance Data Maybeable repr a where
251 Nothing :: Data Maybeable repr (Maybe a)
252 Just :: Data Maybeable repr (a -> Maybe a)
253 instance Maybeable repr => Trans (Data Maybeable repr) repr where
254 trans = \case
255 Nothing -> nothing
256 Just -> just
257 instance
258 ( Maybeable repr
259 ) => Maybeable (SomeData repr) where
260 nothing = SomeData Nothing
261 just = SomeData Just
262 instance Maybeable (Data Maybeable repr) where
263 nothing = Nothing
264 just = Just