www

commit cc27c76ab8968d4fbd1118725c15ee207001fa08
parent 9743656778f81529b8bb4cde11496b805be0b6ef
Author: AlexKnauth <alexander@knauth.org>
Date:   Thu, 25 Aug 2016 10:07:00 -0400

rosette2: support applying symbolic function types

Diffstat:
M
turnstile/examples/rosette/rosette2.rkt
 | 
11
++++++++++-
M
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
@@ -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
@@ -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)
+