forked from lives-group/redexPEG
-
Notifications
You must be signed in to change notification settings - Fork 0
/
LC
157 lines (131 loc) · 4.54 KB
/
LC
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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
#lang racket
(require redex)
(define-language L
(e (e e)
(λ (x t) e)
x
(amb t e ...)
number
(+ e ...)
(if0 e e e)
(fix e))
(t (→ t t) num )
(x variable-not-otherwise-mentioned))
(define-extended-language L+Γ L
[Γ · (x : t Γ)])
(define-judgment-form
L+Γ
#:mode (types I I O)
#:contract (types Γ e t)
[(types Γ e_1 (→ t_2 t_3))
(types Γ e_2 t_2)
-------------------------
(types Γ (e_1 e_2) t_3)]
[(types (x : t_1 Γ) e t_2)
-----------------------------------
(types Γ (λ (x t_1) e) (→ t_1 t_2))]
[(types Γ e (→ (→ t_1 t_2) (→ t_1 t_2)))
---------------------------------------
(types Γ (fix e) (→ t_1 t_2))]
[---------------------
(types (x : t Γ) x t)]
[(types Γ x_1 t_1)
(side-condition (different x_1 x_2))
------------------------------------
(types (x_2 : t_2 Γ) x_1 t_1)]
[(types Γ e num) ...
-----------------------
(types Γ (+ e ...) num)]
[--------------------
(types Γ number num)]
[(types Γ e_1 num)
(types Γ e_2 t)
(types Γ e_3 t)
-----------------------------
(types Γ (if0 e_1 e_2 e_3) t)]
[
-----------------------
(types Γ (amb t ) (mt t) )]
[ (types Γ e t_1) ...
(side-condition (allEquals t t_1 ... ))
-----------------------
(types Γ (amb t e ...) t)])
(define-metafunction L+Γ
allEquals : t ... -> boolean
[(allEquals) #t]
[(allEquals t) #t]
[(allEquals t t t_1 ...) (allEquals t t_1 ...)]
[(allEquals t _ ...) #f])
(define-metafunction L+Γ
extend : Γ (x t) ... -> Γ
[(extend ((x_Γ t_Γ) ...) (x t) ...)
((x t) ... (x_Γ t_Γ) ...)])
(define-metafunction L+Γ
[(different x_1 x_1) #f]
[(different x_1 x_2) #t])
(test-equal (judgment-holds (types · 1 t) t) (list (term num )))
(test-equal (judgment-holds (types · (+ 10 20) t) t) (list (term num )))
(test-equal (judgment-holds (types · (if0 0 10 20) t) t) (list (term num )))
(test-equal (judgment-holds (types · (λ (x num) x) t) t) (list (term (→ num num) )))
(test-equal (judgment-holds (types · ((λ (x num) x) 0) t) t) (list (term num )) )
(test-equal (judgment-holds (types · ((λ (x num) (λ (y num) (+ x y))) 0) t) t) (list (term (→ num num) )))
(test-equal (judgment-holds (types · (λ (x num) (λ (x num) (+ x x))) t) t) (list (term (→ num (→ num num)) )))
(test-equal (judgment-holds (types · (amb num 0 1) t) t) (list (term num)))
(test-equal (judgment-holds (types · (amb (→ num num) (λ (x num) x) (λ (x num) x)) t) t) (list (term (→ num num))))
; falhas
(test-equal (judgment-holds (types · (λ (y num) x) t) t) null) ; variável não definida
(test-equal (judgment-holds (types · ((λ (x num) x) (λ (x num) x)) t) t) null) ; aplicação incompatível
(test-equal (judgment-holds (types · (if0 0 (λ (x num) x) 20) t) t) null) ; if divergente !
(test-equal (judgment-holds (types · (amb num 0 (λ (x num) x)) t) t) null) ; Amb divergente !
(test-results)
(judgment-holds (types · (amb (→ num num) (λ (x num) x) (λ (x num) x)) t) t)
(judgment-holds (types · (λ (x num) (λ (x (→ num num)) x) ) t) t)
(collection-file-path "tut-subst.rkt" "redex")
(define-extended-language Ev L+Γ
(p (e ...))
(P (e ... E e ...))
(E (v E)
(E e)
(+ v ... E e ...)
(if0 E e e)
(fix E)
hole)
(v (λ (x t) e)
(fix v)
number))
(define red
(reduction-relation
Ev
#:domain p
(--> (in-hole P (if0 0 e_1 e_2))
(in-hole P e_1)
"if0t")
(--> (in-hole P (if0 v e_1 e_2))
(in-hole P e_2)
(side-condition (not (equal? 0 (term v))))
"if0f")
(--> (in-hole P ((fix (λ (x t) e)) v))
(in-hole P (((λ (x t) e) (fix (λ (x t) e))) v))
"fix")
(--> (in-hole P ((λ (x t) e) v))
(in-hole P (subst x v e))
"βv")
(--> (in-hole P (+ number ...))
(in-hole P (∑ number ...))
"+")
(--> (e_1 ... (in-hole E (amb e_2 ...)) e_3 ...)
(e_1 ... (in-hole E e_2) ... e_3 ...)
"amb")))
(require redex/tut-subst)
(define-metafunction Ev
subst : x v e -> e
[(subst x v e)
,(subst/proc x? (list (term x)) (list (term v)) (term e))])
(define x? (redex-match Ev x))
(define-metafunction Ev
∑ : number ... -> number
[(∑ number ...)
,(apply + (term (number ...)))])
;(traces red (term ( (λ (y num) (+ y 5)) ((λ (x num) x) (+ 1 2)) ) ))
;(traces red (term (( (λ (y num) (+ y 5)) ((λ (x num) x) (+ 1 2)) ) )) )
(traces red (term ( (fix (λ (x num) (amb (+ x -1) x) ) ) 2 ) ) )