start using expand/ro; fix define-synthax, woo!

2016-11-22 15:37:44 -05:00 · 2016-11-22 15:37:44 -05:00 · 13ef7c8b72
commit 13ef7c8b72
parent 8949a9fbf1
9 changed files with 122 additions and 85 deletions
--- a/turnstile/examples/rosette/lib/synthax3.rkt
+++ b/turnstile/examples/rosette/lib/synthax3.rkt
@ -2,22 +2,22 @@
 (require
 (prefix-in 
  t/ro:
-  (only-in "../rosette3.rkt" U Int Bool C→ CSolution Unit CSyntax CListof))
+  (only-in "../rosette3.rkt" U Int C→ CSolution Unit CSyntax CListof expand/ro))
 (prefix-in ro: rosette/lib/synthax))

 (provide (typed-out [print-forms : (t/ro:C→ t/ro:CSolution t/ro:Unit)])
         ??)

-(provide generate-forms choose)
+(provide generate-forms choose define-synthax)

 (define-typed-syntax ??
  [(qq) ≫
   #:with ??/progsrc (datum->syntax #'here 'ro:?? #'qq)
   --------
-   [⊢ [_ ≫ (??/progsrc) ⇒ : t/ro:Int]]]
+   [⊢ (??/progsrc) ⇒ t/ro:Int]]
  [(qq pred?) ≫
   #:with ??/progsrc (datum->syntax #'here 'ro:?? #'qq)
-   [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?) (⇒ function? f?)]]
+   [⊢ pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?) (⇒ function? f?)]
   #:fail-unless (syntax-e #'s?)
                 (format "Expected a Rosette-solvable type, given ~a." 
                         (syntax->datum #'pred?))
@ -25,19 +25,23 @@
               (format "Expected a non-function Rosette type, given ~a." 
                       (syntax->datum #'pred?))
   --------
-   [⊢ [_ ≫ (??/progsrc pred?-) ⇒ : ty]]])
+   [⊢ (??/progsrc pred?-) ⇒ ty]])
  
 (define-syntax print-forms
  (make-variable-like-transformer
-   (assign-type #'ro:print-forms #'(t/ro:C→ t/ro:CSolution t/ro:Unit))))
+   (assign-type #'ro:print-forms
+                #'(t/ro:C→ t/ro:CSolution t/ro:Unit))))

 (define-syntax generate-forms
  (make-variable-like-transformer
-   (assign-type #'ro:generate-forms #'(t/ro:C→ t/ro:CSolution (t/ro:CListof t/ro:CSyntax)))))
+   (assign-type #'ro:generate-forms 
+                #'(t/ro:C→ t/ro:CSolution (t/ro:CListof t/ro:CSyntax)))))

 (define-typed-syntax choose
  [(ch e ...+) ≫
-   [⊢ [e ≫ e- ⇒ : ty]] ...
+   ;; [⊢ e ≫ e- ⇒ ty] ...
+   #:with (e- ...) (stx-map t/ro:expand/ro #'(e ...))
+   #:with (ty ...) (stx-map typeof #'(e- ...))
   #:with (e/disarmed ...) (stx-map replace-stx-loc #'(e- ...) #'(e ...))
   ;; the #'choose identifier itself must have the location of its use
   ;; see define-synthax implementation, specifically syntax/source in utils
@ -45,36 +49,25 @@
   --------
   [⊢ (ch/disarmed e/disarmed ...) ⇒ (t/ro:U ty ...)]])

-;; TODO: not sure how to handle define-synthax
-;; it defines a macro, but may refer to itself in #:base and #:else
-;; - so must expand "be" and "ee", but what to do about self reference?
-;; - the current letrec-like implementation results in an #%app of the the f macro
-;;   which isnt quite right
-#;(define-typed-syntax define-synthax #:datum-literals (: -> →)
-  #;[(_ x:id ([pat e] ...+)) ≫
-   [⊢ [e ≫ e- ⇒ : τ]] ...
-   #:with y (generate-temporary #'x)
+;; define-synthax defines macro f, which may be referenced in #:base and #:else
+;; - thus cannot expand "be" and "ee", and arguments to f invocation
+;; - last arg is an int that will be eval'ed to determine unroll depth
+;; - must do some expansion to check types,
+;;   but dont use expanded stx objs as args to ro:define-synthax
+(define-typed-syntax define-synthax
+  [(_ (f [x (~datum :) ty] ... k (~datum ->) ty-out) #:base be #:else ee) ≫
+   #:with f- (generate-temporary #'f)
+   #:with (a ...) (generate-temporaries #'(ty ...))
   --------
-   [_ ≻ (begin-
-          (define-syntax- x (make-rename-transformer (⊢ y : t/ro:Int)))
-          (ro:define-synthax y ([pat e-] ...)))]]
-  [(_ (f [x:id : ty] ... [k:id : tyk] -> ty_out) #:base be #:else ee) ≫
-   #:with (e ...) #'(be ee)
-   [() ([x ≫ x- : ty] ... [k ≫ k- : tyk] [f ≫ f- : (t/ro:C→ ty ... tyk ty_out)]) ⊢ 
-    [e ≫ e- ⇒ : ty_e] ...]
-   #:with (be- ee-) #'(e- ...)
-   #:with f* (generate-temporary)
-   #:with app-f (format-id #'f "apply-~a" #'f)
-   --------
-   [_ ≻ (begin-
-          (ro:define-synthax (f- x- ... k-) #:base be- #:else ee-)
-          (define-syntax- app-f
-            (syntax-parser
-              [(_ . es)
-               ;; TODO: typecheck es
-               #:with es- (stx-map expand/df #'es)
-;               #:with es/fixsrc (stx-map replace-stx-loc #'es- #'es)
-               (assign-type #'(f- . es) #'ty_out)])))]])
-;             (⊢ f- : (t/ro:C→ ty ... tyk ty_out))
-;          #;(ro:define-synthax (f- x- ... k-)
-;            #:base be- #:else ee-))]])
+   [≻ (begin-
+        (ro:define-synthax (f- x ... k) #:base be #:else ee)
+        (define-typed-syntax f
+          [(ff a ... j) ≫
+           [⊢ a ≫ _ ⇐ ty] ...
+           [⊢ j ≫ _ ⇐ t/ro:Int]
+           ;; j will be eval'ed, so strip its context
+           #:with j- (assign-type (datum->syntax #'H (stx->datum #'j))
+                                  #'t/ro:Int)
+           #:with f-- (replace-stx-loc #'f- #'ff)
+           --------
+           [⊢ (f-- a ... j-) ⇒ ty-out]]))]])
--- a/turnstile/examples/rosette/rosette-notes.txt
+++ b/turnstile/examples/rosette/rosette-notes.txt
@ -1,11 +1,9 @@
 2016-11-18 --------------------

- working on synthcl lang
+working on synthcl3 lang
 - added `grammar` form, which expands to define-synthax
 - definition does not error, but applying a "grammar" definition results in
  strange error, during type eval
- last time I saw something like this, it was a bad type regexp parse in #%app
-  but app is not being invoked here

 Strange error:
 t: unbound identifier in module
@ -15,6 +13,9 @@ Strange error:
 ;  /home/stchang/NEU_Research/macrotypes/macrotypes/typecheck.rkt:86:7
 ;  /home/stchang/racket/rosette-stchang/rosette/base/form/module.rkt:16:0

+- last time I saw something like this, it was a bad type regexp parse in #%app
+  but app is not being invoked here
+- UPDATE: it's the same regexp problem, in define-coercing-real-binop

 2016-11-02 --------------------
 ** Problem: typed forms should not expand all the way down
@ -32,6 +33,10 @@ since e1+ and e2+ are already fully expanded

 see rosette:define/debug as an example

+1b) related to 1), term-cache will not be properly populated if ro:XX forms
+    are handed full-expanded stx objs
+    - see define-synthax
+
 2) syntax taints

 If the host lang (eg rosette) uses syntax rules, then the typed layer will
@ -46,6 +51,15 @@ Further requirements for this solution:
 - workound by converting to explicit internal definition contexts rather than
  lambda wrappers?
 2) local expand must use a stop list containing host lang prompt macro
+UPDATE 2016-11-22: tried to use internal-def-ctx to get around requirement #1
+ but couldnt get it to work
+- specifically, how to return x- in infer fn
+- tried to get x- with separate call (using same int-def-ctx) to local-expand
+  but it was causing nesting issues (eg, unbound tyvars)
+
+** current solution (2016-11-22)
+- use special expand fn (eg, expand/ro) with stop-list containing all rosette
+identifiers


 2016-09-08 --------------------
--- a/turnstile/examples/rosette/rosette3.rkt
+++ b/turnstile/examples/rosette/rosette3.rkt
@ -17,12 +17,12 @@
 (only-in "../stlc+union+case.rkt" [~U* ~CU*] [~case-> ~Ccase->] [~→ ~C→])
 (only-in "../stlc+cons.rkt" [~List ~CListof])
 ;; base lang
- (prefix-in ro: rosette)
+ (prefix-in ro: (combine-in rosette rosette/lib/synthax))
 (rename-in "rosette-util.rkt" [bitvector? lifted-bitvector?]))

 (provide (rename-out [ro:#%module-begin #%module-begin] 
                     [stlc+union:λ lambda])
-         (for-syntax get-pred)
+         (for-syntax get-pred expand/ro)
         Any CNothing Nothing
         CU U (for-syntax ~U*)
         Constant
@ -50,6 +50,14 @@
         CSolution CSolver CPict CSyntax CRegexp CSymbol CPred CPredC)

 (begin-for-syntax
+  ;; TODO: fix this so it's not using hardcoded list of ids
+  (define (expand/ro e)
+    (define e+
+      (local-expand
+       e 'expression
+       (list #'ro:#%app #'ro:choose #'ro:synthesize)))
+;    (displayln (stx->datum e+))
+    e+)
  (define (mk-ro:-id id) (format-id id "ro:~a" id))
  (current-host-lang mk-ro:-id))

@ -389,19 +397,29 @@
 (define-typed-syntax app #:export-as #%app
  ;; concrete functions
  [(_ e_fn e_arg ...) ≫
-   [⊢ [e_fn ≫ e_fn- ⇒ : (~C→ ~! τ_in ... τ_out)]]
+;   [⊢ e_fn ≫ e_fn- ⇒ (~C→ ~! τ_in ... τ_out)]
+   #:with e_fn- (expand/ro #'e_fn)
+   #:with (~C→ ~! τ_in ... τ_out) (typeof #'e_fn-)
   #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn)
   #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
-   (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
-   [⊢ [e_arg ≫ e_arg- ⇐ : τ_in] ...]
+                 (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
+;   [⊢ e_arg ≫ e_arg- ⇐ τ_in] ...
+   #:with (e_arg- ...) (stx-map expand/ro #'(e_arg ...))
+   #:with ty_args (stx-map typeof #'(e_arg- ...))
+   #:fail-unless (typechecks? #'ty_args #'(τ_in ...))
+                 (typecheck-fail-msg/multi #'(τ_in ...) #'ty_args #'(e_arg ...))
   --------
   ;; 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- (expand/ro #'e_fn)
+   #:with (~Ccase-> ~! . (~and ty_fns ((~C→ . _) ...))) (typeof #'e_fn-)
+;   [⊢ [e_fn ≫ e_fn- ⇒ : (~Ccase-> ~! . (~and ty_fns ((~C→ . _) ...)))]]
   #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn)
-   [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
+;   [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
+   #:with (e_arg- ...) (stx-map expand/ro #'(e_arg ...))
+   #:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))
   #:with τ_out
   (for/first ([ty_f (stx->list #'ty_fns)]
               #:when (syntax-parse ty_f
@ -433,9 +451,13 @@
   [⊢ [_ ≫ (ro:#%app e_fn/progsrc- e_arg- ...) ⇒ : τ_out]]]
  ;; concrete union functions
  [(_ e_fn e_arg ...) ≫
-   [⊢ [e_fn ≫ e_fn- ⇒ : (~CU* τ_f ...)]]
+   #:with e_fn- (expand/ro #'e_fn)
+   #:with (~CU* τ_f ...) (typeof #'e_fn-)
+;   [⊢ [e_fn ≫ e_fn- ⇒ : (~CU* τ_f ...)]]
   #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn)
-   [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
+;   [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
+   #:with (e_arg- ...) (stx-map expand/ro #'(e_arg ...))
+   #:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))
   #:with (f a ...) (generate-temporaries #'(e_fn e_arg ...))
   [([f ≫ _ : τ_f] [a ≫ _ : τ_arg] ...)
    ⊢ [(app f a ...) ≫ _ ⇒ : τ_out]]
@ -444,9 +466,13 @@
   [⊢ [_ ≫ (ro:#%app e_fn/progsrc- e_arg- ...) ⇒ : (CU τ_out ...)]]]
  ;; symbolic functions
  [(_ e_fn e_arg ...) ≫
-   [⊢ [e_fn ≫ e_fn- ⇒ : (~U* τ_f ...)]]
+   #:with e_fn- (expand/ro #'e_fn)
+   #:with (~U* τ_f ...) (typeof #'e_fn-)
+;   [⊢ [e_fn ≫ e_fn- ⇒ : (~U* τ_f ...)]]
   #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn)
-   [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
+;   [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
+   #:with (e_arg- ...) (stx-map expand/ro #'(e_arg ...))
+   #:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))
   #:with (f a ...) (generate-temporaries #'(e_fn e_arg ...))
   [([f ≫ _ : τ_f] [a ≫ _ : τ_arg] ...)
    ⊢ [(app f a ...) ≫ _ ⇒ : τ_out]]
@ -455,9 +481,13 @@
   [⊢ [_ ≫ (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- (expand/ro #'e_fn)
+   #:with (~Constant* (~U* τ_f ...)) (typeof #'e_fn-)
+;   [⊢ [e_fn ≫ e_fn- ⇒ : (~Constant* (~U* τ_f ...))]]
   #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn)
-   [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
+;   [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
+   #:with (e_arg- ...) (stx-map expand/ro #'(e_arg ...))
+   #:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))
   #:with (f a ...) (generate-temporaries #'(e_fn e_arg ...))
   [([f ≫ _ : τ_f] [a ≫ _ : τ_arg] ...)
    ⊢ [(app f a ...) ≫ _ ⇒ : τ_out]]
--- a/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec43-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec43-tests.rkt
@ -70,7 +70,7 @@
 ;(define-symbolic b boolean?)
 ;; typed Rosette rejects this program
 (typecheck-fail (bvnot (if b 0 (bv 0 4)))
- #:with-msg "expected BV, given \\(U Zero CBV\\)")
+ #:with-msg "expected.*BV.*given.*\\(U Zero CBV\\)")
 ;; need assert-type annotation
 (check-type (bvnot (assert-type (if b 0 (bv 0 4)) : BV)) : BV -> (bv -1 4)) 
 (check-type (asserts) : (CListof Bool) -> (list (! b)))
@ -82,7 +82,7 @@
 ;(define-symbolic b boolean?)
 ;; typed Rosette rejects this program
 (typecheck-fail (bvand (bv -1 4) (if b 0 (bv 2 4)))
- #:with-msg "expected BV, given \\(U Zero CBV\\)")
+ #:with-msg "expected.*BV.*given.*\\(U Zero CBV\\)")
 ;; need assert-type annotation
 (check-type (bvand (bv -1 4) (assert-type (if b 0 (bv 2 4)) : BV)) : BV -> (bv 2 4))
 (check-type (asserts) : (CListof Bool) -> (list (! b)))
@ -94,7 +94,7 @@
 ;(define-symbolic b boolean?)
 ;; typed Rosette rejects this program
 (typecheck-fail (bvshl (bv -1 4) (if b 0 (bv 2 4)))
- #:with-msg "expected BV, given \\(U Zero CBV\\)")
+ #:with-msg "expected.*BV.*given.*\\(U Zero CBV\\)")
 ;; need assert-type annotation
 (check-type (bvshl (bv -1 4) (assert-type (if b 0 (bv 2 4)) : BV)) : BV -> (bv -4 4))
 (check-type (asserts) : CAsserts -> (list (! b)))
@ -180,7 +180,7 @@
 ;> (define-symbolic b c boolean?)
 ;; typed Rosette rejects this program
 (typecheck-fail (integer->bitvector (if b pi 3) (if c (bitvector 5) (bitvector 6)))
- #:with-msg "expected Int, given.*Num")
+ #:with-msg "expected.*Int.*given.*Num")
 (check-type (if b pi 3) : Num)
 (check-not-type (if b pi 3) : Int)
 ;; need assert-type annotation
--- a/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec44-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec44-tests.rkt
@ -20,7 +20,7 @@
 (check-not-type (f 1) : CBool)
 (define-symbolic x real?)
 ; typed Rosette rejects tis program
-(typecheck-fail (f x) #:with-msg "expected Int, given.*Num")
+(typecheck-fail (f x) #:with-msg "expected.*Int.* given.*Num")
 ;; must use assert-type to cast to Int
 (check-type (f (assert-type x : Int)) 
            : Bool -> (f (assert-type x : Int))) ;(app f (real->integer x)))
@ -30,7 +30,7 @@

 ;; typed Rosette rejects this program
 (typecheck-fail (solve (assert (not (equal? (f x) (f 1)))))
-                #:with-msg "expected Int, given.*Num")
+                #:with-msg "expected.*Int.*given.*Num")
 ;; must use assert-type to cast x toInt
 (define sol (solve (assert (not (equal? (f (assert-type x : Int)) (f 1))))))
 (check-type sol : CSolution)
--- a/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec5-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec5-tests.rkt
@ -16,7 +16,7 @@
 (struct pnt ([x : Int] [y : Int]) #:mutable #:transparent)

 (check-type (point 1 2) : (CPoint Int Int) -> (point 1 2))
-(typecheck-fail (point #f 2) #:with-msg "expected Int, given False")
+(typecheck-fail (point #f 2) #:with-msg "expected.*Int.*given.*False")
 (check-type (pt 1 2) : (CPt Int Int)) ; opaque, incomparable
 (check-type (pnt 1 2) : (CPnt Int Int) -> (pnt 1 2))

--- a/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec6-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec6-tests.rkt
@ -26,26 +26,26 @@
 #;(printf "expected output:\n~a\n" 
        "'(define (div2 [x : BV] -> BV) (bvlshr x (bv 1 8)))")

-;; TODO: define-synthax
-; Defines a grammar for boolean expressions
-; in negation normal form (NNF).
-#;(define-synthax (nnf [x : Bool] [y : Bool] [depth : Int] -> Bool)
+;; define-synthax
+(define-synthax (nnf [x : Bool] [y : Bool] depth -> Bool)
 #:base (choose x (! x) y (! y))
 #:else (choose
         x (! x) y (! y)
         ((choose && ||) (nnf x y (- depth 1))
                         (nnf x y (- depth 1)))))
- 
-; The body of nnf=> is a hole to be filled with an
-; expression of depth (up to) 1 from the NNF grammar.
-#;(define (nnf=> [x : Bool] [y : Bool] -> Bool)
-  (apply-nnf x y 1))
- 
-;; (define-symbolic a b boolean?)
-;; (print-forms
-;;    (synthesize
-;;     #:forall (list a b)
-;;     #:guarantee (assert (equal? (=> a b) (nnf=> a b)))))
+(define (nnf=> [x : Bool] [y : Bool] -> Bool)
+  (nnf x y 1))
+
+(define-symbolic a b boolean?)
+(check-type
+ (with-output-to-string
+   (λ ()
+     (print-forms
+      (synthesize
+       #:forall (list a b)
+       #:guarantee (assert (equal? (=> a b) (nnf=> a b)))))))
+ : CString
+ -> "/home/stchang/NEU_Research/macrotypes/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec6-tests.rkt:36:0\n'(define (nnf=> (x : Bool) (y : Bool) -> Bool) (|| (! x) y))\n")
 ;; (printf "expected output:\n~a\n"
 ;;         "'(define (nnf=> [x : Bool] [y : Bool] -> Bool) (|| (! x) y))")

--- a/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec7-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette3/rosette-guide-sec7-tests.rkt
@ -99,19 +99,19 @@
 (check-type (racket/string-length "abababa") : CNat -> 7)
 (check-not-type (string-length "abababa") : CNat)

-(typecheck-fail (string-length 3) #:with-msg "expected String")
+(typecheck-fail (string-length 3) #:with-msg "expected.*String")
 ;> (define-symbolic b boolean?)
 (check-type (string-length (if b "a" "abababa")) : Nat -> (if b 1 7)) ;(ite b 1 7)
 (check-not-type (string-length (if b "a" "abababa")) : CNat)

 ;; Typed Rosette rejects this program
-(typecheck-fail (string-length (if b "a" 3)) #:with-msg "expected String")
+(typecheck-fail (string-length (if b "a" 3)) #:with-msg "expected.*String")
 ;; need assert-type
 ;; TODO: this doesnt work yet because String has no pred
 ;; - and we cant use string? bc it's unlifted --- will always be assert fail
 ;(check-type (string-length (assert-type (if b "a" 3) : String)) : Nat -> 1)
 ;;(check-type (asserts) : CAsserts -> (list b))
-(typecheck-fail (string-length (if b 3 #f)) #:with-msg "expected String")
+(typecheck-fail (string-length (if b 3 #f)) #:with-msg "expected.*String")
 ;; not runtime exn: for/all: all paths infeasible

 ;; Making symbolic evaluation more efficient.
--- a/turnstile/examples/tests/rosette/rosette3/rosette3-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette3/rosette3-tests.rkt
@ -241,8 +241,8 @@
 (typecheck-fail ((λ ([f : (Ccase-> (C→ Zero Zero)
                                   (C→ Int Int))]) (f 10)) add1) 
  #:with-msg
-  (string-append "expected \\(Ccase-> \\(C→ Zero Zero\\) \\(C→ Int Int\\)\\), "
-                 "given \\(Ccase-> .*\\(C→ NegInt \\(U NegInt Zero\\)\\) .*\\(C→ Zero PosInt\\) "
+  (string-append "expected.*\\(Ccase-> \\(C→ Zero Zero\\) \\(C→ Int Int\\)\\).*"
+                 "given.*\\(Ccase-> .*\\(C→ NegInt \\(U NegInt Zero\\)\\) .*\\(C→ Zero PosInt\\) "
                 ".*\\(C→ PosInt PosInt\\) .*\\(C→ Nat PosInt\\) .*\\(C→ Int Int\\)\\)"))

 ;; applying symbolic function types
@ -265,9 +265,9 @@
 ;; check BVPred as type annotation
 ;; CBV input annotation on arg is too restrictive to work as BVPred
 (typecheck-fail ((λ ([bvp : BVPred]) bvp) (λ ([bv : CBV]) #t)) 
-                #:with-msg "expected BVPred.*given.*CBV")
+                #:with-msg "expected.*BVPred.*given.*CBV")
 (typecheck-fail ((λ ([bvp : BVPred]) bvp) (λ ([bv : BV]) #t))
-                #:with-msg "expected BVPred.*given.*BV")
+                #:with-msg "expected.*BVPred.*given.*BV")
 ;; BVpred arg must have Any input type
 (check-type ((λ ([bvp : BVPred]) bvp) (λ ([bv : Any]) ((bitvector 2) bv))) : BVPred)