From cff784384a1c884761a764552de70c73f41a544b Mon Sep 17 00:00:00 2001 From: Sam Caldwell Date: Wed, 13 Dec 2017 12:16:10 -0500 Subject: [PATCH] add constructor types --- racket/typed/examples/bank-account.rkt | 31 ++- racket/typed/examples/two-buyer-protocol.rkt | 143 +++++++---- racket/typed/main.rkt | 254 +++++++++++++++---- 3 files changed, 316 insertions(+), 112 deletions(-) diff --git a/racket/typed/examples/bank-account.rkt b/racket/typed/examples/bank-account.rkt index 81a5bfe..a3d4ed1 100644 --- a/racket/typed/examples/bank-account.rkt +++ b/racket/typed/examples/bank-account.rkt @@ -1,33 +1,46 @@ #lang typed/syndicate +(define-constructor (account balance) + #:type-constructor AccountT + #:with Account (AccountT Int) + #:with AccountRequest (AccountT ★)) + +(define-constructor (deposit amount) + #:type-constructor DepositT + #:with Deposit (DepositT Int) + #:with DepositRequest (DepositT ★)) + (define-type-alias ds-type - (U (Tuple String Int) - (Observe (Tuple String ★)) - (Observe (Observe (Tuple String ★))))) + (U Account + (Observe AccountRequest) + (Observe (Observe AccountRequest)) + Deposit + (Observe DepositRequest) + (Observe (Observe DepositRequest)))) (dataspace ds-type (spawn ds-type (facet _ (fields [balance Int 0]) - (assert (tuple "balance" (ref balance))) - (on (asserted (tuple "deposit" (bind amount Int))) + (assert (account (ref balance))) + (on (asserted (deposit (bind amount Int))) (set! balance (+ (ref balance) amount))))) (spawn ds-type (facet _ (fields) - (on (asserted (tuple "balance" (bind amount Int))) + (on (asserted (account (bind amount Int))) (displayln amount)))) (spawn ds-type (facet _ (fields) - (on (asserted (observe (tuple "deposit" discard))) + (on (asserted (observe (deposit discard))) (facet _ (fields) - (assert (tuple "deposit" 100)) - (assert (tuple "deposit" -30))))))) + (assert (deposit 100)) + (assert (deposit -30))))))) #| ;; Hello-worldish "bank account" example. diff --git a/racket/typed/examples/two-buyer-protocol.rkt b/racket/typed/examples/two-buyer-protocol.rkt index f72f692..fcf1568 100644 --- a/racket/typed/examples/two-buyer-protocol.rkt +++ b/racket/typed/examples/two-buyer-protocol.rkt @@ -1,25 +1,58 @@ #lang typed/syndicate +(define-constructor (price v) + #:type-constructor PriceT + #:with Price (PriceT Int)) + +(define-constructor (out-of-stock) + #:type-constructor OutOfStockT + #:with OutOfStock (OutOfStockT)) + +(define-type-alias QuoteAnswer + (U Price OutOfStock)) + +(define-constructor (quote title answer) + #:type-constructor QuoteT + #:with Quote (QuoteT String QuoteAnswer) + #:with QuoteRequest (Observe (QuoteT String ★)) + #:with QuoteInterest (Observe (QuoteT ★ ★))) + +(define-constructor (split-proposal title price contribution accepted) + #:type-constructor SplitProposalT + #:with SplitProposal (SplitProposalT String Int Int Bool) + #:with SplitRequest (Observe (SplitProposalT String Int Int ★)) + #:with SplitInterest (Observe (SplitProposalT ★ ★ ★ ★))) + +(define-constructor (order-id id) + #:type-constructor OrderIdT + #:with OrderId (OrderIdT Int)) + +(define-constructor (delivery-date date) + #:type-constructor DeliveryDateT + #:with DeliveryDate (DeliveryDateT String)) + +(define-type-alias (Maybe t) + (U t Bool)) + +(define-constructor (order title price id delivery-date) + #:type-constructor OrderT + #:with Order (OrderT String Int (Maybe OrderId) (Maybe DeliveryDate)) + #:with OrderRequest (Observe (OrderT String Int ★ ★)) + #:with OrderInterest (Observe (OrderT ★ ★ ★ ★))) + (define-type-alias ds-type (U ;; quotes - (Tuple String String Int) - (Observe (Tuple String String ★)) - (Observe (Observe (Tuple String ★ ★))) - ;; out of stock - (Tuple String String) - (Observe (Tuple String String)) + Quote + QuoteRequest + (Observe QuoteInterest) ;; splits - (Tuple String String Int Int Bool) - (Observe (Tuple String String Int Int ★)) - (Observe (Observe (Tuple String ★ ★ ★ ★))) + SplitProposal + SplitRequest + (Observe SplitInterest) ;; orders - ;; work around generativity by putting it all inside a tuple - (Tuple (Tuple String String Int Int String)) - (Observe (Tuple (Tuple String String Int ★ ★))) - (Observe (Observe (Tuple (Tuple String ★ ★ ★ ★)))) - ;; denied order - (Tuple (Tuple String String Int)) - (Observe (Tuple (Tuple String String Int))))) + Order + OrderRequest + (Observe OrderInterest))) (dataspace ds-type @@ -28,76 +61,80 @@ (facet _ (fields [book (Tuple String Int) (tuple "Catch 22" 22)] [next-order-id Int 10001483]) - (on (asserted (observe (tuple "book-quote" (bind title String) discard))) + (on (asserted (observe (quote (bind title String) discard))) (facet x (fields) - (on (retracted (observe (tuple "book-quote" title discard))) + (on (retracted (observe (quote title discard))) (stop x (begin))) (match title ["Catch 22" - (assert (tuple "book-quote" title 22))] + (assert (quote title (price 22)))] [discard - (assert (tuple "out-of-stock" title))]))) - (on (asserted (observe (tuple (tuple "order" (bind title String) (bind offer Int) discard discard)))) + (assert (quote title (out-of-stock)))]))) + (on (asserted (observe (order (bind title String) (bind offer Int) discard discard))) (facet x (fields) - (on (retracted (observe (tuple (tuple "order" title offer discard discard)))) + (on (retracted (observe (order title offer discard discard))) (stop x (begin))) (let [asking-price 22] (if (and (equal? title "Catch 22") (>= offer asking-price)) - (let [order-id (ref next-order-id)] - (begin (set! next-order-id (+ 1 order-id)) - (assert (tuple (tuple "order" title offer order-id "March 9th"))))) - (assert (tuple (tuple "no-order" title offer))))))))) + (let [id (ref next-order-id)] + (begin (set! next-order-id (+ 1 id)) + (assert (order title offer (order-id id) (delivery-date "March 9th"))))) + (assert (order title offer #f #f)))))))) ;; buyer A (spawn ds-type (facet buyer (fields [title String "Catch 22"] [budget Int 1000]) - (on (asserted (tuple "out-of-stock" (ref title))) - (stop buyer (begin))) - (on (asserted (tuple "book-quote" (ref title) (bind price Int))) - (facet negotiation - (fields [contribution Int (/ price 2)]) - (on (asserted (tuple "split" (ref title) price (ref contribution) (bind accept? Bool))) - (if accept? - (stop buyer (begin)) - (if (> (ref contribution) (- price 5)) - (stop negotiation (displayln "negotiation failed")) - (set! contribution - (+ (ref contribution) (/ (- price (ref contribution)) 2)))))))))) + (on (asserted (quote (ref title) (bind answer QuoteAnswer))) + (match answer + [(out-of-stock) + (stop buyer (begin))] + [(price (bind amount Int)) + (facet negotiation + (fields [contribution Int (/ amount 2)]) + (on (asserted (split-proposal (ref title) amount (ref contribution) (bind accept? Bool))) + (if accept? + (stop buyer (begin)) + (if (> (ref contribution) (- amount 5)) + (stop negotiation (displayln "negotiation failed")) + (set! contribution + (+ (ref contribution) (/ (- amount (ref contribution)) 2)))))))])))) ;; buyer B (spawn ds-type (facet buyer-b (fields [funds Int 5]) - (on (asserted (observe (tuple "split" (bind title String) (bind price Int) (bind their-contribution Int) discard))) + (on (asserted (observe (split-proposal (bind title String) (bind price Int) (bind their-contribution Int) discard))) (let [my-contribution (- price their-contribution)] (cond [(> my-contribution (ref funds)) (facet decline (fields) - (assert (tuple "split" title price their-contribution #f)) - (on (retracted (observe (tuple "split" title price their-contribution discard))) + (assert (split-proposal title price their-contribution #f)) + (on (retracted (observe (split-proposal title price their-contribution discard))) (stop decline (begin))))] [#t (facet accept (fields) - (assert (tuple "split" title price their-contribution #t)) - (on (retracted (observe (tuple "split" title price their-contribution discard))) + (assert (split-proposal title price their-contribution #t)) + (on (retracted (observe (split-proposal title price their-contribution discard))) (stop accept (begin))) (on start (spawn ds-type - (facet order + (facet purchase (fields) - (on (asserted (tuple (tuple "no-order" title price))) - (begin (displayln "Order Rejected") - (stop order (begin)))) - (on (asserted (tuple (tuple "order" title price (bind order-id Int) (bind delivery-date String)))) - ;; complete! - (begin (displayln "Completed Order:") - (displayln order-id) - (displayln delivery-date) - (stop order (begin))))))))]))))) + (on (asserted (order title price (bind order-id? (Maybe OrderId)) (bind delivery-date? (Maybe DeliveryDate)))) + (match (tuple order-id? delivery-date?) + [(tuple (order-id (bind id Int)) (delivery-date (bind date String))) + ;; complete! + (begin (displayln "Completed Order:") + (displayln id) + (displayln date) + (stop purchase (begin)))] + [discard + (begin (displayln "Order Rejected") + (stop purchase (begin)))]))))))]))))) ) \ No newline at end of file diff --git a/racket/typed/main.rkt b/racket/typed/main.rkt index 1c8b88e..bb2a5f1 100644 --- a/racket/typed/main.rkt +++ b/racket/typed/main.rkt @@ -4,7 +4,6 @@ (rename-out [typed-app #%app]) (rename-out [syndicate:begin-for-declarations declare-types]) #%top-interaction - #%top require only-in ;; Types Int Bool String Tuple Bind Discard Case → Behavior FacetName Field ★ @@ -21,8 +20,10 @@ bind discard ;; primitives + - * / and or not > < >= <= = equal? displayln - ;; DEBUG and utilities + ;; making types define-type-alias + define-constructor + ;; DEBUG and utilities print-type (rename-out [printf- printf]) ;; Extensions @@ -58,6 +59,137 @@ (define-type-constructor Outbound #:arity = 1) (define-type-constructor Actor #:arity = 1) +(define-for-syntax (type-eval t) + ((current-type-eval) t)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; User Defined Types, aka Constructors + +;; τ.norm in 1st case causes "not valid type" error when file is compiled +;; (copied from ext-stlc example) +(define-syntax define-type-alias + (syntax-parser + [(_ alias:id τ:any-type) + #'(define-syntax- alias + (make-variable-like-transformer #'τ.norm))] + [(_ (f:id x:id ...) ty) + #'(define-syntax- (f stx) + (syntax-parse stx + [(_ x ...) + #:with τ:any-type #'ty + #'τ.norm]))])) + +(begin-for-syntax + (define-splicing-syntax-class type-constructor-decl + (pattern (~seq #:type-constructor TypeCons:id)) + (pattern (~seq) #:attr TypeCons #f)) + + (struct user-ctor (typed-ctor untyped-ctor) + #:property prop:procedure + (lambda (v stx) + (define transformer (user-ctor-typed-ctor v)) + (syntax-parse stx + [(_ e ...) + #`(#,transformer e ...)])))) + +(define-syntax (define-constructor stx) + (syntax-parse stx + [(_ (Cons:id slot:id ...) + ty-cons:type-constructor-decl + (~seq #:with + Alias AliasBody) ...) + #:with TypeCons (or (attribute ty-cons.TypeCons) (format-id stx "~a/t" (syntax-e #'Cons))) + #:with MakeTypeCons (format-id #'TypeCons "make-~a" #'TypeCons) + #:with GetTypeParams (format-id #'TypeCons "get-~a-type-params" #'TypeCons) + #:with TypeConsExpander (format-id #'TypeCons "~~~a" #'TypeCons) + #:with TypeConsExtraInfo (format-id #'TypeCons "~a-extra-info" #'TypeCons) + #:with (StructName Cons- type-tag) (generate-temporaries #'(Cons Cons Cons)) + (define arity (stx-length #'(slot ...))) + #`(begin- + (struct- StructName (slot ...) #:reflection-name 'Cons #:transparent) + (define-syntax (TypeConsExtraInfo stx) + (syntax-parse stx + [(_ X (... ...)) #'('type-tag 'MakeTypeCons 'GetTypeParams)])) + (define-type-constructor TypeCons + #:arity = #,arity + #:extra-info 'TypeConsExtraInfo) + (define-syntax (MakeTypeCons stx) + (syntax-parse stx + [(_ t (... ...)) + #:fail-unless (= #,arity (stx-length #'(t (... ...)))) "arity mismatch" + #'(TypeCons t (... ...))])) + (define-syntax (GetTypeParams stx) + (syntax-parse stx + [(_ (TypeConsExpander t (... ...))) + #'(t (... ...))])) + (define-syntax Cons + (user-ctor #'Cons- #'StructName)) + (define-typed-syntax (Cons- e (... ...)) ≫ + #:fail-unless (= #,arity (stx-length #'(e (... ...)))) "arity mismatch" + [⊢ e ≫ e- (⇒ : τ)] (... ...) + ---------------------- + [⊢ (#%app- StructName e- (... ...)) (⇒ : (TypeCons τ (... ...))) + (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))]) + (define-type-alias Alias AliasBody) ...)])) + +(begin-for-syntax + (define-syntax ~constructor-extra-info + (pattern-expander + (syntax-parser + [(_ tag mk get) + #'(_ (_ tag) (_ mk) (_ get))]))) + + (define-syntax ~constructor-type + (pattern-expander + (syntax-parser + [(_ tag . rst) + #'(~and it + (~fail #:unless (user-defined-type? #'it)) + (~parse tag (get-type-tag #'it)) + (~Any _ . rst))]))) + + (define-syntax ~constructor-exp + (pattern-expander + (syntax-parser + [(_ cons . rst) + #'(~and (cons . rst) + (~fail #:unless (ctor-id? #'cons)))]))) + + (define (inspect t) + (syntax-parse t + [(~constructor-type tag t ...) + (list (syntax-e #'tag) (stx-map type->str #'(t ...)))])) + + (define (tags-equal? t1 t2) + (equal? (syntax-e t1) (syntax-e t2))) + + (define (user-defined-type? t) + (get-extra-info (type-eval t))) + + (define (get-type-tag t) + (syntax-parse (get-extra-info t) + [(~constructor-extra-info tag _ _) + (syntax-e #'tag)])) + + (define (get-type-args t) + (syntax-parse (get-extra-info t) + [(~constructor-extra-info _ _ get) + (define f (syntax-local-value #'get)) + (syntax->list (f #`(get #,t)))])) + + (define (make-cons-type t args) + (syntax-parse (get-extra-info t) + [(~constructor-extra-info _ mk _) + (define f (syntax-local-value #'mk)) + (type-eval (f #`(mk #,@args)))])) + + (define (ctor-id? stx) + (and (identifier? stx) + (user-ctor? (syntax-local-value stx (const #f))))) + + (define (untyped-ctor stx) + (user-ctor-untyped-ctor (syntax-local-value stx (const #f))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Syntax @@ -121,19 +253,19 @@ is meant to be (~literal -) (~literal displayln)))) - (define-syntax-class endpoint + #;(define-syntax-class endpoint #:datum-literals (on start stop) (pattern (~or (on ed:event-desc s) (assert e:expr)))) - (define-syntax-class event-desc + #;(define-syntax-class event-desc #:datum-literals (start stop asserted retracted) (pattern (~or start stop (asserted p:pat) (retracted p:pat)))) - (define-syntax-class pat + #;(define-syntax-class pat #:datum-literals (tuple _ discard bind) #:attributes (syndicate-pattern match-pattern) (pattern (~or (~and (tuple ps:pat ...) @@ -153,7 +285,35 @@ is meant to be [match-pattern #'(== x)])) (~and e:expr (~bind [syndicate-pattern #'e] - [match-pattern #'(== e)])))))) + [match-pattern #'(== e)]))))) + + (define (compile-pattern pat bind-id-transformer exp-transformer) + (let loop ([pat pat]) + (syntax-parse pat + #:datum-literals (tuple discard bind) + [(tuple p ...) + #`(list 'tuple #,@(stx-map loop #'(p ...)))] + [(k:kons1 p) + #`(#,(kons1->constructor #'k) #,(loop #'p))] + [(bind x:id τ:type) + (bind-id-transformer #'x)] + [discard + #'_] + [(~constructor-exp ctor p ...) + (define/with-syntax uctor (untyped-ctor #'ctor)) + #`(uctor #,@(stx-map loop #'(p ...)))] + [_ + (exp-transformer pat)]))) + + (define (compile-match-pattern pat) + (compile-pattern pat + identity + (lambda (exp) #`(== #,exp)))) + + (define (compile-syndicate-pattern pat) + (compile-pattern pat + (lambda (id) #`($ #,id)) + identity))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Subtyping @@ -189,6 +349,10 @@ is meant to be (<: #'τ1 #'τ2)] [((~Outbound τ1:type) (~Outbound τ2:type)) (<: #'τ1 #'τ2)] + [((~constructor-type t1 τ1:type ...) (~constructor-type t2 τ2:type ...)) + #:when (tags-equal? #'t1 #'t2) + (and (stx-length=? #'(τ1 ...) #'(τ2 ...)) + (stx-andmap <: #'(τ1 ...) #'(τ2 ...)))] [((~Behavior τ-v1 τ-i1 τ-o1 τ-a1) (~Behavior τ-v2 τ-i2 τ-o2 τ-a2)) (and (<: #'τ-v1 #'τ-v2) ;; HMMMMMM. i2 and i1 are types of patterns. TODO @@ -236,6 +400,11 @@ is meant to be ;; I don't think stx-ormap is part of the documented api of turnstile *shrug* #:fail-when (stx-ormap (lambda (t) (<: t (type-eval #'(U)))) #'(τ ...)) #f (type-eval #'(Tuple τ ...))] + [((~constructor-type tag1 τ1:type ...) (~constructor-type tag2 τ2:type ...)) + #:when (tags-equal? #'tag1 #'tag2) + #:with (τ ...) (stx-map ∩ #'(τ1 ...) #'(τ2 ...)) + #:fail-when (stx-ormap (lambda (t) (<: t (type-eval #'(U)))) #'(τ ...)) #f + (make-cons-type t1 #'(τ ...))] ;; these three are just the same :( [((~Observe τ1:type) (~Observe τ2:type)) #:with τ (∩ #'τ1 #'τ2) @@ -267,6 +436,9 @@ is meant to be [((~Tuple τ1:type ...) (~Tuple τ2:type ...)) #:when (overlap? t1 t2) (stx-andmap project-safe? #'(τ1 ...) #'(τ2 ...))] + [((~constructor-type t1 τ1:type ...) (~constructor-type t2 τ2:type ...)) + #:when (tags-equal? #'t1 #'t2) + (stx-andmap project-safe? #'(τ1 ...) #'(τ2 ...))] [((~Observe τ1:type) (~Observe τ2:type)) (project-safe? #'τ1 #'τ2)] [((~Inbound τ1:type) (~Inbound τ2:type)) @@ -290,6 +462,9 @@ is meant to be [((~Tuple τ1:type ...) (~Tuple τ2:type ...)) (and (stx-length=? #'(τ1 ...) #'(τ2 ...)) (stx-andmap overlap? #'(τ1 ...) #'(τ2 ...)))] + [((~constructor-type t1 τ1:type ...) (~constructor-type t2 τ2:type ...)) + (and (tags-equal? #'t1 #'t2) + (stx-andmap overlap? #'(τ1 ...) #'(τ2 ...)))] [((~Observe τ1:type) (~Observe τ2:type)) (overlap? #'τ1 #'τ2)] [((~Inbound τ1:type) (~Inbound τ2:type)) @@ -307,6 +482,8 @@ is meant to be (stx-andmap finite? #'(τ ...))] [(~Tuple τ:type ...) (stx-andmap finite? #'(τ ...))] + [(~constructor-type _ τ:type ...) + (stx-andmap finite? #'(τ ...))] [(~Observe τ:type) (finite? #'τ)] [(~Inbound τ:type) @@ -482,14 +659,15 @@ is meant to be [⊢ s ≫ s- (⇒ :i τi) (⇒ :o τ-o) (⇒ :a τ-a)] ----------------------------------- [⊢ (syndicate:on-stop s-) (⇒ : (U)) (⇒ :i τi) (⇒ :o τ-o) (⇒ :a τ-a)]] - [(on (a/r:asserted-or-retracted p:pat) s) ≫ + [(on (a/r:asserted-or-retracted p) s) ≫ [⊢ p ≫ _ (⇒ : τp)] + #:with p- (compile-syndicate-pattern #'p) #:with ([x:id τ:type] ...) (pat-bindings #'p) [[x ≫ x- : τ] ... ⊢ s ≫ s- (⇒ :i τi) (⇒ :o τ-o) (⇒ :a τ-a)] ;; the type of subscriptions to draw assertions to the pattern #:with pat-sub (replace-bind-and-discard-with-★ #'τp) ----------------------------------- - [⊢ (syndicate:on (a/r.syndicate-kw p.syndicate-pattern) + [⊢ (syndicate:on (a/r.syndicate-kw p-) (let- ([x- x] ...) s-)) (⇒ : (U)) (⇒ :i (U τi τp)) @@ -513,10 +691,12 @@ is meant to be (type-eval #`(Inbound #,(replace-bind-and-discard-with-★ #'τ)))] [(~Outbound τ) (type-eval #`(Outbound #,(replace-bind-and-discard-with-★ #'τ)))] + [(~constructor-type _ τ ...) + (make-cons-type t (stx-map replace-bind-and-discard-with-★ #'(τ ...)))] [_ t])) (define-typed-syntax (assert e:expr) ≫ - [⊢ e ≫ e- (⇒ : τ)] + [⊢ e ≫ e- (⇒ : τ:type)] #:with τ-in (strip-? #'τ.norm) ------------------------------------- [⊢ (syndicate:assert e-) (⇒ : (U)) (⇒ :i τ-in) (⇒ :o τ) (⇒ :a (U))]) @@ -534,16 +714,17 @@ is meant to be ------------------------ [⊢ (x-) (⇒ : τ) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))]) -(define-typed-syntax (λ [p:pat s] ...) ≫ +(define-typed-syntax (λ [p s] ...) ≫ #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...)) - [[x ≫ x- : τ] ... ⊢ s ≫ s- (⇒ : τv) (⇒ :i τ1) (⇒ :o τ2) (⇒ :a τ3)] ... + [[x ≫ x- : τ :i (U) :o (U) :a (U)] ... ⊢ s ≫ s- (⇒ : τv) (⇒ :i τ1) (⇒ :o τ2) (⇒ :a τ3)] ... ;; 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 ≫ _ ⇒ τ-p] ... + #:with (p- ...) (stx-map compile-match-pattern #'(p ...)) #:with (τ-in ...) (stx-map lower-pattern-type #'(τ-p ...)) -------------------------------------------------------------- ;; TODO: add a catch-all error clause - [⊢ (match-lambda- [p.match-pattern (let- ([x- x] ...) s-)] ...) + [⊢ (match-lambda- [p- (let- ([x- x] ...) s-)] ...) (⇒ : (→ (U τ-p ...) (Behavior (U τv ...) (U τ1 ...) (U τ2 ...) (U τ3 ...)))) (⇒ :i (U)) (⇒ :o (U)) @@ -567,6 +748,8 @@ is meant to be (type-eval #`(Inbound #,(lower-pattern-type #'τ)))] [(~Outbound τ) (type-eval #`(Outbound #,(lower-pattern-type #'τ)))] + [(~constructor-type _ τ ...) + (make-cons-type t (stx-map lower-pattern-type #'(τ ...)))] [_ t])) (define-typed-syntax (typed-app e_fn e_arg ...) ≫ @@ -619,12 +802,15 @@ is meant to be #:datum-literals (bind tuple) [(bind x:id τ:type) #'([x τ])] - [(tuple p:pat ...) + [(tuple p ...) #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...)) #'([x τ] ... ...)] - [(k:kons1 p:pat) + [(k:kons1 p) (pat-bindings #'p)] - [_:pat + [(~constructor-exp cons p ...) + #:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...)) + #'([x τ] ... ...)] + [_ #'()])) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -693,8 +879,7 @@ is meant to be [(_ expr0 expr ...) (syntax/loc stx (begin- expr0 expr ...))])) -(define-for-syntax (type-eval t) - ((current-type-eval) t)) + (define-typed-syntax (print-type e) ≫ [⊢ e ≫ e- ⇒ τ] @@ -702,20 +887,6 @@ is meant to be ---------------------------------- [⊢ e- ⇒ τ]) -;; τ.norm in 1st case causes "not valid type" error when file is compiled -;; (copied from ext-stlc example) -(define-syntax define-type-alias - (syntax-parser - [(_ alias:id τ:any-type) - #'(define-syntax- alias - (make-variable-like-transformer #'τ.norm))] - [(_ (f:id x:id ...) ty) - #'(define-syntax- (f stx) - (syntax-parse stx - [(_ x ...) - #:with τ:any-type #'ty - #'τ.norm]))])) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Extensions @@ -768,21 +939,4 @@ is meant to be (syntax-parse e [(~var _ class) #'#t] [_ #'#f])) - (test-result))])) - -#;(begin-for-syntax - (displayln (syntax-parse ((current-type-eval) #'(U String)) - [(~U τ ...) - #'(τ ...)] - [_ 'boo]))) - -#;(define-typed-syntax (λ2 ([x:id τ:type] ...) e:expr ...+) ≫ - [[x ≫ x- : τ] ... ⊢ (e ≫ e- ⇒ τ-e) ...] - ;;#:do ((printf "~v\n" #'((x- ...) ...))) - ------------------------------ - [⊢ (lambda- (x- ...) e- ...) - ⇒ (→ τ ... #,(last (stx->list #'(τ-e ...))))]) - -#;(define-syntax (#%top stx) - (printf "my #%top\n") - #'f) \ No newline at end of file + (test-result))])) \ No newline at end of file