diff --git a/turnstile/scribblings/reference.scrbl b/turnstile/scribblings/reference.scrbl index 12d6e36..d320324 100644 --- a/turnstile/scribblings/reference.scrbl +++ b/turnstile/scribblings/reference.scrbl @@ -78,7 +78,9 @@ and then press Control-@litchar{\}. [expr-template ≫ expr-pattern ⇐ type-template] [expr-template ≫ expr-pattern ⇐ key type-template] [expr-template ≫ expr-pattern (⇐ key type-template) ooo ...]] - [type-relation (code:line [type-template τ⊑ type-template] ooo ...) + [type-relation (code:line [type-template τ= type-template] ooo ...) + (code:line [type-template τ= type-template #:for expr-template] ooo ...) + (code:line [type-template τ⊑ type-template] ooo ...) (code:line [type-template τ⊑ type-template #:for expr-template] ooo ...)] [conclusion [⊢ expr-template ⇒ key type-template] [⊢ [_ ≫ expr-template ⇒ type-template]] diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt index 5977921..318ebcb 100644 --- a/turnstile/turnstile.rkt +++ b/turnstile/turnstile.rkt @@ -232,7 +232,7 @@ ) (define-splicing-syntax-class clause #:attributes (pat) - #:datum-literals (τ⊑) + #:datum-literals (τ⊑ τ=) [pattern :tc-clause] [pattern [a τ⊑ b] #:with pat @@ -254,6 +254,26 @@ #'(~post (~fail #:unless (typechecks? #'[a ooo] #'[b ooo]) (typecheck-fail-msg/multi #'[b ooo] #'[a ooo] #'[e ooo])))] + [pattern [a τ= b] + #:with pat + #'(~post + (~fail #:unless ((current-type=?) #'a #'b) + (typecheck-fail-msg/1/no-expr #'b #'a)))] + [pattern [a τ= b #:for e] + #:with pat + #'(~post + (~fail #:unless ((current-type=?) #'a #'b) + (typecheck-fail-msg/1 #'b #'a #'e)))] + [pattern (~seq [a τ= b] ooo:elipsis) + #:with pat + #'(~post + (~fail #:unless (types=? #'[a ooo] #'[b ooo]) + (typecheck-fail-msg/multi/no-exprs #'[b ooo] #'[a ooo])))] + [pattern (~seq [a τ= b #:for e] ooo:elipsis) + #:with pat + #'(~post + (~fail #:unless (types=? #'[a ooo] #'[b ooo]) + (typecheck-fail-msg/multi #'[b ooo] #'[a ooo] #'[e ooo])))] [pattern (~seq #:when condition:expr) #:with pat #'(~fail #:unless condition)]