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