Compare commits
10 Commits
Author | SHA1 | Date |
---|---|---|
Michael Ballantyne | 7cdf676ac8 | |
Sam Caldwell | e63da2679b | |
Sam Caldwell | d53b5041f3 | |
Michael Ballantyne | 512783ec0f | |
Sam Caldwell | 8a74f7ffee | |
Sam Caldwell | 721fb1c30f | |
Sam Caldwell | 4e97151cc5 | |
Sam Caldwell | 0a8e400f63 | |
Sam Caldwell | 8d6a037841 | |
Sam Caldwell | 23616488ce |
|
@ -1,16 +1,31 @@
|
||||||
#lang turnstile
|
#lang turnstile
|
||||||
|
|
||||||
(provide (all-defined-out)
|
(provide (except-out (all-defined-out) → ∀ Role)
|
||||||
(for-syntax (all-defined-out))
|
(rename-out [→+ →]
|
||||||
|
[∀+ ∀]
|
||||||
|
[Role+Body Role])
|
||||||
|
(for-syntax (except-out (all-defined-out) ~→ ~∀ ~Role)
|
||||||
|
(rename-out [~→+ ~→]
|
||||||
|
[~∀+ ~∀]
|
||||||
|
[~Role+Body ~Role]))
|
||||||
(for-meta 2 (all-defined-out)))
|
(for-meta 2 (all-defined-out)))
|
||||||
(require (only-in turnstile
|
(require (only-in turnstile
|
||||||
[define-type-constructor define-type-constructor-]))
|
[define-type-constructor define-type-constructor-]
|
||||||
|
[type? type?-]
|
||||||
|
[get-arg-variances get-arg-variances-]))
|
||||||
|
|
||||||
|
(require turnstile/typedefs)
|
||||||
|
(begin-for-syntax
|
||||||
|
;; turnstile/typedefs sets it to #t, which breaks things
|
||||||
|
(current-use-stop-list? #f))
|
||||||
|
|
||||||
(require (prefix-in syndicate: syndicate/actor-lang))
|
(require (prefix-in syndicate: syndicate/actor-lang))
|
||||||
|
|
||||||
(require (for-meta 2 macrotypes/stx-utils racket/list syntax/stx syntax/parse racket/base))
|
(require (for-meta 2 macrotypes/stx-utils racket/list syntax/stx syntax/parse racket/base))
|
||||||
(require (for-syntax turnstile/examples/util/filter-maximal))
|
(require (for-syntax turnstile/examples/util/filter-maximal))
|
||||||
(require (for-syntax macrotypes/type-constraints macrotypes/variance-constraints))
|
(require (for-syntax (prefix-in ttc: turnstile/type-constraints)
|
||||||
|
(prefix-in mtc: macrotypes/type-constraints)
|
||||||
|
(prefix-in mvc: macrotypes/variance-constraints)))
|
||||||
#;(require (only-in (for-syntax macrotypes/typecheck-core) get-orig))
|
#;(require (only-in (for-syntax macrotypes/typecheck-core) get-orig))
|
||||||
(require (for-syntax racket/struct-info
|
(require (for-syntax racket/struct-info
|
||||||
syntax/id-table))
|
syntax/id-table))
|
||||||
|
@ -20,6 +35,7 @@
|
||||||
(require (postfix-in - racket/set))
|
(require (postfix-in - racket/set))
|
||||||
(require (postfix-in - racket/match))
|
(require (postfix-in - racket/match))
|
||||||
(require (postfix-in - (only-in racket/format ~a)))
|
(require (postfix-in - (only-in racket/format ~a)))
|
||||||
|
(require (for-syntax "syntax-serializer.rkt"))
|
||||||
|
|
||||||
|
|
||||||
(module+ test
|
(module+ test
|
||||||
|
@ -65,7 +81,10 @@
|
||||||
(define (un- id)
|
(define (un- id)
|
||||||
(define match?
|
(define match?
|
||||||
(regexp-match #px"^(\\S*)-\\S*$" (symbol->string (syntax-e id))))
|
(regexp-match #px"^(\\S*)-\\S*$" (symbol->string (syntax-e id))))
|
||||||
(string->symbol (second match?)))
|
(if match?
|
||||||
|
(string->symbol (second match?))
|
||||||
|
(begin (printf "no match! ~a\n" id)
|
||||||
|
match?)))
|
||||||
|
|
||||||
;; Identifier -> (U #f type-metadata)
|
;; Identifier -> (U #f type-metadata)
|
||||||
(define (get-type-info ty-cons)
|
(define (get-type-info ty-cons)
|
||||||
|
@ -141,7 +160,7 @@
|
||||||
#:with mk- (format-id #'Name- "mk-~a-" (syntax-e #'Name-))
|
#:with mk- (format-id #'Name- "mk-~a-" (syntax-e #'Name-))
|
||||||
(quasisyntax/loc stx
|
(quasisyntax/loc stx
|
||||||
(begin-
|
(begin-
|
||||||
(define-type-constructor- Name-
|
(define-type-constructor Name-
|
||||||
#:arity op arity
|
#:arity op arity
|
||||||
#:arg-variances variances
|
#:arg-variances variances
|
||||||
#,@(if (attribute extra-info)
|
#,@(if (attribute extra-info)
|
||||||
|
@ -149,16 +168,16 @@
|
||||||
#'()))
|
#'()))
|
||||||
(define-syntax (Name stx)
|
(define-syntax (Name stx)
|
||||||
(syntax-parse stx
|
(syntax-parse stx
|
||||||
[(_ t (... ...))
|
[(_ . ts)
|
||||||
(syntax/loc stx
|
(syntax/loc stx
|
||||||
(Name- t (... ...)))]))
|
(Name- . ts))]))
|
||||||
(begin-for-syntax
|
(begin-for-syntax
|
||||||
(set-type-info! 'Name '#,(attribute desc.val) mk-)
|
(set-type-info! 'Name '#,(attribute desc.val) mk-)
|
||||||
(define-syntax NamePat
|
(define-syntax NamePat
|
||||||
(pattern-expander
|
(pattern-expander
|
||||||
(syntax-parser
|
(syntax-parser
|
||||||
[(_ p (... ...))
|
[(_ . p)
|
||||||
#'(NamePat- p (... ...))]))))
|
#'(NamePat- . p)]))))
|
||||||
(define-for-syntax mk mk-)))]))
|
(define-for-syntax mk mk-)))]))
|
||||||
|
|
||||||
(begin-for-syntax
|
(begin-for-syntax
|
||||||
|
@ -185,7 +204,7 @@
|
||||||
#'(#:extra-info extra-info)
|
#'(#:extra-info extra-info)
|
||||||
#'())))]))
|
#'())))]))
|
||||||
|
|
||||||
;; Define a type constructor that acts like a container:
|
;; Define a type constructor that acts like a product:
|
||||||
;; - covariant
|
;; - covariant
|
||||||
;; - does not have an empty element (i.e. intersection may be empty)
|
;; - does not have an empty element (i.e. intersection may be empty)
|
||||||
(define-syntax (define-product-type stx)
|
(define-syntax (define-product-type stx)
|
||||||
|
@ -201,7 +220,108 @@
|
||||||
#'(#:extra-info extra-info)
|
#'(#:extra-info extra-info)
|
||||||
#'())))]))
|
#'())))]))
|
||||||
|
|
||||||
(define-binding-type Role #:arity >= 0 #:bvs = 1)
|
(define-type Type : Type)
|
||||||
|
|
||||||
|
(begin-for-syntax
|
||||||
|
|
||||||
|
(define (Type? stx)
|
||||||
|
(syntax-parse stx
|
||||||
|
[~Type #t]
|
||||||
|
[_ #f]))
|
||||||
|
|
||||||
|
(define (new-type? t)
|
||||||
|
(or (type?- t)
|
||||||
|
(Type? (detach t ':))))
|
||||||
|
#;(require racket/trace)
|
||||||
|
#;(trace new-type?)
|
||||||
|
|
||||||
|
(current-type? new-type?))
|
||||||
|
|
||||||
|
(begin-for-syntax
|
||||||
|
(define-generic-type-method get-arg-variances-data #:default #f)
|
||||||
|
(define-generic-type-method get-extra-info-data #:default #f)
|
||||||
|
|
||||||
|
(define (retrieve/apply meth ty)
|
||||||
|
(define fn (meth ty))
|
||||||
|
(and fn
|
||||||
|
(syntax-parse ty
|
||||||
|
[(~Any/new τcons τ ...)
|
||||||
|
(fn #'(τcons τ ...))])))
|
||||||
|
|
||||||
|
(define (get-arg-variances/new ty)
|
||||||
|
(retrieve/apply get-arg-variances-data ty))
|
||||||
|
|
||||||
|
(define (get-extra-info/new ty)
|
||||||
|
(retrieve/apply get-extra-info-data ty))
|
||||||
|
|
||||||
|
(define (get-arg-variances ty)
|
||||||
|
(or (get-arg-variances/new ty)
|
||||||
|
(get-arg-variances- ty)))
|
||||||
|
|
||||||
|
|
||||||
|
;; ID Nat -> (Listof ID)
|
||||||
|
(define (make-arity-domain op arity)
|
||||||
|
(define prefix (make-list arity #'Type))
|
||||||
|
(syntax-parse op #:datum-literals (>= > =)
|
||||||
|
[=
|
||||||
|
prefix]
|
||||||
|
[>
|
||||||
|
(append prefix (list #'Type #'Type #'*))]
|
||||||
|
[>=
|
||||||
|
(append prefix (list #'Type #'*))]))
|
||||||
|
|
||||||
|
;; PatternExpander (Syntax-Listof ID) ID -> Pattern
|
||||||
|
(define (make-type-recognizer pat dom ty)
|
||||||
|
(define pats (for/list ([t (in-syntax dom)])
|
||||||
|
(if (free-identifier=? t #'Type)
|
||||||
|
#'_
|
||||||
|
#'(... ...))))
|
||||||
|
#`(syntax-parse ty
|
||||||
|
[(#,pat #,@pats) #t]
|
||||||
|
[_ #f])))
|
||||||
|
|
||||||
|
(define-syntax (define-type-constructor stx)
|
||||||
|
(syntax-parse stx
|
||||||
|
[(_ Name:id #:arity op arity:nat
|
||||||
|
(~optional (~seq #:arg-variances variances))
|
||||||
|
(~optional (~seq #:extra-info extra-info)))
|
||||||
|
#:with mk- (mk-mk (mk-- #'Name))
|
||||||
|
#:with Name? (mk-? #'Name)
|
||||||
|
#:with Name-exp (mk-~ #'Name)
|
||||||
|
#:with dom (make-arity-domain #'op (syntax-e #'arity))
|
||||||
|
#:do [
|
||||||
|
(define arg-var-meth #'(~? (get-arg-variances-data variances)
|
||||||
|
()))
|
||||||
|
(define extra-info-meth #'(~? (get-extra-info-data extra-info)
|
||||||
|
()))
|
||||||
|
(define implements? (if (or (attribute variances) (attribute extra-info))
|
||||||
|
#'(#:implements)
|
||||||
|
#'()))]
|
||||||
|
#`(begin-
|
||||||
|
(define-type Name : #,@#'dom -> Type
|
||||||
|
#,@implements?
|
||||||
|
#,@arg-var-meth
|
||||||
|
#,@extra-info-meth)
|
||||||
|
(define-for-syntax (mk- args)
|
||||||
|
((current-type-eval) #`(Name #,@args)))
|
||||||
|
(define-for-syntax (Name? ty)
|
||||||
|
#,(make-type-recognizer #'Name-exp #'dom #'ty)))]))
|
||||||
|
|
||||||
|
(define-simple-macro (define-base-type Name:id)
|
||||||
|
(define-type Name : Type))
|
||||||
|
|
||||||
|
(define-simple-macro (define-base-types Name:id ...)
|
||||||
|
(begin- (define-base-type Name) ...))
|
||||||
|
|
||||||
|
(define-base-types Discard ★/t)
|
||||||
|
|
||||||
|
(define-type FacetName : FacetName)
|
||||||
|
|
||||||
|
#;(define-type-constructor? Shares #:arity = 1)
|
||||||
|
|
||||||
|
#;(define-binding-type Role #:arity >= 0 #:bvs = 1)
|
||||||
|
(define-type Role #:with-binders [X : FacetName] : Type -> Type)
|
||||||
|
(define-type RoleBody : Type * -> Type)
|
||||||
(define-type-constructor Shares #:arity = 1)
|
(define-type-constructor Shares #:arity = 1)
|
||||||
(define-type-constructor Sends #:arity = 1)
|
(define-type-constructor Sends #:arity = 1)
|
||||||
(define-type-constructor Realizes #:arity = 1)
|
(define-type-constructor Realizes #:arity = 1)
|
||||||
|
@ -211,7 +331,8 @@
|
||||||
(define-type-constructor Know #:arity = 1)
|
(define-type-constructor Know #:arity = 1)
|
||||||
(define-type-constructor Forget #:arity = 1)
|
(define-type-constructor Forget #:arity = 1)
|
||||||
(define-product-type Realize #:arity = 1)
|
(define-product-type Realize #:arity = 1)
|
||||||
(define-type-constructor Stop #:arity >= 1)
|
#;(define-type-constructor Stop #:arity >= 1)
|
||||||
|
(define-type Stop : FacetName Type * -> Type)
|
||||||
(define-type-constructor Field #:arity = 1)
|
(define-type-constructor Field #:arity = 1)
|
||||||
(define-type-constructor Bind #:arity = 1)
|
(define-type-constructor Bind #:arity = 1)
|
||||||
;; keep track of branches for facet effects
|
;; keep track of branches for facet effects
|
||||||
|
@ -232,9 +353,63 @@
|
||||||
(define-container-type Patch #:arity = 2)
|
(define-container-type Patch #:arity = 2)
|
||||||
|
|
||||||
;; functions and type abstractions
|
;; functions and type abstractions
|
||||||
(define-binding-type ∀)
|
#;(define-binding-type ∀)
|
||||||
|
(define-type ∀ #:with-binders [X : Type] : Type -> Type)
|
||||||
(define-type-constructor → #:arity > 0)
|
(define-type-constructor → #:arity > 0)
|
||||||
|
|
||||||
|
(define-simple-macro (→+ in ... out)
|
||||||
|
(→ out in ...))
|
||||||
|
|
||||||
|
(begin-for-syntax
|
||||||
|
;; because rest types are *trailing*, define a convenience pattern expander for var-arity domain of →
|
||||||
|
(define-syntax ~→+
|
||||||
|
(pattern-expander
|
||||||
|
(syntax-parser
|
||||||
|
[(_ I ... O)
|
||||||
|
#'(~→ O I ...)]))))
|
||||||
|
|
||||||
|
(define-syntax-parser ∀+
|
||||||
|
[(_ () ty) #'ty]
|
||||||
|
[(_ (X:id Y ...) ty)
|
||||||
|
#'(∀ (X : Type) (∀+ (Y ...) ty))])
|
||||||
|
|
||||||
|
(begin-for-syntax
|
||||||
|
|
||||||
|
(define (flatten-∀ ty)
|
||||||
|
(define-values (body vars)
|
||||||
|
(let loop ([ty ty]
|
||||||
|
[vars/rev '()])
|
||||||
|
(syntax-parse ty
|
||||||
|
[(~∀ (X : _) τ)
|
||||||
|
(loop #'τ (cons #'X vars/rev))]
|
||||||
|
[τ
|
||||||
|
(values #'τ (reverse vars/rev))])))
|
||||||
|
#`(#,vars #,body))
|
||||||
|
|
||||||
|
(define-syntax ~∀+
|
||||||
|
(pattern-expander
|
||||||
|
(syntax-parser
|
||||||
|
[(_ vars-pat ty-pat)
|
||||||
|
#'(~and (~∀ (_ : _) _)
|
||||||
|
TY
|
||||||
|
(~parse (vars-pat ty-pat) (flatten-∀ #'TY)))]))))
|
||||||
|
|
||||||
|
(define-simple-macro (Role+Body (x:id) ty ...)
|
||||||
|
(Role (x : FacetName)
|
||||||
|
(RoleBody ty ...)))
|
||||||
|
|
||||||
|
(begin-for-syntax
|
||||||
|
(define-syntax ~Role+Body
|
||||||
|
(pattern-expander
|
||||||
|
(syntax-parser
|
||||||
|
[(_ var-pat . ty-pat)
|
||||||
|
(syntax/loc this-syntax
|
||||||
|
(~and (~Role (internal-name : _)
|
||||||
|
(~RoleBody . tys))
|
||||||
|
(~parse var-pat #'(internal-name))
|
||||||
|
(~parse ty-pat #'tys)))]))))
|
||||||
|
|
||||||
|
|
||||||
;; for describing the RHS
|
;; for describing the RHS
|
||||||
;; a value and a description of the effects
|
;; a value and a description of the effects
|
||||||
(define-type-constructor Computation #:arity = 4)
|
(define-type-constructor Computation #:arity = 4)
|
||||||
|
@ -244,7 +419,6 @@
|
||||||
(define-type-constructor Spawns #:arity >= 0)
|
(define-type-constructor Spawns #:arity >= 0)
|
||||||
|
|
||||||
|
|
||||||
(define-base-types Discard ★/t FacetName)
|
|
||||||
|
|
||||||
(define-for-syntax (type-eval t)
|
(define-for-syntax (type-eval t)
|
||||||
((current-type-eval) t))
|
((current-type-eval) t))
|
||||||
|
@ -257,15 +431,18 @@
|
||||||
;; (copied from ext-stlc example)
|
;; (copied from ext-stlc example)
|
||||||
(define-syntax define-type-alias
|
(define-syntax define-type-alias
|
||||||
(syntax-parser
|
(syntax-parser
|
||||||
[(_ alias:id τ)
|
[(_ alias:id τ:type)
|
||||||
|
;; #:with kind (detach #'τ.norm ':)
|
||||||
|
#:with serialized-τ (serialize-syntax #'τ.norm)
|
||||||
#'(define-syntax- alias
|
#'(define-syntax- alias
|
||||||
(make-variable-like-transformer #'τ))]
|
(make-variable-like-transformer (deserialize-syntax #'serialized-τ)))]
|
||||||
[(_ (f:id x:id ...) ty)
|
[(_ (f:id x:id ...) ty)
|
||||||
#'(define-syntax- (f stx)
|
#'(define-syntax- (f stx)
|
||||||
(syntax-parse stx
|
(syntax-parse stx
|
||||||
[(_ x ...)
|
[(_ x ...)
|
||||||
#:with τ:any-type #'ty
|
#'ty
|
||||||
#'τ.norm]))]))
|
;; #:with τ:any-type #'ty
|
||||||
|
#;#'τ.norm]))]))
|
||||||
|
|
||||||
(define-type-alias ⊥ (U*))
|
(define-type-alias ⊥ (U*))
|
||||||
(define-type-alias Unit (Tuple))
|
(define-type-alias Unit (Tuple))
|
||||||
|
@ -296,10 +473,10 @@
|
||||||
(syntax/loc stx (U* . tys-)))]))
|
(syntax/loc stx (U* . tys-)))]))
|
||||||
|
|
||||||
(define-simple-macro (→fn ty-in ... ty-out)
|
(define-simple-macro (→fn ty-in ... ty-out)
|
||||||
(→ ty-in ... (Computation (Value ty-out)
|
(→+ ty-in ... (Computation (Value ty-out)
|
||||||
(Endpoints)
|
(Endpoints)
|
||||||
(Roles)
|
(Roles)
|
||||||
(Spawns))))
|
(Spawns))))
|
||||||
|
|
||||||
(begin-for-syntax
|
(begin-for-syntax
|
||||||
(define-syntax ~Base
|
(define-syntax ~Base
|
||||||
|
@ -313,10 +490,10 @@
|
||||||
(pattern-expander
|
(pattern-expander
|
||||||
(syntax-parser
|
(syntax-parser
|
||||||
[(_ ty-in:id ... ty-out)
|
[(_ ty-in:id ... ty-out)
|
||||||
#'(~→ ty-in ... (~Computation (~Value ty-out)
|
#'(~→+ ty-in ... (~Computation (~Value ty-out)
|
||||||
(~Endpoints)
|
(~Endpoints)
|
||||||
(~Roles)
|
(~Roles)
|
||||||
(~Spawns)))])))
|
(~Spawns)))])))
|
||||||
|
|
||||||
;; matching possibly polymorphic types
|
;; matching possibly polymorphic types
|
||||||
(define-syntax ~?∀
|
(define-syntax ~?∀
|
||||||
|
@ -324,8 +501,8 @@
|
||||||
(lambda (stx)
|
(lambda (stx)
|
||||||
(syntax-case stx ()
|
(syntax-case stx ()
|
||||||
[(?∀ vars-pat body-pat)
|
[(?∀ vars-pat body-pat)
|
||||||
#'(~or (~∀ vars-pat body-pat)
|
#'(~or (~∀+ vars-pat body-pat)
|
||||||
(~and (~not (~∀ _ _))
|
(~and (~not (~∀+ _ _))
|
||||||
(~parse vars-pat #'())
|
(~parse vars-pat #'())
|
||||||
body-pat))])))))
|
body-pat))])))))
|
||||||
|
|
||||||
|
@ -342,12 +519,12 @@
|
||||||
#:with spawns (if (attribute s) #'(s ...) #'())
|
#:with spawns (if (attribute s) #'(s ...) #'())
|
||||||
#:with roles (if (attribute r) #'(r ...) #'())
|
#:with roles (if (attribute r) #'(r ...) #'())
|
||||||
#:with endpoints (if (attribute e) #'(e ...) #'())
|
#:with endpoints (if (attribute e) #'(e ...) #'())
|
||||||
#:with body #`(→ ty-in ... (Computation (Value ty-out)
|
#:with body #`(→+ ty-in ... (Computation (Value ty-out)
|
||||||
(Endpoints #,@#'endpoints)
|
(Endpoints #,@#'endpoints)
|
||||||
(Roles #,@#'roles)
|
(Roles #,@#'roles)
|
||||||
(Spawns #,@#'spawns)))
|
(Spawns #,@#'spawns)))
|
||||||
(if (attribute X)
|
(if (attribute X)
|
||||||
#'(∀ (X ...) body)
|
#'(∀+ (X ...) body)
|
||||||
#'body)])
|
#'body)])
|
||||||
|
|
||||||
(begin-for-syntax
|
(begin-for-syntax
|
||||||
|
@ -365,12 +542,12 @@
|
||||||
#:with spawns (if (attribute s) #'(s) #'())
|
#:with spawns (if (attribute s) #'(s) #'())
|
||||||
#:with roles (if (attribute r) #'(r) #'())
|
#:with roles (if (attribute r) #'(r) #'())
|
||||||
#:with endpoints (if (attribute e) #'(e) #'())
|
#:with endpoints (if (attribute e) #'(e) #'())
|
||||||
#:with body #`(~→ ty-in ... (~Computation (~Value ty-out)
|
#:with body #`(~→+ ty-in ... (~Computation (~Value ty-out)
|
||||||
(~Endpoints #,@#'endpoints)
|
(~Endpoints #,@#'endpoints)
|
||||||
(~Roles #,@#'roles)
|
(~Roles #,@#'roles)
|
||||||
(~Spawns #,@#'spawns)))
|
(~Spawns #,@#'spawns)))
|
||||||
(if (attribute X)
|
(if (attribute X)
|
||||||
#'(~∀ (X ...) body)
|
#'(~∀+ (X ...) body)
|
||||||
#'body)]))))
|
#'body)]))))
|
||||||
|
|
||||||
;; for looking at the "effects"
|
;; for looking at the "effects"
|
||||||
|
@ -430,20 +607,21 @@
|
||||||
(define arity (stx-length #'(slot ...)))
|
(define arity (stx-length #'(slot ...)))
|
||||||
#`(begin-
|
#`(begin-
|
||||||
(struct- StructName (slot ...) #:reflection-name 'Cons #:transparent)
|
(struct- StructName (slot ...) #:reflection-name 'Cons #:transparent)
|
||||||
(define-syntax (TypeConsExtraInfo stx)
|
(define-for-syntax (TypeConsExtraInfo stx)
|
||||||
(syntax-parse stx
|
(list #'type-tag #'MakeTypeCons #'GetTypeParams)
|
||||||
|
#;(syntax-parse stx
|
||||||
[(_ X (... ...)) #'(#%app- 'type-tag 'MakeTypeCons 'GetTypeParams)]))
|
[(_ X (... ...)) #'(#%app- 'type-tag 'MakeTypeCons 'GetTypeParams)]))
|
||||||
(define-product-type TypeCons
|
(define-product-type TypeCons
|
||||||
#:arity = #,arity
|
#:arity = #,arity
|
||||||
#:extra-info 'TypeConsExtraInfo)
|
#:extra-info TypeConsExtraInfo)
|
||||||
(define-syntax (MakeTypeCons stx)
|
(define-syntax (MakeTypeCons stx)
|
||||||
(syntax-parse stx
|
(syntax-parse stx
|
||||||
[(_ t (... ...))
|
[(_ . ts)
|
||||||
#:fail-unless (= #,arity (stx-length #'(t (... ...)))) "arity mismatch"
|
#:fail-unless (= #,arity (stx-length #'ts)) "arity mismatch"
|
||||||
#'(TypeCons t (... ...))]))
|
#'(TypeCons . ts)]))
|
||||||
(define-syntax (GetTypeParams stx)
|
(define-syntax (GetTypeParams stx)
|
||||||
(syntax-parse stx
|
(syntax-parse stx
|
||||||
[(_ (TypeConsExpander t (... ...)))
|
[(_ (~Any/new (~literal TypeCons) t (... ...)))
|
||||||
#'(t (... ...))]))
|
#'(t (... ...))]))
|
||||||
(define-syntax Cons
|
(define-syntax Cons
|
||||||
(user-ctor #'Cons- #'StructName 'type-tag))
|
(user-ctor #'Cons- #'StructName 'type-tag))
|
||||||
|
@ -486,14 +664,15 @@
|
||||||
(unless (equal? #t sup)
|
(unless (equal? #t sup)
|
||||||
(raise-syntax-error #f "structs with super-type not supported" #'#,stx #'ucons))
|
(raise-syntax-error #f "structs with super-type not supported" #'#,stx #'ucons))
|
||||||
(define arity (length accs)))
|
(define arity (length accs)))
|
||||||
(define-syntax (TypeConsExtraInfo stx)
|
(define-for-syntax (TypeConsExtraInfo stx)
|
||||||
(syntax-parse stx
|
(list #'type-tag #'MakeTypeCons #'GetTypeParams)
|
||||||
|
#;(syntax-parse stx
|
||||||
[(_ X (... ...)) #'(#%app- 'type-tag 'MakeTypeCons 'GetTypeParams)]))
|
[(_ X (... ...)) #'(#%app- 'type-tag 'MakeTypeCons 'GetTypeParams)]))
|
||||||
(define-product-type TypeCons
|
(define-product-type TypeCons
|
||||||
;; issue: arity needs to parse as an exact-nonnegative-integer
|
;; issue: arity needs to parse as an exact-nonnegative-integer
|
||||||
;; fix: check arity in MakeTypeCons
|
;; fix: check arity in MakeTypeCons
|
||||||
#:arity >= 0
|
#:arity >= 0
|
||||||
#:extra-info 'TypeConsExtraInfo)
|
#:extra-info TypeConsExtraInfo)
|
||||||
(define-syntax (MakeTypeCons stx)
|
(define-syntax (MakeTypeCons stx)
|
||||||
(syntax-parse stx
|
(syntax-parse stx
|
||||||
[(_ t (... ...))
|
[(_ t (... ...))
|
||||||
|
@ -501,7 +680,7 @@
|
||||||
#'(TypeCons t (... ...))]))
|
#'(TypeCons t (... ...))]))
|
||||||
(define-syntax (GetTypeParams stx)
|
(define-syntax (GetTypeParams stx)
|
||||||
(syntax-parse stx
|
(syntax-parse stx
|
||||||
[(_ (TypeConsExpander t (... ...)))
|
[(_ (~Any/new (~literal TypeCons) t (... ...)))
|
||||||
#'(t (... ...))]))
|
#'(t (... ...))]))
|
||||||
(define-typed-syntax (Cons- e (... ...)) ≫
|
(define-typed-syntax (Cons- e (... ...)) ≫
|
||||||
#:fail-unless (= arity (stx-length #'(e (... ...)))) "arity mismatch"
|
#:fail-unless (= arity (stx-length #'(e (... ...)))) "arity mismatch"
|
||||||
|
@ -526,7 +705,7 @@
|
||||||
#'(~and it
|
#'(~and it
|
||||||
(~fail #:unless (user-defined-type? #'it))
|
(~fail #:unless (user-defined-type? #'it))
|
||||||
(~parse tag (get-type-tag #'it))
|
(~parse tag (get-type-tag #'it))
|
||||||
(~Any _ . rst))])))
|
(~Any/new _ . rst))])))
|
||||||
|
|
||||||
(define-syntax ~constructor-exp
|
(define-syntax ~constructor-exp
|
||||||
(pattern-expander
|
(pattern-expander
|
||||||
|
@ -544,21 +723,31 @@
|
||||||
(equal? (syntax-e t1) (syntax-e t2)))
|
(equal? (syntax-e t1) (syntax-e t2)))
|
||||||
|
|
||||||
(define (user-defined-type? t)
|
(define (user-defined-type? t)
|
||||||
(get-extra-info (type-eval t)))
|
(get-extra-info/new (type-eval t)))
|
||||||
|
|
||||||
(define (get-type-tag t)
|
(define (get-type-tag t)
|
||||||
(syntax-parse (get-extra-info t)
|
(match (get-extra-info/new t)
|
||||||
|
[(list tag _ _) tag])
|
||||||
|
#;(syntax-parse (get-extra-info t)
|
||||||
[(~constructor-extra-info tag _ _)
|
[(~constructor-extra-info tag _ _)
|
||||||
(syntax-e #'tag)]))
|
(syntax-e #'tag)]))
|
||||||
|
|
||||||
(define (get-type-args t)
|
(define (get-type-args t)
|
||||||
(syntax-parse (get-extra-info t)
|
(match (get-extra-info/new t)
|
||||||
|
[(list _ _ get)
|
||||||
|
(define f (syntax-local-value get))
|
||||||
|
(syntax->list (f #`(#,get #,t)))])
|
||||||
|
#;(syntax-parse (get-extra-info t)
|
||||||
[(~constructor-extra-info _ _ get)
|
[(~constructor-extra-info _ _ get)
|
||||||
(define f (syntax-local-value #'get))
|
(define f (syntax-local-value #'get))
|
||||||
(syntax->list (f #`(get #,t)))]))
|
(syntax->list (f #`(get #,t)))]))
|
||||||
|
|
||||||
(define (make-cons-type t args)
|
(define (make-cons-type t args)
|
||||||
(syntax-parse (get-extra-info t)
|
(match (get-extra-info/new t)
|
||||||
|
[(list _ mk _)
|
||||||
|
(define f (syntax-local-value mk))
|
||||||
|
(type-eval (f #`(#,mk #,@args)))])
|
||||||
|
#;(syntax-parse (get-extra-info t)
|
||||||
[(~constructor-extra-info _ mk _)
|
[(~constructor-extra-info _ mk _)
|
||||||
(define f (syntax-local-value #'mk))
|
(define f (syntax-local-value #'mk))
|
||||||
(type-eval (f #`(mk #,@args)))]))
|
(type-eval (f #`(mk #,@args)))]))
|
||||||
|
@ -586,11 +775,15 @@
|
||||||
#:datum-literals (:)
|
#:datum-literals (:)
|
||||||
[(_ lib [name:id : ty:type] ...)
|
[(_ lib [name:id : ty:type] ...)
|
||||||
#:with (name- ...) (format-ids "~a-" #'(name ...))
|
#:with (name- ...) (format-ids "~a-" #'(name ...))
|
||||||
|
#:with (serialized-ty ...) (for/list ([t (in-syntax #'(ty.norm ...))])
|
||||||
|
(serialize-syntax t))
|
||||||
(syntax/loc stx
|
(syntax/loc stx
|
||||||
(begin-
|
(begin-
|
||||||
(require (only-in lib [name name-] ...))
|
(require (only-in lib [name name-] ...))
|
||||||
(define-syntax name
|
(define-syntax name
|
||||||
(make-variable-like-transformer (add-orig (assign-type #'name- #'ty #:wrap? #f) #'name)))
|
(make-variable-like-transformer
|
||||||
|
(add-orig (assign-type #'name- (deserialize-syntax #'serialized-ty)
|
||||||
|
#:wrap? #f) #'name)))
|
||||||
...))]))
|
...))]))
|
||||||
|
|
||||||
;; Format identifiers in the same way
|
;; Format identifiers in the same way
|
||||||
|
@ -668,13 +861,14 @@
|
||||||
((current-typecheck-relation) t (mk-U*- '())))
|
((current-typecheck-relation) t (mk-U*- '())))
|
||||||
|
|
||||||
(define-for-syntax bot
|
(define-for-syntax bot
|
||||||
|
#;#'(U)
|
||||||
(mk-U*- '()))
|
(mk-U*- '()))
|
||||||
|
|
||||||
(define-for-syntax (flat-type? τ)
|
(define-for-syntax (flat-type? τ)
|
||||||
(syntax-parse τ
|
(syntax-parse τ
|
||||||
[(~→ τ ...) #f]
|
[(~→+ i ... o) #f]
|
||||||
[(~Actor τ) #f]
|
[(~Actor τ) #f]
|
||||||
[(~Role (_) _ ...) #f]
|
[(~Role+Body (_) _ ...) #f]
|
||||||
[_ #t]))
|
[_ #t]))
|
||||||
|
|
||||||
(define-for-syntax (strip-? t)
|
(define-for-syntax (strip-? t)
|
||||||
|
@ -735,7 +929,7 @@
|
||||||
|
|
||||||
;; Wanted test case, but can't use it bc it uses things defined for-syntax
|
;; Wanted test case, but can't use it bc it uses things defined for-syntax
|
||||||
#;(module+ test
|
#;(module+ test
|
||||||
(let ([r (type-eval #'(Role (x) (Shares Int)))])
|
(let ([r (type-eval #'(Role+Body (x) (Shares Int)))])
|
||||||
(syntax-parse (analyze-role-input/output r)
|
(syntax-parse (analyze-role-input/output r)
|
||||||
[(τ-i τ-o)
|
[(τ-i τ-o)
|
||||||
(check-true (type=? #'τ-o (type-eval #'Int)))])))
|
(check-true (type=? #'τ-o (type-eval #'Int)))])))
|
||||||
|
@ -757,13 +951,13 @@
|
||||||
(values bot (mk-Message- #'(τ-m)) bot bot bot)]
|
(values bot (mk-Message- #'(τ-m)) bot bot bot)]
|
||||||
[(~Realizes τ-m)
|
[(~Realizes τ-m)
|
||||||
(values bot bot bot (mk-Realize- #'(τ-m)) bot)]
|
(values bot bot bot (mk-Realize- #'(τ-m)) bot)]
|
||||||
[(~Role (name:id)
|
[(~Role+Body (name:id)
|
||||||
(~or (~Shares τ-s)
|
(~or (~Shares τ-s)
|
||||||
(~Know τ-k)
|
(~Know τ-k)
|
||||||
(~Sends τ-m)
|
(~Sends τ-m)
|
||||||
(~Realizes τ-rlz)
|
(~Realizes τ-rlz)
|
||||||
(~Reacts τ-if τ-then ...)) ...
|
(~Reacts τ-if τ-then ...)) ...
|
||||||
(~and (~Role _ ...) sub-role) ...)
|
(~and (~Role+Body _ _ ...) sub-role) ...)
|
||||||
#:with (msg ...) (for/list ([m (in-syntax #'(τ-m ...))])
|
#:with (msg ...) (for/list ([m (in-syntax #'(τ-m ...))])
|
||||||
(mk-Message- (list m)))
|
(mk-Message- (list m)))
|
||||||
#:with (rlz ...) (for/list ([r (in-syntax #'(τ-rlz ...))])
|
#:with (rlz ...) (for/list ([r (in-syntax #'(τ-rlz ...))])
|
||||||
|
@ -829,7 +1023,7 @@
|
||||||
(type-eval #'★/t)]
|
(type-eval #'★/t)]
|
||||||
[(~U* τ ...)
|
[(~U* τ ...)
|
||||||
(mk-U- (stx-map replace-bind-and-discard-with-★ #'(τ ...)))]
|
(mk-U- (stx-map replace-bind-and-discard-with-★ #'(τ ...)))]
|
||||||
[(~Any/bvs τ-cons () τ ...)
|
[(~Any/new τ-cons τ ...)
|
||||||
#:when (reassemblable? #'τ-cons)
|
#:when (reassemblable? #'τ-cons)
|
||||||
(define subitems (for/list ([t (in-syntax #'(τ ...))])
|
(define subitems (for/list ([t (in-syntax #'(τ ...))])
|
||||||
(replace-bind-and-discard-with-★ t)))
|
(replace-bind-and-discard-with-★ t)))
|
||||||
|
@ -855,6 +1049,18 @@
|
||||||
(paren-join (cons "U" (stx-map type->strX #'(τ ...))))]
|
(paren-join (cons "U" (stx-map type->strX #'(τ ...))))]
|
||||||
[(~Base x)
|
[(~Base x)
|
||||||
(un-gensym #'x)]
|
(un-gensym #'x)]
|
||||||
|
[(~Role+Body (x:id) τ ...)
|
||||||
|
(define nm (un-gensym #'x))
|
||||||
|
(define body (stx-map type->strX #'(τ ...)))
|
||||||
|
(paren-join (list* "Role" (format "(~a)" nm) body))]
|
||||||
|
[(~∀+ (X ...) τ)
|
||||||
|
(define vars
|
||||||
|
(paren-join (stx-map type->strX #'(X ...))))
|
||||||
|
(paren-join (list "∀" vars (type->strX #'τ)))]
|
||||||
|
[(~Any/new τ-cons τ ...)
|
||||||
|
(define ctor (un-gensym #'τ-cons))
|
||||||
|
(define body (stx-map type->strX #'(τ ...)))
|
||||||
|
(paren-join (cons ctor body))]
|
||||||
[(~Any/bvs τ-cons (X ...) τ ...)
|
[(~Any/bvs τ-cons (X ...) τ ...)
|
||||||
(define ctor (un-gensym #'τ-cons))
|
(define ctor (un-gensym #'τ-cons))
|
||||||
(define body (stx-map type->strX #'(τ ...)))
|
(define body (stx-map type->strX #'(τ ...)))
|
||||||
|
@ -879,13 +1085,16 @@
|
||||||
;; subtyping
|
;; subtyping
|
||||||
(define (<: t1 t2)
|
(define (<: t1 t2)
|
||||||
(when (trace-sub?)
|
(when (trace-sub?)
|
||||||
(printf "~a\n<:\n~a\n" t1 t2))
|
(unless (syntax-parse t1
|
||||||
|
[~Type #t]
|
||||||
|
[_ #f])
|
||||||
|
(printf "~a\n<:\n~a\n" t1 t2)))
|
||||||
(syntax-parse #`(#,t1 #,t2)
|
(syntax-parse #`(#,t1 #,t2)
|
||||||
[(_ ~★/t)
|
[(_ ~★/t)
|
||||||
(flat-type? t1)]
|
(flat-type? t1)]
|
||||||
[((~U* τ1 ...) _)
|
[((~U* τ1 ...) _)
|
||||||
(stx-andmap (lambda (t) (<: t t2)) #'(τ1 ...))]
|
(stx-andmap (lambda (t) (<: t t2)) #'(τ1 ...))]
|
||||||
[(_ (~U* τ2:type ...))
|
[(_ (~U* τ2 ...))
|
||||||
(stx-ormap (lambda (t) (<: t1 t)) #'(τ2 ...))]
|
(stx-ormap (lambda (t) (<: t1 t)) #'(τ2 ...))]
|
||||||
[((~Actor τ1) (~Actor τ2))
|
[((~Actor τ1) (~Actor τ2))
|
||||||
(and (<: #'τ1 #'τ2)
|
(and (<: #'τ1 #'τ2)
|
||||||
|
@ -908,20 +1117,38 @@
|
||||||
[(~Discard _)
|
[(~Discard _)
|
||||||
#t]
|
#t]
|
||||||
[(X:id Y:id)
|
[(X:id Y:id)
|
||||||
(free-identifier=? #'X #'Y)]
|
(or (free-identifier=? #'X #'Y)
|
||||||
[((~∀ (X:id ...) τ1) (~∀ (Y:id ...) τ2))
|
#;(let ()
|
||||||
|
(printf "X:\n")
|
||||||
|
(pretty-print (syntax-debug-info (values #;syntax-local-introduce #'X)))
|
||||||
|
(pretty-print (identifier-binding #'X))
|
||||||
|
(printf ":\n")
|
||||||
|
(pretty-print (syntax-debug-info (values #;syntax-local-introduce #'Y)))
|
||||||
|
(pretty-print (identifier-binding #'Y))
|
||||||
|
#f))]
|
||||||
|
[((~∀+ (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 "∀ <: ∀")
|
||||||
|
;; (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)]
|
(or (free-identifier=? #'τ1 #'τ2)
|
||||||
[((~Role (x) _ ...) (~Role (y) _ ...))
|
(let ()
|
||||||
|
(printf "τ1:\n")
|
||||||
|
(pretty-print (syntax-debug-info (values #;syntax-local-introduce #'τ1)))
|
||||||
|
(pretty-print (identifier-binding #'τ1))
|
||||||
|
(printf "τ2:\n")
|
||||||
|
(pretty-print (syntax-debug-info (values #;syntax-local-introduce #'τ2)))
|
||||||
|
(pretty-print (identifier-binding #'τ2))
|
||||||
|
#f))]
|
||||||
|
[((~Role+Body (x) _ ...) (~Role+Body (y) _ ...))
|
||||||
;; Extremely Coarse subtyping for Role types
|
;; Extremely Coarse subtyping for Role types
|
||||||
(type=? t1 t2)]
|
(type=? t1 t2)]
|
||||||
;; TODO: clauses for Roles, effectful functions, and so on
|
;; TODO: clauses for Roles, effectful functions, and so on
|
||||||
[((~Any/bvs τ-cons1 () τ1 ...) (~Any/bvs τ-cons2 () τ2 ...))
|
[((~Any/new τ-cons1 τ1 ...) (~Any/new τ-cons2 τ2 ...))
|
||||||
#:when (free-identifier=? #'τ-cons1 #'τ-cons2)
|
#:when (free-identifier=? #'τ-cons1 #'τ-cons2)
|
||||||
#:do [(define variances (syntax-property #'τ-cons1 'arg-variances))]
|
#:do [(define variances (get-arg-variances t1))]
|
||||||
#:when variances
|
#:when variances
|
||||||
#:when (stx-length=? #'(τ1 ...) #'(τ2 ...))
|
#:when (stx-length=? #'(τ1 ...) #'(τ2 ...))
|
||||||
(for/and ([ty1 (in-syntax #'(τ1 ...))]
|
(for/and ([ty1 (in-syntax #'(τ1 ...))]
|
||||||
|
@ -938,7 +1165,7 @@
|
||||||
[(== irrelevant)
|
[(== irrelevant)
|
||||||
#t]))]
|
#t]))]
|
||||||
[_
|
[_
|
||||||
#f]))
|
(type=? t1 t2)]))
|
||||||
|
|
||||||
;; shortcuts for mapping
|
;; shortcuts for mapping
|
||||||
(define ((<:l l) r)
|
(define ((<:l l) r)
|
||||||
|
@ -952,7 +1179,8 @@
|
||||||
;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
||||||
|
|
||||||
(begin-for-syntax
|
(begin-for-syntax
|
||||||
(current-typecheck-relation <:))
|
(current-typecheck-relation <:)
|
||||||
|
(current-check-relation <:))
|
||||||
|
|
||||||
;; Flat-Type Flat-Type -> Type
|
;; Flat-Type Flat-Type -> Type
|
||||||
;; Intersection
|
;; Intersection
|
||||||
|
@ -976,7 +1204,7 @@
|
||||||
[((~Base τ1:id) (~Base τ2:id))
|
[((~Base τ1:id) (~Base τ2:id))
|
||||||
#:when (free-identifier=? #'τ1 #'τ2)
|
#:when (free-identifier=? #'τ1 #'τ2)
|
||||||
t1]
|
t1]
|
||||||
[((~Any/bvs τ-cons1 () τ1 ...) (~Any/bvs τ-cons2 () τ2 ...))
|
[((~Any/new τ-cons1 τ1 ...) (~Any/new τ-cons2 τ2 ...))
|
||||||
#:when (free-identifier=? #'τ-cons1 #'τ-cons2)
|
#:when (free-identifier=? #'τ-cons1 #'τ-cons2)
|
||||||
#:when (stx-length=? #'(τ1 ...) #'(τ2 ...))
|
#:when (stx-length=? #'(τ1 ...) #'(τ2 ...))
|
||||||
#:do [(define desc (get-type-isec-desc #'τ-cons1))]
|
#:do [(define desc (get-type-isec-desc #'τ-cons1))]
|
||||||
|
@ -1009,7 +1237,7 @@
|
||||||
(stx-andmap (lambda (t) (project-safe? t t2)) #'(τ1 ...))]
|
(stx-andmap (lambda (t) (project-safe? t t2)) #'(τ1 ...))]
|
||||||
[(_ (~U* τ2:type ...))
|
[(_ (~U* τ2:type ...))
|
||||||
(stx-andmap (lambda (t) (project-safe? t1 t)) #'(τ2 ...))]
|
(stx-andmap (lambda (t) (project-safe? t1 t)) #'(τ2 ...))]
|
||||||
[((~Any/bvs τ-cons1 () τ1 ...) (~Any/bvs τ-cons2 () τ2 ...))
|
[((~Any/new τ-cons1 τ1 ...) (~Any/new τ-cons2 τ2 ...))
|
||||||
#:when (free-identifier=? #'τ-cons1 #'τ-cons2)
|
#:when (free-identifier=? #'τ-cons1 #'τ-cons2)
|
||||||
#:when (stx-length=? #'(τ1 ...) #'(τ2 ...))
|
#:when (stx-length=? #'(τ1 ...) #'(τ2 ...))
|
||||||
#:do [(define desc (get-type-isec-desc #'τ-cons1))]
|
#:do [(define desc (get-type-isec-desc #'τ-cons1))]
|
||||||
|
@ -1036,7 +1264,7 @@
|
||||||
[X:id
|
[X:id
|
||||||
#t]
|
#t]
|
||||||
[(~Base _) #t]
|
[(~Base _) #t]
|
||||||
[(~Any/bvs τ-cons (X ...) τ ...)
|
[(~Any/new τ-cons τ ...)
|
||||||
(stx-andmap finite? #'(τ ...))]))
|
(stx-andmap finite? #'(τ ...))]))
|
||||||
|
|
||||||
;; PatternType -> Type
|
;; PatternType -> Type
|
||||||
|
@ -1048,7 +1276,7 @@
|
||||||
(type-eval #'★/t)]
|
(type-eval #'★/t)]
|
||||||
[(~U* τ ...)
|
[(~U* τ ...)
|
||||||
(mk-U- (stx-map pattern-matching-assertions #'(τ ...)))]
|
(mk-U- (stx-map pattern-matching-assertions #'(τ ...)))]
|
||||||
[(~Any/bvs τ-cons () τ ...)
|
[(~Any/new τ-cons τ ...)
|
||||||
#:when (reassemblable? #'τ-cons)
|
#:when (reassemblable? #'τ-cons)
|
||||||
(define subitems (for/list ([t (in-syntax #'(τ ...))])
|
(define subitems (for/list ([t (in-syntax #'(τ ...))])
|
||||||
(pattern-matching-assertions t)))
|
(pattern-matching-assertions t)))
|
||||||
|
@ -1087,28 +1315,29 @@
|
||||||
(⇒ ν-s (~effs τ-s ...))
|
(⇒ ν-s (~effs τ-s ...))
|
||||||
(⇒ ν-f (~effs τ-f ...))]
|
(⇒ ν-f (~effs τ-f ...))]
|
||||||
----------------------------------------
|
----------------------------------------
|
||||||
[⊢ (lambda- (x- ...) body-) (⇒ : (→ τ ... (Computation (Value τ-e)
|
[⊢ (lambda- (x- ...) body-) (⇒ : (→+ τ ... (Computation (Value τ-e)
|
||||||
(Endpoints τ-ep ...)
|
(Endpoints τ-ep ...)
|
||||||
(Roles τ-f ...)
|
(Roles τ-f ...)
|
||||||
(Spawns τ-s ...))))])
|
(Spawns τ-s ...))))])
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
;; Type Abstraction
|
;; Type Abstraction
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
||||||
(define-typed-syntax (Λ (tv:id ...) e) ≫
|
(define-typed-syntax (Λ (tv:id ...) e) ≫
|
||||||
[([tv ≫ tv- :: #%type] ...) () ⊢ e ≫ e- ⇒ τ]
|
[([tv ≫ tv- : Type] ...) () ⊢ e ≫ e- ⇒ τ]
|
||||||
--------
|
--------
|
||||||
;; can't use internal mk-∀- constructor here
|
;; can't use internal mk-∀- constructor here
|
||||||
;; - will cause the bound-id=? quirk to show up
|
;; - will cause the bound-id=? quirk to show up
|
||||||
;; (when subsequent tyvar refs are expanded with `type` stx class)
|
;; (when subsequent tyvar refs are expanded with `type` stx class)
|
||||||
;; - requires converting type= and subst to use free-id=?
|
;; - requires converting type= and subst to use free-id=?
|
||||||
;; (which is less performant)
|
;; (which is less performant)
|
||||||
[⊢ e- ⇒ (∀ (tv- ...) τ)])
|
[⊢ e- ⇒ (∀+ (tv- ...) τ)])
|
||||||
|
|
||||||
(define-typed-syntax inst
|
(define-typed-syntax inst
|
||||||
[(_ e τ:type ...) ≫
|
[(_ e τ:type ...) ≫
|
||||||
#:cut
|
#:cut
|
||||||
[⊢ e ≫ e- ⇒ (~∀ tvs τ_body)]
|
[⊢ e ≫ e- ⇒ (~∀+ tvs τ_body)]
|
||||||
#:fail-unless (stx-andmap instantiable? #'tvs #'(τ.norm ...))
|
#:fail-unless (stx-andmap instantiable? #'tvs #'(τ.norm ...))
|
||||||
"types must be instantiable"
|
"types must be instantiable"
|
||||||
#:fail-unless (pure? #'e-) "expression must be pure"
|
#:fail-unless (pure? #'e-) "expression must be pure"
|
||||||
|
@ -1124,6 +1353,10 @@
|
||||||
(and (flat-type? ty)
|
(and (flat-type? ty)
|
||||||
(finite? ty))))
|
(finite? ty))))
|
||||||
|
|
||||||
|
#;(begin-for-syntax
|
||||||
|
(require racket/trace)
|
||||||
|
(trace instantiable?))
|
||||||
|
|
||||||
(begin-for-syntax
|
(begin-for-syntax
|
||||||
;; CONVENTION: Type variables for effects are prefixed with ρ
|
;; CONVENTION: Type variables for effects are prefixed with ρ
|
||||||
(define (row-variable? x)
|
(define (row-variable? x)
|
||||||
|
@ -1137,7 +1370,7 @@
|
||||||
;; instantiate row variables with types from procedure arguments
|
;; instantiate row variables with types from procedure arguments
|
||||||
;; BRITTLE?
|
;; BRITTLE?
|
||||||
(define-typed-syntax (call/inst e:expr args:expr ...) ≫
|
(define-typed-syntax (call/inst e:expr args:expr ...) ≫
|
||||||
[⊢ e ≫ e- (⇒ : (~∀ (X:row-id ...) τ))]
|
[⊢ e ≫ e- (⇒ : (~∀+ (X:row-id ...) τ))]
|
||||||
[⊢ args ≫ args- (⇒ : τ-a)] ...
|
[⊢ args ≫ args- (⇒ : τ-a)] ...
|
||||||
#:fail-unless (all-pure? #'(e- args- ...))
|
#:fail-unless (all-pure? #'(e- args- ...))
|
||||||
"expressions must be pure"
|
"expressions must be pure"
|
||||||
|
@ -1165,11 +1398,12 @@
|
||||||
(define-for-syntax (int-def-ctx-bind-type-rename x x- t ctx)
|
(define-for-syntax (int-def-ctx-bind-type-rename x x- t ctx)
|
||||||
(when DEBUG-BINDINGS?
|
(when DEBUG-BINDINGS?
|
||||||
(printf "adding to context ~a\n" (syntax-debug-info x)))
|
(printf "adding to context ~a\n" (syntax-debug-info x)))
|
||||||
|
(define serialized-ty (serialize-syntax t))
|
||||||
(syntax-local-bind-syntaxes (list x-) #f ctx)
|
(syntax-local-bind-syntaxes (list x-) #f ctx)
|
||||||
(syntax-local-bind-syntaxes (list x)
|
(syntax-local-bind-syntaxes (list x)
|
||||||
#`(make-rename-transformer
|
#`(make-rename-transformer
|
||||||
(add-orig
|
(add-orig
|
||||||
(attach #'#,x- ': #'#,t)
|
(attach #'#,x- ': (deserialize-syntax #'#,serialized-ty))
|
||||||
#'#,x)
|
#'#,x)
|
||||||
#;(add-orig (assign-type #'#,x- #'#,t #:wrap? #f) #'#,x))
|
#;(add-orig (assign-type #'#,x- #'#,t #:wrap? #f) #'#,x))
|
||||||
ctx))
|
ctx))
|
||||||
|
@ -1250,20 +1484,23 @@
|
||||||
[(_ [x:id x-:id τ e-] ...)
|
[(_ [x:id x-:id τ e-] ...)
|
||||||
#'(syndicate:field [x- e-] ...)]))
|
#'(syndicate:field [x- e-] ...)]))
|
||||||
|
|
||||||
|
(define-for-syntax KIND-TAG ':)
|
||||||
|
|
||||||
(define-syntax (define/intermediate stx)
|
(define-syntax (define/intermediate stx)
|
||||||
(syntax-parse stx
|
(syntax-parse stx
|
||||||
[(_ x:id x-:id τ e)
|
[(_ x:id x-:id τ e)
|
||||||
;; including a syntax binding for x allows for module-top-level references
|
;; including a syntax binding for x allows for module-top-level references
|
||||||
;; (where walk/bind won't replace further uses) and subsequent provides
|
;; (where walk/bind won't replace further uses) and subsequent provides
|
||||||
|
#:with serialized-τ (serialize-syntax #'τ)
|
||||||
#'(begin-
|
#'(begin-
|
||||||
(define-syntax x
|
(define-syntax x
|
||||||
(make-variable-like-transformer (add-orig (attach #'x- ': #'τ) #'x)))
|
(make-variable-like-transformer (add-orig (attach #'x- ': (deserialize-syntax #'serialized-τ)) #'x)))
|
||||||
(define- x- e))]))
|
(define- x- e))]))
|
||||||
|
|
||||||
;; copied from ext-stlc
|
;; copied from ext-stlc
|
||||||
(define-typed-syntax define
|
(define-typed-syntax define
|
||||||
[(_ x:id (~datum :) τ:type e:expr) ≫
|
[(_ x:id (~datum :) τ:type e:expr) ≫
|
||||||
|
#:cut
|
||||||
[⊢ e ≫ e- (⇐ : τ.norm) (⇒ ν-ep (~effs τ-ep ...)) (⇒ ν-f (~effs τ-f ...)) (⇒ ν-s (~effs τ-s ...))]
|
[⊢ e ≫ e- (⇐ : τ.norm) (⇒ ν-ep (~effs τ-ep ...)) (⇒ ν-f (~effs τ-f ...)) (⇒ ν-s (~effs τ-s ...))]
|
||||||
#:with x- (generate-temporary #'x)
|
#:with x- (generate-temporary #'x)
|
||||||
#:with x+ (syntax-local-identifier-as-binding #'x)
|
#:with x+ (syntax-local-identifier-as-binding #'x)
|
||||||
|
@ -1274,6 +1511,7 @@
|
||||||
(⇒ ν-f (τ-f ...))
|
(⇒ ν-f (τ-f ...))
|
||||||
(⇒ ν-s (τ-s ...))]]
|
(⇒ ν-s (τ-s ...))]]
|
||||||
[(_ x:id e) ≫
|
[(_ x:id e) ≫
|
||||||
|
#:cut
|
||||||
;This won't work with mutually recursive definitions
|
;This won't work with mutually recursive definitions
|
||||||
[⊢ e ≫ e- (⇒ : τ) (⇒ ν-ep (~effs τ-ep ...)) (⇒ ν-f (~effs τ-f ...)) (⇒ ν-s (~effs τ-s ...))]
|
[⊢ e ≫ e- (⇒ : τ) (⇒ ν-ep (~effs τ-ep ...)) (⇒ ν-f (~effs τ-f ...)) (⇒ ν-s (~effs τ-s ...))]
|
||||||
#:with x- (generate-temporary #'x)
|
#:with x- (generate-temporary #'x)
|
||||||
|
@ -1287,10 +1525,10 @@
|
||||||
[(_ (f [x (~optional (~datum :)) ty:type] ...
|
[(_ (f [x (~optional (~datum :)) ty:type] ...
|
||||||
(~or (~datum →) (~datum ->)) ty_out:type)
|
(~or (~datum →) (~datum ->)) ty_out:type)
|
||||||
e ...+) ≫
|
e ...+) ≫
|
||||||
|
#:cut
|
||||||
[⊢ (lambda ([x : ty] ...) (block e ...)) ≫ e- (⇒ : (~and fun-ty
|
[⊢ (lambda ([x : ty] ...) (block e ...)) ≫ e- (⇒ : (~and fun-ty
|
||||||
(~→ (~not (~Computation _ ...)) ...
|
(~→+ (~not (~Computation _ _ _ _)) ...
|
||||||
(~Computation (~Value τ-v)
|
(~Computation (~Value τ-v) _ _ _))))]
|
||||||
_ ...))))]
|
|
||||||
#:fail-unless (<: #'τ-v #'ty_out.norm)
|
#:fail-unless (<: #'τ-v #'ty_out.norm)
|
||||||
(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
|
#'τ-v #'ty_out
|
||||||
|
@ -1301,6 +1539,7 @@
|
||||||
[⊢ (erased (define/intermediate f f- fun-ty e-)) (⇒ : ★/t)]]
|
[⊢ (erased (define/intermediate f f- fun-ty e-)) (⇒ : ★/t)]]
|
||||||
[(_ (f [x (~optional (~datum :)) ty] ...)
|
[(_ (f [x (~optional (~datum :)) ty] ...)
|
||||||
e ...+) ≫
|
e ...+) ≫
|
||||||
|
#:cut
|
||||||
----------------------------
|
----------------------------
|
||||||
[≻ (define (f [x ty] ... -> ★/t) e ...)]]
|
[≻ (define (f [x ty] ... -> ★/t) e ...)]]
|
||||||
;; Polymorphic definitions
|
;; Polymorphic definitions
|
||||||
|
@ -1308,25 +1547,39 @@
|
||||||
(f [x (~optional (~datum :)) ty] ...
|
(f [x (~optional (~datum :)) ty] ...
|
||||||
(~or (~datum →) (~datum ->)) ty_out))
|
(~or (~datum →) (~datum ->)) ty_out))
|
||||||
e ...+) ≫
|
e ...+) ≫
|
||||||
|
#:cut
|
||||||
|
#:do [(displayln 'A)]
|
||||||
#:with e+ #'(Λ (X ...)
|
#:with e+ #'(Λ (X ...)
|
||||||
(lambda ([x : ty] ...)
|
(lambda ([x : ty] ...)
|
||||||
(block e ...)))
|
(block e ...)))
|
||||||
[[X ≫ X- :: #%type] ... ⊢ e+ ≫ e-
|
#:do [(displayln 'B)]
|
||||||
(⇒ : (~and res-ty
|
[[X ≫ X- : Type] ... ⊢ e+ ≫ e- (⇒ : TTTT)
|
||||||
(~∀ (Y ...)
|
#;(⇒ : (~and res-ty
|
||||||
(~→ (~not (~Computation _ ...)) ...
|
(~∀+ (Y ...)
|
||||||
(~Computation (~Value τ-v)
|
(~→ (~not (~Computation _ _ _ _)) ...
|
||||||
_ ...)))))]
|
(~Computation (~Value τ-v) _ _ _)))))]
|
||||||
#:fail-unless (<: (type-eval #'(∀ (Y ...) τ-v))
|
#:do [(displayln 'C)
|
||||||
(type-eval #'(∀ (X ...) ty_out)))
|
(local-require turnstile/typedefs)
|
||||||
|
(pretty-print (resugar-type #'TTTT))]
|
||||||
|
#:with (~and res-ty
|
||||||
|
(~∀+ (Y ...)
|
||||||
|
(~→+ (~not (~Computation _ _ _ _)) ...
|
||||||
|
(~Computation (~Value τ-v) _ _ _)))) #'TTTT
|
||||||
|
#:do [(displayln 'D)]
|
||||||
|
#:with ty_out- (substs #'(X- ...) #'(X ...) #'ty_out)
|
||||||
|
#:with actual (type-eval #'(∀+ (Y ...) τ-v))
|
||||||
|
#: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)]
|
||||||
#:with f- (add-orig (generate-temporary #'f) #'f)
|
#:with f- (add-orig (generate-temporary #'f) #'f)
|
||||||
-------------------------------------------------------
|
-------------------------------------------------------
|
||||||
[⊢ (erased (define/intermediate f f- res-ty e-)) (⇒ : ★/t)]]
|
[⊢ (erased (define/intermediate f f- res-ty e-)) (⇒ : ★/t)]]
|
||||||
[(_ ((~datum ∀) (X:id ...)
|
[(_ ((~datum ∀) (X:id ...)
|
||||||
(f [x (~optional (~datum :)) ty] ...))
|
(f [x (~optional (~datum :)) ty] ...))
|
||||||
e ...+) ≫
|
e ...+) ≫
|
||||||
|
#:cut
|
||||||
--------------------------------------------------
|
--------------------------------------------------
|
||||||
[≻ (define (∀ (X ...) (f [x ty] ... -> ★/t)) e ...)]])
|
[≻ (define (∀ (X ...) (f [x ty] ... -> ★/t)) e ...)]])
|
||||||
|
|
||||||
|
@ -1358,26 +1611,28 @@
|
||||||
(define-typed-syntax #%app
|
(define-typed-syntax #%app
|
||||||
;; Polymorphic, Effectful Function - Perform Simple Matching on Argument Types
|
;; Polymorphic, Effectful Function - Perform Simple Matching on Argument Types
|
||||||
[(_ e_fn e_arg ...) ≫
|
[(_ e_fn e_arg ...) ≫
|
||||||
[⊢ e_fn ≫ e_fn- (⇒ : (~∀ (X:row-id ...+) τ))]
|
[⊢ e_fn ≫ e_fn- (⇒ : (~∀+ (X:row-id ...+) τ))]
|
||||||
---------------------------------------------
|
---------------------------------------------
|
||||||
[≻ (call/inst e_fn- e_arg ...)]]
|
[≻ (call/inst e_fn- e_arg ...)]]
|
||||||
;; Polymorphic, Pure Function - Perform Local Inference
|
;; Polymorphic, Pure Function - Perform Local Inference
|
||||||
[(_ e_fn e_arg ...) ≫
|
[(_ e_fn e_arg ...) ≫
|
||||||
;; compute fn type (ie ∀ and →)
|
;; compute fn type (ie ∀ and →)
|
||||||
[⊢ e_fn ≫ e_fn- ⇒ (~∀ Xs (~→fn tyX_in ... tyX_out))]
|
[⊢ e_fn ≫ e_fn- ⇒ (~∀+ Xs (~→fn tyX_in ... tyX_out))]
|
||||||
;; successfully matched a polymorphic fn type, don't backtrack
|
;; successfully matched a polymorphic fn type, don't backtrack
|
||||||
#:cut
|
#:cut
|
||||||
|
#:do [(printf "A\n")]
|
||||||
#:with tyX_args #'(tyX_in ... tyX_out)
|
#:with tyX_args #'(tyX_in ... tyX_out)
|
||||||
;; solve for type variables Xs
|
;; solve for type variables Xs
|
||||||
#:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args this-syntax)
|
#:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args this-syntax)
|
||||||
;; make sure types are legal
|
;; make sure types are legal
|
||||||
#:with tyXs (inst-types/cs #'Xs* #'cs #'Xs)
|
#:with tyXs (ttc:inst-types/cs #'Xs* #'cs #'Xs)
|
||||||
#:fail-unless (for/and ([ty (in-syntax #'tyXs)]
|
#:fail-unless (for/and ([ty (in-syntax #'tyXs)]
|
||||||
[x (in-syntax #'Xs)])
|
[x (in-syntax #'Xs)])
|
||||||
(instantiable? x ty))
|
(instantiable? x ty))
|
||||||
"type variables must be flat and finite"
|
"type variables must be flat and finite"
|
||||||
;; instantiate polymorphic function type
|
;; instantiate polymorphic function type
|
||||||
#:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args)
|
#:do [(printf "B\n")]
|
||||||
|
#:with [τ_in ... τ_out] (ttc:inst-types/cs #'Xs* #'cs #'tyX_args)
|
||||||
#:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out)
|
#:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out)
|
||||||
;; arity check
|
;; arity check
|
||||||
#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
|
#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
|
||||||
|
@ -1388,6 +1643,7 @@
|
||||||
#:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))
|
#:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))
|
||||||
;; typecheck args
|
;; typecheck args
|
||||||
[τ_arg τ⊑ τ_in #:for e_arg] ...
|
[τ_arg τ⊑ τ_in #:for e_arg] ...
|
||||||
|
#:do [(printf "C\n")]
|
||||||
#:with τ_out* (if (stx-null? #'(unsolved-X ...))
|
#:with τ_out* (if (stx-null? #'(unsolved-X ...))
|
||||||
#'τ_out
|
#'τ_out
|
||||||
(syntax-parse #'τ_out
|
(syntax-parse #'τ_out
|
||||||
|
@ -1400,17 +1656,18 @@
|
||||||
#f
|
#f
|
||||||
(mk-app-poly-infer-error this-syntax #'(τ_in ...) #'(τ_arg ...) #'e_fn)
|
(mk-app-poly-infer-error this-syntax #'(τ_in ...) #'(τ_arg ...) #'e_fn)
|
||||||
this-syntax)))
|
this-syntax)))
|
||||||
(mk-∀- #'(unsolved-X ... Y ...) #'(τ_out))]))
|
(type-eval #'(∀+ (unsolved-X ... Y ...) τ_out))]))
|
||||||
|
#:do [(printf "D\n")]
|
||||||
--------
|
--------
|
||||||
[⊢ (#%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 ...])
|
||||||
|
@ -1439,7 +1696,8 @@
|
||||||
(stx-contains-id? ty X))]
|
(stx-contains-id? ty X))]
|
||||||
[(~Base _) #f]
|
[(~Base _) #f]
|
||||||
[X:id #f]
|
[X:id #f]
|
||||||
[(~Any/bvs _ _ τ ...)
|
[(~or* (~Any/new _ τ ...)
|
||||||
|
(~Any/bvs _ _ τ ...))
|
||||||
(for/or ([ty2 (in-syntax #'(τ ...))])
|
(for/or ([ty2 (in-syntax #'(τ ...))])
|
||||||
(tyvar-under-union? Xs ty2))]
|
(tyvar-under-union? Xs ty2))]
|
||||||
[_
|
[_
|
||||||
|
@ -1466,7 +1724,7 @@
|
||||||
((current-type-eval) (get-expected-type stx)))
|
((current-type-eval) (get-expected-type stx)))
|
||||||
(define initial-cs
|
(define initial-cs
|
||||||
(if (and (syntax-e #'expected-ty) (stx-null? #'Vs))
|
(if (and (syntax-e #'expected-ty) (stx-null? #'Vs))
|
||||||
(add-constraints Xs '() (list (list #'expected-ty #'τ_outX)))
|
(ttc:add-constraints Xs '() (list (list #'expected-ty #'τ_outX)))
|
||||||
'()))
|
'()))
|
||||||
(syntax-parse stx
|
(syntax-parse stx
|
||||||
[(_ e_fn . args)
|
[(_ e_fn . args)
|
||||||
|
@ -1474,7 +1732,7 @@
|
||||||
(for/fold ([as- null] [cs initial-cs])
|
(for/fold ([as- null] [cs initial-cs])
|
||||||
([a (in-stx-list #'args)]
|
([a (in-stx-list #'args)]
|
||||||
[tyXin (in-stx-list #'(τ_inX ...))])
|
[tyXin (in-stx-list #'(τ_inX ...))])
|
||||||
(define ty_in (inst-type/cs/orig Xs cs tyXin datum=?))
|
(define ty_in (ttc:inst-type/cs/orig Xs cs tyXin datum=?))
|
||||||
(when (tyvar-under-union? Xs ty_in)
|
(when (tyvar-under-union? Xs ty_in)
|
||||||
(type-error #:src a
|
(type-error #:src a
|
||||||
#:msg (format "can't infer types with unions: ~a\nraw: ~a"
|
#:msg (format "can't infer types with unions: ~a\nraw: ~a"
|
||||||
|
@ -1489,8 +1747,8 @@
|
||||||
(type->str #'ty_a) #'ty_a)))
|
(type->str #'ty_a) #'ty_a)))
|
||||||
(values
|
(values
|
||||||
(cons #'a- as-)
|
(cons #'a- as-)
|
||||||
(add-constraints Xs cs (list (list ty_in #'ty_a))
|
(ttc:add-constraints Xs cs (list (list ty_in #'ty_a))
|
||||||
(list (list (inst-type/cs/orig
|
(list (list (ttc:inst-type/cs/orig
|
||||||
Xs cs ty_in
|
Xs cs ty_in
|
||||||
datum=?)
|
datum=?)
|
||||||
#'ty_a))))))
|
#'ty_a))))))
|
||||||
|
@ -1540,9 +1798,9 @@
|
||||||
(for/list ([X (in-list Xs)])
|
(for/list ([X (in-list Xs)])
|
||||||
(cond [(free-identifier=? X #'A) ctxt-variance]
|
(cond [(free-identifier=? X #'A) ctxt-variance]
|
||||||
[else irrelevant]))]
|
[else irrelevant]))]
|
||||||
[(~Any tycons)
|
[(~Any/new tycons)
|
||||||
(stx-map (λ _ irrelevant) Xs)]
|
(stx-map (λ _ irrelevant) Xs)]
|
||||||
[(~?∀ () (~Any tycons τ ...))
|
[(~?∀ () (~Any/new tycons τ ...))
|
||||||
#:when (get-arg-variances #'tycons)
|
#:when (get-arg-variances #'tycons)
|
||||||
#:when (stx-length=? #'[τ ...] (get-arg-variances #'tycons))
|
#:when (stx-length=? #'[τ ...] (get-arg-variances #'tycons))
|
||||||
(define τ-ctxt-variances
|
(define τ-ctxt-variances
|
||||||
|
@ -1551,7 +1809,7 @@
|
||||||
(for/fold ([acc (stx-map (λ _ irrelevant) Xs)])
|
(for/fold ([acc (stx-map (λ _ irrelevant) Xs)])
|
||||||
([τ (in-stx-list #'[τ ...])]
|
([τ (in-stx-list #'[τ ...])]
|
||||||
[τ-ctxt-variance (in-list τ-ctxt-variances)])
|
[τ-ctxt-variance (in-list τ-ctxt-variances)])
|
||||||
(map variance-join
|
(map mvc:variance-join
|
||||||
acc
|
acc
|
||||||
(find-variances Xs τ τ-ctxt-variance)))]
|
(find-variances Xs τ τ-ctxt-variance)))]
|
||||||
[ty
|
[ty
|
||||||
|
@ -1559,3 +1817,18 @@
|
||||||
(stx-contains-id? #'ty X)))
|
(stx-contains-id? #'ty X)))
|
||||||
(stx-map (λ _ irrelevant) Xs)]
|
(stx-map (λ _ irrelevant) Xs)]
|
||||||
[_ (stx-map (λ _ invariant) Xs)])))
|
[_ (stx-map (λ _ invariant) Xs)])))
|
||||||
|
|
||||||
|
#;(begin-for-syntax
|
||||||
|
(define t #'Unit)
|
||||||
|
(define t- ((current-type-eval) t))
|
||||||
|
(displayln ((current-type?) t-))
|
||||||
|
(define tt (syntax-parse (detach t- ':)
|
||||||
|
[(#%plain-app x) #'x]))
|
||||||
|
(pretty-print (syntax-debug-info tt)))
|
||||||
|
|
||||||
|
#;(begin-for-syntax
|
||||||
|
(define t #'(→ Unit Unit))
|
||||||
|
#;(define t #'(Actor Unit))
|
||||||
|
(define t- ((current-type-eval) t))
|
||||||
|
(values #;displayln ((current-type?) t-))
|
||||||
|
(printf "flat-type? ~a\n" (flat-type? t-)))
|
||||||
|
|
|
@ -19,8 +19,13 @@
|
||||||
(U (Left A)
|
(U (Left A)
|
||||||
(Right B)))
|
(Right B)))
|
||||||
|
|
||||||
|
(define (∀ (X) (f [x : X] -> X))
|
||||||
|
x)
|
||||||
|
|
||||||
|
|
||||||
(define (∀ (X Y Z) (partition/either [xs : (List X)]
|
(define (∀ (X Y Z) (partition/either [xs : (List X)]
|
||||||
[pred : (→fn X (Either Y Z))]
|
[pred : (→fn X (U (Left Y)
|
||||||
|
(Right Z)) #;(Either Y Z))]
|
||||||
-> (Tuple (List Y) (List Z))))
|
-> (Tuple (List Y) (List Z))))
|
||||||
(for/fold ([acc (Tuple (List Y) (List Z)) (tuple (list) (list))])
|
(for/fold ([acc (Tuple (List Y) (List Z)) (tuple (list) (list))])
|
||||||
([x xs])
|
([x xs])
|
||||||
|
|
|
@ -3,6 +3,7 @@
|
||||||
;; ---------------------------------------------------------------------------------------------------
|
;; ---------------------------------------------------------------------------------------------------
|
||||||
;; Protocol
|
;; Protocol
|
||||||
|
|
||||||
|
|
||||||
#|
|
#|
|
||||||
Conversations in the flink dataspace primarily concern two topics: presence and
|
Conversations in the flink dataspace primarily concern two topics: presence and
|
||||||
task execution.
|
task execution.
|
||||||
|
@ -168,9 +169,12 @@ The JobManager then performs the job and, when finished, asserts
|
||||||
(printf fmt . args)
|
(printf fmt . args)
|
||||||
(printf "\n")))
|
(printf "\n")))
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
;; ---------------------------------------------------------------------------------------------------
|
;; ---------------------------------------------------------------------------------------------------
|
||||||
;; TaskRunner
|
;; TaskRunner
|
||||||
|
|
||||||
|
|
||||||
(define (word-count-increment [h : WordCount]
|
(define (word-count-increment [h : WordCount]
|
||||||
[word : String]
|
[word : String]
|
||||||
-> WordCount)
|
-> WordCount)
|
||||||
|
@ -214,6 +218,7 @@ The JobManager then performs the job and, when finished, asserts
|
||||||
;; ---------------------------------------------------------------------------------------------------
|
;; ---------------------------------------------------------------------------------------------------
|
||||||
;; TaskManager
|
;; TaskManager
|
||||||
|
|
||||||
|
|
||||||
(define (spawn-task-manager [num-task-runners : Int])
|
(define (spawn-task-manager [num-task-runners : Int])
|
||||||
(define id (gensym 'task-manager))
|
(define id (gensym 'task-manager))
|
||||||
(spawn τc
|
(spawn τc
|
||||||
|
@ -281,23 +286,9 @@ The JobManager then performs the job and, when finished, asserts
|
||||||
[(finished discard)
|
[(finished discard)
|
||||||
(set! status st)])))))))))
|
(set! status st)])))))))))
|
||||||
|
|
||||||
|
|
||||||
;; ---------------------------------------------------------------------------------------------------
|
;; ---------------------------------------------------------------------------------------------------
|
||||||
;; JobManager
|
;; JobManager
|
||||||
|
|
||||||
;; Task -> Bool
|
|
||||||
;; Test if the task is ready to run
|
|
||||||
(define (task-ready? [t : PendingTask] -> (Maybe ConcreteTask))
|
|
||||||
(match t
|
|
||||||
[(task $tid (map-work $s))
|
|
||||||
;; having to re-produce this is directly bc of no occurrence typing
|
|
||||||
(some (task tid (map-work s)))]
|
|
||||||
[(task $tid (reduce-work (right $v1)
|
|
||||||
(right $v2)))
|
|
||||||
(some (task tid (reduce-work v1 v2)))]
|
|
||||||
[_
|
|
||||||
none]))
|
|
||||||
|
|
||||||
;; Task Int Any -> Task
|
;; Task Int Any -> Task
|
||||||
;; If the given task is waiting for this data, replace the waiting ID with the data
|
;; If the given task is waiting for this data, replace the waiting ID with the data
|
||||||
(define (task+data [t : PendingTask]
|
(define (task+data [t : PendingTask]
|
||||||
|
@ -321,6 +312,20 @@ The JobManager then performs the job and, when finished, asserts
|
||||||
(define l (split-at/lenient- xs n))
|
(define l (split-at/lenient- xs n))
|
||||||
(tuple (first l) (second l)))
|
(tuple (first l) (second l)))
|
||||||
|
|
||||||
|
;; Task -> Bool
|
||||||
|
;; Test if the task is ready to run
|
||||||
|
(define (task-ready? [t : PendingTask] -> (Maybe ConcreteTask))
|
||||||
|
(match t
|
||||||
|
[(task $tid (map-work $s))
|
||||||
|
;; having to re-produce this is directly bc of no occurrence typing
|
||||||
|
(some (task tid (map-work s)))]
|
||||||
|
[(task $tid (reduce-work (right $v1)
|
||||||
|
(right $v2)))
|
||||||
|
(some (task tid (reduce-work v1 v2)))]
|
||||||
|
[_
|
||||||
|
none]))
|
||||||
|
|
||||||
|
|
||||||
(define (partition-ready-tasks [tasks : (List PendingTask)]
|
(define (partition-ready-tasks [tasks : (List PendingTask)]
|
||||||
-> (Tuple (List PendingTask)
|
-> (Tuple (List PendingTask)
|
||||||
(List ConcreteTask)))
|
(List ConcreteTask)))
|
||||||
|
@ -333,6 +338,27 @@ The JobManager then performs the job and, when finished, asserts
|
||||||
[none
|
[none
|
||||||
(left t)]))))
|
(left t)]))))
|
||||||
|
|
||||||
|
|
||||||
|
#;(define (partition-ready-tasks [tasks : (List Int)]
|
||||||
|
-> (Tuple (List Int)
|
||||||
|
(List Int)))
|
||||||
|
(define part (inst partition/either Int Int Int))
|
||||||
|
(part tasks
|
||||||
|
(lambda ([t : Int])
|
||||||
|
(right 0)
|
||||||
|
#;(match (some 5)
|
||||||
|
[(some $ct)
|
||||||
|
(right ct)]
|
||||||
|
[none
|
||||||
|
(left 0)]))))
|
||||||
|
|
||||||
|
#;(define (debug [tasks : (List Int)] -> (Tuple (List String) (List Int)))
|
||||||
|
(define part (inst partition/either Int String Int))
|
||||||
|
(tuple (list) (list))
|
||||||
|
(part tasks
|
||||||
|
(lambda ([t : Int])
|
||||||
|
(left "hi"))))
|
||||||
|
|
||||||
(define (input->pending-task [t : InputTask] -> PendingTask)
|
(define (input->pending-task [t : InputTask] -> PendingTask)
|
||||||
(match t
|
(match t
|
||||||
[(task $id (map-work $s))
|
[(task $id (map-work $s))
|
||||||
|
@ -341,6 +367,7 @@ The JobManager then performs the job and, when finished, asserts
|
||||||
[(task $id (reduce-work $l $r))
|
[(task $id (reduce-work $l $r))
|
||||||
(task id (reduce-work (left l) (left r)))]))
|
(task id (reduce-work (left l) (left r)))]))
|
||||||
|
|
||||||
|
|
||||||
(message-struct tasks-finished : TasksFinished (id results))
|
(message-struct tasks-finished : TasksFinished (id results))
|
||||||
|
|
||||||
;; assertions used for internal slot-management protocol
|
;; assertions used for internal slot-management protocol
|
||||||
|
|
|
@ -14,7 +14,7 @@
|
||||||
Branch Effs
|
Branch Effs
|
||||||
FacetName Field ★/t
|
FacetName Field ★/t
|
||||||
Observe Inbound Outbound Actor U ⊥
|
Observe Inbound Outbound Actor U ⊥
|
||||||
Computation Value Endpoints Roles Spawns
|
Computation Value Endpoints Roles Spawns Sends
|
||||||
→fn proc
|
→fn proc
|
||||||
;; Statements
|
;; Statements
|
||||||
let let* if spawn dataspace start-facet set! begin stop begin/dataflow #;unsafe-do
|
let let* if spawn dataspace start-facet set! begin stop begin/dataflow #;unsafe-do
|
||||||
|
@ -84,6 +84,7 @@
|
||||||
(require (for-meta 2 macrotypes/stx-utils racket/list syntax/stx syntax/parse racket/base))
|
(require (for-meta 2 macrotypes/stx-utils racket/list syntax/stx syntax/parse racket/base))
|
||||||
(require macrotypes/postfix-in)
|
(require macrotypes/postfix-in)
|
||||||
(require (for-syntax turnstile/mode))
|
(require (for-syntax turnstile/mode))
|
||||||
|
(require turnstile/typedefs)
|
||||||
(require (postfix-in - racket/list))
|
(require (postfix-in - racket/list))
|
||||||
(require (postfix-in - racket/set))
|
(require (postfix-in - racket/set))
|
||||||
|
|
||||||
|
@ -139,7 +140,7 @@
|
||||||
(~and τ-k (~Know _))
|
(~and τ-k (~Know _))
|
||||||
;; untyped syndicate might allow this - TODO
|
;; untyped syndicate might allow this - TODO
|
||||||
#;(~and τ-m (~Sends _))
|
#;(~and τ-m (~Sends _))
|
||||||
(~and τ-r (~Reacts _ ...))
|
(~and τ-r (~Reacts _ _ ...))
|
||||||
~MakesField)
|
~MakesField)
|
||||||
...)
|
...)
|
||||||
ep-effects
|
ep-effects
|
||||||
|
@ -204,7 +205,7 @@
|
||||||
(⇒ ν-ep (~effs))
|
(⇒ ν-ep (~effs))
|
||||||
(⇒ ν-s (~effs))
|
(⇒ ν-s (~effs))
|
||||||
(⇒ ν-f (~effs τ-f ...))]
|
(⇒ ν-f (~effs τ-f ...))]
|
||||||
#:with τ (mk-Stop- #`(facet-name- τ-f ...))
|
#:with τ #'(Stop facet-name- τ-f ...)
|
||||||
---------------------------------------------------------------------------------
|
---------------------------------------------------------------------------------
|
||||||
[⊢ (syndicate:stop-facet facet-name- cont-) (⇒ : ★/t)
|
[⊢ (syndicate:stop-facet facet-name- cont-) (⇒ : ★/t)
|
||||||
(⇒ ν-f (τ))])
|
(⇒ ν-f (τ))])
|
||||||
|
@ -450,7 +451,7 @@
|
||||||
#'τ]
|
#'τ]
|
||||||
[(~U* τ ...)
|
[(~U* τ ...)
|
||||||
(mk-U- (stx-map instantiate-pattern-type #'(τ ...)))]
|
(mk-U- (stx-map instantiate-pattern-type #'(τ ...)))]
|
||||||
[(~Any/bvs τ-cons () τ ...)
|
[(~Any/new τ-cons τ ...)
|
||||||
#:when (reassemblable? #'τ-cons)
|
#:when (reassemblable? #'τ-cons)
|
||||||
(define subitems (for/list ([t (in-syntax #'(τ ...))])
|
(define subitems (for/list ([t (in-syntax #'(τ ...))])
|
||||||
(instantiate-pattern-type t)))
|
(instantiate-pattern-type t)))
|
||||||
|
@ -609,6 +610,12 @@
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
||||||
(module+ test
|
(module+ test
|
||||||
|
(check-type
|
||||||
|
(spawn (U (Observe (Tuple Int ★/t)))
|
||||||
|
(start-facet echo
|
||||||
|
(on (message (tuple 1 $x))
|
||||||
|
#f)))
|
||||||
|
: ★/t)
|
||||||
(check-type (spawn (U (Message (Tuple String Int))
|
(check-type (spawn (U (Message (Tuple String Int))
|
||||||
(Observe (Tuple String ★/t)))
|
(Observe (Tuple String ★/t)))
|
||||||
(start-facet echo
|
(start-facet echo
|
||||||
|
|
|
@ -0,0 +1,317 @@
|
||||||
|
#lang racket/base
|
||||||
|
|
||||||
|
(provide serialize-syntax deserialize-syntax)
|
||||||
|
|
||||||
|
(require racket/dict racket/match)
|
||||||
|
|
||||||
|
(struct serialized-syntax (unique-tag table contents) #:prefab)
|
||||||
|
(struct stx-with-props (stx ps) #:prefab)
|
||||||
|
(struct syntax-val (stx) #:prefab)
|
||||||
|
(struct datum-val (d) #:prefab)
|
||||||
|
(struct ref (unique-tag sym) #:prefab)
|
||||||
|
|
||||||
|
;(require racket/pretty)
|
||||||
|
|
||||||
|
(define (serialize-syntax stx)
|
||||||
|
(displayln 'serialize)
|
||||||
|
;(print-syntax-width +inf.0)
|
||||||
|
;(println stx)
|
||||||
|
;(pretty-print (syntax->datum stx))
|
||||||
|
|
||||||
|
(define unique-tag (gensym))
|
||||||
|
(define table (hasheq))
|
||||||
|
(define dedup-table (hasheq))
|
||||||
|
(define (dedup k f)
|
||||||
|
(if (hash-has-key? dedup-table k)
|
||||||
|
(hash-ref dedup-table k)
|
||||||
|
(let ([res (f)])
|
||||||
|
(set! dedup-table (hash-set dedup-table k res))
|
||||||
|
res)))
|
||||||
|
|
||||||
|
(define (lift! el)
|
||||||
|
(define tag-sym (gensym))
|
||||||
|
(set! table (hash-set table tag-sym el))
|
||||||
|
(ref unique-tag tag-sym))
|
||||||
|
|
||||||
|
(define (build-props! orig-s d)
|
||||||
|
(stx-with-props
|
||||||
|
(datum->syntax orig-s d orig-s #f)
|
||||||
|
(for/list ([k (syntax-property-symbol-keys orig-s)]
|
||||||
|
#:when (syntax-property-preserved? orig-s k))
|
||||||
|
(define val (syntax-property orig-s k))
|
||||||
|
(define serialized-val
|
||||||
|
(if (syntax? val)
|
||||||
|
(syntax-val (serialize-element! val))
|
||||||
|
(datum-val (serialize-element! val #:always-lift? #t))))
|
||||||
|
(cons k serialized-val))))
|
||||||
|
|
||||||
|
(define (serialize-element! el #:always-lift? [always-lift? #f])
|
||||||
|
(dedup
|
||||||
|
el
|
||||||
|
(lambda ()
|
||||||
|
(syntax-map
|
||||||
|
el
|
||||||
|
(lambda (tail? d) d)
|
||||||
|
(lambda (orig-s d)
|
||||||
|
;(when (and always-lift? (not (ref? (hash-ref dedup-table orig-s)))) ; TODO
|
||||||
|
;(error 'dedup "lift error"))
|
||||||
|
(dedup
|
||||||
|
orig-s
|
||||||
|
(lambda ()
|
||||||
|
(if (or always-lift?
|
||||||
|
(ormap (lambda (p) (syntax-property-preserved? orig-s p))
|
||||||
|
(syntax-property-symbol-keys orig-s)))
|
||||||
|
(lift! (build-props! orig-s d))
|
||||||
|
(datum->syntax orig-s d orig-s #f)))))
|
||||||
|
syntax-e))))
|
||||||
|
|
||||||
|
(define top-s (serialize-element! stx))
|
||||||
|
(define res (datum->syntax #f (serialized-syntax unique-tag table top-s)))
|
||||||
|
|
||||||
|
;(displayln 'serialize-out)
|
||||||
|
;(println res)
|
||||||
|
;(pretty-print (syntax->datum res))
|
||||||
|
res)
|
||||||
|
|
||||||
|
(define (deserialize-syntax ser)
|
||||||
|
(displayln 'deserialize)
|
||||||
|
;(print-syntax-width +inf.0)
|
||||||
|
;(println ser)
|
||||||
|
;(pretty-print (syntax->datum ser))
|
||||||
|
(match (syntax-e ser)
|
||||||
|
[(serialized-syntax unique-tag-stx table-stx contents)
|
||||||
|
(define unique-tag (syntax-e unique-tag-stx))
|
||||||
|
(define table (syntax-e table-stx))
|
||||||
|
(define dedup-table (hasheq))
|
||||||
|
(define (dedup k f)
|
||||||
|
(if (hash-has-key? dedup-table k)
|
||||||
|
(hash-ref dedup-table k)
|
||||||
|
(let ([res (f)])
|
||||||
|
(set! dedup-table (hash-set dedup-table k res))
|
||||||
|
res)))
|
||||||
|
|
||||||
|
|
||||||
|
(define (maybe-syntax-e v)
|
||||||
|
(if (syntax? v) (syntax-e v) v))
|
||||||
|
|
||||||
|
(define (deserialize-stx-with-props ref-sym)
|
||||||
|
(match-define (stx-with-props stx ps) (syntax-e (hash-ref table ref-sym)))
|
||||||
|
(define deserialized-nested-stx (deserialize-element stx))
|
||||||
|
(for/fold ([stx deserialized-nested-stx])
|
||||||
|
([stx-pr (syntax->list ps)])
|
||||||
|
(define pr (syntax-e stx-pr))
|
||||||
|
(define k (syntax-e (car pr)))
|
||||||
|
(define v (syntax-e (cdr pr)))
|
||||||
|
(define prop-val
|
||||||
|
(match v
|
||||||
|
[(syntax-val v)
|
||||||
|
(deserialize-element v)]
|
||||||
|
[(datum-val v)
|
||||||
|
(deserialize-element (syntax->datum v))]))
|
||||||
|
(syntax-property stx k prop-val #t)))
|
||||||
|
|
||||||
|
(define (deserialize-element el)
|
||||||
|
(dedup
|
||||||
|
el
|
||||||
|
(lambda ()
|
||||||
|
(syntax-map
|
||||||
|
el
|
||||||
|
(lambda (tail? d)
|
||||||
|
(match d
|
||||||
|
[(ref tag sym)
|
||||||
|
#:when (equal? (maybe-syntax-e tag) unique-tag)
|
||||||
|
(dedup
|
||||||
|
sym
|
||||||
|
(lambda () (deserialize-stx-with-props (maybe-syntax-e sym))))]
|
||||||
|
[_ d]))
|
||||||
|
(lambda (orig-s d)
|
||||||
|
(dedup
|
||||||
|
orig-s
|
||||||
|
(lambda () (datum->syntax orig-s d orig-s #f))))
|
||||||
|
syntax-e))))
|
||||||
|
|
||||||
|
(define res (deserialize-element contents))
|
||||||
|
;(displayln 'deserialize-out)
|
||||||
|
;(println res)
|
||||||
|
;(pretty-print (syntax->datum res))
|
||||||
|
res]))
|
||||||
|
|
||||||
|
(module+ test
|
||||||
|
(require rackunit)
|
||||||
|
|
||||||
|
(define type
|
||||||
|
(syntax-property
|
||||||
|
(syntax-property #'Int ':: #'Type #t)
|
||||||
|
'orig (list #'Int) #t))
|
||||||
|
(define term (syntax-property #`(1 #,(syntax-property #'2 ': type #t)) ': #'Type #t))
|
||||||
|
(define s (serialize-syntax term))
|
||||||
|
(define d (deserialize-syntax s))
|
||||||
|
|
||||||
|
(check-true
|
||||||
|
(bound-identifier=?
|
||||||
|
(syntax-property d ':)
|
||||||
|
#'Type))
|
||||||
|
|
||||||
|
; syntax with properties inside outer syntax with properties.
|
||||||
|
(check-true
|
||||||
|
(bound-identifier=?
|
||||||
|
(syntax-property (syntax-property (cadr (syntax-e d)) ':) '::)
|
||||||
|
#'Type))
|
||||||
|
|
||||||
|
(check-true
|
||||||
|
(bound-identifier=?
|
||||||
|
(syntax-property (cadr (syntax-e d)) ':)
|
||||||
|
#'Int))
|
||||||
|
|
||||||
|
(check-equal?
|
||||||
|
(syntax-position term)
|
||||||
|
(syntax-position d))
|
||||||
|
|
||||||
|
(check-equal?
|
||||||
|
(syntax-position (syntax-property (cadr (syntax-e term)) ':))
|
||||||
|
(syntax-position (syntax-property (cadr (syntax-e d)) ':)))
|
||||||
|
|
||||||
|
(check-equal?
|
||||||
|
(syntax-position (car (syntax-e term)))
|
||||||
|
(syntax-position (car (syntax-e d))))
|
||||||
|
|
||||||
|
; syntax in datum in properties
|
||||||
|
(check-true
|
||||||
|
(bound-identifier=?
|
||||||
|
(car (syntax-property (syntax-property (cadr (syntax-e d)) ':) 'orig))
|
||||||
|
#'Int))
|
||||||
|
)
|
||||||
|
|
||||||
|
|
||||||
|
;; ----------------------------------------------------------------
|
||||||
|
|
||||||
|
;; syntax-map and datum-map copied from the expander files
|
||||||
|
;; syntax/datum-map.rkt
|
||||||
|
;; syntax/syntax.rkt
|
||||||
|
|
||||||
|
(require racket/fixnum racket/prefab)
|
||||||
|
|
||||||
|
;; `(datum-map v f)` walks over `v`, traversing objects that
|
||||||
|
;; `datum->syntax` traverses to convert content to syntax objects.
|
||||||
|
;;
|
||||||
|
;; `(f tail? d)` is called on each datum `d`, where `tail?`
|
||||||
|
;; indicates that the value is a pair/null in a `cdr` --- so that it
|
||||||
|
;; doesn't need to be wrapped for `datum->syntax`, for example;
|
||||||
|
;; the `tail?` argument is actually #f or a fixnum for a lower bound
|
||||||
|
;; on `cdr`s that have been taken
|
||||||
|
;;
|
||||||
|
;; `gf` is like `f`, but `gf` is used when the argument might be
|
||||||
|
;; syntax; if `gf` is provided, `f` can assume that its argument
|
||||||
|
;; is not syntax
|
||||||
|
;;
|
||||||
|
;; If a `seen` argument is provided, then it should be an `eq?`-based
|
||||||
|
;; hash table, and cycle checking is enabled; when a cycle is
|
||||||
|
;; discovered, the procedure attached to 'cycle-fail in the initial
|
||||||
|
;; table is called
|
||||||
|
;;
|
||||||
|
;; If a `known-pairs` argument is provided, then it should be an
|
||||||
|
;; `eq?`-based hash table to map pairs that can be returned as-is
|
||||||
|
;; in a `tail?` position
|
||||||
|
|
||||||
|
;; The inline version uses `f` only in an application position to
|
||||||
|
;; help avoid allocating a closure. It also covers only the most common
|
||||||
|
;; cases, defering to the general (not inlined) function for other cases.
|
||||||
|
(define (datum-map s f [gf f] [seen #f] [known-pairs #f])
|
||||||
|
(let loop ([tail? #f] [s s] [prev-depth 0])
|
||||||
|
(define depth (fx+ 1 prev-depth)) ; avoid cycle-checking overhead for shallow cases
|
||||||
|
(cond
|
||||||
|
[(and seen (depth . fx> . 32))
|
||||||
|
(datum-map-slow tail? s (lambda (tail? s) (gf tail? s)) seen known-pairs)]
|
||||||
|
[(null? s) (f tail? s)]
|
||||||
|
[(pair? s)
|
||||||
|
(f tail? (cons (loop #f (car s) depth)
|
||||||
|
(loop 1 (cdr s) depth)))]
|
||||||
|
[(symbol? s) (f #f s)]
|
||||||
|
[(boolean? s) (f #f s)]
|
||||||
|
[(number? s) (f #f s)]
|
||||||
|
[(or (vector? s) (box? s) (prefab-struct-key s) (hash? s))
|
||||||
|
(datum-map-slow tail? s (lambda (tail? s) (gf tail? s)) seen known-pairs)]
|
||||||
|
[else (gf #f s)])))
|
||||||
|
|
||||||
|
(define (datum-map-slow tail? s f seen known-pairs)
|
||||||
|
(let loop ([tail? tail?] [s s] [prev-seen seen])
|
||||||
|
(define seen
|
||||||
|
(cond
|
||||||
|
[(and prev-seen (datum-has-elements? s))
|
||||||
|
(cond
|
||||||
|
[(hash-ref prev-seen s #f)
|
||||||
|
((hash-ref prev-seen 'cycle-fail) s)]
|
||||||
|
[else (hash-set prev-seen s #t)])]
|
||||||
|
[else prev-seen]))
|
||||||
|
(cond
|
||||||
|
[(null? s) (f tail? s)]
|
||||||
|
[(pair? s)
|
||||||
|
(cond
|
||||||
|
[(and known-pairs
|
||||||
|
tail?
|
||||||
|
(hash-ref known-pairs s #f))
|
||||||
|
s]
|
||||||
|
[else
|
||||||
|
(f tail? (cons (loop #f (car s) seen)
|
||||||
|
(loop (if tail? (fx+ 1 tail?) 1) (cdr s) seen)))])]
|
||||||
|
[(or (symbol? s) (boolean? s) (number? s))
|
||||||
|
(f #f s)]
|
||||||
|
[(vector? s)
|
||||||
|
(f #f (vector->immutable-vector
|
||||||
|
(for/vector #:length (vector-length s) ([e (in-vector s)])
|
||||||
|
(loop #f e seen))))]
|
||||||
|
[(box? s)
|
||||||
|
(f #f (box-immutable (loop #f (unbox s) seen)))]
|
||||||
|
[(immutable-prefab-struct-key s)
|
||||||
|
=> (lambda (key)
|
||||||
|
(f #f
|
||||||
|
(apply make-prefab-struct
|
||||||
|
key
|
||||||
|
(for/list ([e (in-vector (struct->vector s) 1)])
|
||||||
|
(loop #f e seen)))))]
|
||||||
|
[(and (hash? s) (immutable? s))
|
||||||
|
(cond
|
||||||
|
[(hash-eq? s)
|
||||||
|
(f #f
|
||||||
|
(for/hasheq ([(k v) (in-hash s)])
|
||||||
|
(values k (loop #f v seen))))]
|
||||||
|
[(hash-eqv? s)
|
||||||
|
(f #f
|
||||||
|
(for/hasheqv ([(k v) (in-hash s)])
|
||||||
|
(values k (loop #f v seen))))]
|
||||||
|
[else
|
||||||
|
(f #f
|
||||||
|
(for/hash ([(k v) (in-hash s)])
|
||||||
|
(values k (loop #f v seen))))])]
|
||||||
|
[else (f #f s)])))
|
||||||
|
|
||||||
|
(define (datum-has-elements? d)
|
||||||
|
(or (pair? d)
|
||||||
|
(vector? d)
|
||||||
|
(box? d)
|
||||||
|
(immutable-prefab-struct-key d)
|
||||||
|
(and (hash? d) (immutable? d) (positive? (hash-count d)))))
|
||||||
|
|
||||||
|
;; `(syntax-map s f d->s)` walks over `s`:
|
||||||
|
;;
|
||||||
|
;; * `(f tail? d)` is called to each datum `d`, where `tail?`
|
||||||
|
;; indicates that the value is a pair/null in a `cdr` --- so that it
|
||||||
|
;; doesn't need to be wrapped for `datum->syntax`, for example
|
||||||
|
;;
|
||||||
|
;; * `(d->s orig-s d)` is called for each syntax object,
|
||||||
|
;; and the second argument is result of traversing its datum
|
||||||
|
;;
|
||||||
|
;; * the `s-e` function extracts content of a syntax object
|
||||||
|
;;
|
||||||
|
;; The optional `seen` argument is an `eq?`-based immutable hash table
|
||||||
|
;; to detect and reject cycles. See `datum-map`.
|
||||||
|
|
||||||
|
(define (syntax-map s f d->s s-e [seen #f])
|
||||||
|
(let loop ([s s])
|
||||||
|
(datum-map s
|
||||||
|
f
|
||||||
|
(lambda (tail? v)
|
||||||
|
(cond
|
||||||
|
[(syntax? v) (d->s v (loop (s-e v)))]
|
||||||
|
[else (f tail? v)]))
|
||||||
|
seen)))
|
|
@ -0,0 +1,163 @@
|
||||||
|
#lang typed/syndicate/roles
|
||||||
|
|
||||||
|
#;(require "core-types.rkt")
|
||||||
|
#;(require "core-expressions.rkt")
|
||||||
|
#;(require "prim.rkt")
|
||||||
|
#;(require "for-loops.rkt")
|
||||||
|
#;(require "list.rkt")
|
||||||
|
#;(require "roles.rkt")
|
||||||
|
#;(require "maybe.rkt")
|
||||||
|
|
||||||
|
#;(require macro-debugger/stepper)
|
||||||
|
|
||||||
|
;; (define-type-alias ID Symbol)
|
||||||
|
;; (require-struct task #:as Task #:from "examples/roles/flink-support.rkt")
|
||||||
|
;; (require-struct map-work #:as MapWork #:from "examples/roles/flink-support.rkt")
|
||||||
|
;; (require-struct reduce-work #:as ReduceWork #:from "examples/roles/flink-support.rkt")
|
||||||
|
;; (define-type-alias TaskID (Tuple Int ID))
|
||||||
|
;; (define-type-alias WordCount (Hash String Int))
|
||||||
|
;; (define-type-alias TaskResult WordCount)
|
||||||
|
;; (define-type-alias Reduce
|
||||||
|
;; (ReduceWork (Either Int TaskResult)
|
||||||
|
;; (Either Int TaskResult)))
|
||||||
|
;; (define-type-alias Work
|
||||||
|
;; (U Reduce (MapWork String)))
|
||||||
|
;; (define-type-alias ConcreteWork
|
||||||
|
;; (U (ReduceWork TaskResult TaskResult)
|
||||||
|
;; (MapWork String)))
|
||||||
|
;; (define-type-alias PendingTask
|
||||||
|
;; (Task TaskID Work))
|
||||||
|
;; (define-type-alias ConcreteTask
|
||||||
|
;; (Task TaskID ConcreteWork))
|
||||||
|
|
||||||
|
#;(define (task-ready? [t : PendingTask] -> (Maybe ConcreteTask))
|
||||||
|
(match t
|
||||||
|
#;[(tuple $tid)
|
||||||
|
;; having to re-produce this is directly bc of no occurrence typing
|
||||||
|
(some (task tid (map-work s)))]
|
||||||
|
#;[(task $tid (reduce-work (right $v1)
|
||||||
|
(right $v2)))
|
||||||
|
(some (task tid (reduce-work v1 v2)))]
|
||||||
|
[_
|
||||||
|
none]))
|
||||||
|
|
||||||
|
#;(cons (lambda () 0) (ann (list) (List (→fn Int))))
|
||||||
|
|
||||||
|
#;(Λ (X) (lambda ([x (Maybe X)]) (match x [none #f])))
|
||||||
|
#;(lambda ([x Int]) (match x [none #f]))
|
||||||
|
#;(match 1 [none #f])
|
||||||
|
#;(if #t 1 none)
|
||||||
|
#;none
|
||||||
|
|
||||||
|
#;(define (∀ (X) (unwrap! [x : (Maybe X)] -> Bool))
|
||||||
|
#;(error "")
|
||||||
|
(match x
|
||||||
|
#;[(some (bind v X))
|
||||||
|
v]
|
||||||
|
[none
|
||||||
|
#f
|
||||||
|
#;(error "none")]))
|
||||||
|
|
||||||
|
#;(lambda ([tasks : (List (Maybe Int))])
|
||||||
|
(define part (inst partition/either (Maybe Int) Int Int))
|
||||||
|
(part tasks
|
||||||
|
(lambda ([t : (Maybe Int)])
|
||||||
|
(left 0)
|
||||||
|
#;(match t
|
||||||
|
[(some $ct)
|
||||||
|
(right ct)]
|
||||||
|
[none
|
||||||
|
(left 0)]))))
|
||||||
|
|
||||||
|
#;(define (debug [tasks : (List Int)] -> (Tuple (List String) (List Int)))
|
||||||
|
(define part (inst partition/either Int String Int))
|
||||||
|
(part tasks
|
||||||
|
(lambda ([t : Int])
|
||||||
|
(left "hi"))))
|
||||||
|
|
||||||
|
(define (partition-ready-tasks [tasks : (List Int)]
|
||||||
|
-> (Tuple (List Int)
|
||||||
|
(List Int)))
|
||||||
|
(define part (inst partition/either Int Int Int))
|
||||||
|
(part tasks
|
||||||
|
(lambda ([t : Int])
|
||||||
|
(right 0)
|
||||||
|
#;(match (some 5)
|
||||||
|
[(some $ct)
|
||||||
|
(right ct)]
|
||||||
|
[none
|
||||||
|
(left 0)]))))
|
||||||
|
|
||||||
|
|
||||||
|
#;(define id : (∀ (X) (→fn X (List X) (List X)))
|
||||||
|
(Λ (X) (lambda ([x X] [y (List X)]) (list x))))
|
||||||
|
|
||||||
|
#;(spawn (U)
|
||||||
|
(start-facet echo
|
||||||
|
(on (message (tuple 1 1))
|
||||||
|
#f)))
|
||||||
|
|
||||||
|
#;(for/fold ([acc Int 0])
|
||||||
|
([x (list 1)])
|
||||||
|
x)
|
||||||
|
|
||||||
|
#;(define-constructor* (left : Left v))
|
||||||
|
|
||||||
|
#;(define (f [x (Left Int)] -> Int)
|
||||||
|
(define y x)
|
||||||
|
(match y
|
||||||
|
[(left (bind z Int))
|
||||||
|
z]))
|
||||||
|
|
||||||
|
#;(#%app- expand/step #'(lambda ([x : Int])
|
||||||
|
(define y x)
|
||||||
|
y))
|
||||||
|
|
||||||
|
#;(lambda ([x : Int])
|
||||||
|
(define y x)
|
||||||
|
y)
|
||||||
|
#;(begin-for-syntax
|
||||||
|
(define t #'(Maybe Unit))
|
||||||
|
(define t- ((current-type-eval) t))
|
||||||
|
(values #;displayln ((current-type?) t-))
|
||||||
|
(define tt (syntax-parse (detach t- ':)
|
||||||
|
[(#%plain-app x) #'x]))
|
||||||
|
(pretty-print (syntax-debug-info tt)))
|
||||||
|
|
||||||
|
#;(begin-for-syntax
|
||||||
|
(define t #'PendingTask)
|
||||||
|
(define t- ((current-type-eval) t))
|
||||||
|
(displayln ((current-type?) t-))
|
||||||
|
)
|
||||||
|
|
||||||
|
#;(define t1 '(→ (Computation (Value ★/t)
|
||||||
|
(Endpoints)
|
||||||
|
(Roles (Branch (Effs (Realizes (TasksFinished- Symbol (Hash- String Int))))
|
||||||
|
(Effs (Branch (Effs (Realizes (TaskIsReady- Symbol (Task- (Tuple- Int Symbol) (U* (MapWork- String) (ReduceWork- (Hash- String Int) (Hash- String Int)))))))
|
||||||
|
(Effs)))))
|
||||||
|
(Spawns))
|
||||||
|
(Tuple- Int Symbol)
|
||||||
|
(Hash- String Int)))
|
||||||
|
|
||||||
|
#;(define t2 '(→ (Computation (Value ★/t)
|
||||||
|
(Endpoints)
|
||||||
|
(Roles (Branch (Effs (Realizes (TasksFinished- Symbol (Hash- String Int))))
|
||||||
|
(Effs (Branch (Effs (Realizes (TaskIsReady- Symbol (Task- (Tuple- Int Symbol) (U* (MapWork- String) (ReduceWork- (Hash- String Int) (Hash- String Int)))))))
|
||||||
|
(Effs)))))
|
||||||
|
(Spawns))
|
||||||
|
(Tuple- Int Symbol)
|
||||||
|
(Hash- String Int)))
|
||||||
|
|
||||||
|
#;(lambda ()
|
||||||
|
(role-strings
|
||||||
|
(start-facet x
|
||||||
|
(define (push-results)
|
||||||
|
(cond
|
||||||
|
[(zero? 0)
|
||||||
|
(start-facet done (assert #t))]
|
||||||
|
[else
|
||||||
|
#f]))
|
||||||
|
(define (∀ (ρ) (perform-task [k : (proc -> ★/t #:roles (ρ))]))
|
||||||
|
(start-facet perform
|
||||||
|
(on start (stop perform (k)))))
|
||||||
|
(on start (call/inst perform-task push-results)))))
|
Loading…
Reference in New Issue