From 87082689925a037d70bd4d87f8c1e9c67c695da5 Mon Sep 17 00:00:00 2001 From: Jay McCarthy Date: Sat, 30 Apr 2011 12:02:29 -0600 Subject: [PATCH] Fixing problems with %is discovered by Casey --- collects/racklog/racklog.rkt | 67 +++++++++++++++++++++++++---- collects/tests/racklog/is.rkt | 80 +++++++++++++++++++++++++++++++++++ 2 files changed, 139 insertions(+), 8 deletions(-) create mode 100644 collects/tests/racklog/is.rkt diff --git a/collects/racklog/racklog.rkt b/collects/racklog/racklog.rkt index 90f577faaa..fbe2c95474 100644 --- a/collects/racklog/racklog.rkt +++ b/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) - (lambda (__fk) - ((%= v (%is/fk e __fk)) __fk))))) -(define-syntax %is/fk +(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 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) diff --git a/collects/tests/racklog/is.rkt b/collects/tests/racklog/is.rkt new file mode 100644 index 0000000000..c9797ddcd4 --- /dev/null +++ b/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) + + )