forked from the-little-typer/pie
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathmain.rkt
354 lines (334 loc) · 15.9 KB
/
main.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
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
#lang racket/base
(require (for-syntax racket/base racket/match racket/string racket/format)
(for-syntax (for-syntax racket/base))
(for-syntax syntax/srcloc))
(require (for-syntax "parser.rkt"))
(require (for-syntax (except-in "basics.rkt" var-name? go-on)))
(require (for-syntax "rep.rkt" "typechecker.rkt" (only-in "normalize.rkt" read-back-ctx)))
(require "basics.rkt" "rep.rkt" "parser.rkt" (only-in "normalize.rkt" val-of-ctx))
(require (for-syntax syntax/parse)
(for-syntax (for-syntax syntax/parse)))
(require "serialization.rkt")
(require (for-syntax "serialization.rkt"))
(require "pie-err.rkt" (for-syntax "pie-err.rkt"))
(require "resugar.rkt" (for-syntax "resugar.rkt"))
(require "pretty.rkt" (for-syntax "pretty.rkt"))
(require (for-syntax "show-goal.rkt"))
(require racket/port (for-syntax racket/port))
(require (prefix-in kw: "pie-info.rkt")
(for-syntax (prefix-in kw: "pie-info.rkt")))
(require (rename-in typed/racket [#%module-begin mod]))
(provide (rename-out [pie-module-begin #%module-begin]
[pie-top-interaction #%top-interaction]
[pie-top #%top]
[pie-datum #%datum])
(for-syntax (rename-out [pie-top #%top]
[pie-datum #%datum]))
the-pie-ctx
list
match norm
(rename-out [kw:U U]
[kw:Nat Nat] [kw:zero zero] [kw:add1 add1] [kw:which-Nat which-Nat] [kw:iter-Nat iter-Nat] [kw:rec-Nat rec-Nat] [kw:ind-Nat ind-Nat]
[kw:-> ->] [kw:→ →] [kw:Π Π] [kw:λ λ] [kw:Pi Pi] [kw:lambda lambda]
[kw:quote quote] [kw:Atom Atom]
[kw:car car] [kw:cdr cdr] [kw:cons cons] [kw:Σ Σ] [kw:Sigma Sigma] [kw:Pair Pair]
[kw:Trivial Trivial] [kw:sole sole]
[kw:List List] [kw::: ::] [kw:nil nil] [kw:rec-List rec-List] [kw:ind-List ind-List]
[kw:Absurd Absurd] [kw:ind-Absurd ind-Absurd]
[kw:= =] [kw:same same] [kw:replace replace] [kw:trans trans] [kw:cong cong] [kw:symm symm]
[kw:Vec Vec] [kw:vecnil vecnil] [kw:vec:: vec::] [kw:head head] [kw:tail tail] [kw:ind-Vec ind-Vec]
[kw:Either Either] [kw:left left] [kw:right right] [kw:ind-Either ind-Either]
[kw:TODO TODO] [kw:the the]
[kw:claim claim] [kw:define define] [kw:check-same check-same])
(all-from-out "pie-info.rkt")
(for-syntax (all-from-out "pie-info.rkt")))
(begin-for-syntax
(define-syntax (go-on stx)
(syntax-parse stx
[(go-on () e) (syntax/loc stx e)]
[(go-on ((p0 b0) (p b) ...) e)
(syntax/loc stx
(match b0
[(go p0) (go-on ((p b) ...) e)]
[(stop where msg) (stop where msg)]))])))
(begin-for-syntax
(require "tooltip.rkt" (only-in "locations.rkt" location->syntax))
(define holes (box '()))
(define (a-or-an t)
(match t
[`(,c . ,_)
(case c
[(-> → Either = add1 iter-Nat ind-Nat ind-List ind-Absurd ind-Vec ind-Either)
"an"]
[else "a"])]
['Atom "an"]
[_ "a"]))
(define (hook loc what)
(when (and (not (eqv? loc #f)))
(define loc-stx (location->syntax loc))
(define start (sub1 (source-location-position loc-stx)))
(define end (sub1 (+ (source-location-position loc-stx)
(source-location-span loc-stx))))
(define loc-stx-str
(let ([src (syntax->datum loc-stx)])
(let ([test-str (format "~a" src)])
(if (> (string-length test-str) 40)
(match src
[(cons op args) (format "(~a ...)" op)]
[_ (string-append (substring test-str 0 37) "...")])
test-str))))
(match what
['definition
(void)]
[`(binding-site ,t)
(attach-tooltip #'a-stx loc-stx (format "Variable with type:\n~a"
(with-output-to-string
(lambda ()
(pprint-pie (resugar t))))))]
[`(is-type ,e)
(attach-tooltip #'a-stx loc-stx "A type")]
[`(has-type ,t)
(let ([sugary (resugar t)])
(attach-tooltip #'a-stx loc-stx (format "~a\nis ~a:\n~a"
loc-stx-str
(a-or-an sugary)
(with-output-to-string
(lambda ()
(pprint-pie sugary))))))]
[`(TODO ,Γ ,t)
(let ([sugary (resugar t)])
(attach-tooltip #'a-stx loc-stx (format "Will be ~a:\n~a"
(a-or-an sugary)
(with-output-to-string
(lambda ()
(pprint-pie sugary))))))
(set-box! holes (cons (list loc-stx Γ t) (unbox holes)))]
[_ (void)])
(void)))
(pie-info-hook hook))
(begin-for-syntax
(struct todo-item (full summary) #:prefab)
(struct command (name module-path function arguments) #:prefab))
(define-syntax (pie-module-begin stx)
(syntax-parse stx
[(_ form ...)
(define Γ
(with-handlers ([exn:fail:pie?
;; If there's an error, log all the tooltips we've
;; generated so far so the user gets some feedback.
(λ (e) (log-all-tooltips!) (raise e))])
(let loop ([forms (syntax->list #'(form ...))]
[Γ init-ctx])
(cond
[(null? forms)
Γ]
[else
(match (parse-pie-decl (car forms))
[`(claim ,f ,f-loc ,ty)
(match (add-claim Γ f f-loc ty)
[(go new-Γ)
(loop (cdr forms) new-Γ)]
[(stop where why)
(raise-pie-error where why)])]
[`(definition ,f ,f-loc ,e)
(match (add-def Γ f f-loc e)
[(go new-Γ)
(loop (cdr forms) new-Γ)]
[(stop where why)
(raise-pie-error where why)])]
[`(check-same ,loc ,ty ,e1 ,e2)
(match (check-same Γ loc ty e1 e2)
[(go _)
(loop (cdr forms) Γ)]
[(stop where why)
(raise-pie-error where why)])]
[`(expression ,e)
(match (norm Γ e)
[(go out)
(begin (pprint-pie (resugar out))
(printf "\n")
(loop (cdr forms) Γ))]
[(stop where why)
(raise-pie-error where why)])])]))))
(log-all-tooltips!)
(define ctx-string (dump (read-back-ctx Γ)))
(with-syntax ([ctx-string ctx-string]
[(hole ...)
(for/list ([info (reverse (unbox holes))])
(match-define (list loc Γ t)
info)
(match-define (list hole-summary hole-details)
(goal->strings loc Γ t))
(define hole-output-str
(string-append
(source-location->prefix loc)
;; Check whether there are free local variables
(if (ormap (lambda (H)
(match H
[(list _ (list 'free _)) #t]
[_ #f]))
Γ)
;; If there are free vars, print the
;; version with the horizontal line
(string-append "TODO:\n"
hole-details)
;; If no free vars, show only the goal type.
(string-append "TODO: "
(if (string-contains? hole-summary "\n")
(string-append "\n"
(indent-string 1 hole-summary))
hole-summary)))
"\n"))
(syntax-property
(syntax-property
(quasisyntax/loc loc (displayln #,hole-output-str))
'todo
(todo-item
hole-details
hole-summary))
'editing-command
(list (command "Auto" 'pie/interactive-editing 'auto (list t))
(command "More Auto" 'pie/interactive-editing 'more-auto (list t)))))])
(syntax/loc stx
(#%module-begin
(pie-decl->binders form) ...
(set-box! the-pie-ctx (val-of-ctx (restore ctx-string)))
(void (list hole ...)))))]))
(define-syntax (pie-top stx)
(syntax-parse stx
[(_ . x) #''x]))
(begin-for-syntax
(define-syntax pie-top
(syntax-rules ()
[(_ . x) 'x])))
(define-syntax (pie-datum stx)
(syntax-parse stx
[(_ . x) #''x]))
(begin-for-syntax
(define-syntax pie-datum
(syntax-rules ()
[(_ . x) 'x])))
(define the-pie-ctx (box init-ctx))
(define-syntax (pie-top-interaction stx)
(syntax-parse stx
[(_ . e)
(syntax/loc stx
(match (parse-pie-decl #'e)
[`(expression ,expr)
(define Γ (unbox the-pie-ctx))
(define n (norm Γ expr))
(match n
[(go out)
(pprint-pie (resugar out))]
[(stop where what)
(raise-pie-error where what)])]
[`(check-same ,loc ,ty ,e1 ,e2)
(match (check-same (unbox the-pie-ctx) loc ty e1 e2)
[(go _)
(void)]
[(stop where why)
(raise-pie-error where why)])]
[_ (raise-syntax-error #f "The Pie REPL does not support adding new definitions. Please load a file containing Pie code." #'e)]))]))
(module reader syntax/module-reader
pie
#:info (lambda (k v default-filter)
(case k
[(drracket:default-filters)
'(("Pie Sources" "*.pie"))]
[(drracket:default-extension)
"pie"]
[(drracket:opt-out-toolbar-buttons)
'(debug-tool)]
[(drracket:indentation)
(lambda (txt pos)
(and-let* ([line (send txt position-paragraph pos)]
[line-start (send txt paragraph-start-position line)]
[sexp-start (send txt find-up-sexp line-start)]
[buffer-end-pos (send txt last-position)]
[op-end (send txt get-forward-sexp (add1 sexp-start))]
[op-start (send txt get-backward-sexp op-end)]
[indent-basis
(- op-start
(send txt paragraph-start-position
(send txt position-paragraph op-start)))]
[default-indent (+ 1 indent-basis)]
[op (string->symbol (send txt get-text op-start op-end #t))])
(define in-Pi-or-Sigma?
(and-let* ([grandparent-sexp-start (send txt find-up-sexp sexp-start)]
[grand-op-end (send txt get-forward-sexp (add1 grandparent-sexp-start))]
[grand-op-start (send txt get-backward-sexp grand-op-end)]
[grand-op (send txt get-text grand-op-start grand-op-end)])
(if (member grand-op '("Pi" "Π" "Sigma" "Σ"))
#t
#f)))
(define real-op
(match op
['lambda 'λ]
['Pi 'Π]
['Sigma 'Σ]
['-> '→]
[other other]))
(match real-op
[(or 'which-Nat 'iter-Nat 'rec-Nat 'ind-Nat
'car 'cdr 'rec-List 'ind-List 'ind-Absurd
'replace 'cong 'trans 'symm 'head 'tail 'ind-Vec
'ind-Either)
(define target-count
(match real-op
[(or 'trans 'ind-Vec) 2]
[_ 1]))
;; find if last
(let ([targets-end
(let loop ([i target-count]
[pos (add1 sexp-start)])
(if (> i 0)
(loop (sub1 i)
(send txt get-forward-sexp pos))
pos))])
(and targets-end
(let ([first-line-sexp-end (send txt get-forward-sexp pos)])
(if (or (not first-line-sexp-end)
(>= first-line-sexp-end targets-end))
(+ 1 indent-basis)
(+ 4 indent-basis)))))]
[other
#:when (or (eqv? op '->) (eqv? op '→))
(and-let* ([sexp-end (send txt get-forward-sexp sexp-start)]
[last-arg-start (send txt get-backward-sexp (sub1 sexp-end))]
[first-arg-start (send txt get-backward-sexp
(send txt get-forward-sexp op-end))]
[last-arg-end (send txt get-forward-sexp last-arg-start)]
[first-line-sexp-end (send txt get-forward-sexp pos)]
[->-indent-basis
(- first-arg-start
(send txt paragraph-start-position
(send txt position-paragraph first-arg-start)))])
(if (>= first-line-sexp-end last-arg-end)
(+ 1 indent-basis)
(+ ->-indent-basis)))]
[_
#:when in-Pi-or-Sigma?
;; Use normal Racket sexp indenting
#f]
[_ default-indent])))]
[(color-lexer)
(lambda (in)
(define-values (tok pie-style paren start end) (pie-lexer in))
(values tok
(case pie-style
[(type-ctor data-ctor) 'constant]
[else pie-style])
paren
start
end))]
[else (default-filter k v)]))
(require "gui/pie-lexer.rkt")
(require racket/class racket/match)
(require (for-syntax racket/base syntax/parse))
(define-syntax (and-let* stx)
(syntax-parse stx
[(_ () e ...) #'(let () e ...)]
[(_ ((x:id e1) (y:id e2) ...) e ...)
#'(let ((x e1))
(and x (and-let* ((y e2) ...) e ...)))]))
)