From ed695c66d65488366aa114bfe90b236313e619bd Mon Sep 17 00:00:00 2001 From: Sam Caldwell Date: Mon, 20 May 2019 14:28:38 -0400 Subject: [PATCH] add error form --- racket/typed/core-expressions.rkt | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/racket/typed/core-expressions.rkt b/racket/typed/core-expressions.rkt index 735111b..04ea507 100644 --- a/racket/typed/core-expressions.rkt +++ b/racket/typed/core-expressions.rkt @@ -12,10 +12,11 @@ match tuple select + error (for-syntax (all-defined-out))) (require "core-types.rkt") -(require (only-in "prim.rkt" Bool #%datum)) +(require (only-in "prim.rkt" Bool String #%datum)) (require (postfix-in - racket/match)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -147,7 +148,7 @@ #'((x ...) ...)) -------------------------------------------------------------- [⊢ (match- e- [p- s-] ... - [_ (#%app- error "incomplete pattern match")]) + [_ (#%app- error- "incomplete pattern match")]) (⇒ : (U τ-s ...)) (⇒ ν-ep (eps ... ...)) (⇒ ν-f #,(make-Branch #'((fs ...) ...))) @@ -171,6 +172,13 @@ (define- (tuple-select n t) (#%app- list-ref- t (#%app- add1- n))) +(define-typed-syntax (error msg args ...) ≫ + [⊢ msg ≫ msg- (⇐ : String)] + [⊢ args ≫ args- (⇒ : τ)] ... + #:fail-unless (all-pure? #'(msg- args- ...)) "expressions must be pure" + ---------------------------------------- + [⊢ (#%app- error- msg- args- ...) (⇒ : ⊥)]) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Helpers ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;