add rosette-guide-tests; add various forms

- let-symbolic
- vector
- begin

turnstile/examples/rosette/bv.rkt

@@ -1,8 +1,8 @@
-;#lang turnstile
-#lang racket/base
-(require (except-in "../../../turnstile/turnstile.rkt" 
+#lang turnstile
+;#lang racket/base
+#;(require (except-in "../../../turnstile/turnstile.rkt"
           #%module-begin 
-          zero? void error sub1 or and not add1 = - * + boolean? integer? real? positive? string? quote pregexp 
+          zero? void error sub1 or and not add1 = >= <= < >  - * + boolean? integer? real? positive? string? quote pregexp
           make-parameter equal? eq? list ~Any)
          (for-syntax (except-in "../../../turnstile/turnstile.rkt")))
 (extends "rosette2.rkt" ; extends typed rosette

turnstile/examples/rosette/rosette-notes.txt

@@ -11,6 +11,9 @@ TODOs:
 - extend BV type with a size
  - requires BV-size-polymorpism?
 - add Any type?
+ - STARTED 2016-08-26
+- support internal definition contexts
+
 
 2016-08-25 --------------------
 

turnstile/examples/rosette/rosette2.rkt

@@ -36,12 +36,13 @@
              PosInt Zero NegInt Float Bool String [U U*] U*? [case-> case->*] → →?)
     (only-in "../stlc+cons.rkt" Unit List)))
  (only-in "../stlc+union+case.rkt" [~U* ~CU*] [~case-> ~Ccase->] [~→ ~C→])
+ (only-in "../stlc+cons.rkt" [~List ~CList])
  (only-in "../stlc+reco+var.rkt" [define stlc:define] define-primop)
  (only-in "lifted-bitvector-pred.rkt" [bitvector? lifted-bitvector?]))
 
 ;; copied from rosette.rkt
 (define-simple-macro (define-rosette-primop op:id : ty)
-  (begin
+  (begin-
     (require (only-in rosette [op op]))
     (define-primop op : ty)))
 
@@ -53,6 +54,7 @@
     (not (or (Any? t) (U*? t)))))
 
 (define-base-types Any CBV CStx CSymbol)
+(define-type-constructor CVector #:arity > 0)
 
 (define-syntax (CU stx)
   (syntax-parse stx
@@ -157,6 +159,38 @@
           (define-syntax- x (make-rename-transformer (⊢ y : ty.norm))) ...
           (ro:define-symbolic y ... pred-))]])
 
+(define-typed-syntax define-symbolic*
+  [(_ x:id ...+ pred : ty:type) ≫
+   ;; TODO: still unsound
+   [⊢ [pred ≫ pred- ⇐ : (C→ ty.norm Bool)]]
+   #:with (y ...) (generate-temporaries #'(x ...))
+   --------
+   [_ ≻ (begin-
+          (define-syntax- x (make-rename-transformer (⊢ y : ty.norm))) ...
+          (ro:define-symbolic* y ... pred-))]])
+
+;; TODO: support internal definition contexts
+(define-typed-syntax let-symbolic
+  [(_ ([(x:id ...+) pred : ty:type]) e) ≫
+   [⊢ [pred ≫ pred- ⇐ : (C→ ty.norm Bool)]]
+   [([x ≫ x- : ty.norm] ...) ⊢ [e ≫ e- ⇒ τ_out]]
+   --------
+   [⊢ [_ ≫ (ro:let-values
+            ([(x- ...) (ro:let ()
+                         (ro:define-symbolic x ... pred-)
+                         (ro:values x ...))])
+            e-) ⇒ : τ_out]]])
+(define-typed-syntax let-symbolic*
+  [(_ ([(x:id ...+) pred : ty:type]) e) ≫
+   [⊢ [pred ≫ pred- ⇐ : (C→ ty.norm Bool)]]
+   [([x ≫ x- : ty.norm] ...) ⊢ [e ≫ e- ⇒ τ_out]]
+   --------
+   [⊢ [_ ≫ (ro:let-values
+            ([(x- ...) (ro:let ()
+                         (ro:define-symbolic* x ... pred-)
+                         (ro:values x ...))])
+            e-) ⇒ : τ_out]]])
+
 ;; ---------------------------------
 ;; assert, assert-type
 
@@ -190,13 +224,13 @@
   [(_ x:id e) ≫
    --------
    [_ ≻ (stlc:define x e)]]
