suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Changed Type to Unv 0

Browse Source 
* 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.
This commit is contained in:
William J. Bowman 2015-02-20 18:20:55 -05:00
parent 38c1ac928a
commit b3388c5413
2 changed files with 112 additions and 110 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
oll.rkt
View File

@ -263,7 +263,7 @@
;; TODO: Need to add these to a literal set and export it ;; TODO: Need to add these to a literal set and export it
;; Or, maybe overwrite syntax-parse ;; Or, maybe overwrite syntax-parse
#:literals (lambda forall data real-app case define-theorem #:literals (lambda forall data real-app case define-theorem
define qed begin) define qed begin Type)
[(begin e ...) [(begin e ...)
(for/fold ([str ""]) (for/fold ([str ""])
([e (syntax->list #'(e ...))]) ([e (syntax->list #'(e ...))])
@ -320,6 +320,7 @@
(format "~a~n| ~a : ~a" strs (syntax-e #'x) (format "~a~n| ~a : ~a" strs (syntax-e #'x)
(output-coq #'t))])))) (output-coq #'t))]))))
"")] "")]
[(Type i) "Type"]
[(case e (ec eb) ...) [(case e (ec eb) ...)
(format "(match ~a with~n~aend)" (format "(match ~a with~n~aend)"
(output-coq #'e) (output-coq #'e)

219
redex-curnel.rkt
View File

@ -18,7 +18,7 @@
;; -> for non-dependent function types, and type inference. ;; -> for non-dependent function types, and type inference.
(define-language cicL (define-language cicL
(i ::= natural) (i ::= natural)
(U ::= Type (Unv i)) (U ::= (Unv i))
(x ::= variable-not-otherwise-mentioned) (x ::= variable-not-otherwise-mentioned)
;; TODO: Having 2 binders is stupid. ;; TODO: Having 2 binders is stupid.
(v ::= (Π (x : t) t) (μ (x : t) t) (λ (x : t) t) x U) (v ::= (Π (x : t) t) (μ (x : t) t) (λ (x : t) t) x U)
@ -38,10 +38,8 @@
(check-true (x? (term s))) (check-true (x? (term s)))
(check-true (t? (term zero))) (check-true (t? (term zero)))
(check-true (t? (term s))) (check-true (t? (term s)))
(check-true (t? (term Type)))
(check-true (x? (term nat))) (check-true (x? (term nat)))
(check-true (t? (term nat))) (check-true (t? (term nat)))
(check-true (U? (term Type)))
(check-true (U? (term (Unv 0)))) (check-true (U? (term (Unv 0))))
(check-true (e? (term (λ (x_0 : (Unv 0)) x_0)))) (check-true (e? (term (λ (x_0 : (Unv 0)) x_0))))
(check-true (v? (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))))) (check-true (t? (term (λ (x_0 : (Unv 0)) x_0)))))
;; 'A' ;; 'A'
;; Types of Universes ;; Universes
;; Replace with sub-typing ;; Replace with sub-typing
(define-judgment-form cicL (define-judgment-form cicL
#:mode (unv-ok I O) #:mode (unv-ok I O)
#:contract (unv-ok U U) #:contract (unv-ok U U)
[-----------------
(unv-ok Type (Unv 0))]
[(where i_1 ,(add1 (term i_0))) [(where i_1 ,(add1 (term i_0)))
----------------- -----------------
(unv-ok (Unv i_0) (Unv i_1))]) (unv-ok (Unv i_0) (Unv i_1))])
@ -69,13 +64,13 @@
#:contract (unv-kind U U U) #: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))) [(where i_3 ,(max (term i_1) (term i_2)))
---------------- ----------------
@ -161,12 +156,12 @@
reduce : e -> e reduce : e -> e
[(reduce e) ,(car (apply-reduction-relation* ==β (term e)))]) [(reduce e) ,(car (apply-reduction-relation* ==β (term e)))])
(module+ test (module+ test
(check-equal? (term (reduce Type)) (term Type)) (check-equal? (term (reduce (Unv 0))) (term (Unv 0)))
(check-equal? (term (reduce ((λ (x : t) x) Type))) (term Type)) (check-equal? (term (reduce ((λ (x : t) x) (Unv 0)))) (term (Unv 0)))
(check-equal? (term (reduce ((Π (x : t) x) Type))) (term Type)) (check-equal? (term (reduce ((Π (x : t) x) (Unv 0)))) (term (Unv 0)))
;; NB: Currently not reducing under binders. I forget why. ;; NB: Currently not reducing under binders. I forget why.
(check-equal? (term (reduce (Π (x : t) ((Π (x_0 : t) x_0) Type)))) (check-equal? (term (reduce (Π (x : t) ((Π (x_0 : t) x_0) (Unv 0)))))
(term (Π (x : t) Type))) (term (Π (x : t) (Unv 0))))
(check-equal? (term (reduce (Π (x : t) ((Π (x_0 : t) x_0) x)))) (check-equal? (term (reduce (Π (x : t) ((Π (x_0 : t) x_0) x))))
(term (Π (x : t) x))) (term (Π (x : t) x)))
(check-equal? (term (reduce (case (s z) (z (s z)) (s (λ (x : nat) (check-equal? (term (reduce (case (s z) (z (s z)) (s (λ (x : nat)
@ -186,12 +181,12 @@
(define Γ? (redex-match? cic-typingL Γ)) (define Γ? (redex-match? cic-typingL Γ))
(module+ test (module+ test
;; TODO: Rename these signatures, and use them in all future tests. ;; 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 Σ0 (term ∅))
(define Σ2 (term (((∅ nat : Type) z : nat) s : (Π (x : nat) nat)))) (define Σ2 (term (((∅ nat : (Unv 0)) z : nat) s : (Π (x : nat) nat))))
(define Σ3 (term (∅ and : (Π (A : Type) (Π (B : Type) Type))))) (define Σ3 (term (∅ and : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0))))))
(define Σ4 (term (,Σ3 conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B) ((and A) B)))))))) (define Σ4 (term (,Σ3 conj : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B))))))))
(check-true (Σ? Σ0)) (check-true (Σ? Σ0))
(check-true (Σ? Σ2)) (check-true (Σ? Σ2))
@ -242,14 +237,14 @@
(constructor-for (Σ x_0 : t_0) t_1 x)]) (constructor-for (Σ x_0 : t_0) t_1 x)])
(module+ test (module+ test
(check-true (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 (check-true
(judgment-holds (judgment-holds
(constructor-for ((∅ nat : Type) zero : nat) (constructor-for ((∅ nat : (Unv 0)) zero : nat)
nat zero))) nat zero)))
(check set=? (check set=?
(judgment-holds (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) nat x) x)
(list (term zero) (term s)))) (list (term zero) (term s))))
(define-metafunction cic-typingL (define-metafunction cic-typingL
@ -260,10 +255,10 @@
(judgment-holds (constructor-for Σ x_0 x_00) x_00))]) (judgment-holds (constructor-for Σ x_0 x_00) x_00))])
(module+ test (module+ test
(check-true (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)))) nat (zero s))))
(check-false (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)))) nat (zero))))
(check-true (check-true
(term (constructors-for ,Σ4 and (conj))))) (term (constructors-for ,Σ4 and (conj)))))
@ -275,13 +270,13 @@
;[(branch-type t_ind t_ind t) t]) ;[(branch-type t_ind t_ind t) t])
[(branch-type t_ind t_other t) t]) [(branch-type t_ind t_other t) t])
(module+ test (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 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? (check-equal?
(term Type) (term (Unv 0))
(term (branch-type and (lookup ,Σ4 conj) (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 (define-metafunction cic-typingL
branch-types-match : Σ (x ...) (t ...) t t -> #t or #f 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) ...)))]) ,(andmap (curry equal? (term t)) (term ((branch-type t_1 (lookup Σ x) t_11) ...)))])
(module+ test (module+ test
(check-true (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 (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 (check-true
(term (branch-types-match ,Σ (zero s) (nat (Π (x : nat) nat)) nat nat)))) (term (branch-types-match ,Σ (zero s) (nat (Π (x : nat) nat)) nat nat))))
;; TODO: Add positivity checking. ;; TODO: Add positivity checking.
(define-metafunction cicL (define-metafunction cicL
positive : t any -> #t or #f positive : t any -> #t or #f
;; Type; not a inductive constructor ;; (Unv 0); not a inductive constructor
[(positive any_1 any_2) #t]) [(positive any_1 any_2) #t])
(module+ test (module+ test
(check-true (term (positive nat nat))) (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))) (check-true (term (positive (Π (x : nat) nat) nat)))
;; (nat -> nat) -> nat ;; (nat -> nat) -> nat
;; Not sure if this is actually supposed to pass ;; Not sure if this is actually supposed to pass
(check-false (term (positive (Π (x : (Π (y : nat) nat)) nat) nat))) (check-false (term (positive (Π (x : (Π (y : nat) nat)) nat) nat)))
;; (Type -> nat) -> nat ;; ((Unv 0) -> nat) -> nat
(check-true (term (positive (Π (x : (Π (y : Type) nat)) nat) nat))) (check-true (term (positive (Π (x : (Π (y : (Unv 0)) nat)) nat) nat)))
;; (((nat -> Type) -> nat) -> nat) ;; (((nat -> (Unv 0)) -> nat) -> nat)
(check-true (term (positive (Π (x : (Π (y : (Π (x : nat) Type)) nat)) nat) nat))) (check-true (term (positive (Π (x : (Π (y : (Π (x : nat) (Unv 0))) nat)) nat) nat)))
;; Not sure if this is actually supposed to pass ;; Not sure if this is actually supposed to pass
(check-false (term (positive (Π (x : (Π (y : (Π (x : nat) nat)) nat)) nat) nat))) (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 (define-judgment-form cic-typingL
#:mode (wf I I) #:mode (wf I I)
@ -336,19 +331,19 @@
(wf (Σ x : t) ∅)]) (wf (Σ x : t) ∅)])
(module+ test (module+ test
(check-true (judgment-holds (wf ∅ ∅))) (check-true (judgment-holds (wf ∅ ∅)))
(check-true (judgment-holds (wf (∅ truth : Type) ∅))) (check-true (judgment-holds (wf (∅ truth : (Unv 0)) ∅)))
(check-true (judgment-holds (wf ∅ (∅ x : Type)))) (check-true (judgment-holds (wf ∅ (∅ x : (Unv 0)))))
(check-true (judgment-holds (wf (∅ nat : Type) (∅ x : nat)))) (check-true (judgment-holds (wf (∅ nat : (Unv 0)) (∅ x : nat))))
(check-true (judgment-holds (wf (∅ nat : Type) (∅ x : (Π (x : nat) nat)))))) (check-true (judgment-holds (wf (∅ nat : (Unv 0)) (∅ x : (Π (x : nat) nat))))))
;; TODO: Add termination checking ;; TODO: Add termination checking
(define-metafunction cicL (define-metafunction cicL
terminates? : t -> #t or #f terminates? : t -> #t or #f
[(terminates? t) #t]) [(terminates? t) #t])
(module+ test (module+ test
(check-false (term (terminates? (μ (x : Type) x)))) (check-false (term (terminates? (μ (x : (Unv 0)) x))))
(check-false (term (terminates? (μ (x : Type) (λ (y : Type) (x y)))))) (check-false (term (terminates? (μ (x : (Unv 0)) (λ (y : (Unv 0)) (x y))))))
(check-true (term (terminates? (μ (x : Type) (λ (y : Type) y)))))) (check-true (term (terminates? (μ (x : (Unv 0)) (λ (y : (Unv 0)) y))))))
(define-judgment-form cic-typingL (define-judgment-form cic-typingL
#:mode (types I I I O) #:mode (types I I I O)
@ -424,64 +419,64 @@
----------------- "DTR-Conversion" ----------------- "DTR-Conversion"
(types Γ e t_1)]) (types Γ e t_1)])
(module+ test (module+ test
(check-true (judgment-holds (types ∅ ∅ Type (Unv 0)))) (check-true (judgment-holds (types ∅ ∅ (Unv 0) (Unv 1))))
(check-true (judgment-holds (types ∅ (∅ x : Type) Type (Unv 0)))) (check-true (judgment-holds (types ∅ (∅ x : (Unv 0)) (Unv 0) (Unv 1))))
(check-true (judgment-holds (types ∅ (∅ x : Type) x Type))) (check-true (judgment-holds (types ∅ (∅ x : (Unv 0)) x (Unv 0))))
(check-true (judgment-holds (types ∅ ((∅ x_0 : Type) x_1 : Type) (check-true (judgment-holds (types ∅ ((∅ x_0 : (Unv 0)) x_1 : (Unv 0))
(Π (x_3 : x_0) x_1) Type))) (Π (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 : (Unv 0)) x_0 U_1)))
(check-true (judgment-holds (types ∅ ((∅ x_0 : Type) x_2 : x_0) Type U_2))) (check-true (judgment-holds (types ∅ ((∅ x_0 : (Unv 0)) x_2 : x_0) (Unv 0) U_2)))
(check-true (judgment-holds (unv-kind Type (Unv 0) (Unv 0)))) (check-true (judgment-holds (unv-kind (Unv 0) (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_2 : x_0) (Unv 0)) t)))
(check-true (judgment-holds (types ∅ ∅ (λ (x : Type) x) (Π (x : Type) Type)))) (check-true (judgment-holds (types ∅ ∅ (λ (x : (Unv 0)) x) (Π (x : (Unv 0)) (Unv 0)))))
(check-true (judgment-holds (types ∅ ∅ (λ (y : Type) (λ (x : y) x)) (check-true (judgment-holds (types ∅ ∅ (λ (y : (Unv 0)) (λ (x : y) x))
(Π (y : Type) (Π (x : y) y))))) (Π (y : (Unv 0)) (Π (x : y) y)))))
(check-equal? (list (term (Unv 0))) (check-equal? (list (term (Unv 1)))
(judgment-holds (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)
U)) U))
(check-true (check-true
(judgment-holds (judgment-holds
(types ∅ ∅ (Π (x2 : Type) (Unv 0)) (types ∅ ∅ (Π (x2 : (Unv 0)) (Unv 0))
U))) U)))
(check-true (check-true
(judgment-holds (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))) t)))
(check-true (check-true
(judgment-holds (types ((∅ truth : Type) T : truth) (judgment-holds (types ((∅ truth : (Unv 0)) T : truth)
∅ ∅
T T
truth))) truth)))
(check-true (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 (check-true
(judgment-holds (types ((∅ truth : Type) T : truth) (judgment-holds (types ((∅ truth : (Unv 0)) T : truth)
∅ ∅
(case T (T Type)) (case T (T (Unv 0)))
(Unv 0)))) (Unv 1))))
(check-false (check-false
(judgment-holds (types ((∅ truth : Type) T : truth) (judgment-holds (types ((∅ truth : (Unv 0)) T : truth)
∅ ∅
(case T (T Type) (T Type)) (case T (T (Unv 0)) (T (Unv 0)))
(Unv 0)))) (Unv 1))))
(define-syntax-rule (nat-test syn ...) (define-syntax-rule (nat-test syn ...)
(check-true (judgment-holds (check-true (judgment-holds
(types (((∅ nat : Type) zero : nat) s : (Π (x : nat) nat)) (types (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat))
syn ...)))) syn ...))))
(nat-test ∅ (Π (x : nat) nat) Type) (nat-test ∅ (Π (x : nat) nat) (Unv 0))
(nat-test ∅ (λ (x : nat) x) (Π (x : nat) nat)) (nat-test ∅ (λ (x : nat) x) (Π (x : nat) nat))
(nat-test ∅ (case zero (zero zero) (s (λ (x : nat) x))) (nat-test ∅ (case zero (zero zero) (s (λ (x : nat) x)))
nat) nat)
(nat-test ∅ nat Type) (nat-test ∅ nat (Unv 0))
(nat-test ∅ zero nat) (nat-test ∅ zero nat)
(nat-test ∅ s (Π (x : nat) nat)) (nat-test ∅ s (Π (x : nat) nat))
(nat-test ∅ (s zero) nat) (nat-test ∅ (s zero) nat)
@ -490,72 +485,72 @@
(nat-test ∅ (case zero (zero (s zero)) (s (λ (x : nat) (s (s x))))) (nat-test ∅ (case zero (zero (s zero)) (s (λ (x : nat) (s (s x)))))
nat) nat)
(check-false (judgment-holds (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))) (case zero (zero (s zero)))
nat))) nat)))
(define lam (term (λ (nat : Type) nat))) (define lam (term (λ (nat : (Unv 0)) nat)))
(check-equal? (check-equal?
(list (term (Π (nat : Type) Type))) (list (term (Π (nat : (Unv 0)) (Unv 0))))
(judgment-holds (types ,Σ0 ∅ ,lam t) t)) (judgment-holds (types ,Σ0 ∅ ,lam t) t))
(check-equal? (check-equal?
(list (term (Π (nat : Type) Type))) (list (term (Π (nat : (Unv 0)) (Unv 0))))
(judgment-holds (types ,Σ2 ∅ ,lam t) t)) (judgment-holds (types ,Σ2 ∅ ,lam t) t))
(check-equal? (check-equal?
(list (term (Π (x : (Π (y : Type) y)) nat))) (list (term (Π (x : (Π (y : (Unv 0)) y)) nat)))
(judgment-holds (types (∅ nat : Type) ∅ (λ (x : (Π (y : Type) y)) (x nat)) (judgment-holds (types (∅ nat : (Unv 0)) ∅ (λ (x : (Π (y : (Unv 0)) y)) (x nat))
t) t)) t) t))
(check-equal? (check-equal?
(list (term (Π (y : Type) Type))) (list (term (Π (y : (Unv 0)) (Unv 0))))
(judgment-holds (types (∅ nat : Type) ∅ (λ (y : Type) y) t) t)) (judgment-holds (types (∅ nat : (Unv 0)) ∅ (λ (y : (Unv 0)) y) t) t))
(check-equal? (check-equal?
(list (term Type)) (list (term (Unv 0)))
(judgment-holds (types (∅ nat : Type) ∅ (judgment-holds (types (∅ nat : (Unv 0)) ∅
((λ (x : (Π (y : Type) Type)) (x nat)) ((λ (x : (Π (y : (Unv 0)) (Unv 0))) (x nat))
(λ (y : Type) y)) (λ (y : (Unv 0)) y))
t) t)) t) t))
(check-equal? (check-equal?
(list (term Type)) (list (term (Unv 0)) (term (Unv 1)))
(judgment-holds (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)) U) U))
(check-true (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 (check-true
(judgment-holds (types ,Σ4 (∅ S : Type) S Type))) (judgment-holds (types ,Σ4 (∅ S : (Unv 0)) S (Unv 0))))
(check-true (check-true
(judgment-holds (types ,Σ4 (∅ S : Type) (conj S) (judgment-holds (types ,Σ4 (∅ S : (Unv 0)) (conj S)
(Π (B : Type) (Π (a : S) (Π (b : B) ((and S) B))))))) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))))
(check-true (check-true
(judgment-holds (types ,Σ4 (∅ S : Type) (conj S) (judgment-holds (types ,Σ4 (∅ S : (Unv 0)) (conj S)
(Π (B : Type) (Π (a : S) (Π (b : B) ((and S) B))))))) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))))
(check-true (check-true
(judgment-holds (types ,Σ4 ∅ (λ (S : Type) (conj S)) (judgment-holds (types ,Σ4 ∅ (λ (S : (Unv 0)) (conj S))
(Π (S : Type) (Π (B : Type) (Π (a : S) (Π (b : B) ((and S) B)))))))) (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))))))
(check-true (check-true
(judgment-holds (types ((,Σ4 true : Type) tt : true) ∅ (judgment-holds (types ((,Σ4 true : (Unv 0)) tt : true) ∅
((((conj true) true) tt) tt) ((((conj true) true) tt) tt)
((and true) true)))) ((and true) true))))
(check-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) (case ((((conj true) true) tt) tt)
(conj (λ (A : Type) (conj (λ (A : (Unv 0))
(λ (B : Type) (λ (B : (Unv 0))
(λ (a : A) (λ (a : A)
(λ (b : B) a)))))) (λ (b : B) a))))))
A))) A)))
(define sigma (term (((((((∅ true : Type) T : true) false : Type) equal : (Π (A : Type) (define sigma (term (((((((∅ true : (Unv 0)) T : true) false : (Unv 0)) equal : (Π (A : (Unv 0))
(Π (B : Type) Type))) (Π (B : (Unv 0)) (Unv 0))))
nat : Type) heap : Type) pre : (Π (temp808 : heap) Type)))) nat : (Unv 0)) heap : (Unv 0)) pre : (Π (temp808 : heap) (Unv 0)))))
(define gamma (term (∅ temp863 : pre))) (define gamma (term (∅ temp863 : pre)))
(check-true (judgment-holds (wf ,sigma ∅))) (check-true (judgment-holds (wf ,sigma ∅)))
(check-true (judgment-holds (wf ,sigma ,gamma))) (check-true (judgment-holds (wf ,sigma ,gamma)))
(check-true (check-true
(judgment-holds (types ,sigma ,gamma Type t))) (judgment-holds (types ,sigma ,gamma (Unv 0) t)))
(check-true (check-true
(judgment-holds (types ,sigma ,gamma pre t))) (judgment-holds (types ,sigma ,gamma pre t)))
(check-true (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 (check-true
(judgment-holds (types ,sigma (,gamma x : false) (case x) t))))) (judgment-holds (types ,sigma (,gamma x : false) (case x) t)))))
@ -606,8 +601,10 @@
[dep-case case] [dep-case case]
[dep-var #%top] [dep-var #%top]
; [dep-datum #%datum] ; [dep-datum #%datum]
[dep-define define]) [dep-define define])
Type
;; DYI syntax extension ;; DYI syntax extension
define-syntax define-syntax
begin-for-syntax begin-for-syntax
@ -695,11 +692,9 @@
;; Locally expand everything down to core forms. ;; Locally expand everything down to core forms.
(define (core-expand syn) (define (core-expand syn)
(disarm (disarm
(if (identifier? syn) (local-expand syn 'expression
syn
(local-expand syn 'expression
(append (syntax-e #'(term reduce subst-all dep-var #%app λ Π μ case (append (syntax-e #'(term reduce subst-all dep-var #%app λ Π μ case
Type))))))) Unv #%datum))))))
;; Only type-check at the top-level, to prevent exponential ;; Only type-check at the top-level, to prevent exponential
;; type-checking. Redex is expensive enough. ;; type-checking. Redex is expensive enough.
@ -715,11 +710,12 @@
(let cur->datum ([syn syn]) (let cur->datum ([syn syn])
(syntax-parse (core-expand syn) (syntax-parse (core-expand syn)
#:literals (term reduce #%app subst-all) #:literals (term reduce #%app subst-all)
#:datum-literals (case Π λ μ : Type) #:datum-literals (case Π λ μ : Unv)
[x:id (syntax->datum #'x)] [x:id (syntax->datum #'x)]
[(subst-all e _ _) (syntax->datum #'e)] [(subst-all e _ _) (syntax->datum #'e)]
[(reduce e) (cur->datum #'e)] [(reduce e) (cur->datum #'e)]
[(term 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 ;; TODO: should really check that b is one of the binders
;; Maybe make a syntax class for the binders, core forms, ;; Maybe make a syntax class for the binders, core forms,
;; etc. ;; etc.
@ -938,6 +934,11 @@
(syntax-case syn (:) (syntax-case syn (:)
[(_ (x : t) e) (syntax->curnel-syntax #`(Π (x : t) e))])) [(_ (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) (define-syntax (dep-fix syn)
(syntax-case syn (:) (syntax-case syn (:)
[(_ (x : t) e) (syntax->curnel-syntax #`(μ (x : t) e))])) [(_ (x : t) e) (syntax->curnel-syntax #`(μ (x : t) e))]))