complete Constant; TODO: check for Constant in synthesize, etc?

turnstile/examples/rosette/rosette2.rkt

@@ -323,6 +323,7 @@
 
 ;; copied from rosette.rkt
 (define-typed-syntax app #:export-as #%app
+  ;; concrete functions
   [(_ e_fn e_arg ...) ≫
    [⊢ [e_fn ≫ e_fn- ⇒ : (~C→ ~! τ_in ... τ_out)]]
    #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn)
@@ -332,6 +333,7 @@
    --------
    ;; TODO: use e_fn/progsrc- (currently causing "cannot use id tainted in macro trans" err)
    [⊢ [_ ≫ (ro:#%app e_fn/progsrc- e_arg- ...) ⇒ : τ_out]]]
+  ;; concrete case->
   [(_ e_fn e_arg ...) ≫
    [⊢ [e_fn ≫ e_fn- ⇒ : (~Ccase-> ~! . (~and ty_fns ((~C→ . _) ...)))]]
    #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn)
@@ -365,6 +367,7 @@
            (string-join (map ~s (stx-map syntax->datum expressions)) ", ")))])
    --------
    [⊢ [_ ≫ (ro:#%app e_fn/progsrc- e_arg- ...) ⇒ : τ_out]]]
+  ;; concrete union functions
   [(_ e_fn e_arg ...) ≫
    [⊢ [e_fn ≫ e_fn- ⇒ : (~CU* τ_f ...)]]
    #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn)
@@ -375,6 +378,7 @@
    ...
    --------
    [⊢ [_ ≫ (ro:#%app e_fn/progsrc- e_arg- ...) ⇒ : (CU τ_out ...)]]]
+  ;; symbolic functions
   [(_ e_fn e_arg ...) ≫
    [⊢ [e_fn ≫ e_fn- ⇒ : (~U* τ_f ...)]]
    #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn)
@@ -384,6 +388,17 @@
     ⊢ [(app f a ...) ≫ _ ⇒ : τ_out]]
    ...
    --------
+   [⊢ [_ ≫ (ro:#%app e_fn/progsrc- e_arg- ...) ⇒ : (U τ_out ...)]]]
+  ;; constant symbolic fns
+  [(_ e_fn e_arg ...) ≫
+   [⊢ [e_fn ≫ e_fn- ⇒ : (~Constant* (~U* τ_f ...))]]
+   #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn)
+   [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
+   #:with (f a ...) (generate-temporaries #'(e_fn e_arg ...))
+   [([f ≫ _ : τ_f] [a ≫ _ : τ_arg] ...)
+    ⊢ [(app f a ...) ≫ _ ⇒ : τ_out]]
+   ...
+   --------
    [⊢ [_ ≫ (ro:#%app e_fn/progsrc- e_arg- ...) ⇒ : (U τ_out ...)]]])
 
 ;; ---------------------------------
@@ -955,7 +970,7 @@
             (mark-functionm
              (add-typeform
               (ro:~> pred?- ...)
-              (C→ ty ...))))
+              (→ ty ...))))
               ⇒ : (C→ Any Bool)]]])
 
 ;; ---------------------------------

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

@@ -9,16 +9,20 @@
 (check-type (boolean? b) : Bool -> #t)
 (check-type (integer? b) : Bool -> #f)
 
-;; TODO: fix these tests
-(check-type (vector b 1) : (CMVectorof (U Bool CPosInt)) -> (vector b 1))
+;; TODO: fix these tests?
+(check-type (vector b 1) : (CMVectorof (U (Constant Bool) CPosInt)) -> (vector b 1))
+;; mut vectors are invariant
+(check-not-type (vector b 1) : (CMVectorof (U Bool CPosInt)))
 (check-not-type (vector b 1) : (CIVectorof (U Bool CPosInt)))
 (check-not-type (vector b 1) : (CMVectorof (CU CBool CPosInt)))
-;; but this is ok
-(check-type (vector b 1) : (CMVectorof (U CBool CPosInt)))
+(check-type (vector b 1) : (CMVectorof (U (Constant Bool) CPosInt)))
 ;; mutable vectors are invariant
+(check-not-type (vector b 1) : (CMVectorof (U CBool CPosInt)))
 (check-not-type (vector b 1) : (CMVectorof (U Bool CInt)))
-(check-type (vector b 1) : (CVectorof (U Bool PosInt)))
+
+(check-type (vector b 1) : (CVectorof (U (Constant Bool) PosInt)))
 ;; vectors are also invariant, because it includes mvectors
+(check-not-type (vector b 1) : (CVectorof (U Bool PosInt)))
 (check-not-type (vector b 1) : (CVectorof (U Bool CInt)))
 (check-not-type (vector b 1) : (CVectorof (U Bool Int)))
 

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

@@ -103,6 +103,8 @@
 (define-symbolic i0 integer?)
 (typecheck-fail (define-symbolic posint1 positive?) 
  #:with-msg "Must provide a Rosette-solvable type, given positive?")
+(typecheck-fail (lambda ([x : (Constant CInt)]) x)
+ #:with-msg "Constant requires a symbolic type")
 (check-type b0 : Bool -> b0)
 (check-type b0 : (Constant Bool) -> b0)
 (check-type i0 : Int -> i0)