move patterns to core expressions
This commit is contained in:
parent
3def83502a
commit
5238b74912
|
@ -1,6 +1,8 @@
|
||||||
#lang turnstile
|
#lang turnstile
|
||||||
|
|
||||||
(provide ann
|
(provide bind
|
||||||
|
discard
|
||||||
|
ann
|
||||||
if
|
if
|
||||||
when
|
when
|
||||||
unless
|
unless
|
||||||
|
@ -16,6 +18,19 @@
|
||||||
(require (only-in "prim.rkt" Bool #%datum))
|
(require (only-in "prim.rkt" Bool #%datum))
|
||||||
(require (postfix-in - racket/match))
|
(require (postfix-in - racket/match))
|
||||||
|
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
;; Patterns
|
||||||
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
||||||
|
(define-typed-syntax (bind x:id τ:type) ≫
|
||||||
|
----------------------------------------
|
||||||
|
[⊢ (error- 'bind "escaped") (⇒ : (Bind τ))])
|
||||||
|
|
||||||
|
(define-typed-syntax discard
|
||||||
|
[_ ≫
|
||||||
|
--------------------
|
||||||
|
[⊢ (error- 'discard "escaped") (⇒ : Discard)]])
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
;; Core-ish forms
|
;; Core-ish forms
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
|
@ -346,19 +346,6 @@
|
||||||
------------------------------
|
------------------------------
|
||||||
[⊢ (syndicate:message e-) (⇒ : (Message τ))])
|
[⊢ (syndicate:message e-) (⇒ : (Message τ))])
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
||||||
;; Patterns
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
||||||
|
|
||||||
(define-typed-syntax (bind x:id τ:type) ≫
|
|
||||||
----------------------------------------
|
|
||||||
[⊢ (error- 'bind "escaped") (⇒ : (Bind τ))])
|
|
||||||
|
|
||||||
(define-typed-syntax discard
|
|
||||||
[_ ≫
|
|
||||||
--------------------
|
|
||||||
[⊢ (error- 'discard "escaped") (⇒ : Discard)]])
|
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
;; Ground Dataspace
|
;; Ground Dataspace
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
Loading…
Reference in New Issue