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

Merge branch 'master' into actual-inductives

Browse Source 
Conflicts:
	redex-curnel.rkt
This commit is contained in:
William J. Bowman 2015-03-23 17:37:04 -04:00
commit 8a5bff1aec
6 changed files with 180 additions and 214 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
README.md
View File

@ -16,7 +16,8 @@ cur (plural curs)
Getting started 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. or worse.
Open up `stlc.rkt` to see an example of what advanced meta-programming can let you do. Open up `stlc.rkt` to see an example of what advanced meta-programming can let you do.

10
oll.rkt
View File

@ -54,10 +54,11 @@
(with-output-to-file (syntax->datum #'latex-file) (with-output-to-file (syntax->datum #'latex-file)
(thunk (thunk
(format "\\fbox{$~a$}$~n$\\begin{mathpar}~n~a~n\end{mathpar}$$" (format "\\fbox{$~a$}$~n$\\begin{mathpar}~n~a~n\end{mathpar}$$"
(syntax->datum #'(n types* ...))
(string-trim (string-trim
(for/fold ([str ""]) (for/fold ([str ""])
([rule (syntax->datum #'(rules.latex ...))]) ([rule (attribute rules.latex)])
(format "~a~a\\and~n" rule)) (format "~a~a\\and~n" str rule))
"\\and" "\\and"
#:left? #f))) #:left? #f)))
#:exists 'append)) #:exists 'append))
@ -263,7 +264,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 ...))])
@ -311,7 +312,7 @@
(begin (begin
(coq-lift-top-level (coq-lift-top-level
(format "Inductive ~a : ~a :=~a." (format "Inductive ~a : ~a :=~a."
(syntax-e #'n) (sanitize-id (format "~a" (syntax-e #'n)))
(output-coq #'t) (output-coq #'t)
(for/fold ([strs ""]) (for/fold ([strs ""])
([clause (syntax->list #'((x* : t*) ...))]) ([clause (syntax->list #'((x* : t*) ...))])
@ -320,6 +321,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)

64
proofs-for-free.rkt
View File

@ -1,5 +1,6 @@
#lang s-exp "redex-curnel.rkt" #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 (begin-for-syntax
@ -7,40 +8,42 @@
(format-id x "~a~a" x i))) (format-id x "~a~a" x i)))
(define-syntax (rename syn) (define-syntax (rename syn)
(syntax-case syn (Type forall Unv lambda :) (syntax-case syn ()
[(_ i ls Type) #'Type] [(_ i ls e)
[(_ i ls (Unv n)) #'(Unv n)] (syntax-case #`(ls #,(cur-expand #'e)) (Type forall Unv lambda :)
[(_ i (xr ...) (lambda (x : t) e)) [(_ Type) #'Type]
#'(lambda (x : (rename i (xr ...) t)) [(_ (Unv n)) #'(Unv n)]
(rename i (xr ... x) e))] [((xr ...) (lambda (x : t) e))
[(_ i (xr ...) (forall (x : t) e)) #'(lambda (x : (rename i (xr ...) t))
#'(forall (x : (rename i (xr ...) t)) (rename i (xr ... x) e))]
(rename i (xr ... x) e))] [((xr ...) (forall (x : t) e))
[(_ i ls (e1 e2)) #'(forall (x : (rename i (xr ...) t))
#'((rename i ls e1) (rename i ls e2))] (rename i (xr ... x) e))]
[(_ i ls x) [(ls (e1 e2))
(if (member (syntax->datum #'x) (syntax->datum #'ls)) #'((rename i ls e1) (rename i ls e2))]
#'x [(ls x)
(rename_id (syntax->datum #'i) #'x))])) (if (member (syntax->datum #'x) (syntax->datum #'ls))
#'x
(rename_id (syntax->datum #'i) #'x))])]))
(define-syntax (translate syn) (trace-define-syntax (translate syn)
(syntax-parse (cur-expand syn) (syntax-parse (cur-expand (syntax-case syn () [(_ e) #'e]))
;; 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 redefine syntax-parse ;; Or, maybe redefine syntax-parse
#:datum-literals (:) #:datum-literals (:)
#:literals (lambda forall data real-app case Type) #:literals (lambda forall data real-app case Type)
[(_ Type) [Type
#'(lambda* (x1 : Type) (x2 : Type) (->* x1 x2 Type))] #'(lambda* (x1 : Type) (x2 : Type) (->* x1 x2 Type))]
[(_ (forall (x : A) B)) [(forall (x : A) B)
(let ([x1 (rename_id 1 #'x)] (let ([x1 (rename_id 1 #'x)]
[x2 (rename_id 2 #'x)] [x2 (rename_id 2 #'x)]
[xr (rename_id 'r #'x)]) [xr (rename_id 'r #'x)])
#`(lambda* (f1 : (rename 1 () (forall (x : A) B))) #`(lambda* (f1 : (rename 1 () (forall (x : A) B)))
(f2 : (rename 2 () (forall (x : A) B))) (f2 : (rename 2 () (forall (x : A) B)))
(forall* (#,x1 : (rename 1 () A)) (#,x2 : (rename 2 () A)) (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)))))] ((translate B) (f1 #,x1) (f2 #,x2)))))]
[(_ (lambda (x : A) B)) [(lambda (x : A) B)
(let ([x1 (rename_id 1 #'x)] (let ([x1 (rename_id 1 #'x)]
[x2 (rename_id 2 #'x)] [x2 (rename_id 2 #'x)]
[xr (rename_id 'r #'x)]) [xr (rename_id 'r #'x)])
@ -48,15 +51,15 @@
(f2 : (rename 2 () (forall (x : A) B))) (f2 : (rename 2 () (forall (x : A) B)))
(forall* (#,x1 : (rename 1 () A)) (forall* (#,x1 : (rename 1 () A))
(#,x2 : (rename 2 () A)) (#,x2 : (rename 2 () A))
(#,xr : ((translate A) #,x1 #,x2)) (#,xr : (run ((translate A) #,x1 #,x2)))
((translate B) (f1 #,x1) (f2 #,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) (let ([t #`(data #,(rename_id 'r #'id) : (translate t)
((translate c) : (translate tc)) ...)]) ((translate c) : (translate tc)) ...)])
t)] t)]
[(_ (f a)) [(f a)
#`((translate f) (rename 1 () a) (rename 2 () a) (translate 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 ;; TODO: Look up x and generate the relation. Otherwise I need to
;; manually translate all dependencies. ;; manually translate all dependencies.
;; Not sure this is quite right; Racket's hygiene might `save' me. ;; Not sure this is quite right; Racket's hygiene might `save' me.
@ -66,15 +69,16 @@
(define-type X Type) (define-type X Type)
(define X1 X) (define X1 X)
(define X2 X) (define X2 X)
(define (Xr (x1 : X) (x2 : X)) true) (define (Xr (x1 : X1) (x2 : X2)) true)
;; The type of a CPS function ;; The type of a CPS function
(define-type CPSf (forall* (ans : Type) (k : (-> X ans)) ans)) (define-type CPSf (forall* (ans : Type) (k : (-> X ans)) ans))
(define (CPSf-relation (f1 : CPSf) (f2 : CPSf)) (define (CPSf-relation (f1 : CPSf) (f2 : CPSf))
;; Run performs substitution, among other things, at compile. ;; TODO: Fix run so I can simply use (run CPSf) to perform
(translate (run CPSf))) ;; substitution
(module+ test (translate (forall* (ans : Type) (k : (-> X ans)) ans)))
#;(module+ test
(require rackunit) (require rackunit)
(check-equal? (check-equal?
(translate (forall* (ans : Type) (k : (-> X ans)) ans)) (translate (forall* (ans : Type) (k : (-> X ans)) ans))

300
redex-curnel.rkt
View File

@ -9,6 +9,8 @@
(provide (provide
(all-defined-out)) (all-defined-out))
(set-cache-size! 10000)
;; References: ;; References:
;; http://www3.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf ;; http://www3.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf
;; https://www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf ;; https://www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf
@ -18,7 +20,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 +40,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,17 +49,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 ;; (Unv 0)s of 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)
;; TODO: Type should be an alias for (Unv 0) I think, instead of a
;; built-in thing, and defined via a macro.
[-----------------
(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))])
@ -71,13 +66,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)))
---------------- ----------------
@ -140,12 +135,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)))
;; TODO: Change uses of case to uses of elim-nat ;; TODO: Change uses of case to uses of elim-nat
@ -171,7 +166,7 @@
(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.
;; TODO: Convert these to new Σ format ;; TODO: Convert these to new Σ format
(define Σ (term (∅ (nat : Type ((zero : nat) (s : (Π (x : nat) nat))) (define Σ (term (∅ (nat : (Unv 0) ((zero : nat) (s : (Π (x : nat) nat)))
(elim-nat : (Π (P : (Π (n : nat) (Unv i))) (elim-nat : (Π (P : (Π (n : nat) (Unv i)))
(Π (mz : (P zero)) (Π (mz : (P zero))
(Π (ms : (Π (n : nat) (Π (p : (P n)) (P (s n))))) (Π (ms : (Π (n : nat) (Π (p : (P n)) (P (s n)))))
@ -215,26 +210,25 @@
(define Σ0 (term ∅)) (define Σ0 (term ∅))
(define Σ2 Σ) (define Σ2 Σ)
(define Σ3 (term (∅ (and : (Π (A : Type) (Π (B : Type) Type)) () (define Σ3 (term (∅ (and : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0))) ()
(elim-and : (Π (A : Type) (Π (B : Type) (elim-and : (Π (A : (Unv 0)) (Π (B : (Unv 0))
(Π (P : (Π (p : ((and A) B)) (Unv i))) (Π (P : (Π (p : ((and A) B)) (Unv i)))
(Π (p : ((and A) B)) (Π (p : ((and A) B))
(P p)))))))))) (P p))))))))))
(define Σ4 (term (∅ (and : (Π (A : Type) (Π (B : Type) Type)) (define Σ4 (term (∅ (and : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
((conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B) ((and A) B))))))) ((conj : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B)))))))
(elim-and : (Π (P : (Π (A : Type) (Π (B : Type) (Π (p : ((and A) B)) (Unv i))))) (elim-and : (Π (P : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (p : ((and A) B)) (Unv i)))))
(Π (Π
(mconj : (mconj :
(Π (A : Type) (Π (A : (Unv 0))
(Π (B : Type) (Π (B : (Unv 0))
(Π (a : A) (Π (a : A)
(Π (b : B) (Π (b : B)
(P A B ((((conj A) B) a) b)))))) (P A B ((((conj A) B) a) b))))))
(Π (A : Type) (Π (A : (Unv 0))
(Π (B : Type) (Π (B : (Unv 0))
(Π (p : ((and A) B)) (Π (p : ((and A) B))
(P A B p)))))))))))) (P A B p))))))))))))
(check-true (Σ? Σ0)) (check-true (Σ? Σ0))
(check-true (Σ? Σ2)) (check-true (Σ? Σ2))
(check-true (Σ? Σ4)) (check-true (Σ? Σ4))
@ -284,14 +278,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
@ -302,10 +296,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)))))
@ -317,13 +311,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
@ -331,33 +325,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)
@ -378,19 +372,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)
@ -405,6 +399,7 @@
----------------- "DTR-Inductive" ----------------- "DTR-Inductive"
(types Σ Γ x t)] (types Σ Γ x t)]
;; TODO: Require alpha-equiv here, at least.
[(where t (lookup Γ x)) [(where t (lookup Γ x))
----------------- "DTR-Start" ----------------- "DTR-Start"
(types Σ Γ x t)] (types Σ Γ x t)]
@ -449,72 +444,72 @@
;; searches it. ;; searches it.
;; Perhaps something closer to Zombies = type would be better. ;; Perhaps something closer to Zombies = type would be better.
;; For now, reduce types ;; 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_0 (in-hole E t))
(where t_1 ,(car (apply-reduction-relation* ==β (term t_0)))) (where t_1 ,(car (apply-reduction-relation* ==β (term t_0))))
(types Γ t_1 U) (types Σ Γ t_1 U)
----------------- "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))))
;; TODO: Change uses of case to uses of elim- ;; TODO: Change uses of case to uses of elim-
(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)
@ -523,121 +518,74 @@
(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)))))
)
(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)]) )
;; This module just provide module language sugar over the redex model. ;; This module just provide module language sugar over the redex model.
@ -683,8 +631,10 @@
[dep-inductive data] [dep-inductive data]
[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
@ -772,11 +722,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 (append (syntax-e #'(term reduce subst-all dep-var #%app λ Π μ case
(local-expand syn 'expression Unv #%datum))))))
(append (syntax-e #'(term reduce subst-all dep-var #%app λ Π
Type)))))))
;; 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.
@ -792,11 +740,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 (Π λ : 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.
@ -840,6 +789,8 @@
dep-forall dep-var)) dep-forall dep-var))
ls))))) 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) (define-syntax (run syn)
(syntax-case syn () (syntax-case syn ()
[(_ expr) (normalize/syn #'expr)])) [(_ expr) (normalize/syn #'expr)]))
@ -1006,6 +957,15 @@
(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)
(syntax-case syn (:)
[(_ (x : t) e) (syntax->curnel-syntax #`(μ (x : t) e))]))
(define-syntax (dep-inductive syn) (define-syntax (dep-inductive syn)
(syntax-case syn (:) (syntax-case syn (:)
[(_ i : ti (x1 : t1) ...) [(_ i : ti (x1 : t1) ...)

4
stdlib/sugar.rkt
View File

@ -18,9 +18,7 @@
(define-syntax (-> syn) (define-syntax (-> syn)
(syntax-case syn () (syntax-case syn ()
[(_ t1 t2) [(_ t1 t2) #`(forall (#,(gensym) : t1) t2)]))
(with-syntax ([(x) (generate-temporaries '(1))])
#`(forall (x : t1) t2))]))
(define-syntax ->* (define-syntax ->*
(syntax-rules () (syntax-rules ()

13
stlc.rkt
View File

@ -15,17 +15,16 @@
;; TODO: Abstract this over stlc-type, and provide from in OLL ;; TODO: Abstract this over stlc-type, and provide from in OLL
(data gamma : Type (data gamma : Type
(emp-gamma : gamma) (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)) (define-rec (lookup-gamma (g : gamma) (x : var) : (maybe stlc-type))
(case* g (case* g
[emp-gamma (none stlc-type)] [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) (if (var-equal? v1 x)
(some stlc-type t1) (some stlc-type t1)
(lookup-gamma g1 x))])) (lookup-gamma g1 x))]))
(define-relation (has-type gamma stlc-term stlc-type) (define-relation (has-type gamma stlc-term stlc-type)
#:output-coq "stlc.v" #:output-coq "stlc.v"
#:output-latex "stlc.tex" #:output-latex "stlc.tex"
@ -41,7 +40,7 @@
------------------------ T-False ------------------------ T-False
(has-type g (stlc-val-->-stlc-term stlc-false) stlc-boolty)] (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)) (== (maybe stlc-type) (lookup-gamma g x) (some stlc-type t))
------------------------ T-Var ------------------------ T-Var
(has-type g (var-->-stlc-term x) t)] (has-type g (var-->-stlc-term x) t)]
@ -55,9 +54,11 @@
[(g : gamma) (e1 : stlc-term) (e2 : stlc-term) [(g : gamma) (e1 : stlc-term) (e2 : stlc-term)
(t1 : stlc-type) (t2 : stlc-type) (t1 : stlc-type) (t2 : stlc-type)
(t : stlc-type)
(x : var) (y : var)
(has-type g e1 (stlc-* t1 t2)) (has-type g e1 (stlc-* t1 t2))
(has-type (extend-gamma (extend-gamma g x t1) t y2) e2 t) (has-type (extend-gamma (extend-gamma g x t1) y t2) e2 t)
---------------------- T-Pair ---------------------- T-Let
(has-type g (stlc-let x y e1 e2) t)] (has-type g (stlc-let x y e1 e2) t)]
[(g : gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : var) [(g : gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : var)