0 | ||| The content of this module is based on the MSc Thesis
  1 | ||| Coinductive Formalization of SECD Machine in Agda
  2 | ||| by Adam Krupička
  3 |
  4 | module Language.IntrinsicTyping.SECD
  5 |
  6 | import public Data.Late
  7 | import Data.List.Elem
  8 | import public Data.List.Quantifiers
  9 |
 10 | %default total
 11 |
 12 | ------------------------------------------------------------------------
 13 | -- Machine types
 14 |
 15 | public export
 16 | data Ty
 17 |   = TyInt
 18 |   | TyBool
 19 |   | TyPair Ty Ty
 20 |   | TyList Ty
 21 |   | TyFun Ty Ty
 22 |
 23 | %name Ty a,b
 24 |
 25 | public export
 26 | data Const : Ty -> Type where
 27 |   AnInt : Int -> Const TyInt
 28 |   True  : Const TyBool
 29 |   False : Const TyBool
 30 |
 31 | public export
 32 | fromInteger : Integer -> Const TyInt
 33 | fromInteger n = AnInt (cast n)
 34 |
 35 | ------------------------------------------------------------------------
 36 | -- Machine states
 37 |
 38 | public export
 39 | Stack : Type
 40 | Stack = List Ty
 41 |
 42 | public export
 43 | Env : Type
 44 | Env = List Ty
 45 |
 46 | public export
 47 | FunDump : Type
 48 | FunDump = List (Ty, Ty)
 49 |
 50 | public export
 51 | record State where
 52 |   constructor MkState
 53 |   stack : Stack
 54 |   env   : Env
 55 |   dump  : FunDump
 56 |
 57 | ------------------------------------------------------------------------
 58 | -- Instructions as state-transforming operations
 59 |
 60 | data Step  : State -> State -> Type
 61 | data Steps : State -> State -> Type
 62 |
 63 | public export
 64 | data Step  : State -> State -> Type where
 65 |   -- Loading
 66 |
 67 |   ||| Load a constant of a base type
 68 |   LDC : (c : Const ty) -> MkState s e f `Step` MkState (ty :: s) e f
 69 |   ||| Load a value from an address in the environment
 70 |   LDA : Elem ty e ->
 71 |         MkState s e f `Step` MkState (ty :: s) e f
 72 |   ||| Load a recursive function
 73 |   LDF : (MkState [] (a :: e) ((a, b) :: f) `Steps` MkState [b] (a :: e) ((a, b) :: f)) ->
 74 |         MkState s e f `Step` MkState (TyFun a b :: s) e f
 75 |   ||| Load a function for recursive application
 76 |   LDR : Elem (a,b) f ->
 77 |         MkState s e f `Step` MkState (TyFun a b :: s) e f
 78 |
 79 |   -- Applying & returning
 80 |
 81 |   ||| Apply a function to its argument
 82 |   APP : MkState (a :: TyFun a b :: s) e f `Step` MkState (b :: s) e f
 83 |   ||| Apply a function to its argument, tail call
 84 |   TAP : MkState (a :: TyFun a b :: s) e f `Step` MkState (b :: s) e f
 85 |   ||| Return a value from inside a function
 86 |   RTN : MkState (b :: s) e ((a, b) :: f) `Step` MkState [ b ] e ((a, b) :: f)
 87 |
 88 |   -- If destructor
 89 |
 90 |   ||| Branch over a boolean
 91 |   BCH : (l, r : MkState s e f `Steps` MkState s' e f) ->
 92 |         MkState (TyBool :: s) e f `Step` MkState s' e f
 93 |
 94 |   -- Stack manipulation
 95 |
 96 |   ||| Flip the stack's top values
 97 |   FLP : MkState (a :: b :: s) e f `Step` MkState (b :: a :: s) e f
 98 |
 99 |   -- List primitives
100 |
101 |   ||| Nil constructor
102 |   NIL : MkState s e f `Step` MkState (TyList a :: s) e f
103 |   ||| Cons constructor
104 |   CNS : MkState (a :: TyList a :: s) e f `Step` MkState (TyList a :: s) e f
105 |   ||| Head destructor
106 |   HED : MkState (TyList a :: s) e f `Step` MkState (a :: s) e f
107 |   ||| Tail destructor
108 |   TAL : MkState (TyList a :: s) e f `Step` MkState (TyList a :: s) e f
109 |
110 |   -- Pair primitives
111 |
112 |   ||| Pair constructor
113 |   MKP : MkState (a :: b :: s) e f `Step` MkState (TyPair a b :: s) e f
114 |   ||| First pair destructor
115 |   FST : MkState (TyPair a b :: s) e f `Step` MkState (a :: s) e f
116 |   ||| Second pair destructor
117 |   SND : MkState (TyPair a b :: s) e f `Step` MkState (b :: s) e f
118 |
119 |   -- Int primitives
120 |
121 |   ||| Addition of ints
122 |   ADD : MkState (TyInt :: TyInt :: s) e f `Step` MkState (TyInt :: s) e f
123 |   ||| Subtraction of ints
124 |   SUB : MkState (TyInt :: TyInt :: s) e f `Step` MkState (TyInt :: s) e f
125 |   ||| Multiplication of ints
126 |   MUL : MkState (TyInt :: TyInt :: s) e f `Step` MkState (TyInt :: s) e f
127 |
128 |   -- Bool primitives
129 |
130 |   ||| Structural equality test
131 |   EQB : {a : Ty} -> MkState (a :: a :: s) e f `Step` MkState (TyBool :: s) e f
132 |   ||| Boolean negation
133 |   NOT : MkState (TyBool :: s) e f `Step` MkState (TyBool :: s) e f
134 |
135 |
136 | ------------------------------------------------------------------------
137 | -- Reflexive transitive closures & combinators
138 |
139 | public export
140 | data Steps : State -> State -> Type where
141 |   Nil  : Steps s s
142 |   (::) : Step s t -> Steps t u -> Steps s u
143 |
144 | public export
145 | data Stepz : State -> State -> Type where
146 |   Lin  : Stepz s s
147 |   (:<) : Stepz s t -> Step t u -> Stepz s u
148 |
149 | public export
150 | (<>>) : Stepz s t -> Steps t u -> Steps s u
151 | [<] <>> ts = ts
152 | (ss :< s) <>> ts = ss <>> (s :: ts)
153 |
154 | public export
155 | (<><) : Stepz s t -> Steps t u -> Stepz s u
156 | ss <>< [] = ss
157 | ss <>< (t :: ts) = (ss :< t) <>< ts
158 |
159 | public export
160 | (++) : Steps s t -> Steps t u -> Steps s u
161 | [] ++ ts = ts
162 | (s :: ss) ++ ts = s :: (ss ++ ts)
163 |
164 | ------------------------------------------------------------------------
165 | -- Basic operations & examples
166 |
167 | public export
168 | NUL : {a : Ty} -> MkState (TyList a :: s) e f `Steps` MkState (TyBool :: s) e f
169 | NUL = [NIL, EQB]
170 |
171 | public export
172 | LDL : List Int -> MkState s e f `Steps` MkState (TyList TyInt :: s) e f
173 | LDL vs = go [<NIL] ([<] <>< vs) <>> [] where
174 |
175 |   go : MkState s e f `Stepz` MkState (TyList TyInt :: s) e f ->
176 |        SnocList Int ->
177 |        MkState s e f `Stepz` MkState (TyList TyInt :: s) e f
178 |   go acc [<] = acc
179 |   go acc (vs :< v) = go (acc :< LDC (AnInt v) :< CNS) vs
180 |
181 | FVE : MkState [] [] [] `Steps` MkState [TyInt] [] []
182 | FVE = [LDC 2, LDC 3, ADD]
183 |
184 | INC : MkState [] (TyInt :: e) ((TyInt, TyInt) :: f)
185 |      `Steps` MkState [TyInt] (TyInt :: e) ((TyInt, TyInt) :: f)
186 | INC =
187 |   [ LDA Here
188 |   , LDC 1
189 |   , ADD
190 |   ]
191 |
192 | INC2 : MkState [] [] [] `Steps` MkState [TyInt] [] []
193 | INC2 =
194 |   [ LDF INC
195 |   , LDC 2
196 |   , APP
197 |   ]
198 |
199 | THR : MkState [] [] [] `Steps` MkState [TyInt] [] []
200 | THR =
201 |   [ LDF [ LDF [LDA Here, LDA (There Here), ADD, RTN ], RTN ]
202 |   , LDC 1
203 |   , APP
204 |   , LDC 2
205 |   , APP
206 |   ]
207 |
208 | public export
209 | PLS : MkState s e f `Step` MkState (TyFun TyInt (TyFun TyInt TyInt) :: s) e f
210 | PLS = LDF [ LDF [ LDA Here
211 |                 , LDA (There Here)
212 |                 , ADD
213 |                 , RTN
214 |                 ]]
215 |
216 | public export
217 | MAP : {a : Ty} -> MkState [] e f `Step` MkState [ TyFun (TyFun a b) (TyFun (TyList a) (TyList b )) ] e f
218 | MAP = LDF [LDF ( LDA Here
219 |               :: NUL
220 |               ++ [ BCH [ NIL ]
221 |                        [ LDR Here, LDA Here, TAL, APP
222 |                        , LDA (There Here), LDA Here, HED, APP
223 |                        , CNS
224 |                        ]
225 |                  ]
226 |               )]
227 |
228 | public export
229 | FLD : {a : Ty} -> MkState [] e f `Step`
230 |       MkState [TyFun (TyFun b (TyFun a b)) (TyFun b (TyFun (TyList a) b))] e f
231 | FLD = LDF [ LDF [ LDF ( LDA Here
232 |                      :: NUL
233 |                      ++ [ BCH [ LDA (There Here) ]
234 |                               [ LDA (There (There Here)) -- c
235 |                               , LDA (There Here) -- n
236 |                               , APP -- c n
237 |                               , LDA Here -- x :: xs
238 |                               , HED
239 |                               , APP -- c n x
240 |                               , LDR (There Here) -- foldl c
241 |                               , FLP
242 |                               , APP -- foldl c (c n x)
243 |                               , LDA Here -- x :: xs
244 |                               , TAL -- xs
245 |                               , APP -- fold c (c n x) xs
246 |                               ]
247 |                         ])]]
248 |
249 | public export
250 | SUM : MkState [] e f `Steps`
251 |       MkState [TyFun (TyList TyInt) TyInt] e f
252 | SUM = [ FLD
253 |       , PLS
254 |       , APP
255 |       , LDC 0
256 |       , APP
257 |       ]
258 |
259 |
260 | ------------------------------------------------------------------------
261 | -- Meaning
262 |
263 | data Closure : (a, b : Ty) -> Type
264 |
265 | namespace Ty
266 |
267 |   public export
268 |   Meaning : Ty -> Type
269 |   Meaning TyInt = Int
270 |   Meaning TyBool = Bool
271 |   Meaning (TyPair a b) = (Meaning a, Meaning b)
272 |   Meaning (TyList a) = List (Meaning a)
273 |   Meaning (TyFun a b) = Closure a b
274 |
275 |   public export
276 |   fromConst : Const ty -> Meaning ty
277 |   fromConst (AnInt i) = i
278 |   fromConst True = True
279 |   fromConst False = False
280 |
281 | namespace StackOrEnv
282 |
283 |   public export
284 |   Meaning : List Ty -> Type
285 |   Meaning = All Meaning
286 |
287 | namespace FunDump
288 |
289 |   public export
290 |   0 Meaning : FunDump -> Type
291 |   Meaning [] = ()
292 |   Meaning ((a, b) :: f) = (Closure a b, Meaning f)
293 |
294 |   public export
295 |   tail : {0 f : FunDump} -> Meaning (ab :: f) -> Meaning f
296 |   tail {ab = (a, b)} (_, f) = f
297 |
298 |   public export
299 |   lookup : Meaning f -> Elem (a,b) f -> Closure a b
300 |   lookup (cl, _) Here = cl
301 |   lookup {f = (a, b) :: _} (_, f) (There p) = lookup f p
302 |
303 | namespace State
304 |
305 |   public export
306 |   record Meaning (st : State) where
307 |     constructor MkMeaning
308 |     stackVal : Meaning st.stack
309 |     envVal   : Meaning st.env
310 |     dumpVal  : Meaning st.dump
311 |
312 | public export
313 | record Closure (a, b : Ty) where
314 |   constructor MkClosure
315 |   {0 localEnv : Env}
316 |   {0 localFunDump : FunDump}
317 |   code : MkState [] (a :: localEnv) ((a, b) :: localFunDump)
318 |          `Steps` MkState [b] (a :: localEnv) ((a, b) :: localFunDump)
319 |   envVal : Meaning localEnv
320 |   dumpVal : Meaning localFunDump
321 |
322 | public export
323 | eqb : (ty : Ty) -> (l, r : Meaning ty) -> Bool
324 | public export
325 | eqbs : (ty : Ty) -> (l, r : Meaning (TyList ty)) -> Bool
326 |
327 | eqb TyInt l r = l == r
328 | eqb TyBool l r = l == r
329 | eqb (TyPair a b) (l1, l2) (r1, r2) = eqb a l1 r1 && eqb b l2 r2
330 | eqb (TyList a) l r = eqbs a l r
331 | eqb (TyFun a b) l r = False
332 |
333 | eqbs a [] [] = True
334 | eqbs a (l :: ls) (r :: rs) = eqb a l r && eqbs a ls rs
335 | eqbs a _ _ = False
336 |
337 | -- TODO: these are not actually tail recursive.
338 | -- APP is the biggest culprit
339 |
340 | public export
341 | steps : Meaning st -> Steps st st' -> Late (Meaning st')
342 | public export
343 | step : Meaning st -> Step st st' -> Late (Meaning st')
344 |
345 | steps st [] = Now st
346 | steps st (stp :: stps)
347 |   = do st' <- step st stp
348 |        steps st' stps
349 |
350 | step (MkMeaning s e f) (LDC c) = Now (MkMeaning (fromConst c :: s) e f)
351 | step (MkMeaning s e f) (LDA p) = Now (MkMeaning (indexAll p e :: s) e f)
352 | step (MkMeaning s e f) (LDF cd) = Now (MkMeaning (MkClosure cd e f :: s) e f)
353 | step (MkMeaning s e f) (LDR p) = Now (MkMeaning (lookup f p :: s) e f)
354 |
355 | step (MkMeaning (a :: fun :: s) e f) APP
356 |   -- TODO: Nisse-style transform for guardedness
357 |   = Later $ do let MkClosure cd e1 f1 = fun
358 |                MkMeaning [v] _ _ <- assert_total (steps (MkMeaning [] (a :: e1) (fun, f1)) cd)
359 |                Now (MkMeaning (v :: s) e f)
360 | step (MkMeaning (a :: fun :: s) e f) TAP
361 |   -- TODO: Actual tail calls
362 |   = Later $ do let MkClosure cd e1 f1 = fun
363 |                MkMeaning [v] _ _ <- assert_total (steps (MkMeaning [] (a :: e1) (fun, f1)) cd)
364 |                Now (MkMeaning (v :: s) e f)
365 | step (MkMeaning (v :: s) e f) RTN = Now (MkMeaning [v] e f)
366 |
367 | step (MkMeaning (b :: s) e f) (BCH l r)
368 |   = let st = MkMeaning s e f in
369 |     ifThenElse b
370 |       (Later (steps st l))
371 |       (Later (steps st r))
372 |
373 | step (MkMeaning (a :: b :: s) e f) FLP = Now (MkMeaning (b :: (a :: s)) e f)
374 |
375 | step (MkMeaning s e f) NIL = Now (MkMeaning ([] :: s) e f)
376 | step (MkMeaning (x :: xs :: s) e f) CNS = Now (MkMeaning ((x :: xs) :: s) e f)
377 | step (MkMeaning (xs :: s) e f) HED = case xs of
378 |   [] => never
379 |   (x :: _) => Now (MkMeaning (x :: s) e f)
380 | step (MkMeaning (xs :: s) e f) TAL = case xs of
381 |   [] => never
382 |   (_ :: xs) => Now (MkMeaning (xs :: s) e f)
383 |
384 | step (MkMeaning (a :: b :: s) e f) MKP = Now (MkMeaning ((a, b) :: s) e f)
385 | step (MkMeaning (ab :: s) e f) FST = Now (MkMeaning (fst ab :: s) e f)
386 | step (MkMeaning (ab :: s) e f) SND = Now (MkMeaning (snd ab :: s) e f)
387 |
388 | step (MkMeaning (m :: n :: s) e f) ADD = Now (MkMeaning (m + n :: s) e f)
389 | step (MkMeaning (m :: n :: s) e f) SUB = Now (MkMeaning (m - n :: s) e f)
390 | step (MkMeaning (m :: n :: s) e f) MUL = Now (MkMeaning (m * n :: s) e f)
391 |
392 | step (MkMeaning (x :: y :: s) e f) EQB = Now (MkMeaning (eqb _ x y :: s) e f)
393 | step (MkMeaning (b :: s) e f) NOT = Now (MkMeaning (not b :: s) e f)
394 |
395 | public export
396 | run : MkState [] [] [] `Steps` MkState (ty :: _) [] [] -> Nat -> Maybe (Meaning ty)
397 | run cd n
398 |   = do MkMeaning (v :: _) _ _ <- petrol n (steps (MkMeaning [] [] ()) cd)
399 |        pure v
400 |
401 | testFVE : run FVE 0 === Just 5
402 | testFVE = Refl
403 |
404 | testINC2 : run INC2 1 === Just 3
405 | testINC2 = Refl
406 |
407 | testTHR : run THR 2 === Just 3
408 | testTHR = Refl
409 |
410 | testLDL : run (LDL [1..4]) 0 === Just [1..4]
411 | testLDL = Refl
412 |
413 | testLST : run (SUM ++ LDL [1..4] ++ [APP]) 24 === Just 10
414 | testLST = Refl
415 |
416 | testMAP : run (MAP :: PLS :: LDC 1 :: APP :: APP :: LDL [1..3] ++ [APP]) 13
417 |           === Just [2..4]
418 | testMAP = Refl
419 |