From 38c1ac928aa78f746d5124ba460080672e75574b Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Fri, 20 Feb 2015 09:55:35 -0500 Subject: [PATCH 1/4] Cleaning up dead code --- redex-curnel.rkt | 50 ++---------------------------------------------- 1 file changed, 2 insertions(+), 48 deletions(-) diff --git a/redex-curnel.rkt b/redex-curnel.rkt index 3273985..6ffc948 100644 --- a/redex-curnel.rkt +++ b/redex-curnel.rkt @@ -405,6 +405,7 @@ ;; 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. ;; TODO: Seem to need bidirectional checking to pull this off + ;; http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf #;[(types Σ Γ e t_9) (where t_1 (inductive-name t_9)) (side-condition (constructors-for Σ t_1 ())) @@ -556,54 +557,7 @@ (check-true (judgment-holds (types ,sigma (,gamma tmp863 : pre) Type (Unv 0)))) (check-true - (judgment-holds (types ,sigma (,gamma x : false) (case x) t))) - ) - - - (define-judgment-form cic-typingL - #:mode (type-check I I I) - #:contract (type-check Γ e t) - - [(types Σ ∅ e t) - --------------- - (type-check Σ e (reduce t))]) - - ;; Infer-core Language - ;; A relaxed core where annotation are optional. - (define-extended-language cic-surfaceL cicL - (v ::= .... (λ x e) (Π t e)) - (t e ::= .... (data x (x : t) (x : t) ...) (case e ([e e] ...)) (e : t))) - - ;; http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf - #;(define-judgment-form cic-typingL - #:mode (synth I I O) - #:contract (synth Γ t t) - - [(unv-ok U_0 U_1) - ----------------- "DTR-SAxiom" - (synth ∅ U_0 U_1)] - - [(where t (lookup Γ x)) - (synth (remove Γ x) t U) - ----------------- "DTR-SStart" - (synth Γ x t)] - - [(synth Γ t t_1) (synth Γ t_0 U) - ----------------- "DTR-SWeakening" - (synth (Γ x : t_0) t t_1)] - - [(check (Γ x : t_0) e t_1) - ----------------- "DTR-SAbstraction" - (check Γ (λ (x : t_0) e) (Π (x : t_0) t_1))] - - [(synth Γ e_0 (Π (x : t_0) t_1)) - (check Γ e_1 t_0) - ----------------- "DTR-SApplication" - (synth Γ (e_0 e_1) (subst t_1 x e_1))] - - [(check Γ e t) - ----------------- "DTR-SAnnotate" - (synth Γ (e : t) t)]) ) + (judgment-holds (types ,sigma (,gamma x : false) (case x) t))))) ;; This module just provide module language sugar over the redex model. From b3388c54134eaa005de012ac5b1f68237fc14d32 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Fri, 20 Feb 2015 18:20:55 -0500 Subject: [PATCH 2/4] Changed Type to Unv 0 * Type should be not be in the core language. Converted all uses of Type to Unv 0, potentially fixing a universe bug in the process. * Added macro Type to Curnel that enables existing code to work more or less as before. --- oll.rkt | 3 +- redex-curnel.rkt | 219 ++++++++++++++++++++++++----------------------- 2 files changed, 112 insertions(+), 110 deletions(-) diff --git a/oll.rkt b/oll.rkt index abb43dd..b80f6a0 100644 --- a/oll.rkt +++ b/oll.rkt @@ -263,7 +263,7 @@ ;; TODO: Need to add these to a literal set and export it ;; Or, maybe overwrite syntax-parse #:literals (lambda forall data real-app case define-theorem - define qed begin) + define qed begin Type) [(begin e ...) (for/fold ([str ""]) ([e (syntax->list #'(e ...))]) @@ -320,6 +320,7 @@ (format "~a~n| ~a : ~a" strs (syntax-e #'x) (output-coq #'t))])))) "")] + [(Type i) "Type"] [(case e (ec eb) ...) (format "(match ~a with~n~aend)" (output-coq #'e) diff --git a/redex-curnel.rkt b/redex-curnel.rkt index 6ffc948..6ba7c2d 100644 --- a/redex-curnel.rkt +++ b/redex-curnel.rkt @@ -18,7 +18,7 @@ ;; -> for non-dependent function types, and type inference. (define-language cicL (i ::= natural) - (U ::= Type (Unv i)) + (U ::= (Unv i)) (x ::= variable-not-otherwise-mentioned) ;; TODO: Having 2 binders is stupid. (v ::= (Π (x : t) t) (μ (x : t) t) (λ (x : t) t) x U) @@ -38,10 +38,8 @@ (check-true (x? (term s))) (check-true (t? (term zero))) (check-true (t? (term s))) - (check-true (t? (term Type))) (check-true (x? (term nat))) (check-true (t? (term nat))) - (check-true (U? (term Type))) (check-true (U? (term (Unv 0)))) (check-true (e? (term (λ (x_0 : (Unv 0)) x_0)))) (check-true (v? (term (λ (x_0 : (Unv 0)) x_0)))) @@ -49,15 +47,12 @@ (check-true (t? (term (λ (x_0 : (Unv 0)) x_0))))) ;; 'A' - ;; Types of Universes + ;; Universes ;; Replace with sub-typing (define-judgment-form cicL #:mode (unv-ok I O) #:contract (unv-ok U U) - [----------------- - (unv-ok Type (Unv 0))] - [(where i_1 ,(add1 (term i_0))) ----------------- (unv-ok (Unv i_0) (Unv i_1))]) @@ -69,13 +64,13 @@ #:contract (unv-kind U U U) [---------------- - (unv-kind Type Type Type)] + (unv-kind (Unv 0) (Unv 0) (Unv 0))] [---------------- - (unv-kind Type (Unv i) (Unv i))] + (unv-kind (Unv 0) (Unv i) (Unv i))] [---------------- - (unv-kind (Unv i) Type Type)] + (unv-kind (Unv i) (Unv 0) (Unv 0))] [(where i_3 ,(max (term i_1) (term i_2))) ---------------- @@ -161,12 +156,12 @@ reduce : e -> e [(reduce e) ,(car (apply-reduction-relation* ==β (term e)))]) (module+ test - (check-equal? (term (reduce Type)) (term Type)) - (check-equal? (term (reduce ((λ (x : t) x) Type))) (term Type)) - (check-equal? (term (reduce ((Π (x : t) x) Type))) (term Type)) + (check-equal? (term (reduce (Unv 0))) (term (Unv 0))) + (check-equal? (term (reduce ((λ (x : t) x) (Unv 0)))) (term (Unv 0))) + (check-equal? (term (reduce ((Π (x : t) x) (Unv 0)))) (term (Unv 0))) ;; NB: Currently not reducing under binders. I forget why. - (check-equal? (term (reduce (Π (x : t) ((Π (x_0 : t) x_0) Type)))) - (term (Π (x : t) Type))) + (check-equal? (term (reduce (Π (x : t) ((Π (x_0 : t) x_0) (Unv 0))))) + (term (Π (x : t) (Unv 0)))) (check-equal? (term (reduce (Π (x : t) ((Π (x_0 : t) x_0) x)))) (term (Π (x : t) x))) (check-equal? (term (reduce (case (s z) (z (s z)) (s (λ (x : nat) @@ -186,12 +181,12 @@ (define Γ? (redex-match? cic-typingL Γ)) (module+ test ;; TODO: Rename these signatures, and use them in all future tests. - (define Σ (term (((∅ nat : Type) zero : nat) s : (Π (x : nat) nat)))) + (define Σ (term (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat)))) (define Σ0 (term ∅)) - (define Σ2 (term (((∅ nat : Type) z : nat) s : (Π (x : nat) nat)))) - (define Σ3 (term (∅ and : (Π (A : Type) (Π (B : Type) Type))))) - (define Σ4 (term (,Σ3 conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B) ((and A) B)))))))) + (define Σ2 (term (((∅ nat : (Unv 0)) z : nat) s : (Π (x : nat) nat)))) + (define Σ3 (term (∅ and : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))))) + (define Σ4 (term (,Σ3 conj : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B)))))))) (check-true (Σ? Σ0)) (check-true (Σ? Σ2)) @@ -242,14 +237,14 @@ (constructor-for (Σ x_0 : t_0) t_1 x)]) (module+ test (check-true - (judgment-holds (constructor-for ((∅ truth : Type) T : truth) truth T))) + (judgment-holds (constructor-for ((∅ truth : (Unv 0)) T : truth) truth T))) (check-true (judgment-holds - (constructor-for ((∅ nat : Type) zero : nat) + (constructor-for ((∅ nat : (Unv 0)) zero : nat) nat zero))) (check set=? (judgment-holds - (constructor-for (((∅ nat : Type) zero : nat) s : (Π (x : nat) nat)) + (constructor-for (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat)) nat x) x) (list (term zero) (term s)))) (define-metafunction cic-typingL @@ -260,10 +255,10 @@ (judgment-holds (constructor-for Σ x_0 x_00) x_00))]) (module+ test (check-true - (term (constructors-for (((∅ nat : Type) zero : nat) s : (Π (x : nat) nat)) + (term (constructors-for (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat)) nat (zero s)))) (check-false - (term (constructors-for (((∅ nat : Type) zero : nat) s : (Π (x : nat) nat)) + (term (constructors-for (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat)) nat (zero)))) (check-true (term (constructors-for ,Σ4 and (conj))))) @@ -275,13 +270,13 @@ ;[(branch-type t_ind t_ind t) t]) [(branch-type t_ind t_other t) t]) (module+ test - (check-equal? (term Type) (term (branch-type nat (lookup ,Σ zero) Type))) + (check-equal? (term (Unv 0)) (term (branch-type nat (lookup ,Σ zero) (Unv 0)))) (check-equal? (term nat) (term (branch-type nat nat nat))) - (check-equal? (term Type) (term (branch-type nat (lookup ,Σ s) (Π (x : nat) Type)))) + (check-equal? (term (Unv 0)) (term (branch-type nat (lookup ,Σ s) (Π (x : nat) (Unv 0))))) (check-equal? - (term Type) + (term (Unv 0)) (term (branch-type and (lookup ,Σ4 conj) - (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B) Type)))))))) + (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) (Unv 0))))))))) (define-metafunction cic-typingL branch-types-match : Σ (x ...) (t ...) t t -> #t or #f @@ -289,33 +284,33 @@ ,(andmap (curry equal? (term t)) (term ((branch-type t_1 (lookup Σ x) t_11) ...)))]) (module+ test (check-true - (term (branch-types-match ((∅ truth : Type) T : truth) () () Type nat))) + (term (branch-types-match ((∅ truth : (Unv 0)) T : truth) () () (Unv 0) nat))) (check-true - (term (branch-types-match ,Σ (zero s) (Type (Π (x : nat) Type)) Type nat))) + (term (branch-types-match ,Σ (zero s) ((Unv 0) (Π (x : nat) (Unv 0))) (Unv 0) nat))) (check-true (term (branch-types-match ,Σ (zero s) (nat (Π (x : nat) nat)) nat nat)))) ;; TODO: Add positivity checking. (define-metafunction cicL positive : t any -> #t or #f - ;; Type; not a inductive constructor + ;; (Unv 0); not a inductive constructor [(positive any_1 any_2) #t]) (module+ test (check-true (term (positive nat nat))) - (check-true (term (positive (Π (x : Type) (Π (y : Type) Type)) #f))) + (check-true (term (positive (Π (x : (Unv 0)) (Π (y : (Unv 0)) (Unv 0))) #f))) (check-true (term (positive (Π (x : nat) nat) nat))) ;; (nat -> nat) -> nat ;; Not sure if this is actually supposed to pass (check-false (term (positive (Π (x : (Π (y : nat) nat)) nat) nat))) - ;; (Type -> nat) -> nat - (check-true (term (positive (Π (x : (Π (y : Type) nat)) nat) nat))) - ;; (((nat -> Type) -> nat) -> nat) - (check-true (term (positive (Π (x : (Π (y : (Π (x : nat) Type)) nat)) nat) nat))) + ;; ((Unv 0) -> nat) -> nat + (check-true (term (positive (Π (x : (Π (y : (Unv 0)) nat)) nat) nat))) + ;; (((nat -> (Unv 0)) -> nat) -> nat) + (check-true (term (positive (Π (x : (Π (y : (Π (x : nat) (Unv 0))) nat)) nat) nat))) ;; Not sure if this is actually supposed to pass (check-false (term (positive (Π (x : (Π (y : (Π (x : nat) nat)) nat)) nat) nat))) - (check-true (term (positive Type #f)))) + (check-true (term (positive (Unv 0) #f)))) (define-judgment-form cic-typingL #:mode (wf I I) @@ -336,19 +331,19 @@ (wf (Σ x : t) ∅)]) (module+ test (check-true (judgment-holds (wf ∅ ∅))) - (check-true (judgment-holds (wf (∅ truth : Type) ∅))) - (check-true (judgment-holds (wf ∅ (∅ x : Type)))) - (check-true (judgment-holds (wf (∅ nat : Type) (∅ x : nat)))) - (check-true (judgment-holds (wf (∅ nat : Type) (∅ x : (Π (x : nat) nat)))))) + (check-true (judgment-holds (wf (∅ truth : (Unv 0)) ∅))) + (check-true (judgment-holds (wf ∅ (∅ x : (Unv 0))))) + (check-true (judgment-holds (wf (∅ nat : (Unv 0)) (∅ x : nat)))) + (check-true (judgment-holds (wf (∅ nat : (Unv 0)) (∅ x : (Π (x : nat) nat)))))) ;; TODO: Add termination checking (define-metafunction cicL terminates? : t -> #t or #f [(terminates? t) #t]) (module+ test - (check-false (term (terminates? (μ (x : Type) x)))) - (check-false (term (terminates? (μ (x : Type) (λ (y : Type) (x y)))))) - (check-true (term (terminates? (μ (x : Type) (λ (y : Type) y)))))) + (check-false (term (terminates? (μ (x : (Unv 0)) x)))) + (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 cic-typingL #:mode (types I I I O) @@ -424,64 +419,64 @@ ----------------- "DTR-Conversion" (types Γ e t_1)]) (module+ test - (check-true (judgment-holds (types ∅ ∅ Type (Unv 0)))) - (check-true (judgment-holds (types ∅ (∅ x : Type) Type (Unv 0)))) - (check-true (judgment-holds (types ∅ (∅ x : Type) x Type))) - (check-true (judgment-holds (types ∅ ((∅ x_0 : Type) x_1 : Type) - (Π (x_3 : x_0) x_1) Type))) + (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-true (judgment-holds (types ∅ (∅ x_0 : Type) x_0 U_1))) - (check-true (judgment-holds (types ∅ ((∅ x_0 : Type) x_2 : x_0) Type U_2))) - (check-true (judgment-holds (unv-kind Type (Unv 0) (Unv 0)))) - (check-true (judgment-holds (types ∅ (∅ x_0 : Type) (Π (x_2 : x_0) Type) 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 : Type) x) (Π (x : Type) Type)))) - (check-true (judgment-holds (types ∅ ∅ (λ (y : Type) (λ (x : y) x)) - (Π (y : Type) (Π (x : y) y))))) + (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-equal? (list (term (Unv 0))) + (check-equal? (list (term (Unv 1))) (judgment-holds - (types ∅ ((∅ x1 : Type) x2 : Type) (Π (t6 : x1) (Π (t2 : x2) Type)) + (types ∅ ((∅ x1 : (Unv 0)) x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0))) U) U)) (check-true (judgment-holds - (types ∅ ∅ (Π (x2 : Type) (Unv 0)) + (types ∅ ∅ (Π (x2 : (Unv 0)) (Unv 0)) U))) (check-true (judgment-holds - (types ∅ (∅ x1 : Type) (λ (x2 : Type) (Π (t6 : x1) (Π (t2 : x2) Type))) + (types ∅ (∅ x1 : (Unv 0)) (λ (x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0)))) t))) (check-true - (judgment-holds (types ((∅ truth : Type) T : truth) + (judgment-holds (types ((∅ truth : (Unv 0)) T : truth) ∅ T truth))) (check-true - (judgment-holds (types ((∅ truth : Type) T : truth) + (judgment-holds (types ((∅ truth : (Unv 0)) T : truth) ∅ - Type - (Unv 0)))) + (Unv 0) + (Unv 1)))) (check-true - (judgment-holds (types ((∅ truth : Type) T : truth) + (judgment-holds (types ((∅ truth : (Unv 0)) T : truth) ∅ - (case T (T Type)) - (Unv 0)))) + (case T (T (Unv 0))) + (Unv 1)))) (check-false - (judgment-holds (types ((∅ truth : Type) T : truth) + (judgment-holds (types ((∅ truth : (Unv 0)) T : truth) ∅ - (case T (T Type) (T Type)) - (Unv 0)))) + (case T (T (Unv 0)) (T (Unv 0))) + (Unv 1)))) (define-syntax-rule (nat-test syn ...) (check-true (judgment-holds - (types (((∅ nat : Type) zero : nat) s : (Π (x : nat) nat)) + (types (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat)) syn ...)))) - (nat-test ∅ (Π (x : nat) nat) Type) + (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))) nat) - (nat-test ∅ nat Type) + (nat-test ∅ nat (Unv 0)) (nat-test ∅ zero nat) (nat-test ∅ s (Π (x : nat) nat)) (nat-test ∅ (s zero) nat) @@ -490,72 +485,72 @@ (nat-test ∅ (case zero (zero (s zero)) (s (λ (x : nat) (s (s x))))) nat) (check-false (judgment-holds - (types (((∅ nat : Type) zero : nat) s : (Π (x : nat) nat)) + (types (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat)) ∅ (case zero (zero (s zero))) nat))) - (define lam (term (λ (nat : Type) nat))) + (define lam (term (λ (nat : (Unv 0)) nat))) (check-equal? - (list (term (Π (nat : Type) Type))) + (list (term (Π (nat : (Unv 0)) (Unv 0)))) (judgment-holds (types ,Σ0 ∅ ,lam t) t)) (check-equal? - (list (term (Π (nat : Type) Type))) + (list (term (Π (nat : (Unv 0)) (Unv 0)))) (judgment-holds (types ,Σ2 ∅ ,lam t) t)) (check-equal? - (list (term (Π (x : (Π (y : Type) y)) nat))) - (judgment-holds (types (∅ nat : Type) ∅ (λ (x : (Π (y : Type) y)) (x nat)) + (list (term (Π (x : (Π (y : (Unv 0)) y)) nat))) + (judgment-holds (types (∅ nat : (Unv 0)) ∅ (λ (x : (Π (y : (Unv 0)) y)) (x nat)) t) t)) (check-equal? - (list (term (Π (y : Type) Type))) - (judgment-holds (types (∅ nat : Type) ∅ (λ (y : Type) y) t) t)) + (list (term (Π (y : (Unv 0)) (Unv 0)))) + (judgment-holds (types (∅ nat : (Unv 0)) ∅ (λ (y : (Unv 0)) y) t) t)) (check-equal? - (list (term Type)) - (judgment-holds (types (∅ nat : Type) ∅ - ((λ (x : (Π (y : Type) Type)) (x nat)) - (λ (y : Type) y)) + (list (term (Unv 0))) + (judgment-holds (types (∅ nat : (Unv 0)) ∅ + ((λ (x : (Π (y : (Unv 0)) (Unv 0))) (x nat)) + (λ (y : (Unv 0)) y)) t) t)) (check-equal? - (list (term Type)) + (list (term (Unv 0)) (term (Unv 1))) (judgment-holds - (types ,Σ4 ∅ (Π (S : Type) (Π (B : Type) (Π (a : S) (Π (b : B) ((and S) B))))) + (types ,Σ4 ∅ (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))) U) U)) (check-true - (judgment-holds (types ,Σ4 (∅ S : Type) conj (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B) ((and A) B)))))))) + (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 : Type) S Type))) + (judgment-holds (types ,Σ4 (∅ S : (Unv 0)) S (Unv 0)))) (check-true - (judgment-holds (types ,Σ4 (∅ S : Type) (conj S) - (Π (B : Type) (Π (a : S) (Π (b : B) ((and S) B))))))) + (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 : Type) (conj S) - (Π (B : Type) (Π (a : S) (Π (b : B) ((and S) B))))))) + (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 : Type) (conj S)) - (Π (S : Type) (Π (B : Type) (Π (a : S) (Π (b : B) ((and S) B)))))))) + (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 : Type) tt : true) ∅ + (judgment-holds (types ((,Σ4 true : (Unv 0)) tt : true) ∅ ((((conj true) true) tt) tt) ((and true) true)))) (check-true - (judgment-holds (types ((,Σ4 true : Type) tt : true) ∅ + (judgment-holds (types ((,Σ4 true : (Unv 0)) tt : true) ∅ (case ((((conj true) true) tt) tt) - (conj (λ (A : Type) - (λ (B : Type) + (conj (λ (A : (Unv 0)) + (λ (B : (Unv 0)) (λ (a : A) (λ (b : B) a)))))) A))) - (define sigma (term (((((((∅ true : Type) T : true) false : Type) equal : (Π (A : Type) - (Π (B : Type) Type))) - nat : Type) heap : Type) pre : (Π (temp808 : heap) Type)))) + (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 Type t))) + (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) Type (Unv 0)))) + (judgment-holds (types ,sigma (,gamma tmp863 : pre) (Unv 0) (Unv 1)))) (check-true (judgment-holds (types ,sigma (,gamma x : false) (case x) t))))) @@ -606,8 +601,10 @@ [dep-case case] [dep-var #%top] + ; [dep-datum #%datum] [dep-define define]) + Type ;; DYI syntax extension define-syntax begin-for-syntax @@ -695,11 +692,9 @@ ;; Locally expand everything down to core forms. (define (core-expand syn) (disarm - (if (identifier? syn) - syn - (local-expand syn 'expression + (local-expand syn 'expression (append (syntax-e #'(term reduce subst-all dep-var #%app λ Π μ case - Type))))))) + Unv #%datum)))))) ;; Only type-check at the top-level, to prevent exponential ;; type-checking. Redex is expensive enough. @@ -715,11 +710,12 @@ (let cur->datum ([syn syn]) (syntax-parse (core-expand syn) #:literals (term reduce #%app subst-all) - #:datum-literals (case Π λ μ : Type) + #:datum-literals (case Π λ μ : Unv) [x:id (syntax->datum #'x)] [(subst-all e _ _) (syntax->datum #'e)] [(reduce e) (cur->datum #'e)] [(term e) (cur->datum #'e)] + [(Unv i) (term (Unv ,(syntax->datum #'i)))] ;; TODO: should really check that b is one of the binders ;; Maybe make a syntax class for the binders, core forms, ;; etc. @@ -938,6 +934,11 @@ (syntax-case syn (:) [(_ (x : t) e) (syntax->curnel-syntax #`(Π (x : t) e))])) + (define-syntax (Type syn) + (syntax-case syn () + [(_ i) (syntax->curnel-syntax #'(Unv i))] + [_ #'(Type 0)])) + (define-syntax (dep-fix syn) (syntax-case syn (:) [(_ (x : t) e) (syntax->curnel-syntax #`(μ (x : t) e))])) From 6b0d09c7d92e8dcb48532ce9db552c6318924f2e Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Fri, 20 Feb 2015 18:22:04 -0500 Subject: [PATCH 3/4] Redex 1.6 enables caching of judgment forms! * Judgment form caching enables running test suite in seconds instead of days. * Fixed numerous bugs after properly exercising the oll/stlc examples. --- README.md | 3 ++- oll.rkt | 7 ++++--- redex-curnel.rkt | 2 +- stlc.rkt | 13 +++++++------ 4 files changed, 14 insertions(+), 11 deletions(-) diff --git a/README.md b/README.md index ea70ba9..2bb701a 100644 --- a/README.md +++ b/README.md @@ -16,7 +16,8 @@ cur (plural curs) Getting started =============== -Don't actually try to run anything. The type-checker may be exponential, +Requires redex-lib version 1.6 if you want answer in a reasonable amount +of time. Otherwise, the type-checker may require exponential time or worse. Open up `stlc.rkt` to see an example of what advanced meta-programming can let you do. diff --git a/oll.rkt b/oll.rkt index b80f6a0..89366bd 100644 --- a/oll.rkt +++ b/oll.rkt @@ -54,10 +54,11 @@ (with-output-to-file (syntax->datum #'latex-file) (thunk (format "\\fbox{$~a$}$~n$\\begin{mathpar}~n~a~n\end{mathpar}$$" + (syntax->datum #'(n types* ...)) (string-trim (for/fold ([str ""]) - ([rule (syntax->datum #'(rules.latex ...))]) - (format "~a~a\\and~n" rule)) + ([rule (attribute rules.latex)]) + (format "~a~a\\and~n" str rule)) "\\and" #:left? #f))) #:exists 'append)) @@ -311,7 +312,7 @@ (begin (coq-lift-top-level (format "Inductive ~a : ~a :=~a." - (syntax-e #'n) + (sanitize-id (format "~a" (syntax-e #'n))) (output-coq #'t) (for/fold ([strs ""]) ([clause (syntax->list #'((x* : t*) ...))]) diff --git a/redex-curnel.rkt b/redex-curnel.rkt index 6ba7c2d..da1e3e4 100644 --- a/redex-curnel.rkt +++ b/redex-curnel.rkt @@ -47,7 +47,7 @@ (check-true (t? (term (λ (x_0 : (Unv 0)) x_0))))) ;; 'A' - ;; Universes + ;; (Unv 0)s of Universes ;; Replace with sub-typing (define-judgment-form cicL #:mode (unv-ok I O) diff --git a/stlc.rkt b/stlc.rkt index 6117061..9616a33 100644 --- a/stlc.rkt +++ b/stlc.rkt @@ -15,17 +15,16 @@ ;; TODO: Abstract this over stlc-type, and provide from in OLL (data gamma : Type (emp-gamma : gamma) - (ext-gamma : (->* gamma var stlc-type gamma))) + (extend-gamma : (->* gamma var stlc-type gamma))) (define-rec (lookup-gamma (g : gamma) (x : var) : (maybe stlc-type)) (case* g [emp-gamma (none stlc-type)] - [(ext-gamma (g1 : gamma) (v1 : var) (t1 : stlc-type)) + [(extend-gamma (g1 : gamma) (v1 : var) (t1 : stlc-type)) (if (var-equal? v1 x) (some stlc-type t1) (lookup-gamma g1 x))])) - (define-relation (has-type gamma stlc-term stlc-type) #:output-coq "stlc.v" #:output-latex "stlc.tex" @@ -41,7 +40,7 @@ ------------------------ T-False (has-type g (stlc-val-->-stlc-term stlc-false) stlc-boolty)] - [(g : gamma) (x : var) (t : style-type) + [(g : gamma) (x : var) (t : stlc-type) (== (maybe stlc-type) (lookup-gamma g x) (some stlc-type t)) ------------------------ T-Var (has-type g (var-->-stlc-term x) t)] @@ -55,9 +54,11 @@ [(g : gamma) (e1 : stlc-term) (e2 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) + (t : stlc-type) + (x : var) (y : var) (has-type g e1 (stlc-* t1 t2)) - (has-type (extend-gamma (extend-gamma g x t1) t y2) e2 t) - ---------------------- T-Pair + (has-type (extend-gamma (extend-gamma g x t1) y t2) e2 t) + ---------------------- T-Let (has-type g (stlc-let x y e1 e2) t)] [(g : gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : var) From 2ddf7ce3520e408ded714db7972df921522b0147 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Fri, 20 Feb 2015 19:12:06 -0500 Subject: [PATCH 4/4] Fixed several bugs, found several more Trying to fix proofs for free examples; found several bugs but more still exist. Added TODOs --- proofs-for-free.rkt | 64 ++++++++++++++++++++++++--------------------- redex-curnel.rkt | 15 +++++++---- stdlib/sugar.rkt | 4 +-- 3 files changed, 45 insertions(+), 38 deletions(-) diff --git a/proofs-for-free.rkt b/proofs-for-free.rkt index 9815121..ac591d1 100644 --- a/proofs-for-free.rkt +++ b/proofs-for-free.rkt @@ -1,5 +1,6 @@ #lang s-exp "redex-curnel.rkt" -(require "stdlib/sugar.rkt" "stdlib/prop.rkt") +(require "stdlib/sugar.rkt" "stdlib/prop.rkt" racket/trace + (for-syntax racket/syntax)) ;; --------- (begin-for-syntax @@ -7,40 +8,42 @@ (format-id x "~a~a" x i))) (define-syntax (rename syn) - (syntax-case syn (Type forall Unv lambda :) - [(_ i ls Type) #'Type] - [(_ i ls (Unv n)) #'(Unv n)] - [(_ i (xr ...) (lambda (x : t) e)) - #'(lambda (x : (rename i (xr ...) t)) - (rename i (xr ... x) e))] - [(_ i (xr ...) (forall (x : t) e)) - #'(forall (x : (rename i (xr ...) t)) - (rename i (xr ... x) e))] - [(_ i ls (e1 e2)) - #'((rename i ls e1) (rename i ls e2))] - [(_ i ls x) - (if (member (syntax->datum #'x) (syntax->datum #'ls)) - #'x - (rename_id (syntax->datum #'i) #'x))])) + (syntax-case syn () + [(_ i ls e) + (syntax-case #`(ls #,(cur-expand #'e)) (Type forall Unv lambda :) + [(_ Type) #'Type] + [(_ (Unv n)) #'(Unv n)] + [((xr ...) (lambda (x : t) e)) + #'(lambda (x : (rename i (xr ...) t)) + (rename i (xr ... x) e))] + [((xr ...) (forall (x : t) e)) + #'(forall (x : (rename i (xr ...) t)) + (rename i (xr ... x) e))] + [(ls (e1 e2)) + #'((rename i ls e1) (rename i ls e2))] + [(ls x) + (if (member (syntax->datum #'x) (syntax->datum #'ls)) + #'x + (rename_id (syntax->datum #'i) #'x))])])) -(define-syntax (translate syn) - (syntax-parse (cur-expand syn) +(trace-define-syntax (translate syn) + (syntax-parse (cur-expand (syntax-case syn () [(_ e) #'e])) ;; TODO: Need to add these to a literal set and export it ;; Or, maybe redefine syntax-parse #:datum-literals (:) #:literals (lambda forall data real-app case Type) - [(_ Type) + [Type #'(lambda* (x1 : Type) (x2 : Type) (->* x1 x2 Type))] - [(_ (forall (x : A) B)) + [(forall (x : A) B) (let ([x1 (rename_id 1 #'x)] [x2 (rename_id 2 #'x)] [xr (rename_id 'r #'x)]) #`(lambda* (f1 : (rename 1 () (forall (x : A) B))) (f2 : (rename 2 () (forall (x : A) B))) (forall* (#,x1 : (rename 1 () A)) (#,x2 : (rename 2 () A)) - (#,xr : ((translate A) #,x1 #,x2)) + (#,xr : (run ((translate A) #,x1 #,x2))) ((translate B) (f1 #,x1) (f2 #,x2)))))] - [(_ (lambda (x : A) B)) + [(lambda (x : A) B) (let ([x1 (rename_id 1 #'x)] [x2 (rename_id 2 #'x)] [xr (rename_id 'r #'x)]) @@ -48,15 +51,15 @@ (f2 : (rename 2 () (forall (x : A) B))) (forall* (#,x1 : (rename 1 () A)) (#,x2 : (rename 2 () A)) - (#,xr : ((translate A) #,x1 #,x2)) + (#,xr : (run ((translate A) #,x1 #,x2))) ((translate B) (f1 #,x1) (f2 #,x2)))))] - [(_ (data id : t (c : tc) ...)) + [(data id : t (c : tc) ...) (let ([t #`(data #,(rename_id 'r #'id) : (translate t) ((translate c) : (translate tc)) ...)]) t)] - [(_ (f a)) + [(f a) #`((translate f) (rename 1 () a) (rename 2 () a) (translate a))] - [(_ x) + [x:id ;; TODO: Look up x and generate the relation. Otherwise I need to ;; manually translate all dependencies. ;; Not sure this is quite right; Racket's hygiene might `save' me. @@ -66,15 +69,16 @@ (define-type X Type) (define X1 X) (define X2 X) -(define (Xr (x1 : X) (x2 : X)) true) +(define (Xr (x1 : X1) (x2 : X2)) true) ;; The type of a CPS function (define-type CPSf (forall* (ans : Type) (k : (-> X ans)) ans)) (define (CPSf-relation (f1 : CPSf) (f2 : CPSf)) - ;; Run performs substitution, among other things, at compile. - (translate (run CPSf))) -(module+ test + ;; TODO: Fix run so I can simply use (run CPSf) to perform + ;; substitution + (translate (forall* (ans : Type) (k : (-> X ans)) ans))) +#;(module+ test (require rackunit) (check-equal? (translate (forall* (ans : Type) (k : (-> X ans)) ans)) diff --git a/redex-curnel.rkt b/redex-curnel.rkt index da1e3e4..fe8b6ba 100644 --- a/redex-curnel.rkt +++ b/redex-curnel.rkt @@ -9,6 +9,8 @@ (provide (all-defined-out)) + (set-cache-size! 10000) + ;; References: ;; http://www3.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf ;; https://www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf @@ -358,6 +360,7 @@ ----------------- "DTR-Inductive" (types Σ Γ x t)] + ;; TODO: Require alpha-equiv here, at least. [(where t (lookup Γ x)) ----------------- "DTR-Start" (types Σ Γ x t)] @@ -412,12 +415,12 @@ ;; searches it. ;; Perhaps something closer to Zombies = type would be better. ;; For now, reduce types - #;[(types Γ e (in-hole E t)) + #;[(types Σ Γ e (in-hole E t)) (where t_0 (in-hole E t)) (where t_1 ,(car (apply-reduction-relation* ==β (term t_0)))) - (types Γ t_1 U) + (types Σ Γ t_1 U) ----------------- "DTR-Conversion" - (types Γ e t_1)]) + (types Σ Γ e t_1)]) (module+ test (check-true (judgment-holds (types ∅ ∅ (Unv 0) (Unv 1)))) (check-true (judgment-holds (types ∅ (∅ x : (Unv 0)) (Unv 0) (Unv 1)))) @@ -693,8 +696,8 @@ (define (core-expand syn) (disarm (local-expand syn 'expression - (append (syntax-e #'(term reduce subst-all dep-var #%app λ Π μ case - Unv #%datum)))))) + (append (syntax-e #'(term reduce subst-all dep-var #%app λ Π μ case + Unv #%datum)))))) ;; Only type-check at the top-level, to prevent exponential ;; type-checking. Redex is expensive enough. @@ -764,6 +767,8 @@ dep-fix dep-forall dep-var)) ls))))) + ;; TODO: OOps, run doesn't return a cur term but a redex term + ;; wrapped in syntax bla. This is bad. (define-syntax (run syn) (syntax-case syn () [(_ expr) (normalize/syn #'expr)])) diff --git a/stdlib/sugar.rkt b/stdlib/sugar.rkt index 8a5affb..a3ed30b 100644 --- a/stdlib/sugar.rkt +++ b/stdlib/sugar.rkt @@ -18,9 +18,7 @@ (define-syntax (-> syn) (syntax-case syn () - [(_ t1 t2) - (with-syntax ([(x) (generate-temporaries '(1))]) - #`(forall (x : t1) t2))])) + [(_ t1 t2) #`(forall (#,(gensym) : t1) t2)])) (define-syntax ->* (syntax-rules ()