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

Bug fixes

Browse Source
This commit is contained in:
William J. Bowman 2015-02-15 21:25:39 -05:00
parent 410ee11cbe
commit b2afc8f9d9
2 changed files with 9 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
proofs-for-free.rkt
View File

@ -27,7 +27,7 @@
(syntax-parse (cur-expand syn)
;; TODO: Need to add these to a literal set and export it
;; Or, maybe redefine syntax-parse
#:dataum-literals (:)
#:datum-literals (:)
#:literals (lambda forall data real-app case Type)
[(_ Type)
#'(lambda* (x1 : Type) (x2 : Type) (->* x1 x2 Type))]
@ -73,7 +73,7 @@
(define (CPSf-relation (f1 : CPSf) (f2 : CPSf))
;; Run performs substitution, among other things, at compile.
(translate (run CPSf))
(translate (run CPSf)))
(module+ test
(require rackunit)
(check-equal?
@ -82,7 +82,7 @@
(forall* (k1 : (-> X ans1)) (k2 : (-> X ans2))
(kr : (forall* (_1 : X) (_2 : X) (_r : (Xr _1 _2))
(ansr (k1 _1) (k2 _2))))
(ansr (f1 ans1 k1) (f2 ans2 k2)))))))
(ansr (f1 ans1 k1) (f2 ans2 k2))))))
;; By parametricity, every CPSf is related it itself in the CPS relation
(define-type paramCPSf (forall* (f : CPSf) (CPSf-relation f f)))

8
stdlib/sugar.rkt
View File

@ -49,8 +49,12 @@
[(_ e1 e2 e3 ...)
#'(#%app (#%app e1 e2) e3 ...)]))
(define-syntax-rule (define-type (name (a : t) ...) body)
(define name (forall* (a : t) ... body)))
(define-syntax define-type
(syntax-rules ()
[(_ (name (a : t) ...) body)
(define name (forall* (a : t) ... body))]
[(_ name type)
(define name type)]))
(define-syntax (define syn)
(syntax-case syn ()