diff --git a/tapl/exist.rkt b/tapl/exist.rkt index e3c51eb..8d0d6a2 100644 --- a/tapl/exist.rkt +++ b/tapl/exist.rkt @@ -1,5 +1,4 @@ -#lang racket/base -(require "typecheck.rkt") +#lang s-exp "typecheck.rkt" (require (except-in "stlc+reco+var.rkt" #%app λ let) (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app λ let)) (only-in "stlc+rec-iso.rkt")) ; to get current-type=? diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt index 8ef4986..ddd0888 100644 --- a/tapl/ext-stlc.rkt +++ b/tapl/ext-stlc.rkt @@ -1,5 +1,4 @@ -#lang racket/base -(require "typecheck.rkt") +#lang s-exp "typecheck.rkt" ;; prefix-in an identifier if: ;; - it will be extended, eg #%datum ;; - want to use racket's version in implemetation (this) file, eg #%app diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt index b2d0a08..b814f90 100644 --- a/tapl/fomega.rkt +++ b/tapl/fomega.rkt @@ -1,5 +1,4 @@ -#lang racket/base -(require "typecheck.rkt") +#lang s-exp "typecheck.rkt" (require (except-in "sysf.rkt" #%app λ #%datum Λ inst ∀) (rename-in (prefix-in sysf: (only-in "sysf.rkt" #%app λ ∀ ~∀)) [sysf:~∀ ~sysf:∀]) diff --git a/tapl/fomega2.rkt b/tapl/fomega2.rkt index ff0b3f5..6552499 100644 --- a/tapl/fomega2.rkt +++ b/tapl/fomega2.rkt @@ -1,5 +1,4 @@ -#lang racket/base -(require "typecheck.rkt") +#lang s-exp "typecheck.rkt" (require (except-in "sysf.rkt" #%app λ #%datum Λ inst ∀) (rename-in (prefix-in sysf: (only-in "sysf.rkt" #%app λ ∀ ~∀)) [sysf:~∀ ~sysf:∀]) diff --git a/tapl/fsub.rkt b/tapl/fsub.rkt index 995b8ac..5a70d2a 100644 --- a/tapl/fsub.rkt +++ b/tapl/fsub.rkt @@ -1,5 +1,4 @@ -#lang racket/base -(require "typecheck.rkt") +#lang s-exp "typecheck.rkt" (require (except-in "stlc+reco+sub.rkt" #%app λ +) (prefix-in stlc: (only-in "stlc+reco+sub.rkt" #%app λ)) (only-in "sysf.rkt" ∀?) diff --git a/tapl/stlc+box.rkt b/tapl/stlc+box.rkt index a84512d..46dc8fb 100644 --- a/tapl/stlc+box.rkt +++ b/tapl/stlc+box.rkt @@ -1,5 +1,4 @@ -#lang racket/base -(require "typecheck.rkt") +#lang s-exp "typecheck.rkt" (require (prefix-in stlc: (only-in "stlc+cons.rkt" #%app)) (except-in "stlc+cons.rkt" #%app)) (provide (rename-out [stlc:#%app #%app])) diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt index 39458c3..54fe74d 100644 --- a/tapl/stlc+cons.rkt +++ b/tapl/stlc+cons.rkt @@ -1,5 +1,4 @@ -#lang racket/base -(require "typecheck.rkt") +#lang s-exp "typecheck.rkt" (require (prefix-in stlc: (only-in "stlc+reco+var.rkt" #%app)) (except-in "stlc+reco+var.rkt" #%app)) (provide (rename-out [stlc:#%app #%app] [cons/tc cons])) diff --git a/tapl/stlc+lit.rkt b/tapl/stlc+lit.rkt index 6041fa4..d574e4f 100644 --- a/tapl/stlc+lit.rkt +++ b/tapl/stlc+lit.rkt @@ -1,5 +1,4 @@ -#lang racket/base -(require "typecheck.rkt") +#lang s-exp "typecheck.rkt" ;(extends "stlc.rkt" #:impl-uses (→)) (require (except-in "stlc.rkt" #%app) (prefix-in stlc: (only-in "stlc.rkt" #%app))) diff --git a/tapl/stlc+rec-iso.rkt b/tapl/stlc+rec-iso.rkt index c32717e..2ba483c 100644 --- a/tapl/stlc+rec-iso.rkt +++ b/tapl/stlc+rec-iso.rkt @@ -1,5 +1,4 @@ -#lang racket/base -(require "typecheck.rkt") +#lang s-exp "typecheck.rkt" (require (except-in "stlc+tup.rkt" #%app λ) ; import tuples, not records (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ)) (only-in "stlc+reco+var.rkt" ∨ var case define-type-alias define)) ; and variants diff --git a/tapl/stlc+reco+sub.rkt b/tapl/stlc+reco+sub.rkt index 9f52ed3..9aa79cd 100644 --- a/tapl/stlc+reco+sub.rkt +++ b/tapl/stlc+reco+sub.rkt @@ -1,5 +1,4 @@ -#lang racket/base -(require "typecheck.rkt") +#lang s-exp "typecheck.rkt" ;;use type=? and eval-type from stlc+reco+var.rkt, not stlc+sub.rkt ;; but extend sub? from stlc+sub.rkt (require (except-in "stlc+sub.rkt" #%app #%datum) diff --git a/tapl/stlc+reco+var.rkt b/tapl/stlc+reco+var.rkt index 5050cc5..8415d3c 100644 --- a/tapl/stlc+reco+var.rkt +++ b/tapl/stlc+reco+var.rkt @@ -1,5 +1,4 @@ -#lang racket/base -(require "typecheck.rkt") +#lang s-exp "typecheck.rkt" (require (only-in racket/bool symbol=?)) (require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app begin let × ×?)) (except-in "stlc+tup.rkt" #%app begin tup proj let ×) @@ -40,6 +39,15 @@ [(_ alias:id τ:type) #'(define-syntax alias (syntax-parser [x:id #'τ.norm]))])) +(define-syntax (define/tc stx) + (syntax-parse stx + [(_ x:id e) + #:with (e- τ) (infer+erase #'e) + #:with y (generate-temporary) + #'(begin + (define-syntax x (make-rename-transformer (⊢ y : τ))) + (define y e-))])) + ; re-define tuples as records ; dont use define-type-constructor because I want the : literal syntax (define-syntax × @@ -138,12 +146,3 @@ (⊢ (let ([l_e (car e-)]) (cond [(symbol=? l_e 'l) (let ([x- (cadr e-)]) e_l-)] ...)) : #,(stx-car #'(τ_el ...)))])) - -(define-syntax (define/tc stx) - (syntax-parse stx - [(_ x:id e) - #:with (e- τ) (infer+erase #'e) - #:with y (generate-temporary) - #'(begin - (define-syntax x (make-rename-transformer (⊢ y : τ))) - (define y e-))])) \ No newline at end of file diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt index a457874..620bdd7 100644 --- a/tapl/stlc+sub.rkt +++ b/tapl/stlc+sub.rkt @@ -1,5 +1,4 @@ -#lang racket/base -(require "typecheck.rkt") +#lang s-exp "typecheck.rkt" (require (except-in "stlc+lit.rkt" #%datum + #%app) (prefix-in stlc: (only-in "stlc+lit.rkt" #%app #%datum))) (provide (rename-out [stlc:#%app #%app] [datum/tc #%datum])) diff --git a/tapl/stlc+tup.rkt b/tapl/stlc+tup.rkt index 4785419..2693cb7 100644 --- a/tapl/stlc+tup.rkt +++ b/tapl/stlc+tup.rkt @@ -1,5 +1,4 @@ -#lang racket/base -(require "typecheck.rkt") +#lang s-exp "typecheck.rkt" (require (prefix-in stlc: (only-in "ext-stlc.rkt" #%app)) (except-in "ext-stlc.rkt" #%app)) (provide (rename-out [stlc:#%app #%app]) diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt index bed5fe7..4312c1c 100644 --- a/tapl/stlc.rkt +++ b/tapl/stlc.rkt @@ -1,5 +1,4 @@ -#lang racket/base -(require "typecheck.rkt") +#lang s-exp "typecheck.rkt" (provide (rename-out [λ/tc λ] [app/tc #%app])) (provide (for-syntax current-type=? types=?)) (provide #%module-begin #%top-interaction #%top require) ; useful racket forms diff --git a/tapl/sysf.rkt b/tapl/sysf.rkt index 4ce13a9..ab86a99 100644 --- a/tapl/sysf.rkt +++ b/tapl/sysf.rkt @@ -1,5 +1,4 @@ -#lang racket/base -(require "typecheck.rkt") +#lang s-exp "typecheck.rkt" (require (except-in "stlc+lit.rkt" #%app λ) (prefix-in stlc: (only-in "stlc+lit.rkt" #%app λ)) (only-in "stlc+rec-iso.rkt")) ; want type=? from here diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt index bea2c16..4a940dc 100644 --- a/tapl/typecheck.rkt +++ b/tapl/typecheck.rkt @@ -7,7 +7,8 @@ (for-meta 2 racket/base syntax/parse racket/syntax syntax/stx "stx-utils.rkt") (for-meta 3 racket/base syntax/parse racket/syntax) racket/provide) -(provide +(provide + (all-from-out racket/base) (for-syntax (all-defined-out)) (all-defined-out) (for-syntax (all-from-out racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt"))