Fixing problems with %is discovered by Casey

collects/racklog/racklog.rkt

@@ -1,5 +1,10 @@
-#lang racket
-(require scheme/stxparam
+#lang racket/base
+(require (for-syntax racket/base
+                     racket/list
+                     syntax/kerncase)
+         racket/list
+         racket/contract
+         racket/stxparam
          "unify.rkt")
 
 ;Dorai Sitaram
@@ -67,12 +72,58 @@
 (define %true
   (lambda (fk) fk))
 
-(define-syntax %is
-  (syntax-rules ()
-    ((%is v e)
+(define-syntax (%is stx)
+  (syntax-case stx ()
+    [(%is v e)
+     (with-syntax ([fe (local-expand #'e 'expression empty)])
+       (syntax/loc stx
          (lambda (__fk)
-       ((%= v (%is/fk e __fk)) __fk)))))
-(define-syntax %is/fk
+           ((%= v (%is/fk fe __fk)) __fk))))]))
+(define-syntax (%is/fk stx)
+  (kernel-syntax-case stx #f
+    [(_ (#%plain-lambda fmls e ...) fk)
+     (syntax/loc stx (#%plain-lambda fmls (%is/fk e fk) ...))]
+    [(_ (case-lambda [fmls e ...] ...) fk)
+     (syntax/loc stx (case-lambda [fmls (%is/fk e fk) ...] ...))]
+    [(_ (if e1 e2 e3) fk)
+     (syntax/loc stx (if (%is/fk e1 fk)
+                         (%is/fk e2 fk) 
+                         (%is/fk e3 fk)))]
+    [(_ (begin e ...) fk)
+     (syntax/loc stx (begin (%is/fk e fk) ...))]
+    [(_ (begin0 e ...) fk)
+     (syntax/loc stx (begin0 (%is/fk e fk) ...))]
+    [(_ (let-values ([(v ...) ve] ...)
+          be ...) fk)
+     (syntax/loc stx
+       (let-values ([(v ...) (%is/fk ve fk)] ...) 
+         (%is/fk be fk) ...))]
+    [(_ (letrec-values ([(v ...) ve] ...)
+          be ...) fk)
+     (syntax/loc stx
+       (letrec-values ([(v ...) (%is/fk ve fk)] ...) 
+         (%is/fk be fk) ...))]
+    [(_ (set! i e) fk)
+     (syntax/loc stx (set! i (%is/fk e fk)))]
+    [(_ (quote d) fk)
+     (syntax/loc stx (quote d))]
+    [(_ (quote-syntax d) fk)
+     (syntax/loc stx (quote-syntax d))]
+    [(_ (with-continuation-mark e1 e2 e3) fk)
+     (syntax/loc stx (with-continuation-mark
+                         (%is/fk e1 fk)
+                       (%is/fk e2 fk) 
+                       (%is/fk e3 fk)))]
+    [(_ (#%plain-app e ...) fk)
+     (syntax/loc stx (#%plain-app (%is/fk e fk) ...))]
+    [(_ x fk)
+     (syntax/loc stx
+       (if (and (logic-var? x) (unbound-logic-var? x))
+           (fk 'fail) (logic-var-val* x)))]
+    
+    ))
+
+#;(define-syntax %is/fk
   (syntax-rules (quote)
     ((%is/fk (quote x) fk) (quote x))
     ((%is/fk (x ...) fk)

collects/tests/racklog/is.rkt

@@ -0,0 +1,80 @@
+#lang racket
+(require racklog
+         racket/stxparam
+         tests/eli-tester)
+
+(define-syntax-parameter Y 
+  (λ (stx)
+    (raise-syntax-error stx 'Y "not allowed outside test-%is")))
+(define-syntax (test-%is stx)
+  (syntax-case stx ()
+    [(_ e)
+     (with-syntax ([the-y #'y])
+       #`(test #:failure-prefix (format "~a" 'e)
+               (test
+                (%which (x)
+                        (syntax-parameterize
+                         ([Y (λ (stx) #'1)])
+                         (%is x e))) => `([x . 1])
+                                     (%more) => #f)
+               #:failure-prefix (format "~a (let)" 'e)
+               (test
+                (%which (x) 
+                        (%let (the-y) 
+                              (%and (%= the-y 1) 
+                                    (syntax-parameterize
+                                     ([Y (make-rename-transformer #'the-y)])
+                                     (%is x e)))))
+                => `([x . 1])
+                (%more) => #f)))]))
+
+(define top-z 1)
+
+(test
+ (test-%is Y)
+ (let ([z 1]) (test-%is z))
+ (test-%is ((λ (x) x) Y))
+ (test-%is ((λ (x) Y) 2))
+ (test-%is ((case-lambda [(x) x]) Y))
+ (test-%is ((case-lambda [(x) Y]) 2))
+ (test-%is (+ 0 Y))
+ (test-%is (if #t Y 2))
+ (test-%is (if #f 2 Y))
+ (test-%is (begin Y))
+ (test-%is (begin0 Y 2))
+ (test-%is (let ([z Y]) z))
+ (test-%is (let ([z 2]) Y))
+ (test-%is (letrec ([z Y]) z))
+ (test-%is (letrec ([z 2]) Y))
+ (let ([z 2])
+   (test-%is (begin (set! z Y) z)))
+ (test-%is '1)
+ (%which (x) (%let (y) (%and (%= y 1) (%is x 'y)))) => `([x . y])
+ (%more) => #f
+ (%which (x) (%let (y) (%and (%= y 1) (%is x #'1)))) 
+ ;=> `([x . ,#'1])
+ (%more) => #f
+ (%which (x) (%let (y) (%and (%= y 1) (%is x #'y))))
+ ;=> `([x . ,#'y])
+ (%more) => #f
+ (test-%is (with-continuation-mark 'k 'v Y))
+ (test-%is (with-continuation-mark 'k Y
+             (first
+              (continuation-mark-set->list
+               (current-continuation-marks)
+               'k))))
+ (test-%is (with-continuation-mark Y Y
+             (first
+              (continuation-mark-set->list
+               (current-continuation-marks)
+               Y))))
+ (test-%is (#%top . top-z))
+ 
+ #;(test
+    (test-%is (#%variable-reference Y))
+    (let ([z 1]) (test-%is (#%variable-reference z)))
+    (test-%is (#%variable-reference (#%top . top-z)))
+    (%which (x) (%let (y) (%and (%= y 1) (%is x (#%variable-reference))))) => `([x . ,(#%variable-reference)])
+    (%more) => #f)
+ 
+ )