commit 3385805f0647798b43f1695632703f67b6e789eb
parent 7b422d9a389f06b010805fa6f3abc3518ac0fa48
Author: AlexKnauth <alexander@knauth.org>
Date: Mon, 20 Jun 2016 14:22:48 -0400
use λ- etc. for untyped forms, λ etc. for typed
Diffstat:
22 files changed, 436 insertions(+), 428 deletions(-)
diff --git a/tapl/exist.rkt b/tapl/exist.rkt
@@ -15,14 +15,14 @@
(define-type-constructor ∃ #:bvs = 1)
(define-typed-syntax pack
- [(_ (τ:type e) as ∃τ:type)
+ [(pack (τ:type e) as ∃τ:type)
#:with (~∃* (τ_abstract) τ_body) #'∃τ.norm
#:with [e- τ_e] (infer+erase #'e)
#:when (typecheck? #'τ_e (subst #'τ.norm #'τ_abstract #'τ_body))
(⊢ e- : ∃τ.norm)])
(define-typed-syntax open #:datum-literals (<=)
- [(_ ([(tv:id x:id) <= e_packed]) e)
+ [(open ([(tv:id x:id) <= e_packed]) e)
#:with [e_packed- ((τ_abstract) (τ_body))] (⇑ e_packed as ∃)
;; The subst below appears to be a hack, but it's not really.
;; It's the (TaPL) type rule itself that is fast and loose.
@@ -71,4 +71,4 @@
(infer #'(e)
#:tvctx #'([tv : #%type])
#:ctx #`([x : #,(subst #'tv #'τ_abstract #'τ_body)]))
- (⊢ (let ([x- e_packed-]) e-) : τ_e)])
-\ No newline at end of file
+ (⊢ (let- ([x- e_packed-]) e-) : τ_e)])
diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt
@@ -23,11 +23,11 @@
(define-base-type Char)
(define-typed-syntax #%datum
- [(_ . b:boolean) (⊢ #,(syntax/loc stx (#%datum . b)) : Bool)]
- [(_ . s:str) (⊢ #,(syntax/loc stx (#%datum . s)) : String)]
- [(_ . f) #:when (flonum? (syntax-e #'f)) (⊢ #,(syntax/loc stx (#%datum . f)) : Float)]
- [(_ . c:char) (⊢ #,(syntax/loc stx (#%datum . c)) : Char)]
- [(_ . x) (syntax/loc stx (stlc+lit:#%datum . x))])
+ [(#%datum . b:boolean) (⊢ #,(syntax/loc stx (#%datum- . b)) : Bool)]
+ [(#%datum . s:str) (⊢ #,(syntax/loc stx (#%datum- . s)) : String)]
+ [(#%datum . f) #:when (flonum? (syntax-e #'f)) (⊢ #,(syntax/loc stx (#%datum- . f)) : Float)]
+ [(#%datum . c:char) (⊢ #,(syntax/loc stx (#%datum- . c)) : Char)]
+ [(#%datum . x) (syntax/loc stx (stlc+lit:#%datum . x))])
(define-primop zero? : (→ Int Bool))
(define-primop = : (→ Int Int Bool))
@@ -37,18 +37,18 @@
(define-primop not : (→ Bool Bool))
(define-typed-syntax and
- [(_ e1 e2)
+ [(and e1 e2)
#:with e1- (⇑ e1 as Bool)
#:with e2- (⇑ e2 as Bool)
- (⊢ (and e1- e2-) : Bool)])
+ (⊢ (and- e1- e2-) : Bool)])
(define-typed-syntax or
- [(_ e ...)
+ [(or e ...)
#:with (e- ...) (⇑s (e ...) as Bool)
; #:with e1- (⇑ e1 as Bool)
; #:with e2- (⇑ e2 as Bool)
-; (⊢ (or e1- e2-) : Bool)])
- (⊢ (or e- ...) : Bool)])
+; (⊢ (or- e1- e2-) : Bool)])
+ (⊢ (or- e- ...) : Bool)])
(begin-for-syntax
(define current-join
@@ -61,8 +61,8 @@
x))))
(define-typed-syntax if
- [(~and ifstx (_ e_tst e1 e2))
- #:with τ-expected (get-expected-type #'ifstx)
+ [(if e_tst e1 e2)
+ #:with τ-expected (get-expected-type stx)
; #:with e_tst- (⇑ e_tst as Bool)
#:with [e_tst- _] (infer+erase #'e_tst)
#:with e1_ann #'(add-expected e1 τ-expected)
@@ -70,51 +70,51 @@
#:with (e1- τ1) (infer+erase #'e1_ann)
#:with (e2- τ2) (infer+erase #'e2_ann)
#:with τ-out ((current-join) #'τ1 #'τ2)
- (⊢ (if e_tst- e1- e2-) : τ-out)])
+ (⊢ (if- e_tst- e1- e2-) : τ-out)])
(define-base-type Unit)
(define-primop void : (→ Unit))
(define-typed-syntax begin
- [(_ e_unit ... e)
+ [(begin e_unit ... e)
#:with ([e_unit- _] ...) (infers+erase #'(e_unit ...)) ;(⇑s (e_unit ...) as Unit)
#:with (e- τ) (infer+erase #'e)
- (⊢ (begin e_unit- ... e-) : τ)])
+ (⊢ (begin- e_unit- ... e-) : τ)])
(define-typed-syntax ann
#:datum-literals (:)
- [(_ e : ascribed-τ:type)
+ [(ann e : ascribed-τ:type)
#:with (e- τ) (infer+erase #'(add-expected e ascribed-τ.norm))
#:fail-unless (typecheck? #'τ #'ascribed-τ.norm)
(format "~a does not have type ~a\n"
(syntax->datum #'e) (syntax->datum #'ascribed-τ))
(⊢ e- : ascribed-τ)])
-(define-typed-syntax let/tc #:export-as let
- [(~and l (_ ([x e] ...) e_body))
- #:with τ-expected (get-expected-type #'l)
+(define-typed-syntax let
+ [(let ([x e] ...) e_body)
+ #:with τ-expected (get-expected-type stx)
#:with ((e- τ) ...) (infers+erase #'(e ...))
#:with ((x- ...) e_body- τ_body) (infer/ctx+erase #'([x τ] ...) #'(add-expected e_body τ-expected))
#:fail-unless (or (not (syntax-e #'τ-expected)) ; no expected type
(typecheck? #'τ_body ((current-type-eval) #'τ-expected)))
(format "let body has type ~a, which does not match expected type ~a"
(type->str #'τ_body) (type->str #'τ-expected))
- (⊢ (let ([x- e-] ...) e_body-) : τ_body)])
+ (⊢ (let- ([x- e-] ...) e_body-) : τ_body)])
; dont need to manually transfer expected type
; result template automatically propagates properties
; - only need to transfer expected type when local expanding an expression
; - see let/tc
-(define-typed-syntax let*/tc #:export-as let*
- [(~and l (_ () e_body))
- #:with τ-expected (get-expected-type #'l)
+(define-typed-syntax let*
+ [(let* () e_body)
+ #:with τ-expected (get-expected-type stx)
#'e_body]
- [(~and l (_ ([x e] [x_rst e_rst] ...) e_body))
- #:with τ-expected (get-expected-type #'l)
- #'(let/tc ([x e]) (let*/tc ([x_rst e_rst] ...) e_body))])
+ [(let* ([x e] [x_rst e_rst] ...) e_body)
+ #:with τ-expected (get-expected-type stx)
+ #'(let ([x e]) (let* ([x_rst e_rst] ...) e_body))])
(define-typed-syntax letrec
- [(_ ([b:type-bind e] ...) e_body)
+ [(letrec ([b:type-bind e] ...) e_body)
#:with ((x- ...) (e- ... e_body-) (τ ... τ_body))
(infers/ctx+erase #'(b ...) #'((add-expected e b.type) ... e_body))
#:fail-unless (typechecks? #'(b.type ...) #'(τ ...))
@@ -129,6 +129,6 @@
(syntax->datum e) (type->str τ) (type->str τ-expect)))
#'(e ...) #'(τ ...) #'(b.type ...))
"\n")))
- (⊢ (letrec ([x- e-] ...) e_body-) : τ_body)])
+ (⊢ (letrec- ([x- e-] ...) e_body-) : τ_body)])
+
-
diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
@@ -51,18 +51,18 @@
; but then also need to normalize in current-promote
(begin-for-syntax
(define (normalize τ)
- (syntax-parse τ
+ (syntax-parse τ #:literals (#%plain-app #%plain-lambda)
[x:id #'x]
- [((~literal #%plain-app)
- ((~literal #%plain-lambda) (tv ...) τ_body) τ_arg ...)
+ [(#%plain-app
+ (#%plain-lambda (tv ...) τ_body) τ_arg ...)
(normalize (substs #'(τ_arg ...) #'(tv ...) #'τ_body))]
- [((~literal #%plain-lambda) (x ...) . bodys)
+ [(#%plain-lambda (x ...) . bodys)
#:with bodys_norm (stx-map normalize #'bodys)
(transfer-stx-props #'(#%plain-lambda (x ...) . bodys_norm) τ #:ctx τ)]
- [((~literal #%plain-app) x:id . args)
+ [(#%plain-app x:id . args)
#:with args_norm (stx-map normalize #'args)
(transfer-stx-props #'(#%plain-app x . args_norm) τ #:ctx τ)]
- [((~literal #%plain-app) . args)
+ [(#%plain-app . args)
#:with args_norm (stx-map normalize #'args)
#:with res (normalize #'(#%plain-app . args_norm))
(transfer-stx-props #'res τ #:ctx τ)]
@@ -83,12 +83,12 @@
(current-typecheck-relation (current-type=?)))
(define-typed-syntax Λ
- [(_ bvs:kind-ctx e)
+ [(Λ bvs:kind-ctx e)
#:with ((tv- ...) e- τ_e) (infer/ctx+erase #'bvs #'e)
(⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))])
(define-typed-syntax inst
- [(_ e τ ...)
+ [(inst e τ ...)
#:with (e- (([tv k] ...) (τ_body))) (⇑ e as ∀)
#:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
#:when (stx-andmap
@@ -101,14 +101,14 @@
;; TODO: merge with regular λ and app?
;; - see fomega2.rkt
(define-typed-syntax tyλ
- [(_ bvs:kind-ctx τ_body)
+ [(tyλ bvs:kind-ctx τ_body)
#:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body)
#:fail-unless ((current-kind?) #'k_body)
(format "not a valid type: ~a\n" (type->str #'τ_body))
- (⊢ (λ tvs- τ_body-) : (⇒ bvs.kind ... k_body))])
+ (⊢ (λ- tvs- τ_body-) : (⇒ bvs.kind ... k_body))])
(define-typed-syntax tyapp
- [(_ τ_fn τ_arg ...)
+ [(tyapp τ_fn τ_arg ...)
#:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒)
#:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...))
#:fail-unless (typechecks? #'(k_arg ...) #'(k_in ...))
@@ -125,4 +125,4 @@
(format "Expected: ~a arguments with type(s): "
(stx-length #'(k_in ...)))
(string-join (stx-map type->str #'(k_in ...)) ", "))
- (⊢ (#%app τ_fn- τ_arg- ...) : k_out)])
+ (⊢ (#%app- τ_fn- τ_arg- ...) : k_out)])
diff --git a/tapl/fomega2.rkt b/tapl/fomega2.rkt
@@ -45,18 +45,18 @@
; but then also need to normalize in current-promote
(begin-for-syntax
(define (normalize τ)
- (syntax-parse τ
+ (syntax-parse τ #:literals (#%plain-app #%plain-lambda)
[x:id #'x]
- [((~literal #%plain-app)
- ((~literal #%plain-lambda) (tv ...) τ_body) τ_arg ...)
+ [(#%plain-app
+ (#%plain-lambda (tv ...) τ_body) τ_arg ...)
(normalize (substs #'(τ_arg ...) #'(tv ...) #'τ_body))]
- [((~literal #%plain-lambda) (x ...) . bodys)
+ [(#%plain-lambda (x ...) . bodys)
#:with bodys_norm (stx-map normalize #'bodys)
(transfer-stx-props #'(#%plain-lambda (x ...) . bodys_norm) τ #:ctx τ)]
- [((~literal #%plain-app) x:id . args)
+ [(#%plain-app x:id . args)
#:with args_norm (stx-map normalize #'args)
(transfer-stx-props #'(#%plain-app x . args_norm) τ #:ctx τ)]
- [((~literal #%plain-app) . args)
+ [(#%plain-app . args)
#:with args_norm (stx-map normalize #'args)
(transfer-stx-props (normalize #'(#%plain-app . args_norm)) τ #:ctx τ)]
[_ τ]))
@@ -79,13 +79,13 @@
(current-typecheck-relation (current-type=?)))
(define-typed-syntax Λ
- [(_ bvs:kind-ctx e)
+ [(Λ bvs:kind-ctx e)
#:with ((tv- ...) e- τ_e)
(infer/ctx+erase #'bvs #'e)
(⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))])
(define-typed-syntax inst
- [(_ e τ ...)
+ [(inst e τ ...)
#:with (e- (([tv k] ...) (τ_body))) (⇑ e as ∀)
#:with ([τ- k_τ] ...) (infers+erase #'(τ ...))
#:when (stx-andmap (λ (t k) (or ((current-kind?) k)
diff --git a/tapl/fsub.rkt b/tapl/fsub.rkt
@@ -44,7 +44,7 @@
;; 2) instantiation of ∀
;; Problem: need type annotations, even in expanded form
;; Solution: store type annotations in a (quasi) kind <:
-(define-typed-syntax ∀ #:export-as ∀ #:datum-literals (<:)
+(define-typed-syntax ∀ #:datum-literals (<:)
[(_ ([tv:id <: τ:type] ...) τ_body)
; eval first to overwrite the old #%type
(⊢ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body)) : (<: τ.norm ...))])
@@ -73,7 +73,7 @@
#:msg "Expected ∀ type, got: ~a" #'any))))]))))
(define-typed-syntax Λ #:datum-literals (<:)
- [(_ ([tv:id <: τsub:type] ...) e)
+ [(Λ ([tv:id <: τsub:type] ...) e)
;; NOTE: store the subtyping relation of tv and τsub in another
;; "environment", ie, a syntax property with another tag: 'sub
;; The "expose" function looks for this tag to enforce the bound,
@@ -82,7 +82,7 @@
#:octx #'([tv : τsub] ...) #:tag 'sub)
(⊢ e- : (∀ ([tv- <: τsub] ...) τ_e))])
(define-typed-syntax inst
- [(_ e τ:type ...)
+ [(inst e τ:type ...)
#:with (e- (([tv τ_sub] ...) τ_body)) (⇑ e as ∀)
#:when (typechecks? #'(τ.norm ...) #'(τ_sub ...))
(⊢ e- : #,(substs #'(τ.norm ...) #'(tv ...) #'τ_body))])
diff --git a/tapl/infer.rkt b/tapl/infer.rkt
@@ -14,10 +14,10 @@
(define-syntax → ; wrapping →
(syntax-parser
- [(_ (~and Xs {X:id ...}) . rst)
+ [(→ (~and Xs {X:id ...}) . rst)
#:when (brace? #'Xs)
(add-orig #'(∀ (X ...) (ext-stlc:→ . rst)) (get-orig this-syntax))]
- [(_ . rst) (add-orig #'(∀ () (ext-stlc:→ . rst)) (get-orig this-syntax))]))
+ [(→ . rst) (add-orig #'(∀ () (ext-stlc:→ . rst)) (get-orig this-syntax))]))
(define-primop + : (→ Int Int Int))
(define-primop - : (→ Int Int Int))
@@ -61,59 +61,59 @@
(list cs (reverse (stx->list e+τs))))))
(define-typed-syntax define
- [(_ x:id e)
+ [(define x:id e)
#:with (e- τ) (infer+erase #'e)
#:with y (generate-temporary)
- #'(begin
+ #'(begin-
(define-syntax x (make-rename-transformer (⊢ y : τ)))
- (define y e-))]
- [(_ (~and Xs {X:id ...}) (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e)
+ (define- y e-))]
+ [(define (~and Xs {X:id ...}) (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e)
#:when (brace? #'Xs)
#:with g (generate-temporary #'f)
#:with e_ann #'(add-expected e τ_out)
- #'(begin
+ #'(begin-
(define-syntax f (make-rename-transformer
(⊢ g : #,(add-orig #'(∀ (X ...) (ext-stlc:→ τ ... τ_out))
#'(→ τ ... τ_out)))))
- (define g (Λ (X ...) (ext-stlc:λ ([x : τ] ...) e_ann))))]
- [(_ (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e)
+ (define- g (Λ (X ...) (ext-stlc:λ ([x : τ] ...) e_ann))))]
+ [(define (f:id [x:id (~datum :) τ] ... (~datum →) τ_out) e)
#:with g (generate-temporary #'f)
#:with e_ann #'(add-expected e τ_out)
- #'(begin
+ #'(begin-
(define-syntax f (make-rename-transformer (⊢ g : (→ τ ... τ_out))))
- (define g (ext-stlc:λ ([x : τ] ...) e_ann)))])
+ (define- g (ext-stlc:λ ([x : τ] ...) e_ann)))])
; all λs have type (∀ (X ...) (→ τ_in ... τ_out))
(define-typed-syntax λ #:datum-literals (:)
- [(~and fn (_ (x:id ...) e)) ; no annotations, try to infer from outer ctx, ie an application
- #:with given-τ-args (syntax-property #'fn 'given-τ-args)
+ [(λ (x:id ...) e) ; no annotations, try to infer from outer ctx, ie an application
+ #:with given-τ-args (syntax-property stx 'given-τ-args)
#:fail-unless (syntax-e #'given-τ-args) ; no inferred types or annotations, so error
(format "input types for ~a could not be inferred; add annotations"
- (syntax->datum #'fn))
+ (syntax->datum stx))
#:with (τ_arg ...) #'given-τ-args
- #:with [λ- τ_λ] (infer+erase #'(ext-stlc:λ ([x : τ_arg] ...) e))
- (⊢ λ- : #,(add-orig #'(∀ () τ_λ) (get-orig #'τ_λ)))]
- [(~and fn (_ (x:id ...) e) ~!) ; no annotations, couldnt infer from ctx (eg, unapplied lam), try to infer from body
+ #:with [fn- τ_fn] (infer+erase #'(ext-stlc:λ ([x : τ_arg] ...) e))
+ (⊢ fn- : #,(add-orig #'(∀ () τ_fn) (get-orig #'τ_fn)))]
+ [(_ (x:id ...) ~! e) ; no annotations, couldnt infer from ctx (eg, unapplied lam), try to infer from body
#:with (xs- e- τ_res) (infer/ctx+erase #'([x : x] ...) #'e)
#:with env (get-env #'e-)
#:fail-unless (syntax-e #'env)
(format "input types for ~a could not be inferred; add annotations"
- (syntax->datum #'fn))
+ (syntax->datum stx))
#:with (τ_arg ...) (stx-map (λ (y) (lookup y #'env)) #'xs-)
#:fail-unless (stx-andmap syntax-e #'(τ_arg ...))
(format "some input types for ~a could not be inferred; add annotations"
- (syntax->datum #'fn))
+ (syntax->datum stx))
;; propagate up inferred types of variables
- #:with res (add-env #'(λ xs- e-) #'env)
-; #:with [λ- τ_λ] (infer+erase #'(ext-stlc:λ ([x : x] ...) e))
+ #:with res (add-env #'(λ- xs- e-) #'env)
+; #:with [fn- τ_fn] (infer+erase #'(ext-stlc:λ ([x : x] ...) e))
(⊢ res : #,(add-orig #'(∀ () (ext-stlc:→ τ_arg ... τ_res))
#`(→ #,@(stx-map get-orig #'(τ_arg ... τ_res)))))]
- ;(⊢ (λ xs- e-) : (∀ () (ext-stlc:→ τ_arg ... τ_res)))]
- [(_ . rst)
- #:with [λ- τ_λ] (infer+erase #'(ext-stlc:λ . rst))
- (⊢ λ- : #,(add-orig #'(∀ () τ_λ) (get-orig #'τ_λ)))])
+ ;(⊢ (λ- xs- e-) : (∀ () (ext-stlc:→ τ_arg ... τ_res)))]
+ [(λ . rst)
+ #:with [fn- τ_fn] (infer+erase #'(ext-stlc:λ . rst))
+ (⊢ fn- : #,(add-orig #'(∀ () τ_fn) (get-orig #'τ_fn)))])
-(define-typed-syntax #%app
+(define-typed-syntax infer:#%app #:export-as #%app
[(_ e_fn e_arg ...) ; infer args first
; #:when (printf "args first ~a\n" (syntax->datum stx))
#:with maybe-inferred-τs (with-handlers ([exn:fail:type:infer? (λ _ #f)])
@@ -158,8 +158,8 @@
(string-join (stx-map type->str #'(τ_in ...)) ", ")))
; propagate inferred types for variables up
#:with env (stx-flatten (filter (λ (x) x) (stx-map get-env #'(e_arg- ...))))
- #:with result-app (add-env #'(#%app e_fn- e_arg- ...) #'env)
- ;(⊢ (#%app e_fn- e_arg- ...) : τ_out)]
+ #:with result-app (add-env #'(#%app- e_fn- e_arg- ...) #'env)
+ ;(⊢ (#%app- e_fn- e_arg- ...) : τ_out)]
(⊢ result-app : τ_out)]
[(_ e_fn e_arg ...) ; infer fn first ------------------------- ; TODO: remove code dup
; #:when (printf "fn first ~a\n" (syntax->datum stx))
@@ -195,6 +195,6 @@
(format "Expected: ~a arguments with type(s): "
(stx-length #'(τ_in ...)))
(string-join (stx-map type->str #'(τ_in ...)) ", "))
- #:with result-app (add-env #'(#%app e_fn- e_arg- ...) #'env)
- ;(⊢ (#%app e_fn- e_arg- ...) : τ_out)])
+ #:with result-app (add-env #'(#%app- e_fn- e_arg- ...) #'env)
+ ;(⊢ (#%app- e_fn- e_arg- ...) : τ_out)])
(⊢ result-app : τ_out)])
diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
@@ -306,16 +306,16 @@
;; - since the order of the inferred type variables depends on expansion order,
;; which is not known to programmers, to make the result slightly more
;; intuitive, we arbitrarily sort the inferred tyvars lexicographically
-(define-typed-syntax define/tc #:export-as define
- [(_ x:id e)
+(define-typed-syntax define
+ [(define x:id e)
#:with (e- τ) (infer+erase #'e)
#:with y (generate-temporary)
- #'(begin
+ #'(begin-
(define-syntax x (make-rename-transformer (⊢ y : τ)))
- (define y e-))]
+ (define- y e-))]
; explicit "forall"
- [(_ Ys (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out)
- e_body ... e)
+ [(define Ys (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out)
+ e_body ... e)
#:when (brace? #'Ys)
;; TODO; remove this code duplication
#:with g (add-orig (generate-temporary #'f) #'f)
@@ -326,15 +326,15 @@
;; top-lvl fns, since they can call each other
#:with (~and ty_fn_expected (~?∀ _ (~ext-stlc:→ _ ... out_expected)))
((current-type-eval) #'(?∀ Ys (ext-stlc:→ τ+orig ...)))
- #`(begin
- (define-syntax f (make-rename-transformer (⊢ g : ty_fn_expected)))
- (define g
- (Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))]
+ #`(begin-
+ (define-syntax f (make-rename-transformer (⊢ g : ty_fn_expected)))
+ (define- g
+ (Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))]
;; alternate type sig syntax, after parameter names
- [(_ (f:id x:id ...) (~datum :) ty ... (~or (~datum ->) (~datum →)) ty_out . b)
- #'(define/tc (f [x : ty] ... -> ty_out) . b)]
- [(_ (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out)
- e_body ... e)
+ [(define (f:id x:id ...) (~datum :) ty ... (~or (~datum ->) (~datum →)) ty_out . b)
+ #'(define (f [x : ty] ... -> ty_out) . b)]
+ [(define (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out)
+ e_body ... e)
#:with Ys (compute-tyvars #'(τ ... τ_out))
#:with g (add-orig (generate-temporary #'f) #'f)
#:with e_ann #'(add-expected e τ_out) ; must be macro bc t_out may have unbound tvs
@@ -347,10 +347,10 @@
((current-type-eval) #'(?∀ Ys (ext-stlc:→ τ+orig ...)))
'orig
(list #'(→ τ+orig ...)))
- #`(begin
- (define-syntax f (make-rename-transformer (⊢ g : ty_fn_expected)))
- (define g
- (?Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))])
+ #`(begin-
+ (define-syntax f (make-rename-transformer (⊢ g : ty_fn_expected)))
+ (define- g
+ (?Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))])
;; define-type -----------------------------------------------
;; TODO: should validate τ as part of define-type definition (before it's used)
@@ -359,21 +359,21 @@
;; for now, validate types but punt if encountering unbound ids
(define-syntax (define-type stx)
(syntax-parse stx
- [(_ Name:id . rst)
+ [(define-type Name:id . rst)
#:with NewName (generate-temporary #'Name)
#:with Name2 (add-orig #'(NewName) #'Name)
- #`(begin
+ #`(begin-
(define-type Name2 . #,(subst #'Name2 #'Name #'rst))
(stlc+rec-iso:define-type-alias Name Name2))]
- [(_ (Name:id X:id ...)
- ;; constructors must have the form (Cons τ ...)
- ;; but the first ~or clause accepts 0-arg constructors as ids;
- ;; the ~and is a workaround to bind the duplicate Cons ids (see Ryan's email)
- (~and (~or (~and IdCons:id
+ [(define-type (Name:id X:id ...)
+ ;; constructors must have the form (Cons τ ...)
+ ;; but the first ~or clause accepts 0-arg constructors as ids;
+ ;; the ~and is a workaround to bind the duplicate Cons ids (see Ryan's email)
+ (~and (~or (~and IdCons:id
(~parse (Cons [fld (~datum :) τ] ...) #'(IdCons)))
- (Cons [fld (~datum :) τ] ...)
- (~and (Cons τ ...)
- (~parse (fld ...) (generate-temporaries #'(τ ...)))))) ...)
+ (Cons [fld (~datum :) τ] ...)
+ (~and (Cons τ ...)
+ (~parse (fld ...) (generate-temporaries #'(τ ...)))))) ...)
;; validate tys
#:with (ty_flat ...) (stx-flatten #'((τ ...) ...))
#:with (_ _ (_ _ (_ _ (_ _ ty+ ...))))
@@ -384,7 +384,7 @@
#`(lambda () (let-syntax () (let-syntax () (#%app void unbound)))))])
(expand/df
#`(lambda (X ...)
- (let-syntax
+ (let-syntax
([Name
(syntax-parser
[(_ X ...) (mk-type #'void)]
@@ -417,7 +417,7 @@
#'(StructName ...) #'((fld ...) ...))
#:with (Cons? ...) (stx-map mk-? #'(StructName ...))
#:with (exposed-Cons? ...) (stx-map mk-? #'(Cons ...))
- #`(begin
+ #`(begin-
(define-syntax (NameExtraInfo stx)
(syntax-parse stx
[(_ X ...) #'(('Cons 'StructName Cons? [acc τ] ...) ...)]))
@@ -432,7 +432,7 @@
(list #'τ ... ...))
#:extra-info 'NameExtraInfo
#:no-provide)
- (struct StructName (fld ...) #:reflection-name 'Cons #:transparent) ...
+ (struct- StructName (fld ...) #:reflection-name 'Cons #:transparent) ...
(define-syntax (exposed-acc stx) ; accessor for records
(syntax-parse stx
[_:id (⊢ acc (?∀ (X ...) (ext-stlc:→ (Name X ...) τ)))]
@@ -678,7 +678,7 @@
(define-syntax (match2 stx)
(syntax-parse stx #:datum-literals (with)
- [(_ e with . clauses)
+ [(match2 e with . clauses)
#:fail-when (null? (syntax->list #'clauses)) "no clauses"
#:with [e- τ_e] (infer+erase #'e)
(syntax-parse #'clauses #:datum-literals (->)
@@ -694,11 +694,11 @@
#'(ctx ...) #'((add-expected e_body ty-expected) ...))
#:when (check-exhaust #'(pat- ...) #'τ_e)
#:with τ_out (stx-foldr (current-join) (stx-car #'(ty_body ...)) (stx-cdr #'(ty_body ...)))
- (⊢ (match e- [pat- (let ([x- x] ...) e_body-)] ...) : τ_out)
+ (⊢ (match- e- [pat- (let- ([x- x] ...) e_body-)] ...) : τ_out)
])]))
(define-typed-syntax match #:datum-literals (with)
- [(_ e with . clauses)
+ [(match e with . clauses)
#:fail-when (null? (syntax->list #'clauses)) "no clauses"
#:with [e- τ_e] (infer+erase #'e)
#:with t_expect (syntax-property stx 'expected-type) ; propagate inferred type
@@ -712,10 +712,10 @@
#:with [(x- ...) e_body- ty_body] (infer/ctx+erase #'([x ty] ...)
#'(add-expected e_body t_expect))
#:with (acc ...) (for/list ([(a i) (in-indexed (syntax->list #'(x ...)))])
- #`(lambda (s) (list-ref s #,(datum->syntax #'here i))))
+ #`(lambda- (s) (list-ref- s #,(datum->syntax #'here i))))
#:with z (generate-temporary)
- (⊢ (let ([z e-])
- (let ([x- (acc z)] ...) e_body-))
+ (⊢ (let- ([z e-])
+ (let- ([x- (acc z)] ...) e_body-))
: ty_body)])]
[(List? #'τ_e) ;; e is List
(syntax-parse #'clauses #:datum-literals (-> ::)
@@ -735,20 +735,20 @@
#'(([x ty] ... [rst (List ty)]) ...) #'((add-expected e_body t_expect) ...))
#:with τ_out (stx-foldr (current-join) (stx-car #'(ty_body ...)) (stx-cdr #'(ty_body ...)))
#:with (len ...) (stx-map (lambda (p) #`#,(stx-length p)) #'((x ...) ...))
- #:with (lenop ...) (stx-map (lambda (p) (if (brack? p) #'= #'>=)) #'(xs ...))
+ #:with (lenop ...) (stx-map (lambda (p) (if (brack? p) #'=- #'>=-)) #'(xs ...))
#:with (pred? ...) (stx-map
- (lambda (l lo) #`(λ (lst) (#,lo (length lst) #,l)))
+ (lambda (l lo) #`(λ- (lst) (#,lo (length- lst) #,l)))
#'(len ...) #'(lenop ...))
#:with ((acc1 ...) ...) (stx-map
(lambda (xs)
(for/list ([(x i) (in-indexed (syntax->list xs))])
- #`(lambda (lst) (list-ref lst #,(datum->syntax #'here i)))))
+ #`(lambda- (lst) (list-ref- lst #,(datum->syntax #'here i)))))
#'((x ...) ...))
- #:with (acc2 ...) (stx-map (lambda (l) #`(lambda (lst) (list-tail lst #,l))) #'(len ...))
- (⊢ (let ([z e-])
- (cond
+ #:with (acc2 ...) (stx-map (lambda (l) #`(lambda- (lst) (list-tail- lst #,l))) #'(len ...))
+ (⊢ (let- ([z e-])
+ (cond-
[(pred? z)
- (let ([x- (acc1 z)] ... [rst- (acc2 z)]) e_body-)] ...))
+ (let- ([x- (acc1 z)] ... [rst- (acc2 z)]) e_body-)] ...))
: τ_out)])]
[else ;; e is variant
(syntax-parse #'clauses #:datum-literals (->)
@@ -793,21 +793,21 @@
"guard expression(s) must have type bool"
#:with τ_out (stx-foldr (current-join) (stx-car #'(τ_ec ...)) (stx-cdr #'(τ_ec ...)))
#:with z (generate-temporary) ; dont duplicate eval of test expr
- (⊢ (let ([z e-])
- (cond
- [(and (Cons? z)
- (let ([x- (acc z)] ...) e_guard-))
- (let ([x- (acc z)] ...) e_c-)] ...))
+ (⊢ (let- ([z e-])
+ (cond-
+ [(and- (Cons? z)
+ (let- ([x- (acc z)] ...) e_guard-))
+ (let- ([x- (acc z)] ...) e_c-)] ...))
: τ_out)])])])
; special arrow that computes free vars; for use with tests
; (because we can't write explicit forall
(define-syntax →/test
(syntax-parser
- [(_ (~and Xs (X:id ...)) . rst)
+ [(→/test (~and Xs (X:id ...)) . rst)
#:when (brace? #'Xs)
#'(?∀ (X ...) (ext-stlc:→ . rst))]
- [(_ . rst)
+ [(→/test . rst)
#:with Xs (compute-tyvars #'rst)
#'(?∀ Xs (ext-stlc:→ . rst))]))
@@ -832,8 +832,8 @@
(define-primop odd? : (→ Int Bool))
; all λs have type (?∀ (X ...) (→ τ_in ... τ_out))
-(define-typed-syntax liftedλ #:export-as λ
- [(_ (x:id ...+) body)
+(define-typed-syntax λ
+ [(λ (x:id ...+) body)
#:with (~?∀ Xs expected) (get-expected-type stx)
#:do [(unless (→? #'expected)
(type-error #:src stx #:msg "λ parameters must have type annotations"))]
@@ -843,10 +843,10 @@
(format "expected a function of ~a arguments, got one with ~a arguments"
(stx-length #'[arg-ty ...] #'[x ...]))))]
#`(?Λ Xs (ext-stlc:λ ([x : arg-ty] ...) #,(add-expected-ty #'body #'body-ty)))]
- [(_ args body)
+ [(λ args body)
#:with (~?∀ () (~ext-stlc:→ arg-ty ... body-ty)) (get-expected-type stx)
#`(?Λ () (ext-stlc:λ args #,(add-expected-ty #'body #'body-ty)))]
- [(_ (~and x+tys ([_ (~datum :) ty] ...)) . body)
+ [(λ (~and x+tys ([_ (~datum :) ty] ...)) . body)
#:with Xs (compute-tyvars #'(ty ...))
;; TODO is there a way to have λs that refer to ids defined after them?
#'(?Λ Xs (ext-stlc:λ x+tys . body))])
@@ -907,7 +907,7 @@
(unless (covariant-X? X #'τ_out)
(raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)))
#'(∀ (unsolved-X ... Y ...) τ_out)]))
- (⊢ (#%app e_fn- e_arg- ...) : τ_out*)])])]
+ (⊢ (#%app- e_fn- e_arg- ...) : τ_out*)])])]
[(_ e_fn . e_args) ; err case; e_fn is not a function
#:with [e_fn- τ_fn] (infer+erase #'e_fn)
(type-error #:src stx
@@ -917,190 +917,190 @@
;; cond and other conditionals
(define-typed-syntax cond
- [(_ [(~or (~and (~datum else) (~parse test #'(ext-stlc:#%datum . #t)))
- test)
- b ... body] ...+)
+ [(cond [(~or (~and (~datum else) (~parse test #'(ext-stlc:#%datum . #t)))
+ test)
+ b ... body] ...+)
#:with (test- ...) (⇑s (test ...) as Bool)
#:with ty-expected (get-expected-type stx)
#:with ([body- ty_body] ...) (infers+erase #'((add-expected body ty-expected) ...))
#:with (([b- ty_b] ...) ...) (stx-map infers+erase #'((b ...) ...))
#:with τ_out (stx-foldr (current-join) (stx-car #'(ty_body ...)) (stx-cdr #'(ty_body ...)))
- (⊢ (cond [test- b- ... body-] ...) : τ_out)])
+ (⊢ (cond- [test- b- ... body-] ...) : τ_out)])
(define-typed-syntax when
- [(_ test body ...)
+ [(when test body ...)
; #:with test- (⇑ test as Bool)
#:with [test- _] (infer+erase #'test)
#:with [(body- _) ...] (infers+erase #'(body ...))
- (⊢ (when test- body- ...) : Unit)])
+ (⊢ (when- test- body- ...) : Unit)])
(define-typed-syntax unless
- [(_ test body ...)
+ [(unless test body ...)
; #:with test- (⇑ test as Bool)
#:with [test- _] (infer+erase #'test)
#:with [(body- _) ...] (infers+erase #'(body ...))
- (⊢ (unless test- body- ...) : Unit)])
+ (⊢ (unless- test- body- ...) : Unit)])
;; sync channels and threads
(define-type-constructor Channel)
(define-typed-syntax make-channel
- [(_ (~and tys {ty}))
+ [(make-channel (~and tys {ty}))
#:when (brace? #'tys)
- (⊢ (make-channel) : (Channel ty))])
+ (⊢ (make-channel-) : (Channel ty))])
(define-typed-syntax channel-get
- [(_ c)
+ [(channel-get c)
#:with (c- (ty)) (⇑ c as Channel)
- (⊢ (channel-get c-) : ty)])
+ (⊢ (channel-get- c-) : ty)])
(define-typed-syntax channel-put
- [(_ c v)
+ [(channel-put c v)
#:with (c- (ty)) (⇑ c as Channel)
#:with [v- ty_v] (infer+erase #'v)
#:fail-unless (typechecks? #'ty_v #'ty)
(format "Cannot send ~a value on ~a channel."
(type->str #'ty_v) (type->str #'ty))
- (⊢ (channel-put c- v-) : Unit)])
+ (⊢ (channel-put- c- v-) : Unit)])
(define-base-type Thread)
;; threads
(define-typed-syntax thread
- [(_ th)
+ [(thread th)
#:with (th- (~?∀ () (~ext-stlc:→ τ_out))) (infer+erase #'th)
- (⊢ (thread th-) : Thread)])
+ (⊢ (thread- th-) : Thread)])
(define-primop random : (→ Int Int))
(define-primop integer->char : (→ Int Char))
(define-primop string->list : (→ String (List Char)))
(define-primop string->number : (→ String Int))
;(define-primop number->string : (→ Int String))
-(define-typed-syntax num->str #:export-as number->string
- [f:id (assign-type #'number->string #'(→ Int String))]
- [(_ n)
- #'(num->str n (ext-stlc:#%datum . 10))]
- [(_ n rad)
+(define-typed-syntax number->string
+ [f:id (assign-type #'number->string- #'(→ Int String))]
+ [(number->string n)
+ #'(number->string n (ext-stlc:#%datum . 10))]
+ [(number->string n rad)
#:with args- (⇑s (n rad) as Int)
- (⊢ (number->string . args-) : String)])
+ (⊢ (number->string- . args-) : String)])
(define-primop string : (→ Char String))
(define-primop sleep : (→ Int Unit))
(define-primop string=? : (→ String String Bool))
(define-primop string<=? : (→ String String Bool))
(define-typed-syntax string-append
- [(_ . strs)
+ [(string-append . strs)
#:with strs- (⇑s strs as String)
- (⊢ (string-append . strs-) : String)])
+ (⊢ (string-append- . strs-) : String)])
;; vectors
(define-type-constructor Vector)
(define-typed-syntax vector
- [(_ (~and tys {ty}))
+ [(vector (~and tys {ty}))
#:when (brace? #'tys)
- (⊢ (vector) : (Vector ty))]
- [(_ v ...)
+ (⊢ (vector-) : (Vector ty))]
+ [(vector v ...)
#:with ([v- ty] ...) (infers+erase #'(v ...))
#:when (same-types? #'(ty ...))
#:with one-ty (stx-car #'(ty ...))
- (⊢ (vector v- ...) : (Vector one-ty))])
-(define-typed-syntax make-vector/tc #:export-as make-vector
- [(_ n) #'(make-vector/tc n (ext-stlc:#%datum . 0))]
- [(_ n e)
+ (⊢ (vector- v- ...) : (Vector one-ty))])
+(define-typed-syntax make-vector
+ [(make-vector n) #'(make-vector n (ext-stlc:#%datum . 0))]
+ [(make-vector n e)
#:with n- (⇑ n as Int)
#:with [e- ty] (infer+erase #'e)
- (⊢ (make-vector n- e-) : (Vector ty))])
+ (⊢ (make-vector- n- e-) : (Vector ty))])
(define-typed-syntax vector-length
- [(_ e)
+ [(vector-length e)
#:with [e- _] (⇑ e as Vector)
- (⊢ (vector-length e-) : Int)])
+ (⊢ (vector-length- e-) : Int)])
(define-typed-syntax vector-ref
- [(_ e n)
+ [(vector-ref e n)
#:with n- (⇑ n as Int)
#:with [e- (ty)] (⇑ e as Vector)
- (⊢ (vector-ref e- n-) : ty)])
+ (⊢ (vector-ref- e- n-) : ty)])
(define-typed-syntax vector-set!
- [(_ e n v)
+ [(vector-set! e n v)
#:with n- (⇑ n as Int)
#:with [e- (ty)] (⇑ e as Vector)
#:with [v- ty_v] (infer+erase #'v)
#:when (typecheck? #'ty_v #'ty)
- (⊢ (vector-set! e- n- v-) : Unit)])
+ (⊢ (vector-set!- e- n- v-) : Unit)])
(define-typed-syntax vector-copy!
- [(_ dest start src)
+ [(vector-copy! dest start src)
#:with start- (⇑ start as Int)
#:with [dest- (ty_dest)] (⇑ dest as Vector)
#:with [src- (ty_src)] (⇑ src as Vector)
#:when (typecheck? #'ty_dest #'ty_src)
- (⊢ (vector-copy! dest- start- src-) : Unit)])
+ (⊢ (vector-copy!- dest- start- src-) : Unit)])
;; sequences and for loops
(define-type-constructor Sequence)
-(define-typed-syntax in-range/tc #:export-as in-range
- [(_ end)
- #'(in-range/tc (ext-stlc:#%datum . 0) end (ext-stlc:#%datum . 1))]
- [(_ start end)
- #'(in-range/tc start end (ext-stlc:#%datum . 1))]
- [(_ start end step)
+(define-typed-syntax in-range
+ [(in-range end)
+ #'(in-range (ext-stlc:#%datum . 0) end (ext-stlc:#%datum . 1))]
+ [(in-range start end)
+ #'(in-range start end (ext-stlc:#%datum . 1))]
+ [(in-range start end step)
#:with (e- ...) (⇑s (start end step) as Int)
- (⊢ (in-range e- ...) : (Sequence Int))])
+ (⊢ (in-range- e- ...) : (Sequence Int))])
-(define-typed-syntax in-naturals/tc #:export-as in-naturals
- [(_) #'(in-naturals/tc (ext-stlc:#%datum . 0))]
- [(_ start)
+(define-typed-syntax in-naturals
+ [(in-naturals) #'(in-naturals (ext-stlc:#%datum . 0))]
+ [(in-naturals start)
#:with start- (⇑ start as Int)
- (⊢ (in-naturals start-) : (Sequence Int))])
+ (⊢ (in-naturals- start-) : (Sequence Int))])
(define-typed-syntax in-vector
- [(_ e)
+ [(in-vector e)
#:with [e- (ty)] (⇑ e as Vector)
- (⊢ (in-vector e-) : (Sequence ty))])
+ (⊢ (in-vector- e-) : (Sequence ty))])
(define-typed-syntax in-list
- [(_ e)
+ [(in-list e)
#:with [e- (ty)] (⇑ e as List)
- (⊢ (in-list e-) : (Sequence ty))])
+ (⊢ (in-list- e-) : (Sequence ty))])
(define-typed-syntax in-lines
- [(_ e)
+ [(in-lines e)
#:with e- (⇑ e as String)
- (⊢ (in-lines (open-input-string e-)) : (Sequence String))])
+ (⊢ (in-lines- (open-input-string e-)) : (Sequence String))])
(define-typed-syntax for
- [(_ ([x:id e]...) b ... body)
+ [(for ([x:id e]...) b ... body)
#:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
#:with [(x- ...) (b- ... body-) (ty_b ... ty_body)]
(infers/ctx+erase #'([x : ty] ...) #'(b ... body))
- (⊢ (for ([x- e-] ...) b- ... body-) : Unit)])
+ (⊢ (for- ([x- e-] ...) b- ... body-) : Unit)])
(define-typed-syntax for*
- [(_ ([x:id e]...) body)
+ [(for* ([x:id e]...) body)
#:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
#:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
- (⊢ (for* ([x- e-] ...) body-) : Unit)])
+ (⊢ (for*- ([x- e-] ...) body-) : Unit)])
(define-typed-syntax for/list
- [(_ ([x:id e]...) body)
+ [(for/list ([x:id e]...) body)
#:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
#:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
- (⊢ (for/list ([x- e-] ...) body-) : (List ty_body))])
+ (⊢ (for/list- ([x- e-] ...) body-) : (List ty_body))])
(define-typed-syntax for/vector
- [(_ ([x:id e]...) body)
+ [(for/vector ([x:id e]...) body)
#:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
#:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
- (⊢ (for/vector ([x- e-] ...) body-) : (Vector ty_body))])
+ (⊢ (for/vector- ([x- e-] ...) body-) : (Vector ty_body))])
(define-typed-syntax for*/vector
- [(_ ([x:id e]...) body)
+ [(for*/vector ([x:id e]...) body)
#:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
#:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
- (⊢ (for*/vector ([x- e-] ...) body-) : (Vector ty_body))])
+ (⊢ (for*/vector- ([x- e-] ...) body-) : (Vector ty_body))])
(define-typed-syntax for*/list
- [(_ ([x:id e]...) body)
+ [(for*/list ([x:id e]...) body)
#:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
#:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
- (⊢ (for*/list ([x- e-] ...) body-) : (List ty_body))])
+ (⊢ (for*/list- ([x- e-] ...) body-) : (List ty_body))])
(define-typed-syntax for/fold
- [(_ ([acc init]) ([x:id e] ...) body)
+ [(for/fold ([acc init]) ([x:id e] ...) body)
#:with [init- ty_init] (infer+erase #`(pass-expected init #,stx))
#:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
#:with [(acc- x- ...) body- ty_body]
@@ -1110,54 +1110,56 @@
#:msg
"for/fold: Type of body and initial accumulator must be the same, given ~a and ~a"
#'ty_init #'ty_body)
- (⊢ (for/fold ([acc- init-]) ([x- e-] ...) body-) : ty_body)])
+ (⊢ (for/fold- ([acc- init-]) ([x- e-] ...) body-) : ty_body)])
(define-typed-syntax for/hash
- [(_ ([x:id e]...) body)
+ [(for/hash ([x:id e]...) body)
#:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
#:with [(x- ...) body- (~× ty_k ty_v)]
(infer/ctx+erase #'([x : ty] ...) #'body)
- (⊢ (for/hash ([x- e-] ...) (let ([t body-]) (values (car t) (cadr t))))
- : (Hash ty_k ty_v))])
+ (⊢ (for/hash- ([x- e-] ...)
+ (let- ([t body-])
+ (values- (car- t) (cadr- t))))
+ : (Hash ty_k ty_v))])
(define-typed-syntax for/sum
- [(_ ([x:id e]...
+ [(for/sum ([x:id e]...
(~optional (~seq #:when guard) #:defaults ([guard #'#t])))
body)
#:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
#:with [(x- ...) (guard- body-) (_ ty_body)]
(infers/ctx+erase #'([x : ty] ...) #'(guard body))
#:when (Int? #'ty_body)
- (⊢ (for/sum ([x- e-] ... #:when guard-) body-) : Int)])
+ (⊢ (for/sum- ([x- e-] ... #:when guard-) body-) : Int)])
; printing and displaying
(define-typed-syntax printf
- [(_ str e ...)
+ [(printf str e ...)
#:with s- (⇑ str as String)
#:with ([e- ty] ...) (infers+erase #'(e ...))
- (⊢ (printf s- e- ...) : Unit)])
+ (⊢ (printf- s- e- ...) : Unit)])
(define-typed-syntax format
- [(_ str e ...)
+ [(format str e ...)
#:with s- (⇑ str as String)
#:with ([e- ty] ...) (infers+erase #'(e ...))
- (⊢ (format s- e- ...) : String)])
+ (⊢ (format- s- e- ...) : String)])
(define-typed-syntax display
- [(_ e)
+ [(display e)
#:with [e- _] (infer+erase #'e)
- (⊢ (display e-) : Unit)])
+ (⊢ (display- e-) : Unit)])
(define-typed-syntax displayln
- [(_ e)
+ [(displayln e)
#:with [e- _] (infer+erase #'e)
- (⊢ (displayln e-) : Unit)])
+ (⊢ (displayln- e-) : Unit)])
(define-primop newline : (→ Unit))
(define-typed-syntax list->vector
- [(_ e)
+ [(list->vector e)
#:with [e- (ty)] (⇑ e as List)
- (⊢ (list->vector e-) : (Vector ty))])
+ (⊢ (list->vector- e-) : (Vector ty))])
(define-typed-syntax let
- [(_ name:id (~datum :) ty:type ~! ([x:id e] ...) b ... body)
+ [(let name:id (~datum :) ty:type ~! ([x:id e] ...) b ... body)
#:with ([e- ty_e] ...) (infers+erase #'(e ...))
#:with [(name- . xs-) (body- ...) (_ ... ty_body)]
(infers/ctx+erase #'([name : (→ ty_e ... ty.norm)][x : ty_e] ...)
@@ -1165,17 +1167,17 @@
#:fail-unless (typecheck? #'ty_body #'ty.norm)
(format "type of let body ~a does not match expected typed ~a"
(type->str #'ty_body) (type->str #'ty))
- (⊢ (letrec ([name- (λ xs- body- ...)])
+ (⊢ (letrec- ([name- (λ- xs- body- ...)])
(name- e- ...))
: ty_body)]
- [(_ ([x:id e] ...) body ...)
- #'(ext-stlc:let ([x e] ...) (begin/tc body ...))])
+ [(let ([x:id e] ...) body ...)
+ #'(ext-stlc:let ([x e] ...) (begin body ...))])
(define-typed-syntax let*
- [(_ ([x:id e] ...) body ...)
- #'(ext-stlc:let* ([x e] ...) (begin/tc body ...))])
+ [(let* ([x:id e] ...) body ...)
+ #'(ext-stlc:let* ([x e] ...) (begin body ...))])
-(define-typed-syntax begin/tc #:export-as begin
- [(_ body ... b)
+(define-typed-syntax begin
+ [(begin body ... b)
#:with expected (get-expected-type stx)
#:with b_ann #'(add-expected b expected)
#'(ext-stlc:begin body ... b_ann)])
@@ -1184,52 +1186,56 @@
(define-type-constructor Hash #:arity = 2)
(define-typed-syntax in-hash
- [(_ e)
+ [(in-hash e)
#:with [e- (ty_k ty_v)] (⇑ e as Hash)
- (⊢ (map (λ (k+v) (list (car k+v) (cdr k+v))) (hash->list e-))
-; (⊢ (hash->list e-)
+ (⊢ (hash-map- e- list-)
: (Sequence (stlc+rec-iso:× ty_k ty_v)))])
; mutable hashes
(define-typed-syntax hash
- [(_ (~and tys {ty_key ty_val}))
+ [(hash (~and tys {ty_key ty_val}))
#:when (brace? #'tys)
- (⊢ (make-hash) : (Hash ty_key ty_val))]
- [(_ (~seq k v) ...)
+ (⊢ (make-hash-) : (Hash ty_key ty_val))]
+ [(hash (~seq k v) ...)
#:with ([k- ty_k] ...) (infers+erase #'(k ...))
#:with ([v- ty_v] ...) (infers+erase #'(v ...))
#:when (same-types? #'(ty_k ...))
#:when (same-types? #'(ty_v ...))
#:with ty_key (stx-car #'(ty_k ...))
#:with ty_val (stx-car #'(ty_v ...))
- (⊢ (make-hash (list (cons k- v-) ...)) : (Hash ty_key ty_val))])
+ (⊢ (make-hash- (list- (cons- k- v-) ...)) : (Hash ty_key ty_val))])
(define-typed-syntax hash-set!
- [(_ h k v)
+ [(hash-set! h k v)
#:with [h- (ty_key ty_val)] (⇑ h as Hash)
#:with [k- ty_k] (infer+erase #'k)
#:with [v- ty_v] (infer+erase #'v)
#:when (typecheck? #'ty_k #'ty_key)
#:when (typecheck? #'ty_v #'ty_val)
- (⊢ (hash-set! h- k- v-) : Unit)])
-(define-typed-syntax hash-ref/tc #:export-as hash-ref
- [(_ h k) #'(hash-ref/tc h k (ext-stlc:#%datum . #f))]
- [(_ h k fail)
+ (⊢ (hash-set!- h- k- v-) : Unit)])
+(define-typed-syntax hash-ref
+ [(hash-ref h k)
#:with [h- (ty_key ty_val)] (⇑ h as Hash)
#:with [k- ty_k] (infer+erase #'k)
#:when (typecheck? #'ty_k #'ty_key)
- #:with (fail- _) (infer+erase #'fail) ; default val can be any
- (⊢ (hash-ref h- k- fail-) : ty_val)])
+ (⊢ (hash-ref- h- k-) : ty_val)]
+ [(hash-ref h k fail)
+ #:with [h- (ty_key ty_val)] (⇑ h as Hash)
+ #:with [k- ty_k] (infer+erase #'k)
+ #:when (typecheck? #'ty_k #'ty_key)
+ #:with [fail- (~?∀ () (~ext-stlc:→ ty_fail))] (infer+erase #'fail)
+ #:when (typecheck? #'ty_fail #'ty_val)
+ (⊢ (hash-ref- h- k- fail-) : ty_val)])
(define-typed-syntax hash-has-key?
- [(_ h k)
+ [(hash-has-key? h k)
#:with [h- (ty_key _)] (⇑ h as Hash)
#:with [k- ty_k] (infer+erase #'k)
#:when (typecheck? #'ty_k #'ty_key)
- (⊢ (hash-has-key? h- k-) : Bool)])
+ (⊢ (hash-has-key?- h- k-) : Bool)])
(define-typed-syntax hash-count
- [(_ h)
+ [(hash-count h)
#:with [h- _] (⇑ h as Hash)
- (⊢ (hash-count h-) : Int)])
+ (⊢ (hash-count- h-) : Int)])
(define-base-type String-Port)
(define-base-type Input-Port)
@@ -1237,34 +1243,34 @@
(define-primop get-output-string : (→ String-Port String))
(define-primop string-upcase : (→ String String))
-(define-typed-syntax write-string/tc #:export-as write-string
- [(_ str out)
- #'(write-string/tc str out (ext-stlc:#%datum . 0) (string-length/tc str))]
- [(_ str out start end)
+(define-typed-syntax write-string
+ [(write-string str out)
+ #'(write-string str out (ext-stlc:#%datum . 0) (string-length str))]
+ [(write-string str out start end)
#:with str- (⇑ str as String)
#:with out- (⇑ out as String-Port)
#:with start- (⇑ start as Int)
#:with end- (⇑ end as Int)
- (⊢ (write-string str- out- start- end-) : Unit)])
+ (⊢ (write-string- str- out- start- end-) : Unit)])
-(define-typed-syntax string-length/tc #:export-as string-length
- [(_ str)
+(define-typed-syntax string-length
+ [(string-length str)
#:with str- (⇑ str as String)
- (⊢ (string-length str-) : Int)])
+ (⊢ (string-length- str-) : Int)])
(define-primop make-string : (→ Int String))
(define-primop string-set! : (→ String Int Char Unit))
(define-primop string-ref : (→ String Int Char))
-(define-typed-syntax string-copy!/tc #:export-as string-copy!
- [(_ dest dest-start src)
- #'(string-copy!/tc
- dest dest-start src (ext-stlc:#%datum . 0) (string-length/tc src))]
- [(_ dest dest-start src src-start src-end)
+(define-typed-syntax string-copy!
+ [(string-copy! dest dest-start src)
+ #'(string-copy!
+ dest dest-start src (ext-stlc:#%datum . 0) (string-length src))]
+ [(string-copy! dest dest-start src src-start src-end)
#:with dest- (⇑ dest as String)
#:with src- (⇑ src as String)
#:with dest-start- (⇑ dest-start as Int)
#:with src-start- (⇑ src-start as Int)
#:with src-end- (⇑ src-end as Int)
- (⊢ (string-copy! dest- dest-start- src- src-start- src-end-) : Unit)])
+ (⊢ (string-copy!- dest- dest-start- src- src-start- src-end-) : Unit)])
(define-primop fl+ : (→ Float Float Float))
(define-primop fl- : (→ Float Float Float))
@@ -1278,37 +1284,38 @@
(define-primop real->decimal-string : (→ Float Int String))
(define-primop fx->fl : (→ Int Float))
(define-typed-syntax quotient+remainder
- [(_ x y)
+ [(quotient+remainder x y)
#:with x- (⇑ x as Int)
#:with y- (⇑ y as Int)
- (⊢ (call-with-values (λ () (quotient/remainder x- y-)) list)
+ (⊢ (let-values- ([[a b] (quotient/remainder- x- y-)])
+ (list- a b))
: (stlc+rec-iso:× Int Int))])
(define-primop quotient : (→ Int Int Int))
(define-typed-syntax set!
- [(_ x:id e)
+ [(set! x:id e)
#:with [x- ty_x] (infer+erase #'x)
#:with [e- ty_e] (infer+erase #'e)
#:when (typecheck? #'ty_e #'ty_x)
- (⊢ (set! x e-) : Unit)])
+ (⊢ (set!- x e-) : Unit)])
-(define-typed-syntax provide-type [(_ ty ...) #'(provide ty ...)])
+(define-typed-syntax provide-type [(provide-type ty ...) #'(provide- ty ...)])
(define-typed-syntax provide
- [(_ x:id ...)
+ [(provide x:id ...)
#:with ([x- ty_x] ...) (infers+erase #'(x ...))
; TODO: use hash-code to generate this tmp
#:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...))
- #'(begin
- (provide x ...)
+ #'(begin-
+ (provide- x ...)
(stlc+rec-iso:define-type-alias x-ty ty_x) ...
- (provide x-ty ...))])
+ (provide- x-ty ...))])
(define-typed-syntax require-typed
- [(_ x:id ... #:from mod)
+ [(require-typed x:id ... #:from mod)
#:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...))
#:with (y ...) (generate-temporaries #'(x ...))
- #'(begin
- (require (rename-in (only-in mod x ... x-ty ...) [x y] ...))
+ #'(begin-
+ (require- (rename-in- (only-in- mod x ... x-ty ...) [x y] ...))
(define-syntax x (make-rename-transformer (assign-type #'y #'x-ty))) ...)])
(define-base-type Regexp)
@@ -1316,18 +1323,18 @@
(define-primop regexp : (→ String Regexp))
(define-typed-syntax equal?
- [(_ e1 e2)
+ [(equal? e1 e2)
#:with [e1- ty1] (infer+erase #'e1)
#:with [e2- ty2] (infer+erase #'(add-expected e2 ty1))
#:fail-unless (typecheck? #'ty1 #'ty2) "arguments to equal? have different types"
- (⊢ (equal? e1- e2-) : Bool)])
+ (⊢ (equal?- e1- e2-) : Bool)])
(define-typed-syntax read
- [(_)
- (⊢ (let ([x (read)])
- (cond [(eof-object? x) ""]
- [(number? x) (number->string x)]
- [(symbol? x) (symbol->string x)])) : String)])
+ [(read)
+ (⊢ (let- ([x (read-)])
+ (cond- [(eof-object?- x) ""]
+ [(number?- x) (number->string- x)]
+ [(symbol?- x) (symbol->string- x)])) : String)])
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/tapl/stlc+box.rkt b/tapl/stlc+box.rkt
@@ -12,16 +12,16 @@
(define-type-constructor Ref)
(define-typed-syntax ref
- [(_ e)
+ [(ref e)
#:with (e- τ) (infer+erase #'e)
- (⊢ (box e-) : (Ref τ))])
+ (⊢ (box- e-) : (Ref τ))])
(define-typed-syntax deref
- [(_ e)
+ [(deref e)
#:with (e- (τ)) (⇑ e as Ref)
- (⊢ (unbox e-) : τ)])
-(define-typed-syntax :=
- [(_ e_ref e)
+ (⊢ (unbox- e-) : τ)])
+(define-typed-syntax := #:literals (:=)
+ [(:= e_ref e)
#:with (e_ref- (τ1)) (⇑ e_ref as Ref)
#:with (e- τ2) (infer+erase #'e)
#:when (typecheck? #'τ1 #'τ2)
- (⊢ (set-box! e_ref- e-) : Unit)])
-\ No newline at end of file
+ (⊢ (set-box!- e_ref- e-) : Unit)])
diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt
@@ -12,29 +12,29 @@
(define-type-constructor List)
-(define-typed-syntax nil/tc #:export-as nil
- [(~and ni (_ ~! τi:type-ann))
- (⊢ null : (List τi.norm))]
+(define-typed-syntax nil
+ [(nil ~! τi:type-ann)
+ (⊢ null- : (List τi.norm))]
; minimal type inference
- [ni:id #:with expected-τ (get-expected-type #'ni)
- #:when (syntax-e #'expected-τ) ; 'expected-type property exists (ie, not false)
- #:with ty_lst (local-expand #'expected-τ 'expression null) ; canonicalize
- #:fail-unless (List? #'ty_lst)
- (raise (exn:fail:type:infer
- (format "~a (~a:~a): Inferred ~a type for nil, which is not a List."
- (syntax-source stx) (syntax-line stx) (syntax-column stx)
- (type->str #'ty_lst))
- (current-continuation-marks)))
- #:with (~List τ) #'ty_lst
- (⊢ null : (List τ))]
+ [nil:id #:with expected-τ (get-expected-type #'nil)
+ #:when (syntax-e #'expected-τ) ; 'expected-type property exists (ie, not false)
+ #:with ty_lst (local-expand #'expected-τ 'expression null) ; canonicalize
+ #:fail-unless (List? #'ty_lst)
+ (raise (exn:fail:type:infer
+ (format "~a (~a:~a): Inferred ~a type for nil, which is not a List."
+ (syntax-source stx) (syntax-line stx) (syntax-column stx)
+ (type->str #'ty_lst))
+ (current-continuation-marks)))
+ #:with (~List τ) #'ty_lst
+ (⊢ null- : (List τ))]
[_:id #:fail-when #t
(raise (exn:fail:type:infer
(format "~a (~a:~a): nil requires type annotation"
(syntax-source stx) (syntax-line stx) (syntax-column stx))
(current-continuation-marks)))
- #'(void)])
-(define-typed-syntax cons/tc #:export-as cons
- [(_ e1 e2)
+ #'(void-)])
+(define-typed-syntax cons
+ [(cons e1 e2)
#:with [e1- τ1] (infer+erase #'e1)
; #:with e2ann (add-expected-type #'e2 #'(List τ1))
#:with (e2- (τ2)) (⇑ (add-expected e2 (List τ1)) as List)
@@ -44,48 +44,48 @@
(syntax->datum #'e2) (type->str #'(List τ2)))
;; propagate up inferred types of variables
#:with env (stx-flatten (filter (λ (x) x) (stx-map get-env #'(e1- e2-))))
- #:with result-cons (add-env #'(cons e1- e2-) #'env)
+ #:with result-cons (add-env #'(cons- e1- e2-) #'env)
(⊢ result-cons : (List τ1))])
(define-typed-syntax isnil
- [(_ e)
+ [(isnil e)
#:with (e- _) (⇑ e as List)
- (⊢ (null? e-) : Bool)])
+ (⊢ (null?- e-) : Bool)])
(define-typed-syntax head
- [(_ e)
+ [(head e)
#:with (e- (τ)) (⇑ e as List)
- (⊢ (car e-) : τ)])
+ (⊢ (car- e-) : τ)])
(define-typed-syntax tail
- [(_ e)
+ [(tail e)
#:with (e- τ-lst) (infer+erase #'e)
#:when (List? #'τ-lst)
- (⊢ (cdr e-) : τ-lst)])
-(define-typed-syntax list/tc #:export-as list
- [(_) #'nil/tc]
- [(~and lst (_ x . rst)) ; has expected type
- #:with expected-τ (get-expected-type #'lst)
+ (⊢ (cdr- e-) : τ-lst)])
+(define-typed-syntax list
+ [(list) #'nil]
+ [(_ x . rst) ; has expected type
+ #:with expected-τ (get-expected-type stx)
#:when (syntax-e #'expected-τ)
#:with (~List τ) (local-expand #'expected-τ 'expression null)
- #'(cons/tc (add-expected x τ) (list/tc . rst))]
+ #'(cons (add-expected x τ) (list . rst))]
[(_ x . rst) ; no expected type
- #'(cons/tc x (list/tc . rst))])
+ #'(cons x (list . rst))])
(define-typed-syntax reverse
- [(_ e)
+ [(reverse e)
#:with (e- τ-lst) (infer+erase #'e)
#:when (List? #'τ-lst)
- (⊢ (reverse e-) : τ-lst)])
+ (⊢ (reverse- e-) : τ-lst)])
(define-typed-syntax length
- [(_ e)
+ [(length e)
#:with (e- τ-lst) (infer+erase #'e)
#:when (List? #'τ-lst)
- (⊢ (length e-) : Int)])
+ (⊢ (length- e-) : Int)])
(define-typed-syntax list-ref
- [(_ e n)
+ [(list-ref e n)
#:with (e- (ty)) (⇑ e as List)
#:with n- (⇑ n as Int)
- (⊢ (list-ref e- n-) : ty)])
+ (⊢ (list-ref- e- n-) : ty)])
(define-typed-syntax member
- [(_ v e)
+ [(member v e)
#:with (e- (ty)) (⇑ e as List)
#:with [v- ty_v] (infer+erase #'(add-expected v ty))
#:when (typecheck? #'ty_v #'ty)
- (⊢ (member v- e-) : Bool)])
+ (⊢ (member- v- e-) : Bool)])
diff --git a/tapl/stlc+effect.rkt b/tapl/stlc+effect.rkt
@@ -45,7 +45,7 @@
[else (set-union locs1 locs2)])))
-(define-typed-syntax #%app
+(define-typed-syntax effect:#%app #:export-as #%app
[(_ efn e ...)
#:with [e_fn- ty_fn fns fas fds] (infer+erase/eff #'efn)
#:with tyns (get-new-effects #'ty_fn)
@@ -61,7 +61,7 @@
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
(mk-app-err-msg stx #:expected #'(τ_in ...)
#:given #'(τ_arg ...))
- (assign-type/eff #'(#%app e_fn- e_arg- ...) #'τ_out
+ (assign-type/eff #'(#%app- e_fn- e_arg- ...) #'τ_out
(stx-flatten #'(fns tyns . (ns ...)))
(stx-flatten #'(fas tyas . (as ...)))
(stx-flatten #'(fds tyds . (ds ...))))
@@ -74,19 +74,19 @@
(foldl loc-union (set) φ-derefs)))])
(define-typed-syntax λ
- [(_ bvs:type-ctx e)
+ [(λ bvs:type-ctx e)
#:with [xs- e- τ_res ns as ds] (infer/ctx+erase/eff #'bvs #'e)
- (assign-type #'(λ xs- e-)
+ (assign-type #'(λ- xs- e-)
(add-effects #'(→ bvs.type ... τ_res) #'ns #'as #'ds))])
#;(define-typed-syntax λ
- [(_ bvs:type-ctx e)
+ [(λ bvs:type-ctx e)
#:with (xs- e- τ_res) (infer/ctx+erase #'bvs #'e)
(let ([φ-news (get-new-effects #'e-)]
[φ-assigns (get-assign-effects #'e-)]
[φ-derefs (get-deref-effects #'e-)])
(assign-type
- #'(λ xs- e-)
+ #'(λ- xs- e-)
(add-effects #'(→ bvs.type ... τ_res) φ-news φ-assigns φ-derefs)))])
(define-type-constructor Ref)
@@ -107,22 +107,22 @@
(assign-type (add-effects e news assigns derefs) ty)))
(define-typed-syntax ref
- [(_ e)
+ [(ref e)
#:with (e- τ ns as ds) (infer+erase/eff #'e)
- (assign-type/eff #'(box e-) #'(Ref τ)
+ (assign-type/eff #'(box- e-) #'(Ref τ)
(cons (syntax-position stx) #'ns) #'as #'ds)])
(define-typed-syntax deref
- [(_ e)
+ [(deref e)
#:with (e- (~Ref ty) ns as ds) (infer+erase/eff #'e)
- (assign-type/eff #'(unbox e-) #'ty
+ (assign-type/eff #'(unbox- e-) #'ty
#'ns #'as (cons (syntax-position stx) #'ds))])
-(define-typed-syntax :=
- [(_ e_ref e)
+(define-typed-syntax := #:literals (:=)
+ [(:= e_ref e)
;#:with (e_ref- (τ1)) (⇑ e_ref as Ref)
#:with [e_ref- (~Ref ty1) ns1 as1 ds1] (infer+erase/eff #'e_ref)
#:with [e- ty2 ns2 as2 ds2] (infer+erase/eff #'e)
#:when (typecheck? #'ty1 #'ty2)
- (assign-type/eff #'(set-box! e_ref- e-) #'Unit
+ (assign-type/eff #'(set-box!- e_ref- e-) #'Unit
(stx-append #'ns1 #'ns2)
(cons (syntax-position stx) (stx-append #'as1 #'as2))
(stx-append #'ds1 #'ds2))])
diff --git a/tapl/stlc+lit.rkt b/tapl/stlc+lit.rkt
@@ -32,8 +32,8 @@
(define-primop + : (→ Int Int Int))
-(define-typed-syntax #%datum
- [(_ . n:integer) (⊢ #,(syntax/loc stx (#%datum . n)) : Int)]
- [(_ . x)
+(define-typed-syntax #%datum #:literals (#%datum)
+ [(#%datum . n:integer) (⊢ #,(syntax/loc stx (#%datum- . n)) : Int)]
+ [(#%datum . x)
#:when (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)
- #'(#%datum . x)])
+ #'(#%datum- . x)])
diff --git a/tapl/stlc+occurrence.rkt b/tapl/stlc+occurrence.rkt
@@ -26,9 +26,9 @@
(define-base-type Str)
(define-typed-syntax #%datum
- [(_ . n:boolean) (⊢ (#%datum . n) : Boolean)]
- [(_ . n:str) (⊢ (#%datum . n) : Str)]
- [(_ . x) #'(stlc+sub:#%datum . x)])
+ [(#%datum . n:boolean) (⊢ (#%datum- . n) : Boolean)]
+ [(#%datum . n:str) (⊢ (#%datum- . n) : Str)]
+ [(#%datum . x) #'(stlc+sub:#%datum . x)])
(define-type-constructor ∪ #:arity >= 1)
@@ -205,21 +205,21 @@
(define (simple-Π τ)
(syntax-parse (τ-eval τ)
[~Boolean
- #'boolean?]
+ #'boolean?-]
[~Int
- #'integer?]
+ #'integer?-]
[~Str
- #'string?]
+ #'string?-]
[~Num
- #'number?]
+ #'number?-]
[~Nat
- #'(lambda (n) (and (integer? n) (not (negative? n))))]
+ #'(lambda- (n) (and- (integer?- n) (not- (negative?- n))))]
[(~→ τ* ... τ)
(define k (stx-length #'(τ* ...)))
- #`(lambda (f) (and (procedure? f) (procedure-arity-includes? f #,k #f)))]
+ #`(lambda- (f) (and- (procedure?- f) (procedure-arity-includes?- f #,k #f)))]
[(~∪ τ* ...)
(define filter* (type*->filter* (syntax->list #'(τ* ...))))
- #`(lambda (v) (for/or ([f (in-list (list #,@filter*))]) (f v)))]
+ #`(lambda- (v) (for/or- ([f (in-list- (list- #,@filter*))]) (f v)))]
[_
(error 'Π "Cannot make filter for type ~a\n" (syntax->datum τ))]))
(current-Π simple-Π)
@@ -231,7 +231,7 @@
;; - allow x not identifier (1. does nothing 2. latent filters)
(define-typed-syntax test #:datum-literals (?)
;; -- THIS CASE BELONGS IN A NEW FILE
- [(_ [τ0+:type ? (unop x-stx:id n-stx:nat)] e1 e2)
+ [(test [τ0+:type ? (unop x-stx:id n-stx:nat)] e1 e2)
;; 1. Check that we're using a known eliminator
#:when (free-identifier=? #'stlc+tup:proj #'unop)
;; 2. Make sure we're filtering with a valid type
@@ -249,23 +249,23 @@
#:with [x1 e1+ τ1] (infer/ctx+erase #'([x-stx : τ+]) #'e1)
#:with [x2 e2+ τ2] (infer/ctx+erase #'([x-stx : τ-]) #'e2)
;; 6. Desugar, replacing the filtered identifier
- (⊢ (if (f e0+)
- ((lambda x1 e1+) x-stx)
- ((lambda x2 e2+) x-stx))
+ (⊢ (if- (f e0+)
+ ((lambda- x1 e1+) x-stx)
+ ((lambda- x2 e2+) x-stx))
: (∪ τ1 τ2))]
;; TODO lists
;; For now, we can't express the type (List* A (U A B)), so our filters are too strong
;; -- THE ORIGINAL
- [(_ [τ0+:type ? x-stx:id] e1 e2)
+ [(test [τ0+:type ? x-stx:id] e1 e2)
#:with f (type->filter #'τ0+)
#:with (x τ0) (infer+erase #'x-stx)
#:with τ0- (∖ #'τ0 #'τ0+)
#:with [x1 e1+ τ1] (infer/ctx+erase #'([x-stx : τ0+]) #'e1)
#:with [x2 e2+ τ2] (infer/ctx+erase #'([x-stx : τ0-]) #'e2)
;; Expand to a conditional, using the runtime predicate
- (⊢ (if (f x-stx)
- ((lambda x1 e1+) x-stx)
- ((lambda x2 e2+) x-stx))
+ (⊢ (if- (f x-stx)
+ ((lambda- x1 e1+) x-stx)
+ ((lambda- x2 e2+) x-stx))
: (∪ τ1 τ2))])
;; =============================================================================
@@ -309,11 +309,11 @@
(syntax-parse (τ-eval τ)
[(~× τ* ...)
(define filter* (type*->filter* (syntax->list #'(τ* ...))))
- #`(lambda (v*)
- (and (list? v*)
- (for/and ([v (in-list v*)]
- [f (in-list (list #,@filter*))])
- (f v))))]
+ #`(lambda- (v*)
+ (and- (list?- v*)
+ (for/and- ([v (in-list- v*)]
+ [f (in-list- (list- #,@filter*))])
+ (f v))))]
[_ ;; Fall back
(Π τ)]))))
(current-Π π-Π))
@@ -346,10 +346,10 @@
(syntax-parse (τ-eval τ)
[(~List τi)
(define f ((current-Π) #'τi))
- #`(lambda (v*)
- (and (list? v*)
- (for/and ([v (in-list v*)])
- (#,f v))))]
+ #`(lambda- (v*)
+ (and- (list?- v*)
+ (for/and- ([v (in-list- v*)])
+ (#,f v))))]
[_ ;; Fall back
(Π τ)]))))
(current-Π list-Π))
diff --git a/tapl/stlc+overloading.rkt b/tapl/stlc+overloading.rkt
@@ -11,8 +11,8 @@
(define-base-type Str)
(define-typed-syntax #%datum
- [(_ . n:str) (⊢ (#%datum . n) : Str)]
- [(_ . x) #'(stlc+sub:#%datum . x)])
+ [(#%datum . n:str) (⊢ (#%datum- . n) : Str)]
+ [(#%datum . x) #'(stlc+sub:#%datum . x)])
(define-for-syntax xerox syntax->datum)
@@ -105,26 +105,26 @@
;; === Overloaded signature environment
(define-typed-syntax signature
- [(_ (name:id α:id) τ)
+ [(signature (name:id α:id) τ)
#:with ((α+) (~→ τ_α:id τ-cod) _) (infer/tyctx+erase #'([α : #%type]) #'τ)
(define ℜ (ℜ-init #'name #'τ-cod))
(⊢ (define-syntax name
(syntax-parser
[_:id
- #'(quote #,ℜ)] ;; Is there a way to transmit ℜ directly?
+ #'(quote- #,ℜ)] ;; Is there a way to transmit ℜ directly?
[(n e)
#:with [e+ τ+] (infer+erase #'e)
#:with n+ (#,ℜ #'τ+)
- (⊢ (#%app n+ e+)
+ (⊢ (#%app- n+ e+)
: τ-cod)]
[(_ e* (... ...))
- #'(raise-arity-error (syntax->datum name) 1 e* (... ...))]))
+ #'(raise-arity-error- (syntax->datum- name) 1 e* (... ...))]))
: Bot)]
- [(_ e* ...)
+ [(signature e* ...)
(error 'signature (format "Expected (signature (NAME VAR) (→ VAR τ)), got ~a" (xerox #'(e* ...))))])
-(define-typed-syntax resolve/tc #:export-as resolve
- [(_ name:id τ)
+(define-typed-syntax resolve
+ [(resolve name:id τ)
#:with τ+ ((current-type-eval) #'τ)
;; Extract a resolver from the syntax object
(define ℜ (syntax->ℜ #'name))
@@ -132,7 +132,7 @@
(⊢ #,(ℜ #'τ+ #:exact? #t) : #,(ℜ->type ℜ #:subst #'τ+))])
(define-typed-syntax instance
- [(_ (name:id τ-stx) e)
+ [(instance (name:id τ-stx) e)
#:with τ ((current-type-eval) #'τ-stx)
#:with [e+ τ+] (infer+erase #'e)
(define ℜ (syntax->ℜ #'name))
@@ -157,7 +157,7 @@
)]))
;; Should we use syntax instead of e+ ?
(ℜ-add! ℜ #'τ #'e+)
- (⊢ (void) : Bot)]
+ (⊢ (void-) : Bot)]
[_
(error 'instance "Expected (instance (id τ) e).")])
diff --git a/tapl/stlc+rec-iso.rkt b/tapl/stlc+rec-iso.rkt
@@ -57,14 +57,14 @@
(current-typecheck-relation type=?))
(define-typed-syntax unfld
- [(_ τ:type-ann e)
+ [(unfld τ:type-ann e)
#:with (~μ* (tv) τ_body) #'τ.norm
#:with [e- τ_e] (infer+erase #'e)
#:when (typecheck? #'τ_e #'τ.norm)
(⊢ e- : #,(subst #'τ.norm #'tv #'τ_body))])
(define-typed-syntax fld
- [(_ τ:type-ann e)
+ [(fld τ:type-ann e)
#:with (~μ* (tv) τ_body) #'τ.norm
#:with [e- τ_e] (infer+erase #'e)
#:when (typecheck? #'τ_e (subst #'τ.norm #'tv #'τ_body))
- (⊢ e- : τ.norm)])
-\ No newline at end of file
+ (⊢ e- : τ.norm)])
diff --git a/tapl/stlc+reco+sub.rkt b/tapl/stlc+reco+sub.rkt
@@ -14,8 +14,8 @@
;; - records and variants from stlc+reco+var
(define-typed-syntax #%datum
- [(_ . n:number) #'(stlc+sub:#%datum . n)]
- [(_ . x) #'(stlc+reco+var:#%datum . x)])
+ [(#%datum . n:number) #'(stlc+sub:#%datum . n)]
+ [(#%datum . x) #'(stlc+reco+var:#%datum . x)])
(begin-for-syntax
(define old-sub? (current-sub?))
diff --git a/tapl/stlc+reco+var.rkt b/tapl/stlc+reco+var.rkt
@@ -28,12 +28,12 @@
[(_ x ...) #'ty]))]))
(define-typed-syntax define
- [(_ x:id e)
+ [(define x:id e)
#:with (e- τ) (infer+erase #'e)
#:with y (generate-temporary)
- #'(begin
+ #'(begin-
(define-syntax x (make-rename-transformer (⊢ y : τ)))
- (define y e-))])
+ (define- y e-))])
; re-define tuples as records
; dont use define-type-constructor because I want the : literal syntax
@@ -63,14 +63,14 @@
;; records
(define-typed-syntax tup #:datum-literals (=)
- [(_ [l:id = e] ...)
+ [(tup [l:id = e] ...)
#:with ([e- τ] ...) (infers+erase #'(e ...))
- (⊢ (list (list 'l e-) ...) : (× [l : τ] ...))])
+ (⊢ (list- (list- 'l e-) ...) : (× [l : τ] ...))])
(define-typed-syntax proj #:literals (quote)
- [(_ e_rec l:id)
+ [(proj e_rec l:id)
#:with (e_rec- ([l_τ τ] ...)) (⇑ e_rec as ×)
#:with (_ τ_match) (stx-assoc #'l #'([l_τ τ] ...))
- (⊢ (cadr (assoc 'l e_rec-)) : τ_match)])
+ (⊢ (cadr- (assoc- 'l e_rec-)) : τ_match)])
(define-type-constructor ∨/internal #:arity >= 0)
@@ -108,7 +108,7 @@
~!)])))) ; dont backtrack here
(define-typed-syntax var #:datum-literals (as =)
- [(_ l:id = e as τ:type)
+ [(var l:id = e as τ:type)
#:with (~∨* [l_τ : τ_l] ...) #'τ.norm
#:with match_res (stx-assoc #'l #'((l_τ τ_l) ...))
#:fail-unless (syntax-e #'match_res)
@@ -116,10 +116,10 @@
#:with (_ τ_match) #'match_res
#:with (e- τ_e) (infer+erase #'e)
#:when (typecheck? #'τ_e #'τ_match)
- (⊢ (list 'l e) : τ)])
+ (⊢ (list- 'l e) : τ)])
(define-typed-syntax case
#:datum-literals (of =>)
- [(_ e [l:id x:id => e_l] ...)
+ [(case e [l:id x:id => e_l] ...)
#:fail-when (null? (syntax->list #'(l ...))) "no clauses"
#:with (e- ([l_x τ_x] ...)) (⇑ e as ∨)
#:fail-unless (= (stx-length #'(l ...)) (stx-length #'(l_x ...))) "wrong number of case clauses"
@@ -127,6 +127,6 @@
#:with (((x-) e_l- τ_el) ...)
(stx-map (λ (bs e) (infer/ctx+erase bs e)) #'(([x : τ_x]) ...) #'(e_l ...))
#:fail-unless (same-types? #'(τ_el ...)) "branches have different types"
- (⊢ (let ([l_e (car e-)])
- (cond [(symbol=? l_e 'l) (let ([x- (cadr e-)]) e_l-)] ...))
+ (⊢ (let- ([l_e (car- e-)])
+ (cond- [(symbol=?- l_e 'l) (let- ([x- (cadr- e-)]) e_l-)] ...))
: #,(stx-car #'(τ_el ...)))])
diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt
@@ -26,10 +26,10 @@
(define-primop * : (→ Num Num Num))
(define-typed-syntax #%datum
- [(_ . n:nat) (⊢ (#%datum . n) : Nat)]
- [(_ . n:integer) (⊢ (#%datum . n) : Int)]
- [(_ . n:number) (⊢ (#%datum . n) : Num)]
- [(_ . x) #'(ext:#%datum . x)])
+ [(#%datum . n:nat) (⊢ (#%datum- . n) : Nat)]
+ [(#%datum . n:integer) (⊢ (#%datum- . n) : Int)]
+ [(#%datum . n:number) (⊢ (#%datum- . n) : Num)]
+ [(#%datum . x) #'(ext:#%datum . x)])
(begin-for-syntax
(define (sub? t1 t2)
diff --git a/tapl/stlc+tup.rkt b/tapl/stlc+tup.rkt
@@ -16,7 +16,7 @@
(make-list (stx-length (stx-cdr stx)) covariant)))
(define-typed-syntax tup
- [(_ e ...)
+ [(tup e ...)
#:with ty-expected (get-expected-type stx)
#:with (e_ann ...) (if (syntax-e #'ty-expected)
(syntax-parse (local-expand #'ty-expected 'expression null)
@@ -24,10 +24,10 @@
[_ #'(e ...)])
#'(e ...))
#:with ([e- τ] ...) (infers+erase #'(e_ann ...))
- (⊢ (list e- ...) : (× τ ...))])
+ (⊢ (list- e- ...) : (× τ ...))])
(define-typed-syntax proj
- [(_ e_tup n:nat)
+ [(proj e_tup n:nat)
#:with [e_tup- τs_tup] (⇑ e_tup as ×)
#:fail-unless (< (syntax-e #'n) (stx-length #'τs_tup)) "index too large"
- (⊢ (list-ref e_tup- n) : #,(stx-list-ref #'τs_tup (syntax-e #'n)))])
+ (⊢ (list-ref- e_tup- n) : #,(stx-list-ref #'τs_tup (syntax-e #'n)))])
diff --git a/tapl/stlc.rkt b/tapl/stlc.rkt
@@ -77,9 +77,9 @@
(list covariant))])))
(define-typed-syntax λ
- [(_ bvs:type-ctx e)
+ [(λ bvs:type-ctx e)
#:with (xs- e- τ_res) (infer/ctx+erase #'bvs #'e)
- (⊢ (λ xs- e-) : (→ bvs.type ... τ_res))])
+ (⊢ (λ- xs- e-) : (→ bvs.type ... τ_res))])
(define-for-syntax (mk-app-err-msg stx #:expected [expected-τs #'()]
#:given [given-τs #'()]
@@ -114,8 +114,8 @@
"\n")
"\n")]))
-(define-typed-syntax #%app
- [(_ e_fn e_arg ...)
+(define-typed-syntax #%app #:literals (#%app)
+ [(#%app e_fn e_arg ...)
#:with [e_fn- (τ_in ... τ_out)] (⇑ e_fn as →)
#:with ([e_arg- τ_arg] ...) (infers+erase #'(e_arg ...))
#:fail-unless (stx-length=? #'(τ_arg ...) #'(τ_in ...))
@@ -127,4 +127,4 @@
(type-error #:src stx
#:msg (mk-app-err-msg stx #:expected #'(τ_in ...)
#:given #'(τ_arg ...)))
- (⊢ (#%app e_fn- e_arg- ...) : τ_out)])
+ (⊢ (#%app- e_fn- e_arg- ...) : τ_out)])
diff --git a/tapl/sysf.rkt b/tapl/sysf.rkt
@@ -15,15 +15,15 @@
(define-type-constructor ∀ #:bvs >= 0)
(define-typed-syntax Λ
- [(_ (tv:id ...) e)
+ [(Λ (tv:id ...) e)
#:with ((tv- ...) e- τ) (infer/tyctx+erase #'([tv : #%type] ...) #'e)
(⊢ e- : (∀ (tv- ...) τ))])
(define-typed-syntax inst
- [(_ e τ:type ...)
+ [(inst e τ:type ...)
#:with (e- (tvs (τ_body))) (⇑ e as ∀)
;#:with [e- (~and t (~∀ tvs τ_body))] (infer+erase #'e)
;#:with (_ Xs τ_orig) (get-orig #'t) ; doesnt work with implicit lifted→
;#:with new-orig (substs #'(τ ...) #'Xs #'τ_orig)
;(⊢ e- : #,(add-orig (substs #'(τ.norm ...) #'tvs #'τ_body) #'new-orig))]
(⊢ e- : #,(substs #'(τ.norm ...) #'tvs #'τ_body))]
- [(_ e) #'e])
-\ No newline at end of file
+ [(_ e) #'e])
diff --git a/tapl/tests/mlish/hash.mlish b/tapl/tests/mlish/hash.mlish
@@ -9,7 +9,7 @@
(tup (number->string j 16) j)))])
(for/sum ([i (in-range 1 (add1 n))]
#:when
- (hash-ref hash (number->string i)))
+ (hash-has-key? hash (number->string i)))
1)))
(check-type (main (vector "2000")) : Int -> 799)
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -1,5 +1,10 @@
#lang racket/base
(require
+ "postfix-in.rkt"
+ (postfix-in - racket/base)
+ (postfix-in - racket/bool)
+ (postfix-in - racket/match)
+ (postfix-in - racket/promise)
(for-syntax (except-in racket extends)
syntax/parse racket/syntax syntax/stx racket/stxparam syntax/parse/define
"stx-utils.rkt")
@@ -7,7 +12,7 @@
(for-meta 3 racket/base syntax/parse racket/syntax)
racket/bool racket/provide racket/require racket/match racket/promise)
(provide
- symbol=? match delay
+ symbol=?- match- delay-
(except-out (all-from-out racket/base) #%module-begin)
(for-syntax (all-defined-out)) (all-defined-out)
(for-syntax
@@ -54,10 +59,10 @@
#'(begin
(provide (rename-out [name out-name]))
(define-syntax (name syntx)
- (syntax-parameterize ([stx (syntax-id-rules () [_ syntx])])
- (syntax-parse syntx #:context #'out-name stx-parse-clause ...))))]
+ (syntax-parameterize ([stx (make-rename-transformer #'syntx)])
+ (syntax-parse syntx stx-parse-clause ...))))]
[(_ name:id stx-parse-clause ...)
- #`(define-typed-syntax #,(generate-temporary #'name) #:export-as name
+ #'(define-typed-syntax name #:export-as name
stx-parse-clause ...)]))
;; need options for
