From 2a6167e4d0d2bc78c8378f96b1fe882e53c06b63 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Tue, 30 Aug 2016 11:41:40 -0400 Subject: [PATCH] add immutable vectors; add "of" suffix to data structure type constructors --- turnstile/examples/rosette/bv.rkt | 2 +- turnstile/examples/rosette/rosette2.rkt | 41 ++++++++++++------- turnstile/examples/tests/rosette/bv-tests.rkt | 2 +- .../tests/rosette/check-type+asserts.rkt | 4 +- .../tests/rosette/rosette-guide-tests.rkt | 18 +++++--- .../examples/tests/rosette/rosette2-tests.rkt | 2 +- 6 files changed, 44 insertions(+), 25 deletions(-) diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt index 2c8fe8b..bd783d5 100644 --- a/turnstile/examples/rosette/bv.rkt +++ b/turnstile/examples/rosette/bv.rkt @@ -19,7 +19,7 @@ (define-typed-syntax current-bvpred [c-bvpred:id ≫ -------- - [⊢ [_ ≫ bv:BV ⇒ : (CParam CBVPred)]]] + [⊢ [_ ≫ bv:BV ⇒ : (CParamof CBVPred)]]] [(_) ≫ -------- [⊢ [_ ≫ (bv:BV) ⇒ : CBVPred]]] diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt index 4fa193f..51306c5 100644 --- a/turnstile/examples/rosette/rosette2.rkt +++ b/turnstile/examples/rosette/rosette2.rkt @@ -10,7 +10,7 @@ CU U C→ → (for-syntax ~C→ C→?) Ccase-> ; TODO: symbolic case-> not supported yet - CList CParam ; TODO: symbolic Param not supported yet + CListof CVectorof CParamof ; TODO: symbolic Param not supported yet CUnit Unit CNegInt NegInt CZero Zero @@ -34,9 +34,9 @@ (combine-in (only-in "../stlc+union+case.rkt" PosInt Zero NegInt Float Bool String [U U*] U*? [case-> case->*] → →?) - (only-in "../stlc+cons.rkt" Unit List))) + (only-in "../stlc+cons.rkt" Unit [List Listof]))) (only-in "../stlc+union+case.rkt" [~U* ~CU*] [~case-> ~Ccase->] [~→ ~C→]) - (only-in "../stlc+cons.rkt" [~List ~CList]) + (only-in "../stlc+cons.rkt" [~List ~CListof]) (only-in "../stlc+reco+var.rkt" [define stlc:define] define-primop) (rename-in "rosette-util.rkt" [bitvector? lifted-bitvector?])) @@ -54,7 +54,12 @@ (not (or (Any? t) (U*? t))))) (define-base-types Any CBV CStx CSymbol) -(define-type-constructor CVector #:arity > 0) +;; CVectorof includes all vectors +;; CIVectorof includes only immutable vectors +;; CMVectorof includes only mutable vectors +(define-type-constructor CIVectorof #:arity = 1) +(define-type-constructor CMVectorof #:arity = 1) +(define-named-type-alias (CVectorof X) (CU (CIVectorof X) (CMVectorof X))) (define-syntax (CU stx) (syntax-parse stx @@ -114,8 +119,8 @@ (define-named-type-alias Bool (add-predm (U CBool) ro:boolean?)) (define-named-type-alias String (U CString)) (define-named-type-alias Unit (add-predm (U CUnit) ro:void?)) -(define-named-type-alias (CParam X) (Ccase-> (C→ X) - (C→ X CUnit))) +(define-named-type-alias (CParamof X) (Ccase-> (C→ X) + (C→ X CUnit))) (define-syntax → (syntax-parser @@ -232,7 +237,7 @@ [⊢ [_ ≫ (quote- x) ⇒ : CSymbol]]] [(_ (x:id ...)) ≫ -------- - [⊢ [_ ≫ (quote- (x ...)) ⇒ : (CList CSymbol)]]]) + [⊢ [_ ≫ (quote- (x ...)) ⇒ : (CListof CSymbol)]]]) ;; --------------------------------- ;; Function Application @@ -365,8 +370,16 @@ [(_ e ...) ≫ [⊢ [e ≫ e- ⇒ : τ] ...] -------- - [⊢ [_ ≫ (ro:vector e- ...) ⇒ : (CVector τ ...)]]]) - + [⊢ [_ ≫ (ro:vector e- ...) ⇒ : #,(if (stx-andmap concrete? #'(τ ...)) + #'(CMVectorof (CU τ ...)) + #'(CMVectorof (U τ ...)))]]]) +(define-typed-syntax vector-immutable + [(_ e ...) ≫ + [⊢ [e ≫ e- ⇒ : τ] ...] + -------- + [⊢ [_ ≫ (ro:vector-immutable e- ...) ⇒ : (if (stx-andmap concrete? #'(τ ...)) + #'(CIVectorof (CU τ ...)) + #'(CIVectorof (U τ ...)))]]]) ;; --------------------------------- ;; Types for built-in operations @@ -424,7 +437,7 @@ (C→ Num Bool))) ;; rosette-specific -(define-rosette-primop asserts : (C→ (CList Bool))) +(define-rosette-primop asserts : (C→ (CListof Bool))) (define-rosette-primop clear-asserts! : (C→ CUnit)) ;; --------------------------------- @@ -513,11 +526,11 @@ (Any? t2) ((current-type=?) t1 t2) (syntax-parse (list t1 t2) - [((~CList ty1) (~CList ty2)) + [((~CListof ty1) (~CListof ty2)) ((current-sub?) #'ty1 #'ty2)] - ;; vectors are mutable and thus invariant - [((~CVector . tys1) (~CVector . tys2)) - (stx-andmap (current-type=?) #'tys1 #'tys2)] + ;; vectors, only immutable vectors are invariant + [((~CIVectorof . tys1) (~CIVectorof . tys2)) + (stx-andmap (current-sub?) #'tys1 #'tys2)] ; 2 U types, subtype = subset [((~CU* . ts1) _) (for/and ([t (stx->list #'ts1)]) diff --git a/turnstile/examples/tests/rosette/bv-tests.rkt b/turnstile/examples/tests/rosette/bv-tests.rkt index 789c1bc..186ea43 100644 --- a/turnstile/examples/tests/rosette/bv-tests.rkt +++ b/turnstile/examples/tests/rosette/bv-tests.rkt @@ -1,7 +1,7 @@ #lang s-exp "../../rosette/bv.rkt" (require "../rackunit-typechecking.rkt") -(check-type current-bvpred : (CParam CBVPred)) +(check-type current-bvpred : (CParamof CBVPred)) (check-type (current-bvpred) : BVPred -> (bitvector 4)) (check-type (current-bvpred (bitvector 5)) : CUnit -> (void)) (check-type (current-bvpred) : BVPred -> (bitvector 5)) diff --git a/turnstile/examples/tests/rosette/check-type+asserts.rkt b/turnstile/examples/tests/rosette/check-type+asserts.rkt index 23f7c58..12b160f 100644 --- a/turnstile/examples/tests/rosette/check-type+asserts.rkt +++ b/turnstile/examples/tests/rosette/check-type+asserts.rkt @@ -4,7 +4,7 @@ (require turnstile/turnstile "check-asserts.rkt" - (only-in "../../rosette/rosette2.rkt" CList Bool CUnit)) + (only-in "../../rosette/rosette2.rkt" CListof Bool CUnit)) (define-typed-syntax check-type+asserts #:datum-literals (: ->) [(_ e : τ-expected -> v asserts) ≫ @@ -12,6 +12,6 @@ -------- [⊢ [_ ≫ (check-equal?/asserts e- (add-expected v τ-expected) - (add-expected asserts (CList Bool))) + (add-expected asserts (CListof Bool))) ⇒ : CUnit]]]) diff --git a/turnstile/examples/tests/rosette/rosette-guide-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-tests.rkt index 7cbafdd..c4d2c8e 100644 --- a/turnstile/examples/tests/rosette/rosette-guide-tests.rkt +++ b/turnstile/examples/tests/rosette/rosette-guide-tests.rkt @@ -12,11 +12,17 @@ (check-type (integer? b) : Bool -> #f) ;; TODO: fix these tests -(check-type (vector b 1) : (CVector Bool CPosInt) -> (vector b 1)) -;; (check-not-type (vector b 1) : (CVector CBool CPosInt)) -;; (check-type (vector b 1) : (CVector Bool PosInt)) -;; (check-type (vector b 1) : (CVector Bool CInt)) -;; (check-type (vector b 1) : (CVector Bool Int)) +(check-type (vector b 1) : (CMVectorof (U Bool CPosInt)) -> (vector b 1)) +(check-not-type (vector b 1) : (CIVectorof (U Bool CPosInt))) +(check-not-type (vector b 1) : (CMVectorof (CU CBool CPosInt))) +;; but this is ok +(check-type (vector b 1) : (CMVectorof (U CBool CPosInt))) +;; mutable vectors are invariant +(check-not-type (vector b 1) : (CMVectorof (U Bool CInt))) +(check-type (vector b 1) : (CVectorof (U Bool PosInt))) +;; vectors are also invariant, because it includes mvectors +(check-not-type (vector b 1) : (CVectorof (U Bool CInt))) +(check-not-type (vector b 1) : (CVectorof (U Bool Int))) (check-type (not b) : Bool -> (! b)) (check-type (boolean? (not b)) : Bool -> #t) @@ -59,7 +65,7 @@ (check-type+asserts (assert (not b)) : Unit -> (void) (list (! b) #f)) (check-type (clear-asserts!) : Unit -> (void)) -(check-type (asserts) : (CList Bool) -> (list)) +(check-type (asserts) : (CListof Bool) -> (list)) ;; sec 2.3 ;; (define (poly [x : Int] -> Int) diff --git a/turnstile/examples/tests/rosette/rosette2-tests.rkt b/turnstile/examples/tests/rosette/rosette2-tests.rkt index eec8e87..efedb3a 100644 --- a/turnstile/examples/tests/rosette/rosette2-tests.rkt +++ b/turnstile/examples/tests/rosette/rosette2-tests.rkt @@ -300,4 +300,4 @@ (check-type+asserts (boolean? (assert-type (if b1 i1 b2) : Int)) : Bool -> #f (list b1)) (check-type+asserts (boolean? (assert-type (if b1 i1 b2) : Bool)) : Bool -> #t (list (not b1))) -(check-type (asserts) : (CList Bool) -> (list)) +(check-type (asserts) : (CListof Bool) -> (list))