-
Notifications
You must be signed in to change notification settings - Fork 0
/
blame.rkt
104 lines (91 loc) · 3.48 KB
/
blame.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
#lang racket
(require redex)
(require "tglc-def.rkt" "types.rkt" "translate.rkt")
(provide extract label check-dups extend-β ϱ blame resolve collect-blame lookup-β L-to-T)
(default-language tglc)
(define-metafunction tglc
extract : r ... L -> L
[(extract L) L]
[(extract RES r_1 ... (→ q L_1 L_2)) (extract r_1 ... L_2)]
[(extract ARG r_1 ... (→ q L_1 L_2)) (extract r_1 ... L_1)]
[(extract DEREF r_1 ... (ref q L_1)) (extract r_1 ... L_1)]
[(extract r_1 r_2 ... *) *])
(define-metafunction tglc
label : L -> q
[(label *) ∈]
[(label (int q)) q]
[(label (→ q L_1 L_2)) q]
[(label (ref q L_1)) q]
[(label (⊥ l)) l])
(define-metafunction tglc
lookup-β : β a -> (b ...)
[(lookup-β ((a_1 b_1 ...) ... (a b ...) (a_2 b_2 ...) ... β) a) (b ...)]
[(lookup-β any_1 any_2) ,(error 'lookup-β "not found: ~e" (term any_2))])
(define-metafunction tglc
collect-blame : r ... β b -> (L ...)
[(collect-blame r_1 ... any_2 L)
(L_1)
(where L_1 (extract r_1 ... L)) (where l (label L_1))]
[(collect-blame r_1 ... any_2 L)
()
(where L_1 (extract r_1 ... L)) (where ∈ (label L_1))]
[(collect-blame r_1 ... any_2 (a r))
,(set-union
(first
(term ((collect-blame r r_1 ... any_2 b_1) ...))))
(where (b_1 ...) (lookup-β any_2 a))])
(define-metafunction tglc
check-dups : a ... -> #t or #f
[(check-dups a_!_1 ... a_!_1) #f]
[(check-dups a_1 ...) ,(error 'check-dups "found duplicate addr: ~e" (term a))])
(define-metafunction tglc
collect-blame-cl : a ... r ... β b -> (L ...)
[(collect-blame-cl a_1 ... r_1 ... any_2 L)
(L_1)
(where L_1 (extract r_1 ... L)) (where l (label L_1))]
[(collect-blame-cl a_1 ... r_1 ... any_2 L)
()
(where L_1 (extract r_1 ... L)) (where ∈ (label L_1))]
[(collect-blame-cl a_1 ... r_1 ... any_2 (a r))
,(set-union
(first
(term ((collect-blame-cl a a_1 ... r r_1 ... any_2 b_1) ...))))
(where (b_1 ...) (lookup-β any_2 a))
(where #f (check-dups a a_1 ...))])
(define-metafunction tglc
L-to-T : L -> T
[(L-to-T *) *]
[(L-to-T (int q)) int]
[(L-to-T (ref q L_1)) (ref T_1)
(where T_1 (L-to-T L_1))]
[(L-to-T (→ q L_1 L_2)) (→ T_1 T_2)
(where T_1 (L-to-T L_1)) (where T_2 (L-to-T L_2))])
(define-metafunction tglc
resolve : σ v L ... -> weird-L
[(resolve any_1 any_2 (⊥ l) L_1 ...)
(l (resolve any_1 any_2 L_1 ...))]
[(resolve any_1 any_2 L_1 L_2 ...)
((label L_1) (resolve any_1 any_2 L_2 ...))
(where #f (hastype any_1 any_2 (T-to-S (L-to-T L_1))))]
[(resolve any_1 any_2 L_1 L_2 ...)
((label L_1) (resolve any_1 any_2 L_2 ...))]
[(resolve any_1 any_2) ·])
;; updates address a in the blame map if present (have have multiple 'a' point to list of b's
;; QUESTION: this will just put all element in the list, instead of the union-set of the elements
(define-metafunction tglc
extend-β : β (a b_4) -> β
[(extend-β ((a_1 b_1 ...) ... (a b_2 ...) (a_3 b_3 ...) ... β) (a b_4))
((a_1 b_1 ...) ... (a b_2 ... b_4) (a_3 b_3 ...) ... β)]
[(extend-β ((a_1 b_1 ...) ... β) (a b_4)) ((a b_4) (a_1 b_1 ...) ... β)])
(define-metafunction tglc
ϱ : β a b -> β
[(ϱ β a_1 b) (extend-β β (a_1 b))])
(define-metafunction tglc
blame : σ v a r β -> ς
[(blame any_1 any_2 any_3 any_4 any_5) (BLAME weird-L)
(where (b_1 ...) (lookup-β any_5 any_3))
(where (L_1 ...)
,(set-union
(first
(term ((collect-blame-cl any_4 any_5 b_1) ...)))))
(where weird-L (resolve any_1 any_2 L_1 ...))])