From 5238b749121081a22f460ee4b816deacece9d2d3 Mon Sep 17 00:00:00 2001 From: Sam Caldwell Date: Fri, 17 May 2019 10:35:40 -0400 Subject: [PATCH] move patterns to core expressions --- racket/typed/core-expressions.rkt | 17 ++++++++++++++++- racket/typed/roles.rkt | 13 ------------- 2 files changed, 16 insertions(+), 14 deletions(-) diff --git a/racket/typed/core-expressions.rkt b/racket/typed/core-expressions.rkt index 348d049..dc0c5b4 100644 --- a/racket/typed/core-expressions.rkt +++ b/racket/typed/core-expressions.rkt @@ -1,6 +1,8 @@ #lang turnstile -(provide ann +(provide bind + discard + ann if when unless @@ -16,6 +18,19 @@ (require (only-in "prim.rkt" Bool #%datum)) (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 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt index 43f0932..4f71831 100644 --- a/racket/typed/roles.rkt +++ b/racket/typed/roles.rkt @@ -346,19 +346,6 @@ ------------------------------ [⊢ (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 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;