From 57934b389f0ed6c54ad6042bf14ade186256f27e Mon Sep 17 00:00:00 2001 From: Sam Caldwell Date: Wed, 12 Sep 2018 15:06:08 -0400 Subject: [PATCH] fix making defn context with #f #f --- .../examples/roles/two-buyer-protocol.rkt | 6 ++ racket/typed/roles.rkt | 69 +++++++++++++++++-- 2 files changed, 68 insertions(+), 7 deletions(-) diff --git a/racket/typed/examples/roles/two-buyer-protocol.rkt b/racket/typed/examples/roles/two-buyer-protocol.rkt index f7cf11a..9027eea 100644 --- a/racket/typed/examples/roles/two-buyer-protocol.rkt +++ b/racket/typed/examples/roles/two-buyer-protocol.rkt @@ -60,6 +60,12 @@ OrderRequest (Observe OrderInterest))) +(define-type-alias seller-role + (Role (seller) + (Reacts (Know (Observe (QuoteT String ★/t))) + (Role (_) + (Shares (QuoteT String Int)))))) + (dataspace ds-type ;; seller diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt index 9664b19..98dbd05 100644 --- a/racket/typed/roles.rkt +++ b/racket/typed/roles.rkt @@ -21,7 +21,7 @@ tuple select lambda ref observe inbound outbound ;; making types define-type-alias - define-constructor + define-constructor define-constructor* ;; values #%datum ;; patterns @@ -53,6 +53,12 @@ (require rackunit) (require turnstile/rackunit-typechecking)) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Debugging +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-for-syntax DEBUG-BINDINGS? #f) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Type Checking Conventions ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -175,6 +181,14 @@ [(_ e ...) #`(#,transformer e ...)])))) +(define-syntax (define-constructor* stx) + (syntax-parse stx + #:datum-literals (:) + [(_ (Cons:id : TyCons:id slot:id ...) clause ...) + #'(define-constructor (Cons slot ...) + #:type-constructor TyCons + clause ...)])) + (define-syntax (define-constructor stx) (syntax-parse stx [(_ (Cons:id slot:id ...) @@ -691,7 +705,8 @@ (<: r spec)])) (module+ test - (begin-for-syntax + (displayln "skipping commented for-syntax tests because it's slow") + #;(begin-for-syntax ;; TESTS (let () ;; utils @@ -888,6 +903,8 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (define-for-syntax (int-def-ctx-bind-type-rename x x- t ctx) + (when DEBUG-BINDINGS? + (printf "adding to context ~a\n" (syntax-debug-info x))) (syntax-local-bind-syntaxes (list x-) #f ctx) (syntax-local-bind-syntaxes (list x) #`(make-rename-transformer @@ -909,12 +926,17 @@ (add-bindings-to-ctx e def-ctx))] [_ (void)])) +(define-for-syntax (display-ctx-bindings ctx) + (printf "context:\n") + (for ([x (in-list (internal-definition-context-binding-identifiers ctx))]) + (printf ">>~a\n" (syntax-debug-info x)))) + ;; -> (Values e-... (Listof Type) (Listof EndpointEffects) (Listof FacetEffects) (Listof SpawnEffects)) ;; recognizes local binding forms ;; (field/intermediate [x e] ... ;; (define/intermediate x x- τ e) (define-for-syntax (walk/bind e... - [def-ctx (syntax-local-make-definition-context #f #f)] + [def-ctx (syntax-local-make-definition-context)] [unique (gensym 'walk/bind)]) (define-values (rev-e-... rev-τ... ep-effects facet-effects spawn-effects) (let loop ([e... (syntax->list e...)] @@ -927,6 +949,10 @@ ['() (values rev-e-... rev-τ... ep-effects facet-effects spawn-effects)] [(cons e more) + (when (and DEBUG-BINDINGS? + (identifier? e)) + (display-ctx-bindings def-ctx) + (printf "expanding ~a\n" (syntax-debug-info e))) (define e- (local-expand e (list unique) (list #'erased #'begin) def-ctx)) (syntax-parse e- #:literals (begin) @@ -1327,15 +1353,17 @@ [⊢ e ≫ e- ⇐ τ.norm] #:fail-unless (pure? #'e-) "expression must be pure" #:with x- (generate-temporary #'x) + #:with x+ (syntax-local-identifier-as-binding #'x) -------- - [⊢ (define/intermediate #,(syntax-local-identifier-as-binding #'x) x- τ.norm e-) (⇒ : ★/t)]] + [⊢ (define/intermediate x+ x- τ.norm e-) (⇒ : ★/t)]] [(_ x:id e) ≫ ;This won't work with mutually recursive definitions [⊢ e ≫ e- ⇒ τ] #:fail-unless (pure? #'e-) "expression must be pure" #:with x- (generate-temporary #'x) + #:with x+ (syntax-local-identifier-as-binding #'x) -------- - [⊢ (define/intermediate x x- τ e-) (⇒ : ★/t)]] + [⊢ (define/intermediate x+ x- τ e-) (⇒ : ★/t)]] [(_ (f [x (~optional (~datum :)) ty:type] ... (~or (~datum →) (~datum ->)) ty_out:type) e ...+) ≫ @@ -1353,7 +1381,7 @@ [⊢ (define/intermediate f f- fun-ty e-) (⇒ : ★/t)]] [(_ (f [x (~optional (~datum :)) ty] ...) e ...+) ≫ - -------- + ---------------------------- [≻ (define (f [x ty] ... -> ★/t) e ...)]]) ;; copied from ext-stlc @@ -1745,4 +1773,31 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Tests -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; \ No newline at end of file +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; local definitions +#;(module+ test + ;; these cause an error in rackunit-typechecking, don't know why :/ + #;(check-type (let () + (begin + (define id : Int 1234) + id)) + : Int + -> 1234) + #;(check-type (let () + (define (spawn-cell [initial-value : Int]) + (define id 1234) + id) + (typed-app spawn-cell 42)) + : Int + -> 1234) + (check-equal? (let () + (define id : Int 1234) + id) + 1234) + #;(check-equal? (let () + (define (spawn-cell [initial-value : Int]) + (define id 1234) + id) + (typed-app spawn-cell 42)) + 1234)) \ No newline at end of file