add some forms required by bv sdsl: Param, let, define (no tests yet)

turnstile/examples/rosette/rosette-notes.txt

@@ -2,8 +2,15 @@
 
 TODOs:
 - add pred properties to types 
-  and use it to validate given pred in define-symbolic
+ - use it to validate given pred in define-symbolic
+ - STARTED 2016-08-25
 - implement assert-type, which adds to the assertion store
+ - DONE 2016-08-25
+- add polymorphism
+ - regular polymorphism
+- extend BV type with a size
+ - requires BV-size-polymorpism?
+- add Any type?
 
 2016-08-25 --------------------
 

turnstile/examples/rosette/rosette2.rkt

@@ -4,7 +4,7 @@
 (reuse #%datum #:from "../stlc+union.rkt")
 (reuse define-type-alias #:from "../stlc+reco+var.rkt")
 (reuse define-named-type-alias #:from "../stlc+union.rkt")
-(reuse void Unit List list #:from "../stlc+cons.rkt")
+(reuse void Unit List define list #:from "../stlc+cons.rkt")
 
 (provide CU U
          C→ →
@@ -106,6 +106,8 @@
 (define-named-type-alias Float (U CFloat))
 (define-named-type-alias Bool (add-predm (U CBool) ro:boolean?))
 (define-named-type-alias String (U CString))
+(define-named-type-alias (Param X) (Ccase-> (C→ X)
+                                            (C→ X Unit)))
 
 (define-syntax →
   (syntax-parser
@@ -151,6 +153,14 @@
    --------
    [⊢ [_ ≫ (ro:let ([x e-]) (ro:assert (ro:#%app pred x)) x) ⇒ : ty.norm]]])  
 
+
+;; ---------------------------------
+;; Racket forms
+
+;; TODO: many of these implementations are copied code, with just the macro
+;; output changed to use the ro: version. 
+;; Is there a way to abstract this? macro mixin?
+
 ;; ---------------------------------
 ;; Function Application
 
@@ -233,7 +243,32 @@
    --------
    [⊢ [_ ≫ (ro:if e_tst- e1- e2-) ⇒ : (U ty1 ty2)]]])
    
-   
+;; ---------------------------------
+;; let, etc (copied from ext-stlc.rkt)
+
+(define-typed-syntax let
+  [(let ([x e] ...) e_body) ⇐ : τ_expected ≫
+   [⊢ [e ≫ e- ⇒ : τ_x] ...]
+   [() ([x ≫ x- : τ_x] ...) ⊢ [e_body ≫ e_body- ⇐ : τ_expected]]
+   --------
+   [⊢ [_ ≫ (ro:let ([x- e-] ...) e_body-) ⇐ : _]]]
+  [(let ([x e] ...) e_body) ≫
+   [⊢ [e ≫ e- ⇒ : τ_x] ...]
+   [() ([x ≫ x- : τ_x] ...) ⊢ [e_body ≫ e_body- ⇒ : τ_body]]
+   --------
+   [⊢ [_ ≫ (ro:let ([x- e-] ...) e_body-) ⇒ : τ_body]]])
+
+; dont need to manually transfer expected type
+; result template automatically propagates properties
+; - only need to transfer expected type when local expanding an expression
+;   - see let/tc
+(define-typed-syntax let*
+  [(let* () e_body) ≫
+   --------
+   [_ ≻ e_body]]
+  [(let* ([x e] [x_rst e_rst] ...) e_body) ≫
+   --------
+   [_ ≻ (let ([x e]) (let* ([x_rst e_rst] ...) e_body))]])
 
 
 ;; ---------------------------------
@@ -286,9 +321,7 @@
 (define-symbolic-named-type-alias BVPred (C→ BV Bool) #:pred ro:bitvector?)
 
 (define-rosette-primop bv : (Ccase-> (C→ CInt CBVPred CBV)
-                                     (C→ Int CBVPred BV)
-                                     (C→ CInt CPosInt CBV)
-                                     (C→ Int CPosInt BV)))
+                                     (C→ CInt CPosInt CBV)))
 (define-rosette-primop bv? : (C→ BV Bool))
 (define-rosette-primop bitvector : (C→ CPosInt CBVPred))
 (define-rosette-primop bitvector? : (C→ BVPred Bool))

turnstile/examples/stlc+union.rkt

@@ -26,7 +26,12 @@
   (syntax-parser
     [(define-named-type-alias Name:id τ:type)
      #'(define-syntax Name
-         (make-variable-like-transformer (add-orig #'τ #'Name)))]))
+         (make-variable-like-transformer (add-orig #'τ #'Name)))]
+    [(define-named-type-alias (f:id x:id ...) ty) ; dont expand yet
+     #'(define-syntax (f stx)
+         (syntax-parse stx
+           [(_ x ...) (add-orig #'ty stx)]))]))
+
 
 (define-base-types Zero NegInt PosInt Float)
 (define-type-constructor U* #:arity > 0)

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

@@ -118,14 +118,12 @@
 ;; BVs
 
 (check-type bv : (Ccase-> (C→ CInt CBVPred CBV)
-                          (C→ Int CBVPred BV)
-                          (C→ CInt CPosInt CBV)
-                          (C→ Int CPosInt BV)))
+                          (C→ CInt CPosInt CBV)))
 (typecheck-fail (bv "1" 2) #:with-msg "expected.*Int.*given.*String")
 (check-type (bv 1 2) : CBV -> (bv 1 (bitvector 2)))
 (check-type (bv 1 (bitvector 2)) : CBV -> (bv 1 (bitvector 2)))
-(check-type (bv (ann 1 : Int) 2) : BV -> (bv 1 (bitvector 2)))
-(check-type (bv (ann 1 : Int) (bitvector 2)) : BV -> (bv 1 (bitvector 2)))
+(typecheck-fail (bv (ann 1 : Int) 2) #:with-msg "expected.*CInt")
+(typecheck-fail (bv (ann 1 : Int) (bitvector 2)) #:with-msg "expected.*CInt")
 
 (typecheck-fail (bv 0 0) #:with-msg "expected.*PosInt.*given.*Zero")
 (check-type bitvector : (C→ CPosInt CBVPred))