redex: unfold nts once during unification
Also: * add a backtracking limit * check for ground terms in both term and pat environments when filling in generated patterns * update tests to be consistent with the above
This commit is contained in:
Burke Fetscher
parent
71bc329278
commit
2ebc200d3d
|
|
@ -32,9 +32,12 @@
|
|||
(let recur ([p p])
|
||||
(match p
|
||||
[(lvar id)
|
||||
(recur (hash-ref eqs p))]
|
||||
;; careful! term-e has terms, eqs has pats!
|
||||
(hash-ref term-e p
|
||||
(λ () (recur (hash-ref eqs p))))]
|
||||
[`(name ,id ,(bound))
|
||||
(recur (hash-ref eqs (lvar id)))]
|
||||
(hash-ref term-e (lvar id)
|
||||
(λ () (recur (hash-ref eqs (lvar id)))))]
|
||||
[`(list ,ps ...)
|
||||
`(,@(for/list ([p ps]) (recur p)))]
|
||||
[`(cstr (,nts ...) ,p)
|
||||
|
|
@ -61,16 +64,16 @@
|
|||
[`(nt ,p-nt)
|
||||
(define all-nts (cons p-nt nts))
|
||||
(for/not-failed ([nt-pat all-nts])
|
||||
(define term (recur `(nt ,nt-pat)))
|
||||
(and/fail (for/and ([nt (remove nt-pat all-nts)])
|
||||
((get-matcher nt) term))
|
||||
term))]
|
||||
(define term (recur `(nt ,nt-pat)))
|
||||
(and/fail (for/and ([nt (remove nt-pat all-nts)])
|
||||
((get-matcher nt) term))
|
||||
term))]
|
||||
[`any
|
||||
(for/not-failed ([nt-pat nts])
|
||||
(define term (recur `(nt ,nt-pat)))
|
||||
(and/fail (for/and ([nt (remove nt-pat nts)])
|
||||
((get-matcher nt) term))
|
||||
term))]
|
||||
(define term (recur `(nt ,nt-pat)))
|
||||
(and/fail (for/and ([nt (remove nt-pat nts)])
|
||||
((get-matcher nt) term))
|
||||
term))]
|
||||
[_
|
||||
(define term (recur pat))
|
||||
(and/fail (for/and ([nt nts])
|
||||
|
|
|
|||
|
|
@ -151,6 +151,7 @@
|
|||
;; disqequations generated (by mismatch-pattern) during a given unification pass
|
||||
(define dqs-found (make-parameter (make-hash)))
|
||||
|
||||
|
||||
;; pat pat env -> (or/c p*e #f)
|
||||
(define (unify t u e L)
|
||||
(parameterize ([dqs-found (make-hash)])
|
||||
|
|
@ -161,20 +162,22 @@
|
|||
(not-failed? u*)
|
||||
(unify* t* u* eqs L)))
|
||||
(and/fail (not-failed? res)
|
||||
(let* ([static-eqs (hash/mut->imm eqs)]
|
||||
[found-pre-dqs
|
||||
(apply set-union (set)
|
||||
(for/list ([dq-sides/id (hash-values (dqs-found))])
|
||||
(list->dq-pairs dq-sides/id)))]
|
||||
[found-dqs
|
||||
(for/list ([pdq found-pre-dqs])
|
||||
(disunify* '() (first pdq) (second pdq) (hash-copy static-eqs) L))])
|
||||
(and/fail (for/and ([d found-dqs]) d)
|
||||
(let* ([real-dqs (filter (λ (dq) (not (boolean? dq))) found-dqs)]
|
||||
[new-dqs (check-and-resimplify static-eqs (append real-dqs (env-dqs e)) L)])
|
||||
(and/fail new-dqs
|
||||
(p*e res
|
||||
(env static-eqs new-dqs)))))))))
|
||||
(let* ([static-eqs (hash/mut->imm (let ([ans eqs])
|
||||
;(printf "1.1\n")
|
||||
ans))]
|
||||
[found-pre-dqs
|
||||
(apply set-union (set)
|
||||
(for/list ([dq-sides/id (hash-values (dqs-found))])
|
||||
(list->dq-pairs dq-sides/id)))]
|
||||
[found-dqs
|
||||
(for/list ([pdq found-pre-dqs])
|
||||
(disunify* '() (first pdq) (second pdq) (hash-copy static-eqs) L))])
|
||||
(and/fail (for/and ([d found-dqs]) d)
|
||||
(let* ([real-dqs (filter (λ (dq) (not (boolean? dq))) found-dqs)]
|
||||
[new-dqs (check-and-resimplify static-eqs (append real-dqs (env-dqs e)) L)])
|
||||
(and/fail new-dqs
|
||||
(p*e res
|
||||
(env static-eqs new-dqs)))))))))
|
||||
|
||||
(define (list->dq-pairs dq-sides)
|
||||
(cond
|
||||
|
|
@ -186,6 +189,7 @@
|
|||
(list (car dq-sides) rhs))
|
||||
(list->dq-pairs (cdr dq-sides)))]))
|
||||
|
||||
|
||||
;; pat pat env lang -> (or/c env #f)
|
||||
(define (disunify params t u e L)
|
||||
(parameterize ([new-eqs (make-hash)])
|
||||
|
|
@ -259,7 +263,7 @@
|
|||
|
||||
|
||||
(define (hash/mut->imm h0)
|
||||
(for/fold ([h (hash)])
|
||||
(for/fold ([h (hash)])
|
||||
([(k v) (in-hash h0)])
|
||||
(hash-set h k v)))
|
||||
|
||||
|
|
@ -397,11 +401,13 @@
|
|||
(unify* u t e L)]
|
||||
;; cstrs
|
||||
[(`(cstr (,nts1 ...) ,p1) `(cstr (,nts2 ...) ,p2))
|
||||
(let ([res (unify* p1 p2 e L)])
|
||||
(let ([res (unify* p1 p2 e L)]
|
||||
[new-nts (merge-ids/sorted nts1 nts2 L)])
|
||||
(and/fail (not-failed? res)
|
||||
new-nts
|
||||
(when (lvar? res)
|
||||
(error 'unify* "unify* returned lvar as result: ~s\n~s\n~s\n" p1 p2 e))
|
||||
`(cstr ,(merge-ids/sorted nts1 nts2) ,res)))]
|
||||
`(cstr ,new-nts ,res)))]
|
||||
[(`(cstr ,nts ,p) _)
|
||||
(let ([res (unify* p u e L)])
|
||||
(and/fail (not-failed? res)
|
||||
|
|
@ -409,12 +415,16 @@
|
|||
[(lvar id)
|
||||
(error 'unify* "unify* returned lvar as result: ~s\n~s\n~s\n" p u e)]
|
||||
[`(nt ,nt)
|
||||
`(cstr ,(merge-ids/sorted (list nt) nts)
|
||||
,p)]
|
||||
(define new-nts (merge-ids/sorted (list nt) nts L))
|
||||
(and/fail new-nts
|
||||
`(cstr ,new-nts ,p))]
|
||||
[`(cstr ,nts2 ,new-p)
|
||||
`(cstr ,(merge-ids/sorted nts nts2) ,new-p)]
|
||||
(define new-nts (merge-ids/sorted nts nts2 L))
|
||||
(and/fail new-nts
|
||||
`(cstr ,new-nts ,new-p))]
|
||||
[_
|
||||
`(cstr ,nts ,res)])))]
|
||||
(and/fail (for/and ([n nts]) (check-nt n L res))
|
||||
`(cstr ,nts ,res))])))]
|
||||
[(_ `(cstr ,nts ,p))
|
||||
(unify* `(cstr ,nts ,p) t e L)]
|
||||
;; nts
|
||||
|
|
@ -423,13 +433,15 @@
|
|||
(hash-ref (compiled-lang-collapsible-nts L) n)
|
||||
`(nt ,n))]
|
||||
[(`(nt ,p) u)
|
||||
(if (hash-has-key? (compiled-lang-collapsible-nts L) p)
|
||||
(unify* (hash-ref (compiled-lang-collapsible-nts L) p) u e L)
|
||||
(let ([res (unify* u u e L)])
|
||||
(and/fail (not-failed? res)
|
||||
(when (lvar? res)
|
||||
(error 'unify* "unify* returned lvar as result: ~s\n~s\n~s\n" u u e))
|
||||
`(cstr (,p) ,res))))]
|
||||
(and/fail
|
||||
(check-nt p L u)
|
||||
(if (hash-has-key? (compiled-lang-collapsible-nts L) p)
|
||||
(unify* (hash-ref (compiled-lang-collapsible-nts L) p) u e L)
|
||||
(let ([res (unify* u u e L)]) ;; look at structure of nt here?
|
||||
(and/fail (not-failed? res)
|
||||
(when (lvar? res)
|
||||
(error 'unify* "unify* returned lvar as result: ~s\n~s\n~s\n" u u e))
|
||||
`(cstr (,p) ,res)))))]
|
||||
[(_ `(nt ,p))
|
||||
(unify* `(nt ,p) t e L)]
|
||||
;; other pat stuff
|
||||
|
|
@ -610,8 +622,10 @@
|
|||
[(_ _)
|
||||
(equal? p* u*)]))
|
||||
|
||||
(define (merge-ids/sorted l1 l2)
|
||||
(de-dupe/sorted (merge/sorted l1 l2)))
|
||||
(define (merge-ids/sorted l1 l2 lang)
|
||||
(and (for*/and ([nt1 l1] [nt2 l2])
|
||||
(check-nt nt1 lang `(nt ,l2)))
|
||||
(de-dupe/sorted (merge/sorted l1 l2))))
|
||||
|
||||
(define (symbol<? s1 s2)
|
||||
(string<? (symbol->string s1) (symbol->string s2)))
|
||||
|
|
@ -672,3 +686,72 @@
|
|||
[_
|
||||
(values (lvar id) res)]))
|
||||
|
||||
(provide check-nt)
|
||||
|
||||
(define check-nt
|
||||
(let ([memo (hash)])
|
||||
(λ (nt clang pat)
|
||||
(define npat (normalize-pat pat))
|
||||
(hash-ref memo (list nt clang npat)
|
||||
(λ ()
|
||||
(define pat-ok?
|
||||
(for/or ([ntp (in-list (map normalize-pat (nt-pats nt clang)))])
|
||||
(not-failed? (unify* npat ntp #f empty-lang))))
|
||||
(set! memo
|
||||
(hash-set memo (list nt clang npat) pat-ok?)))))))
|
||||
|
||||
(define (normalize-pat pat)
|
||||
(let loop ([pat pat])
|
||||
(match-a-pattern pat
|
||||
[`any pat]
|
||||
[`number pat]
|
||||
[`string pat]
|
||||
[`natural pat]
|
||||
[`integer pat]
|
||||
[`real pat]
|
||||
[`boolean pat]
|
||||
[`variable pat]
|
||||
[`(variable-except ,s ...) `variable]
|
||||
[`(variable-prefix ,s) `variable]
|
||||
[`variable-not-otherwise-mentioned pat]
|
||||
[`hole (error "can't normalize pattern: ~s" pat)]
|
||||
[`(nt ,id) `any]
|
||||
[`(name ,name ,npat)
|
||||
(if (bound? npat)
|
||||
`any
|
||||
`(name ,name ,(loop npat)))]
|
||||
[`(mismatch-name ,name ,pat) (loop pat)]
|
||||
[`(in-hole ,p1 ,p2) (error "can't normalize pattern: ~s" pat)]
|
||||
[`(hide-hole ,p) (loop p)]
|
||||
[`(side-condition ,p ,g ,e)
|
||||
(error "can't normalize pattern: ~s" pat)]
|
||||
[`(cross ,s) (error "can't normalize pattern: ~s" pat)]
|
||||
[`(list ,sub-pats ...)
|
||||
`(list ,@(for/list ([sub-pat (in-list sub-pats)])
|
||||
(match sub-pat
|
||||
[`(repeat ,pat ,name ,mismatch)
|
||||
(error "can't normalize pattern: ~s" pat)]
|
||||
[else
|
||||
(loop sub-pat)])))]
|
||||
[(? (compose not pair?))
|
||||
pat])))
|
||||
|
||||
(define (nt-pats nt lang)
|
||||
(define this-rhs
|
||||
(nt-rhs
|
||||
(let ([the-nt (findf (λ (lang-nt)
|
||||
(equal? nt (nt-name lang-nt)))
|
||||
(compiled-lang-lang lang))])
|
||||
(unless the-nt
|
||||
(error 'unify "nonterminal ~s not found for provided language... nts found: ~s"
|
||||
nt (hash-keys (compiled-lang-nt-map lang))))
|
||||
the-nt)))
|
||||
(match this-rhs
|
||||
[(list (rhs `(nt ,alias)))
|
||||
(nt-pats alias lang)]
|
||||
[_
|
||||
(map rhs-pattern this-rhs)]))
|
||||
|
||||
(define empty-lang
|
||||
(compiled-lang
|
||||
#f #f #f #f #f #f #f #f #f #f '() #f (hash)))
|
||||
|
|
|
|||
|
|
@ -45,6 +45,12 @@
|
|||
|
||||
(define-struct gen-trace (tr-loc clause input state bound env) #:prefab)
|
||||
|
||||
|
||||
(define bt-count (make-parameter 0))
|
||||
(define BT-LIMIT 40)
|
||||
(define (inc-bt-count)
|
||||
(bt-count (add1 (bt-count))))
|
||||
|
||||
(define (search/next clauses input bound lang)
|
||||
(define name-nums 0)
|
||||
(define fresh-pat (parameterize ([unique-name-nums 0])
|
||||
|
|
@ -57,7 +63,7 @@
|
|||
(define v-locs (make-hash))
|
||||
(λ ()
|
||||
(parameterize ([unique-name-nums name-nums]
|
||||
[visited-locs v-locs])
|
||||
[bt-count 0])
|
||||
(define-values (ans fails)
|
||||
(with-handlers ([exn:fail:redex:search-failure? (λ (e)
|
||||
(define f-conts (exn:fail:redex:search-failure-fails e))
|
||||
|
|
@ -69,7 +75,6 @@
|
|||
(set-last-gen-trace! (generation-trace))
|
||||
(set! fs (shuffle-fails fails)) ;; how to test if we're randomizing here?
|
||||
(set! name-nums (unique-name-nums))
|
||||
(set! v-locs (visited-locs))
|
||||
ans)))
|
||||
|
||||
(define (trim-fails fs)
|
||||
|
|
@ -90,6 +95,7 @@
|
|||
[else fs]))
|
||||
|
||||
(define (fail-back fs)
|
||||
(inc-bt-count)
|
||||
(match fs
|
||||
[(list (fail-cont e f b) rest ...)
|
||||
(choose-rule e f rest)]
|
||||
|
|
@ -100,10 +106,7 @@
|
|||
[(empty? fringe)
|
||||
(values env fail)]
|
||||
[else
|
||||
(define new-f fringe)
|
||||
(if new-f
|
||||
(push-down (car new-f) env (cdr new-f) fail)
|
||||
(fail-back fail))]))
|
||||
(push-down (car fringe) env (cdr fringe) fail)]))
|
||||
|
||||
(define (push-down a-partial-rule env fringe fail)
|
||||
(match a-partial-rule
|
||||
|
|
@ -184,7 +187,6 @@
|
|||
['()
|
||||
(p*e (p*e-p head-p*e) e)]
|
||||
[(cons (eqn lhs rhs) rest)
|
||||
(eqn lhs rhs)
|
||||
(define u-res (unify lhs rhs e lang))
|
||||
(and (not-failed? u-res)
|
||||
(loop (p*e-e u-res) rest))]))]
|
||||
|
|
@ -236,38 +238,18 @@
|
|||
[(prem mk-clauses pat)
|
||||
(prem mk-clauses (fresh-pat-vars pat instantiations))]))]))
|
||||
|
||||
(define visited-locs (make-parameter (make-hash)))
|
||||
|
||||
(define-struct (exn:fail:redex:search-failure exn:fail:redex) (fails))
|
||||
|
||||
(define (check-depth-limits bound tr-loc fails)
|
||||
(when (> (bt-count) BT-LIMIT)
|
||||
(define str (format "backtrack count of ~s exceeded at ~s" BT-LIMIT tr-loc))
|
||||
(raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails)))
|
||||
(when (> (length tr-loc) (* 3 (+ (length tr-loc) bound)))
|
||||
(define str (format "depth bound exceeded at depth: ~s" (length tr-loc)))
|
||||
(raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails))))
|
||||
|
||||
(define (check-backtrack-limits tr-loc)
|
||||
(define v-locs (visited-locs))
|
||||
(when (< 5 (hash-ref v-locs tr-loc 0))
|
||||
(define str (format "backtracking limit exceeded at location: ~s" tr-loc))
|
||||
(raise (make-exn:fail:redex:search-failure str (current-continuation-marks))))
|
||||
(define loc-count (hash-ref v-locs tr-loc 0))
|
||||
(for ([(k v) (in-hash v-locs)])
|
||||
(let loop ([l1 tr-loc]
|
||||
[l2 k])
|
||||
(cond
|
||||
[(null? l1)
|
||||
(void)]
|
||||
[(null? l2)
|
||||
(hash-set! v-locs k 0)]
|
||||
[(= (car l1) (car l2))
|
||||
(loop (cdr l1) (cdr l2))]
|
||||
[else
|
||||
(void)])))
|
||||
(hash-set! v-locs tr-loc (add1 (hash-ref v-locs tr-loc 0))))
|
||||
|
||||
(define unique-name-nums (make-parameter 0))
|
||||
|
||||
|
||||
(define generation-logger (make-logger 'generation-log (current-logger)))
|
||||
|
||||
(define gen-log-recv #f)
|
||||
|
|
|
|||
|
|
@ -254,7 +254,22 @@
|
|||
res-p
|
||||
res-p-bkwd)]))
|
||||
|
||||
(define-language L0)
|
||||
;; This looks really strange but it is for backwards compatability
|
||||
;; with tests that didn't take nonterminal productions into account.
|
||||
;; There nts will all (except n) accept anything, but since they
|
||||
;; have two productions they don't get collapsed (and so will create
|
||||
;; cstr's).
|
||||
(define-language L0
|
||||
(e any any)
|
||||
(q any any)
|
||||
(v any any)
|
||||
(b any any)
|
||||
(x any any)
|
||||
(Γ any any)
|
||||
(s any any)
|
||||
(a any any)
|
||||
(Q any any)
|
||||
(n number any))
|
||||
|
||||
|
||||
(check-equal? (unify/format `number `number (hash) L0)
|
||||
|
|
@ -540,7 +555,7 @@
|
|||
['boolean `(name x ,(bound)) (make-hash `((,(lvar 'x) . boolean)))]
|
||||
['variable `(name x ,(bound)) (make-hash `((,(lvar 'x) . variable)))]
|
||||
['variable-not-otherwise-mentioned `(name x ,(bound)) (make-hash `((,(lvar 'x) . variable-not-otherwise-mentioned)))]
|
||||
['(cstr (number) any) `(name x ,(bound)) (make-hash `((,(lvar 'x) . (cstr (number) any))))]
|
||||
['(cstr (n) any) `(name x ,(bound)) (make-hash `((,(lvar 'x) . (cstr (n) any))))]
|
||||
['(list 1 2) `(name x ,(bound)) (make-hash `((,(lvar 'x) . (list 1 2))))]
|
||||
['(mismatch-name z any) `(name x ,(bound)) (make-hash `((,(lvar 'x) . any)))]
|
||||
['(nt q) `(name x ,(bound)) (make-hash `((,(lvar 'x) . (cstr (q) any))))]))
|
||||
|
|
@ -555,7 +570,8 @@
|
|||
|
||||
(define-language ntl
|
||||
(n number)
|
||||
((x y) variable))
|
||||
((x y) variable)
|
||||
(Q any any))
|
||||
|
||||
(check-equal? (unify/format `(nt n) `any (hash) ntl)
|
||||
(p*e `number (hash)))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user