add if and define-symbolic

turnstile/examples/rosette/rosette-notes.txt

@@ -0,0 +1,18 @@
+2016-08-25 --------------------
+
+** Problem:
+
+The following subtyping relation holds but is potentially unintuitive for a 
+programmer:
+
+(U Int Bool) <: (U CInt Bool)
+
+** Possible Solutions:
+1) leave as is
+2) allow only symbolic arguments to user-facing U constructor
+ - user-facing U constructor expands to U** flattening constructor,
+   which then expands to internal U* constructor
+ - disadvantage: an if expression will expose the internal U** constructor,
+   since if may need to create a symbolic union from potentially concrete types
+
+Choosing #1 for now.

turnstile/examples/rosette/rosette2.rkt

@@ -1,13 +1,13 @@
 #lang turnstile
 (extends "../stlc.rkt"
-  #:except #%app)
+  #: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->
+         C→ →
+         Ccase-> ; TODO: symbolic case-> not supported yet
          CNegInt NegInt
          CZero Zero
          CPosInt PosInt
@@ -16,10 +16,10 @@
          CFloat Float
          CNum Num
          CBool Bool
-         CString ; symbolic string are not supported
+         CString String
          ;; BV types
          CBV BV
-         CBVPred ; symbolic bvpreds are not supported (yet)
+         CBVPred BVPred
          )
 
 (require
@@ -48,11 +48,13 @@
     [(_ . tys)
      #:with tys+ (stx-map (current-type-eval) #'tys)
      #:fail-unless (stx-andmap concrete? #'tys+)
-                   "CU require concrete arguments"
+                   "CU requires concrete types"
      #'(CU* . tys+)]))
 
 ;; internal symbolic union constructor
 (define-type-constructor U* #:arity >= 0)
+
+;; user-facing symbolic U constructor: flattens and prunes
 (define-syntax (U stx)
   (syntax-parse stx
     [(_ . tys)
@@ -90,6 +92,12 @@
 (define-named-type-alias PosInt (U CPosInt))
 (define-named-type-alias Float (U CFloat))
 (define-named-type-alias Bool (U CBool))
+(define-named-type-alias String (U CString))
+
+(define-syntax →
+  (syntax-parser
+    [(_ ty ...+) 
+     (add-orig #'(U (C→ ty ...)) this-syntax)]))
 
 (define-syntax define-symbolic-named-type-alias
   (syntax-parser
@@ -106,6 +114,19 @@
 (define-symbolic-named-type-alias Int (CU CNegInt CNat))
 (define-symbolic-named-type-alias Num (CU CFloat CInt))
 
+;; ---------------------------------
+;; define-symbolic
+
+(define-typed-syntax define-symbolic
+  [(_ x:id ...+ pred : ty:type) ≫
+   ;; TODO: still unsound
+   [⊢ [pred ≫ pred- ⇐ : (→ ty.norm Bool)]]
+   #:with (y ...) (generate-temporaries #'(x ...))
+   --------
+   [_ ≻ (begin-
+          (define-syntax- x (make-rename-transformer (⊢ y : ty.norm))) ...
+          (ro:define-symbolic y ... pred-))]])
+
 ;; ---------------------------------
 ;; Function Application
 
@@ -160,6 +181,28 @@
    --------
    [⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : (U τ_out ...)]]])
 
+;; ---------------------------------
+;; if
+
+(define-typed-syntax if
+  [(_ e_tst e1 e2) ≫
+   [⊢ [e_tst ≫ e_tst- ⇒ : ty_tst]]
+   #:when (concrete? #'ty_tst)
+   [⊢ [e1 ≫ e1- ⇒ : ty1]]
+   [⊢ [e2 ≫ e2- ⇒ : ty2]]
+   #:when (and (concrete? #'ty1) (concrete? #'ty2))
+   --------
+   [⊢ [_ ≫ (ro:if e_tst- e1- e2-) ⇒ : (CU ty1 ty2)]]]
+  [(_ e_tst e1 e2) ≫
+   [⊢ [e_tst ≫ e_tst- ⇒ : _]]
+   [⊢ [e1 ≫ e1- ⇒ : ty1]]
+   [⊢ [e2 ≫ e2- ⇒ : ty2]]
+   --------
+   [⊢ [_ ≫ (ro:if e_tst- e1- e2-) ⇒ : (U ty1 ty2)]]])
+   
+   
+
+
 ;; ---------------------------------
 ;; Types for built-in operations
 
@@ -190,10 +233,16 @@
                                     (C→ CNum CNum CNum)
                                     (C→ Num Num Num)))
 
+;; TODO: fix types of these predicates
+(define-rosette-primop boolean? : (C→ Bool Bool))
+(define-rosette-primop integer? : (C→ Num Bool))
+(define-rosette-primop real? : (C→ Num Bool))
+
 ;; ---------------------------------
 ;; BV Types and Operations
 
 (define-named-type-alias BV (U CBV))
+(define-named-type-alias BVPred (U CBVPred))
 
 (define-rosette-primop bv : (Ccase-> (C→ CInt CBVPred CBV)
                                      (C→ Int CBVPred BV)

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

@@ -85,6 +85,36 @@
 (check-type (+ (ann 1 : PosInt) (ann 10 : PosInt)) : Nat -> 11)
 (check-type (+ (ann -10 : NegInt) (ann 10 : PosInt)) : Int -> 0)
 
+;; if tests
+;; if expr has concrete type only if test and both branches are concrete
+(check-type (if #t 1 #f) : (CU CBool CInt))
+(check-type (if #t 1 #f) : (U CBool CInt))
+(check-type (if #t 1 #f) : (U Bool CInt))
+(check-type (if #t 1 #f) : (U Bool Int))
+(check-type (if #t 1 2) : CInt)
+(check-type (if #t 1 2) : Int)
+(check-type (if #t 1 2) : (CU CInt CBool))
+(check-type (if #t 1 2) : (U Int Bool))
+;; non-bool test
+(check-type (if 1 2 3) : CInt)
+;; else, if expr produces symbolic type
+(define-symbolic b0 boolean? : Bool)
+(define-symbolic i0 integer? : Int)
+(check-type (if b0 1 2) : Int)
+(check-not-type (if b0 1 2) : CInt)
+(check-type (if #t i0 2) : Int)
+(check-not-type (if #t i0 2) : CInt)
+(check-type (if #t 2 i0) : Int)
+(check-not-type (if #t 2 i0) : CInt)
+(check-type (if b0 i0 2) : Int)
+(check-type (if b0 1 #f) : (U CInt CBool))
+(check-type (if b0 1 #f) : (U Int Bool))
+;; slightly unintuitive case: (U Int Bool) <: (U CInt Bool), ok for now (see notes)
+(check-type (if #f i0 #f) : (U CInt CBool))
+(check-type (if #f i0 #f) : (U CInt Bool))
+(check-type (if #f i0 #f) : (U Int Bool))
+(check-type (if #f (+ i0 1) #f) : (U Int Bool))
+
 ;; BVs
 
 (check-type bv : (Ccase-> (C→ CInt CBVPred CBV)