commit 9743656778f81529b8bb4cde11496b805be0b6ef
parent add4a2d7d5b09688350b195a095c5a6243277634
Author: AlexKnauth <alexander@knauth.org>
Date: Thu, 25 Aug 2016 09:53:22 -0400
rosette2: support applying Ccase-> functions
Diffstat:
2 files changed, 123 insertions(+), 18 deletions(-)
diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
@@ -1,10 +1,13 @@
#lang turnstile
-(extends "../stlc.rkt")
+(extends "../stlc.rkt"
+ #:except #%app)
(reuse #%datum #:from "../stlc+union.rkt")
(reuse define-type-alias #:from "../stlc+reco+var.rkt")
(reuse define-named-type-alias #:from "../stlc+union.rkt")
(provide CU U
+ C→
+ Ccase->
CNegInt NegInt
CZero Zero
CPosInt PosInt
@@ -16,11 +19,22 @@
CString ; symbolic string are not supported
)
-(require
+(require
+ (prefix-in ro: rosette)
(only-in "../stlc+union.rkt" define-named-type-alias prune+sort current-sub?)
(prefix-in C (only-in "../stlc+union+case.rkt"
- PosInt Zero NegInt Float Bool String [U U*] U*? case-> →))
- (only-in "../stlc+union+case.rkt" [~U* ~CU*] [~case-> ~Ccase->] [~→ ~C→]))
+ PosInt Zero NegInt Float Bool String [U U*] U*? [case-> case->*] → →?))
+ (only-in "../stlc+union+case.rkt" [~U* ~CU*] [~case-> ~Ccase->] [~→ ~C→])
+ (only-in "../ext-stlc.rkt" define-primop))
+
+;; copied from rosette.rkt
+(define-simple-macro (define-rosette-primop op:id : ty)
+ (begin
+ (require (only-in rosette [op op]))
+ (define-primop op : ty)))
+
+;; ---------------------------------
+;; Concrete and Symbolic union types
(define-syntax (CU stx)
(syntax-parse stx
@@ -45,6 +59,23 @@
(not (U*? t))))
;; ---------------------------------
+;; case-> and Ccase->
+
+;; Ccase-> must check that its subparts are concrete → types
+(define-syntax (Ccase-> stx)
+ (syntax-parse stx
+ [(_ . tys)
+ #:with tys+ (stx-map (current-type-eval) #'tys)
+ #:fail-unless (stx-andmap →? #'tys+)
+ "CU require concrete arguments"
+ #'(Ccase->* . tys+)]))
+
+;; TODO: What should case-> do when given symbolic function
+;; types? Should it transform (case-> (U (C→ τ ...)) ...)
+;; into (U (Ccase-> (C→ τ ...) ...)) ? What makes sense here?
+
+
+;; ---------------------------------
;; Symbolic versions of types
(define-named-type-alias NegInt (U CNegInt))
@@ -69,6 +100,66 @@
(define-symbolic-named-type-alias Num (CU CFloat CInt))
;; ---------------------------------
+;; Function Application
+
+;; copied from rosette.rkt
+(define-typed-syntax app #:export-as #%app
+ [(_ e_fn e_arg ...) ≫
+ [⊢ [e_fn ≫ e_fn- ⇒ : (~C→ ~! τ_in ... τ_out)]]
+ #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
+ (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
+ [⊢ [e_arg ≫ e_arg- ⇐ : τ_in] ...]
+ --------
+ [⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : τ_out]]]
+ [(_ e_fn e_arg ...) ≫
+ [⊢ [e_fn ≫ e_fn- ⇒ : (~Ccase-> ~! . (~and ty_fns ((~C→ . _) ...)))]]
+ [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
+ #:with τ_out
+ (for/first ([ty_f (stx->list #'ty_fns)]
+ #:when (syntax-parse ty_f
+ [(~C→ τ_in ... τ_out)
+ (and (stx-length=? #'(τ_in ...) #'(e_arg ...))
+ (typechecks? #'(τ_arg ...) #'(τ_in ...)))]))
+ (syntax-parse ty_f [(~C→ _ ... t_out) #'t_out]))
+ #:fail-unless (syntax-e #'τ_out)
+ ; use (failing) typechecks? to get err msg
+ (syntax-parse #'ty_fns
+ [((~C→ τ_in ... _) ...)
+ (let* ([τs_expecteds #'((τ_in ...) ...)]
+ [τs_given #'(τ_arg ...)]
+ [expressions #'(e_arg ...)])
+ (format (string-append "type mismatch\n"
+ " expected one of:\n"
+ " ~a\n"
+ " given: ~a\n"
+ " expressions: ~a")
+ (string-join
+ (stx-map
+ (lambda (τs_expected)
+ (string-join (stx-map type->str τs_expected) ", "))
+ τs_expecteds)
+ "\n ")
+ (string-join (stx-map type->str τs_given) ", ")
+ (string-join (map ~s (stx-map syntax->datum expressions)) ", ")))])
+ --------
+ [⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : τ_out]]])
+
+;; ---------------------------------
+;; Types for built-in operations
+
+(define-rosette-primop add1 : (Ccase-> (C→ CNegInt (CU CNegInt CZero))
+ (C→ NegInt (U NegInt Zero))
+ (C→ CZero CPosInt)
+ (C→ Zero PosInt)
+ (C→ CPosInt CPosInt)
+ (C→ PosInt PosInt)
+ (C→ CNat CPosInt)
+ (C→ Nat PosInt)
+ (C→ CInt CInt)
+ (C→ Int Int)))
+
+;; ---------------------------------
+;; Subtyping
(begin-for-syntax
(define (sub? t1 t2)
diff --git a/turnstile/examples/tests/rosette/rosette2-tests.rkt b/turnstile/examples/tests/rosette/rosette2-tests.rkt
@@ -58,6 +58,20 @@
(check-type ((λ ([x : (U Int Bool)]) x) ((λ ([x : (U CInt CBool)]) x) 1)) : (U CInt CBool))
(check-type ((λ ([x : (U CInt CBool)]) x) ((λ ([x : (U Int Bool)]) x) 1)) : (U CInt CBool))
+;; add1 has a case-> type with cases for different subtypes of Int
+;; to preserve some of the type information through the operation
+(check-type (add1 9) : CPosInt -> 10)
+(check-type (add1 0) : CPosInt -> 1)
+(check-type (add1 -1) : (CU CNegInt CZero) -> 0)
+(check-type (add1 -9) : (CU CNegInt CZero) -> -8)
+(check-type (add1 (ann 9 : PosInt)) : PosInt -> 10)
+(check-type (add1 (ann 0 : Zero)) : PosInt -> 1)
+(check-type (add1 (ann 9 : Nat)) : PosInt -> 10)
+(check-type (add1 (ann 0 : Nat)) : PosInt -> 1)
+(check-type (add1 (ann -1 : NegInt)) : (U NegInt Zero) -> 0)
+(check-type (add1 (ann -9 : NegInt)) : (U NegInt Zero) -> -8)
+(check-type (add1 (ann 9 : Int)) : Int -> 10)
+
;; (check-type (sub1 10) : Nat -> 9)
;; (check-type (sub1 0) : NegInt -> -1)
;; (check-type (sub1 -1) : NegInt -> -2)
@@ -167,18 +181,18 @@
;; (if c (bitvector 5) (bitvector 6)))
;; : BV -> (if c (bv 3 5) (bv 3 6)))
-;; ;; case-> subtyping
-;; (check-type ((λ ([f : (→ Int Int)]) (f 10)) add1) : Int -> 11)
-;; (check-type ((λ ([f : (case-> (→ Int Int))]) (f 10)) add1) : Int -> 11)
-;; (check-type ((λ ([f : (case-> (→ Nat Nat)
-;; (→ Int Int))]) (f 10)) add1) : Int -> 11)
-;; (check-not-type ((λ ([f : (case-> (→ Int Int))]) (f 10)) add1) : Nat)
-;; (check-type ((λ ([f : (case-> (→ Nat Nat)
-;; (→ Int Int))]) (f 10)) add1) : Nat -> 11)
-;; (typecheck-fail ((λ ([f : (case-> (→ Zero Zero)
-;; (→ Int Int))]) (f 10)) add1)
-;; #:with-msg
-;; (string-append "expected \\(case-> \\(→ Zero Zero\\) \\(→ Int Int\\)\\), "
-;; "given \\(case-> \\(→ NegInt \\(U NegInt Zero\\)\\) \\(→ Zero PosInt\\) "
-;; "\\(→ PosInt PosInt\\) \\(→ Nat PosInt\\) \\(→ Int Int\\)\\)"))
+;; case-> subtyping
+(check-type ((λ ([f : (C→ Int Int)]) (f 10)) add1) : Int -> 11)
+(check-type ((λ ([f : (Ccase-> (C→ Int Int))]) (f 10)) add1) : Int -> 11)
+(check-type ((λ ([f : (Ccase-> (C→ Nat Nat)
+ (C→ Int Int))]) (f 10)) add1) : Int -> 11)
+(check-not-type ((λ ([f : (Ccase-> (C→ Int Int))]) (f 10)) add1) : Nat)
+(check-type ((λ ([f : (Ccase-> (C→ Nat Nat)
+ (C→ Int Int))]) (f 10)) add1) : Nat -> 11)
+(typecheck-fail ((λ ([f : (Ccase-> (C→ Zero Zero)
+ (C→ Int Int))]) (f 10)) add1)
+ #:with-msg
+ (string-append "expected \\(Ccase-> \\(C→ Zero Zero\\) \\(C→ Int Int\\)\\), "
+ "given \\(Ccase-> .*\\(C→ NegInt \\(U NegInt Zero\\)\\) .*\\(C→ Zero PosInt\\) "
+ ".*\\(C→ PosInt PosInt\\) .*\\(C→ Nat PosInt\\) .*\\(C→ Int Int\\)\\)"))
