more docs and cleanup
This commit is contained in:
parent
aa74ffa14d
commit
4f6089c805
|
@ -1,8 +1,9 @@
|
||||||
#lang scribble/manual
|
#lang scribble/manual
|
||||||
|
|
||||||
@(require (for-label (only-in racket struct #;equal?)
|
@(require (for-label (only-in racket struct)
|
||||||
typed/syndicate/roles)
|
typed/syndicate/roles)
|
||||||
(prefix-in untyped: (for-label syndicate/actor)))
|
(prefix-in racket: (for-label racket))
|
||||||
|
(prefix-in untyped: (for-label syndicate/actor)))
|
||||||
|
|
||||||
@title{Typed Syndicate}
|
@title{Typed Syndicate}
|
||||||
|
|
||||||
|
@ -13,6 +14,14 @@
|
||||||
|
|
||||||
@section{Types}
|
@section{Types}
|
||||||
|
|
||||||
|
@deftogether[(@defidform[Int]
|
||||||
|
@defidform[Bool]
|
||||||
|
@defidform[String]
|
||||||
|
@defidform[ByteString]
|
||||||
|
@defidform[Symbol])]{
|
||||||
|
Base types.
|
||||||
|
}
|
||||||
|
|
||||||
@defform[(U type ...)]{
|
@defform[(U type ...)]{
|
||||||
The type representing the union of @racket[type ...].
|
The type representing the union of @racket[type ...].
|
||||||
}
|
}
|
||||||
|
@ -385,10 +394,205 @@ result of @racket[expr] each time any referenced field changes. When
|
||||||
|
|
||||||
@section{Expressions}
|
@section{Expressions}
|
||||||
|
|
||||||
|
@defform*[#:literals (:)
|
||||||
|
[(ann expr : type)
|
||||||
|
(ann expr type)]]{
|
||||||
|
Ensure that @racket[expr] has the given @racket[type].
|
||||||
|
}
|
||||||
|
|
||||||
|
@defform[(if test-expr then-expr else-expr)]{
|
||||||
|
The same as Racket's @racket[racket:if].
|
||||||
|
}
|
||||||
|
|
||||||
|
@deftogether[(@defform[(cond [test-expr body-expr ...+] ...+)]
|
||||||
|
@defthing[else Bool #:value #t])]{
|
||||||
|
Like Racket's @racket[racket:cond].
|
||||||
|
}
|
||||||
|
|
||||||
|
@defform[(when test-expr expr)]{
|
||||||
|
Like Racket's @racket[racket:when], but results in @racket[#f] when
|
||||||
|
@racket[test-expr] is @racket[#f].
|
||||||
|
}
|
||||||
|
|
||||||
|
@defform[(unless test-expr expr)]{
|
||||||
|
Like Racket's @racket[racket:unless], but results in @racket[#f] when
|
||||||
|
@racket[test-expr] is @racket[#f].
|
||||||
|
}
|
||||||
|
|
||||||
|
@defform[(let ([id expr] ...) body ...+)]{
|
||||||
|
The same as Racket's @racket[racket:let].
|
||||||
|
}
|
||||||
|
|
||||||
|
@defform[(let* ([id expr] ...) body ...+)]{
|
||||||
|
The same as Racket's @racket[racket:let*].
|
||||||
|
}
|
||||||
|
|
||||||
|
@defform[#:literals (:)
|
||||||
|
(lambda ([x opt-: type] ...) expr ...+)
|
||||||
|
#:grammar
|
||||||
|
[(opt-: (code:line)
|
||||||
|
(code:line :))]]{
|
||||||
|
Constructsa an anonymous function.
|
||||||
|
}
|
||||||
|
|
||||||
|
@defidform[λ]{Synonym for @racket[lambda].}
|
||||||
|
|
||||||
|
@defform[(Λ (X ...) expr)]{
|
||||||
|
Parametric abstraction over type variables @racket[X ...].
|
||||||
|
}
|
||||||
|
|
||||||
|
@defform[(inst expr type ...)]{
|
||||||
|
Instantiates the type variables @racket[X ...] with @racket[type ...], where
|
||||||
|
@racket[expr] has type @racket[(∀ (X ...) t)].
|
||||||
|
}
|
||||||
|
|
||||||
|
@defform*[#:literals (: → -> ∀)
|
||||||
|
[(define id : type expr)
|
||||||
|
(define id expr)
|
||||||
|
(define (id [arg-id opt-: arg-type] ... opt-res-ty) expr ...+)
|
||||||
|
(define (∀ (X ...) (id [arg-id opt-: arg-type] ... opt-res-ty)) expr ...+)]
|
||||||
|
#:grammar
|
||||||
|
[(opt-: (code:line) (code:line :))
|
||||||
|
(opt-res-ty (code:line)
|
||||||
|
(code:line arr res-type))
|
||||||
|
(arr (code:line →) (code:line ->))]]{
|
||||||
|
Define a constant or a (potentially polymorphic) function.
|
||||||
|
}
|
||||||
|
|
||||||
|
@defform[(define-tuple (id ...) expr)]{
|
||||||
|
Define @racket[id ...] to each of the slots of the tuple produced by
|
||||||
|
@racket[expr].
|
||||||
|
}
|
||||||
|
|
||||||
|
@defform[(match-define pattern expr)]{
|
||||||
|
Define the binders of @racket[pattern] to the matching values of @racket[expr].
|
||||||
|
}
|
||||||
|
|
||||||
|
@defform[(begin expr ...+)]{
|
||||||
|
Sequencing form whose value and type is that of the final @racket[expr].
|
||||||
|
}
|
||||||
|
|
||||||
|
@defform[(block expr ...+)]{
|
||||||
|
Like @racket[begin], but also introduces a definition context for its body.
|
||||||
|
}
|
||||||
|
|
||||||
|
@defform[(match expr [pattern body-expr ...+] ...+)]{
|
||||||
|
Like Racket's @racket[racket:match] but with the pattern syntax described by
|
||||||
|
@racket[on].
|
||||||
|
}
|
||||||
|
|
||||||
@defform[(tuple expr ...)]{
|
@defform[(tuple expr ...)]{
|
||||||
Constructs a tuple of arbitrary arity.
|
Constructs a tuple of arbitrary arity.
|
||||||
}
|
}
|
||||||
|
|
||||||
@section{Requiring From Outside Typed Syndicate}
|
@defform[(select i expr)]{
|
||||||
|
Extract the @racket[i]th element of a @racket[tuple].
|
||||||
|
}
|
||||||
|
|
||||||
|
@defform[(error format-expr arg-expr ...)]{
|
||||||
|
Raises an exception using @racket[format-expr] as a format string together with
|
||||||
|
@racket[arg-expr ...].
|
||||||
|
}
|
||||||
|
|
||||||
|
@defthing[unit Unit #:value (tuple)]
|
||||||
|
|
||||||
|
@deftogether[(
|
||||||
|
@defthing[+ (→fn Int Int Int)]
|
||||||
|
@defthing[- (→fn Int Int Int)]
|
||||||
|
@defthing[* (→fn Int Int Int)]
|
||||||
|
@defthing[< (→fn Int Int Bool)]
|
||||||
|
@defthing[> (→fn Int Int Bool)]
|
||||||
|
@defthing[<= (→fn Int Int Bool)]
|
||||||
|
@defthing[>= (→fn Int Int Bool)]
|
||||||
|
@defthing[= (→fn Int Int Bool)]
|
||||||
|
@defthing[even? (→fn Int Bool)]
|
||||||
|
@defthing[odd? (→fn Int Bool)]
|
||||||
|
@defthing[add1 (→fn Int Int)]
|
||||||
|
@defthing[sub1 (→fn Int Int)]
|
||||||
|
@defthing[max (→fn Int Int Int)]
|
||||||
|
@defthing[min (→fn Int Int Int)]
|
||||||
|
@defthing[zero? (→fn Int Bool)]
|
||||||
|
@defthing[positive? (→fn Int Bool)]
|
||||||
|
@defthing[negative? (→fn Int Bool)]
|
||||||
|
@defthing[current-inexact-milleseconds? (→fn Int)]
|
||||||
|
@defthing[string=? (→fn String String Bool)]
|
||||||
|
@defthing[bytes->string/utf-8 (→fn ByteString String)]
|
||||||
|
@defthing[string->bytes/utf-8 (→fn String ByteString)]
|
||||||
|
@defthing[gensym (→fn Symbol Symbol)]
|
||||||
|
@defthing[symbol->string (→fn Symbol String)]
|
||||||
|
@defthing[string->symbol (→fn String Symbol)]
|
||||||
|
@defthing[not (→fn Bool Bool)]
|
||||||
|
@defform[(/ e1 e2)]
|
||||||
|
@defform[(and e ...)]
|
||||||
|
@defform[(or e ...)]
|
||||||
|
@defform[(equal? e1 e2)]
|
||||||
|
@defform[(displayln e)]
|
||||||
|
@defform[(printf fmt-expr val-expr ...)]
|
||||||
|
@defform[(~a e ...)]
|
||||||
|
)]{
|
||||||
|
Primitive operations imported from Racket.
|
||||||
|
}
|
||||||
|
|
||||||
|
@section{Require & Provide}
|
||||||
|
|
||||||
|
@defform[(struct-out ctor-id)]{
|
||||||
|
}
|
||||||
|
|
||||||
|
@subsection{Requiring From Outside Typed Syndicate}
|
||||||
|
|
||||||
|
@defform[#:literals (:)
|
||||||
|
(require/typed lib clause ...)
|
||||||
|
#:grammar
|
||||||
|
[(clause (code:line [id : type])
|
||||||
|
(code:line opaque))
|
||||||
|
(opaque (code:line [#:opaque type-name])
|
||||||
|
(code:line [#:opaque type-name #:arity op arity-nat]))
|
||||||
|
(opaque (code:line =) (code:line >) (code:line >=))]]{
|
||||||
|
Import and assign types to bindings from outside Typed Syndicate.
|
||||||
|
|
||||||
|
An @racket[#:opaque] declaration defines a type @racket[type-name] (or, in the
|
||||||
|
@racket[#:arity] case, a type constructor) that may be used to describe imports
|
||||||
|
but otherwise has no other operations.
|
||||||
|
}
|
||||||
|
|
||||||
|
@defform[(require-struct ctor-id #:as ty-ctor-id #:from lib maybe-omit-accs)
|
||||||
|
#:grammar
|
||||||
|
[(maybe-omit-accs (code:line)
|
||||||
|
(code:line #:omit-accs))]]{
|
||||||
|
Import a Racket @racket[struct] named @racket[ctor-id] and create a type
|
||||||
|
constructor @racket[ty-ctor-id] for its instances.
|
||||||
|
|
||||||
|
Unless @racket[#:omit-accs] is specified, defines the accessor functions for the
|
||||||
|
struct.
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
@section{Builtin Data Structures}
|
||||||
|
|
||||||
|
@deftogether[(@defstruct[observe ([claim any?]) #:omit-constructor]
|
||||||
|
@defform[(Observe type)])]{
|
||||||
|
Constructs an assertion of interest.
|
||||||
|
}
|
||||||
|
|
||||||
|
@deftogether[(@defstruct[inbound ([assertion any?]) #:omit-constructor]
|
||||||
|
@defform[(Inbound type)])]{
|
||||||
|
Constructor for an assertion inbound from an outer dataspace.
|
||||||
|
}
|
||||||
|
|
||||||
|
@deftogether[(@defstruct[outbound ([assertion any?]) #:omit-constructor]
|
||||||
|
@defform[(Outbound type)])]{
|
||||||
|
Constructor for an assertion outbound to an outer dataspace.
|
||||||
|
}
|
||||||
|
|
||||||
|
@deftogether[(@defstruct[message ([body any?]) #:omit-constructor]
|
||||||
|
@defform[(Message type)])]{
|
||||||
|
Constructor for a broadcast message.
|
||||||
|
}
|
||||||
|
|
||||||
|
@subsection{Lists}
|
||||||
|
|
||||||
|
@subsection{Sets}
|
||||||
|
|
||||||
|
@subsection{Hashes}
|
||||||
|
|
||||||
@section{Behavioral Checking}
|
@section{Behavioral Checking}
|
||||||
|
|
|
@ -210,8 +210,6 @@
|
||||||
[(tuple p ...)
|
[(tuple p ...)
|
||||||
#:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
|
#:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
|
||||||
#'([x τ] ... ...)]
|
#'([x τ] ... ...)]
|
||||||
#;[(k:kons1 p)
|
|
||||||
(pat-bindings #'p)]
|
|
||||||
[(~constructor-exp cons p ...)
|
[(~constructor-exp cons p ...)
|
||||||
#:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
|
#:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
|
||||||
#'([x τ] ... ...)]
|
#'([x τ] ... ...)]
|
||||||
|
@ -265,9 +263,6 @@
|
||||||
[(tuple p ...)
|
[(tuple p ...)
|
||||||
(quasisyntax/loc pat
|
(quasisyntax/loc pat
|
||||||
(tuple #,@(stx-map elaborate-pattern #'(p ...))))]
|
(tuple #,@(stx-map elaborate-pattern #'(p ...))))]
|
||||||
[(k:kons1 p)
|
|
||||||
(quasisyntax/loc pat
|
|
||||||
(k #,(elaborate-pattern #'p)))]
|
|
||||||
[(~constructor-exp ctor p ...)
|
[(~constructor-exp ctor p ...)
|
||||||
(quasisyntax/loc pat
|
(quasisyntax/loc pat
|
||||||
(ctor #,@(stx-map elaborate-pattern #'(p ...))))]
|
(ctor #,@(stx-map elaborate-pattern #'(p ...))))]
|
||||||
|
@ -355,8 +350,6 @@
|
||||||
#:datum-literals (tuple discard bind)
|
#:datum-literals (tuple discard bind)
|
||||||
[(tuple p ...)
|
[(tuple p ...)
|
||||||
#`(#,list-binding 'tuple #,@(stx-map loop #'(p ...)))]
|
#`(#,list-binding 'tuple #,@(stx-map loop #'(p ...)))]
|
||||||
#;[(k:kons1 p)
|
|
||||||
#`(#,(kons1->constructor #'k) #,(loop #'p))]
|
|
||||||
[(bind x:id τ:type)
|
[(bind x:id τ:type)
|
||||||
(bind-id-transformer #'x)]
|
(bind-id-transformer #'x)]
|
||||||
[discard
|
[discard
|
||||||
|
|
|
@ -921,33 +921,6 @@
|
||||||
(require-struct outbound #:as Outbound #:from syndicate/protocol/standard-relay)
|
(require-struct outbound #:as Outbound #:from syndicate/protocol/standard-relay)
|
||||||
(require-struct message #:as Message #:from syndicate/core)
|
(require-struct message #:as Message #:from syndicate/core)
|
||||||
|
|
||||||
(begin-for-syntax
|
|
||||||
|
|
||||||
;; constructors with arity one
|
|
||||||
(define-syntax-class kons1
|
|
||||||
(pattern (~or (~datum observe)
|
|
||||||
(~datum inbound)
|
|
||||||
(~datum outbound)
|
|
||||||
(~datum message))))
|
|
||||||
|
|
||||||
(define (kons1->constructor stx)
|
|
||||||
(syntax-parse stx
|
|
||||||
#:datum-literals (observe inbound outbound)
|
|
||||||
[observe #'syndicate:observe]
|
|
||||||
[inbound #'syndicate:inbound]
|
|
||||||
[outbound #'syndicate:outbound]
|
|
||||||
[message #'syndicate:message]))
|
|
||||||
|
|
||||||
(define-syntax-class basic-val
|
|
||||||
(pattern (~or boolean
|
|
||||||
integer
|
|
||||||
string)))
|
|
||||||
|
|
||||||
(define-syntax-class prim-op
|
|
||||||
(pattern (~or (~literal +)
|
|
||||||
(~literal -)
|
|
||||||
(~literal displayln)))))
|
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
;; Utilities Over Types
|
;; Utilities Over Types
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
@ -1581,7 +1554,6 @@
|
||||||
(make-variable-like-transformer (add-orig (attach #'x- ': (deserialize-syntax #'serialized-τ)) #'x)))
|
(make-variable-like-transformer (add-orig (attach #'x- ': (deserialize-syntax #'serialized-τ)) #'x)))
|
||||||
(define- x- e))]))
|
(define- x- e))]))
|
||||||
|
|
||||||
;; 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
|
#:cut
|
||||||
|
|
|
@ -12,7 +12,7 @@
|
||||||
;; Start dataspace programs
|
;; Start dataspace programs
|
||||||
run-ground-dataspace
|
run-ground-dataspace
|
||||||
;; Types
|
;; Types
|
||||||
Tuple Bind Discard → ∀
|
Tuple Bind Discard → ∀ AssertionSet
|
||||||
Role Reacts Shares Asserted Retracted Message OnDataflow Stop OnStart OnStop
|
Role Reacts Shares Asserted Retracted Message OnDataflow Stop OnStart OnStop
|
||||||
Know Forget Realize
|
Know Forget Realize
|
||||||
Branch Effs
|
Branch Effs
|
||||||
|
@ -21,7 +21,7 @@
|
||||||
Computation Value Endpoints Roles Spawns Sends
|
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 block stop begin/dataflow #;unsafe-do
|
||||||
when unless send! realize! define during/spawn
|
when unless send! realize! define during/spawn
|
||||||
;; Derived Forms
|
;; Derived Forms
|
||||||
during During
|
during During
|
||||||
|
@ -33,7 +33,7 @@
|
||||||
;; endpoints
|
;; endpoints
|
||||||
assert know on field
|
assert know on field
|
||||||
;; expressions
|
;; expressions
|
||||||
tuple select lambda λ ref observe inbound outbound
|
tuple select lambda λ ref (struct-out observe) (struct-out message) (struct-out inbound) (struct-out outbound)
|
||||||
Λ inst call/inst
|
Λ inst call/inst
|
||||||
;; making types
|
;; making types
|
||||||
define-type-alias
|
define-type-alias
|
||||||
|
@ -482,8 +482,6 @@
|
||||||
#:datum-literals (tuple discard bind)
|
#:datum-literals (tuple discard bind)
|
||||||
[(tuple p ...)
|
[(tuple p ...)
|
||||||
#`(tuple #,@(stx-map loop #'(p ...)))]
|
#`(tuple #,@(stx-map loop #'(p ...)))]
|
||||||
[(k:kons1 p)
|
|
||||||
#`(k #,(loop #'p))]
|
|
||||||
[(bind x:id τ)
|
[(bind x:id τ)
|
||||||
#'x]
|
#'x]
|
||||||
;; not sure about this
|
;; not sure about this
|
||||||
|
|
Loading…
Reference in New Issue