lua-gc-redex-model/interpreter.rkt at master · Mallku2/lua-gc-redex-model · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
#lang racket
(require redex
         "./grammar.rkt"
         "./executionEnvironment.rkt"
         "Desugar/parser.rkt"
         "Relations/fullProgs.rkt"
         "Relations/gc.rkt"
         "Tests/LuaTests/tests_aux.rkt")

; PARAM : code, the actual Lua program to be executed, as a string value
; required for the execution of the program
;
; example:
; (execute "print(\"hello, world!\")")
;
; NOTE: if the code being executed makes use of the service "load", and the
; library services used in the code passed to load are not stated explicitly,
; it will be required to provide by hand every library service used by the
; snippet being executed; for example:
; (execute "(load(\"return ty\" .. \"pe(1)\"))()")
; ...
; ($err "attempt to call a nil value.")
;
; in this case we will need to reduce the previous term by invoking:
;
; (apply-reduction-relation* full-progs-rel
;        (plugIntoExecutionEnvironment services
;                                      '("load" "type")
;                                      (parse-this "(load(\"return ty\" .. \"pe(1)\"))()"
;                                                  #f (void))))

(define (execute code)
  (apply-reduction-relation* full-progs-rel
        (plugIntoExecutionEnvironment services
                                      (services-from code)
                                      (parse-this code #f (void)))))

(define (luatrace code)
  (begin
    (reduction-steps-cutoff 500)
    (traces full-progs-rel
        (plugIntoExecutionEnvironment services
                                      (services-from code)
                                      (parse-this code #f (void))))))

(define (luagctrace code selec_servs)
  (begin
    (reduction-steps-cutoff 500)
    (traces gc-rel
        (plugIntoExecutionEnvironment services
                                      selec_servs
                                      (parse-this code #f (void))))))

(provide execute
         luatrace
         luagctrace)