From 59c1b3945f119a3c9d8ca3440765b8eb03aae419 Mon Sep 17 00:00:00 2001 From: David Christiansen Date: Tue, 4 May 2021 06:56:08 +0200 Subject: [PATCH] When constructing hidden internal variables, don't capture Fixes #42. --- basics.rkt | 103 ++++++++++++++++++++++++++++++++++++++++++++++++ typechecker.rkt | 66 +++++++++++++++---------------- 2 files changed, 136 insertions(+), 33 deletions(-) diff --git a/basics.rkt b/basics.rkt index 1efb3d8..3841b27 100644 --- a/basics.rkt +++ b/basics.rkt @@ -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))) @@ -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: diff --git a/typechecker.rkt b/typechecker.rkt index 98dd935..1e3d78f 100644 --- a/typechecker.rkt +++ b/typechecker.rkt @@ -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 @@ -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 @@ -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 @@ -207,7 +207,7 @@ `(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 @@ -215,7 +215,7 @@ '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 @@ -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) @@ -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) @@ -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" @@ -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)