drop more parens
This commit is contained in:
Stephen Chang
parent
f545503d19
commit
e1ea378f7d
|
|
@ -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]])
|
||||
|
|
|
|||
|
|
@ -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]])
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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]])
|
||||
|
||||
|
|
|
|||
|
|
@ -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]])
|
||||
|
||||
|
|
|
|||
|
|
@ -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]])
|
||||
|
|
|
|||
|
|
@ -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 ...))]])
|
||||
|
||||
|
|
|
|||
|
|
@ -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)]])
|
||||
|
|
|
|||
|
|
@ -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]])
|
||||
|
|
|
|||
|
|
@ -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 ...)]])
|
||||
|
|
|
|||
|
|
@ -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)]])
|
||||
|
|
|
|||
|
|
@ -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))]])
|
||||
|
||||
|
|
|
|||
|
|
@ -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]])
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user