1 {-# LANGUAGE ConstraintKinds #-} -- For Executable
2 {-# LANGUAGE PatternSynonyms #-} -- For Fmap, App, …
3 {-# LANGUAGE DerivingStrategies #-} -- For Show (Label a)
4 module Symantic.Parser.Automaton.Instructions where
6 import Data.Bool (Bool)
7 import Data.Char (Char)
8 import Data.Either (Either)
10 import Data.Function (($), (.))
11 import Data.Kind (Type)
12 import Text.Show (Show(..), showString)
13 import qualified Data.Functor as Functor
14 import qualified Language.Haskell.TH as TH
15 import qualified Symantic.Parser.Staging as H
17 import Symantic.Parser.Grammar
18 import Symantic.Parser.Automaton.Input
19 import Symantic.Univariant.Trans
22 -- | 'Instr'uctions for the 'Automaton'.
23 data Instr input valueStack (exceptionStack::Peano) returnValue where
24 -- | @('Push' x k)@ pushes @(x)@ on the value-stack
25 -- and continues with the next 'Instr'uction @(k)@.
28 Instr inp (v ': vs) es ret ->
30 -- | @('Pop' k)@ pushes @(x)@ on the value-stack.
32 Instr inp vs es ret ->
33 Instr inp (v ': vs) es ret
34 -- | @('LiftI2' f k)@ pops two values from the value-stack,
35 -- and pushes the result of @(f)@ applied to them.
37 InstrPure (x -> y -> z) ->
38 Instr inp (z : vs) es ret ->
39 Instr inp (y : x : vs) es ret
40 -- | @('Fail')@ raises an error from the exception-stack.
42 Instr inp vs ('Succ es) ret
43 -- | @('Commit' k)@ removes an exception from the exception-stack
44 -- and continues with the next 'Instr'uction @(k)@.
46 Instr inp vs es ret ->
47 Instr inp vs ('Succ es) ret
48 -- | @('Catch' l r)@ tries the @(l)@ 'Instr'uction,
49 -- if it raises an exception, catches it,
50 -- pushes the input as it was before trying @(l)@ on the value-stack,
51 -- and continues with the @(r)@ 'Instr'uction.
53 Instr inp vs ('Succ es) ret ->
54 Instr inp (inp ': vs) es ret ->
56 -- | @('Seek' k)@ removes the input from the value-stack
57 -- and continues with the next 'Instr'uction @(k)@.
60 Instr inp (inp : vs) es r
61 -- | @('Tell' k)@ pushes the input @(inp)@ on the value-stack
62 -- and continues with the next 'Instr'uction @(k)@.
64 Instr inp (inp ': vs) es ret ->
68 Instr inp (x ': vs) es r ->
69 Instr inp (y ': vs) es r ->
70 Instr inp (Either x y ': vs) es r
71 -- | @('Swap' k)@ pops two values on the value-stack,
72 -- pushes the first popped-out, then the second,
73 -- and continues with the next 'Instr'uction @(k)@.
75 Instr inp (x ': y ': vs) es r ->
76 Instr inp (y ': x ': vs) es r
77 -- | @('Choices' ps bs d)@.
79 [InstrPure (v -> Bool)] ->
80 [Instr inp vs es ret] ->
81 Instr inp vs es ret ->
82 Instr inp (v ': vs) es ret
83 -- | @('Subroutine' n v k)@ binds the 'Label' @(n)@ to the 'Instr'uction's @(v)@,
85 -- continues with the next 'Instr'uction @(k)@.
87 Label v -> Instr inp '[] ('Succ 'Zero) v ->
88 Instr inp vs ('Succ es) ret ->
89 Instr inp vs ('Succ es) ret
90 -- | @('Jump' n k)@ pass the control-flow to the 'Subroutine' named @(n)@.
93 Instr inp '[] ('Succ es) ret
94 -- | @('Call' n k)@ pass the control-flow to the 'Subroutine' named @(n)@,
95 -- and when it 'Ret'urns, continues with the next 'Instr'uction @(k)@.
98 Instr inp (v ': vs) ('Succ es) ret ->
99 Instr inp vs ('Succ es) ret
100 -- | @('Ret')@ returns the value stored in a singleton value-stack.
102 Instr inp '[ret] es ret
103 -- | @('Read' p k)@ reads a 'Char' @(c)@ from the 'inp'ut,
104 -- if @(p c)@ is 'True' then continues with the next 'Instr'uction @(k)@ on,
107 InstrPure (Char -> Bool) ->
108 Instr inp (Char ': vs) ('Succ es) ret ->
109 Instr inp vs ('Succ es) ret
111 -- ** Type 'InstrPure'
112 data InstrPure a where
113 InstrPureHaskell :: H.Haskell a -> InstrPure a
114 InstrPureSameOffset :: Cursorable inp => InstrPure (inp -> inp -> Bool)
116 instance Show (InstrPure a) where
118 InstrPureHaskell x -> showsPrec p x
119 InstrPureSameOffset -> showString "InstrPureSameOffset"
120 instance Trans InstrPure TH.CodeQ where
122 InstrPureHaskell x -> trans x
123 InstrPureSameOffset -> same
126 newtype Label a = Label { unLabel :: TH.Name }
128 deriving newtype Show
130 -- * Class 'Executable'
131 type Executable repr =
140 -- ** Class 'Stackable'
141 class Stackable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
144 repr inp (v ': vs) n ret ->
148 repr inp (v ': vs) n ret
150 InstrPure (x -> y -> z) ->
151 repr inp (z ': vs) es ret ->
152 repr inp (y ': x ': vs) es ret
154 repr inp (x ': y ': vs) n r ->
155 repr inp (y ': x ': vs) n r
157 -- ** Class 'Branchable'
158 class Branchable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
160 repr inp (x ': vs) n r ->
161 repr inp (y ': vs) n r ->
162 repr inp (Either x y ': vs) n r
164 [InstrPure (v -> Bool)] ->
165 [repr inp vs es ret] ->
166 repr inp vs es ret ->
167 repr inp (v ': vs) es ret
169 -- ** Class 'Exceptionable'
170 class Exceptionable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
171 fail :: repr inp vs ('Succ es) ret
173 repr inp vs es ret ->
174 repr inp vs ('Succ es) ret
176 repr inp vs ('Succ es) ret ->
177 repr inp (inp ': vs) es ret ->
180 -- ** Class 'Inputable'
181 class Inputable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
184 repr inp (inp ': vs) es r
186 repr inp (inp ': vs) es ret ->
189 -- ** Class 'Routinable'
190 class Routinable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
192 Label v -> repr inp '[] ('Succ 'Zero) v ->
193 repr inp vs ('Succ es) ret ->
194 repr inp vs ('Succ es) ret
196 Label v -> repr inp (v ': vs) ('Succ es) ret ->
197 repr inp vs ('Succ es) ret
199 repr inp '[ret] es ret
202 repr inp '[] ('Succ es) ret
204 -- ** Class 'Readable'
205 class Readable (repr :: Type -> [Type] -> Peano -> Type -> Type) where
207 InstrPure (Char -> Bool) ->
208 repr inp (Char ': vs) ('Succ es) ret ->
209 repr inp vs ('Succ es) ret
213 Trans (Instr inp vs es) (repr inp vs es) where
215 Push x k -> push x (trans k)
216 Pop k -> pop (trans k)
217 LiftI2 f k -> liftI2 f (trans k)
219 Commit k -> commit (trans k)
220 Catch l r -> catch (trans l) (trans r)
221 Seek k -> seek (trans k)
222 Tell k -> tell (trans k)
223 Case l r -> case_ (trans l) (trans r)
224 Swap k -> swap (trans k)
225 Choices ps bs d -> choices ps (trans Functor.<$> bs) (trans d)
226 Subroutine n sub k -> subroutine n (trans sub) (trans k)
228 Call n k -> call n (trans k)
230 Read p k -> read p (trans k)
233 -- | Type-level natural numbers, using the Peano recursive encoding.
234 data Peano = Zero | Succ Peano
238 InstrPure (x -> y) ->
239 Instr inp (y ': xs) es ret ->
240 Instr inp (x ': xs) es ret
241 pattern Fmap f k = Push f (LiftI2 (InstrPureHaskell (H.Flip H.:@ (H.:$))) k)
243 -- | @('App' k)@ pops @(x)@ and @(x2y)@ from the value-stack,
244 -- pushes @(x2y x)@ and continues with the next 'Instr'uction @(k)@.
246 Instr inp (y : vs) es ret ->
247 Instr inp (x : (x -> y) : vs) es ret
248 pattern App k = LiftI2 (InstrPureHaskell (H.:$)) k
250 -- | @('If' ok ko)@ pops a 'Bool' from the value-stack
251 -- and continues either with the 'Instr'uction @(ok)@ if it is 'True'
252 -- or @(ko)@ otherwise.
254 Instr inp vs es ret ->
255 Instr inp vs es ret ->
256 Instr inp (Bool ': vs) es ret
257 pattern If ok ko = Choices [InstrPureHaskell H.Id] [ok] ko
261 Instr inp vs ('Succ es) ret ->
262 Instr inp (inp : vs) ('Succ es) ret
263 parsecHandler k = Tell (LiftI2 InstrPureSameOffset (If k Fail))
265 -- * Type 'Automaton'
266 -- | Making the control-flow explicit.
267 data Automaton inp v = Automaton { unAutomaton ::
269 {-k-}Instr inp (v ': vs) ('Succ es) ret ->
270 Instr inp vs ('Succ es) ret
274 forall inp v es repr.
276 Automaton inp v -> repr inp '[] ('Succ es) v
277 runAutomaton (Automaton auto) =
278 trans @(Instr inp '[] ('Succ es)) $
281 instance Applicable (Automaton inp) where
282 pure x = Automaton $ Push (InstrPureHaskell x)
283 Automaton f <*> Automaton x = Automaton $ f . x . App
284 liftA2 f (Automaton x) (Automaton y) = Automaton $
285 x . y . LiftI2 (InstrPureHaskell f)
286 Automaton x *> Automaton y = Automaton $ x . Pop . y
287 Automaton x <* Automaton y = Automaton $ x . y . Pop
290 Alternable (Automaton inp) where
291 empty = Automaton $ \_k -> Fail
292 Automaton l <|> Automaton r = Automaton $ \k ->
294 Catch (l (Commit k)) (parsecHandler (r k))
295 try (Automaton x) = Automaton $ \k ->
296 Catch (x (Commit k)) (Seek Fail)
297 instance Charable (Automaton inp) where
298 satisfy p = Automaton $ Read (InstrPureHaskell p)
299 instance Selectable (Automaton inp) where
300 branch (Automaton lr) (Automaton l) (Automaton r) = Automaton $ \k ->
302 lr (Case (l (Swap (App k)))
304 instance Matchable (Automaton inp) where
305 conditional ps bs (Automaton a) (Automaton default_) = Automaton $ \k ->
307 a (Choices (InstrPureHaskell Functor.<$> ps)
308 ((\b -> unAutomaton b k) Functor.<$> bs)
310 instance Lookable (Automaton inp) where
311 look (Automaton x) = Automaton $ \k ->
312 Tell (x (Swap (Seek k)))
313 negLook (Automaton x) = Automaton $ \k ->
314 Catch (Tell (x (Pop (Seek (Commit Fail)))))
315 (Seek (Push (InstrPureHaskell H.unit) k))
316 instance Letable TH.Name (Automaton inp) where
317 def n v = Automaton $ \k ->
318 Subroutine (Label n) (unAutomaton v Ret) (Call (Label n) k)
321 -- Subroutine (Label n) (v Ret) (v k)
322 ref _isRec n = Automaton $ \case
323 Ret -> Jump (Label n)
324 k -> Call (Label n) k
325 instance Cursorable inp => Foldable (Automaton inp) where
327 chainPre op p = go <*> p
328 where go = (H..) <$> op <*> go <|> pure H.id
329 chainPost p op = p <**> go
330 where go = (H..) <$> op <*> go <|> pure H.id