diff --git a/proofs-for-free.rkt b/proofs-for-free.rkt index 849ddf8..9815121 100644 --- a/proofs-for-free.rkt +++ b/proofs-for-free.rkt @@ -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))) diff --git a/stdlib/sugar.rkt b/stdlib/sugar.rkt index a407158..8a5affb 100644 --- a/stdlib/sugar.rkt +++ b/stdlib/sugar.rkt @@ -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 ()