www

commit e8faad889b4fdd8a80fed1dd888e549d0b3b60c7
parent 41491136b6e82b57981f3641bb5db59741dffcdc
Author: Stephen Chang <stchang@ccs.neu.edu>
Date:   Mon,  3 Oct 2016 10:16:42 -0400

add τ= in addition to τ⊑

Diffstat:
M
turnstile/scribblings/reference.scrbl
 | 
4
+++-
M
turnstile/turnstile.rkt
 | 
22
+++++++++++++++++++++-

2 files changed, 24 insertions(+), 2 deletions(-)
diff --git 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
@@ -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)]