suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

redex: add variable-not-in to derivation generator

Browse Source
This commit is contained in:
Burke Fetscher 2014-06-26 15:22:23 -05:00
parent 116555c517
commit 72a5e3949a
6 changed files with 231 additions and 158 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
pkgs/redex-pkgs/redex-examples/redex/examples/let-poly.rkt
View File

@ -339,6 +339,21 @@ Capture avoiding substitution
[(subst M x M_z) [(subst M x M_z)
M]) M])
(define-metafunction stlc
[(replace x x x_new)
x_new]
[(replace (λ x_0 M) x x_new)
(λ (replace x_0 x x_new) (replace M x x_new))]
[(replace (let ([x_0 M]) N) x x_new)
(let ([(replace x_0 x x_new)
(replace M x x_new)])
(replace N x x_new))]
[(replace (M N) x x_new)
((replace M x x_new) (replace N x x_new))]
[(replace M x x_new)
M])
#;
(define-metafunction stlc (define-metafunction stlc
[(replace (any_1 ...) x_1 x_new) [(replace (any_1 ...) x_1 x_new)
((replace any_1 x_1 x_new) ...)] ((replace any_1 x_1 x_new) ...)]

6
pkgs/redex-pkgs/redex-lib/redex/private/jdg-gen.rkt
View File

@ -7,6 +7,7 @@
(only-in "reduction-semantics.rkt" (only-in "reduction-semantics.rkt"
do-test-match) do-test-match)
"pat-unify.rkt" "pat-unify.rkt"
(only-in "fresh.rkt" variable-not-in)
(for-syntax racket/base)) (for-syntax racket/base))
(provide pat->term (provide pat->term
@ -20,6 +21,7 @@
;; pat->term lang pat* env env -> term ;; pat->term lang pat* env env -> term
(define (pat->term lang pat full-env [term-e (make-hash)]) (define (pat->term lang pat full-env [term-e (make-hash)])
(displayln (list 'pat->term lang pat))
(define nt-matchers (make-hash)) (define nt-matchers (make-hash))
(define eqs (env-eqs full-env)) (define eqs (env-eqs full-env))
(define (get-matcher nt) (define (get-matcher nt)
@ -42,6 +44,8 @@
`(,@(for/list ([p ps]) (recur p)))] `(,@(for/list ([p ps]) (recur p)))]
[`(cstr (,nts ...) ,p) [`(cstr (,nts ...) ,p)
(recur p)] (recur p)]
[`(variable-not-in ,not-in-p ,sym)
(recur not-in-p)]
[`(nt ,_) [`(nt ,_)
(okk (ok))] (okk (ok))]
[(? predef-pat? _) [(? predef-pat? _)
@ -87,6 +91,8 @@
(let ([res (recur p)]) (let ([res (recur p)])
(unless (not-failed? res) (fail (unif-fail))) (unless (not-failed? res) (fail (unif-fail)))
res))))] res))))]
[`(variable-not-in ,not-in-p ,sym)
(variable-not-in (recur not-in-p) sym)]
[_ [_
(make-term p lang)]))) (make-term p lang)])))
(and/fail (and/fail

3
pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt
View File

@ -1492,6 +1492,9 @@
(and (identifier? #'in-hole) (and (identifier? #'in-hole)
(eq? (syntax-e #'in-hole) 'in-hole)) (eq? (syntax-e #'in-hole) 'in-hole))
#''(in-hole . rest)] #''(in-hole . rest)]
;; TODO check that s is quoted or a term
[(undatum (variable-not-in (term . tr) . s))
#f]
[(undatum . rest) [(undatum . rest)
(and (identifier? #'undatum) (and (identifier? #'undatum)
(eq? (syntax-e #'undatum) 'undatum)) (eq? (syntax-e #'undatum) 'undatum))

196
pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt
View File

@ -414,6 +414,12 @@
(if (not-failed? res) (if (not-failed? res)
res res
(fail (unif-fail))))))] (fail (unif-fail))))))]
[`(variable-not-in ,p ,s)
(define pat (bind-names p e L))
(and/fail (not-failed? pat)
(let ([s-pat (bind-names s e L)])
(and/fail (not-failed? s-pat)
`(variable-not-in ,pat ,s-pat))))]
[`(mismatch-name ,name ,p) [`(mismatch-name ,name ,p)
(define b-pat (bind-names p e L)) (define b-pat (bind-names p e L))
(and/fail (not-failed? b-pat) (and/fail (not-failed? b-pat)
@ -426,51 +432,52 @@
(define t (resolve t0 e)) (define t (resolve t0 e))
(define u (resolve u0 e)) (define u (resolve u0 e))
#2dmatch #2dmatch
╔═════════════════╦═════════════════╦═════════════╦═══════════════╦═══════════╦══════╦════════════╦══════════════╦═════════════════╦═════════╦══════════╦══════════════╦═════════════╗ ╔═════════════════╦═════════════════╦═════════════╦═══════════════╦═══════════╦══════╦════════════╦══════════════╦═══════════════════╦═════════╦══════════╦══════════════╦═════════════╗
║ u ║ `(mismatch-name ║ `(name ║ `(cstr ║`(nt ,n-u) ║`any ║ (? num-ty?)║`(list ║ (? pvar?) ║ `string ║ `boolean ║ (? base-ty?) ║(? not-pair?)║ ║ u ║ `(mismatch-name ║ `(name ║ `(cstr ║`(nt ,n-u) ║`any ║ (? num-ty?)║`(list ║ (? pvar?) ║ `string ║ `boolean ║ (? base-ty?) ║(? not-pair?)║
║ ║ ,u-name ║ ,name-u ║ (,nts1 ...) ║ ║ ║ ║ ,us ...) ║ ║ ║ ║ ║ ║ ║ ║ ,u-name ║ ,name-u ║ (,nts1 ...) ║ ║ ║ ║ ,us ...) ║ ║ ║ ║ ║ ║
║ t ║ ,u-pat) ║ ,(bound)) ║ ,p1) ║ ║ ║ ║ ║ ║ ║ ║ ║ ║ ║ t ║ ,u-pat) ║ ,(bound)) ║ ,p1) ║ ║ ║ ║ ║ ║ ║ ║ ║ ║
╠═════════════════╬═════════════════╩═════════════╩═══════════════╩═══════════╩══════╩════════════╩══════════════╩═════════════════╩═════════╩══════════╩══════════════╩═════════════╣ ╠═════════════════╬═════════════════╩═════════════╩═══════════════╩═══════════╩══════╩════════════╩══════════════╩═══════════════════╩═════════╩══════════╩══════════════╩═════════════╣
║`(mismatch-name ║ (hash-set! (dqs-found) t-name (cons u (hash-ref (dqs-found) t-name (λ () '())))) ║ ║`(mismatch-name ║ (hash-set! (dqs-found) t-name (cons u (hash-ref (dqs-found) t-name (λ () '())))) ║
║ ,t-name ║ (unify* t-pat u e L) ║ ║ ,t-name ║ (unify* t-pat u e L) ║
║ ,t-pat) ║ ║ ║ ,t-pat) ║ ║
╠═════════════════╬═════════════════╦════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╣ ╠═════════════════╬═════════════════╦══════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╣
║`(name ,name-t ║ ║ (instantiate* name-t u e L) ║ ║`(name ,name-t ║ ║ (instantiate* name-t u e L) ║
║ ,(bound)) ║ ║ ║ ║ ,(bound)) ║ ║ ║
╠═════════════════╣ ╚═════════════╦═══════════════╦══════════════════════════════════════════════════════════════════════════════════════════════════════════════════╣ ╠═════════════════╣ ╚═════════════╦═══════════════╦════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╣
║`(cstr ║ ║(u*-2cstrs ║ (u*-1cstr nts2 p2 u e L) ║ ║`(cstr ║ ║(u*-2cstrs ║ (u*-1cstr nts2 p2 u e L) ║
║ (,nts2 ...) ║ ║ nts1 p1 ║ ║ ║ (,nts2 ...) ║ ║ nts1 p1 ║ ║
║ ,p2) ║ ║ nts2 p2 e L) ║ ║ ║ ,p2) ║ ║ nts2 p2 e L) ║ ║
╠═════════════════╣ ╚═══════════════╬═══════════╦══════════════════════════════════════════════════════════════════════════════════════════════════════╣ ╠═════════════════╣ ╚═══════════════╬═══════════╦════════════════════════════════════════════════════════════════════════════════════════════════════════╣
║ `(nt ,n-t) ║ ║(u*-2nts ║ (u*-1nt n-t u e L) ║ ║ `(nt ,n-t) ║ ║(u*-2nts ║ (u*-1nt n-t u e L) ║
║ ║ ║ n-t n-u ║ ║ ║ ║ ║ n-t n-u ║ ║
║ ║ ║ e L) ║ ║ ║ ║ ║ e L) ║ ║
╠═════════════════╣ ╚═══════════╬══════════════════════════════════════════════════════════════════════════════════════════════════════╣ ╠═════════════════╣ ╚═══════════╬════════════════════════════════════════════════════════════════════════════════════════════════════════╣
║ `any ║ ║ u ║ ║ `any ║ ║ u ║
║ ║ ║ ║ ║ ║ ║ ║
╠═════════════════╣ ╚══════╦════════════╦════════════════════════════════════════════════════════════════════╦═════════════╣ ╠═════════════════╣ ╚══════╦════════════╦══════════════════════════════════════════════════════════════════════╦═════════════╣
║ (? num-ty?) ║ ║(u*-2nums ║ ║ ║ ║ (? num-ty?) ║ ║(u*-2nums ║ ║ ║
║ ║ ║ t u) ║ ║ ║ ║ ║ ║ t u) ║ ║ ║
╠═════════════════╣ ╚════════════╬══════════════╗ ║ ║ ╠═════════════════╣ ╚════════════╬══════════════╗ ║ ║
║ `(list ,ts ...) ║ ║(u*-2lsts ║ (unif-fail) ║ ║ ║ `(list ,ts ...) ║ ║(u*-2lsts ║ (unif-fail) ║ ║
║ ║ ║ ts us e L) ║ ║(u*-matches? ║ ║ ║ ║ ts us e L) ║ ║(u*-matches? ║
╠═════════════════╣ ╚══════════════╬═════════════════╗ ║ t u ║ ╠═════════════════╣ ╚══════════════╬═══════════════════╗ ║ t u ║
║ (? pvar?) ║ ║(u*-2pvars u t L)║ ║ e L) ║ ║ (? pvar?) ║ ║(u*-2pvars u t e L)║ ║ e L) ║
╠═════════════════╣ ╚═════════════════╬═════════╗ ║ ║ ╠═════════════════╣ ╚═══════════════════╬═════════╗ ║ ║
║ `string ║ (unify* u t e L) ║ t ║ ║ ║ ║ `string ║ (unify* u t e L) ║ t ║ ║ ║
╠═════════════════╣ ╚═════════╬══════════╗ ║ ║ ╠═════════════════╣ ╚═════════╬══════════╗ ║ ║
║ `boolean ║ ║ t ║ ║ ║ ║ `boolean ║ ║ t ║ ║ ║
╠═════════════════╣ ╚══════════╬══════════════╣ ║ ╠═════════════════╣ ╚══════════╬══════════════╣ ║
║ (? base-ty?) ║ ║ t ║ ║ ║ (? base-ty?) ║ ║ t ║ ║
╠═════════════════╣ ╚══════════════╬═════════════╣ ╠═════════════════╣ ╚══════════════╬═════════════╣
║ (? not-pair?) ║ ║(and/fail ║ ║ (? not-pair?) ║ ║(and/fail ║
║ ║ ║ (equal? t u)║ ║ ║ ║ (equal? t u)║
║ ║ ║ t) ║ ║ ║ ║ t) ║
╚═════════════════╩════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╩═════════════╝) ╚═════════════════╩══════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╩═════════════╝)
(define (pvar? x) (or (vnom? x) (define (pvar? x) (or (vnom? x)
(var-pref? x) (var-pref? x)
(var-exc? x) (var-exc? x)
(vni? x)
(equal? 'variable x))) (equal? 'variable x)))
(define (vnom? x) (equal? x 'variable-not-otherwise-mentioned)) (define (vnom? x) (equal? x 'variable-not-otherwise-mentioned))
(define (var-pref? x) (match x (define (var-pref? x) (match x
@ -480,33 +487,56 @@
[`(variable-except ,p ...) #t] [`(variable-except ,p ...) #t]
[_ #f])) [_ #f]))
(define (not-pair? x) (not (pair? x))) (define (not-pair? x) (not (pair? x)))
(define vni?
(match-lambda [`(variable-not-in ,e ,s) #t]
[_ #f]))
(define (u*-2pvars v1 v2 L) (define (u*-2pvars v1 v2 e L)
#2dmatch #2dmatch
╔════════════════════════╦══════════════════════════╦════════════════════════════════╦═══════════════════════════════╦════════════════╗ ╔══════════════════════════╦══════════════════════════╦════════════════════════════════╦═══════════════════════════════╦════════════════╦══════════════════════════════════════╗
║ v1 ║`(variable-prefix ,p1) ║ `(variable-except ,e1 ... ) ║ (? vnom?) ║ `variable ║ ║ v1 ║`(variable-prefix ,p1) ║ `(variable-except ,e1 ... ) ║ (? vnom?) ║ `variable ║`(variable-not-in ,e1 ,s) ║
║ v2 ║ ║ ║ ║ ║ ║ v2 ║ ║ ║ ║ ║ ║
╠════════════════════════╬══════════════════════════╬════════════════════════════════╬═══════════════════════════════╬════════════════╣ ╠══════════════════════════╬══════════════════════════╬════════════════════════════════╬═══════════════════════════════╬════════════════╬══════════════════════════════════════╣
║ ║ (cond ║ (and/fail ║(u*-2pvars ║ ║ ║ ║ (cond ║ (and/fail ║(u*-2pvars ║ ║(and/fail ║
║ `(variable-prefix ,p2) ║ [(sym-pref? p1 p2) ║ (not (ormap ║ v2 ║ ║ ║ `(variable-prefix ,p2) ║ [(sym-pref? p1 p2) ║ (not (ormap ║ v2 ║ ║ (sym-pref? p2 s) ║
║ ║ `(variable-prefix ,p2)]║ (curry sym-pref? p2) ║ `(variable-except ║ ║ ║ ║ `(variable-prefix ,p2)]║ (curry sym-pref? p2) ║ `(variable-except ║ ║ v1) ║
║ ║ [(sym-pref? p2 p1) ║ e1)) ║ ,@(compiled-lang-literals L)) ║ ║ ║ ║ [(sym-pref? p2 p1) ║ e1)) ║ ,@(compiled-lang-literals L)) ║ ║ ║
║ ║ `(variable-prefix ,p1)]║ v2) ║ L) ║ ║ ║ ║ `(variable-prefix ,p1)]║ v2) ║ e L) ║ ║ ║
║ ║ [else (unif-fail)]) ║ ║ ║ ║ ║ ║ [else (unif-fail)]) ║ ║ ║ ║ ║
╠════════════════════════╬══════════════════════════╬════════════════════════════════╣ ║ ║ ╠══════════════════════════╬══════════════════════════╬════════════════════════════════╣ ║ ╠══════════════════════════════════════╣
║ ║ ║ `(variable-except ║ ║ ║ ║ ║ ║ `(variable-except ║ ║ ║`(variable-not-in ║
║ `(variable-except ║ ║ ,@(de-dupe/sorted ║ ║ v2 ║ ║ `(variable-except ║ ║ ,@(de-dupe/sorted ║ ║ v2 ║ (list ,e1 ,@e2) ║
║ ,e2 ...) ║ ║ (merge/sorted e1 e2))) ║ ║ ║ ║ ,e2 ...) ║ ║ (merge/sorted e1 e2))) ║ ║ ║ ,s) ║
║ ║ ║ ║ ║ ║ ║ ║ ║ ║ ║ ║ ║
╠════════════════════════╣ ╚════════════════════════════════╬═══════════════════════════════╣ ║ ╠══════════════════════════╣ ╚════════════════════════════════╬═══════════════════════════════╣ ╠══════════════════════════════════════╣
║ ║ ║ ║ ║ ║ ║ ║ ║ ║(u*-2pvars v1 ║
║ (? vnom?) ║ ║ v1 ║ ║ ║ (? vnom?) ║ ║ v1 ║ ║`(variable-except ║
║ ║ ║ ║ ║ ║ ║ ║ ║ ║ ,@(compiled-lang-literals L)) ║
╠════════════════════════╣ (u*-2pvars v2 v1 L) ╚═══════════════════════════════╣ ║ ║ ║ ║ ║ ║ e L) ║
║ ║ ║ ║ ╠══════════════════════════╣ (u*-2pvars v2 v1 e L) ╚═══════════════════════════════╣ ╠══════════════════════════════════════╣
║ `variable ║ ║ ║ ║ ║ ║ ║ ║
║ ║ ║ ║ ║ `variable ║ ║ ║ v1 ║
╚════════════════════════╩═══════════════════════════════════════════════════════════════════════════════════════════╩════════════════╝) ║ ║ ║ ║ ║
╠══════════════════════════╣ ╚════════════════╬══════════════════════════════════════╣
║ ║ ║ ║
║ `(variable-not-in ,e2 ,t)║ ║ (2-vnis v1 v2 e L) ║
║ ║ ║ ║
╚══════════════════════════╩════════════════════════════════════════════════════════════════════════════════════════════════════════════╩══════════════════════════════════════╝)
(define (2-vnis v1 v2 e L)
(match-define `(variable-not-in ,e1 ,s1) v1)
(match-define `(variable-not-in ,e2 ,s2) v2)
(cond
[(not (and (symbol? s1) (symbol? s2)))
(displayln (list s1 s2))
(define s-res (unify* s1 s2 e L))
(and/fail s-res
`(variable-not-in (list ,e1 ,e2) ,s-res))]
[(sym-pref? s1 s2)
`(variable-not-in (list ,e1 ,e2) s2)]
[(sym-pref? s2 s1)
`(variable-not-in (list ,e1 ,e2) s1)]
[else (unif-fail)]))
(define (sym-pref? sp s) (define (sym-pref? sp s)
(regexp-match (regexp-match
@ -780,24 +810,25 @@
[_ [_
(values (lvar id) res)])) (values (lvar id) res)]))
(provide check-nt) (provide check-nt
normalize-pat)
(define check-nt (define check-nt
(let ([memo (hash)]) (let ([memo (hash)])
(λ (nt clang pat) (λ (nt clang pat)
(define npat (normalize-pat pat)) (define npat (normalize-pat clang pat))
(hash-ref memo (list nt clang npat) (hash-ref memo (list nt clang npat)
(λ () (λ ()
(define pat-ok? (define pat-ok?
(for/or ([ntp (in-list (map normalize-pat (nt-pats nt clang)))]) (for/or ([ntp (in-list (map ((curry normalize-pat) clang) (nt-pats nt clang)))])
(not-failed? (unify* npat ntp #f empty-lang)))) (not-failed? (unify* npat ntp #f empty-lang))))
(set! memo (set! memo
(hash-set memo (list nt clang npat) pat-ok?)) (hash-set memo (list nt clang npat) pat-ok?))
pat-ok?))))) pat-ok?)))))
(define (normalize-pat pat) (define (normalize-pat lang pat)
(let loop ([pat pat]) (let loop ([pat pat])
(match-a-pattern pat (match-a-pattern #:allow-else pat
[`any pat] [`any pat]
[`number pat] [`number pat]
[`string pat] [`string pat]
@ -809,27 +840,34 @@
[`(variable-except ,s ...) `variable] [`(variable-except ,s ...) `variable]
[`(variable-prefix ,s) `variable] [`(variable-prefix ,s) `variable]
[`variable-not-otherwise-mentioned pat] [`variable-not-otherwise-mentioned pat]
[`hole (error "can't normalize pattern: ~s" pat)] [`hole (error 'normalize-pat "can't normalize pattern: ~s" pat)]
[`(nt ,id) `any] [`(nt ,id)
(loop (hash-ref (compiled-lang-collapsible-nts lang) id 'any))]
[`(name ,name ,npat) [`(name ,name ,npat)
(if (bound? npat) (if (bound? npat)
`any `any
`(name ,name ,(loop npat)))] `(name ,name ,(loop npat)))]
[`(mismatch-name ,name ,pat) (loop pat)] [`(mismatch-name ,name ,pat) (loop pat)]
[`(in-hole ,p1 ,p2) (error "can't normalize pattern: ~s" pat)] [`(in-hole ,p1 ,p2) (error 'normalize-pat "can't normalize pattern: ~s" pat)]
[`(hide-hole ,p) (loop p)] [`(hide-hole ,p) (loop p)]
[`(side-condition ,p ,g ,e) [`(side-condition ,p ,g ,e)
(error "can't normalize pattern: ~s" pat)] (error 'normalize-pat "can't normalize pattern: ~s" pat)]
[`(cross ,s) (error "can't normalize pattern: ~s" pat)] [`(cross ,s) (error 'normalize-pat "can't normalize pattern: ~s" pat)]
[`(list ,sub-pats ...) [`(list ,sub-pats ...)
`(list ,@(for/list ([sub-pat (in-list sub-pats)]) `(list ,@(for/list ([sub-pat (in-list sub-pats)])
(match sub-pat (match sub-pat
[`(repeat ,pat ,name ,mismatch) [`(repeat ,pat ,name ,mismatch)
(error "can't normalize pattern: ~s" pat)] (error 'normalize-pat "can't normalize pattern: ~s" sub-pat)]
[_ [_
(loop sub-pat)])))] (loop sub-pat)])))]
[(? (compose not pair?)) [(? (compose not pair?))
pat]))) pat]
[_
(match pat
[`(variable-not-in ,p ,s)
`variable])])))
(provide nt-pats)
(define (nt-pats nt lang) (define (nt-pats nt lang)
(define this-rhs (define this-rhs
@ -868,6 +906,8 @@
`(name ,new-id ,(fresh-pat-vars pat instantiations))] `(name ,new-id ,(fresh-pat-vars pat instantiations))]
[`(list ,pats ...) [`(list ,pats ...)
`(list ,@(for/list ([p pats]) (fresh-pat-vars p instantiations)))] `(list ,@(for/list ([p pats]) (fresh-pat-vars p instantiations)))]
[`(variable-not-in ,pat ,s)
`(variable-not-in ,(fresh-pat-vars pat instantiations) ,s)]
[_ pre-pat])) [_ pre-pat]))
(define (make-uid id) (define (make-uid id)

159
pkgs/redex-pkgs/redex-lib/redex/private/search.rkt
View File

@ -69,14 +69,14 @@
(define name-nums 0) (define name-nums 0)
(define fresh-pat (parameterize ([unique-name-nums 0]) (define fresh-pat (parameterize ([unique-name-nums 0])
(begin0 (begin0
(fresh-pat-vars input (make-hash)) (fresh-pat-vars input (make-hash))
(set! name-nums (unique-name-nums))))) (set! name-nums (unique-name-nums)))))
(define fs (list (fail-cont empty-env (define fs (list (fail-cont empty-env
(list (make-partial-rule fresh-pat (if (shuffle-clauses?) (list (make-partial-rule fresh-pat (if (shuffle-clauses?)
(shuffle clauses) (shuffle clauses)
(order-clauses clauses)) (order-clauses clauses))
'() bound)) '() bound))
bound))) bound)))
(define v-locs (make-hash)) (define v-locs (make-hash))
(λ () (λ ()
(parameterize ([unique-name-nums name-nums] (parameterize ([unique-name-nums name-nums]
@ -93,11 +93,12 @@
(values (and/fail env/f (unify fresh-pat 'any env/f lang)) (values (and/fail env/f (unify fresh-pat 'any env/f lang))
fails))) fails)))
(set-last-gen-trace! (generation-trace)) (set-last-gen-trace! (generation-trace))
(when (success-jump?) (set! fs (if (success-jump?)
(set! fs (shuffle-fails fails))) ;; how to test if we're randomizing here? fails
(shuffle-fails fails))) ;; how to test if we're randomizing here?
(set! name-nums (unique-name-nums)) (set! name-nums (unique-name-nums))
ans))) ans)))
(define (trim-fails fs) (define (trim-fails fs)
(define rev-fs (reverse fs)) (define rev-fs (reverse fs))
(reverse (reverse
@ -131,44 +132,43 @@
(define (push-down a-partial-rule env fringe fail) (define (push-down a-partial-rule env fringe fail)
(inc-pushdown-count) (inc-pushdown-count)
(match a-partial-rule (match-define (partial-rule pat clauses tr-loc bound) a-partial-rule)
[(partial-rule pat clauses tr-loc bound) (check-depth-limits bound tr-loc fail)
(check-depth-limits bound tr-loc fail) (cond
[(null? clauses)
(fail-back fail)]
[else
(define the-clause (fresh-clause-vars (car clauses)))
(define res-pe (do-unification the-clause pat env))
(when (log-receiver? gen-log-recv)
(log-message (current-logger) 'info (symbol->string (clause-name the-clause))
(gen-trace tr-loc the-clause pat (and res-pe #t) bound env)))
(define failure-fringe
(cons (struct-copy partial-rule
a-partial-rule
[clauses (cdr clauses)])
fringe))
(cond (cond
[(null? clauses) [(not res-pe)
(fail-back fail)] (choose-rule env failure-fringe fail)]
[else [else
(define the-clause (fresh-clause-vars (car clauses))) (define new-fringe-elements
(define res-pe (do-unification the-clause pat env)) (for/list ([prem (in-list (clause-prems the-clause))]
(when (log-receiver? gen-log-recv) [n (in-naturals)])
(log-message (current-logger) 'info (symbol->string (clause-name the-clause)) (define prem-cls (prem-clauses prem))
(gen-trace tr-loc the-clause pat (and res-pe #t) bound env))) (make-partial-rule (prem-pat prem)
(define failure-fringe (if (positive? bound)
(cons (struct-copy partial-rule (if (shuffle-clauses?)
a-partial-rule (shuffle prem-cls)
[clauses (cdr clauses)]) (order-clauses prem-cls))
fringe)) (order-clauses prem-cls))
(cond (cons n tr-loc)
[(not res-pe) (- bound 1))))
(choose-rule env failure-fringe fail)] (define new-fringe (append new-fringe-elements
[else fringe))
(define new-fringe-elements (choose-rule (p*e-e res-pe)
(for/list ([prem (in-list (clause-prems the-clause))] new-fringe
[n (in-naturals)]) (cons (fail-cont env failure-fringe bound) fail))])]))
(define prem-cls (prem-clauses prem))
(make-partial-rule (prem-pat prem)
(if (positive? bound)
(if (shuffle-clauses?)
(shuffle prem-cls)
(order-clauses prem-cls))
(order-clauses prem-cls))
(cons n tr-loc)
(- bound 1))))
(define new-fringe (append new-fringe-elements
fringe))
(choose-rule (p*e-e res-pe)
new-fringe
(cons (fail-cont env failure-fringe bound) fail))])])]))
(define (order-clauses cs) (define (order-clauses cs)
(define num-prems->cs (hash)) (define num-prems->cs (hash))
@ -184,37 +184,36 @@
(apply append (apply append
(for/list ([k (sort (hash-keys num-prems->cs) <)]) (for/list ([k (sort (hash-keys num-prems->cs) <)])
(shuffle (set->list (hash-ref num-prems->cs k)))))) (shuffle (set->list (hash-ref num-prems->cs k))))))
(define (do-unification clse input env) (define (do-unification clse input env)
(match clse (match-define (clause head-pat eq/dqs prems lang name) clse)
[(clause head-pat eq/dqs prems lang name) (clause head-pat eq/dqs prems lang name)
(define-values (eqs dqs) (partition eqn? eq/dqs)) (define-values (eqs dqs) (partition eqn? eq/dqs))
(define env1 (define env1
(let loop ([e env] (let loop ([e env]
[dqs dqs]) [dqs dqs])
(match dqs (match dqs
['() e] ['() e]
[(cons (dqn ps lhs rhs) rest) [(cons (dqn ps lhs rhs) rest)
(dqn ps lhs rhs) (define u-res (disunify ps lhs rhs e lang))
(define u-res (disunify ps lhs rhs e lang)) (and u-res
(and u-res (loop u-res rest))])))
(loop u-res rest))]))) (define head-p*e (and/fail env1 (unify input head-pat env1 lang)))
(define head-p*e (and/fail env1 (unify input head-pat env1 lang))) (cond
(cond [(not-failed? head-p*e)
[(not-failed? head-p*e) (define res-p (p*e-p head-p*e))
(define res-p (p*e-p head-p*e)) (let loop ([e (p*e-e head-p*e)]
(let loop ([e (p*e-e head-p*e)] [eqs eqs])
[eqs eqs]) (match eqs
(match eqs ['()
['() (p*e (p*e-p head-p*e) e)]
(p*e (p*e-p head-p*e) e)] [(cons (eqn lhs rhs) rest)
[(cons (eqn lhs rhs) rest) (define u-res (unify lhs rhs e lang))
(define u-res (unify lhs rhs e lang)) (and (not-failed? u-res)
(and (not-failed? u-res) (loop (p*e-e u-res) rest))]))]
(loop (p*e-e u-res) rest))]))] [else #f]))
[else #f])]))
(define (fresh-clause-vars clause-raw) (define (fresh-clause-vars clause-raw)
(define instantiations (make-hash)) (define instantiations (make-hash))
@ -227,10 +226,10 @@
(fresh-pat-vars rhs instantiations))] (fresh-pat-vars rhs instantiations))]
[(dqn ps lhs rhs) [(dqn ps lhs rhs)
(dqn (map (λ (id) (hash-ref instantiations id (dqn (map (λ (id) (hash-ref instantiations id
(λ () (λ ()
(define unique-id (make-uid id)) (define unique-id (make-uid id))
(hash-set! instantiations id unique-id) (hash-set! instantiations id unique-id)
unique-id))) unique-id)))
ps) ps)
(fresh-pat-vars lhs instantiations) (fresh-pat-vars lhs instantiations)
(fresh-pat-vars rhs instantiations))]))] (fresh-pat-vars rhs instantiations))]))]
@ -244,13 +243,15 @@
(define (check-depth-limits bound tr-loc fails) (define (check-depth-limits bound tr-loc fails)
(when ((pushdown-count) . > . (pushdown-limit)) (when ((pushdown-count) . > . (pushdown-limit))
(define str (format "pushdown count of ~s exceeded at ~s" (pushdown-count) tr-loc)) (define str (format "pushdown count of ~s exceeded at ~s" (pushdown-count) tr-loc))
;(printf "!*\n\t~s\t*!\n" str) (printf "!*\n\t~s\t*!\n" str)
(raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails))) (raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails)))
(when (> (bt-count) (bt-limit)) (when (> (bt-count) (bt-limit))
(define str (format "backtrack count of ~s exceeded at ~s" (bt-limit) tr-loc)) (define str (format "backtrack count of ~s exceeded at ~s" (bt-limit) tr-loc))
(displayln str)
(raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails))) (raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails)))
(when (> (length tr-loc) (* 3 (+ (length tr-loc) bound))) (when (> (length tr-loc) (* 3 (+ (length tr-loc) bound)))
(define str (format "depth bound exceeded at depth: ~s" (length tr-loc))) (define str (format "depth bound exceeded at depth: ~s" (length tr-loc)))
(displayln str)
(raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails)))) (raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails))))

10
pkgs/redex-pkgs/redex-lib/redex/private/term.rkt
View File

@ -8,6 +8,7 @@
(only-in racket/list flatten) (only-in racket/list flatten)
"keyword-macros.rkt" "keyword-macros.rkt"
"matcher.rkt") "matcher.rkt")
(only-in "fresh.rkt" variable-not-in)
syntax/datum syntax/datum
"error.rkt" "error.rkt"
"lang-struct.rkt" "lang-struct.rkt"
@ -330,9 +331,16 @@
(d->pat #'d names)])) (d->pat #'d names)]))
(define-for-syntax (d->pat d names) (define-for-syntax (d->pat d names)
(syntax-case d (... undatum in-hole undatum-splicing) (syntax-case d (... undatum in-hole undatum-splicing variable-not-in term quote)
[() [()
#'(list)] #'(list)]
[(undatum (variable-not-in (term t) (quote s)))
(with-syntax ([t-pat (d->pat #'t names)])
#'(variable-not-in t-pat s))]
[(undatum (variable-not-in (term t1) (term t2)))
(with-syntax ([t1-pat (d->pat #'t1 names)]
[t2-pat (d->pat #'t2 names)])
#'(variable-not-in t1-pat t2-pat))]
[(undatum rest ...) ;; holes are also undatumed [(undatum rest ...) ;; holes are also undatumed
d] d]
[(undatum-splicing rest ...) [(undatum-splicing rest ...)