diff --git a/turnstile/examples/exist.rkt b/turnstile/examples/exist.rkt index 868ac40..9f1353a 100644 --- a/turnstile/examples/exist.rkt +++ b/turnstile/examples/exist.rkt @@ -18,9 +18,9 @@ [(pack (τ:type e) as ∃τ:type) ≫ #:with (~∃* (τ_abstract) τ_body) #'∃τ.norm #:with τ_e (subst #'τ.norm #'τ_abstract #'τ_body) - [⊢ [e ≫ e- ⇐ : τ_e]] + [⊢ e ≫ e- ⇐ τ_e] -------- - [⊢ [_ ≫ e- ⇒ : ∃τ.norm]]]) + [⊢ _ ≫ e- ⇒ ∃τ.norm]]) (define-typed-syntax open #:datum-literals (<= with) [(open [x:id <= e_packed with X:id] e) @@ -68,8 +68,8 @@ ;; ------------------------------ ;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e ;; - [⊢ [e_packed ≫ e_packed- ⇒ : (~∃ (Y) τ_body)]] + [⊢ e_packed ≫ e_packed- ⇒ (~∃ (Y) τ_body)] #:with τ_x (subst #'X #'Y #'τ_body) - [([X ≫ X- : #%type]) ([x ≫ x- : τ_x]) ⊢ [e ≫ e- ⇒ : τ_e]] + [([X ≫ X- : #%type]) ([x ≫ x- : τ_x]) ⊢ e ≫ e- ⇒ τ_e] -------- - [⊢ [_ ≫ (let- ([x- e_packed-]) e-) ⇒ : τ_e]]]) + [⊢ _ ≫ (let- ([x- e_packed-]) e-) ⇒ τ_e]]) diff --git a/turnstile/examples/ext-stlc.rkt b/turnstile/examples/ext-stlc.rkt index f380703..b0d28f2 100644 --- a/turnstile/examples/ext-stlc.rkt +++ b/turnstile/examples/ext-stlc.rkt @@ -25,17 +25,17 @@ (define-typed-syntax #%datum [(#%datum . b:boolean) ≫ -------- - [⊢ [_ ≫ (#%datum- . b) ⇒ : Bool]]] + [⊢ _ ≫ (#%datum- . b) ⇒ Bool]] [(#%datum . s:str) ≫ -------- - [⊢ [_ ≫ (#%datum- . s) ⇒ : String]]] + [⊢ _ ≫ (#%datum- . s) ⇒ String]] [(#%datum . f) ≫ #:when (flonum? (syntax-e #'f)) -------- - [⊢ [_ ≫ (#%datum- . f) ⇒ : Float]]] + [⊢ _ ≫ (#%datum- . f) ⇒ Float]] [(#%datum . c:char) ≫ -------- - [⊢ [_ ≫ (#%datum- . c) ⇒ : Char]]] + [⊢ _ ≫ (#%datum- . c) ⇒ Char]] [(#%datum . x) ≫ -------- [_ ≻ (stlc+lit:#%datum . x)]]) @@ -50,16 +50,16 @@ (define-typed-syntax and [(and e1 e2) ≫ - [⊢ [e1 ≫ e1- ⇐ : Bool]] - [⊢ [e2 ≫ e2- ⇐ : Bool]] + [⊢ e1 ≫ e1- ⇐ Bool] + [⊢ e2 ≫ e2- ⇐ Bool] -------- - [⊢ [_ ≫ (and- e1- e2-) ⇒ : Bool]]]) + [⊢ _ ≫ (and- e1- e2-) ⇒ Bool]]) (define-typed-syntax or [(or e ...) ≫ - [⊢ [e ≫ e- ⇐ : Bool] ...] + [⊢ [e ≫ e- ⇐ Bool] ...] -------- - [⊢ [_ ≫ (or- e- ...) ⇒ : Bool]]]) + [⊢ _ ≫ (or- e- ...) ⇒ Bool]]) (begin-for-syntax (define current-join @@ -79,45 +79,45 @@ ((current-join) τ τ2))])) (define-typed-syntax if - [(if e_tst e1 e2) ⇐ : τ-expected ≫ - [⊢ [e_tst ≫ e_tst- ⇒ : _]] ; Any non-false value is truthy. - [⊢ [e1 ≫ e1- ⇐ : τ-expected]] - [⊢ [e2 ≫ e2- ⇐ : τ-expected]] + [(if e_tst e1 e2) ⇐ τ-expected ≫ + [⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy. + [⊢ e1 ≫ e1- ⇐ τ-expected] + [⊢ e2 ≫ e2- ⇐ τ-expected] -------- - [⊢ [_ ≫ (if- e_tst- e1- e2-) ⇐ : _]]] + [⊢ _ ≫ (if- e_tst- e1- e2-) ⇐ _]] [(if e_tst e1 e2) ≫ - [⊢ [e_tst ≫ e_tst- ⇒ : _]] ; Any non-false value is truthy. - [⊢ [e1 ≫ e1- ⇒ : τ1]] - [⊢ [e2 ≫ e2- ⇒ : τ2]] + [⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy. + [⊢ e1 ≫ e1- ⇒ τ1] + [⊢ e2 ≫ e2- ⇒ τ2] -------- - [⊢ [_ ≫ (if- e_tst- e1- e2-) ⇒ : (⊔ τ1 τ2)]]]) + [⊢ _ ≫ (if- e_tst- e1- e2-) ⇒ (⊔ τ1 τ2)]]) (define-base-type Unit) (define-primop void : (→ Unit)) (define-typed-syntax begin - [(begin e_unit ... e) ⇐ : τ_expected ≫ - [⊢ [e_unit ≫ e_unit- ⇒ : _] ...] - [⊢ [e ≫ e- ⇐ : τ_expected]] + [(begin e_unit ... e) ⇐ τ_expected ≫ + [⊢ [e_unit ≫ e_unit- ⇒ _] ...] + [⊢ e ≫ e- ⇐ τ_expected] -------- - [⊢ [_ ≫ (begin- e_unit- ... e-) ⇐ : _]]] + [⊢ _ ≫ (begin- e_unit- ... e-) ⇐ _]] [(begin e_unit ... e) ≫ - [⊢ [e_unit ≫ e_unit- ⇒ : _] ...] - [⊢ [e ≫ e- ⇒ : τ_e]] + [⊢ [e_unit ≫ e_unit- ⇒ _] ...] + [⊢ e ≫ e- ⇒ τ_e] -------- - [⊢ [_ ≫ (begin- e_unit- ... e-) ⇒ : τ_e]]]) + [⊢ _ ≫ (begin- e_unit- ... e-) ⇒ τ_e]]) (define-typed-syntax let - [(let ([x e] ...) e_body) ⇐ : τ_expected ≫ + [(let ([x e] ...) e_body) ⇐ τ_expected ≫ [⊢ [e ≫ e- ⇒ : τ_x] ...] - [() ([x ≫ x- : τ_x] ...) ⊢ [e_body ≫ e_body- ⇐ : τ_expected]] + [[x ≫ x- : τ_x] ... ⊢ e_body ≫ e_body- ⇐ τ_expected] -------- - [⊢ [_ ≫ (let- ([x- e-] ...) e_body-) ⇐ : _]]] + [⊢ _ ≫ (let- ([x- e-] ...) e_body-) ⇐ _]] [(let ([x e] ...) e_body) ≫ [⊢ [e ≫ e- ⇒ : τ_x] ...] - [() ([x ≫ x- : τ_x] ...) ⊢ [e_body ≫ e_body- ⇒ : τ_body]] + [[x ≫ x- : τ_x] ... ⊢ e_body ≫ e_body- ⇒ τ_body] -------- - [⊢ [_ ≫ (let- ([x- e-] ...) e_body-) ⇒ : τ_body]]]) + [⊢ _ ≫ (let- ([x- e-] ...) e_body-) ⇒ τ_body]]) ; dont need to manually transfer expected type ; result template automatically propagates properties @@ -132,15 +132,15 @@ [_ ≻ (let ([x e]) (let* ([x_rst e_rst] ...) e_body))]]) (define-typed-syntax letrec - [(letrec ([b:type-bind e] ...) e_body) ⇐ : τ_expected ≫ - [() ([b.x ≫ x- : b.type] ...) - ⊢ [e ≫ e- ⇐ : b.type] ... [e_body ≫ e_body- ⇐ : τ_expected]] + [(letrec ([b:type-bind e] ...) e_body) ⇐ τ_expected ≫ + [[b.x ≫ x- : b.type] ... + ⊢ [e ≫ e- ⇐ b.type] ... [e_body ≫ e_body- ⇐ τ_expected]] -------- - [⊢ [_ ≫ (letrec- ([x- e-] ...) e_body-) ⇐ : _]]] + [⊢ _ ≫ (letrec- ([x- e-] ...) e_body-) ⇐ _]] [(letrec ([b:type-bind e] ...) e_body) ≫ - [() ([b.x ≫ x- : b.type] ...) - ⊢ [e ≫ e- ⇐ : b.type] ... [e_body ≫ e_body- ⇒ : τ_body]] + [[b.x ≫ x- : b.type] ... + ⊢ [e ≫ e- ⇐ b.type] ... [e_body ≫ e_body- ⇒ τ_body]] -------- - [⊢ [_ ≫ (letrec- ([x- e-] ...) e_body-) ⇒ : τ_body]]]) + [⊢ _ ≫ (letrec- ([x- e-] ...) e_body-) ⇒ τ_body]]) diff --git a/turnstile/examples/fsub.rkt b/turnstile/examples/fsub.rkt index f45138d..31ac5af 100644 --- a/turnstile/examples/fsub.rkt +++ b/turnstile/examples/fsub.rkt @@ -48,7 +48,7 @@ [(∀ ([tv:id <: τ:type] ...) τ_body) ≫ -------- ; eval first to overwrite the old #%type - [⊢ [_ ≫ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body)) ⇒ : (<: τ.norm ...)]]]) + [⊢ _ ≫ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body)) ⇒ (<: τ.norm ...)]]) (begin-for-syntax (define-syntax ~∀ (pattern-expander @@ -79,14 +79,14 @@ ;; environment with a syntax property using another tag: '<: ;; The "expose" function looks for this tag to enforce the bound, ;; as in TaPL (fig 28-1) - [([tv ≫ tv- : #%type <: τsub] ...) () ⊢ [e ≫ e- ⇒ : τ_e]] + [([tv ≫ tv- : #%type <: τsub] ...) () ⊢ e ≫ e- ⇒ τ_e] -------- - [⊢ [_ ≫ e- ⇒ : (∀ ([tv- <: τsub] ...) τ_e)]]]) + [⊢ _ ≫ e- ⇒ (∀ ([tv- <: τsub] ...) τ_e)]]) (define-typed-syntax inst [(inst e τ:type ...) ≫ - [⊢ [e ≫ e- ⇒ : (~∀ ([tv <: τ_sub] ...) τ_body)]] + [⊢ e ≫ e- ⇒ (~∀ ([tv <: τ_sub] ...) τ_body)] [τ.norm τ⊑ τ_sub #:for τ] ... #:with τ_inst (substs #'(τ.norm ...) #'(tv ...) #'τ_body) -------- - [⊢ [_ ≫ e- ⇒ : τ_inst]]]) + [⊢ _ ≫ e- ⇒ τ_inst]]) diff --git a/turnstile/examples/stlc+box.rkt b/turnstile/examples/stlc+box.rkt index db65a84..9565108 100644 --- a/turnstile/examples/stlc+box.rkt +++ b/turnstile/examples/stlc+box.rkt @@ -13,20 +13,20 @@ (define-typed-syntax ref [(ref e) ≫ - [⊢ [e ≫ e- ⇒ : τ]] + [⊢ e ≫ e- ⇒ τ] -------- - [⊢ [_ ≫ (box- e-) ⇒ : (Ref τ)]]]) + [⊢ _ ≫ (box- e-) ⇒ (Ref τ)]]) (define-typed-syntax deref [(deref e) ≫ - [⊢ [e ≫ e- ⇒ : (~Ref τ)]] + [⊢ e ≫ e- ⇒ (~Ref τ)] -------- - [⊢ [_ ≫ (unbox- e-) ⇒ : τ]]]) + [⊢ _ ≫ (unbox- e-) ⇒ τ]]) (define-typed-syntax := #:literals (:=) [(:= e_ref e) ≫ - [⊢ [e_ref ≫ e_ref- ⇒ : (~Ref τ)]] - [⊢ [e ≫ e- ⇐ : τ]] + [⊢ e_ref ≫ e_ref- ⇒ (~Ref τ)] + [⊢ e ≫ e- ⇐ τ] -------- - [⊢ [_ ≫ (set-box!- e_ref- e-) ⇒ : Unit]]]) + [⊢ _ ≫ (set-box!- e_ref- e-) ⇒ Unit]]) diff --git a/turnstile/examples/stlc+cons.rkt b/turnstile/examples/stlc+cons.rkt index b366783..568dd85 100644 --- a/turnstile/examples/stlc+cons.rkt +++ b/turnstile/examples/stlc+cons.rkt @@ -15,67 +15,67 @@ (define-typed-syntax nil [(nil ~! τi:type-ann) ≫ -------- - [⊢ [_ ≫ null- ⇒ : (List τi.norm)]]] + [⊢ _ ≫ null- ⇒ (List τi.norm)]] ; minimal type inference - [nil:id ⇐ : (~List τ) ≫ + [nil:id ⇐ (~List τ) ≫ -------- - [⊢ [_ ≫ null- ⇐ : _]]]) + [⊢ _ ≫ null- ⇐ _]]) (define-typed-syntax cons [(cons e1 e2) ≫ - [⊢ [e1 ≫ e1- ⇒ : τ1]] - [⊢ [e2 ≫ e2- ⇐ : (List τ1)]] + [⊢ e1 ≫ e1- ⇒ τ1] + [⊢ e2 ≫ e2- ⇐ (List τ1)] -------- - [⊢ [_ ≫ (cons- e1- e2-) ⇒ : (List τ1)]]]) + [⊢ _ ≫ (cons- e1- e2-) ⇒ (List τ1)]]) (define-typed-syntax isnil [(isnil e) ≫ - [⊢ [e ≫ e- ⇒ : (~List _)]] + [⊢ e ≫ e- ⇒ (~List _)] -------- - [⊢ [_ ≫ (null?- e-) ⇒ : Bool]]]) + [⊢ _ ≫ (null?- e-) ⇒ Bool]]) (define-typed-syntax head [(head e) ≫ - [⊢ [e ≫ e- ⇒ : (~List τ)]] + [⊢ e ≫ e- ⇒ (~List τ)] -------- - [⊢ [_ ≫ (car- e-) ⇒ : τ]]]) + [⊢ _ ≫ (car- e-) ⇒ τ]]) (define-typed-syntax tail [(tail e) ≫ - [⊢ [e ≫ e- ⇒ : τ-lst]] + [⊢ e ≫ e- ⇒ τ-lst] #:fail-unless (List? #'τ-lst) (format "Expected a list type, got: ~a" (type->str #'τ-lst)) -------- - [⊢ [_ ≫ (cdr- e-) ⇒ : τ-lst]]]) + [⊢ _ ≫ (cdr- e-) ⇒ τ-lst]]) (define-typed-syntax list [(list) ≫ -------- [_ ≻ nil]] - [(list x . rst) ⇐ : (~List τ) ≫ ; has expected type + [(list x . rst) ⇐ (~List τ) ≫ ; has expected type -------- - [⊢ [_ ≫ (cons (add-expected x τ) (list . rst)) ⇐ : _]]] + [⊢ _ ≫ (cons (add-expected x τ) (list . rst)) ⇐ _]] [(list x . rst) ≫ ; no expected type -------- [_ ≻ (cons x (list . rst))]]) (define-typed-syntax reverse [(reverse e) ≫ - [⊢ [e ≫ e- ⇒ : τ-lst]] + [⊢ e ≫ e- ⇒ τ-lst] #:fail-unless (List? #'τ-lst) (format "Expected a list type, got: ~a" (type->str #'τ-lst)) -------- - [⊢ [_ ≫ (reverse- e-) ⇒ : τ-lst]]]) + [⊢ _ ≫ (reverse- e-) ⇒ τ-lst]]) (define-typed-syntax length [(length e) ≫ - [⊢ [e ≫ e- ⇒ : τ-lst]] + [⊢ e ≫ e- ⇒ τ-lst] #:fail-unless (List? #'τ-lst) (format "Expected a list type, got: ~a" (type->str #'τ-lst)) -------- - [⊢ [_ ≫ (length- e-) ⇒ : Int]]]) + [⊢ _ ≫ (length- e-) ⇒ Int]]) (define-typed-syntax list-ref [(list-ref e n) ≫ - [⊢ [e ≫ e- ⇒ : (~List τ)]] - [⊢ [n ≫ n- ⇐ : Int]] + [⊢ e ≫ e- ⇒ (~List τ)] + [⊢ n ≫ n- ⇐ Int] -------- - [⊢ [_ ≫ (list-ref- e- n-) ⇒ : τ]]]) + [⊢ _ ≫ (list-ref- e- n-) ⇒ τ]]) (define-typed-syntax member [(member v e) ≫ - [⊢ [e ≫ e- ⇒ : (~List τ)]] - [⊢ [v ≫ v- ⇐ : τ]] + [⊢ e ≫ e- ⇒ (~List τ)] + [⊢ v ≫ v- ⇐ τ] -------- - [⊢ [_ ≫ (member- v- e-) ⇒ : Bool]]]) + [⊢ _ ≫ (member- v- e-) ⇒ Bool]]) diff --git a/turnstile/examples/stlc+effect.rkt b/turnstile/examples/stlc+effect.rkt index 0ca4753..eb20eae 100644 --- a/turnstile/examples/stlc+effect.rkt +++ b/turnstile/examples/stlc+effect.rkt @@ -30,14 +30,14 @@ (define-typed-syntax effect:#%app #:export-as #%app [(_ efn e ...) ≫ - [⊢ [efn ≫ e_fn- + [⊢ efn ≫ e_fn- (⇒ : (~→ τ_in ... τ_out) (⇒ ν (~locs tyns ...)) (⇒ := (~locs tyas ...)) (⇒ ! (~locs tyds ...))) (⇒ ν (~locs fns ...)) (⇒ := (~locs fas ...)) - (⇒ ! (~locs fds ...))]] + (⇒ ! (~locs fds ...))] #:fail-unless (stx-length=? #'[e ...] #'[τ_in ...]) (num-args-fail-msg #'efn #'[τ_in ...] #'[e ...]) [⊢ [e ≫ e_arg- @@ -47,71 +47,71 @@ (⇒ ! (~locs ds ...))] ...] -------- - [⊢ [_ ≫ (#%app- e_fn- e_arg- ...) + [⊢ _ ≫ (#%app- e_fn- e_arg- ...) (⇒ : τ_out) (⇒ ν (locs fns ... tyns ... ns ... ...)) (⇒ := (locs fas ... tyas ... as ... ...)) - (⇒ ! (locs fds ... tyds ... ds ... ...))]]]) + (⇒ ! (locs fds ... tyds ... ds ... ...))]]) (define-typed-syntax λ [(λ bvs:type-ctx e) ≫ - [() ([bvs.x ≫ x- : bvs.type] ...) ⊢ - [e ≫ e- + [[bvs.x ≫ x- : bvs.type] ... ⊢ + e ≫ e- (⇒ : τ_res) (⇒ ν (~locs ns ...)) (⇒ := (~locs as ...)) - (⇒ ! (~locs ds ...))]] + (⇒ ! (~locs ds ...))] -------- - [⊢ [_ ≫ (λ- (x- ...) e-) + [⊢ _ ≫ (λ- (x- ...) e-) (⇒ : (→ bvs.type ... τ_res) (⇒ ν (locs ns ...)) (⇒ := (locs as ...)) - (⇒ ! (locs ds ...)))]]]) + (⇒ ! (locs ds ...)))]]) (define-type-constructor Ref) (define-typed-syntax ref [(ref e) ≫ - [⊢ [e ≫ e- + [⊢ e ≫ e- (⇒ : τ) (⇒ ν (~locs ns ...)) (⇒ := (~locs as ...)) - (⇒ ! (~locs ds ...))]] + (⇒ ! (~locs ds ...))] -------- - [⊢ [_ ≫ (box- e-) + [⊢ _ ≫ (box- e-) (⇒ : (Ref τ)) (⇒ ν (locs #,(syntax-position stx) ns ...)) (⇒ := (locs as ...)) - (⇒ ! (locs ds ...))]]]) + (⇒ ! (locs ds ...))]]) (define-typed-syntax deref [(deref e) ≫ - [⊢ [e ≫ e- + [⊢ e ≫ e- (⇒ : (~Ref ty)) (⇒ ν (~locs ns ...)) (⇒ := (~locs as ...)) - (⇒ ! (~locs ds ...))]] + (⇒ ! (~locs ds ...))] -------- - [⊢ [_ ≫ (unbox- e-) + [⊢ _ ≫ (unbox- e-) (⇒ : ty) (⇒ ν (locs ns ...)) (⇒ := (locs as ...)) - (⇒ ! (locs #,(syntax-position stx) ds ...))]]]) + (⇒ ! (locs #,(syntax-position stx) ds ...))]]) (define-typed-syntax := #:literals (:=) [(:= e_ref e) ≫ - [⊢ [e_ref ≫ e_ref- + [⊢ e_ref ≫ e_ref- (⇒ : (~Ref ty)) (⇒ ν (~locs ns1 ...)) (⇒ := (~locs as1 ...)) - (⇒ ! (~locs ds1 ...))]] - [⊢ [e ≫ e- + (⇒ ! (~locs ds1 ...))] + [⊢ e ≫ e- (⇐ : ty) (⇒ ν (~locs ns2 ...)) (⇒ := (~locs as2 ...)) - (⇒ ! (~locs ds2 ...))]] + (⇒ ! (~locs ds2 ...))] -------- - [⊢ [_ ≫ (set-box!- e_ref- e-) + [⊢ _ ≫ (set-box!- e_ref- e-) (⇒ : Unit) (⇒ ν (locs ns1 ... ns2 ...)) (⇒ := (locs #,(syntax-position stx) as1 ... as2 ...)) - (⇒ ! (locs ds1 ... ds2 ...))]]]) + (⇒ ! (locs ds1 ... ds2 ...))]]) diff --git a/turnstile/examples/stlc+lit.rkt b/turnstile/examples/stlc+lit.rkt index 4f3d33d..218eb37 100644 --- a/turnstile/examples/stlc+lit.rkt +++ b/turnstile/examples/stlc+lit.rkt @@ -35,7 +35,7 @@ (define-typed-syntax #%datum [(#%datum . n:integer) ≫ -------- - [⊢ [_ ≫ (#%datum- . n) ⇒ : Int]]] + [⊢ _ ≫ (#%datum- . n) ⇒ Int]] [(_ . x) ≫ -------- [_ #:error (type-error #:src #'x #:msg "Unsupported literal: ~v" #'x)]]) diff --git a/turnstile/examples/stlc+rec-iso.rkt b/turnstile/examples/stlc+rec-iso.rkt index 7e5306b..fb00631 100644 --- a/turnstile/examples/stlc+rec-iso.rkt +++ b/turnstile/examples/stlc+rec-iso.rkt @@ -39,13 +39,13 @@ (define-typed-syntax unfld [(unfld τ:type-ann e) ≫ #:with (~μ* (tv) τ_body) #'τ.norm - [⊢ [e ≫ e- ⇐ : τ.norm]] + [⊢ e ≫ e- ⇐ τ.norm] -------- - [⊢ [_ ≫ e- ⇒ : #,(subst #'τ.norm #'tv #'τ_body)]]]) + [⊢ _ ≫ e- ⇒ #,(subst #'τ.norm #'tv #'τ_body)]]) (define-typed-syntax fld [(fld τ:type-ann e) ≫ #:with (~μ* (tv) τ_body) #'τ.norm #:with τ_e (subst #'τ.norm #'tv #'τ_body) - [⊢ [e ≫ e- ⇐ : τ_e]] + [⊢ e ≫ e- ⇐ τ_e] -------- - [⊢ [_ ≫ e- ⇒ : τ.norm]]]) + [⊢ _ ≫ e- ⇒ τ.norm]]) diff --git a/turnstile/examples/stlc+reco+var.rkt b/turnstile/examples/stlc+reco+var.rkt index c68bff9..a7b988b 100644 --- a/turnstile/examples/stlc+reco+var.rkt +++ b/turnstile/examples/stlc+reco+var.rkt @@ -38,7 +38,7 @@ (define-syntax x (make-rename-transformer (⊢ y : τ.norm))) (define- y (ann e : τ.norm)))]] [(define x:id e) ≫ - [⊢ [e ≫ e- ⇒ : τ]] + [⊢ e ≫ e- ⇒ τ] #:with y (generate-temporary #'x) -------- [_ ≻ (begin- @@ -89,18 +89,18 @@ ;; records (define-typed-syntax tup #:datum-literals (=) [(tup [l:id = e] ...) ≫ - [⊢ [e ≫ e- ⇒ : τ] ...] + [⊢ [e ≫ e- ⇒ τ] ...] -------- - [⊢ [_ ≫ (list- (list- 'l e-) ...) ⇒ : (× [l : τ] ...)]]]) + [⊢ _ ≫ (list- (list- 'l e-) ...) ⇒ (× [l : τ] ...)]]) (define-typed-syntax proj #:literals (quote) [(proj e_rec l:id) ≫ - [⊢ [e_rec ≫ e_rec- ⇒ : τ_e]] + [⊢ e_rec ≫ e_rec- ⇒ τ_e] #:fail-unless (×? #'τ_e) (format "Expected expression ~s to have × type, got: ~a" (syntax->datum #'e_rec) (type->str #'τ_e)) #:with τ_l (×-ref #'τ_e #'l) -------- - [⊢ [_ ≫ (cadr- (assoc- 'l e_rec-)) ⇒ : τ_l]]]) + [⊢ _ ≫ (cadr- (assoc- 'l e_rec-)) ⇒ τ_l]]) (define-type-constructor ∨/internal #:arity >= 0) @@ -149,7 +149,7 @@ [(var l:id = e as τ:type) ≫ -------- [_ ≻ (ann (var l = e) : τ.norm)]] - [(var l:id = e) ⇐ : τ ≫ + [(var l:id = e) ⇐ τ ≫ #:fail-unless (∨? #'τ) (format "Expected the expected type to be a ∨ type, got: ~a" (type->str #'τ)) #:with τ_e @@ -157,20 +157,20 @@ (λ () (raise-syntax-error #f (format "~a field does not exist" (syntax->datum #'l)) stx))) - [⊢ [e ≫ e- ⇐ : τ_e]] + [⊢ e ≫ e- ⇐ τ_e] -------- - [⊢ [_ ≫ (list- 'l e) ⇐ : _]]]) + [⊢ _ ≫ (list- 'l e) ⇐ _]]) (define-typed-syntax case #:datum-literals (of =>) [(case e [l:id x:id => e_l] ...) ≫ #:fail-unless (not (null? (syntax->list #'(l ...)))) "no clauses" - [⊢ [e ≫ e- ⇒ : (~∨* [l_x : τ_x] ...)]] + [⊢ e ≫ e- ⇒ (~∨* [l_x : τ_x] ...)] #:fail-unless (stx-length=? #'(l ...) #'(l_x ...)) "wrong number of case clauses" #:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive" - [() ([x ≫ x- : τ_x]) ⊢ [e_l ≫ e_l- ⇒ : τ_el]] ... + [[x ≫ x- : τ_x] ⊢ e_l ≫ e_l- ⇒ τ_el] ... -------- - [⊢ [_ ≫ + [⊢ _ ≫ (let- ([l_e (car- e-)]) (cond- [(symbol=?- l_e 'l) (let- ([x- (cadr- e-)]) e_l-)] ...)) - ⇒ : (⊔ τ_el ...)]]]) + ⇒ (⊔ τ_el ...)]]) diff --git a/turnstile/examples/stlc+sub.rkt b/turnstile/examples/stlc+sub.rkt index 7bb477d..a451dd0 100644 --- a/turnstile/examples/stlc+sub.rkt +++ b/turnstile/examples/stlc+sub.rkt @@ -30,13 +30,13 @@ (define-typed-syntax #%datum [(#%datum . n:nat) ≫ -------- - [⊢ [_ ≫ (#%datum- . n) ⇒ : Nat]]] + [⊢ _ ≫ (#%datum- . n) ⇒ Nat]] [(#%datum . n:integer) ≫ -------- - [⊢ [_ ≫ (#%datum- . n) ⇒ : Int]]] + [⊢ _ ≫ (#%datum- . n) ⇒ Int]] [(#%datum . n:number) ≫ -------- - [⊢ [_ ≫ (#%datum- . n) ⇒ : Num]]] + [⊢ _ ≫ (#%datum- . n) ⇒ Num]] [(#%datum . x) ≫ -------- [_ ≻ (ext:#%datum . x)]]) diff --git a/turnstile/examples/stlc+tup.rkt b/turnstile/examples/stlc+tup.rkt index 985db16..bd04074 100644 --- a/turnstile/examples/stlc+tup.rkt +++ b/turnstile/examples/stlc+tup.rkt @@ -16,20 +16,20 @@ (make-list (stx-length (stx-cdr stx)) covariant))) (define-typed-syntax tup - [(tup e ...) ⇐ : (~× τ ...) ≫ + [(tup e ...) ⇐ (~× τ ...) ≫ #:when (stx-length=? #'[e ...] #'[τ ...]) - [⊢ [e ≫ e- ⇐ : τ] ...] + [⊢ [e ≫ e- ⇐ τ] ...] -------- - [⊢ [_ ≫ (list- e- ...) ⇐ : _]]] + [⊢ _ ≫ (list- e- ...) ⇐ _]] [(tup e ...) ≫ - [⊢ [e ≫ e- ⇒ : τ] ...] + [⊢ [e ≫ e- ⇒ τ] ...] -------- - [⊢ [_ ≫ (list- e- ...) ⇒ : (× τ ...)]]]) + [⊢ _ ≫ (list- e- ...) ⇒ (× τ ...)]]) (define-typed-syntax proj [(proj e_tup n:nat) ≫ - [⊢ [e_tup ≫ e_tup- ⇒ : (~× τ ...)]] + [⊢ e_tup ≫ e_tup- ⇒ (~× τ ...)] #:fail-unless (< (syntax-e #'n) (stx-length #'[τ ...])) "index too large" -------- - [⊢ [_ ≫ (list-ref- e_tup- n) ⇒ : #,(stx-list-ref #'[τ ...] (syntax-e #'n))]]]) + [⊢ _ ≫ (list-ref- e_tup- n) ⇒ #,(stx-list-ref #'[τ ...] (syntax-e #'n))]]) diff --git a/turnstile/examples/sysf.rkt b/turnstile/examples/sysf.rkt index 85f9579..a4bd85a 100644 --- a/turnstile/examples/sysf.rkt +++ b/turnstile/examples/sysf.rkt @@ -16,16 +16,16 @@ (define-typed-syntax Λ [(Λ (tv:id ...) e) ≫ - [([tv ≫ tv- : #%type] ...) () ⊢ [e ≫ e- ⇒ : τ]] + [([tv ≫ tv- : #%type] ...) () ⊢ e ≫ e- ⇒ τ] -------- - [⊢ [_ ≫ e- ⇒ : (∀ (tv- ...) τ)]]]) + [⊢ _ ≫ e- ⇒ (∀ (tv- ...) τ)]]) (define-typed-syntax inst [(inst e τ:type ...) ≫ - [⊢ [e ≫ e- ⇒ : (~∀ tvs τ_body)]] + [⊢ e ≫ e- ⇒ (~∀ tvs τ_body)] #:with τ_inst (substs #'(τ.norm ...) #'tvs #'τ_body) -------- - [⊢ [_ ≫ e- ⇒ : τ_inst]]] + [⊢ _ ≫ e- ⇒ τ_inst]] [(inst e) ≫ -------- [_ ≻ e]])