split Bool into True and False in stlc+union; add current-bitwidth to rosett2

turnstile/examples/rosette/bv.rkt

@@ -24,7 +24,7 @@
    --------
    [⊢ [_ ≫ (bv:BV) ⇒ : CBVPred]]]
   [(_ e) ≫
-   [⊢ [e ≫ e- ⇒ : CBVPred]]
+   [⊢ [e ≫ e- ⇐ : CBVPred]]
    --------
    [⊢ [_ ≫ (bv:BV e-) ⇒ : CUnit]]])
 

turnstile/examples/rosette/rosette-notes.txt

@@ -60,6 +60,7 @@ TODOs:
 - create version of turnstile that does not provide #%module-begin
   - eg rename existing turnstile to turnstile/lang?
 - remove my-this-syntax stx param
+- add symbolic True and False?
 
 
 2016-08-25 --------------------

turnstile/examples/rosette/rosette2.rkt

@@ -19,7 +19,7 @@
          CInt Int
          CFloat Float
          CNum Num
-         CBool Bool
+         CFalse CTrue CBool Bool
          CString String
          CStx ; symblic Stx not supported
          ;; BV types
@@ -33,7 +33,7 @@
  (prefix-in C
    (combine-in
     (only-in "../stlc+union+case.rkt"
-             PosInt Zero NegInt Float Bool String [U U*] U*? [case-> case->*] → →?)
+             PosInt Zero NegInt Float True False String [U U*] U*? [case-> case->*] → →?)
     (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 ~CListof])
@@ -116,7 +116,6 @@
 (define-named-type-alias Zero (add-predm (U CZero) zero-integer?))
 (define-named-type-alias PosInt (add-predm (U CPosInt) positive-integer?))
 (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 Unit (add-predm (U CUnit) ro:void?))
 (define-named-type-alias (CParamof X) (Ccase-> (C→ X)
@@ -138,6 +137,7 @@
          (define-named-type-alias CName Cτ)
          (define-named-type-alias Name (add-predm (U CName) p?)))]))
 
+(define-symbolic-named-type-alias Bool (CU CFalse CTrue) #:pred ro:boolean?)
 (define-symbolic-named-type-alias Nat (CU CZero CPosInt) #:pred nonnegative-integer?)
 (define-symbolic-named-type-alias Int (CU CNegInt CNat) #:pred ro:integer?)
 (define-symbolic-named-type-alias Num (CU CFloat CInt) #:pred ro:real?)
@@ -489,6 +489,20 @@
 ;; ---------------------------------
 ;; BV Types and Operations
 
+;; this must be a macro in order to support Racket's overloaded set/get
+;; parameter patterns
+(define-typed-syntax current-bitwidth
+  [_:id ≫
+   --------
+   [⊢ [_ ≫ ro:current-bitwidth ⇒ : (CParamof (CU CFalse CPosInt))]]]
+  [(_) ≫
+   --------
+   [⊢ [_ ≫ (ro:current-bitwidth) ⇒ : (CU CFalse CPosInt)]]]
+  [(_ e) ≫
+   [⊢ [e ≫ e- ⇐ : (CU CFalse CPosInt)]]
+   --------
+   [⊢ [_ ≫ (ro:current-bitwidth e-) ⇒ : CUnit]]])
+
 (define-named-type-alias BV (add-predm (U CBV) bv?))
 (define-symbolic-named-type-alias BVPred (C→ BV Bool) #:pred lifted-bitvector?)
 

turnstile/examples/stlc+union.rkt

@@ -1,8 +1,9 @@
 #lang turnstile
 (extends "ext-stlc.rkt" 
- #:except #%app #%datum + add1 sub1 * Int Int? ~Int Float Float? ~Float)
+ #:except #%app #%datum + add1 sub1 *
+          Int Int? ~Int Float Float? ~Float Bool ~Bool Bool?)
 (reuse define-type-alias #:from "stlc+reco+var.rkt")
-(provide Int Num Nat U
+(provide Int Num Nat U Bool
          define-named-type-alias
          (for-syntax current-sub? prune+sort))
 
@@ -33,7 +34,7 @@
            [(_ x ...) (add-orig #'ty stx)]))]))
 
 
-(define-base-types Zero NegInt PosInt Float)
+(define-base-types Zero NegInt PosInt Float False True)
 (define-type-constructor U* #:arity >= 0)
 
 (define-for-syntax (prune+sort tys)
@@ -53,6 +54,9 @@
      (if (= 1 (stx-length #'tys-))
          (stx-car #'tys)
          #'(U* . tys-))]))
+(define-syntax Bool
+  (make-variable-like-transformer
+   (add-orig #'(U False True) #'Bool)))
 (define-syntax Nat
   (make-variable-like-transformer 
    (add-orig #'(U Zero PosInt) #'Nat)))
@@ -68,6 +72,10 @@
 (define-primop sub1 : (→ Int Int))
 
 (define-typed-syntax datum #:export-as #%datum
+  [(_ . b:boolean) ≫
+   #:with ty_out (if (syntax-e #'b) #'True #'False)
+   --------
+   [⊢ [_ ≫ (#%datum- . b) ⇒ : ty_out]]]
   [(_ . n:integer) ≫
    #:with ty_out (let ([m (syntax-e #'n)])
                    (cond [(zero? m) #'Zero]

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

@@ -141,3 +141,4 @@
 (check-type (evaluate (poly x) sol) : Int -> 120)
 (check-type (evaluate (poly y) sol) : Int -> 120)
 
+;; 2.4 Symbolic Reasoning