Skip to content

Commit

Permalink
When constructing hidden internal variables, don't capture
Browse files Browse the repository at this point in the history 
Fixes #42.
  • Loading branch information
@david-christiansen
david-christiansen committed May 4, 2021
1 parent a698d4c commit 59c1b39
Show file tree
Hide file tree
Showing 2 changed files with 136 additions and 33 deletions.
103 changes: 103 additions & 0 deletions basics.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -542,6 +542,15 @@
(define (fresh Γ x)
(freshen (names-only Γ) x))

;; Find a fresh name, using none of those described in a context nor
;; occurring in an expression. This is used when constructing a fresh
;; binding to avoid capturing a free variable that would otherwise be
;; an error because it points at the context.
(: fresh-binder (-> Ctx Src Symbol Symbol))
(define (fresh-binder Γ expr x)
(freshen (append (names-only Γ) (occurring-names expr)) x))


;; Find the names that are described in a context, so they can be
;; avoided.
(: names-only (-> Ctx (Listof Symbol)))
Expand All @@ -550,6 +559,100 @@
[(null? Γ) '()]
[else (cons (car (car Γ)) (names-only (cdr Γ)))]))

;; Find all the names that occur in an expression. For correctness, we
;; need only find the free identifiers, but finding the bound
;; identifiers as well means that the bindings introduced by
;; desugaring expressions are more different from the program as
;; written, which can help readability of internals.
(: occurring-names (-> Src (Listof Symbol)))
(define (occurring-names expr)
(match (src-stx expr)
[`(the ,t ,e)
(append (occurring-names t) (occurring-names e))]
[`(quote ,x)
'()]
[`(add1 ,n)
(occurring-names n)]
[`(which-Nat ,tgt ,base ,step)
(append (occurring-names tgt) (occurring-names base) (occurring-names step))]
[`(iter-Nat ,tgt ,base ,step)
(append (occurring-names tgt) (occurring-names base) (occurring-names step))]
[`(rec-Nat ,tgt ,base ,step)
(append (occurring-names tgt) (occurring-names base) (occurring-names step))]
[`(ind-Nat ,tgt ,mot ,base ,step)
(append (occurring-names tgt) (occurring-names mot) (occurring-names base) (occurring-names step))]
[(cons '-> (cons t0 ts))
(append (occurring-names t0) (apply append (map occurring-names ts)))]
[`(Π ,bindings ,t)
(append (apply append (map occurring-binder-names bindings)) (occurring-names t))]
[`(λ ,bindings ,t)
(append (map binder-var bindings) (occurring-names t))]
[`(Σ ,bindings ,t)
(append (apply append (map occurring-binder-names bindings)) (occurring-names t))]
[`(Pair ,A ,D)
(append (occurring-names A) (occurring-names D))]
[`(cons ,A ,D)
(append (occurring-names A) (occurring-names D))]
[`(car ,p)
(occurring-names p)]
[`(cdr ,p)
(occurring-names p)]
[`(:: ,A ,D)
(append (occurring-names A) (occurring-names D))]
[`(List ,E)
(occurring-names E)]
[`(rec-List ,tgt ,base ,step)
(append (occurring-names tgt) (occurring-names base) (occurring-names step))]
[`(ind-List ,tgt ,mot ,base ,step)
(append (occurring-names tgt) (occurring-names mot) (occurring-names base) (occurring-names step))]
[`(ind-Absurd ,tgt ,mot)
(append (occurring-names tgt) (occurring-names mot))]
[`(= ,A ,from ,to)
(append (occurring-names A) (occurring-names from) (occurring-names to))]
[`(same ,e)
(occurring-names e)]
[`(replace ,tgt ,mot ,base)
(append (occurring-names tgt) (occurring-names mot) (occurring-names base))]
[`(trans ,tgt1 ,tgt2)
(append (occurring-names tgt1) (occurring-names tgt2))]
[`(cong ,tgt ,f)
(append (occurring-names tgt) (occurring-names f))]
[`(symm ,tgt)
(occurring-names tgt)]
[`(ind-= ,tgt ,mot ,base)
(append (occurring-names tgt) (occurring-names mot) (occurring-names base))]
[`(Vec ,E ,len)
(append (occurring-names E) (occurring-names len))]
[`(vec:: ,hd ,tl)
(append (occurring-names hd) (occurring-names tl))]
[`(head ,tgt)
(occurring-names tgt)]
[`(tail ,tgt)
(occurring-names tgt)]
[`(ind-Vec ,len ,tgt ,mot ,base ,step)
(append (occurring-names len) (occurring-names tgt)
(occurring-names mot)
(occurring-names base) (occurring-names step))]
[`(Either ,A ,B)
(append (occurring-names A) (occurring-names B))]
[`(left ,e)
(occurring-names e)]
[`(right ,e)
(occurring-names e)]
[`(ind-Either ,tgt ,mot ,l ,r)
(append (occurring-names tgt) (occurring-names mot) (occurring-names l) (occurring-names r))]
[(cons (? src? f) (cons arg0 args))
(append (occurring-names f) (occurring-names arg0) (apply append (map occurring-names args)))]
[x
(if (and (symbol? x) (var-name? x))
(list x)
'())]))

(: occurring-binder-names (-> Typed-Binder (Listof Symbol)))
(define (occurring-binder-names b)
(match b
[(list (binder where x) t)
(cons x (occurring-names t))]))


;; Local Variables:
Expand Down
66 changes: 33 additions & 33 deletions typechecker.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,7 @@
['U (go 'U)]
['Nat (go 'Nat)]
[`(-> ,A ,B)
(let ([x (fresh Γ 'x)])
(let ([x (fresh-binder Γ B 'x)])
(go-on ([A-out (is-type Γ r A)]
[B-out (is-type (bind-free Γ
x
Expand All @@ -105,7 +105,7 @@
B)])
(go `(Π ((,x ,A-out)) ,B-out))))]
[`(-> ,A ,B ,C . ,C*)
(let ([x (fresh Γ 'x)])
(let ([x (fresh-binder Γ (make-app B C C*) 'x)])
(go-on ([A-out (is-type Γ r A)]
[t-out (is-type (bind-free Γ x (val-in-ctx Γ A-out))
r
Expand All @@ -132,7 +132,7 @@
['Atom
(go 'Atom)]
[`(Pair ,A ,D)
(let ([x (fresh Γ 'x)])
(let ([x (fresh-binder Γ D 'x)])
(go-on ([A-out (is-type Γ r A)]
[D-out (is-type (bind-free Γ x (val-in-ctx Γ A-out))
r
Expand Down Expand Up @@ -207,15 +207,15 @@
`(U
"is a type, but it does not have a type."))]
[`(-> ,A ,B)
(let ([z (fresh Γ 'x)])
(let ([z (fresh-binder Γ B 'x)])
(go-on ([A-out (check Γ r A 'UNIVERSE)]
[B-out (check (bind-free Γ z (val-in-ctx Γ A-out))
r
B
'UNIVERSE)])
(go `(the U (Π ((,z ,A-out)) ,B-out)))))]
[`(-> ,A ,B ,C . ,C*)
(let ([z (fresh Γ 'x)])
(let ([z (fresh-binder Γ (make-app B C C*) 'x)])
(go-on ([A-out (check Γ r A 'UNIVERSE)]
[t-out (check (bind-free Γ z (val-in-ctx Γ A-out))
r
Expand Down Expand Up @@ -390,17 +390,14 @@
[(LIST E)
(go-on ((`(the ,b-t-out ,b-out) (synth Γ r b))
(b-t-val (go (val-in-ctx Γ b-t-out)))
(s-out (let ([x (fresh Γ 'x)]
[xs (fresh Γ 'xs)]
[ih (fresh Γ 'ih)])
(check
Γ
r
s
(Π-type ((e E)
(es (LIST E))
(ih b-t-val))
b-t-val)))))
(s-out (check
Γ
r
s
(Π-type ((e E)
(es (LIST E))
(ih b-t-val))
b-t-val))))
(go `(the ,b-t-out
(rec-List ,tgt-out
(the ,b-t-out ,b-out)
Expand Down Expand Up @@ -431,16 +428,15 @@
(go-on ((`(the ,tgt-t-out ,tgt-out) (synth Γ r tgt)))
(match (val-in-ctx Γ tgt-t-out)
[(EQUAL Av fromv tov)
(let ((x (fresh Γ 'x)))
(go-on ((mot-out (check Γ
r
mot
(Π-type ((x Av)) 'UNIVERSE)))
(b-out (check Γ r b (do-ap (val-in-ctx Γ mot-out)
fromv))))
(go `(the ,(read-back-type Γ (do-ap (val-in-ctx Γ mot-out)
tov))
(replace ,tgt-out ,mot-out ,b-out)))))]
(go-on ((mot-out (check Γ
r
mot
(Π-type ((x Av)) 'UNIVERSE)))
(b-out (check Γ r b (do-ap (val-in-ctx Γ mot-out)
fromv))))
(go `(the ,(read-back-type Γ (do-ap (val-in-ctx Γ mot-out)
tov))
(replace ,tgt-out ,mot-out ,b-out))))]
[non-equal
(stop
(src-loc e)
Expand Down Expand Up @@ -582,13 +578,12 @@
(go-on ((`(the ,tgt-t ,tgt-out) (synth Γ r tgt)))
(match (val-in-ctx Γ tgt-t)
[(EITHER Lv Rv)
(let ([x^ (fresh Γ 'x)])
(go-on ((mot-out (check Γ r mot (Π-type ((x (EITHER Lv Rv))) 'UNIVERSE)))
(mot-val (go (val-in-ctx Γ mot-out)))
(l-out (check Γ r on-left (Π-type ((x Lv)) (do-ap mot-val (LEFT x)))))
(r-out (check Γ r on-right (Π-type ((x Rv)) (do-ap mot-val (RIGHT x))))))
(go `(the (,mot-out ,tgt-out)
(ind-Either ,tgt-out ,mot-out ,l-out ,r-out)))))]
(go-on ((mot-out (check Γ r mot (Π-type ((x (EITHER Lv Rv))) 'UNIVERSE)))
(mot-val (go (val-in-ctx Γ mot-out)))
(l-out (check Γ r on-left (Π-type ((x Lv)) (do-ap mot-val (LEFT x)))))
(r-out (check Γ r on-right (Π-type ((x Rv)) (do-ap mot-val (RIGHT x))))))
(go `(the (,mot-out ,tgt-out)
(ind-Either ,tgt-out ,mot-out ,l-out ,r-out))))]
[non-Either
(stop (src-loc e)
`("Expected an Either, but got a"
Expand Down Expand Up @@ -871,6 +866,11 @@
(all-ok-atom (cdr cs))]
[else #f]))

;; Helper to concoct a function application form in source syntax
(: make-app (-> Src Src (Listof Src) Src))
(define (make-app a b cs)
(@ (src-loc a) (list* a b cs)))

(module+ test
(require typed/rackunit)

Expand Down

0 comments on commit 59c1b39

Please sign in to comment.