add predicates for concrete-only types

typed/rosette.rkt

@@ -1114,9 +1114,7 @@
   [_:id ≫
    --------
    [⊢ [_ ≫ ro:&& ⇒ :
-           (Ccase-> (C→ Bool)
-                    (C→ Bool Bool)
-                    (C→ Bool Bool Bool))]]]
+         (C→* [] [] #:rest (Listof Bool) Bool)]]]
   [(_ e ...) ≫
    [⊢ [e ≫ e- ⇐ : Bool] ...]
    --------
@@ -1125,9 +1123,7 @@
   [_:id ≫
    --------
    [⊢ [_ ≫ ro:|| ⇒ :
-           (Ccase-> (C→ Bool)
-                    (C→ Bool Bool)
-                    (C→ Bool Bool Bool))]]]
+           (C→* [] [] #:rest (Listof Bool) Bool)]]]
   [(_ e ...) ≫
    [⊢ [e ≫ e- ⇐ : Bool] ...]
    --------

typed/rosette/base-forms.rkt

@@ -537,7 +537,7 @@
    --------
    [⊢ (ro:apply f- lst-) ⇒ τ_out]]
   [(_ f:expr lst:expr) ≫
-   [⊢ f ≫ f- ⇒ (~Ccase-> τ_f ...)]
+   [⊢ f ≫ f- ⇒ (~Ccase-> ~! τ_f ...)]
    [⊢ lst ≫ lst- ⇒ τ_lst]
    #:with τ_out
    (for/or ([τ_f (in-list (stx->list #'[τ_f ...]))])

typed/rosette/concrete-predicate.rkt

@@ -0,0 +1,47 @@
+#lang racket/base
+
+(provide concrete-boolean?
+         concrete-integer?
+         concrete-zero-integer?
+         concrete-positive-integer?
+         concrete-negative-integer?
+         concrete-nonnegative-integer?
+         concrete-real?
+         concrete-positive-real?
+         concrete-negative-real?
+         concrete-nonnegative-real?
+         )
+
+(require (only-in racket/base
+                  [boolean? concrete-boolean?]
+                  [integer? concrete-integer?]
+                  [real? concrete-real?]))
+
+;; concrete-zero-integer? : Any -> Bool
+(define (concrete-zero-integer? x)
+  (and (concrete-integer? x) (zero? x)))
+
+;; concrete-positive-integer? : Any -> Bool
+(define (concrete-positive-integer? x)
+  (and (concrete-integer? x) (positive? x)))
+
+;; concrete-negative-integer? : Any -> Bool
+(define (concrete-negative-integer? x)
+  (and (concrete-integer? x) (negative? x)))
+
+;; concrete-nonnegative-integer? : Any -> Bool
+(define (concrete-nonnegative-integer? x)
+  (and (concrete-integer? x) (not (negative? x))))
+
+;; concrete-positive-real? : Any -> Bool
+(define (concrete-positive-real? x)
+  (and (concrete-real? x) (positive? x)))
+
+;; concrete-negative-real? : Any -> Bool
+(define (concrete-negative-real? x)
+  (and (concrete-real? x) (negative? x)))
+
+;; concrete-nonnegative-real? : Any -> Bool
+(define (concrete-nonnegative-real? x)
+  (and (concrete-real? x) (not (negative? x))))
+

typed/rosette/types.rkt

@@ -88,7 +88,8 @@
            [List CListof] [~List ~CListof])
          (prefix-in ro: rosette)
          (prefix-in ro: rosette/lib/synthax)
-         (rename-in "../rosette-util.rkt" [bitvector? lifted-bitvector?]))
+         (rename-in "../rosette-util.rkt" [bitvector? lifted-bitvector?])
+         "concrete-predicate.rkt")
 
 ;; ---------------------------------
 ;; Concrete and Symbolic union types
@@ -142,7 +143,7 @@
      ;; canonicalize by expanding to U*, with only (sorted and pruned) leaf tys
      #:with ((~or (~U* ty1- ...) (~CU* ty2- ...) ty3-) ...) (stx-map (current-type-eval) #'tys)
      #:with tys- (prune+sort #'(ty1- ... ... ty2- ... ... ty3- ...))
-     #'(U* . tys-)]))
+     (syntax/loc this-syntax (U* . tys-))]))
 
 ;; user-facing symbolic Term constructor: check solvable
 (define-syntax-parser Term
@@ -279,7 +280,7 @@
      #:with tys+ (stx-map (current-type-eval) #'tys)
      #:fail-unless (stx-andmap concrete-function-type? #'tys+)
                    "Ccase-> require concrete function types"
-     #'(Ccase->* . tys+)]))
+     (syntax/loc this-syntax (Ccase->* . tys+))]))
 
 
 ;; TODO: What should case-> do when given symbolic function
@@ -322,11 +323,11 @@
 ;; ---------------------------------
 ;; Concrete types
 
-(define-named-type-alias CBool (CU CFalse CTrue))
+(define-named-type-alias CBool (add-predm (CU CFalse CTrue) concrete-boolean?))
 
-(define-named-type-alias CNat (CU CZero CPosInt))
-(define-named-type-alias CInt (CU CNegInt CNat))
-(define-named-type-alias CNum (CU CFloat CInt))
+(define-named-type-alias CNat (add-predm (CU CZero CPosInt) concrete-nonnegative-integer?))
+(define-named-type-alias CInt (add-predm (CU CNegInt CNat) concrete-integer?))
+(define-named-type-alias CNum (add-predm (CU CFloat CInt) concrete-real?))
 
 (begin-for-syntax
   (define (concrete-type-solvable? τ)