]> Git — Sourcephile - haskell/symantic-parser.git/blob - src/Symantic/Parser/Machine/Instructions.hs
test: save
[haskell/symantic-parser.git] / src / Symantic / Parser / Machine / Instructions.hs
1 {-# LANGUAGE ConstraintKinds #-} -- For Executable
2 {-# LANGUAGE DerivingStrategies #-} -- For Show (LetName a)
3 {-# LANGUAGE PatternSynonyms #-} -- For Fmap, App, …
4 {-# LANGUAGE UndecidableInstances #-} -- For Cursorable (Cursor inp)
5 module Symantic.Parser.Machine.Instructions where
6
7 import Data.Bool (Bool(..))
8 import Data.Either (Either)
9 import Data.Eq (Eq)
10 import Data.Ord (Ord)
11 import Data.Function (($), (.))
12 import Data.Kind (Type)
13 import System.IO.Unsafe (unsafePerformIO)
14 import Text.Show (Show(..), showString)
15 import qualified Data.Functor as Functor
16 import qualified Language.Haskell.TH as TH
17 import qualified Language.Haskell.TH.Syntax as TH
18 import qualified Symantic.Parser.Grammar.Pure as H
19
20 import Symantic.Parser.Grammar
21 import Symantic.Parser.Machine.Input
22 import Symantic.Univariant.Trans
23
24 -- * Type 'Instr'
25 -- | 'Instr'uctions for the 'Machine'.
26 data Instr input valueStack (failStack::Peano) returnValue where
27 -- | @('Push' x k)@ pushes @(x)@ on the 'valueStack'
28 -- and continues with the next 'Instr'uction @(k)@.
29 Push ::
30 InstrPure v ->
31 Instr inp (v ': vs) es ret ->
32 Instr inp vs es ret
33 -- | @('Pop' k)@ pushes @(x)@ on the 'valueStack'.
34 Pop ::
35 Instr inp vs es ret ->
36 Instr inp (v ': vs) es ret
37 -- | @('LiftI2' f k)@ pops two values from the 'valueStack',
38 -- and pushes the result of @(f)@ applied to them.
39 LiftI2 ::
40 InstrPure (x -> y -> z) ->
41 Instr inp (z : vs) es ret ->
42 Instr inp (y : x : vs) es ret
43 -- | @('Fail')@ raises an error from the 'failStack'.
44 Fail ::
45 [ErrorItem (InputToken inp)] ->
46 Instr inp vs ('Succ es) ret
47 -- | @('PopFail' k)@ removes a 'FailHandler' from the 'failStack'
48 -- and continues with the next 'Instr'uction @(k)@.
49 PopFail ::
50 Instr inp vs es ret ->
51 Instr inp vs ('Succ es) ret
52 -- | @('CatchFail' l r)@ tries the @(l)@ 'Instr'uction
53 -- in a new failure scope such that if @(l)@ raises a failure, it is caught,
54 -- then the input is pushed as it was before trying @(l)@ on the 'valueStack',
55 -- and the control flow goes on with the @(r)@ 'Instr'uction.
56 CatchFail ::
57 Instr inp vs ('Succ es) ret ->
58 Instr inp (Cursor inp ': vs) es ret ->
59 Instr inp vs es ret
60 -- | @('LoadInput' k)@ removes the input from the 'valueStack'
61 -- and continues with the next 'Instr'uction @(k)@ using that input.
62 LoadInput ::
63 Instr inp vs es r ->
64 Instr inp (Cursor inp : vs) es r
65 -- | @('PushInput' k)@ pushes the input @(inp)@ on the 'valueStack'
66 -- and continues with the next 'Instr'uction @(k)@.
67 PushInput ::
68 Instr inp (Cursor inp ': vs) es ret ->
69 Instr inp vs es ret
70 -- | @('Case' l r)@.
71 Case ::
72 Instr inp (x ': vs) es r ->
73 Instr inp (y ': vs) es r ->
74 Instr inp (Either x y ': vs) es r
75 -- | @('Swap' k)@ pops two values on the 'valueStack',
76 -- pushes the first popped-out, then the second,
77 -- and continues with the next 'Instr'uction @(k)@.
78 Swap ::
79 Instr inp (x ': y ': vs) es r ->
80 Instr inp (y ': x ': vs) es r
81 -- | @('Choices' ps bs d)@.
82 Choices ::
83 [InstrPure (v -> Bool)] ->
84 [Instr inp vs es ret] ->
85 Instr inp vs es ret ->
86 Instr inp (v ': vs) es ret
87 -- | @('Subroutine' n v k)@ binds the 'LetName' @(n)@ to the 'Instr'uction's @(v)@,
88 -- 'Call's @(n)@ and
89 -- continues with the next 'Instr'uction @(k)@.
90 Subroutine ::
91 LetName v -> Instr inp '[] ('Succ 'Zero) v ->
92 Instr inp vs ('Succ es) ret ->
93 Instr inp vs ('Succ es) ret
94 -- | @('Jump' n k)@ pass the control-flow to the 'Subroutine' named @(n)@.
95 Jump ::
96 LetName ret ->
97 Instr inp '[] ('Succ es) ret
98 -- | @('Call' n k)@ pass the control-flow to the 'Subroutine' named @(n)@,
99 -- and when it 'Ret'urns, continues with the next 'Instr'uction @(k)@.
100 Call ::
101 LetName v ->
102 Instr inp (v ': vs) ('Succ es) ret ->
103 Instr inp vs ('Succ es) ret
104 -- | @('Ret')@ returns the value stored in a singleton 'valueStack'.
105 Ret ::
106 Instr inp '[ret] es ret
107 -- | @('Read' expected p k)@ reads a 'Char' @(c)@ from the 'inp'ut,
108 -- if @(p c)@ is 'True' then continues with the next 'Instr'uction @(k)@ on,
109 -- otherwise 'Fail'.
110 Read ::
111 [ErrorItem (InputToken inp)] ->
112 InstrPure (InputToken inp -> Bool) ->
113 Instr inp (InputToken inp ': vs) ('Succ es) ret ->
114 Instr inp vs ('Succ es) ret
115 DefJoin ::
116 LetName v -> Instr inp (v ': vs) es ret ->
117 Instr inp vs es ret ->
118 Instr inp vs es ret
119 RefJoin ::
120 LetName v ->
121 Instr inp (v ': vs) es ret
122
123 -- ** Type 'InstrPure'
124 data InstrPure a where
125 InstrPure :: H.CombPure a -> InstrPure a
126 InstrPureSameOffset :: CodeQ (cur -> cur -> Bool) -> InstrPure (cur -> cur -> Bool)
127 InstrP
128
129 instance Show (InstrPure a) where
130 showsPrec p = \case
131 InstrPure x -> showsPrec p x
132 InstrPureSameOffset{} -> showString "InstrPureSameOffset"
133 instance Trans InstrPure TH.CodeQ where
134 trans = \case
135 InstrPure x -> trans x
136 InstrPureSameOffset x -> x
137
138 -- ** Type 'LetName'
139 newtype LetName a = LetName { unLetName :: TH.Name }
140 deriving (Eq)
141 deriving newtype Show
142
143 -- * Class 'Executable'
144 type Executable repr =
145 ( Stackable repr
146 , Branchable repr
147 , Failable repr
148 , Inputable repr
149 , Routinable repr
150 , Joinable repr
151 )
152
153 -- ** Class 'Stackable'
154 class Stackable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
155 push ::
156 InstrPure v ->
157 repr inp (v ': vs) n ret ->
158 repr inp vs n ret
159 pop ::
160 repr inp vs n ret ->
161 repr inp (v ': vs) n ret
162 liftI2 ::
163 InstrPure (x -> y -> z) ->
164 repr inp (z ': vs) es ret ->
165 repr inp (y ': x ': vs) es ret
166 swap ::
167 repr inp (x ': y ': vs) n r ->
168 repr inp (y ': x ': vs) n r
169
170 -- ** Class 'Branchable'
171 class Branchable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
172 case_ ::
173 repr inp (x ': vs) n r ->
174 repr inp (y ': vs) n r ->
175 repr inp (Either x y ': vs) n r
176 choices ::
177 [InstrPure (v -> Bool)] ->
178 [repr inp vs es ret] ->
179 repr inp vs es ret ->
180 repr inp (v ': vs) es ret
181
182 -- ** Class 'Failable'
183 class Failable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
184 fail :: [ErrorItem (InputToken inp)] -> repr inp vs ('Succ es) ret
185 popFail ::
186 repr inp vs es ret ->
187 repr inp vs ('Succ es) ret
188 catchFail ::
189 repr inp vs ('Succ es) ret ->
190 repr inp (Cursor inp ': vs) es ret ->
191 repr inp vs es ret
192
193 -- ** Class 'Inputable'
194 class Inputable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
195 loadInput ::
196 repr inp vs es r ->
197 repr inp (Cursor inp ': vs) es r
198 pushInput ::
199 repr inp (Cursor inp ': vs) es ret ->
200 repr inp vs es ret
201
202 -- ** Class 'Routinable'
203 class Routinable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
204 subroutine ::
205 LetName v -> repr inp '[] ('Succ 'Zero) v ->
206 repr inp vs ('Succ es) ret ->
207 repr inp vs ('Succ es) ret
208 call ::
209 LetName v -> repr inp (v ': vs) ('Succ es) ret ->
210 repr inp vs ('Succ es) ret
211 ret ::
212 repr inp '[ret] es ret
213 jump ::
214 LetName ret ->
215 repr inp '[] ('Succ es) ret
216
217 -- ** Class 'Joinable'
218 class Joinable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
219 defJoin ::
220 LetName v ->
221 repr inp (v ': vs) es ret ->
222 repr inp vs es ret ->
223 repr inp vs es ret
224 refJoin ::
225 LetName v ->
226 repr inp (v ': vs) es ret
227
228 -- ** Class 'Readable'
229 class Readable (repr :: Type -> [Type] -> Peano -> Type -> Type) (tok::Type) where
230 read ::
231 tok ~ InputToken inp =>
232 [ErrorItem tok] ->
233 InstrPure (tok -> Bool) ->
234 repr inp (tok ': vs) ('Succ es) ret ->
235 repr inp vs ('Succ es) ret
236
237 instance
238 ( Executable repr
239 , Readable repr (InputToken inp)
240 ) => Trans (Instr inp vs es) (repr inp vs es) where
241 trans = \case
242 Push x k -> push x (trans k)
243 Pop k -> pop (trans k)
244 LiftI2 f k -> liftI2 f (trans k)
245 Fail err -> fail err
246 PopFail k -> popFail (trans k)
247 CatchFail l r -> catchFail (trans l) (trans r)
248 LoadInput k -> loadInput (trans k)
249 PushInput k -> pushInput (trans k)
250 Case l r -> case_ (trans l) (trans r)
251 Swap k -> swap (trans k)
252 Choices ps bs d -> choices ps (trans Functor.<$> bs) (trans d)
253 Subroutine n sub k -> subroutine n (trans sub) (trans k)
254 Jump n -> jump n
255 Call n k -> call n (trans k)
256 Ret -> ret
257 Read es p k -> read es p (trans k)
258 DefJoin n sub k -> defJoin n (trans sub) (trans k)
259 RefJoin n -> refJoin n
260
261 -- ** Type 'Peano'
262 -- | Type-level natural numbers, using the Peano recursive encoding.
263 data Peano = Zero | Succ Peano
264
265 -- | @('Fmap' f k)@.
266 pattern Fmap ::
267 InstrPure (x -> y) ->
268 Instr inp (y ': xs) es ret ->
269 Instr inp (x ': xs) es ret
270 pattern Fmap f k = Push f (LiftI2 (InstrPure (H.Flip H.:@ (H.:$))) k)
271
272 -- | @('App' k)@ pops @(x)@ and @(x2y)@ from the 'valueStack',
273 -- pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
274 pattern App ::
275 Instr inp (y : vs) es ret ->
276 Instr inp (x : (x -> y) : vs) es ret
277 pattern App k = LiftI2 (InstrPure (H.:$)) k
278
279 -- | @('If' ok ko)@ pops a 'Bool' from the 'valueStack'
280 -- and continues either with the 'Instr'uction @(ok)@ if it is 'True'
281 -- or @(ko)@ otherwise.
282 pattern If ::
283 Instr inp vs es ret ->
284 Instr inp vs es ret ->
285 Instr inp (Bool ': vs) es ret
286 pattern If ok ko = Choices [InstrPure H.Id] [ok] ko
287
288 -- * Type 'Machine'
289 -- | Making the control-flow explicit.
290 data Machine inp v = Machine { unMachine ::
291 forall vs es ret.
292 {-k-}Instr inp (v ': vs) ('Succ es) ret ->
293 Instr inp vs ('Succ es) ret
294 }
295
296 runMachine ::
297 forall inp v es repr.
298 Executable repr =>
299 Readable repr (InputToken inp) =>
300 Machine inp v -> repr inp '[] ('Succ es) v
301 runMachine (Machine auto) =
302 trans @(Instr inp '[] ('Succ es)) $
303 auto Ret
304
305 instance Applicable (Machine inp) where
306 pure x = Machine $ Push (InstrPure x)
307 Machine f <*> Machine x = Machine $ f . x . App
308 liftA2 f (Machine x) (Machine y) = Machine $
309 x . y . LiftI2 (InstrPure f)
310 Machine x *> Machine y = Machine $ x . Pop . y
311 Machine x <* Machine y = Machine $ x . y . Pop
312 instance
313 Cursorable (Cursor inp) =>
314 Alternable (Machine inp) where
315 empty = Machine $ \_k -> Fail []
316 Machine l <|> Machine r = Machine $ \k ->
317 makeJoin k $ \j ->
318 CatchFail
319 (l (PopFail j))
320 (failIfConsumed (r j))
321 try (Machine x) = Machine $ \k ->
322 CatchFail (x (PopFail k))
323 -- On exception, reset the input,
324 -- and propagate the failure.
325 (LoadInput (Fail []))
326
327 -- | If no input has been consumed by the failing alternative
328 -- then continue with the given continuation.
329 -- Otherwise, propagate the 'Fail'ure.
330 failIfConsumed ::
331 Cursorable (Cursor inp) =>
332 Instr inp vs ('Succ es) ret ->
333 Instr inp (Cursor inp : vs) ('Succ es) ret
334 failIfConsumed k = PushInput (LiftI2 (InstrPureSameOffset sameOffset) (If k (Fail [])))
335
336 -- | @('makeJoin' k f)@ factorizes @(k)@ in @(f)@,
337 -- by introducing a 'DefJoin' if necessary,
338 -- and passing the corresponding 'RefJoin' to @(f)@,
339 -- or @(k)@ as is when factorizing is useless.
340 makeJoin ::
341 Instr inp (v : vs) es ret ->
342 (Instr inp (v : vs) es ret -> Instr inp vs es ret) ->
343 Instr inp vs es ret
344 -- Double RefJoin Optimization:
345 -- If a join-node points directly to another join-node,
346 -- then reuse it
347 makeJoin k@RefJoin{} = ($ k)
348 -- Terminal RefJoin Optimization:
349 -- If a join-node points directly to a terminal operation,
350 -- then it's useless to introduce a join-point.
351 makeJoin k@Ret = ($ k)
352 makeJoin k =
353 let joinName = LetName $ unsafePerformIO $ TH.qNewName "join" in
354 \f -> DefJoin joinName k (f (RefJoin joinName))
355
356 instance tok ~ InputToken inp => Satisfiable (Machine inp) tok where
357 satisfy es p = Machine $ Read es (InstrPure p)
358 instance Selectable (Machine inp) where
359 branch (Machine lr) (Machine l) (Machine r) = Machine $ \k ->
360 makeJoin k $ \j ->
361 lr (Case (l (Swap (App j)))
362 (r (Swap (App j))))
363 instance Matchable (Machine inp) where
364 conditional ps bs (Machine m) (Machine default_) = Machine $ \k ->
365 makeJoin k $ \j ->
366 m (Choices (InstrPure Functor.<$> ps)
367 ((\b -> unMachine b j) Functor.<$> bs)
368 (default_ j))
369 instance
370 ( Ord (InputToken inp)
371 , Cursorable (Cursor inp)
372 ) => Lookable (Machine inp) where
373 look (Machine x) = Machine $ \k ->
374 PushInput (x (Swap (LoadInput k)))
375 eof = negLook (satisfy [{-discarded by negLook-}] (H.const H..@ H.bool True))
376 -- Set a better failure message
377 <|> (Machine $ \_k -> Fail [ErrorItemEnd])
378 negLook (Machine x) = Machine $ \k ->
379 CatchFail
380 -- On x success, discard the result,
381 -- and replace this 'CatchFail''s failure handler
382 -- by a 'Fail'ure whose 'farthestExpecting' is negated,
383 -- then a failure is raised from the input
384 -- when entering 'negLook', to avoid odd cases:
385 -- - where the failure that made (negLook x)
386 -- succeed can get the blame for the overall
387 -- failure of the grammar.
388 -- - where the overall failure of
389 -- the grammar might be blamed on something in x
390 -- that, if corrected, still makes x succeed and
391 -- (negLook x) fail.
392 (PushInput (x (Pop (PopFail (LoadInput (Fail []))))))
393 -- On x failure, reset the input,
394 -- and go on with the next 'Instr'uctions.
395 (LoadInput (Push (InstrPure H.unit) k))
396 instance Letable TH.Name (Machine inp) where
397 def n v = Machine $ \k ->
398 Subroutine (LetName n) (unMachine v Ret) (Call (LetName n) k)
399 ref _isRec n = Machine $ \case
400 Ret -> Jump (LetName n)
401 k -> Call (LetName n) k
402 instance Cursorable (Cursor inp) => Foldable (Machine inp) where
403 {-
404 chainPre op p = go <*> p
405 where go = (H..) <$> op <*> go <|> pure H.id
406 chainPost p op = p <**> go
407 where go = (H..) <$> op <*> go <|> pure H.id
408 -}