some work towards a better pattern language
This commit is contained in:
Sam Caldwell
parent
24efe43a6f
commit
13e988fe58
|
|
@ -138,18 +138,20 @@
|
|||
(define-typed-syntax (match e [p s ...+] ...+) ≫
|
||||
[⊢ e ≫ e- (⇒ : τ-e)]
|
||||
#:fail-unless (pure? #'e-) "expression must be pure"
|
||||
#:with (([x τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
|
||||
#:with (p/e ...) (for/list ([pat (in-syntax #'(p ...))])
|
||||
(elaborate-pattern/with-type pat #'τ-e))
|
||||
#:with (([x τ:type] ...) ...) (stx-map pat-bindings #'(p/e ...))
|
||||
[[x ≫ x- : τ.norm] ... ⊢ (begin s ...) ≫ s- (⇒ : τ-s)
|
||||
(⇒ ν-ep (~effs eps ...))
|
||||
(⇒ ν-f (~effs fs ...))
|
||||
(⇒ ν-s (~effs ss ...))] ...
|
||||
;; 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] ...
|
||||
[⊢ p/e ≫ p-- ⇒ τ-p] ...
|
||||
#:fail-unless (project-safe? #'τ-e (mk-U*- #'(τ-p ...))) "possibly unsafe pattern match"
|
||||
#:fail-unless (stx-andmap pure? #'(p-- ...)) "patterns must be pure"
|
||||
#:with (p- ...) (stx-map (lambda (p x-s xs) (substs x-s xs (compile-match-pattern p)))
|
||||
#'(p ...)
|
||||
#'(p/e ...)
|
||||
#'((x- ...) ...)
|
||||
#'((x ...) ...))
|
||||
--------------------------------------------------------------
|
||||
|
|
@ -200,7 +202,7 @@
|
|||
[(tuple p ...)
|
||||
#:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
|
||||
#'([x τ] ... ...)]
|
||||
[(k:kons1 p)
|
||||
#;[(k:kons1 p)
|
||||
(pat-bindings #'p)]
|
||||
[(~constructor-exp cons p ...)
|
||||
#:with (([x:id τ:type] ...) ...) (stx-map pat-bindings #'(p ...))
|
||||
|
|
@ -208,6 +210,134 @@
|
|||
[_
|
||||
#'()]))
|
||||
|
||||
(begin-for-syntax
|
||||
;; Any -> Bool
|
||||
(define (dollar-variable? x)
|
||||
(and (identifier? x)
|
||||
(char=? (string-ref (symbol->string (syntax-e x)) 0) #\$)))
|
||||
|
||||
;; dollar-id -> Identifier
|
||||
(define (un-dollar x)
|
||||
(datum->syntax x (string->symbol (substring (symbol->string (syntax-e x)) 1))))
|
||||
|
||||
(define-syntax-class dollar-id
|
||||
#:attributes (id)
|
||||
(pattern x:id
|
||||
#:when (dollar-variable? #'x)
|
||||
#:attr id (un-dollar #'x)))
|
||||
|
||||
;; match things of the for "$X...:Y..." where X and Y are things without
|
||||
;; spaces (i.e. likely but not definitely legal identifiers)
|
||||
(define DOLLAR-ANN-RX #px"^\\$(\\S*):(\\S*)$")
|
||||
|
||||
;; Any -> RegexpMatchResults
|
||||
(define (dollar-ann-variable? x)
|
||||
(and (identifier? x)
|
||||
(regexp-match DOLLAR-ANN-RX (symbol->string (syntax-e x)))))
|
||||
|
||||
(define-syntax-class dollar-ann-id
|
||||
#:attributes (id ty)
|
||||
(pattern x:id
|
||||
#:do [(define match? (dollar-ann-variable? #'x))]
|
||||
#:when match?
|
||||
#:attr id (datum->syntax #'x (string->symbol (second match?)))
|
||||
#:attr ty (datum->syntax #'x (string->symbol (third match?)))))
|
||||
|
||||
;; expand uses of $ short-hand
|
||||
;; doesn't handle uses of $id or ($) w/o a type
|
||||
(define (elaborate-pattern pat)
|
||||
(syntax-parse pat
|
||||
#:datum-literals (tuple _ $)
|
||||
[_
|
||||
#'discard]
|
||||
[x:dollar-ann-id
|
||||
(syntax/loc pat (bind x.id x.ty))]
|
||||
[($ x:id ty)
|
||||
(syntax/loc pat (bind x ty))]
|
||||
[(tuple p ...)
|
||||
(quasisyntax/loc pat
|
||||
(tuple #,@(stx-map elaborate-pattern #'(p ...))))]
|
||||
[(k:kons1 p)
|
||||
(quasisyntax/loc pat
|
||||
(k #,(elaborate-pattern #'p)))]
|
||||
[(~constructor-exp ctor p ...)
|
||||
(quasisyntax/loc pat
|
||||
(ctor #,@(stx-map elaborate-pattern #'(p ...))))]
|
||||
[e:expr
|
||||
#'e]))
|
||||
|
||||
(define (elaborate-pattern/with-type pat ty)
|
||||
(syntax-parse pat
|
||||
#:datum-literals (tuple $)
|
||||
[(~datum _)
|
||||
#'discard]
|
||||
[x:dollar-ann-id
|
||||
(syntax/loc pat (bind x.id x.ty))]
|
||||
[x:dollar-id
|
||||
(quasisyntax/loc pat (bind x.id #,ty))]
|
||||
[($ x:id ty)
|
||||
(syntax/loc pat (bind x ty))]
|
||||
[($ x:id)
|
||||
(quasisyntax/loc pat (bind x #,ty))]
|
||||
[(tuple p ...)
|
||||
(define (matching? t)
|
||||
(syntax-parse t
|
||||
[(~Tuple tt ...)
|
||||
#:when (stx-length=? #'(p ...) #'(tt ...))
|
||||
#t]
|
||||
[_ #f]))
|
||||
(define selected
|
||||
(syntax-parse ty
|
||||
[tt
|
||||
#:when (matching? ty)
|
||||
#'tt]
|
||||
[(~U* (~or (~and tt (~fail #:unless (matching? #'tt)))
|
||||
_) ...)
|
||||
(mk-U- #'(tt ...))]))
|
||||
(define (proj t i)
|
||||
(syntax-parse t
|
||||
[(~Tuple tt ...)
|
||||
(stx-list-ref #'(tt ...) i)]
|
||||
[(~U* tt ...)
|
||||
(mk-U- (stx-map (lambda (x) (proj x i)) #'(tt ...)))]))
|
||||
(define sub-pats
|
||||
(for/list ([pat (in-syntax #'(p ...))]
|
||||
[i (in-naturals)])
|
||||
(elaborate-pattern/with-type pat (proj selected i))))
|
||||
(quasisyntax/loc pat
|
||||
(tuple #,@sub-pats))]
|
||||
[(~constructor-exp ctor p ...)
|
||||
(define tag (ctor-type-tag #'ctor))
|
||||
(define (matching? t)
|
||||
(syntax-parse t
|
||||
[(~constructor-type tag2 tt ...)
|
||||
#:when (equal? tag (syntax-e #'tag2))
|
||||
#:when (stx-length=? #'(p ...) #'(tt ...))
|
||||
#t]
|
||||
[_ #f]))
|
||||
(define selected
|
||||
(syntax-parse ty
|
||||
[tt
|
||||
#:when (matching? ty)
|
||||
#'tt]
|
||||
[(~U* (~or (~and tt (~fail #:unless (matching? #'tt)))
|
||||
_) ...)
|
||||
(mk-U- #'(tt ...))]))
|
||||
(define (proj t i)
|
||||
(syntax-parse t
|
||||
[(~constructor-type _ tt ...)
|
||||
(stx-list-ref #'(tt ...) i)]
|
||||
[(~U* tt ...)
|
||||
(mk-U- (stx-map (lambda (x) (proj x i)) #'(tt ...)))]))
|
||||
(define sub-pats
|
||||
(for/list ([pat (in-syntax #'(p ...))]
|
||||
[i (in-naturals)])
|
||||
(elaborate-pattern/with-type pat (proj selected i))))
|
||||
(quasisyntax/loc pat
|
||||
(ctor #,@sub-pats))]
|
||||
[e:expr
|
||||
#'e])))
|
||||
|
||||
;; TODO - figure out why this needs different list identifiers
|
||||
(define-for-syntax (compile-pattern pat list-binding bind-id-transformer exp-transformer)
|
||||
(define (l-e stx) (local-expand stx 'expression '()))
|
||||
|
|
@ -216,7 +346,7 @@
|
|||
#:datum-literals (tuple discard bind)
|
||||
[(tuple p ...)
|
||||
#`(#,list-binding 'tuple #,@(stx-map loop #'(p ...)))]
|
||||
[(k:kons1 p)
|
||||
#;[(k:kons1 p)
|
||||
#`(#,(kons1->constructor #'k) #,(loop #'p))]
|
||||
[(bind x:id τ:type)
|
||||
(bind-id-transformer #'x)]
|
||||
|
|
|
|||
|
|
@ -47,14 +47,32 @@
|
|||
(struct type-metadata (isec cons) #:transparent)
|
||||
;; (IdTable type-metadata)
|
||||
(define TypeInfo# (make-free-id-table))
|
||||
;; (MutableHashOf Symbol type-metadata)
|
||||
(define TypeInfo#* (make-hash))
|
||||
;; Identifier isect-desc TypeCons -> Void
|
||||
(define (set-type-info! ty-cons isec cons)
|
||||
(free-id-table-set! TypeInfo#
|
||||
ty-cons
|
||||
(type-metadata isec cons)))
|
||||
(define (set-type-info!* ty-cons isec cons)
|
||||
(when (hash-has-key? TypeInfo#* ty-cons)
|
||||
;; TODO
|
||||
#f)
|
||||
(hash-set! TypeInfo#*
|
||||
ty-cons
|
||||
(type-metadata isec cons)))
|
||||
;; Identifier -> Symbol
|
||||
;; XYZ-.*
|
||||
(define (un- id)
|
||||
(define match?
|
||||
(regexp-match #px"^(\\S*)-\\S*$" (symbol->string (syntax-e id))))
|
||||
(string->symbol (second match?)))
|
||||
|
||||
;; Identifier -> (U #f type-metadata)
|
||||
(define (get-type-info ty-cons)
|
||||
(free-id-table-ref TypeInfo# ty-cons #f))
|
||||
(define (get-type-info* ty-cons)
|
||||
(hash-ref TypeInfo#* (un- ty-cons) #f))
|
||||
|
||||
;; Identifier -> (U #f isec-desc)
|
||||
(define (get-type-isec-desc ty-cons)
|
||||
|
|
@ -64,6 +82,14 @@
|
|||
(define (get-type-cons ty-cons)
|
||||
(define result? (get-type-info ty-cons))
|
||||
(and result? (type-metadata-cons result?)))
|
||||
;; Identifier -> (U #f isec-desc)
|
||||
(define (get-type-isec-desc* ty-cons)
|
||||
(define result? (get-type-info* ty-cons))
|
||||
(and result? (type-metadata-isec result?)))
|
||||
;; Identifier -> (U #f TypeCons)
|
||||
(define (get-type-cons* ty-cons)
|
||||
(define result? (get-type-info* ty-cons))
|
||||
(and result? (type-metadata-cons result?)))
|
||||
|
||||
;; a isect-desc describes how a type (constructor) behaves with respect to
|
||||
;; intersection, and is one of
|
||||
|
|
@ -101,13 +127,13 @@
|
|||
;; Identifier -> Bool
|
||||
;; check if the type has a syntax property allowing us to create new instances
|
||||
(define (reassemblable? t)
|
||||
(and (get-type-cons t) #t))
|
||||
(and (get-type-cons* t) #t))
|
||||
|
||||
;; Identifier (Listof Type) -> Type
|
||||
;; Create a new instance of the type with the given arguments
|
||||
;; needs to have the type-cons-key
|
||||
(define (reassemble-type ty args)
|
||||
(define tycons (get-type-cons ty))
|
||||
(define tycons (get-type-cons* ty))
|
||||
(unless tycons
|
||||
(error "expected to find type-cons-key"))
|
||||
(tycons args)))
|
||||
|
|
@ -138,7 +164,8 @@
|
|||
(syntax/loc stx
|
||||
(Name- t (... ...)))]))
|
||||
(begin-for-syntax
|
||||
(set-type-info! #'Name- '#,(attribute desc.val) #'mk-)
|
||||
#;(set-type-info! #'Name- '#,(attribute desc.val) #'mk-)
|
||||
(set-type-info!* 'Name '#,(attribute desc.val) mk-)
|
||||
(define-syntax NamePat
|
||||
(pattern-expander
|
||||
(syntax-parser
|
||||
|
|
@ -204,11 +231,11 @@
|
|||
(define-for-syntax field-prop-name 'fields)
|
||||
(define-type-constructor Actor #:arity = 1)
|
||||
|
||||
(define-product-type Message #:arity = 1)
|
||||
#;(define-product-type Message #:arity = 1)
|
||||
(define-product-type Tuple #:arity >= 0)
|
||||
(define-product-type Observe #:arity = 1)
|
||||
(define-product-type Inbound #:arity = 1)
|
||||
(define-product-type Outbound #:arity = 1)
|
||||
#;(define-product-type Observe #:arity = 1)
|
||||
#;(define-product-type Inbound #:arity = 1)
|
||||
#;(define-product-type Outbound #:arity = 1)
|
||||
(define-container-type AssertionSet #:arity = 1)
|
||||
(define-container-type Patch #:arity = 2)
|
||||
|
||||
|
|
@ -372,7 +399,7 @@
|
|||
(pattern (~seq #:type-constructor TypeCons:id))
|
||||
(pattern (~seq) #:attr TypeCons #f))
|
||||
|
||||
(struct user-ctor (typed-ctor untyped-ctor)
|
||||
(struct user-ctor (typed-ctor untyped-ctor type-tag)
|
||||
#:property prop:procedure
|
||||
(lambda (v stx)
|
||||
(define transformer (user-ctor-typed-ctor v))
|
||||
|
|
@ -406,7 +433,7 @@
|
|||
(struct- StructName (slot ...) #:reflection-name 'Cons #:transparent)
|
||||
(define-syntax (TypeConsExtraInfo stx)
|
||||
(syntax-parse stx
|
||||
[(_ X (... ...)) #'('type-tag 'MakeTypeCons 'GetTypeParams)]))
|
||||
[(_ X (... ...)) #'(#%app- 'type-tag 'MakeTypeCons 'GetTypeParams)]))
|
||||
(define-product-type TypeCons
|
||||
#:arity = #,arity
|
||||
#:extra-info 'TypeConsExtraInfo)
|
||||
|
|
@ -420,7 +447,7 @@
|
|||
[(_ (TypeConsExpander t (... ...)))
|
||||
#'(t (... ...))]))
|
||||
(define-syntax Cons
|
||||
(user-ctor #'Cons- #'StructName))
|
||||
(user-ctor #'Cons- #'StructName 'type-tag))
|
||||
(define-typed-syntax (Cons- e (... ...)) ≫
|
||||
#:fail-unless (= #,arity (stx-length #'(e (... ...)))) "arity mismatch"
|
||||
[⊢ e ≫ e- (⇒ : τ)] (... ...)
|
||||
|
|
@ -462,8 +489,8 @@
|
|||
(define arity (length accs)))
|
||||
(define-syntax (TypeConsExtraInfo stx)
|
||||
(syntax-parse stx
|
||||
[(_ X (... ...)) #'('type-tag 'MakeTypeCons 'GetTypeParams)]))
|
||||
(define-type-constructor TypeCons
|
||||
[(_ X (... ...)) #'(#%app- 'type-tag 'MakeTypeCons 'GetTypeParams)]))
|
||||
(define-product-type TypeCons
|
||||
;; issue: arity needs to parse as an exact-nonnegative-integer
|
||||
;; fix: check arity in MakeTypeCons
|
||||
#:arity >= 0
|
||||
|
|
@ -484,7 +511,7 @@
|
|||
----------------------
|
||||
[⊢ (#%app- orig-struct-info e- (... ...)) (⇒ : (TypeCons τ (... ...)))])
|
||||
(define-syntax ucons
|
||||
(user-ctor #'Cons- #'orig-struct-info)))))]))
|
||||
(user-ctor #'Cons- #'orig-struct-info 'type-tag)))))]))
|
||||
|
||||
(begin-for-syntax
|
||||
(define-syntax ~constructor-extra-info
|
||||
|
|
@ -542,7 +569,12 @@
|
|||
(user-ctor? (syntax-local-value stx (const #f)))))
|
||||
|
||||
(define (untyped-ctor stx)
|
||||
(user-ctor-untyped-ctor (syntax-local-value stx (const #f)))))
|
||||
(user-ctor-untyped-ctor (syntax-local-value stx (const #f))))
|
||||
|
||||
;; requires (ctor-id? stx)
|
||||
;; fetch the type tag
|
||||
(define (ctor-type-tag stx)
|
||||
(user-ctor-type-tag (syntax-local-value stx (const #f)))))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Require & Provide
|
||||
|
|
@ -597,6 +629,11 @@
|
|||
;; Syntax
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
|
||||
(require-struct observe #:as Observe #:from syndicate/actor-lang)
|
||||
(require-struct inbound #:as Inbound #:from syndicate/actor-lang)
|
||||
(require-struct outbound #:as Outbound #:from syndicate/actor-lang)
|
||||
(require-struct message #:as Message #:from syndicate/actor-lang)
|
||||
|
||||
(begin-for-syntax
|
||||
|
||||
;; constructors with arity one
|
||||
|
|
@ -1084,7 +1121,7 @@
|
|||
[(_ e τ:type ...) ≫
|
||||
#:cut
|
||||
[⊢ e ≫ e- ⇒ (~∀ tvs τ_body)]
|
||||
#:fail-unless (stx-andmap instantiable? #'(τ.norm ...) #'tvs)
|
||||
#:fail-unless (stx-andmap instantiable? #'tvs #'(τ.norm ...))
|
||||
"types must be instantiable"
|
||||
#:fail-unless (pure? #'e-) "expression must be pure"
|
||||
--------
|
||||
|
|
@ -1512,3 +1549,14 @@
|
|||
(stx-contains-id? #'ty X)))
|
||||
(stx-map (λ _ irrelevant) Xs)]
|
||||
[_ (stx-map (λ _ invariant) Xs)])))
|
||||
|
||||
#;(begin-for-syntax
|
||||
(define k (sixth (free-id-table-keys TypeInfo#)))
|
||||
(define t
|
||||
(syntax-parse (type-eval #'(Observe (Bind (Tuple))))
|
||||
[(~Any/bvs cons () tt ...)
|
||||
#'cons]))
|
||||
(displayln k)
|
||||
(displayln (hash-ref (syntax-debug-info k) 'bindings))
|
||||
(displayln t)
|
||||
(displayln (hash-ref (syntax-debug-info t) 'bindings)))
|
||||
|
|
|
|||
|
|
@ -360,25 +360,26 @@
|
|||
[⊢ (#%app- x-) (⇒ : τ)])
|
||||
|
||||
;; it would be nice to abstract over these three
|
||||
(define-typed-syntax (observe e:expr) ≫
|
||||
;; TODO - make the constructors
|
||||
#;(define-typed-syntax (observe e:expr) ≫
|
||||
[⊢ e ≫ e- (⇒ : τ)]
|
||||
#:fail-unless (pure? #'e-) "expression not allowed to have effects"
|
||||
---------------------------------------------------------------------------
|
||||
[⊢ (syndicate:observe e-) (⇒ : (Observe τ))])
|
||||
|
||||
(define-typed-syntax (inbound e:expr) ≫
|
||||
#;(define-typed-syntax (inbound e:expr) ≫
|
||||
[⊢ e ≫ e- (⇒ : τ)]
|
||||
#:fail-unless (pure? #'e-) "expression not allowed to have effects"
|
||||
---------------------------------------------------------------------------
|
||||
[⊢ (syndicate:inbound e-) (⇒ : (Inbound τ))])
|
||||
|
||||
(define-typed-syntax (outbound e:expr) ≫
|
||||
#;(define-typed-syntax (outbound e:expr) ≫
|
||||
[⊢ e ≫ e- (⇒ : τ)]
|
||||
#:fail-unless (pure? #'e-) "expression not allowed to have effects"
|
||||
---------------------------------------------------------------------------
|
||||
[⊢ (syndicate:outbound e-) (⇒ : (Outbound τ))])
|
||||
|
||||
(define-typed-syntax (message e:expr) ≫
|
||||
#;(define-typed-syntax (message e:expr) ≫
|
||||
[⊢ e ≫ e- (⇒ : τ)]
|
||||
#:fail-unless (pure? #'e-) "expression must be pure"
|
||||
------------------------------
|
||||
|
|
|
|||
|
|
@ -70,3 +70,24 @@
|
|||
|
||||
(typecheck-fail (inst id5 (→fn Int Int))
|
||||
#:with-msg "types must be instantiable")
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Shorthands for match
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
|
||||
(check-type (match 5
|
||||
[$x:Int (add1 x)])
|
||||
: Int
|
||||
⇒ 6)
|
||||
|
||||
(check-type (match (tuple 3 "hello")
|
||||
[(tuple _ $str:String)
|
||||
str])
|
||||
: String
|
||||
⇒ "hello")
|
||||
|
||||
(check-type (match (tuple 3 "hello")
|
||||
[(tuple _ $str)
|
||||
str])
|
||||
: String
|
||||
⇒ "hello")
|
||||
|
|
|
|||
Loading…
Reference in New Issue