starter for typed/syndicate/core
This commit is contained in:
Sam Caldwell
Sam Caldwell
parent
cff784384a
commit
9a3d921de3
|
|
@ -0,0 +1,865 @@
|
|||
#lang turnstile
|
||||
|
||||
(provide (rename-out [syndicate:#%module-begin #%module-begin])
|
||||
(rename-out [typed-app #%app])
|
||||
(rename-out [syndicate:begin-for-declarations declare-types])
|
||||
#%top-interaction
|
||||
require only-in
|
||||
;; Types
|
||||
Int Bool String Tuple Bind Discard → ★/t
|
||||
Observe Inbound Outbound Actor U
|
||||
Event AssertionSet Patch Instruction
|
||||
;; Core Forms
|
||||
actor dataspace make-assertion-set project ★ patch
|
||||
tuple lambda observe inbound outbound
|
||||
quit transition patch-added patch-removed
|
||||
;; values
|
||||
#%datum
|
||||
;; patterns
|
||||
bind discard
|
||||
;; primitives
|
||||
+ - * / and or not > < >= <= = equal? displayln
|
||||
;; making types
|
||||
define-type-alias
|
||||
define-constructor
|
||||
;; DEBUG and utilities
|
||||
print-type
|
||||
(rename-out [printf- printf])
|
||||
;; Extensions
|
||||
)
|
||||
|
||||
(require (for-meta 2 macrotypes/stx-utils racket/list syntax/stx))
|
||||
|
||||
(require (rename-in racket/match [match-lambda match-lambda-]))
|
||||
(require (rename-in racket/math [exact-truncate exact-truncate-]))
|
||||
(require (rename-in racket/set [set->list set->list-]))
|
||||
(require (prefix-in syndicate: syndicate/core-lang)
|
||||
(prefix-in syndicate: syndicate/trie)
|
||||
(prefix-in syndicate: syndicate/comprehensions))
|
||||
|
||||
(module+ test
|
||||
(require rackunit)
|
||||
(require turnstile/rackunit-typechecking))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Needed Forms
|
||||
;; * dataspace DONE
|
||||
;; * actor DONE
|
||||
;; * make-assertion-set DONE
|
||||
;; - ★ DONE
|
||||
;; * patch DONE
|
||||
;; * project DONE
|
||||
;; - bind
|
||||
;; - discard
|
||||
;; * transition DONE
|
||||
;; * quit DONE
|
||||
;; * fold DONE
|
||||
;; * list DONE
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Types
|
||||
|
||||
(define-base-types Int Bool String Discard ★/t)
|
||||
|
||||
(define-type-constructor Bind #:arity = 1)
|
||||
(define-type-constructor Tuple #:arity >= 0)
|
||||
(define-type-constructor U #: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)
|
||||
(define-type-constructor AssertionSet #:arity = 1)
|
||||
(define-type-constructor Patch #:arity = 2)
|
||||
(define-type-constructor List #:arity = 1)
|
||||
;; essentially the sum type of a transition or quit
|
||||
(define-type-constructor Instruction #:arity = 3)
|
||||
|
||||
(define-for-syntax (type-eval t)
|
||||
((current-type-eval) t))
|
||||
|
||||
(begin-for-syntax
|
||||
(define-syntax ~U/no-order
|
||||
(pattern-expander
|
||||
(syntax-parser
|
||||
[(_ p ...)
|
||||
#:fail-when (stx-ormap (lambda [x] (and (identifier? x)
|
||||
(free-identifier=? x #'(... ...))))
|
||||
#'(p ...))
|
||||
"ellipses not allowed"
|
||||
#:with ((v ...) ...) (permutations (stx->list #'(p ...)))
|
||||
#'(~or* (~U v ...) ...)]))))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; User Defined Types, aka Constructors
|
||||
|
||||
;; τ.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]))]))
|
||||
|
||||
(begin-for-syntax
|
||||
(define-splicing-syntax-class type-constructor-decl
|
||||
(pattern (~seq #:type-constructor TypeCons:id))
|
||||
(pattern (~seq) #:attr TypeCons #f))
|
||||
|
||||
(struct user-ctor (typed-ctor untyped-ctor)
|
||||
#:property prop:procedure
|
||||
(lambda (v stx)
|
||||
(define transformer (user-ctor-typed-ctor v))
|
||||
(syntax-parse stx
|
||||
[(_ e ...)
|
||||
#`(#,transformer e ...)]))))
|
||||
|
||||
(define-syntax (define-constructor stx)
|
||||
(syntax-parse stx
|
||||
[(_ (Cons:id slot:id ...)
|
||||
ty-cons:type-constructor-decl
|
||||
(~seq #:with
|
||||
Alias AliasBody) ...)
|
||||
#:with TypeCons (or (attribute ty-cons.TypeCons) (format-id stx "~a/t" (syntax-e #'Cons)))
|
||||
#:with MakeTypeCons (format-id #'TypeCons "make-~a" #'TypeCons)
|
||||
#:with GetTypeParams (format-id #'TypeCons "get-~a-type-params" #'TypeCons)
|
||||
#:with TypeConsExpander (format-id #'TypeCons "~~~a" #'TypeCons)
|
||||
#:with TypeConsExtraInfo (format-id #'TypeCons "~a-extra-info" #'TypeCons)
|
||||
#:with (StructName Cons- type-tag) (generate-temporaries #'(Cons Cons Cons))
|
||||
(define arity (stx-length #'(slot ...)))
|
||||
#`(begin-
|
||||
(struct- StructName (slot ...) #:reflection-name 'Cons #:transparent)
|
||||
(define-syntax (TypeConsExtraInfo stx)
|
||||
(syntax-parse stx
|
||||
[(_ X (... ...)) #'('type-tag 'MakeTypeCons 'GetTypeParams)]))
|
||||
(define-type-constructor TypeCons
|
||||
#:arity = #,arity
|
||||
#:extra-info 'TypeConsExtraInfo)
|
||||
(define-syntax (MakeTypeCons stx)
|
||||
(syntax-parse stx
|
||||
[(_ t (... ...))
|
||||
#:fail-unless (= #,arity (stx-length #'(t (... ...)))) "arity mismatch"
|
||||
#'(TypeCons t (... ...))]))
|
||||
(define-syntax (GetTypeParams stx)
|
||||
(syntax-parse stx
|
||||
[(_ (TypeConsExpander t (... ...)))
|
||||
#'(t (... ...))]))
|
||||
(define-syntax Cons
|
||||
(user-ctor #'Cons- #'StructName))
|
||||
(define-typed-syntax (Cons- e (... ...)) ≫
|
||||
#:fail-unless (= #,arity (stx-length #'(e (... ...)))) "arity mismatch"
|
||||
[⊢ e ≫ e- (⇒ : τ)] (... ...)
|
||||
----------------------
|
||||
[⊢ (#%app- StructName e- (... ...)) (⇒ : (TypeCons τ (... ...)))])
|
||||
(define-type-alias Alias AliasBody) ...)]))
|
||||
|
||||
(begin-for-syntax
|
||||
(define-syntax ~constructor-extra-info
|
||||
(pattern-expander
|
||||
(syntax-parser
|
||||
[(_ tag mk get)
|
||||
#'(_ (_ tag) (_ mk) (_ get))])))
|
||||
|
||||
(define-syntax ~constructor-type
|
||||
(pattern-expander
|
||||
(syntax-parser
|
||||
[(_ tag . rst)
|
||||
#'(~and it
|
||||
(~fail #:unless (user-defined-type? #'it))
|
||||
(~parse tag (get-type-tag #'it))
|
||||
(~Any _ . rst))])))
|
||||
|
||||
(define-syntax ~constructor-exp
|
||||
(pattern-expander
|
||||
(syntax-parser
|
||||
[(_ cons . rst)
|
||||
#'(~and (cons . rst)
|
||||
(~fail #:unless (ctor-id? #'cons)))])))
|
||||
|
||||
(define (inspect t)
|
||||
(syntax-parse t
|
||||
[(~constructor-type tag t ...)
|
||||
(list (syntax-e #'tag) (stx-map type->str #'(t ...)))]))
|
||||
|
||||
(define (tags-equal? t1 t2)
|
||||
(equal? (syntax-e t1) (syntax-e t2)))
|
||||
|
||||
(define (user-defined-type? t)
|
||||
(get-extra-info (type-eval t)))
|
||||
|
||||
(define (get-type-tag t)
|
||||
(syntax-parse (get-extra-info t)
|
||||
[(~constructor-extra-info tag _ _)
|
||||
(syntax-e #'tag)]))
|
||||
|
||||
(define (get-type-args t)
|
||||
(syntax-parse (get-extra-info t)
|
||||
[(~constructor-extra-info _ _ get)
|
||||
(define f (syntax-local-value #'get))
|
||||
(syntax->list (f #`(get #,t)))]))
|
||||
|
||||
(define (make-cons-type t args)
|
||||
(syntax-parse (get-extra-info t)
|
||||
[(~constructor-extra-info _ mk _)
|
||||
(define f (syntax-local-value #'mk))
|
||||
(type-eval (f #`(mk #,@args)))]))
|
||||
|
||||
(define (ctor-id? stx)
|
||||
(and (identifier? stx)
|
||||
(user-ctor? (syntax-local-value stx (const #f)))))
|
||||
|
||||
(define (untyped-ctor stx)
|
||||
(user-ctor-untyped-ctor (syntax-local-value stx (const #f)))))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Conveniences
|
||||
|
||||
(define-type-alias (Action τ-a τ-s)
|
||||
(U (Patch τ-a ★/t) (Actor τ-s)))
|
||||
|
||||
(begin-for-syntax
|
||||
(define-syntax ~Action
|
||||
(pattern-expander
|
||||
(syntax-parser
|
||||
[(_ p1 p2)
|
||||
#'(~U/no-order (~Patch p1 _) (~Actor p2))]))))
|
||||
|
||||
(define-type-alias (Event τ)
|
||||
(Patch τ τ))
|
||||
|
||||
#;(begin-for-syntax
|
||||
(define-syntax ~Event
|
||||
(pattern-expander
|
||||
(syntax-parser
|
||||
[(_ t)
|
||||
#`(~and (~Patch τ1:type τ2:type)
|
||||
(~parse t #,(type-eval #'(U τ1 τ2))))]))))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Syntax
|
||||
|
||||
(begin-for-syntax
|
||||
|
||||
;; 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
|
||||
integer
|
||||
string)))
|
||||
|
||||
(define-syntax-class prim-op
|
||||
(pattern (~or (~literal +)
|
||||
(~literal -)
|
||||
(~literal displayln)))))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Subtyping
|
||||
|
||||
;; 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))]
|
||||
[((~AssertionSet τ1) (~AssertionSet τ2))
|
||||
(<: #'τ1 #'τ2)]
|
||||
[((~Patch τ11 τ12) (~Patch τ21 τ22))
|
||||
(and (<: #'τ11 #'τ21)
|
||||
(<: #'τ12 #'τ22))]
|
||||
[((~Instruction τs1 τo1 τa1) (~Instruction τs2 τo2 τa2))
|
||||
(and (<: #'τs1 #'τs2)
|
||||
(<: #'τo1 #'τo2)
|
||||
(<: (type-eval #'(Actor τa1)) (type-eval #'(Actor τa2))))]
|
||||
[((~Tuple τ1:type ...) (~Tuple τ2:type ...))
|
||||
#:when (stx-length=? #'(τ1 ...) #'(τ2 ...))
|
||||
(stx-andmap <: #'(τ1 ...) #'(τ2 ...))]
|
||||
[(_ ~★/t)
|
||||
(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)]
|
||||
[((~constructor-type t1 τ1:type ...) (~constructor-type t2 τ2:type ...))
|
||||
#:when (tags-equal? #'t1 #'t2)
|
||||
(and (stx-length=? #'(τ1 ...) #'(τ2 ...))
|
||||
(stx-andmap <: #'(τ1 ...) #'(τ2 ...)))]
|
||||
[((~→ τ-in1 ... τ-out1) (~→ τ-in2 ... τ-out2))
|
||||
#:when (stx-length=? #'(τ-in1 ...) #'(τ-in2 ...))
|
||||
(and (stx-andmap <: #'(τ-in2 ...) #'(τ-in1 ...))
|
||||
(<: #'τ-out1 #'τ-out2))]
|
||||
[(~Discard _)
|
||||
#t]
|
||||
;; should probably put this first.
|
||||
[_ (type=? t1 t2)]))
|
||||
|
||||
(define-for-syntax (bot? t)
|
||||
(<: t (type-eval #'(U))))
|
||||
|
||||
;; 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)
|
||||
[(_ ~★/t)
|
||||
t1]
|
||||
[(~★/t _)
|
||||
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 ...))))]
|
||||
[((~AssertionSet τ1) (~AssertionSet τ2))
|
||||
#:with τ12 (∩ #'τ1 #'τ2)
|
||||
(type-eval #'(AssertionSet τ12))]
|
||||
[((~Patch τ11 τ12) (~Patch τ21 τ22))
|
||||
#:with τ1 (∩ #'τ11 #'τ12)
|
||||
#:with τ2 (∩ #'τ21 #'τ22)
|
||||
(type-eval #'(Patch τ1 τ2))]
|
||||
[((~Instruction τs1 τo1 τa1) (~Instruction τs2 τo2 τa2))
|
||||
#:with τs (∩ #'τs1 #'τs2)
|
||||
#:fail-when (bot? #'τs) #f
|
||||
#:with τa (∩ #'τa1 #'τa2)
|
||||
#:fail-when (bot? #'τa) #f
|
||||
#:with τo (∩ #'τo1 #'τo2)
|
||||
(type-eval #'(Instruction τs τo τa))]
|
||||
;; 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 τ ...))]
|
||||
[((~constructor-type tag1 τ1:type ...) (~constructor-type tag2 τ2:type ...))
|
||||
#:when (tags-equal? #'tag1 #'tag2)
|
||||
#:with (τ ...) (stx-map ∩ #'(τ1 ...) #'(τ2 ...))
|
||||
#:fail-when (stx-ormap (lambda (t) (<: t (type-eval #'(U)))) #'(τ ...)) #f
|
||||
(make-cons-type t1 #'(τ ...))]
|
||||
;; 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]
|
||||
[(_ ~★/t)
|
||||
#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 ...))]
|
||||
[((~constructor-type _ τ1:type ...) (~constructor-type _ τ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 + ★/t, Bind, Discard (assertion and pattern types)
|
||||
(define-for-syntax (overlap? t1 t2)
|
||||
(syntax-parse #`(#,t1 #,t2)
|
||||
[(~★/t _) #t]
|
||||
[(_ (~Bind _)) #t]
|
||||
[(_ ~Discard) #t]
|
||||
[(_ ~★/t) #t]
|
||||
[((~U τ1:type ...) _)
|
||||
(stx-ormap (lambda (t) (overlap? t t2)) #'(τ1 ...))]
|
||||
[(_ (~U τ2:type ...))
|
||||
(stx-ormap (lambda (t) (overlap? t1 t)) #'(τ2 ...))]
|
||||
[((~List _) (~List _))
|
||||
;; share the empty list
|
||||
#t]
|
||||
[((~Tuple τ1:type ...) (~Tuple τ2:type ...))
|
||||
(and (stx-length=? #'(τ1 ...) #'(τ2 ...))
|
||||
(stx-andmap overlap? #'(τ1 ...) #'(τ2 ...)))]
|
||||
[((~constructor-type t1 τ1:type ...) (~constructor-type t2 τ2:type ...))
|
||||
(and (tags-equal? #'t1 #'t2)
|
||||
(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
|
||||
[~★/t #f]
|
||||
[(~U τ:type ...)
|
||||
(stx-andmap finite? #'(τ ...))]
|
||||
[(~Tuple τ:type ...)
|
||||
(stx-andmap finite? #'(τ ...))]
|
||||
[(~constructor-type _ τ:type ...)
|
||||
(stx-andmap finite? #'(τ ...))]
|
||||
[(~Observe τ:type)
|
||||
(finite? #'τ)]
|
||||
[(~Inbound τ:type)
|
||||
(finite? #'τ)]
|
||||
[(~Outbound τ:type)
|
||||
(finite? #'τ)]
|
||||
[_ #t]))
|
||||
|
||||
;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
||||
;; MODIFYING GLOBAL TYPECHECKING STATE!!!!!
|
||||
;; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
||||
|
||||
(begin-for-syntax
|
||||
(current-typecheck-relation <:))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Core forms
|
||||
|
||||
(define-typed-syntax (actor τ-c:type beh st0 as0) ≫
|
||||
#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
|
||||
[⊢ beh ≫ beh- ⇒ (~→ (~Patch τ-i1:type τ-i2:type)
|
||||
τ-s:type
|
||||
(~Instruction τ-s2:type τ-ta:type τ-ts:type))]
|
||||
[⊢ st0 ≫ st0- ⇒ τ-st0:type]
|
||||
[⊢ as0 ≫ as0- ⇒ (~AssertionSet τ-as0:type)]
|
||||
#:with τ-out:type (type-eval #'(U τ-ta τ-as0))
|
||||
#:with τ-in:type (type-eval #'(U τ-i1 τ-i2))
|
||||
#:fail-unless (<: #'τ-st0.norm #'τ-s.norm)
|
||||
"bad initial state"
|
||||
#:fail-unless (<: #'τ-s2.norm #'τ-s.norm)
|
||||
"bad state update"
|
||||
#:fail-unless (<: #'τ-out.norm #'τ-c.norm)
|
||||
"output not allowed in dataspace"
|
||||
#:fail-unless (<: (type-eval #'(Actor τ-ts.norm))
|
||||
(type-eval #'(Actor τ-c.norm)))
|
||||
"spawned actors not valid in dataspace"
|
||||
#:fail-unless (<: (∩ (strip-? #'τ-out.norm) #'τ-c.norm) #'τ-in.norm)
|
||||
"Not prepared to handle all inputs"
|
||||
--------------------------------------------------------------------------------------------
|
||||
[⊢ (syndicate:actor beh- st0- (list- (syndicate:patch as0- syndicate:trie-empty)))
|
||||
⇒ (Actor τ-c)])
|
||||
|
||||
(define-typed-syntax (dataspace τ-c:type e) ≫
|
||||
#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
|
||||
[⊢ e ≫ e- ⇒ (~List τa:type)]
|
||||
#:fail-unless (<: #'τa.norm (type-eval #'(Actor τ-c.norm)))
|
||||
"Not all actors conform to communication type"
|
||||
#:with τ-ds-i (strip-inbound #'τ-c.norm)
|
||||
#:with τ-ds-o (strip-outbound #'τ-c.norm)
|
||||
#:with τ-relay (relay-interests #'τ-c.norm)
|
||||
-----------------------------------------------------------------------------------
|
||||
[⊢ (syndicate:dataspace e-) ⇒ (Actor (U τ-ds-i τ-ds-o τ-relay))])
|
||||
|
||||
(define-typed-syntax (transition e-s e-as) ≫
|
||||
[⊢ e-s ≫ e-s- ⇒ τ-s]
|
||||
[⊢ e-as ≫ e-as- ⇒ (~List (~Action τ-o τ-a))]
|
||||
-----------------------------------------
|
||||
[⊢ (syndicate:transition e-s- e-as-) ⇒ (Instruction τ-s τ-o τ-a)])
|
||||
|
||||
(define-typed-syntax quit
|
||||
[(quit) ≫
|
||||
-------------------------------------
|
||||
[⊢ (syndicate:quit) ⇒ (Instruction (U) (U) (U))]]
|
||||
[(quit as) ≫
|
||||
[⊢ as ≫ as- ⇒ (~List (~Action τ-o τ-a))]
|
||||
----------------------------------------
|
||||
[⊢ (syndicate:quit as-) ⇒ (Instruction (U) τ-o τ-a)]])
|
||||
|
||||
(define-typed-syntax ★
|
||||
[_ ≫
|
||||
-------------------------
|
||||
[⊢ syndicate:? ⇒ ★/t]])
|
||||
|
||||
(define-typed-syntax (make-assertion-set e ...) ≫
|
||||
[⊢ e ≫ e- ⇒ τ] ...
|
||||
#:fail-unless (stx-andmap flat-type? #'(τ ...))
|
||||
"assertions must be first-order"
|
||||
-------------------------------------------------
|
||||
[⊢ (syndicate:trie-union-all (list- (syndicate:pattern->trie 'typed e-) ...))
|
||||
⇒ (AssertionSet (U τ ...))])
|
||||
|
||||
(define-typed-syntax (patch e-add e-sub) ≫
|
||||
[⊢ e-add ≫ e-add- ⇒ (~AssertionSet τ-add)]
|
||||
[⊢ e-sub ≫ e-sub- ⇒ (~AssertionSet τ-sub)]
|
||||
--------------------------------------------
|
||||
[⊢ (syndicate:patch e-add- e-sub-) ⇒ (Patch τ-add τ-sub)])
|
||||
|
||||
(define-typed-syntax (project [pat e-set] e-body) ≫
|
||||
[⊢ e-set ≫ e-set- ⇒ (~AssertionSet τ-s:type)]
|
||||
[⊢ pat ≫ _ ⇒ τ-p:type]
|
||||
#:with ([x:id τ:type] ...) (pat-bindings #'pat)
|
||||
[[x ≫ x- : τ] ... ⊢ e-body ≫ e-body- ⇒ τ-b]
|
||||
#:fail-unless (project-safe? #'τ-s.norm #'τ-p.norm)
|
||||
"pattern captures infinite set"
|
||||
#:with pat- (substs #'(x- ...) #'(x ...) (compile-syndicate-pattern #'pat))
|
||||
--------------------------------------------------------
|
||||
[⊢ (syndicate:for-trie/list ([pat- e-set-])
|
||||
e-body-)
|
||||
⇒ (List τ-b)])
|
||||
|
||||
(begin-for-syntax
|
||||
(define (compile-pattern pat bind-id-transformer exp-transformer)
|
||||
(define (l-e stx) (local-expand stx 'expression '()))
|
||||
(let loop ([pat pat])
|
||||
(syntax-parse pat
|
||||
#:datum-literals (tuple discard bind)
|
||||
[(tuple p ...)
|
||||
#`(list- 'tuple #,@(stx-map loop #'(p ...)))]
|
||||
[(k:kons1 p)
|
||||
#`(#,(kons1->constructor #'k) #,(loop #'p))]
|
||||
[(bind x:id τ:type)
|
||||
(bind-id-transformer #'x)]
|
||||
[discard
|
||||
#'_]
|
||||
[(~constructor-exp ctor p ...)
|
||||
(define/with-syntax uctor (untyped-ctor #'ctor))
|
||||
#`(uctor #,@(stx-map loop #'(p ...)))]
|
||||
[_
|
||||
;; local expanding "expression-y" syntax allows variable references to transform
|
||||
;; according to the mappings set up by turnstile.
|
||||
(exp-transformer (l-e pat))])))
|
||||
|
||||
(define (compile-syndicate-pattern pat)
|
||||
(compile-pattern pat
|
||||
(lambda (id) #`($ #,id))
|
||||
identity)))
|
||||
|
||||
(define-typed-syntax (list e ...) ≫
|
||||
[⊢ e ≫ e- ⇒ τ] ...
|
||||
-------------------
|
||||
[⊢ (list- e- ...) ⇒ (List (U τ ...))])
|
||||
|
||||
(define-typed-syntax (for/fold [acc:id e-acc]
|
||||
[x:id e-list]
|
||||
e-body) ≫
|
||||
[⊢ e-list ≫ e-list- ⇒ (~List τ-l)]
|
||||
[⊢ e-acc ≫ e-acc- ⇒ τ-a:type]
|
||||
[[x ≫ x- : τ-l] [acc ≫ acc- : τ-a] ⊢ e-body ≫ e-body- ⇒ τ-b:type]
|
||||
#:fail-unless (<: #'τ-b.norm #'τ-a.norm)
|
||||
"loop body doesn't match accumulator"
|
||||
-------------------------------------------------------
|
||||
[⊢ (for/fold- ([acc- e-acc-])
|
||||
([x- (in-list- e-list-)])
|
||||
e-body-)
|
||||
⇒ τ-b])
|
||||
|
||||
(define-for-syntax (strip-? t)
|
||||
(type-eval
|
||||
(syntax-parse t
|
||||
;; TODO: probably need to `normalize` the result
|
||||
[(~U τ ...) #`(U #,@(stx-map strip-? #'(τ ...)))]
|
||||
[~★/t #'★/t]
|
||||
[(~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-? #'(τ ...)))]
|
||||
[~★/t #'★/t]
|
||||
[(~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-? #'(τ ...)))]
|
||||
[~★/t #'★/t]
|
||||
[(~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-? #'(τ ...)))]
|
||||
[~★/t #'★/t]
|
||||
[(~Observe (~Inbound τ)) #'(Observe τ)]
|
||||
[_ #'(U)])))
|
||||
|
||||
(define-for-syntax (procedure-type? τ)
|
||||
(syntax-parse τ
|
||||
[(~→ τ ...+) #t]
|
||||
[_ #f]))
|
||||
|
||||
(define-for-syntax (flat-type? τ)
|
||||
(syntax-parse τ
|
||||
[(~→ τ ...) #f]
|
||||
[_ #t]))
|
||||
|
||||
(define-typed-syntax (unsafe-do rkt:expr ...) ≫
|
||||
------------------------
|
||||
[⊢ (let- () rkt ...) (⇒ : (U)) (⇒ :i (U)) (⇒ :o (U)) (⇒ :a (U))])
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Expressions
|
||||
|
||||
(define-typed-syntax (lambda ([x:id (~optional (~literal :)) τ:type] ...) e) ≫
|
||||
[[x ≫ x- : τ] ... ⊢ e ≫ e- ⇒ τ-e]
|
||||
----------------------------------------
|
||||
[⊢ (lambda- (x- ...) e-) ⇒ (→ τ ... τ-e)])
|
||||
|
||||
(define-typed-syntax (tuple e:expr ...) ≫
|
||||
[⊢ e ≫ e- (⇒ : τ)] ...
|
||||
-----------------------
|
||||
[⊢ (list- 'tuple e- ...) (⇒ : (Tuple τ ...))])
|
||||
|
||||
(define-typed-syntax (typed-app e_fn e_arg ...) ≫
|
||||
[⊢ e_fn ≫ e_fn- (⇒ : (~→ τ_in:type ... τ_out:type))]
|
||||
#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
|
||||
(num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
|
||||
[⊢ e_arg ≫ e_arg- ⇐ τ_in] ...
|
||||
------------------------------------------------------------------------
|
||||
[⊢ (#%app- e_fn- e_arg- ...) (⇒ : τ_out)])
|
||||
|
||||
;; it would be nice to abstract over these three
|
||||
(define-typed-syntax (observe e:expr) ≫
|
||||
[⊢ e ≫ e- (⇒ : τ)]
|
||||
---------------------------------------------------------------------------
|
||||
[⊢ (syndicate:observe e-) (⇒ : (Observe τ))])
|
||||
|
||||
(define-typed-syntax (inbound e:expr) ≫
|
||||
[⊢ e ≫ e- ⇒ τ]
|
||||
---------------------------------------------------------------------------
|
||||
[⊢ (syndicate:inbound e-) (⇒ : (Inbound τ))])
|
||||
|
||||
(define-typed-syntax (outbound e:expr) ≫
|
||||
[⊢ e ≫ e- ⇒ τ]
|
||||
---------------------------------------------------------------------------
|
||||
[⊢ (syndicate:outbound e-) (⇒ : (Outbound τ))])
|
||||
|
||||
(define-typed-syntax (patch-added e) ≫
|
||||
[⊢ e ≫ e- ⇒ (~Patch τ _)]
|
||||
--------------------------
|
||||
[⊢ (syndicate:patch-added e-) ⇒ (AssertionSet τ)])
|
||||
|
||||
(define-typed-syntax (patch-removed e) ≫
|
||||
[⊢ e ≫ e- ⇒ (~Patch _ τ)]
|
||||
--------------------------
|
||||
[⊢ (syndicate:patch-removed e-) ⇒ (AssertionSet τ)])
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Patterns
|
||||
|
||||
(define-typed-syntax (bind x:id τ:type) ≫
|
||||
----------------------------------------
|
||||
[⊢ (error- 'bind "escaped") ⇒ (Bind τ)])
|
||||
|
||||
(define-typed-syntax discard
|
||||
[_ ≫
|
||||
--------------------
|
||||
;; TODO: change void to _
|
||||
[⊢ (error- 'discard "escaped") ⇒ Discard]])
|
||||
|
||||
;; pat -> ([Id Type] ...)
|
||||
(define-for-syntax (pat-bindings stx)
|
||||
(syntax-parse stx
|
||||
#:datum-literals (bind tuple)
|
||||
[(bind x:id τ:type)
|
||||
#'([x τ])]
|
||||
[(tuple p ...)
|
||||
#:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
|
||||
#'([x τ] ... ...)]
|
||||
[(k:kons1 p)
|
||||
(pat-bindings #'p)]
|
||||
[(~constructor-exp cons p ...)
|
||||
#:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
|
||||
#'([x τ] ... ...)]
|
||||
[_
|
||||
#'()]))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Primitives
|
||||
|
||||
;; hmmm
|
||||
(define-primop + (→ Int Int Int))
|
||||
(define-primop - (→ Int Int Int))
|
||||
(define-primop * (→ Int Int Int))
|
||||
#;(define-primop and (→ Bool Bool Bool))
|
||||
(define-primop or (→ Bool Bool Bool))
|
||||
(define-primop not (→ Bool Bool))
|
||||
(define-primop < (→ Int Int Bool))
|
||||
(define-primop > (→ Int Int Bool))
|
||||
(define-primop <= (→ Int Int Bool))
|
||||
(define-primop >= (→ Int Int Bool))
|
||||
(define-primop = (→ Int Int Bool))
|
||||
|
||||
(define-typed-syntax (/ e1 e2) ≫
|
||||
[⊢ e1 ≫ e1- (⇐ : Int)]
|
||||
[⊢ e2 ≫ e2- (⇐ : Int)]
|
||||
------------------------
|
||||
[⊢ (exact-truncate- (/- e1- e2-)) (⇒ : Int)])
|
||||
|
||||
;; for some reason defining `and` as a prim op doesn't work
|
||||
(define-typed-syntax (and e ...) ≫
|
||||
[⊢ e ≫ e- (⇐ : Bool)] ...
|
||||
------------------------
|
||||
[⊢ (and- e- ...) (⇒ : Bool)])
|
||||
|
||||
(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)])
|
||||
|
||||
(define-typed-syntax (displayln e:expr) ≫
|
||||
[⊢ e ≫ e- ⇒ τ]
|
||||
---------------
|
||||
[⊢ (displayln- e-) (⇒ : (U))])
|
||||
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Basic Values
|
||||
|
||||
(define-typed-syntax #%datum
|
||||
[(_ . n:integer) ≫
|
||||
----------------
|
||||
[⊢ (#%datum- . n) (⇒ : Int)]]
|
||||
[(_ . b:boolean) ≫
|
||||
----------------
|
||||
[⊢ (#%datum- . b) (⇒ : Bool)]]
|
||||
[(_ . s:string) ≫
|
||||
----------------
|
||||
[⊢ (#%datum- . s) (⇒ : String)]])
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Utilities
|
||||
|
||||
(define-typed-syntax (print-type e) ≫
|
||||
[⊢ e ≫ e- ⇒ τ]
|
||||
#:do [(displayln (type->str #'τ))]
|
||||
----------------------------------
|
||||
[⊢ e- ⇒ τ])
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Extensions
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Tests
|
||||
|
||||
;; project
|
||||
(module+ test
|
||||
|
||||
|
||||
(check-type (project [(tuple) (make-assertion-set (tuple 1 2))]
|
||||
(tuple))
|
||||
: (List (Tuple))
|
||||
-> (list-))
|
||||
|
||||
(check-type (project [(tuple) (make-assertion-set (tuple))]
|
||||
(tuple))
|
||||
: (List (Tuple))
|
||||
-> (list- (tuple)))
|
||||
|
||||
(check-type (project [(tuple (bind x Int) 2) (make-assertion-set (tuple 1 2))]
|
||||
x)
|
||||
: (List Int)
|
||||
-> (list- 1))
|
||||
|
||||
(check-type (project [(tuple (bind x Int) 2) (make-assertion-set (tuple 1 2) "hello")]
|
||||
x)
|
||||
: (List Int)
|
||||
-> (list- 1))
|
||||
|
||||
(check-type (project [(tuple (bind x (U Int (Tuple Int Int))) 2)
|
||||
(make-assertion-set (tuple 1 2)
|
||||
"hello"
|
||||
(tuple (tuple 4 5) 2))]
|
||||
|
||||
x)
|
||||
: (List (U Int (Tuple Int Int)))
|
||||
-> (list- (tuple 4 5) 1))
|
||||
|
||||
;; nested project to test for ambiguous binding error
|
||||
(check-type (project [(tuple (bind x Int) 2) (make-assertion-set (tuple 1 2))]
|
||||
(project [(tuple discard x) (make-assertion-set (tuple "bizboz" 1))]
|
||||
x))
|
||||
: (List (List Int))
|
||||
-> (list- (list- 1))))
|
||||
|
||||
;; fold
|
||||
(module+ test
|
||||
(check-type (for/fold (sum 0)
|
||||
(x (list 1 2 3))
|
||||
(typed-app + x sum))
|
||||
: Int
|
||||
-> 6))
|
||||
|
||||
;; functions
|
||||
(module+ test
|
||||
(check-type (lambda ([x Int]) x) : (→ Int Int))
|
||||
(check-type (typed-app (lambda ([x : Int]) x) 5)
|
||||
: Int
|
||||
-> 5))
|
||||
|
||||
;; patches
|
||||
(module+ test
|
||||
(check-type (patch-added (patch (make-assertion-set 12) (make-assertion-set)))
|
||||
: (AssertionSet Int)
|
||||
-> (make-assertion-set 12))
|
||||
(check-type (patch-removed (patch (make-assertion-set 12) (make-assertion-set)))
|
||||
: (AssertionSet (U))
|
||||
-> (make-assertion-set)))
|
||||
|
|
@ -0,0 +1,33 @@
|
|||
#lang typed/syndicate/core
|
||||
|
||||
(define-constructor (set-box new-value)
|
||||
#:type-constructor SetBoxT
|
||||
#:with SetBox (SetBoxT Int))
|
||||
|
||||
(define-constructor (box-state value)
|
||||
#:type-constructor BoxStateT
|
||||
#:with BoxState (BoxStateT Int))
|
||||
|
||||
(define-type-alias τ-c
|
||||
(U BoxState
|
||||
(Observe (BoxStateT ★/t))
|
||||
SetBox
|
||||
(Observe (SetBoxT ★/t))))
|
||||
|
||||
(actor τ-c
|
||||
(lambda ([e : (Event τ-c)]
|
||||
[current-value : Int])
|
||||
(quit))
|
||||
0
|
||||
(make-assertion-set (box-state 0)
|
||||
(observe (set-box ★))))
|
||||
|
||||
#;(actor (lambda (e current-value)
|
||||
(match-event e
|
||||
[(message (set-box new-value))
|
||||
(log-info "box: taking on new-value ~v" new-value)
|
||||
(transition new-value (patch-seq (retract (box-state current-value))
|
||||
(assert (box-state new-value))))]))
|
||||
0
|
||||
(patch-seq (sub (set-box ?))
|
||||
(assert (box-state 0))))
|
||||
|
|
@ -62,6 +62,11 @@
|
|||
(define-for-syntax (type-eval t)
|
||||
((current-type-eval) t))
|
||||
|
||||
;; this needs to be here until I stop 'compiling' patterns and just have them expand to the right
|
||||
;; thing
|
||||
(begin-for-syntax
|
||||
(current-use-stop-list? #f))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; User Defined Types, aka Constructors
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,2 @@
|
|||
#lang s-exp syntax/module-reader
|
||||
typed/core
|
||||
Loading…
Reference in New Issue