From 0d839cbb12a641cbe71aaf00460fea247cdd1d67 Mon Sep 17 00:00:00 2001 From: Sam Caldwell Date: Fri, 15 Jul 2022 16:31:17 -0400 Subject: [PATCH] wip on with-facets --- racket/typed/examples/with-facets.rkt | 16 ++++++++++ racket/typed/syndicate/core-types.rkt | 8 +++++ racket/typed/syndicate/roles.rkt | 46 ++++++++++++++++++++------- 3 files changed, 58 insertions(+), 12 deletions(-) create mode 100644 racket/typed/examples/with-facets.rkt diff --git a/racket/typed/examples/with-facets.rkt b/racket/typed/examples/with-facets.rkt new file mode 100644 index 0000000..bab1f44 --- /dev/null +++ b/racket/typed/examples/with-facets.rkt @@ -0,0 +1,16 @@ +#lang typed/syndicate + +(lambda () +(spawn + (with-facets + ([onn (facet (assert (tuple 'on)))] + [off (facet (on (asserted (tuple 'go)) + (stop off + (start onn))))]) + off))) + +;; BAD +#;(spawn + (with-facets + [on (facet (on start (start on)))] + on)) diff --git a/racket/typed/syndicate/core-types.rkt b/racket/typed/syndicate/core-types.rkt index 34b1d76..9279150 100644 --- a/racket/typed/syndicate/core-types.rkt +++ b/racket/typed/syndicate/core-types.rkt @@ -380,6 +380,14 @@ (define-type FacetImpls : Type * -> Type) (define-type WSFBody : Type StartableFacet -> Type) +(define-for-syntax (WithStartableFacet? stx) + (syntax-parse stx + [(~WithStartableFacet (_ : _) _) #t] + [_ #f])) + +(define-for-syntax (TypeStartsFacet? t) + (or (Role? t) (WithStartableFacet? t))) + (define-syntax (WithFacets stx) (syntax-parse stx [(WithFacets ([X:id FacetBody] ...+) Y:id) diff --git a/racket/typed/syndicate/roles.rkt b/racket/typed/syndicate/roles.rkt index 550c2b0..3106429 100644 --- a/racket/typed/syndicate/roles.rkt +++ b/racket/typed/syndicate/roles.rkt @@ -314,7 +314,7 @@ (define-typed-syntax on #:datum-literals (start stop) - [(on start s ...) ≫ + [(on start s ...+) ≫ [⊢ (block s ...) ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-f (~effs τ-f ...)) (⇒ ν-s (~effs τ-s ...))] @@ -322,7 +322,7 @@ ----------------------------------- [⊢ (syndicate:on-start s-) (⇒ : ★/t) (⇒ ν-ep (τ-r))]] - [(on stop s ...) ≫ + [(on stop s ...+) ≫ [⊢ (block s ...) ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-f (~effs τ-f ...)) (⇒ ν-s (~effs τ-s ...))] @@ -332,7 +332,7 @@ (⇒ ν-ep (τ-r))]] [(on (evt:event-cons p) priority:priority - s ...) ≫ + s ...+) ≫ #:do [(define msg? (free-identifier=? #'syndicate:message (attribute evt.syndicate-kw))) (define elab (elaborate-pattern/with-com-ty (if msg? #'(message p) #'p)))] @@ -384,7 +384,7 @@ [⊢ (block s) ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs)) (⇒ ν-f (~effs τ-f ...))] ] ;; TODO: s shouldn't refer to facets or fields! - #:fail-unless (and (stx-andmap Role? #'(τ-f ...)) + #:fail-unless (and (stx-andmap TypeStartsFacet? #'(τ-f ...)) (= 1 (length (syntax->list #'(τ-f ...))))) "expected exactly one Role for body" #:with (τ-i τ-o τ-i/i τ-o/i τ-a) (analyze-roles #'(τ-f ...)) @@ -411,7 +411,8 @@ #:cut [⊢ (block s) ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs)) (⇒ ν-f (~effs τ-f ...))] ;; TODO: s shouldn't refer to facets or fields! - #:fail-unless (and (stx-andmap Role? #'(τ-f ...)) + #:do [(displayln #'(τ-f ...))] + #:fail-unless (and (stx-andmap TypeStartsFacet? #'(τ-f ...)) (= 1 (length (syntax->list #'(τ-f ...))))) "expected exactly one Role for body" #:with (τ-i τ-o τ-i/i τ-o/i τ-a) (analyze-roles #'(τ-f ...)) @@ -535,34 +536,55 @@ ;; With Facets ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(define-for-syntax (walk/with-facets e... [unique (gensym 'walk/with-facets)]) + (define-values (rev-e-... facet-effects) + (let loop ([e... (syntax->list e...)] + [rev-e-... '()] + [facet-effects '()]) + (match e... + ['() + (values rev-e-... facet-effects)] + [(cons e more) + (define e- (local-expand e (list unique) (list #'erased))) + (syntax-parse e- + #:literals (erased) + [(erased impl) + (define f-effs (syntax->list (get-effect e- 'ν-f))) + (loop more + (cons #'impl rev-e-...) + (append f-effs facet-effects))])]))) + (values (reverse rev-e-...) + facet-effects)) + (define-typed-syntax (with-facets ([x:id impl:expr] ...) fst:id) ≫ #:fail-unless (for/or ([y (in-syntax #'(x ...))]) (free-identifier=? #'fst y)) "must select one facet to start" [[x ≫ x- : StartableFacet] ... ⊢ (with-facets-impls ([x impl] ...) fst) ≫ impl- (⇒ ν-f (~effs wsf-body))] + #:with WSFs (type-eval #'(WithStartableFacets [x ...] wsf-body)) ---------------------------------------- - [⊢ impl- (⇒ ν-f ((WithStartableFacets [x ...] wsf-body)))]) + [⊢ impl- (⇒ : ★/t) (⇒ ν-f (WSFs))]) (define-typed-syntax (with-facets-impls ([x impl] ...) fst) ≫ ;; need to set use-stop-list to true mb? - [⊢ (facet-impl x impl) ≫ x-impl- (⇒ ν-f (~effs FI))] ... + #:do [(define-values (bodies FIs) (walk/with-facets #'([facet-impl x impl] ...)))] + ;; [⊢ (facet-impl x impl) ≫ x-impl- (⇒ ν-f (~effs FI))] ... [⊢ fst ≫ fst-] ---------------------------------------- [⊢ (let- () - x-impl- ... + #,@bodies (#%app- fst-)) - (⇒ ν-f ((WSFBody (FacetImpls FI ...) fst)))]) + (⇒ ν-f ((WSFBody (FacetImpls #,@FIs) fst)))]) (define-typed-syntax (facet-impl x ((~datum facet) impl ...+)) ≫ [⊢ x ≫ x-] [⊢ (start-facet x impl ...) ≫ impl- (⇒ ν-f (~effs (~and R (~Role (x--) Body ...))))] ---------------------------------------- - [⊢ (define- (x-) impl-) (⇒ ν-f ((FacetImpl x R)))]) + [⊢ (erased (define- (x-) impl-)) (⇒ ν-f ((FacetImpl x R)))]) (define-typed-syntax (start x:id) ≫ [⊢ x ≫ x- (⇒ : ~StartableFacet)] ---------------------------------------- - [⊢ (#%app- x-) (⇒ ν-f ((Start x)))]) - + [⊢ (#%app- x-) (⇒ : ★/t) (⇒ ν-f ((Start x)))]) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Derived Forms