From 13e988fe587f0af8ae26be099a3cbeee5c3b8979 Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samc@ccs.neu.edu>
Date: Thu, 23 May 2019 16:43:39 -0400
Subject: [PATCH] some work towards a better pattern language

---
 racket/typed/core-expressions.rkt  | 140 +++++++++++++++++++++++++++--
 racket/typed/core-types.rkt        |  78 ++++++++++++----
 racket/typed/roles.rkt             |   9 +-
 racket/typed/tests/expressions.rkt |  21 +++++
 4 files changed, 224 insertions(+), 24 deletions(-)

diff --git a/racket/typed/core-expressions.rkt b/racket/typed/core-expressions.rkt
index 2d35ff2..6022be8 100644
--- a/racket/typed/core-expressions.rkt
+++ b/racket/typed/core-expressions.rkt
@@ -138,18 +138,20 @@
 (define-typed-syntax (match e [p s ...+] ...+) ≫
   [⊢ e ≫ e- (⇒ : τ-e)]
   #:fail-unless (pure? #'e-) "expression must be pure"
-  #:with (([x τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
+  #:with (p/e ...) (for/list ([pat (in-syntax #'(p ...))])
+                     (elaborate-pattern/with-type pat #'τ-e))
+  #:with (([x τ:type] ...) ...) (stx-map pat-bindings #'(p/e ...))
   [[x ≫ x- : τ.norm] ... ⊢ (begin s ...) ≫ s- (⇒ : τ-s)
                 (⇒ ν-ep (~effs eps ...))
                 (⇒ ν-f (~effs fs ...))
                 (⇒ ν-s (~effs ss ...))] ...
   ;; REALLY not sure how to handle p/p-/p.match-pattern,
   ;; particularly w.r.t. typed terms that appear in p.match-pattern
-  [⊢ p ≫ p-- ⇒ τ-p] ...
+  [⊢ p/e ≫ p-- ⇒ τ-p] ...
   #:fail-unless (project-safe? #'τ-e (mk-U*- #'(τ-p ...))) "possibly unsafe pattern match"
   #:fail-unless (stx-andmap pure? #'(p-- ...)) "patterns must be pure"
   #:with (p- ...) (stx-map (lambda (p x-s xs) (substs x-s xs (compile-match-pattern p)))
-                           #'(p ...)
+                           #'(p/e ...)
                            #'((x- ...) ...)
                            #'((x ...) ...))
   --------------------------------------------------------------
@@ -200,7 +202,7 @@
     [(tuple p ...)
      #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
      #'([x τ] ... ...)]
-    [(k:kons1 p)
+    #;[(k:kons1 p)
      (pat-bindings #'p)]
     [(~constructor-exp cons p ...)
      #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
@@ -208,6 +210,134 @@
     [_
      #'()]))
 
+(begin-for-syntax
+  ;; Any -> Bool
+  (define (dollar-variable? x)
+    (and (identifier? x)
+         (char=? (string-ref (symbol->string (syntax-e x)) 0) #\$)))
+
+  ;; dollar-id -> Identifier
+  (define (un-dollar x)
+    (datum->syntax x (string->symbol (substring (symbol->string (syntax-e x)) 1))))
+
+  (define-syntax-class dollar-id
+    #:attributes (id)
+    (pattern x:id
+             #:when (dollar-variable? #'x)
+             #:attr id (un-dollar #'x)))
+
+  ;; match things of the for "$X...:Y..." where X and Y are things without
+  ;; spaces (i.e. likely but not definitely legal identifiers)
+  (define DOLLAR-ANN-RX #px"^\\$(\\S*):(\\S*)$")
+
+  ;; Any -> RegexpMatchResults
+  (define (dollar-ann-variable? x)
+    (and (identifier? x)
+         (regexp-match DOLLAR-ANN-RX (symbol->string (syntax-e x)))))
+
+  (define-syntax-class dollar-ann-id
+    #:attributes (id ty)
+    (pattern x:id
+             #:do [(define match? (dollar-ann-variable? #'x))]
+             #:when match?
+             #:attr id (datum->syntax #'x (string->symbol (second match?)))
+             #:attr ty (datum->syntax #'x (string->symbol (third match?)))))
+
+  ;; expand uses of $ short-hand
+  ;; doesn't handle uses of $id or ($) w/o a type
+  (define (elaborate-pattern pat)
+    (syntax-parse pat
+      #:datum-literals (tuple _ $)
+      [_
+       #'discard]
+      [x:dollar-ann-id
+       (syntax/loc pat (bind x.id x.ty))]
+      [($ x:id ty)
+       (syntax/loc pat (bind x ty))]
+      [(tuple p ...)
+       (quasisyntax/loc pat
+         (tuple #,@(stx-map elaborate-pattern #'(p ...))))]
+      [(k:kons1 p)
+       (quasisyntax/loc pat
+         (k #,(elaborate-pattern #'p)))]
+      [(~constructor-exp ctor p ...)
+       (quasisyntax/loc pat
+         (ctor #,@(stx-map elaborate-pattern #'(p ...))))]
+      [e:expr
+       #'e]))
+
+  (define (elaborate-pattern/with-type pat ty)
+    (syntax-parse pat
+      #:datum-literals (tuple $)
+      [(~datum _)
+       #'discard]
+      [x:dollar-ann-id
+       (syntax/loc pat (bind x.id x.ty))]
+      [x:dollar-id
+       (quasisyntax/loc pat (bind x.id #,ty))]
+      [($ x:id ty)
+       (syntax/loc pat (bind x ty))]
+      [($ x:id)
+       (quasisyntax/loc pat (bind x #,ty))]
+      [(tuple p ...)
+       (define (matching? t)
+         (syntax-parse t
+           [(~Tuple tt ...)
+            #:when (stx-length=? #'(p ...) #'(tt ...))
+            #t]
+           [_ #f]))
+       (define selected
+         (syntax-parse ty
+           [tt
+            #:when (matching? ty)
+            #'tt]
+           [(~U* (~or (~and tt (~fail #:unless (matching? #'tt)))
+                      _) ...)
+            (mk-U- #'(tt ...))]))
+       (define (proj t i)
+         (syntax-parse t
+           [(~Tuple tt ...)
+            (stx-list-ref #'(tt ...) i)]
+           [(~U* tt ...)
+            (mk-U- (stx-map (lambda (x) (proj x i)) #'(tt ...)))]))
+       (define sub-pats
+         (for/list ([pat (in-syntax #'(p ...))]
+                    [i (in-naturals)])
+           (elaborate-pattern/with-type pat (proj selected i))))
+       (quasisyntax/loc pat
+         (tuple #,@sub-pats))]
+      [(~constructor-exp ctor p ...)
+       (define tag (ctor-type-tag #'ctor))
+       (define (matching? t)
+         (syntax-parse t
+           [(~constructor-type tag2 tt ...)
+            #:when (equal? tag (syntax-e #'tag2))
+            #:when (stx-length=? #'(p ...) #'(tt ...))
+            #t]
+           [_ #f]))
+       (define selected
+         (syntax-parse ty
+           [tt
+            #:when (matching? ty)
+            #'tt]
+           [(~U* (~or (~and tt (~fail #:unless (matching? #'tt)))
+                      _) ...)
+            (mk-U- #'(tt ...))]))
+       (define (proj t i)
+         (syntax-parse t
+           [(~constructor-type _ tt ...)
+            (stx-list-ref #'(tt ...) i)]
+           [(~U* tt ...)
+            (mk-U- (stx-map (lambda (x) (proj x i)) #'(tt ...)))]))
+       (define sub-pats
+         (for/list ([pat (in-syntax #'(p ...))]
+                    [i (in-naturals)])
+           (elaborate-pattern/with-type pat (proj selected i))))
+       (quasisyntax/loc pat
+         (ctor #,@sub-pats))]
+      [e:expr
+       #'e])))
+
 ;; TODO - figure out why this needs different list identifiers
 (define-for-syntax (compile-pattern pat list-binding bind-id-transformer exp-transformer)
     (define (l-e stx) (local-expand stx 'expression '()))
@@ -216,7 +346,7 @@
         #:datum-literals (tuple discard bind)
         [(tuple p ...)
          #`(#,list-binding 'tuple #,@(stx-map loop #'(p ...)))]
-        [(k:kons1 p)
+        #;[(k:kons1 p)
          #`(#,(kons1->constructor #'k) #,(loop #'p))]
         [(bind x:id τ:type)
          (bind-id-transformer #'x)]
diff --git a/racket/typed/core-types.rkt b/racket/typed/core-types.rkt
index 7e06421..2f01c79 100644
--- a/racket/typed/core-types.rkt
+++ b/racket/typed/core-types.rkt
@@ -47,14 +47,32 @@
   (struct type-metadata (isec cons) #:transparent)
   ;; (IdTable type-metadata)
   (define TypeInfo# (make-free-id-table))
+  ;; (MutableHashOf Symbol type-metadata)
+  (define TypeInfo#* (make-hash))
   ;; Identifier isect-desc TypeCons -> Void
   (define (set-type-info! ty-cons isec cons)
     (free-id-table-set! TypeInfo#
                         ty-cons
                         (type-metadata isec cons)))
+  (define (set-type-info!* ty-cons isec cons)
+    (when (hash-has-key? TypeInfo#* ty-cons)
+      ;; TODO
+      #f)
+    (hash-set! TypeInfo#*
+               ty-cons
+               (type-metadata isec cons)))
+  ;; Identifier -> Symbol
+  ;; XYZ-.*
+  (define (un- id)
+    (define match?
+      (regexp-match #px"^(\\S*)-\\S*$" (symbol->string (syntax-e id))))
+    (string->symbol (second match?)))
+
   ;; Identifier -> (U #f type-metadata)
   (define (get-type-info ty-cons)
     (free-id-table-ref TypeInfo# ty-cons #f))
+  (define (get-type-info* ty-cons)
+    (hash-ref TypeInfo#* (un- ty-cons) #f))
 
   ;; Identifier -> (U #f isec-desc)
   (define (get-type-isec-desc ty-cons)
@@ -64,6 +82,14 @@
   (define (get-type-cons ty-cons)
     (define result? (get-type-info ty-cons))
     (and result? (type-metadata-cons result?)))
+  ;; Identifier -> (U #f isec-desc)
+  (define (get-type-isec-desc* ty-cons)
+    (define result? (get-type-info* ty-cons))
+    (and result? (type-metadata-isec result?)))
+  ;; Identifier -> (U #f TypeCons)
+  (define (get-type-cons* ty-cons)
+    (define result? (get-type-info* ty-cons))
+    (and result? (type-metadata-cons result?)))
 
   ;; a isect-desc describes how a type (constructor) behaves with respect to
   ;; intersection, and is one of
@@ -101,13 +127,13 @@
   ;; Identifier -> Bool
   ;; check if the type has a syntax property allowing us to create new instances
   (define (reassemblable? t)
-    (and (get-type-cons t) #t))
+    (and (get-type-cons* t) #t))
 
   ;; Identifier (Listof Type) -> Type
   ;; Create a new instance of the type with the given arguments
   ;; needs to have the type-cons-key
   (define (reassemble-type ty args)
-    (define tycons (get-type-cons ty))
+    (define tycons (get-type-cons* ty))
     (unless tycons
       (error "expected to find type-cons-key"))
     (tycons args)))
@@ -138,7 +164,8 @@
               (syntax/loc stx
                 (Name- t (... ...)))]))
          (begin-for-syntax
-           (set-type-info! #'Name- '#,(attribute desc.val) #'mk-)
+           #;(set-type-info! #'Name- '#,(attribute desc.val) #'mk-)
+           (set-type-info!* 'Name '#,(attribute desc.val) mk-)
            (define-syntax NamePat
              (pattern-expander
               (syntax-parser
@@ -204,11 +231,11 @@
 (define-for-syntax field-prop-name 'fields)
 (define-type-constructor Actor #:arity = 1)
 
-(define-product-type Message #:arity = 1)
+#;(define-product-type Message #:arity = 1)
 (define-product-type Tuple #:arity >= 0)
-(define-product-type Observe #:arity = 1)
-(define-product-type Inbound #:arity = 1)
-(define-product-type Outbound #:arity = 1)
+#;(define-product-type Observe #:arity = 1)
+#;(define-product-type Inbound #:arity = 1)
+#;(define-product-type Outbound #:arity = 1)
 (define-container-type AssertionSet #:arity = 1)
 (define-container-type Patch #:arity = 2)
 
@@ -372,7 +399,7 @@
     (pattern (~seq #:type-constructor TypeCons:id))
     (pattern (~seq) #:attr TypeCons #f))
 
-  (struct user-ctor (typed-ctor untyped-ctor)
+  (struct user-ctor (typed-ctor untyped-ctor type-tag)
     #:property prop:procedure
     (lambda (v stx)
       (define transformer (user-ctor-typed-ctor v))
@@ -406,7 +433,7 @@
          (struct- StructName (slot ...) #:reflection-name 'Cons #:transparent)
          (define-syntax (TypeConsExtraInfo stx)
            (syntax-parse stx
-             [(_ X (... ...)) #'('type-tag 'MakeTypeCons 'GetTypeParams)]))
+             [(_ X (... ...)) #'(#%app- 'type-tag 'MakeTypeCons 'GetTypeParams)]))
          (define-product-type TypeCons
            #:arity = #,arity
            #:extra-info 'TypeConsExtraInfo)
@@ -420,7 +447,7 @@
              [(_ (TypeConsExpander t (... ...)))
               #'(t (... ...))]))
          (define-syntax Cons
-           (user-ctor #'Cons- #'StructName))
+           (user-ctor #'Cons- #'StructName 'type-tag))
          (define-typed-syntax (Cons- e (... ...)) ≫
            #:fail-unless (= #,arity (stx-length #'(e (... ...)))) "arity mismatch"
            [⊢ e ≫ e- (⇒ : τ)] (... ...)
@@ -462,8 +489,8 @@
              (define arity (length accs)))
            (define-syntax (TypeConsExtraInfo stx)
              (syntax-parse stx
-               [(_ X (... ...)) #'('type-tag 'MakeTypeCons 'GetTypeParams)]))
-           (define-type-constructor TypeCons
+               [(_ X (... ...)) #'(#%app- 'type-tag 'MakeTypeCons 'GetTypeParams)]))
+           (define-product-type TypeCons
              ;; issue: arity needs to parse as an exact-nonnegative-integer
              ;; fix: check arity in MakeTypeCons
              #:arity >= 0
@@ -484,7 +511,7 @@
              ----------------------
              [⊢ (#%app- orig-struct-info e- (... ...)) (⇒ : (TypeCons τ (... ...)))])
            (define-syntax ucons
-             (user-ctor #'Cons- #'orig-struct-info)))))]))
+             (user-ctor #'Cons- #'orig-struct-info 'type-tag)))))]))
 
 (begin-for-syntax
   (define-syntax ~constructor-extra-info
@@ -542,7 +569,12 @@
          (user-ctor? (syntax-local-value stx (const #f)))))
 
   (define (untyped-ctor stx)
-    (user-ctor-untyped-ctor (syntax-local-value stx (const #f)))))
+    (user-ctor-untyped-ctor (syntax-local-value stx (const #f))))
+
+  ;; requires (ctor-id? stx)
+  ;; fetch the type tag
+  (define (ctor-type-tag stx)
+    (user-ctor-type-tag (syntax-local-value stx (const #f)))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Require & Provide
@@ -597,6 +629,11 @@
 ;; Syntax
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
+(require-struct observe #:as Observe #:from syndicate/actor-lang)
+(require-struct inbound #:as Inbound #:from syndicate/actor-lang)
+(require-struct outbound #:as Outbound #:from syndicate/actor-lang)
+(require-struct message #:as Message #:from syndicate/actor-lang)
+
 (begin-for-syntax
 
   ;; constructors with arity one
@@ -1084,7 +1121,7 @@
   [(_ e τ:type ...) ≫
    #:cut
    [⊢ e ≫ e- ⇒ (~∀ tvs τ_body)]
-   #:fail-unless (stx-andmap instantiable? #'(τ.norm ...) #'tvs)
+   #:fail-unless (stx-andmap instantiable? #'tvs #'(τ.norm ...))
                  "types must be instantiable"
    #:fail-unless (pure? #'e-) "expression must be pure"
    --------
@@ -1512,3 +1549,14 @@
                      (stx-contains-id? #'ty X)))
        (stx-map (λ _ irrelevant) Xs)]
       [_ (stx-map (λ _ invariant) Xs)])))
+
+#;(begin-for-syntax
+  (define k (sixth (free-id-table-keys TypeInfo#)))
+  (define t
+    (syntax-parse (type-eval #'(Observe (Bind (Tuple))))
+      [(~Any/bvs cons () tt ...)
+       #'cons]))
+  (displayln k)
+  (displayln (hash-ref (syntax-debug-info k) 'bindings))
+  (displayln t)
+  (displayln (hash-ref (syntax-debug-info t) 'bindings)))
diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt
index f891d77..dd37a04 100644
--- a/racket/typed/roles.rkt
+++ b/racket/typed/roles.rkt
@@ -360,25 +360,26 @@
   [⊢ (#%app- x-) (⇒ : τ)])
 
 ;; it would be nice to abstract over these three
-(define-typed-syntax (observe e:expr) ≫
+;; TODO - make the constructors
+#;(define-typed-syntax (observe e:expr) ≫
   [⊢ e ≫ e- (⇒ : τ)]
   #:fail-unless (pure? #'e-) "expression not allowed to have effects"
   ---------------------------------------------------------------------------
   [⊢ (syndicate:observe e-) (⇒ : (Observe τ))])
 
-(define-typed-syntax (inbound e:expr) ≫
+#;(define-typed-syntax (inbound e:expr) ≫
   [⊢ e ≫ e- (⇒ : τ)]
   #:fail-unless (pure? #'e-) "expression not allowed to have effects"
   ---------------------------------------------------------------------------
   [⊢ (syndicate:inbound e-) (⇒ : (Inbound τ))])
 
-(define-typed-syntax (outbound e:expr) ≫
+#;(define-typed-syntax (outbound e:expr) ≫
   [⊢ e ≫ e- (⇒ : τ)]
   #:fail-unless (pure? #'e-) "expression not allowed to have effects"
   ---------------------------------------------------------------------------
   [⊢ (syndicate:outbound e-) (⇒ : (Outbound τ))])
 
-(define-typed-syntax (message e:expr) ≫
+#;(define-typed-syntax (message e:expr) ≫
   [⊢ e ≫ e- (⇒ : τ)]
   #:fail-unless (pure? #'e-) "expression must be pure"
   ------------------------------
diff --git a/racket/typed/tests/expressions.rkt b/racket/typed/tests/expressions.rkt
index a5626ab..dcec5bd 100644
--- a/racket/typed/tests/expressions.rkt
+++ b/racket/typed/tests/expressions.rkt
@@ -70,3 +70,24 @@
 
 (typecheck-fail (inst id5 (→fn Int Int))
                 #:with-msg "types must be instantiable")
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Shorthands for match
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(check-type (match 5
+              [$x:Int (add1 x)])
+            : Int
+            ⇒ 6)
+
+(check-type (match (tuple 3 "hello")
+              [(tuple _ $str:String)
+               str])
+            : String
+            ⇒ "hello")
+
+(check-type (match (tuple 3 "hello")
+              [(tuple _ $str)
+               str])
+            : String
+            ⇒ "hello")