more wip on TS
This commit is contained in:
Sam Caldwell
Sam Caldwell
parent
82e5c8504c
commit
b1c000e12e
|
|
@ -1,26 +1,27 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(require turnstile/rackunit-typechecking)
|
||||
(define-type-alias ds-type
|
||||
(U (Observe (Tuple String ★)) (Tuple String Int)))
|
||||
|
||||
#;(spawn
|
||||
(assert (list "hello")))
|
||||
(dataspace ds-type
|
||||
|
||||
#;(spawn
|
||||
(on (asserted (list "hello"))
|
||||
(printf "hello\n")))
|
||||
(spawn ds-type
|
||||
(facet _
|
||||
(fields [the-thing Int 0])
|
||||
(assert (tuple "the thing" (ref the-thing)))
|
||||
(on (asserted (tuple "set thing" (bind new-v Int)))
|
||||
(set! the-thing new-v))))
|
||||
|
||||
(check-type 1 : Int)
|
||||
(spawn ds-type
|
||||
(let [k (λ [10 (begin)]
|
||||
[(bind x Int)
|
||||
(facet _ (fields)
|
||||
(assert (tuple "set thing" (+ x 1))))])]
|
||||
(facet _ (fields)
|
||||
(on (asserted (tuple "the thing" (bind x Int)))
|
||||
(k x)))))
|
||||
|
||||
(check-type (let-field x : Int 5 nil) : ⊥)
|
||||
(check-type (let-field x : Int 5 nil) :2 ⊥)
|
||||
(check-type (let-field x : Int 5 nil) :3 ⊥)
|
||||
|
||||
(check-type (tuple 1 2 3) : (Tuple Int Int Int))
|
||||
|
||||
(typecheck-fail (let-field x : Int 5
|
||||
(let-field y : (Field Int) x nil))
|
||||
#:with-msg "Keep your functions out of fields")
|
||||
|
||||
(check-type (tuple discard 1 (bind x Int)) : (Tuple Discard Int (Bind Int)))
|
||||
|
||||
(check-type (λ [(bind x Int) nil]) : (Case [→ (Bind Int) (Facet ⊥ ⊥ ⊥)]))
|
||||
(spawn ds-type
|
||||
(facet _ (fields)
|
||||
(on (asserted (tuple "the thing" (bind t Int)))
|
||||
(displayln t)))))
|
||||
|
|
@ -0,0 +1,49 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(define-type-alias ds-type
|
||||
(U (Tuple String Int)
|
||||
(Observe (Tuple String ★))
|
||||
(Observe (Observe (Tuple String ★)))))
|
||||
|
||||
(dataspace ds-type
|
||||
|
||||
(spawn ds-type
|
||||
(facet _
|
||||
(fields [balance Int 0])
|
||||
(assert (tuple "balance" (ref balance)))
|
||||
(on (asserted (tuple "deposit" (bind amount Int)))
|
||||
(set! balance (+ (ref balance) amount)))))
|
||||
|
||||
(spawn ds-type
|
||||
(facet _
|
||||
(fields)
|
||||
(on (asserted (tuple "balance" (bind amount Int)))
|
||||
(displayln amount))))
|
||||
|
||||
(spawn ds-type
|
||||
(facet _
|
||||
(fields)
|
||||
(on (asserted (observe (tuple "deposit" discard)))
|
||||
(facet _
|
||||
(fields)
|
||||
(assert (tuple "deposit" 100))
|
||||
(assert (tuple "deposit" -30)))))))
|
||||
|
||||
#|
|
||||
;; Hello-worldish "bank account" example.
|
||||
|
||||
(struct account (balance) #:prefab)
|
||||
(struct deposit (amount) #:prefab)
|
||||
|
||||
(spawn (field [balance 0])
|
||||
(assert (account (balance)))
|
||||
(on (message (deposit $amount))
|
||||
(balance (+ (balance) amount))))
|
||||
|
||||
(spawn (on (asserted (account $balance))
|
||||
(printf "Balance changed to ~a\n" balance)))
|
||||
|
||||
(spawn* (until (asserted (observe (deposit _))))
|
||||
(send! (deposit +100))
|
||||
(send! (deposit -30)))
|
||||
|#
|
||||
|
|
@ -0,0 +1,103 @@
|
|||
#lang typed/syndicate
|
||||
|
||||
(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))
|
||||
;; splits
|
||||
(Tuple String String Int Int Bool)
|
||||
(Observe (Tuple String String Int Int ★))
|
||||
(Observe (Observe (Tuple String ★ ★ ★ ★)))
|
||||
;; 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)))))
|
||||
|
||||
(dataspace ds-type
|
||||
|
||||
;; seller
|
||||
(spawn ds-type
|
||||
(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)))
|
||||
(facet x
|
||||
(fields)
|
||||
(on (retracted (observe (tuple "book-quote" title discard)))
|
||||
(stop x (begin)))
|
||||
(match title
|
||||
["Catch 22"
|
||||
(assert (tuple "book-quote" title 22))]
|
||||
[discard
|
||||
(assert (tuple "out-of-stock" title))])))
|
||||
(on (asserted (observe (tuple (tuple "order" (bind title String) (bind offer Int) discard discard))))
|
||||
(facet x
|
||||
(fields)
|
||||
(on (retracted (observe (tuple (tuple "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)))))))))
|
||||
|
||||
;; 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))))))))))
|
||||
|
||||
;; 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)))
|
||||
(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)))
|
||||
(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)))
|
||||
(stop accept (begin)))
|
||||
(on start
|
||||
(spawn ds-type
|
||||
(facet order
|
||||
(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))))))))])))))
|
||||
)
|
||||
|
|
@ -1,41 +1,115 @@
|
|||
#lang turnstile
|
||||
|
||||
(provide #%module-begin
|
||||
#%app
|
||||
(provide (rename-out [syndicate:#%module-begin #%module-begin])
|
||||
(rename-out [typed-app #%app])
|
||||
(rename-out [syndicate:begin-for-declarations declare-types])
|
||||
#%top-interaction
|
||||
require
|
||||
Int
|
||||
let-field
|
||||
#%top
|
||||
require only-in
|
||||
;; Types
|
||||
Int Bool String Tuple Bind Discard Case → Behavior FacetName Field ★
|
||||
Observe Inbound Outbound Actor U
|
||||
;; Statements
|
||||
let spawn dataspace facet set! begin stop unsafe-do
|
||||
;; endpoints
|
||||
assert on
|
||||
;; expressions
|
||||
tuple λ ref observe inbound outbound
|
||||
;; values
|
||||
#%datum
|
||||
Field
|
||||
⊥
|
||||
nil
|
||||
tuple Tuple
|
||||
bind Bind
|
||||
discard Discard
|
||||
+ -
|
||||
λ Case →
|
||||
Facet)
|
||||
;; patterns
|
||||
bind discard
|
||||
;; primitives
|
||||
+ - * / and or not > < >= <= = equal? displayln
|
||||
;; DEBUG and utilities
|
||||
define-type-alias
|
||||
print-type
|
||||
(rename-out [printf- printf])
|
||||
;; Extensions
|
||||
match if cond
|
||||
)
|
||||
|
||||
;(require syndicate/actor-lang)
|
||||
#;(provide (all-from-out syndicate/actor-lang))
|
||||
(require (rename-in racket/match [match-lambda match-lambda-]))
|
||||
(require (rename-in racket/math [exact-truncate exact-truncate-]))
|
||||
(require (prefix-in syndicate: syndicate/actor-lang))
|
||||
|
||||
(define-base-types Int Bool String ⊥ Discard)
|
||||
(module+ test
|
||||
(require rackunit)
|
||||
(require turnstile/rackunit-typechecking))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Types
|
||||
|
||||
(define-base-types Int Bool String Discard ★ FacetName)
|
||||
(define-type-constructor Field #:arity = 1)
|
||||
(define-type-constructor Facet #:arity = 3)
|
||||
;; (Behavior τv τi τo τa)
|
||||
;; τv is the type of thing it evaluates to
|
||||
;; τi is the type of patterns used to consume incoming assertions
|
||||
;; τo is the type of assertions made
|
||||
;; τa is the type of spawned actors
|
||||
(define-type-constructor Behavior #:arity = 4)
|
||||
(define-type-constructor Bind #:arity = 1)
|
||||
(define-type-constructor Tuple #:arity >= 0)
|
||||
(define-type-constructor U #:arity >= 0)
|
||||
(define-type-constructor Case #:arity >= 0)
|
||||
(define-type-constructor → #:arity > 0)
|
||||
(define-type-constructor Observe #:arity = 1)
|
||||
(define-type-constructor Inbound #:arity = 1)
|
||||
(define-type-constructor Outbound #:arity = 1)
|
||||
(define-type-constructor Actor #:arity = 1)
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Syntax
|
||||
|
||||
(begin-for-syntax
|
||||
|
||||
#|
|
||||
it's expensive and inflexible to fully parse these, but this is what the language
|
||||
is meant to be
|
||||
(define-syntax-class stmt
|
||||
#:datum-literals (:
|
||||
begin
|
||||
let
|
||||
set!
|
||||
spawn
|
||||
dataspace
|
||||
stop
|
||||
facet
|
||||
unsafe-do
|
||||
fields)
|
||||
(pattern (~or (begin seq:stmt ...)
|
||||
(e1:exp e2:exp)
|
||||
(let [f:id e:exp] let-fun-body:stmt)
|
||||
(set! x:id e:exp)
|
||||
(spawn τ:type s:stmt)
|
||||
(dataspace τ:type nested:stmt ...)
|
||||
(stop x:id s:stmt)
|
||||
(facet x:id (fields [fn:id τf:type ef:exp] ...) ep:endpoint ...+)
|
||||
;; note racket expr, not exp
|
||||
(unsafe-do rkt:expr ...))))
|
||||
|
||||
(define-syntax-class exp
|
||||
#:datum-literals (tuple λ)
|
||||
(pattern (~or (o:prim-op e:exp ...)
|
||||
#:datum-literals (tuple λ ref)
|
||||
(pattern (~or (o:prim-op es:exp ...)
|
||||
basic-val
|
||||
(tuple e:exp ...)
|
||||
(k:kons1 e:exp)
|
||||
(tuple es:exp ...)
|
||||
(ref x:id)
|
||||
(λ [p:pat s:stmt] ...))))
|
||||
|#
|
||||
|
||||
;; constructors with arity one
|
||||
(define-syntax-class kons1
|
||||
(pattern (~or (~datum observe)
|
||||
(~datum inbound)
|
||||
(~datum outbound))))
|
||||
|
||||
(define (kons1->constructor stx)
|
||||
(syntax-parse stx
|
||||
#:datum-literals (observe inbound outbound)
|
||||
[observe #'syndicate:observe]
|
||||
[inbound #'syndicate:inbound]
|
||||
[outbound #'syndicate:outbound]))
|
||||
|
||||
(define-syntax-class basic-val
|
||||
(pattern (~or boolean
|
||||
|
|
@ -44,33 +118,13 @@
|
|||
|
||||
(define-syntax-class prim-op
|
||||
(pattern (~or (~literal +)
|
||||
(~literal -))))
|
||||
|
||||
(define-syntax-class stmt
|
||||
#:datum-literals (:
|
||||
begin
|
||||
let-field
|
||||
let-function
|
||||
set!
|
||||
spawn
|
||||
dataspace
|
||||
stop
|
||||
facet)
|
||||
(pattern (~or (begin seq:stmt ...)
|
||||
(e1:exp e2:exp)
|
||||
nil ;; TODO - remove, only for making some initial examples
|
||||
(let-field [x:id : τ:type e:exp] lf-body:stmt)
|
||||
(let-function [f:id : τ:type e:exp] let-fun-body:stmt)
|
||||
(set! x:id e:exp)
|
||||
(spawn τ:type s:stmt)
|
||||
(dataspace τ:type nested:stmt ...)
|
||||
(stop x:id s:stmt)
|
||||
(facet x:id ep:endpoint ...))))
|
||||
(~literal -)
|
||||
(~literal displayln))))
|
||||
|
||||
(define-syntax-class endpoint
|
||||
#:datum-literals (on start stop)
|
||||
(pattern (~or (on ed:event-desc s:stmt)
|
||||
(assert e:exp))))
|
||||
(pattern (~or (on ed:event-desc s)
|
||||
(assert e:expr))))
|
||||
|
||||
(define-syntax-class event-desc
|
||||
#:datum-literals (start stop asserted retracted)
|
||||
|
|
@ -80,69 +134,484 @@
|
|||
(retracted p:pat))))
|
||||
|
||||
(define-syntax-class pat
|
||||
#:datum-literals (tuple _ discard)
|
||||
(pattern (~or (tuple p:pat ...)
|
||||
($ x:id : τ:type)
|
||||
discard
|
||||
x:id
|
||||
e:exp))))
|
||||
#:datum-literals (tuple _ discard bind)
|
||||
#:attributes (syndicate-pattern match-pattern)
|
||||
(pattern (~or (~and (tuple ps:pat ...)
|
||||
(~bind [syndicate-pattern #'(list 'tuple ps.syndicate-pattern ...)]
|
||||
[match-pattern #'(list 'tuple ps.match-pattern ...)]))
|
||||
(~and (k:kons1 p:pat)
|
||||
(~bind [syndicate-pattern #`(#,(kons1->constructor #'k) p.syndicate-pattern)]
|
||||
[match-pattern #`(#,(kons1->constructor #'k) p.match-pattern)]))
|
||||
(~and (bind ~! x:id τ:type)
|
||||
(~bind [syndicate-pattern #'($ x)]
|
||||
[match-pattern #'x]))
|
||||
(~and discard
|
||||
(~bind [syndicate-pattern #'_]
|
||||
[match-pattern #'_]))
|
||||
(~and x:id
|
||||
(~bind [syndicate-pattern #'x]
|
||||
[match-pattern #'(== x)]))
|
||||
(~and e:expr
|
||||
(~bind [syndicate-pattern #'e]
|
||||
[match-pattern #'(== e)]))))))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Subtyping
|
||||
|
||||
;; TODO: subtyping for facets
|
||||
|
||||
;; Type Type -> Bool
|
||||
(define-for-syntax (<: t1 t2)
|
||||
#;(printf "Checking ~a <: ~a\n" (type->str t1) (type->str t2))
|
||||
;; should add a check for type=?
|
||||
(syntax-parse #`(#,t1 #,t2)
|
||||
#;[(τ1 τ2) #:do [(displayln (type->str #'τ1))
|
||||
(displayln (type->str #'τ2))]
|
||||
#:when #f
|
||||
(error "")]
|
||||
[((~U τ1 ...) _)
|
||||
(stx-andmap (lambda (t) (<: t t2)) #'(τ1 ...))]
|
||||
[(_ (~U τ2:type ...))
|
||||
(stx-ormap (lambda (t) (<: t1 t)) #'(τ2 ...))]
|
||||
[((~Actor τ1:type) (~Actor τ2:type))
|
||||
;; should these be .norm? Is the invariant that inputs are always fully
|
||||
;; evalutated/expanded?
|
||||
(and (<: #'τ1 #'τ2)
|
||||
(<: (∩ (strip-? #'τ1) #'τ2) #'τ1))]
|
||||
[((~Tuple τ1:type ...) (~Tuple τ2:type ...))
|
||||
#:when (stx-length=? #'(τ1 ...) #'(τ2 ...))
|
||||
(stx-andmap <: #'(τ1 ...) #'(τ2 ...))]
|
||||
[(_ ~★)
|
||||
(flat-type? t1)]
|
||||
[((~Observe τ1:type) (~Observe τ2:type))
|
||||
(<: #'τ1 #'τ2)]
|
||||
[((~Inbound τ1:type) (~Inbound τ2:type))
|
||||
(<: #'τ1 #'τ2)]
|
||||
[((~Outbound τ1:type) (~Outbound τ2:type))
|
||||
(<: #'τ1 #'τ2)]
|
||||
[((~Behavior τ-v1 τ-i1 τ-o1 τ-a1) (~Behavior τ-v2 τ-i2 τ-o2 τ-a2))
|
||||
(and (<: #'τ-v1 #'τ-v2)
|
||||
;; HMMMMMM. i2 and i1 are types of patterns. TODO
|
||||
;; Want: ∀σ. project-safe(σ, τ-i2) ⇒ project-safe(σ, τ-i1)
|
||||
(<: #'τ-i2 #'τ-i1)
|
||||
(<: #'τ-o1 #'τ-o2)
|
||||
(<: (type-eval #'(Actor τ-a1)) (type-eval #'(Actor τ-a2))))]
|
||||
[((~→ τ-in1 ... τ-out1) (~→ τ-in2 ... τ-out2))
|
||||
#:when (stx-length=? #'(τ-in1 ...) #'(τ-in2 ...))
|
||||
(and (stx-andmap <: #'(τ-in2 ...) #'(τ-in1 ...))
|
||||
(<: #'τ-out1 #'τ-out2))]
|
||||
[((~Field τ1) (~Field τ2))
|
||||
(and (<: #'τ1 #'τ2)
|
||||
(<: #'τ2 #'τ1))]
|
||||
[(~Discard _)
|
||||
#t]
|
||||
[((~Bind τ1) (~Bind τ2))
|
||||
(<: #'τ1 #'τ2)]
|
||||
;; should probably put this first.
|
||||
[_ (type=? t1 t2)]))
|
||||
|
||||
;; Flat-Type Flat-Type -> Type
|
||||
(define-for-syntax (∩ t1 t2)
|
||||
(unless (and (flat-type? t1) (flat-type? t2))
|
||||
(error '∩ "expected two flat-types"))
|
||||
(syntax-parse #`(#,t1 #,t2)
|
||||
[(_ ~★)
|
||||
t1]
|
||||
[(~★ _)
|
||||
t2]
|
||||
[(_ _)
|
||||
#:when (type=? t1 t2)
|
||||
t1]
|
||||
[((~U τ1:type ...) _)
|
||||
(type-eval #`(U #,@(stx-map (lambda (t) (∩ t t2)) #'(τ1 ...))))]
|
||||
[(_ (~U τ2:type ...))
|
||||
(type-eval #`(U #,@(stx-map (lambda (t) (∩ t1 t)) #'(τ2 ...))))]
|
||||
;; all of these fail-when/unless clauses are meant to cause this through to
|
||||
;; the last case and result in ⊥.
|
||||
;; Also, using <: is OK, even though <: refers to ∩, because <:'s use of ∩ is only
|
||||
;; in the Actor case.
|
||||
[((~Tuple τ1:type ...) (~Tuple τ2:type ...))
|
||||
#:fail-unless (stx-length=? #'(τ1 ...) #'(τ2 ...)) #f
|
||||
#:with (τ ...) (stx-map ∩ #'(τ1 ...) #'(τ2 ...))
|
||||
;; 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 τ ...))]
|
||||
;; these three are just the same :(
|
||||
[((~Observe τ1:type) (~Observe τ2:type))
|
||||
#:with τ (∩ #'τ1 #'τ2)
|
||||
#:fail-when (<: #'τ (type-eval #'(U))) #f
|
||||
(type-eval #'(Observe τ))]
|
||||
[((~Inbound τ1:type) (~Inbound τ2:type))
|
||||
#:with τ (∩ #'τ1 #'τ2)
|
||||
#:fail-when (<: #'τ (type-eval #'(U))) #f
|
||||
(type-eval #'(Inbound τ))]
|
||||
[((~Outbound τ1:type) (~Outbound τ2:type))
|
||||
#:with τ (∩ #'τ1 #'τ2)
|
||||
#:fail-when (<: #'τ (type-eval #'(U))) #f
|
||||
(type-eval #'(Outbound τ))]
|
||||
[_ (type-eval #'(U))]))
|
||||
|
||||
;; Type Type -> Bool
|
||||
;; first type is the contents of the set
|
||||
;; second type is the type of a pattern
|
||||
(define-for-syntax (project-safe? t1 t2)
|
||||
(syntax-parse #`(#,t1 #,t2)
|
||||
[(_ (~Bind τ2:type))
|
||||
(and (finite? t1) (<: t1 #'τ2))]
|
||||
[(_ ~Discard)
|
||||
#t]
|
||||
[((~U τ1:type ...) _)
|
||||
(stx-andmap (lambda (t) (project-safe? t t2)) #'(τ1 ...))]
|
||||
[(_ (~U τ2:type ...))
|
||||
(stx-andmap (lambda (t) (project-safe? t1 t)) #'(τ2 ...))]
|
||||
[((~Tuple τ1:type ...) (~Tuple τ2:type ...))
|
||||
#:when (overlap? t1 t2)
|
||||
(stx-andmap project-safe? #'(τ1 ...) #'(τ2 ...))]
|
||||
[((~Observe τ1:type) (~Observe τ2:type))
|
||||
(project-safe? #'τ1 #'τ2)]
|
||||
[((~Inbound τ1:type) (~Inbound τ2:type))
|
||||
(project-safe? #'τ1 #'τ2)]
|
||||
[((~Outbound τ1:type) (~Outbound τ2:type))
|
||||
(project-safe? #'τ1 #'τ2)]
|
||||
[_ #t]))
|
||||
|
||||
;; AssertionType PatternType -> Bool
|
||||
;; Is it possible for things of these two types to match each other?
|
||||
;; Flattish-Type = Flat-Types + ★, Bind, Discard (assertion and pattern types)
|
||||
(define-for-syntax (overlap? t1 t2)
|
||||
(syntax-parse #`(#,t1 #,t2)
|
||||
[(~★ _) #t]
|
||||
[(_ (~Bind _)) #t]
|
||||
[(_ ~Discard) #t]
|
||||
[((~U τ1:type ...) _)
|
||||
(stx-ormap (lambda (t) (overlap? t t2)) #'(τ1 ...))]
|
||||
[(_ (~U τ2:type ...))
|
||||
(stx-ormap (lambda (t) (overlap? t1 t)) #'(τ2 ...))]
|
||||
[((~Tuple τ1:type ...) (~Tuple τ2:type ...))
|
||||
(and (stx-length=? #'(τ1 ...) #'(τ2 ...))
|
||||
(stx-andmap overlap? #'(τ1 ...) #'(τ2 ...)))]
|
||||
[((~Observe τ1:type) (~Observe τ2:type))
|
||||
(overlap? #'τ1 #'τ2)]
|
||||
[((~Inbound τ1:type) (~Inbound τ2:type))
|
||||
(overlap? #'τ1 #'τ2)]
|
||||
[((~Outbound τ1:type) (~Outbound τ2:type))
|
||||
(overlap? #'τ1 #'τ2)]
|
||||
[_ (<: t1 t2)]))
|
||||
|
||||
|
||||
;; Flattish-Type -> Bool
|
||||
(define-for-syntax (finite? t)
|
||||
(syntax-parse t
|
||||
[~★ #f]
|
||||
[(~U τ:type ...)
|
||||
(stx-andmap finite? #'(τ ...))]
|
||||
[(~Tuple τ:type ...)
|
||||
(stx-andmap finite? #'(τ ...))]
|
||||
[(~Observe τ:type)
|
||||
(finite? #'τ)]
|
||||
[(~Inbound τ:type)
|
||||
(finite? #'τ)]
|
||||
[(~Outbound τ:type)
|
||||
(finite? #'τ)]
|
||||
[_ #t]))
|
||||
|
||||
;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
||||
;; MODIFYING GLOBAL TYPECHECKING STATE!!!!!
|
||||
;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
||||
|
||||
(begin-for-syntax
|
||||
(current-typecheck-relation <:))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Statements
|
||||
|
||||
(define-typed-syntax (let-field x:id (~datum :) τ:type e:expr body:expr) ≫
|
||||
[⊢ e ≫ e- (⇐ : τ.norm)]
|
||||
[[x ≫ x- : (Field τ)] ⊢ body ≫ body- (⇒ : τ-body) (⇒ :2 τ-body2) (⇒ :3 τ-body3)]
|
||||
#:fail-unless (flat-type? #'τ.norm) "Keep your functions out of fields"
|
||||
---------
|
||||
[⊢ (let- ([x- e-]) body-) (⇒ : τ-body) (⇒ :2 τ-body2) (⇒ :3 τ-body3)])
|
||||
;; CONVENTIONS
|
||||
;; The `:` key is for evaluated expressions
|
||||
;; The `:i` key is for input patterns
|
||||
;; The `:o` key is for output assertions
|
||||
;; The `:a` key is for spawned actors
|
||||
|
||||
(define-typed-syntax nil
|
||||
[_:id ≫
|
||||
---------------
|
||||
[⊢ (void-) (⇒ : ⊥) (⇒ :2 ⊥) (⇒ :3 ⊥)]])
|
||||
(define-typed-syntax (set! x:id e:expr) ≫
|
||||
[⊢ e ≫ e- (⇒ : τ)]
|
||||
[⊢ x ≫ x- (⇒ : (~Field τ-x:type))]
|
||||
#:fail-unless (<: #'τ #'τ-x) "Ill-typed field write"
|
||||
----------------------------------------------------
|
||||
[⊢ (x- e-) (⇒ : (U)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
|
||||
|
||||
(define-typed-syntax (stop facet-name:id cont) ≫
|
||||
[⊢ facet-name ≫ facet-name- (⇐ : FacetName)]
|
||||
[⊢ cont ≫ cont- (⇒ :i τ-i) (⇒ :o τ-o) (⇒ :a τ-a)]
|
||||
--------------------------------------------------
|
||||
[⊢ (syndicate:stop-facet facet-name- cont-) (⇒ : (U)) (⇒ :i τ-i) (⇒ :o τ-o) (⇒ :a τ-a)])
|
||||
|
||||
(define-typed-syntax (facet name:id ((~datum fields) [x:id τ:type e:expr] ...) ep ...+) ≫
|
||||
#:fail-unless (stx-andmap flat-type? #'(τ ...)) "keep your uppity data outa my fields"
|
||||
[⊢ e ≫ e- (⇐ : τ)] ...
|
||||
[[name ≫ name- : FacetName] [x ≫ x- : (Field τ)] ...
|
||||
⊢ [ep ≫ ep- (⇒ :i τ-i) (⇒ :o τ-o) (⇒ :a τ-a)] ...]
|
||||
--------------------------------------------------------------
|
||||
;; name NOT name- here because I get an error that way.
|
||||
;; Since name is just an identifier I think it's OK?
|
||||
[⊢ (syndicate:react (let- ([name- (syndicate:current-facet-id)])
|
||||
#,(make-fields #'(x- ...) #'(e- ...))
|
||||
#;(syndicate:field [x- e-] ...)
|
||||
ep- ...))
|
||||
(⇒ : (U)) (⇒ :i (U τ-i ...)) (⇒ :o (U τ-o ...)) (⇒ :a (U τ-a ...))])
|
||||
|
||||
(define-for-syntax (make-fields names inits)
|
||||
(syntax-parse #`(#,names #,inits)
|
||||
[((x:id ...) (e ...))
|
||||
#'(syndicate:field [x e] ...)]))
|
||||
|
||||
(define-typed-syntax (dataspace τ-c:type s ...) ≫
|
||||
;; #:do [(printf "τ-c: ~a\n" (type->str #'τ-c.norm))]
|
||||
#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
|
||||
[⊢ s ≫ s- (⇒ :i τ-i:type) (⇒ :o τ-o:type) (⇒ :a τ-s:type)] ...
|
||||
;; #:do [(printf "dataspace types: ~a\n" (stx-map type->str #'(τ-s.norm ...)))
|
||||
;; (printf "dataspace type: ~a\n" (type->str ((current-type-eval) #'(Actor τ-c.norm))))]
|
||||
#:fail-unless (stx-andmap (lambda (t) (<: (type-eval #`(Actor #,t))
|
||||
(type-eval #'(Actor τ-c.norm))))
|
||||
#'(τ-s.norm ...))
|
||||
"Not all actors conform to communication type"
|
||||
#:fail-unless (stx-andmap (lambda (t) (<: t (type-eval #'(U))))
|
||||
#'(τ-i.norm ...)) "dataspace init should only be a spawn"
|
||||
#:fail-unless (stx-andmap (lambda (t) (<: t (type-eval #'(U))))
|
||||
#'(τ-o.norm ...)) "dataspace init should only be a spawn"
|
||||
#:with τ-ds-i (strip-inbound #'τ-c.norm)
|
||||
#:with τ-ds-o (strip-outbound #'τ-c.norm)
|
||||
#:with τ-relay (relay-interests #'τ-c.norm)
|
||||
-----------------------------------------------------------------------------------
|
||||
[⊢ (syndicate:dataspace s- ...) (⇒ : (U)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U τ-ds-i τ-ds-o τ-relay))])
|
||||
|
||||
(define-for-syntax (strip-? t)
|
||||
(type-eval
|
||||
(syntax-parse t
|
||||
;; TODO: probably need to `normalize` the result
|
||||
[(~U τ ...) #`(U #,@(stx-map strip-? #'(τ ...)))]
|
||||
[~★ #'★]
|
||||
[(~Observe τ) #'τ]
|
||||
[_ #'(U)])))
|
||||
|
||||
(define-for-syntax (strip-inbound t)
|
||||
(type-eval
|
||||
(syntax-parse t
|
||||
;; TODO: probably need to `normalize` the result
|
||||
[(~U τ ...) #`(U #,@(stx-map strip-? #'(τ ...)))]
|
||||
[~★ #'★]
|
||||
[(~Inbound τ) #'τ]
|
||||
[_ #'(U)])))
|
||||
|
||||
(define-for-syntax (strip-outbound t)
|
||||
(type-eval
|
||||
(syntax-parse t
|
||||
;; TODO: probably need to `normalize` the result
|
||||
[(~U τ ...) #`(U #,@(stx-map strip-? #'(τ ...)))]
|
||||
[~★ #'★]
|
||||
[(~Outbound τ) #'τ]
|
||||
[_ #'(U)])))
|
||||
|
||||
(define-for-syntax (relay-interests t)
|
||||
(type-eval
|
||||
(syntax-parse t
|
||||
;; TODO: probably need to `normalize` the result
|
||||
[(~U τ ...) #`(U #,@(stx-map strip-? #'(τ ...)))]
|
||||
[~★ #'★]
|
||||
[(~Observe (~Inbound τ)) #'(Observe τ)]
|
||||
[_ #'(U)])))
|
||||
|
||||
(define-typed-syntax (spawn τ-c:type s) ≫
|
||||
#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
|
||||
[⊢ s ≫ s- (⇒ :i τ-i:type) (⇒ :o τ-o:type) (⇒ :a τ-a:type)]
|
||||
;; TODO: s shouldn't refer to facets or fields!
|
||||
#:fail-unless (<: #'τ-o.norm #'τ-c.norm)
|
||||
(format "Output ~a not valid in dataspace ~a" (type->str #'τ-o.norm) (type->str #'τ-c.norm))
|
||||
#:fail-unless (<: (type-eval #'(Actor τ-a.norm))
|
||||
(type-eval #'(Actor τ-c.norm))) "Spawned actors not valid in dataspace"
|
||||
#:fail-unless (project-safe? (∩ (strip-? #'τ-o.norm) #'τ-c.norm)
|
||||
#'τ-i.norm) "Not prepared to handle all inputs"
|
||||
;; #:do [(printf "spawning: ~v\n" #'s-)]
|
||||
--------------------------------------------------------------------------------------------
|
||||
[⊢ (syndicate:spawn (syndicate:on-start s-)) (⇒ : (U)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a τ-c)])
|
||||
|
||||
(define-typed-syntax (let [f:id e:expr] body:expr) ≫
|
||||
[⊢ e ≫ e- (⇒ : τ:type)]
|
||||
#:fail-unless (or (procedure-type? #'τ.norm) (flat-type? #'τ.norm))
|
||||
(format "let doesn't bind actions; got ~a" (type->str #'τ.norm))
|
||||
[[f ≫ f- : τ] ⊢ body ≫ body- (⇒ : τ-body) (⇒ :i τ-body-i) (⇒ :o τ-body-o) (⇒ :a τ-body-a)]
|
||||
------------------------------------------------------------------------
|
||||
[⊢ (let- ([f- e-]) body-) (⇒ : τ-body) (⇒ :i τ-body-i) (⇒ :o τ-body-o) (⇒ :a τ-body-a)])
|
||||
|
||||
(define-for-syntax (procedure-type? τ)
|
||||
(syntax-parse τ
|
||||
[(~→ τ ...+) #t]
|
||||
[_ #f]))
|
||||
|
||||
(define-typed-syntax (begin s ...) ≫
|
||||
[⊢ s ≫ s- (⇒ :i τ1) (⇒ :o τ2) (⇒ :a τ3)] ...
|
||||
------------------------------------------
|
||||
[⊢ (begin- (void-) s- ...) (⇒ : (U)) (⇒ :i (U τ1 ...)) (⇒ :o (U τ2 ...)) (⇒ :a (U τ3 ...))])
|
||||
|
||||
(define-for-syntax (flat-type? τ)
|
||||
(syntax-parse τ
|
||||
[(~→ _ ...) #f]
|
||||
[(~→ τ ...) #f]
|
||||
[(~Field _) #f]
|
||||
[(~Behavior _ _ _ _) #f]
|
||||
[_ #t]))
|
||||
|
||||
(define-typed-syntax (unsafe-do rkt:expr ...) ≫
|
||||
------------------------
|
||||
[⊢ (let- () rkt ...) (⇒ : (U)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Endpoints
|
||||
|
||||
(begin-for-syntax
|
||||
(define-syntax-class asserted-or-retracted
|
||||
#:datum-literals (asserted retracted)
|
||||
(pattern (~or (~and asserted
|
||||
(~bind [syndicate-kw #'syndicate:asserted]))
|
||||
(~and retracted
|
||||
(~bind [syndicate-kw #'syndicate:retracted]))))))
|
||||
|
||||
(define-typed-syntax on
|
||||
[(on (~literal start) s) ≫
|
||||
[⊢ s ≫ s- (⇒ :i τi) (⇒ :o τ-o) (⇒ :a τ-a)]
|
||||
-----------------------------------
|
||||
[⊢ (syndicate:on-start s-) (⇒ : (U)) (⇒ :i τi) (⇒ :o τ-o) (⇒ :a τ-a)]]
|
||||
[(on (~literal stop) s) ≫
|
||||
[⊢ 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) ≫
|
||||
[⊢ p ≫ _ (⇒ : τ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)
|
||||
(let- ([x- x] ...) s-))
|
||||
(⇒ : (U))
|
||||
(⇒ :i (U τi τp))
|
||||
(⇒ :o (U (Observe pat-sub) τ-o))
|
||||
(⇒ :a τ-a)]])
|
||||
|
||||
;; FlattishType -> FlattishType
|
||||
(define-for-syntax (replace-bind-and-discard-with-★ t)
|
||||
(syntax-parse t
|
||||
[(~Bind _)
|
||||
(type-eval #'★)]
|
||||
[~Discard
|
||||
(type-eval #'★)]
|
||||
[(~U τ ...)
|
||||
(type-eval #`(U #,@(stx-map replace-bind-and-discard-with-★ #'(τ ...))))]
|
||||
[(~Tuple τ ...)
|
||||
(type-eval #`(Tuple #,@(stx-map replace-bind-and-discard-with-★ #'(τ ...))))]
|
||||
[(~Observe τ)
|
||||
(type-eval #`(Observe #,(replace-bind-and-discard-with-★ #'τ)))]
|
||||
[(~Inbound τ)
|
||||
(type-eval #`(Inbound #,(replace-bind-and-discard-with-★ #'τ)))]
|
||||
[(~Outbound τ)
|
||||
(type-eval #`(Outbound #,(replace-bind-and-discard-with-★ #'τ)))]
|
||||
[_ t]))
|
||||
|
||||
(define-typed-syntax (assert e:expr) ≫
|
||||
[⊢ e ≫ e- (⇒ : τ)]
|
||||
#:with τ-in (strip-? #'τ.norm)
|
||||
-------------------------------------
|
||||
[⊢ (syndicate:assert e-) (⇒ : (U)) (⇒ :i τ-in) (⇒ :o τ) (⇒ :a (U))])
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Expressions
|
||||
|
||||
#;(define-syntax-class exp
|
||||
#:datum-literals (tuple λ)
|
||||
(pattern (~or (o:prim-op e:exp ...)
|
||||
basic-val
|
||||
(tuple e:exp ...)
|
||||
(λ [p:pat s:stmt] ...))))
|
||||
|
||||
(define-typed-syntax (tuple e:expr ...) ≫
|
||||
[⊢ e ≫ e- (⇒ : τ)] ...
|
||||
-----------------------
|
||||
[⊢ (list 'tuple e- ...) (⇒ : (Tuple τ ...))])
|
||||
[⊢ (list 'tuple e- ...) (⇒ : (Tuple τ ...)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
|
||||
|
||||
(define-typed-syntax (λ [p:pat s:stmt] ...) ≫
|
||||
(define-typed-syntax (ref x:id) ≫
|
||||
[⊢ x ≫ x- ⇒ (~Field τ)]
|
||||
------------------------
|
||||
[⊢ (x-) (⇒ : τ) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
|
||||
|
||||
(define-typed-syntax (λ [p:pat s] ...) ≫
|
||||
#:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
|
||||
[[x ≫ x- : τ] ... ⊢ s ≫ s- (⇒ : τ1) (⇒ :2 τ2) (⇒ :3 τ3)] ...
|
||||
[[x ≫ x- : τ] ... ⊢ 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] ...
|
||||
#:with (τ-in ...) (stx-map lower-pattern-type #'(τ-p ...))
|
||||
--------------------------------------------------------------
|
||||
[⊢ (match-lambda- [p- s-] ...) ⇒ (Case [→ τ-p (Facet τ1 τ2 τ3)] ...)])
|
||||
;; TODO: add a catch-all error clause
|
||||
[⊢ (match-lambda- [p.match-pattern (let- ([x- x] ...) s-)] ...)
|
||||
(⇒ : (→ (U τ-p ...) (Behavior (U τv ...) (U τ1 ...) (U τ2 ...) (U τ3 ...))))
|
||||
(⇒ :i (U))
|
||||
(⇒ :o (U))
|
||||
(⇒ :a (U))])
|
||||
|
||||
;; FlattishType -> FlattishType
|
||||
;; replaces (Bind τ) with τ and Discard with ★
|
||||
(define-for-syntax (lower-pattern-type t)
|
||||
(syntax-parse t
|
||||
[(~Bind τ)
|
||||
#'τ]
|
||||
[~Discard
|
||||
(type-eval #'★)]
|
||||
[(~U τ ...)
|
||||
(type-eval #`(U #,@(stx-map lower-pattern-type #'(τ ...))))]
|
||||
[(~Tuple τ ...)
|
||||
(type-eval #`(Tuple #,@(stx-map lower-pattern-type #'(τ ...))))]
|
||||
[(~Observe τ)
|
||||
(type-eval #`(Observe #,(lower-pattern-type #'τ)))]
|
||||
[(~Inbound τ)
|
||||
(type-eval #`(Inbound #,(lower-pattern-type #'τ)))]
|
||||
[(~Outbound τ)
|
||||
(type-eval #`(Outbound #,(lower-pattern-type #'τ)))]
|
||||
[_ t]))
|
||||
|
||||
(define-typed-syntax (typed-app e_fn e_arg ...) ≫
|
||||
[⊢ e_fn ≫ e_fn- (⇒ : (~→ τ_in:type ... (~Behavior τ-v τ-i τ-o τ-a)))]
|
||||
#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
|
||||
(num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
|
||||
[⊢ e_arg ≫ e_arg- (⇒ : τ_arg:type)] ...
|
||||
;; #:do [(printf "~a\n" (stx-map type->str #'(τ_arg.norm ...)))
|
||||
;; (printf "~a\n" (stx-map type->str #'(τ_in.norm ...) #;(stx-map lower-pattern-type #'(τ_in.norm ...))))]
|
||||
#:fail-unless (stx-andmap <: #'(τ_arg.norm ...) (stx-map lower-pattern-type #'(τ_in.norm ...)))
|
||||
"argument mismatch"
|
||||
#:fail-unless (stx-andmap project-safe? #'(τ_arg.norm ...) #'(τ_in.norm ...))
|
||||
"match error"
|
||||
------------------------------------------------------------------------
|
||||
[⊢ (#%app- e_fn- e_arg- ...) (⇒ : τ-v) (⇒ :i τ-i) (⇒ :o τ-o) (⇒ :a τ-a)])
|
||||
|
||||
;; it would be nice to abstract over these three
|
||||
(define-typed-syntax (observe e:expr) ≫
|
||||
[⊢ e ≫ e- (⇒ : τ)]
|
||||
---------------------------------------------------------------------------
|
||||
[⊢ (syndicate:observe e-) (⇒ : (Observe τ)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
|
||||
|
||||
(define-typed-syntax (inbound e:expr) ≫
|
||||
[⊢ e ≫ e- ⇒ τ]
|
||||
---------------------------------------------------------------------------
|
||||
[⊢ (syndicate:inbound e-) (⇒ : (Inbound τ)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
|
||||
|
||||
(define-typed-syntax (outbound e:expr) ≫
|
||||
[⊢ e ≫ e- ⇒ τ]
|
||||
---------------------------------------------------------------------------
|
||||
[⊢ (syndicate:outbound e-) (⇒ : (Outbound τ)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Patterns
|
||||
|
||||
(define-typed-syntax (bind x:id τ:type) ≫
|
||||
--------------------
|
||||
----------------------------------------
|
||||
;; TODO: at some point put $ back in
|
||||
[⊢ (void-) ⇒ (Bind τ)])
|
||||
[⊢ (void-) (⇒ : (Bind τ)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
|
||||
|
||||
(define-typed-syntax discard
|
||||
[_ ≫
|
||||
--------------------
|
||||
;; TODO: change void to _
|
||||
[⊢ (void-) ⇒ Discard]])
|
||||
[⊢ (void-) (⇒ : Discard) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))]])
|
||||
|
||||
;; pat -> ([Id Type] ...)
|
||||
(define-for-syntax (pat-bindings stx)
|
||||
|
|
@ -153,6 +622,8 @@
|
|||
[(tuple p:pat ...)
|
||||
#:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
|
||||
#'([x τ] ... ...)]
|
||||
[(k:kons1 p:pat)
|
||||
(pat-bindings #'p)]
|
||||
[_:pat
|
||||
#'()]))
|
||||
|
||||
|
|
@ -160,8 +631,43 @@
|
|||
;; Primitives
|
||||
|
||||
;; hmmm
|
||||
(define-primop + (→ Int Int Int))
|
||||
(define-primop - (→ Int Int Int))
|
||||
(define-primop + (→ Int Int (Behavior Int (U) (U) (U))))
|
||||
(define-primop - (→ Int Int (Behavior Int (U) (U) (U))))
|
||||
(define-primop * (→ Int Int (Behavior Int (U) (U) (U))))
|
||||
#;(define-primop and (→ Bool Bool (Behavior Bool (U) (U) (U))))
|
||||
(define-primop or (→ Bool Bool (Behavior Bool (U) (U) (U))))
|
||||
(define-primop not (→ Bool (Behavior Bool (U) (U) (U))))
|
||||
(define-primop < (→ Int Int (Behavior Bool (U) (U) (U))))
|
||||
(define-primop > (→ Int Int (Behavior Bool (U) (U) (U))))
|
||||
(define-primop <= (→ Int Int (Behavior Bool (U) (U) (U))))
|
||||
(define-primop >= (→ Int Int (Behavior Bool (U) (U) (U))))
|
||||
(define-primop = (→ Int Int (Behavior Bool (U) (U) (U))))
|
||||
|
||||
(define-typed-syntax (/ e1 e2) ≫
|
||||
[⊢ e1 ≫ e1- (⇐ : Int)]
|
||||
[⊢ e2 ≫ e2- (⇐ : Int)]
|
||||
------------------------
|
||||
[⊢ (exact-truncate- (/- e1- e2-)) (⇒ : Int) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
|
||||
|
||||
;; for some reason defining `and` as a prim op doesn't work
|
||||
(define-typed-syntax (and e ...) ≫
|
||||
[⊢ e ≫ e- (⇐ : Bool)] ...
|
||||
------------------------
|
||||
[⊢ (and- e- ...) (⇒ : Bool) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
|
||||
|
||||
(define-typed-syntax (equal? e1:expr e2:expr) ≫
|
||||
[⊢ e1 ≫ e1- (⇒ : τ1:type)]
|
||||
#:fail-unless (flat-type? #'τ1.norm)
|
||||
(format "equality only available on flat data; got ~a" (type->str #'τ1))
|
||||
[⊢ e2 ≫ e2- (⇐ : τ1)]
|
||||
---------------------------------------------------------------------------
|
||||
[⊢ (equal?- e1- e2-) (⇒ : Bool) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
|
||||
|
||||
(define-typed-syntax (displayln e:expr) ≫
|
||||
[⊢ e ≫ e- ⇒ τ]
|
||||
---------------
|
||||
[⊢ (displayln- e-) (⇒ : (U)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
|
||||
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Basic Values
|
||||
|
|
@ -169,19 +675,114 @@
|
|||
(define-typed-syntax #%datum
|
||||
[(_ . n:integer) ≫
|
||||
----------------
|
||||
[⊢ (#%datum- . n) ⇒ Int]]
|
||||
[⊢ (#%datum- . n) (⇒ : Int) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))]]
|
||||
[(_ . b:boolean) ≫
|
||||
----------------
|
||||
[⊢ (#%datum- . b) ⇒ Bool]]
|
||||
[⊢ (#%datum- . b) (⇒ : Bool) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))]]
|
||||
[(_ . s:string) ≫
|
||||
----------------
|
||||
[⊢ (#%datum- . s) ⇒ String]])
|
||||
[⊢ (#%datum- . s) (⇒ : String) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))]])
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Utilities
|
||||
|
||||
#;(define-syntax (begin/void-default stx)
|
||||
(syntax-parse stx
|
||||
[(_)
|
||||
(syntax/loc stx (void))]
|
||||
[(_ expr0 expr ...)
|
||||
(syntax/loc stx (begin- expr0 expr ...))]))
|
||||
|
||||
;; x[A (D S) ...]
|
||||
(define-for-syntax (type-eval t)
|
||||
((current-type-eval) t))
|
||||
|
||||
#;(react x
|
||||
(assert A)
|
||||
(on D S)
|
||||
...)
|
||||
(define-typed-syntax (print-type e) ≫
|
||||
[⊢ e ≫ e- ⇒ τ]
|
||||
#:do [(displayln (type->str #'τ))]
|
||||
----------------------------------
|
||||
[⊢ 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
|
||||
|
||||
(define-syntax (match stx)
|
||||
(syntax-parse stx
|
||||
[(match e [pat body] ...+)
|
||||
(syntax/loc stx
|
||||
(typed-app (λ [pat body] ...) e))]))
|
||||
|
||||
(define-syntax (if stx)
|
||||
(syntax-parse stx
|
||||
[(if e1 e2 e3)
|
||||
(syntax/loc stx
|
||||
(typed-app (λ [#f e3] [discard e2]) e1))]))
|
||||
|
||||
(define-typed-syntax (cond [pred:expr s] ...+) ≫
|
||||
[⊢ pred ≫ pred- (⇐ : Bool)] ...
|
||||
[⊢ s ≫ s- (⇒ :i τ-i) (⇒ :o τ-o) (⇒ :a τ-a)] ...
|
||||
------------------------------------------------
|
||||
[⊢ (cond- [pred- s-] ...) (⇒ : (U)) (⇒ :i (U τ-i ...)) (⇒ :o (U τ-o ...)) (⇒ :a (U τ-a ...))])
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Tests
|
||||
|
||||
;; WANTED UNIT TESTS
|
||||
;; (check-true (<: #'(U String) #'String))
|
||||
;; (check-true (<: #'(U (U)) #'String))
|
||||
;; (check-true (<: #'(Actor (U (U))) #'(Actor String))
|
||||
;; (check-true (<: #'(Actor (U (U))) #'(Actor (U (Observe ★) String)))
|
||||
;; (check-true (<: ((current-type-eval) #'(U (U) (U))) ((current-type-eval) #'(U))))
|
||||
;; (check-false (<: ((current-type-eval) #'(Actor (U (Observe ★) String Int)))
|
||||
;; ((current-type-eval) #'(Actor (U (Observe ★) String)))))
|
||||
;; (check-true (<: (Actor (U (Observe ★) String)) (Actor (U (Observe ★) String)))
|
||||
|
||||
(module+ test
|
||||
(check-type 1 : Int)
|
||||
|
||||
(check-type (tuple 1 2 3) : (Tuple Int Int Int))
|
||||
|
||||
(check-type (tuple discard 1 (bind x Int)) : (Tuple Discard Int (Bind Int)))
|
||||
|
||||
#;(check-type (λ [(bind x Int) (begin)]) : (Case [→ (Bind Int) (Facet (U) (U) (U))]))
|
||||
#;(check-true (void? ((λ [(bind x Int) (begin)]) 1))))
|
||||
|
||||
(define-syntax (test-syntax-class stx)
|
||||
(syntax-parse stx
|
||||
[(_ e class:id)
|
||||
#`(let ()
|
||||
(define-syntax (test-result stx)
|
||||
(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)
|
||||
Loading…
Reference in New Issue