From 4f400b5e0a3afd97d04de3bf18aa2f5618441a9c Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Mon, 31 Oct 2016 12:28:18 -0400 Subject: [PATCH] refine if: create sym val only when test is sym bool --- turnstile/examples/rosette/rosette2.rkt | 6 +++++- turnstile/examples/tests/rosette/rosette2-tests.rkt | 1 + 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt index 97c6a1d..f7ae136 100644 --- a/turnstile/examples/rosette/rosette2.rkt +++ b/turnstile/examples/rosette/rosette2.rkt @@ -491,10 +491,14 @@ ;; --------------------------------- ;; if +;; TODO: this is not precise enough +;; specifically, a symbolic non-bool should produce a concrete val (define-typed-syntax if [(_ e_tst e1 e2) ≫ [⊢ [e_tst ≫ e_tst- ⇒ : ty_tst]] - #:when (concrete? #'ty_tst) + #:when (or (concrete? #'ty_tst) ; either concrete + ; or non-bool symbolic + (not (typecheck? #'ty_tst ((current-type-eval) #'Bool)))) [⊢ [e1 ≫ e1- ⇒ : ty1]] [⊢ [e2 ≫ e2- ⇒ : ty2]] #:when (and (concrete? #'ty1) (concrete? #'ty2)) diff --git a/turnstile/examples/tests/rosette/rosette2-tests.rkt b/turnstile/examples/tests/rosette/rosette2-tests.rkt index de61ffd..5424206 100644 --- a/turnstile/examples/tests/rosette/rosette2-tests.rkt +++ b/turnstile/examples/tests/rosette/rosette2-tests.rkt @@ -107,6 +107,7 @@ #:with-msg "Constant requires a symbolic type") (check-type b0 : Bool -> b0) (check-type b0 : (Constant Bool) -> b0) +(check-not-type b0 : CBool) (check-type i0 : Int -> i0) (check-type i0 : (Constant Int) -> i0) (check-type (if b0 1 2) : Int)