wip on addying var asserts to SPIN

racket/typed/syndicate/core-types.rkt

@@ -461,33 +461,70 @@
 (define-base-types OnStart OnStop OnDataflow)
 
 ;; (MakesField x τ)
-(define-type-constructor MakesField #:arity = 2)
+(define-type-constructor MakesField #:arity = 2
+  #:implements get-resugar-info
+  (syntax-parser
+    [(~and stx (~MakesField _ τ))
+     (list #'MakesField (get-orig-field-name #'stx) (resugar-type #'τ))]))
+(begin-for-syntax
+  (define FN-KEY 'FIELD-NAME)
+
+  (define (as-type x)
+    (with-syntax ([x* x])
+      (syntax-parse/typecheck null
+        [_ ≫
+           [[x* ≫ _ : Type] ⊢ x* ≫ x-]
+           ---
+           (≻ x-)])))
+
+  (define (mk-MakesField x t)
+    (define x-T (as-type x))
+    (attach (type-eval #`(MakesField #,x-T #,t)) FN-KEY x))
+
+  (define (get-orig-field-name MF)
+    (detach MF FN-KEY)))
 
 ;; (ReadsField x)
-(define-type-constructor ReadsField #:arity = 1)
+(define-type-constructor ReadsField #:arity = 1
+  #:implements get-resugar-info
+  (syntax-parser
+    [(~and stx (~ReadsField _))
+     (list #'ReadsField (get-orig-field-name #'stx))]))
 ;; need the original name so that we can re-typecheck an assert expression with
 ;; different types for that name. Could also subst the original name in after
 ;; constructing a valid type.
 (begin-for-syntax
-  (define RF-KEY 'ReadsField)
-  (define (mk-ReadsField x x-)
-    (attach (type-eval #`(ReadsField #,x-)) RF-KEY x))
-  (define (get-ReadsField-orig-field RF)
-    (detach RF RF-KEY)))
+  (define (mk-ReadsField x)
+    (define x-T (as-type x))
+    (attach (type-eval #`(ReadsField #,x-T)) FN-KEY x)))
 
 ;; (WritesField x τ)
-(define-type-constructor WritesField #:arity = 2)
+(define-type-constructor WritesField #:arity = 2
+  #:implements get-resugar-info
+  (syntax-parser
+    [(~and stx (~WritesField _ τ))
+     (list #'WritesField (get-orig-field-name #'stx) (resugar-type #'τ))]))
+
 (begin-for-syntax
-  (define WF-KEY 'WritesField)
-  (define (mk-WritesField x x- t)
-    (attach (type-eval #`(WritesField #,x- #,t)) WF-KEY x))
-  (define (get-WritesField-orig-field WF)
-    (detach WF WF-KEY)))
+  (define (mk-WritesField x t)
+    (define x-T (as-type x))
+    (attach (type-eval #`(WritesField #,x-T #,t)) FN-KEY x)))
 
 ;; (VarAssert x [--> τ-field τ-assert])
-(define-type-constructor VarAssert #:arity > 1)
+(define-type-constructor VarAssert #:arity > 1
+  #:implements get-resugar-info
+  (syntax-parser
+    [(~and stx (~VarAssert _ t1 ts ...))
+     (list* #'VarAssert (get-orig-field-name #'stx) (resugar-type #'t1) (stx-map resugar-type #'(ts ...)))]))
+
 (define-type-constructor --> #:arity = 2)
 
+(begin-for-syntax
+  (define (mk-VarAssert x t ts)
+    (define x-T (as-type x))
+    (attach (type-eval #`(VarAssert #,x-T #,t #,@ts)) FN-KEY x)))
+
+
 (define-type-constructor Actor #:arity = 1)
 (define-type-constructor ActorWithRole #:arity >= 1)
 ;; usage: (ActorWithRole τc τr)

racket/typed/syndicate/proto.rkt

@@ -13,6 +13,7 @@
 ;; Role Type Data Definitions
 
 ;; a FacetName is a symbol
+;; a Name is a Symbol
 
 ;; a T is one of
 ;;   - (Role FacetName (Listof EP)), also abbreviated as just Role
@@ -20,19 +21,24 @@
 ;;   - (Sends τ)
 ;;   - (Realizes τ)
 ;;   - (Stop FacetName Body)
+;;   - (WriteField Name τ)
 (struct Role (nm eps) #:prefab)
 (struct Spawn (ty) #:prefab)
 (struct Sends (ty) #:prefab)
 (struct Realizes (ty) #:prefab)
 (struct Stop (nm body) #:prefab)
+(struct WriteField (nm ty) #:prefab)
+(struct ReadField (nm) #:prefab)
 
 ;; a EP is one of
 ;;   - (Reacts D Body), describing an event handler
 ;;   - (Shares τ), describing an assertion
 ;;   - (Know τ), describing an internal assertion
+;;   - (Field Name τ), describing a field declaration
 (struct Reacts (evt body) #:prefab)
 (struct Shares (ty) #:prefab)
 (struct Know (ty) #:prefab)
+(struct Field (nm ty) #:prefab)
 
 ;; a Body describes actions carried out in response to some event, and
 ;; is one of
@@ -84,6 +90,8 @@
 ;;   - ⋆
 ;;   - (Base Symbol)
 ;;   - (internal-label Symbol τ)
+;;   - (VarTy Name (NEListof (List τ τ))), describing an assertion endpoint
+;;       whose type varies depending on the type of the named field
 (struct U (tys) #:prefab)
 (struct Struct (nm tys) #:prefab)
 (struct Observe (ty) #:prefab)
@@ -92,6 +100,7 @@
 (struct Hash (ty-k ty-v) #:prefab)
 (struct Mk⋆ () #:prefab)
 (struct internal-label (actor-id ty) #:prefab)
+(struct VarTy (nm tys) #:prefab)
 ;; TODO this might be a problem when used as a match pattern
 (define ⋆ (Mk⋆))
 (struct Base (name) #:prefab)

racket/typed/syndicate/roles.rkt

@@ -260,8 +260,7 @@
    #:fail-unless (all-pure? #'(e- ...)) "field initializers not allowed to have effects"
    #:with (x- ...) (generate-temporaries #'(x ...))
    #:with (τ ...) (stx-map type-eval #'((Field τ-f.norm) ...))
-   [[x ≫ _ : Type] ⊢ x ≫ x--] ...
-   #:with (MF ...) (stx-map mk-MakesField- #'((x-- τ-f.norm) ...))
+   #:with (MF ...) (stx-map mk-MakesField #'(x ...) #'(τ-f.norm ...))
    ----------------------------------------------------------------------
    [⊢ (erased (field/intermediate [x x- τ e-] ...))
       (⇒ : ★/t)
@@ -280,7 +279,7 @@
   #:with kont (syntax-parse #'(F ...)
                 [(~and ((~and RF (~ReadsField _)))
                        #;(~do (displayln 0))
-                       (~parse x (get-ReadsField-orig-field #'RF))
+                       (~parse x:id (get-orig-field-name #'RF))
                        (~typecheck [⊢ x ≫ x- (⇒ : (~Field τ-f))])
                        #;(~do (displayln 'B))
                        (~parse (~and τ-U (~U* τ1 τ2)) (find-union #'τ-f)))
@@ -316,9 +315,9 @@
                                         ----------------------------------------
                                         [≻ (#,specific τe_i)]]))
   #:do [(displayln 'D)]
-  [[x ≫ _ : Type] ⊢ x ≫ x--]
+  ;; [[x ≫ _ : Type] ⊢ x ≫ x--]
   #:do [(displayln 'E)]
-  #:with VA (type-eval #`(VarAssert x-- [--> τ-f τe] [--> τ-specific τe_i] ...))
+  #:with VA (mk-VarAssert #'x #'[--> τ-f τe] #'([--> τ-specific τe_i] ...))
   #:do [(pretty-display (type->strX #'VA))]
   -------------------------------------------------------------------------
   [⊢ (syndicate:assert e-)
@@ -695,8 +694,7 @@
   [⊢ e ≫ e- (⇒ : τ) (⇒ ν (~effs F ...))]
   [⊢ x ≫ x- (⇒ : (~Field τ-x:type))]
   #:fail-unless (<: #'τ #'τ-x) "Ill-typed field write"
-  [[x- ≫ _ : Type] ⊢ x- ≫ x--]
-  #:with WF (mk-WritesField #'x #'x-- #'τ-x)
+  #:with WF (mk-WritesField #'x #'τ-x)
   ----------------------------------------------------
   [⊢ (#%app- x- e-) (⇒ : ★/t) (⇒ ν (WF F ...))])
 
@@ -933,8 +931,7 @@
 
 (define-typed-syntax (ref x:id) ≫
   [⊢ x ≫ x- ⇒ (~Field τ)]
-  [[x- ≫ _ : Type] ⊢ x- ≫ x--]
-  #:with RF (mk-ReadsField #'x #'x--)
+  #:with RF (mk-ReadsField #'x)
   ------------------------
   [⊢ (#%app- x-)
      (⇒ : τ)
@@ -1060,6 +1057,11 @@
                     OnStart proto:StartEvt
                     OnStop proto:StopEvt
                     OnDataflow proto:DataflowEvt
+                    ;; Type Varying Assertion Stuff
+                    MakesField (lambda (nm ty) (proto:Field (syntax-e nm) ty))
+                    ReadsField (lambda (nm) (proto:ReadField (syntax-e nm)))
+                    WritesField (lambda (nm ty) (proto:WriteField (syntax-e nm) ty))
+                    --> list
                     ;; LTL
                     TT #t
                     FF #f
@@ -1084,7 +1086,8 @@
   (define (synd->proto ty)
     (let convert ([ty (resugar-type ty)])
       (syntax-parse ty
-        #:literals (★/t Bind Discard ∀/internal →/internal Role/internal Stop Reacts Actor ActorWithRole)
+        #:literals (★/t Bind Discard ∀/internal →/internal Role/internal Stop Reacts Actor ActorWithRole
+                        VarAssert)
         [(ctor:id t ...)
          #:when (dict-has-key? TRANSLATION# #'ctor)
          (apply (dict-ref TRANSLATION# #'ctor) (stx-map convert #'(t ...)))]
@@ -1119,6 +1122,9 @@
                (first converted-body)
                converted-body))
          (proto:Reacts (convert #'evt) body+)]
+        [(VarAssert nm t1 . ts)
+         (define convs (stx-map convert #'(t1 . ts)))
+         (proto:Shares (proto:VarTy (syntax-e #'nm) convs))]
         [t:id
          (proto:Base (syntax-e #'t))]
         [(ctor:id args ...)
@@ -1174,7 +1180,7 @@
 
 (define- (ensure-Role! r)
   (unless- (#%app- proto:Role? r)
-    (#%app- error- 'check-simulates "expected a Role type, got " r))
+    (#%app- error- 'check-simulates "expected a Role type, got ~a" r))
   r)
 
 (begin-for-syntax