From 2e7e6a5d5cf55a3421f1e6d0e485afe285ab4fe0 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Wed, 7 Sep 2016 16:52:03 -0400 Subject: [PATCH] better checks for pred?s in debug --- turnstile/examples/rosette/query/debug.rkt | 12 +++++++++--- turnstile/examples/rosette/rosette-notes.txt | 1 + .../tests/rosette/rosette-guide-sec2-tests.rkt | 4 ++++ 3 files changed, 14 insertions(+), 3 deletions(-) diff --git a/turnstile/examples/rosette/query/debug.rkt b/turnstile/examples/rosette/query/debug.rkt index 7d23e55..a3feed6 100644 --- a/turnstile/examples/rosette/query/debug.rkt +++ b/turnstile/examples/rosette/query/debug.rkt @@ -26,9 +26,15 @@ (t/ro:ann (t/ro:begin e ...) : ty_out))))]]) (define-typed-syntax debug - [(_ (solvable-pred ...+) e) ≫ - [⊢ solvable-pred ≫ solvable-pred- ⇐ (t/ro:C→ t/ro:Nothing t/ro:Bool)] ... + [(_ (pred? ...+) e) ≫ + [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?) (⇒ function? f?)]] ... + #:fail-unless (stx-andmap syntax-e #'(s? ...)) + (format "Must provide a Rosette-solvable type, given ~a." + (syntax->datum #'(pred? ...))) + #:fail-when (stx-ormap syntax-e #'(f? ...)) + (format "Must provide a non-function Rosette type, given ~a." + (syntax->datum #'(pred? ...))) [⊢ [e ≫ e- ⇒ : τ]] -------- - [⊢ [_ ≫ (ro:debug (solvable-pred- ...) e-) ⇒ : t/ro:CSolution]]]) + [⊢ [_ ≫ (ro:debug (pred?- ...) e-) ⇒ : t/ro:CSolution]]]) diff --git a/turnstile/examples/rosette/rosette-notes.txt b/turnstile/examples/rosette/rosette-notes.txt index 37acb7c..66736ce 100644 --- a/turnstile/examples/rosette/rosette-notes.txt +++ b/turnstile/examples/rosette/rosette-notes.txt @@ -84,6 +84,7 @@ TODOs: - orig stx prop confuses distinction between symbolic and non-sym values - use variance information in type constructors? - instead of special-casing individual constructors +- ok to say "Rosette type" in type err msgs? 2016-08-25 -------------------- diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt index 10873f0..b6e74d1 100644 --- a/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt +++ b/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt @@ -103,6 +103,10 @@ (* x (+ x 1) (+ x 2) (+ x 2))) (define ucore (debug [integer?] (same poly factored/d 12))) +(typecheck-fail (debug [positive?] (same poly factored/d 12)) + #:with-msg "Must provide a Rosette-solvable type, given.*positive?") +(typecheck-fail (debug [(~> integer?)] (same poly factored/d 12)) + #:with-msg "Must provide a non-function Rosette type, given.*~> integer?") (check-type ucore : CSolution) ;; TESTING TODO: requires visual inspection (in DrRacket) (check-type (render ucore) : CPict)