From 9723870f1494c142c111bd906d2566e3fb3c5563 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Fri, 10 Apr 2015 22:05:54 -0400 Subject: [PATCH 1/2] =?UTF-8?q?Added=20capture-avoiding=20subst,=20=CE=B1-?= =?UTF-8?q?equivalence?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Added capture-avoiding substitution * Added equivalence during typing checking, including α-equivalence and limited β-equivalence * Exposed better typing-check reflection features to allow typing checking modulo equivalence * Tweaked QED macro to use new type-checking reflection feature. * Fixed some test cases --- redex-curnel.rkt | 322 +++++++++++++++++++++++++++-------------------- stdlib/nat.rkt | 6 +- stdlib/prop.rkt | 4 +- stdlib/sugar.rkt | 12 +- 4 files changed, 201 insertions(+), 143 deletions(-) diff --git a/redex-curnel.rkt b/redex-curnel.rkt index 0555070..ee9c740 100644 --- a/redex-curnel.rkt +++ b/redex-curnel.rkt @@ -36,6 +36,7 @@ (require rackunit) (define-term Type (Unv 0)) (check-true (x? (term T))) + (check-true (x? (term A))) (check-true (x? (term truth))) (check-true (x? (term zero))) (check-true (x? (term s))) @@ -43,6 +44,8 @@ (check-true (t? (term s))) (check-true (x? (term nat))) (check-true (t? (term nat))) + (check-true (t? (term A))) + (check-true (t? (term S))) (check-true (U? (term (Unv 0)))) (check-true (U? (term Type))) (check-true (e? (term (λ (x_0 : (Unv 0)) x_0)))) @@ -81,12 +84,15 @@ (unv-kind (Unv i_1) (Unv i_2) (Unv i_3))]) ;; NB: Substitution is hard + ;; NB: Copy and pasted from Redex examples (define-metafunction cicL subst-vars : (x any) ... any -> any [(subst-vars (x_1 any_1) x_1) any_1] - [(subst-vars (x_1 any_1) (any_2 ...)) ((subst-vars (x_1 any_1) any_2) ...)] + [(subst-vars (x_1 any_1) (any_2 ...)) + ((subst-vars (x_1 any_1) any_2) ...)] [(subst-vars (x_1 any_1) any_2) any_2] - [(subst-vars (x_1 any_1) (x_2 any_2) ... any_3) (subst-vars (x_1 any_1) (subst-vars (x_2 any_2) ... any_3))] + [(subst-vars (x_1 any_1) (x_2 any_2) ... any_3) + (subst-vars (x_1 any_1) (subst-vars (x_2 any_2) ... any_3))] [(subst-vars any) any]) (define-metafunction cicL @@ -94,20 +100,21 @@ [(subst U x t) U] [(subst x x t) t] [(subst x_0 x t) x_0] - [(subst (Π (x : t_0) t_1) x t) (Π (x : (subst t_0 x t)) t_1)] - [(subst (λ (x : t_0) t_1) x t) (λ (x : (subst t_0 x t)) t_1)] - [(subst (μ (x : t_0) t_1) x t) (μ (x : (subst t_0 x t)) t_1)] - ;; TODO: Broken: needs capture avoiding, but currently require - ;; binders to be the same in term/type, so this is not a local - ;; change. - [(subst (Π (x_0 : t_0) t_1) x t) (Π (x_0 : (subst t_0 x t)) (subst t_1 x t)) ] - [(subst (λ (x_0 : t_0) t_1) x t) (λ (x_0 : (subst t_0 x t)) (subst t_1 x t))] - [(subst (μ (x_0 : t_0) t_1) x t) (μ (x_0 : (subst t_0 x t)) (subst t_1 x t))] + [(subst (any (x : t_0) t_1) x t) + (any (x : (subst t_0 x t)) t_1)] + [(subst (any (x_0 : t_0) t_1) x t) + (any (x_new : (subst (subst-vars (x_0 x_new) t_0) x t)) + (subst (subst-vars (x_0 x_new) t_1) x t)) + (where x_new + ,(variable-not-in + (term (x_0 t_0 x t t_1)) + (term x_0)))] [(subst (e_0 e_1) x t) ((subst e_0 x t) (subst e_1 x t))] [(subst (case e (x_0 e_0) ...) x t) (case (subst e x t) (x_0 (subst e_0 x t)) ...)]) (module+ test + (check-true (t? (term (Π (a : A) (Π (b : B) ((and A) B)))))) (check-equal? (term (Π (a : S) (Π (b : B) ((and S) B)))) (term (subst (Π (a : A) (Π (b : B) ((and A) B))) A S)))) @@ -142,12 +149,12 @@ ;; TODO: Congruence-closure instead of β (define ==β (reduction-relation cic-redL - (==> ((Π (x : t_0) t_1) t_2) - (subst t_1 x t_2)) - (==> ((λ (x : t) e_0) e_1) - (subst e_0 x e_1)) (==> ((μ (x : t) e_0) e_1) ((subst e_0 x (μ (x : t) e_0)) e_1)) + (==> ((λ (x : t_0) t_1) t_2) + (subst t_1 x t_2)) + (==> ((Π (x : t_0) t_1) t_2) + (subst t_1 x t_2)) (==> (case e_9 (x_0 e_0) ... (x e) (x_r e_r) ...) (inductive-apply e e_9) @@ -158,7 +165,8 @@ (define-metafunction cic-redL reduce : e -> e - [(reduce e) ,(car (apply-reduction-relation* ==β (term e)))]) + [(reduce e) t_1 + (where t_1 ,(car (apply-reduction-relation* ==β (term e))))]) (module+ test (check-equal? (term (reduce (Unv 0))) (term (Unv 0))) (check-equal? (term (reduce ((λ (x : t) x) (Unv 0)))) (term (Unv 0))) @@ -323,12 +331,12 @@ [----------------- (wf ∅ ∅)] - [(types Σ Γ t t_0) + [(type-infer Σ Γ t t_0) (wf Σ Γ) ----------------- (wf Σ (Γ x : t))] - [(types Σ ∅ t t_0) + [(type-infer Σ ∅ t t_0) (wf Σ ∅) (side-condition (positive t (result-type Σ t))) ----------------- @@ -349,58 +357,106 @@ (check-false (term (terminates? (μ (x : (Unv 0)) (λ (y : (Unv 0)) (x y)))))) (check-true (term (terminates? (μ (x : (Unv 0)) (λ (y : (Unv 0)) y)))))) + (define-judgment-form cicL + #:mode (α-equivalent I I) + #:contract (α-equivalent t t) + + [----------------- "α-x" + (α-equivalent x x)] + + [----------------- "α-U" + (α-equivalent U U)] + + [(α-equivalent t_1 (subst t_3 x_1 x_0)) + (α-equivalent t_0 t_2) + ----------------- "α-binder" + (α-equivalent (any (x_0 : t_0) t_1) + (any (x_1 : t_2) t_3))] + + [(α-equivalent e_0 e_2) + (α-equivalent e_1 e_3) + ----------------- "α-app" + (α-equivalent (e_0 e_1) (e_2 e_3))] + + [(α-equivalent e_0 e_1) + (α-equivalent e_r0 e_r1) ... + ----------------- "α-case" + (α-equivalent (case e_0 (x_r0 e_r0) ..._1) + (case e_1 (x_r1 e_r1) ..._1))]) + (module+ test + (define-syntax-rule (check-holds (e ...)) + (check-true + (judgment-holds (e ...)))) + (define-syntax-rule (check-not-holds (e ...)) + (check-false + (judgment-holds (e ...)))) + + (check-holds (α-equivalent x x)) + (check-not-holds (α-equivalent x y)) + (check-holds (α-equivalent (λ (x : A) x) + (λ (y : A) y)))) + + (define-judgment-form cicL + #:mode (equivalent I I) + #:contract (equivalent t t) + + [(where t_2 (reduce t_0)) + (where t_3 (reduce t_1)) + (α-equivalent t_2 t_3) + ----------------- "≡-αβ" + (equivalent t_0 t_1)]) + (define-judgment-form cic-typingL - #:mode (types I I I O) - #:contract (types Σ Γ e t) + #:mode (type-infer I I I O) + #:contract (type-infer Σ Γ e t) [(unv-ok U_0 U_1) (wf Σ Γ) ----------------- "DTR-Axiom" - (types Σ Γ U_0 U_1)] + (type-infer Σ Γ U_0 U_1)] [(where t (lookup Σ x)) ----------------- "DTR-Inductive" - (types Σ Γ x t)] + (type-infer Σ Γ x t)] - ;; TODO: Require alpha-equiv here, at least. [(where t (lookup Γ x)) ----------------- "DTR-Start" - (types Σ Γ x t)] + (type-infer Σ Γ x t)] - [(types Σ Γ t_0 U_1) - (types Σ (Γ x : t_0) t U_2) + [(type-infer Σ Γ t_0 U_1) + (type-infer Σ (Γ x : t_0) t U_2) (unv-kind U_1 U_2 U) ----------------- "DTR-Product" - (types Σ Γ (Π (x : t_0) t) U)] + (type-infer Σ Γ (Π (x : t_0) t) U)] - [(types Σ Γ e_0 (Π (x_0 : t_0) t_1)) - (types Σ Γ e_1 t_0) + [(type-infer Σ Γ e_0 (Π (x_0 : t_0) t_1)) + (type-infer Σ Γ e_1 t_2) + (equivalent t_0 t_2) ----------------- "DTR-Application" - (types Σ Γ (e_0 e_1) (subst t_1 x_0 e_1))] + (type-infer Σ Γ (e_0 e_1) (subst t_1 x_0 e_1))] - ;; TODO: This restriction that the names be the same is a little annoying - [(types Σ (Γ x : t_0) e t_1) - (types Σ Γ (Π (x : t_0) t_1) U) + [(type-infer Σ (Γ x : t_0) e t_1) + (type-infer Σ Γ (Π (x : t_0) t_1) U) ----------------- "DTR-Abstraction" - (types Σ Γ (λ (x : t_0) e) (Π (x : t_0) t_1))] + (type-infer Σ Γ (λ (x : t_0) e) (Π (x : t_0) t_1))] [(side-condition (terminates? (μ (x : t_0) e))) - (types Σ (Γ x : t_0) e t_0) - (types Σ Γ t_0 U) + (type-infer Σ (Γ x : t_0) e t_0) + (type-infer Σ Γ t_0 U) ----------------- "DTR-Fix" - (types Σ Γ (μ (x : t_0) e) t_0)] + (type-infer Σ Γ (μ (x : t_0) e) t_0)] - [(types Σ Γ e t_9) + [(type-infer Σ Γ e t_9) (where t_1 (inductive-name t_9)) (side-condition (constructors-for Σ t_1 (x_0 x_1 ...))) - (types Σ Γ e_0 t_00) - (types Σ Γ e_1 t_11) ... + (type-infer Σ Γ e_0 t_00) + (type-infer Σ Γ e_1 t_11) ... ;; TODO Some of these meta-functions aren't very consistent in terms ;; of interface (where t (branch-type t_1 (lookup Σ x_0) t_00)) (side-condition (branch-types-match Σ (x_1 ...) (t_11 ...) t t_1)) ----------------- "DTR-Case" - (types Σ Γ (case e (x_0 e_0) (x_1 e_1) ...) t)] + (type-infer Σ Γ (case e (x_0 e_0) (x_1 e_1) ...) t)] ;; TODO: This shouldn't be a special case, but I failed to forall ;; quantify properly over the branches in the above case, and I'm lazy. @@ -423,60 +479,59 @@ (types Σ Γ t_1 U) ----------------- "DTR-Conversion" (types Σ Γ e t_1)]) + + (define-judgment-form cic-typingL + #:mode (type-check I I I I) + #:contract (type-check Σ Γ e t) + + [(type-infer Σ Γ e t_0) + (equivalent t t_0) + ----------------- "DTR-Check" + (type-check Σ Γ e t)]) (module+ test - (check-true (judgment-holds (types ∅ ∅ (Unv 0) (Unv 1)))) - (check-true (judgment-holds (types ∅ (∅ x : (Unv 0)) (Unv 0) (Unv 1)))) - (check-true (judgment-holds (types ∅ (∅ x : (Unv 0)) x (Unv 0)))) - (check-true (judgment-holds (types ∅ ((∅ x_0 : (Unv 0)) x_1 : (Unv 0)) - (Π (x_3 : x_0) x_1) (Unv 0)))) + (check-holds (type-infer ∅ ∅ (Unv 0) (Unv 1))) + (check-holds (type-infer ∅ (∅ x : (Unv 0)) (Unv 0) (Unv 1))) + (check-holds (type-infer ∅ (∅ x : (Unv 0)) x (Unv 0))) + (check-holds (type-infer ∅ ((∅ x_0 : (Unv 0)) x_1 : (Unv 0)) + (Π (x_3 : x_0) x_1) (Unv 0))) + (check-holds (type-infer ∅ (∅ x_0 : (Unv 0)) x_0 U_1)) + (check-holds (type-infer ∅ ((∅ x_0 : (Unv 0)) x_2 : x_0) (Unv 0) U_2)) + (check-holds (unv-kind (Unv 0) (Unv 0) (Unv 0))) + (check-holds (type-infer ∅ (∅ x_0 : (Unv 0)) (Π (x_2 : x_0) (Unv 0)) t)) - (check-true (judgment-holds (types ∅ (∅ x_0 : (Unv 0)) x_0 U_1))) - (check-true (judgment-holds (types ∅ ((∅ x_0 : (Unv 0)) x_2 : x_0) (Unv 0) U_2))) - (check-true (judgment-holds (unv-kind (Unv 0) (Unv 0) (Unv 0)))) - (check-true (judgment-holds (types ∅ (∅ x_0 : (Unv 0)) (Π (x_2 : x_0) (Unv 0)) t))) - - (check-true (judgment-holds (types ∅ ∅ (λ (x : (Unv 0)) x) (Π (x : (Unv 0)) (Unv 0))))) - (check-true (judgment-holds (types ∅ ∅ (λ (y : (Unv 0)) (λ (x : y) x)) - (Π (y : (Unv 0)) (Π (x : y) y))))) + (check-holds (type-infer ∅ ∅ (λ (x : (Unv 0)) x) (Π (x : (Unv 0)) (Unv 0)))) + (check-holds (type-infer ∅ ∅ (λ (y : (Unv 0)) (λ (x : y) x)) + (Π (y : (Unv 0)) (Π (x : y) y)))) (check-equal? (list (term (Unv 1))) (judgment-holds - (types ∅ ((∅ x1 : (Unv 0)) x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0))) + (type-infer ∅ ((∅ x1 : (Unv 0)) x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0))) U) U)) - (check-true - (judgment-holds - (types ∅ ∅ (Π (x2 : (Unv 0)) (Unv 0)) - U))) - (check-true - (judgment-holds - (types ∅ (∅ x1 : (Unv 0)) (λ (x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0)))) - t))) - (check-true - (judgment-holds (types ((∅ truth : (Unv 0)) T : truth) - ∅ - T - truth))) - (check-true - (judgment-holds (types ((∅ truth : (Unv 0)) T : truth) + (check-holds + (type-infer ∅ ∅ (Π (x2 : (Unv 0)) (Unv 0)) U)) + (check-holds + (type-infer ∅ (∅ x1 : (Unv 0)) (λ (x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0)))) + t)) + (check-holds (type-infer ((∅ truth : (Unv 0)) T : truth) + ∅ T truth)) + (check-holds (type-infer ((∅ truth : (Unv 0)) T : truth) ∅ (Unv 0) - (Unv 1)))) - (check-true - (judgment-holds (types ((∅ truth : (Unv 0)) T : truth) + (Unv 1))) + (check-holds (type-infer ((∅ truth : (Unv 0)) T : truth) ∅ (case T (T (Unv 0))) - (Unv 1)))) + (Unv 1))) - (check-false - (judgment-holds (types ((∅ truth : (Unv 0)) T : truth) - ∅ - (case T (T (Unv 0)) (T (Unv 0))) - (Unv 1)))) + (check-not-holds + (type-infer ((∅ truth : (Unv 0)) T : truth) + ∅ + (case T (T (Unv 0)) (T (Unv 0))) + (Unv 1))) (define-syntax-rule (nat-test syn ...) - (check-true (judgment-holds - (types (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat)) - syn ...)))) + (check-holds (type-infer (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat)) + syn ...))) (nat-test ∅ (Π (x : nat) nat) (Unv 0)) (nat-test ∅ (λ (x : nat) x) (Π (x : nat) nat)) (nat-test ∅ (case zero (zero zero) (s (λ (x : nat) x))) @@ -489,75 +544,68 @@ nat) (nat-test ∅ (case zero (zero (s zero)) (s (λ (x : nat) (s (s x))))) nat) - (check-false (judgment-holds - (types (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat)) - ∅ - (case zero (zero (s zero))) - nat))) + (check-not-holds (type-infer (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat)) + ∅ + (case zero (zero (s zero))) + nat)) (define lam (term (λ (nat : (Unv 0)) nat))) (check-equal? (list (term (Π (nat : (Unv 0)) (Unv 0)))) - (judgment-holds (types ,Σ0 ∅ ,lam t) t)) + (judgment-holds (type-infer ,Σ0 ∅ ,lam t) t)) (check-equal? (list (term (Π (nat : (Unv 0)) (Unv 0)))) - (judgment-holds (types ,Σ2 ∅ ,lam t) t)) + (judgment-holds (type-infer ,Σ2 ∅ ,lam t) t)) (check-equal? (list (term (Π (x : (Π (y : (Unv 0)) y)) nat))) - (judgment-holds (types (∅ nat : (Unv 0)) ∅ (λ (x : (Π (y : (Unv 0)) y)) (x nat)) + (judgment-holds (type-infer (∅ nat : (Unv 0)) ∅ (λ (x : (Π (y : (Unv 0)) y)) (x nat)) t) t)) (check-equal? (list (term (Π (y : (Unv 0)) (Unv 0)))) - (judgment-holds (types (∅ nat : (Unv 0)) ∅ (λ (y : (Unv 0)) y) t) t)) + (judgment-holds (type-infer (∅ nat : (Unv 0)) ∅ (λ (y : (Unv 0)) y) t) t)) (check-equal? (list (term (Unv 0))) - (judgment-holds (types (∅ nat : (Unv 0)) ∅ + (judgment-holds (type-infer (∅ nat : (Unv 0)) ∅ ((λ (x : (Π (y : (Unv 0)) (Unv 0))) (x nat)) (λ (y : (Unv 0)) y)) t) t)) (check-equal? (list (term (Unv 0)) (term (Unv 1))) (judgment-holds - (types ,Σ4 ∅ (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))) + (type-infer ,Σ4 ∅ (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))) U) U)) - (check-true - (judgment-holds (types ,Σ4 (∅ S : (Unv 0)) conj (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B)))))))) - (check-true - (judgment-holds (types ,Σ4 (∅ S : (Unv 0)) S (Unv 0)))) - (check-true - (judgment-holds (types ,Σ4 (∅ S : (Unv 0)) (conj S) - (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))))) - (check-true - (judgment-holds (types ,Σ4 (∅ S : (Unv 0)) (conj S) - (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))))) - (check-true - (judgment-holds (types ,Σ4 ∅ (λ (S : (Unv 0)) (conj S)) - (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))))) - (check-true - (judgment-holds (types ((,Σ4 true : (Unv 0)) tt : true) ∅ + (check-holds + (type-infer ,Σ4 (∅ S : (Unv 0)) conj (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B))))))) + (check-holds (type-infer ,Σ4 (∅ S : (Unv 0)) S (Unv 0))) + (check-holds (type-check ,Σ4 (∅ S : (Unv 0)) (conj S) + (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))) + (check-holds (type-check ,Σ4 (∅ S : (Unv 0)) (conj S) + (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))) + (check-holds (type-check ,Σ4 ∅ (λ (S : (Unv 0)) (conj S)) + (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))))) + (check-holds (type-check ((,Σ4 true : (Unv 0)) tt : true) ∅ ((((conj true) true) tt) tt) - ((and true) true)))) - (check-true - (judgment-holds (types ((,Σ4 true : (Unv 0)) tt : true) ∅ + ((and true) true))) + (check-holds (type-infer ((,Σ4 true : (Unv 0)) tt : true) ∅ (case ((((conj true) true) tt) tt) - (conj (λ (A : (Unv 0)) - (λ (B : (Unv 0)) - (λ (a : A) - (λ (b : B) a)))))) - A))) + (conj (λ (A : (Unv 0)) + (λ (B : (Unv 0)) + (λ (a : A) + (λ (b : B) a)))))) + A)) (define sigma (term (((((((∅ true : (Unv 0)) T : true) false : (Unv 0)) equal : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))) nat : (Unv 0)) heap : (Unv 0)) pre : (Π (temp808 : heap) (Unv 0))))) (define gamma (term (∅ temp863 : pre))) - (check-true (judgment-holds (wf ,sigma ∅))) - (check-true (judgment-holds (wf ,sigma ,gamma))) - (check-true - (judgment-holds (types ,sigma ,gamma (Unv 0) t))) - (check-true - (judgment-holds (types ,sigma ,gamma pre t))) - (check-true - (judgment-holds (types ,sigma (,gamma tmp863 : pre) (Unv 0) (Unv 1)))) - (check-true - (judgment-holds (types ,sigma (,gamma x : false) (case x) t))))) + (check-holds (wf ,sigma ∅)) + (check-holds (wf ,sigma ,gamma)) + (check-holds + (type-infer ,sigma ,gamma (Unv 0) t)) + (check-holds + (type-infer ,sigma ,gamma pre t)) + (check-holds + (type-infer ,sigma (,gamma tmp863 : pre) (Unv 0) (Unv 1))) + (check-holds + (type-infer ,sigma (,gamma x : false) (case x) t)))) ;; This module just provide module language sugar over the redex model. @@ -681,13 +729,18 @@ ;; TODO: Still absurdly slow. Probably doing n^2 checks of sigma and ;; gamma. And lookup on sigma, gamma are linear, so probably n^2 lookup time. (define (type-infer/term t) - (let ([t (judgment-holds (types ,(sigma) ,(gamma) ,t t_0) t_0)]) + (let ([t (judgment-holds (type-infer ,(sigma) ,(gamma) ,t t_0) t_0)]) (and (pair? t) (car t)))) + (define (type-check/term? e t) + (and (judgment-holds (type-check ,(sigma) ,(gamma) ,e ,t)) #t)) + (define (syntax->curnel-syntax syn) (denote syn (cur->datum syn))) (define (denote syn t) - #`(term (reduce (subst-all #,(datum->syntax syn t) #,(first (bind-subst)) #,(second (bind-subst)))))) + (quasisyntax/loc + syn + (term (reduce (subst-all #,(datum->syntax syn t) #,(first (bind-subst)) #,(second (bind-subst))))))) ;; TODO: Blanket disarming is probably a bad idea. (define orig-insp (variable-reference->module-declaration-inspector @@ -746,19 +799,20 @@ reified-term) ;; Reflection tools + (define (normalize/syn syn) + (denote syn (term (reduce (subst-all ,(cur->datum syn) ,(first (bind-subst)) ,(second (bind-subst))))))) + + (define (run-cur->datum syn) + (cur->datum (normalize/syn syn))) ;; TODO: OOps, type-infer doesn't return a cur term but a redex term ;; wrapped in syntax bla. This is bad. (define (type-infer/syn syn) - (let ([t (type-infer/term (cur->datum syn))]) + (let ([t (type-infer/term (run-cur->datum syn))]) (and t (datum->syntax syn t)))) (define (type-check/syn? syn type) - (let ([t (type-infer/term (cur->datum syn))]) - (equal? t (cur->datum type)))) - - (define (normalize/syn syn) - (denote syn (term (reduce (subst-all ,(cur->datum syn) ,(first (bind-subst)) ,(second (bind-subst))))))) + (type-check/term? (run-cur->datum syn) (run-cur->datum type))) ;; Takes a Cur term syn and an arbitrary number of identifiers ls. The cur term is ;; expanded until expansion reaches a Curnel form, or one of the diff --git a/stdlib/nat.rkt b/stdlib/nat.rkt index 1a80012..5795ee0 100644 --- a/stdlib/nat.rkt +++ b/stdlib/nat.rkt @@ -42,6 +42,6 @@ [z btrue] [(s (n4 : nat)) (nat-equal? n3 n4)])])) (module+ test - (check-equal? btrue (nat-equal? z z)) - (check-equal? bfalse (nat-equal? z (s z))) - (check-equal? btrue (nat-equal? (s z) (s z)))) + (check-equal? (nat-equal? z z) btrue) + (check-equal? (nat-equal? z (s z)) bfalse) + (check-equal? (nat-equal? (s z) (s z)) btrue)) diff --git a/stdlib/prop.rkt b/stdlib/prop.rkt index 0049924..8b838b7 100644 --- a/stdlib/prop.rkt +++ b/stdlib/prop.rkt @@ -18,7 +18,7 @@ (define-theorem thm:anything-implies-true (forall (P : Type) true)) -(qed (run thm:anything-implies-true) (lambda (P : Type) T)) +(qed thm:anything-implies-true (lambda (P : Type) T)) (data false : Type) @@ -37,7 +37,7 @@ (case* ab ((conj (P : Type) (Q : Type) (x : P) (y : Q)) (conj Q P y x))))) -#;(qed thm:and-is-symmetric proof:and-is-symmetric) +(qed thm:and-is-symmetric proof:and-is-symmetric) (define-theorem thm:proj1 (forall* (A : Type) (B : Type) (c : (and A B)) A)) diff --git a/stdlib/sugar.rkt b/stdlib/sugar.rkt index a3ed30b..08663ab 100644 --- a/stdlib/sugar.rkt +++ b/stdlib/sugar.rkt @@ -80,8 +80,12 @@ (define-syntax-rule (define-theorem name prop) (define name prop)) -;; TODO: Current implementation doesn't do beta/eta while type-checking -;; because reasons. So manually insert a run in the type annotation -(define-syntax-rule (qed thm pf) - ((lambda (x : (run thm)) Type) pf)) +(define-syntax (qed stx) + (syntax-case stx () + [(_ t pf) + (begin + (unless (type-check/syn? #'pf #'t) + (raise-syntax-error 'qed "Invalid proof" + #'pf #'t)) + #'pf)])) From f8a51e65ca75dfc49e73cb5f54512d6d1e7ca9c2 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Fri, 10 Apr 2015 22:42:51 -0400 Subject: [PATCH 2/2] Attempting to fix case typing checking Maybe I shouldn't bother and should fix that after fixing inductives --- redex-curnel.rkt | 17 +++++++++++++---- stdlib/prop.rkt | 2 +- 2 files changed, 14 insertions(+), 5 deletions(-) diff --git a/redex-curnel.rkt b/redex-curnel.rkt index ee9c740..c8c9417 100644 --- a/redex-curnel.rkt +++ b/redex-curnel.rkt @@ -277,8 +277,9 @@ (define-metafunction cicL branch-type : t t t -> t - [(branch-type t_ind (Π (x_0 : t) e_0) (Π (x_1 : t) e_1)) - (branch-type t_ind e_0 e_1)] + [(branch-type t_ind (Π (x_0 : t_0) e_0) (Π (x_1 : t_1) e_1)) + (branch-type t_ind e_0 e_1) + #;(side-condition (judgment-holds (equivalent t_0 t_1)))] ;[(branch-type t_ind t_ind t) t]) [(branch-type t_ind t_other t) t]) (module+ test @@ -293,7 +294,8 @@ (define-metafunction cic-typingL branch-types-match : Σ (x ...) (t ...) t t -> #t or #f [(branch-types-match Σ (x ...) (t_11 ...) t t_1) - ,(andmap (curry equal? (term t)) (term ((branch-type t_1 (lookup Σ x) t_11) ...)))]) + ,(andmap (lambda (x) (judgment-holds (equivalent ,x t))) + (term ((branch-type t_1 (lookup Σ x) t_11) ...)))]) (module+ test (check-true (term (branch-types-match ((∅ truth : (Unv 0)) T : truth) () () (Unv 0) nat))) @@ -605,7 +607,14 @@ (check-holds (type-infer ,sigma (,gamma tmp863 : pre) (Unv 0) (Unv 1))) (check-holds - (type-infer ,sigma (,gamma x : false) (case x) t)))) + (type-infer ,sigma (,gamma x : false) (case x) t)) + (check-true + (judgment-holds + (type-infer ,Σ4 ∅ + (λ (A3 : (Unv 0)) (λ (B3 : (Unv 0)) (λ (c1 : ((and A3) B3)) + (case c1 + (conj (λ (A1 : (Unv 0)) (λ (B1 : (Unv 0)) (λ (a1 : A1) (λ (b1 : B1) a1))))))))) + t) t)))) ;; This module just provide module language sugar over the redex model. diff --git a/stdlib/prop.rkt b/stdlib/prop.rkt index 8b838b7..9c19266 100644 --- a/stdlib/prop.rkt +++ b/stdlib/prop.rkt @@ -37,7 +37,7 @@ (case* ab ((conj (P : Type) (Q : Type) (x : P) (y : Q)) (conj Q P y x))))) -(qed thm:and-is-symmetric proof:and-is-symmetric) +#;(qed thm:and-is-symmetric proof:and-is-symmetric) (define-theorem thm:proj1 (forall* (A : Type) (B : Type) (c : (and A B)) A))