add rhs Constant clause in sub?; fix cons to create U

turnstile/examples/rosette/rosette-notes.txt

@@ -1,3 +1,28 @@
+2016-09-08
+
+Typed Rosette tricky subtyping examples
+
+) Both these should be true:
+
+(Constant Int) <: (U (Constant Int) (Constant Bool))
+(Constant Int) <: Int = (U CInt)
+
+However, the first case will not hold unless the (rhs) U subtyping clause
+appears first, but the second case will not hold unless the (lhs) Constant
+subtyping clause appears first.
+
+Bad alternative: put (lhs) Constant clause first, but attach stx prop
+Con: complicated bc must propagate stx prop whenever descending lhs type
+
+Bad alternative: Perform reductions on U of Constants?
+Possibly?: (U (Constant Int) (Constant Bool)) -> (U Int Bool)
+But then, (U (Constant Int)) <: (U Int), which should *not* hold.
+
+Bad alternative: lift Constant out of U
+Con: non-constant values, eg (if b i1 i2) will be recognized as "constant"
+
+Current solution: disallow first case
+
 2016-09-02 --------------------
 
 Is concrete? broken?

turnstile/examples/rosette/rosette2.rkt

@@ -532,10 +532,13 @@
    [⊢ [_ ≫ ro:cons ⇒ : (Ccase-> (C→ Any (CListof Any) (CListof Any))
                                 (C→ Any (Listof Any) (Listof Any)))]]]
   [(_ e1 e2) ≫
-   [⊢ [e2 ≫ e2- ⇒ : (~CListof τ)]]
-   [⊢ [e1 ≫ e1- ⇐ : τ]]
+   [⊢ [e2 ≫ e2- ⇒ : (~CListof τ1)]]
+   [⊢ [e1 ≫ e1- ⇒ : τ2]]
    --------
-   [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (CListof τ)]]]
+   [⊢ [_ ≫ (ro:cons e1- e2-) 
+           ⇒ : #,(if (and (concrete? #'τ1) (concrete? #'τ2))
+                     #'(CListof (CU τ1 τ2))
+                     #'(CListof (U τ1 τ2)))]]]
   [(_ e1 e2) ≫
    [⊢ [e2 ≫ e2- ⇒ : (~U* (~CListof τ) ...)]]
    [⊢ [e1 ≫ e1- ⇒ : τ1]]
@@ -1054,6 +1057,7 @@
 ;(define-rosette-primop exists : (C→ (CListof Any) Bool Bool))
 (define-typed-syntax forall
   [(_ vs body) ≫
+   ;; TODO: allow U of Constants?
    [⊢ [vs ≫ vs- ⇒ : (~CListof ~! ty)]]
    #:fail-unless (Constant*? #'ty)
    (format "Expected list of symbolic constants, given list of ~a" 
@@ -1072,6 +1076,7 @@
 (define-typed-syntax exists
   [(_ vs body) ≫
    [⊢ [vs ≫ vs- ⇒ : (~CListof ~! ty)]]
+   ;; TODO: allow U of Constants?
    #:fail-unless (Constant*? #'ty)
    (format "Expected list of symbolic constants, given list of ~a" 
            (type->str #'ty))
@@ -1167,8 +1172,11 @@
      (Any? t2)
      ((current-type=?) t1 t2)
      (syntax-parse (list t1 t2)
-       [((~Constant* ty1) _)
-        (typecheck? #'ty1 t2)]
+       ;; Constant clause must appear before U, ow (Const Int) <: Int wont hold
+       [((~Constant* ty1) (~Constant* ty2))
+        (typecheck? #'ty1 #'ty2)]
+       [((~Constant* ty) _) 
+        (typecheck? #'ty t2)]
        [((~CListof ty1) (~CListof ty2))
         (typecheck? #'ty1 #'ty2)]
        [((~CList . tys1) (~CList . tys2))

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

@@ -309,3 +309,35 @@
 (check-type+asserts (boolean? (assert-type (if b1 i1 b2) : Bool)) : Bool -> #t (list (not b1)))
 
 (check-type (asserts) : (CListof Bool) -> (list))
+
+;; tests for Constant
+(define-symbolic ci1 integer?)
+(define-symbolic bi1 bi2 boolean?)
+
+(check-type ci1 : (Constant Int))
+(check-type ci1 : Int)
+(check-type ci1 : (Constant Num))
+(check-type ci1 : Num)
+
+;; homogeneous list of constants
+(check-type (list bi1 bi2) : (CList (Constant Bool) (Constant Bool)))
+(check-type (list bi1 bi2) : (CListof (Constant Bool)))
+
+;; heterogeneous list of constants
+(check-type (list ci1 bi1) : (CList (Constant Int) (Constant Bool)))
+(check-type (cons ci1 (cons bi1 (list))) : (CList (Constant Int) (Constant Bool)))
+
+(check-type
+ (lambda ([x : CInt] [lst : (CListof CBool)]) (cons x lst))
+ : (C→ CInt (CListof CBool) (CListof (CU CInt CBool))))
+(check-not-type
+ (lambda ([x : Int] [lst : (CListof Bool)]) (cons x lst))
+ : (C→ Int (CListof Bool) (CListof (CU CInt CBool))))
+(check-type
+ (lambda ([x : Int] [lst : (CListof Bool)]) (cons x lst))
+ : (C→ Int (CListof Bool) (CListof (U Int Bool))))
+
+;; TODO: should these tests hold?
+;(check-type ci1 : (U (Constant Int) (Constant Bool)))
+;(check-type (list ci1 bi1) : (CListof (U (Constant Int) (Constant Bool))))
+;(check-type (cons ci1 (cons bi1 (list))) : (CListof (U (Constant Int) (Constant Bool))))