From cc27c76ab8968d4fbd1118725c15ee207001fa08 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Thu, 25 Aug 2016 10:07:00 -0400 Subject: [PATCH] rosette2: support applying symbolic function types --- turnstile/examples/rosette/rosette2.rkt | 11 ++++++++++- turnstile/examples/tests/rosette/rosette2-tests.rkt | 6 ++++++ 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt index cbd32f9..e982236 100644 --- a/turnstile/examples/rosette/rosette2.rkt +++ b/turnstile/examples/rosette/rosette2.rkt @@ -142,7 +142,16 @@ (string-join (stx-map type->str τs_given) ", ") (string-join (map ~s (stx-map syntax->datum expressions)) ", ")))]) -------- - [⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : τ_out]]]) + [⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : τ_out]]] + [(_ e_fn e_arg ...) ≫ + [⊢ [e_fn ≫ e_fn- ⇒ : (~U* τ_f ...)]] + [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...] + #:with (f a ...) (generate-temporaries #'(e_fn e_arg ...)) + [([f ≫ _ : τ_f] [a ≫ _ : τ_arg] ...) + ⊢ [(app f a ...) ≫ _ ⇒ : τ_out]] + ... + -------- + [⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : (U τ_out ...)]]]) ;; --------------------------------- ;; Types for built-in operations diff --git a/turnstile/examples/tests/rosette/rosette2-tests.rkt b/turnstile/examples/tests/rosette/rosette2-tests.rkt index 77e87e0..e1a7bc0 100644 --- a/turnstile/examples/tests/rosette/rosette2-tests.rkt +++ b/turnstile/examples/tests/rosette/rosette2-tests.rkt @@ -196,3 +196,9 @@ "given \\(Ccase-> .*\\(C→ NegInt \\(U NegInt Zero\\)\\) .*\\(C→ Zero PosInt\\) " ".*\\(C→ PosInt PosInt\\) .*\\(C→ Nat PosInt\\) .*\\(C→ Int Int\\)\\)")) +;; applying symbolic function types +(check-type ((λ ([f : (U (C→ CInt CInt))]) (f 10)) add1) : Int -> 11) +;; it's either (→ CInt CInt) or (→ CInt CBool), but not both, so +;; add1 can have this type even though it never returns a boolean +(check-type ((λ ([f : (U (C→ CInt CInt) (C→ CInt CBool))]) (f 10)) add1) : (U Int Bool) -> 11) +