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

Starting fixing uses of elim, but there is a bug

Browse Source
This commit is contained in:
William J. Bowman 2015-09-24 13:51:29 -04:00
parent e600c32b77
commit d82727a3fb
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
3 changed files with 19 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
stdlib/bool.rkt
View File

@ -9,9 +9,11 @@
(syntax-case syn () (syntax-case syn ()
[(_ t s f) [(_ t s f)
;; Compute the motive ;; Compute the motive
(let ([M #`(lambda (x : #,(type-infer/syn #'t)) (let* ([sty (type-infer/syn #'s)]
#,(type-infer/syn #'s))]) [M #`(lambda (x : #,(type-infer/syn #'t))
(quasisyntax/loc syn (elim bool t #,M s f)))])) #,sty)]
[U (type-infer/syn sty)])
(quasisyntax/loc syn (elim bool #,U #,M s f t)))]))
(define (bnot (x : bool)) (if x bfalse btrue)) (define (bnot (x : bool)) (if x bfalse btrue))
(module+ test (module+ test

21
stdlib/nat.rkt
View File

@ -15,14 +15,14 @@
(check-equal? (add1 (s z)) (s (s z)))) (check-equal? (add1 (s z)) (s (s z))))
(define (sub1 (n : nat)) (define (sub1 (n : nat))
(case* nat n (lambda (x : nat) nat) (case* nat Type n (lambda (x : nat) nat)
[z z] [z z]
[(s (x : nat)) IH: ((ih-n : nat)) x])) [(s (x : nat)) IH: ((ih-n : nat)) x]))
(module+ test (module+ test
(check-equal? (sub1 (s z)) z)) (check-equal? (sub1 (s z)) z))
(define (plus (n1 : nat) (n2 : nat)) (define (plus (n1 : nat) (n2 : nat))
(case* nat n1 (lambda (x : nat) nat) (case* nat Type n1 (lambda (x : nat) nat)
[z n2] [z n2]
[(s (x : nat)) IH: ((ih-n1 : nat)) [(s (x : nat)) IH: ((ih-n1 : nat))
(s ih-n1)])) (s ih-n1)]))
@ -32,17 +32,20 @@
;; Credit to this function goes to Max ;; Credit to this function goes to Max
(define (nat-equal? (n1 : nat)) (define (nat-equal? (n1 : nat))
(elim nat n1 (lambda (x : nat) (-> nat bool)) (elim nat Type (lambda (x : nat) (-> nat bool))
(lambda (n2 : nat) (lambda (b2 : nat)
(elim nat n2 (lambda (x : nat) bool) (elim nat Type (lambda (x : nat) bool)
btrue btrue
(lambda* (x : nat) (ih-n2 : bool) bfalse))) (lambda* (x : nat) (ih-n2 : bool) bfalse)
b2))
(lambda* (x : nat) (ih : (-> nat bool)) (lambda* (x : nat) (ih : (-> nat bool))
(lambda (n2 : nat) (lambda (a2 : nat)
(elim nat n2 (lambda (x : nat) bool) (elim nat Type (lambda (x : nat) bool)
bfalse bfalse
(lambda* (x : nat) (ih-bla : bool) (lambda* (x : nat) (ih-bla : bool)
(ih x))))))) (ih x))
a2)))
n1))
(module+ test (module+ test
(check-equal? (nat-equal? z z) btrue) (check-equal? (nat-equal? z z) btrue)
(check-equal? (nat-equal? z (s z)) bfalse) (check-equal? (nat-equal? z (s z)) bfalse)

4
stdlib/sugar.rkt
View File

@ -78,8 +78,8 @@
;; TODO: inductive D is defined. ;; TODO: inductive D is defined.
(define-syntax (case* syn) (define-syntax (case* syn)
(syntax-case syn () (syntax-case syn ()
[(_ D e P clause* ...) [(_ D U e P clause* ...)
#`(elim D e P #,@(map rewrite-clause (syntax->list #'(clause* ...))))])) #`(elim D U P #,@(map rewrite-clause (syntax->list #'(clause* ...))) e)]))
(define-syntax-rule (define-theorem name prop) (define-syntax-rule (define-theorem name prop)
(define name prop)) (define name prop))