-
Notifications
You must be signed in to change notification settings - Fork 0
/
Syntax.rkt
199 lines (169 loc) · 5.48 KB
/
Syntax.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
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
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
#lang racket
(require redex
rackunit
(prefix-in racket: racket))
(provide (all-defined-out))
;; ITT core language
(define-language ITT-core
(e tm ty prop ::= (V n)
(bind b e)
(e e)
★
unit
tt
void
(exfalso ty tm)
bool
true
false
(if e e e e)
(sigma ty e)
(pair ty e e e)
(π1 e)
(π2 e)
;; OTT stuff
(embed prop)
⊤
⊥
(= ty ty)
(≡ tm ty tm ty)
(coe tm ty tm ty)
(coh tm ty tm ty)
(∧ prop prop)
;; Bidi stuff
(: e e))
(neutral ::= (V n)
(exfalso neutral val)
(if (bind b e) neutral val val)
(neutral tm)
(π1 neutral)
(π2 neutral)
(= neutral neutral)
(embed neutral)
(∧ neutral neutral)
(coe neutral neutral neutral neutral)
(coh neutral neutral neutral neutral))
(val ::= unit void bool
(bind b e)
tt
true false
(pair val val val val)
⊤ ⊥
)
(b ::= (lam ty)
(Pi ty)
(forall e))
(n ::= natural))
;; ITT source language, which desugars to ITT-core
(define-extended-language ITT ITT-core
(e ::= ....
x
(λ (x ty) tm)
(Π (x ty) tm)
(Σ (x ty) tm)
(∀ (x ty) prop))
(x ::= variable-not-otherwise-mentioned))
;; helpers for sets of variables
(define-metafunction ITT
in : x (x ...) -> boolean
[(in x (x_1 ... x x_2 ...)) #t]
[(in x _) #f])
(define-metafunction ITT
∪ : (x ...) ... -> (x ...)
[(∪ (x_1 ...) (x_2 ...) (x_3 ...) ...)
(∪ (x_1 ... x_2 ...) (x_3 ...) ...)]
[(∪ (x_1 ...))
(x_1 ...)]
[(∪) ()])
(define-metafunction ITT
- : (x ...) (x ...) -> (x ...)
[(- (x ...) ()) (x ...)]
[(- (x_1 ... x_2 x_3 ...) (x_2 x_4 ...))
(- (x_1 ... x_3 ...) (x_2 x_4 ...))
(side-condition (not (memq (term x_2) (term (x_3 ...)))))]
[(- (x_1 ...) (x_2 x_3 ...))
(- (x_1 ...) (x_3 ...))])
;; lowering ITT to ITT-core
(define-metafunction ITT
lower/ctx : (x ...) e -> e
[(lower/ctx (x_c1 ... x x_c2 ...) x)
(V n)
(where n ,(length (term (x_c1 ...))))
(where #f (in x (x_c1 ...)))]
[(lower/ctx (x_c ...) (λ (x ty) e_b))
(bind (lam (lower/ctx (x_c ...) ty))
(lower/ctx (x x_c ...) e_b))]
[(lower/ctx (x_c ...) (Π (x e_t1) e_t2))
(bind (Pi (lower/ctx (x_c ...) e_t1))
(lower/ctx (x x_c ...) e_t2))]
[(lower/ctx (x_c ...) (Σ (x e_t1) e_t2))
(sigma e_t1 (lower/ctx (x_c ...) (λ (x e_t1) e_t2)))]
[(lower/ctx (x_c ...) (∀ (x e_t1) prop))
(bind (forall e_t1) (lower/ctx (x x_c ...) prop))]
[(lower/ctx (x ...) (V n)) (V n)]
[(lower/ctx (x ...) (bind b e))
(bind (lower/ctx-bind (x ...) b)
(lower/ctx (x ...) e))]
[(lower/ctx (x ...) (e_1 e_2))
((lower/ctx (x ...) e_1) (lower/ctx (x ...) e_2 ))]
[(lower/ctx (x ...) (any e ...))
(any (lower/ctx (x ...) e) ...)]
[(lower/ctx (x ...) any) any])
(define-metafunction ITT
lower/ctx-bind : (x ...) b -> b
[(lower/ctx-bind (x ...) (lam e))
(lam (lower/ctx (x ...) e))]
[(lower/ctx-bind (x ...) (Pi e))
(Pi (lower/ctx (x ...) e))]
[(lower/ctx-bind (x ...) (Sig e))
(forall (lower/ctx (x ...) e))])
(define-metafunction ITT
lower : e -> e
[(lower e) (lower/ctx () e)])
;; ITT source sugar helpers
(define-metafunction ITT
=> : e e -> e
[(=> ty_1 ty_2)
(Π (,(variable-not-in (term ty_2) 'arr_x) ty_1) ty_2)])
;; ITT source terms
(define (id-e e_t) (term (λ (x ,e_t) x)))
(define (id-t e_t) (term (=> ,e_t ,e_t)))
;; OTT source terms
(define lam-void-coerce
(term (bind (lam void)
(coe (V 0) void tt void))))
(module+ test
;; test '=>' sugar
(test-equal (term (lower (=> unit unit))) (term (bind (Pi unit) unit)))
;; test lower
(test-equal (term (lower (λ (x unit) x)))
(term (bind (lam unit) (V 0))))
(test-equal (term (lower (λ (x unit) (λ (x unit) x))))
(term (bind (lam unit) (bind (lam unit) (V 0)))))
(test-equal (term (lower (pair (Π (x unit) unit) unit
(λ (x unit) x) tt)))
(term (pair (bind (Pi unit) unit) unit
(bind (lam unit) (V 0)) tt)))
#;
(redex-check ITT e (equal? (lower e) (lower (lower e)))
#:prepare (close-all-fv (redex-match? ITT e))))
;;---------------------------------------------------------------------
(define dapp (term
(λ (a ★)
(λ (P (=> a ★))
(λ (f (Π (x a) (P x)))
(λ (y a)
(f y)))))))
(module+ test
(test-equal (term (α= ,dapp
(λ (b ★)
(λ (Q (=> b ★))
(λ (g (Π (x b) (Q x)))
(λ (y b)
(g y)))))))
#t))
(define-metafunction ITT
α= : e e -> boolean
[(α= e_1 e_2) ,(equal? (term (lower e_1)) (term (lower e_2)))])
(module+ test
(test-results))