syndicate-lang
/
syndicate-2017
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

workaround: combine big and little lambda

This commit is contained in:
Sam Caldwell 2020-07-24 12:10:29 -04:00
parent 48344856c3
commit 074ec24da4
1 changed files with 14 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
racket/typed/core-types.rkt
View File

@ -1084,14 +1084,14 @@
[(X:id Y:id) [(X:id Y:id)
(or (free-identifier=? #'X #'Y) (or (free-identifier=? #'X #'Y)
(let () (let ()
(displayln (identifier-binding #'X)) #;(displayln (identifier-binding #'X))
(displayln (identifier-binding #'Y)) #;(displayln (identifier-binding #'Y))
#f))] #f))]
[((~∀+ (X:id ...) τ1) (~∀+ (Y:id ...) τ2)) [((~∀+ (X:id ...) τ1) (~∀+ (Y:id ...) τ2))
#:when (stx-length=? #'(X ...) #'(Y ...)) #:when (stx-length=? #'(X ...) #'(Y ...))
#:with τ2-X/Y (substs #'(X ...) #'(Y ...) #'τ2) #:with τ2-X/Y (substs #'(X ...) #'(Y ...) #'τ2)
#:do [(displayln "∀ <: ∀") ;; #:do [(displayln "∀ <: ∀")
(displayln #'τ2-X/Y)] ;; (displayln #'τ2-X/Y)]
(<: #'τ1 #'τ2-X/Y)] (<: #'τ1 #'τ2-X/Y)]
[((~Base τ1:id) (~Base τ2:id)) [((~Base τ1:id) (~Base τ2:id))
(free-identifier=? #'τ1 #'τ2)] (free-identifier=? #'τ1 #'τ2)]
@ -1271,6 +1271,7 @@
(Endpoints τ-ep ...) (Endpoints τ-ep ...)
(Roles τ-f ...) (Roles τ-f ...)
(Spawns τ-s ...))))]) (Spawns τ-s ...))))])
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Type Abstraction ;; Type Abstraction
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@ -1511,10 +1512,11 @@
(~Computation (~Value τ-v) _ _ _)))) #'TTTT (~Computation (~Value τ-v) _ _ _)))) #'TTTT
#:do [(displayln 'D)] #:do [(displayln 'D)]
#:with ty_out- (substs #'(X- ...) #'(X ...) #'ty_out) #:with ty_out- (substs #'(X- ...) #'(X ...) #'ty_out)
#:fail-unless (<: (type-eval #'(∀+ (Y ...) τ-v)) #:with actual (type-eval #'(∀+ (Y ...) τ-v))
(type-eval #'(∀+ (X- ...) ty_out-))) #:with expected (type-eval #'(∀+ (X- ...) ty_out-))
#:fail-unless (<: #'actual #'expected)
(format "expected different return type\n got ~a\n expected ~a\n" (format "expected different return type\n got ~a\n expected ~a\n"
#'τ-v #'ty_out) (resugar-type #'actual) (resugar-type #'expected))
#:do [(displayln 'E)] #:do [(displayln 'E)]
#:with f- (add-orig (generate-temporary #'f) #'f) #:with f- (add-orig (generate-temporary #'f) #'f)
------------------------------------------------------- -------------------------------------------------------
@ -1601,12 +1603,12 @@
[⊢ (#%plain-app- e_fn- e_arg- ...) ⇒ τ_out*]] [⊢ (#%plain-app- e_fn- e_arg- ...) ⇒ τ_out*]]
;; All Other Functions ;; All Other Functions
[(_ e_fn e_arg ...) ≫ [(_ e_fn e_arg ...) ≫
[⊢ e_fn ≫ e_fn- (⇒ : (~→+ τ_in ... (~Computation (~Value τ-out)
(~Endpoints τ-ep ...)
(~Roles τ-f ...)
(~Spawns τ-s ...))))]
;; TODO - don't know why this cut is needed for error messages
#:cut #:cut
[⊢ e_fn ≫ e_fn- (⇒ : (~→+ τ_in ... (~Computation (~Value τ-out)
(~Endpoints τ-ep ...)
(~Roles τ-f ...)
(~Spawns τ-s ...))))]
;; TODO - don't know why this cut is needed for error messages
#:fail-unless (pure? #'e_fn-) "expression not allowed to have effects" #:fail-unless (pure? #'e_fn-) "expression not allowed to have effects"
#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...]) #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
(num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...]) (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])