-  [(_ (f [x : ty] ... (~or → ->) ty_out) e) ≫
+  [(_ (f [x : ty] ... (~or → ->) ty_out) e ...+) ≫
 ;   [⊢ [e ≫ e- ⇒ : ty_e]]
    #:with f- (generate-temporary #'f)
    --------
    [_ ≻ (begin-
           (define-syntax- f (make-rename-transformer (⊢ f- : (C→ ty ... ty_out))))
-          (ro:define f- (stlc:λ ([x : ty] ...) (ann e : ty_out))))]])
+          (ro:define f- (stlc:λ ([x : ty] ...) (ann (begin e ...) : ty_out))))]])
 
 ;; ---------------------------------
 ;; quote
@@ -318,6 +352,30 @@
    --------
    [_ ≻ (let ([x e]) (let* ([x_rst e_rst] ...) e_body))]])
 
+;; --------------------
+;; begin
+
+(define-typed-syntax begin
+  [(begin e_unit ... e) ⇐ : τ_expected ≫
+   [⊢ [e_unit ≫ e_unit- ⇒ : _] ...]
+   [⊢ [e ≫ e- ⇐ : τ_expected]]
+   --------
+   [⊢ [_ ≫ (begin- e_unit- ... e-) ⇐ : _]]]
+  [(begin e_unit ... e) ≫
+   [⊢ [e_unit ≫ e_unit- ⇒ : _] ...]
+   [⊢ [e ≫ e- ⇒ : τ_e]]
+   --------
+   [⊢ [_ ≫ (ro:begin e_unit- ... e-) ⇒ : τ_e]]])
+
+;; ---------------------------------
+;; vector
+
+(define-typed-syntax vector
+  [(_ e ...) ≫
+   [⊢ [e ≫ e- ⇒ : τ] ...]
+   --------
+   [⊢ [_ ≫ (ro:vector e- ...) ⇒ : (CVector τ ...)]]])
+
 ;; ---------------------------------
 ;; Types for built-in operations
 
@@ -432,6 +490,23 @@
 
 (define-rosette-primop bitvector-size : (C→ CBVPred CPosInt))
 
+
+;; ---------------------------------
+;; Logic operators
+
+(define-rosette-primop ! : (C→ Bool Bool))
+
+(define-typed-syntax &&
+  [(_ e ...) ≫
+   [⊢ [e ≫ e- ⇐ : Bool] ...]
+   --------
+   [⊢ [_ ≫ (ro:&& e- ...) ⇒ : Bool]]])
+(define-typed-syntax ||
+  [(_ e ...) ≫
+   [⊢ [e ≫ e- ⇐ : Bool] ...]
+   --------
+   [⊢ [_ ≫ (ro:|| e- ...) ⇒ : Bool]]])
+
 ;; ---------------------------------
 ;; Subtyping
 
@@ -446,6 +521,10 @@
      (Any? t2)
      ((current-type=?) t1 t2)
      (syntax-parse (list t1 t2)
+       [((~CList ty1) (~CList ty2))
+        ((current-sub?) t1 t2)]
+       [((~CVector . tys1) (~CVector . tys2))
+        (stx-andmap (current-sub?) #'tys1 #'tys2)]
        ; 2 U types, subtype = subset
        [((~CU* . ts1) _)
         (for/and ([t (stx->list #'ts1)])

turnstile/examples/tests/rosette/rosette-guide-tests.rkt

@@ -0,0 +1,46 @@
+#lang s-exp "../../rosette/rosette2.rkt"
+(require "../rackunit-typechecking.rkt"
+         "check-type+asserts.rkt")
+
+;; all examples from the Rosette Guide
+
+;; sec 2
+
+(define-symbolic b boolean? : Bool)
+(check-type b : Bool)
+(check-type (boolean? b) : Bool -> #t)
+(check-type (integer? b) : Bool -> #f)
+
+(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 (not b) : Bool -> (! b))
+(check-type (boolean? (not b)) : Bool -> #t)
+
+(define-symbolic* n integer? : Int)
+
+(define (static -> Bool)
+  (let-symbolic ([(x) boolean? : Bool]) x))
+#;(define (static -> Bool)
+ (define-symbolic x boolean? : Bool) ; creates the same constant when evaluated
+ x)
+ 
+(define (dynamic -> Int)
+  (let-symbolic* ([(y) integer? : Int]) y))
+#;(define (dynamic -> Int)
+ (define-symbolic* y integer? : Int) ; creates a different constant when evaluated
+ y)
+ 
+(check-type static : (C→ Bool))
+(check-not-type static : (C→ CBool))
+(check-type dynamic : (C→ Int))
+(check-type dynamic : (C→ Num))
+(check-not-type dynamic : (C→ CInt))
+(check-type (eq? (static) (static)) : Bool -> #t)
+
+(define y0 (dynamic))
+(define y1 (dynamic))
+(check-type (eq? y0 y1) : Bool -> (= y0 y1))