1 {-# LANGUAGE PatternSynonyms #-} -- For Instr
2 {-# LANGUAGE ViewPatterns #-} -- For unSomeInstr
3 {-# LANGUAGE UndecidableInstances #-}
4 -- | Initial encoding with bottom-up optimizations of 'Instr'uctions,
5 -- re-optimizing downward as needed after each optimization.
6 -- There is only one optimization (for 'push') so far,
7 -- but the introspection enabled by the 'Instr' data-type
8 -- is also useful to optimize with more context in the 'Machine'.
9 module Symantic.Parser.Machine.Optimize where
11 import Data.Bool (Bool(..))
12 import Data.Either (Either)
13 import Data.Maybe (Maybe(..))
14 import Data.Function ((.))
15 import Data.Kind (Constraint)
16 import Type.Reflection (Typeable, typeRep, eqTypeRep, (:~~:)(..))
17 import qualified Data.Functor as Functor
19 import Symantic.Parser.Grammar
20 import Symantic.Parser.Machine.Input
21 import Symantic.Parser.Machine.Instructions
22 import Symantic.Univariant.Trans
24 -- * Data family 'Instr'
25 -- | 'Instr'uctions of the 'Machine'.
26 -- This is an extensible data-type.
28 (instr :: ReprInstr -> Constraint)
32 -- | Convenient utility to pattern-match a 'SomeInstr'.
33 pattern Instr :: Typeable comb =>
34 Instr comb repr inp vs es a ->
35 SomeInstr repr inp vs es a
36 pattern Instr x <- (unSomeInstr -> Just x)
38 -- ** Type 'SomeInstr'
39 -- | Some 'Instr'uction existantialized over the actual instruction symantic class.
40 -- Useful to handle a list of 'Instr'uctions
41 -- without requiring impredicative quantification.
42 -- Must be used by pattern-matching
43 -- on the 'SomeInstr' data-constructor,
44 -- to bring the constraints in scope.
46 -- As in 'SomeComb', a first pass of optimizations
47 -- is directly applied in it
48 -- to avoid introducing an extra newtype,
49 -- this also give a more comprehensible code.
50 data SomeInstr repr inp vs es a =
52 (Trans (Instr instr repr inp vs es) (repr inp vs es), Typeable instr) =>
53 SomeInstr (Instr instr repr inp vs es a)
55 instance Trans (SomeInstr repr inp vs es) (repr inp vs es) where
56 trans (SomeInstr x) = trans x
58 -- | @(unSomeInstr i :: 'Maybe' ('Instr' comb repr inp vs es a))@
59 -- extract the data-constructor from the given 'SomeInstr'
60 -- iif. it belongs to the @('Instr' comb repr a)@ data-instance.
62 forall instr repr inp vs es a.
64 SomeInstr repr inp vs es a ->
65 Maybe (Instr instr repr inp vs es a)
66 unSomeInstr (SomeInstr (i::Instr i repr inp vs es a)) =
67 case typeRep @instr `eqTypeRep` typeRep @i of
72 data instance Instr Stackable repr inp vs fs a where
73 -- | @('Push' x k)@ pushes @(x)@ on the 'valueStack'
74 -- and continues with the next 'Instr'uction @(k)@.
77 SomeInstr repr inp (v ': vs) es a ->
78 Instr Stackable repr inp vs es a
79 -- | @('Pop' k)@ pushes @(x)@ on the 'valueStack'.
81 SomeInstr repr inp vs es a ->
82 Instr Stackable repr inp (v ': vs) es a
83 -- | @('LiftI2' f k)@ pops two values from the 'valueStack',
84 -- and pushes the result of @(f)@ applied to them.
86 TermInstr (x -> y -> z) ->
87 SomeInstr repr inp (z : vs) es a ->
88 Instr Stackable repr inp (y : x : vs) es a
89 -- | @('Swap' k)@ pops two values on the 'valueStack',
90 -- pushes the first popped-out, then the second,
91 -- and continues with the next 'Instr'uction @(k)@.
93 SomeInstr repr inp (x ': y ': vs) es a ->
94 Instr Stackable repr inp (y ': x ': vs) es a
95 instance Stackable repr => Trans (Instr Stackable repr inp vs es) (repr inp vs es) where
97 Push x k -> push x (trans k)
98 Pop k -> pop (trans k)
99 LiftI2 f k -> liftI2 f (trans k)
100 Swap k -> swap (trans k)
101 instance Stackable repr => Stackable (SomeInstr repr) where
102 push _v (Instr (Pop i)) = i
103 push v i = SomeInstr (Push v i)
104 pop = SomeInstr . Pop
105 liftI2 f = SomeInstr . LiftI2 f
106 swap = SomeInstr . Swap
109 data instance Instr Routinable repr inp vs fs a where
110 -- | @('Subroutine' n v k)@ binds the 'LetName' @(n)@ to the 'Instr'uction's @(v)@,
112 -- continues with the next 'Instr'uction @(k)@.
114 LetName v -> SomeInstr repr inp '[] ('Succ 'Zero) v ->
115 SomeInstr repr inp vs ('Succ es) a ->
116 Instr Routinable repr inp vs ('Succ es) a
117 -- | @('Jump' n k)@ pass the control-flow to the 'Subroutine' named @(n)@.
120 Instr Routinable repr inp '[] ('Succ es) a
121 -- | @('Call' n k)@ pass the control-flow to the 'Subroutine' named @(n)@,
122 -- and when it 'Ret'urns, continues with the next 'Instr'uction @(k)@.
125 SomeInstr repr inp (v ': vs) ('Succ es) a ->
126 Instr Routinable repr inp vs ('Succ es) a
127 -- | @('Ret')@ returns the value stored in a singleton 'valueStack'.
129 Instr Routinable repr inp '[a] es a
130 instance Routinable repr => Trans (Instr Routinable repr inp vs es) (repr inp vs es) where
132 Subroutine n sub k -> subroutine n (trans sub) (trans k)
134 Call n k -> call n (trans k)
136 instance Routinable repr => Routinable (SomeInstr repr) where
137 subroutine n sub = SomeInstr . Subroutine n sub
138 jump = SomeInstr . Jump
139 call n = SomeInstr . Call n
143 data instance Instr Branchable repr inp vs fs a where
146 SomeInstr repr inp (x ': vs) es a ->
147 SomeInstr repr inp (y ': vs) es a ->
148 Instr Branchable repr inp (Either x y ': vs) es a
149 -- | @('Choices' ps bs d)@.
151 [TermInstr (v -> Bool)] ->
152 [SomeInstr repr inp vs es a] ->
153 SomeInstr repr inp vs es a ->
154 Instr Branchable repr inp (v ': vs) es a
155 instance Branchable repr => Trans (Instr Branchable repr inp vs es) (repr inp vs es) where
157 Case l r -> caseI (trans l) (trans r)
158 Choices ps bs d -> choices ps (trans Functor.<$> bs) (trans d)
159 instance Branchable repr => Branchable (SomeInstr repr) where
160 caseI l = SomeInstr . Case l
161 choices ps bs = SomeInstr . Choices ps bs
164 data instance Instr Failable repr inp vs fs a where
165 -- | @('Fail')@ raises an error from the 'failStack'.
167 [ErrorItem (InputToken inp)] ->
168 Instr Failable repr inp vs ('Succ es) a
169 -- | @('PopFail' k)@ removes a 'FailHandler' from the 'failStack'
170 -- and continues with the next 'Instr'uction @(k)@.
172 SomeInstr repr inp vs es ret ->
173 Instr Failable repr inp vs ('Succ es) ret
174 -- | @('CatchFail' l r)@ tries the @(l)@ 'Instr'uction
175 -- in a new failure scope such that if @(l)@ raises a failure, it is caught,
176 -- then the input is pushed as it was before trying @(l)@ on the 'valueStack',
177 -- and the control flow goes on with the @(r)@ 'Instr'uction.
179 SomeInstr repr inp vs ('Succ es) ret ->
180 SomeInstr repr inp (Cursor inp ': vs) es ret ->
181 Instr Failable repr inp vs es ret
182 instance Failable repr => Trans (Instr Failable repr inp vs es) (repr inp vs es) where
185 PopFail k -> popFail (trans k)
186 CatchFail l r -> catchFail (trans l) (trans r)
187 instance Failable repr => Failable (SomeInstr repr) where
188 fail = SomeInstr . Fail
189 popFail = SomeInstr . PopFail
190 catchFail x = SomeInstr . CatchFail x
193 data instance Instr Inputable repr inp vs fs a where
194 -- | @('LoadInput' k)@ removes the input from the 'valueStack'
195 -- and continues with the next 'Instr'uction @(k)@ using that input.
197 SomeInstr repr inp vs es a ->
198 Instr Inputable repr inp (Cursor inp : vs) es a
199 -- | @('PushInput' k)@ pushes the input @(inp)@ on the 'valueStack'
200 -- and continues with the next 'Instr'uction @(k)@.
202 SomeInstr repr inp (Cursor inp ': vs) es a ->
203 Instr Inputable repr inp vs es a
204 instance Inputable repr => Trans (Instr Inputable repr inp vs es) (repr inp vs es) where
206 LoadInput k -> loadInput (trans k)
207 PushInput k -> pushInput (trans k)
208 instance Inputable repr => Inputable (SomeInstr repr) where
209 loadInput = SomeInstr . LoadInput
210 pushInput = SomeInstr . PushInput
213 data instance Instr Joinable repr inp vs fs a where
215 LetName v -> SomeInstr repr inp (v ': vs) es a ->
216 SomeInstr repr inp vs es a ->
217 Instr Joinable repr inp vs es a
220 Instr Joinable repr inp (v ': vs) es a
221 instance Joinable repr => Trans (Instr Joinable repr inp vs es) (repr inp vs es) where
223 DefJoin n sub k -> defJoin n (trans sub) (trans k)
224 RefJoin n -> refJoin n
225 instance Joinable repr => Joinable (SomeInstr repr) where
226 defJoin n sub = SomeInstr . DefJoin n sub
227 refJoin = SomeInstr . RefJoin
230 data instance Instr (Readable tok) repr inp vs fs a where
231 -- | @('Read' expected p k)@ reads a 'Char' @(c)@ from the 'inp'ut,
232 -- if @(p c)@ is 'True' then continues with the next 'Instr'uction @(k)@ on,
235 [ErrorItem (InputToken inp)] ->
236 TermInstr (InputToken inp -> Bool) ->
237 SomeInstr repr inp (InputToken inp ': vs) ('Succ es) a ->
238 Instr (Readable tok) repr inp vs ('Succ es) a
240 ( Readable tok repr, tok ~ InputToken inp ) =>
241 Trans (Instr (Readable tok) repr inp vs es) (repr inp vs es) where
243 Read es p k -> read es p (trans k)
245 ( Readable tok repr, Typeable tok ) =>
246 Readable tok (SomeInstr repr) where
247 read es p = SomeInstr . Read es p