-
Notifications
You must be signed in to change notification settings - Fork 0
/
attribute.rkt
118 lines (98 loc) · 3.47 KB
/
attribute.rkt
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
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
#lang racket
(require redex)
; Syntax
(define-language AttributeL
(update (attr ...))
(attr (← x expr))
(expr number
(+ expr expr)
(* expr expr)
(/ expr expr)
(- expr expr)
x)
(x variable-not-otherwise-mentioned)
(value number
undef)
(ctx ((x value)...)))
(define-extended-language ctx-AttributeL AttributeL
(VS (expr ctx))
(ctx ((x value)...))
(H (+ H expr)
(+ value H)
(* H expr)
(* value H)
(- H expr)
(- value H)
(/ H expr)
(/ value H)
hole)
(value number
undef))
(define-judgment-form ctx-AttributeL
#:mode (eval I I O)
#:contract (eval ctx expr value)
[--------------------------------
(eval ctx number number)]
[
--------------------------------
(eval ctx x (look x ctx))]
[(eval ctx expr_1 number_1)
(eval ctx expr_2 number_2)
------------------------------------
(eval ctx (+ expr_1 expr_2) ,(+ (term number_1) (term number_2)))]
[(eval ctx expr_1 number_1)
(eval ctx expr_2 number_2)
------------------------------------
(eval ctx (* expr_1 expr_2) ,(* (term number_1) (term number_2)))]
[(eval ctx expr_1 number_1)
(eval ctx expr_2 number_2)
------------------------------------
(eval ctx (- expr_1 expr_2) ,(- (term number_1) (term number_2)))]
[(eval ctx expr_1 number_1)
(eval ctx expr_2 number_2)
------------------------------------
(eval ctx (/ expr_1 expr_2) ,(/ (term number_1) (term number_2)))]
)
(define-metafunction ctx-AttributeL
look : x ((x value) ...) -> value
[(look x ()) undef]
[(look x ((x value) (x_1 value_1)...) ) value]
[(look x ((x_1 value) (x_2 value_1)...) ) (look x ((x_2 value_1) ...)) ]
)
(define expr-red
(reduction-relation
ctx-AttributeL
#:domain VS
(--> ((in-hole H (+ number_1 number_2) ) ctx)
((in-hole H ,(+ (term number_1) (term number_2)) ) ctx)
"add1")
(--> ((in-hole H x) ( (x_1 value_1)... (x value) (x_2 value_2)... ) )
((in-hole H value ) ( (x_1 value_1)... (x value) (x_2 value_2)... ) )
"var")
(--> ((in-hole H (* number_1 number_2) ) ctx)
((in-hole H ,(* (term number_1) (term number_2)) ) ctx)
"mult1")
(--> ((in-hole H (- number_1 number_2) ) ctx)
((in-hole H ,(- (term number_1) (term number_2)) ) ctx)
"sub1")
(--> ((in-hole H (/ number_1 number_2) ) ctx)
((in-hole H ,(/ (term number_1) (term number_2)) ) ctx)
"div1")
))
;(traces expr-red (term ((* 1 2) () ) ) )
;(judgment-holds (eval ((x 4)) (+ (* x 7) (* 1 3)) value) value)
;(judgment-holds (eval ((x 3)) (+ (* x 7) (/ x 3)) value) value)
;(judgment-holds (eval ((x 4) (y 2)) (+ (* x 7) (* y 3)) value) value)
;(judgment-holds (eval ((x 4) (y 2)) (+ (* x 7) (* t 3)) value) value)
#;(traces expr-red (term ( Z ((X 10) (Y 20)))) )
#;(traces expr-red (term ((+ 1 2) () ) ) )
#;(traces expr-red (term ((+ 2 (+ 1 2)) ()) ))
#;(traces expr-red (term ((+ (+ 1 1) 2) ())) )
#;(traces expr-red (term ((+ (+ X 1) 2) ((X 10)))) )
#;(traces expr-red (term ((+ (+ 2 4) (+ 1 2)) ()) ))
(traces expr-red (term ((+ (+ 2 4) (+ 1 2)) ()) ) )
; The so-precious in-hole examaples !
;
#;(redex-match ctx-AttributeL (in-hole H (+ number_1 number_2)) (term (+ 5 (+ 1 (+ 2 3))) ) )
#;(redex-match ctx-AttributeL (in-hole H expr) (term ( + (+ 1 (+ 2 3)) 5) ) )
(redex-match ctx-AttributeL (in-hole H expr) (term ( + (+ 2 4) (+ 1 2)) ) )