From dc8ae059c6f85c93a36e335df0898c5dcc2e6078 Mon Sep 17 00:00:00 2001 From: Burke Fetscher Date: Mon, 26 Aug 2013 13:19:53 -0500 Subject: [PATCH] Preprocess nt patterns in pattern unification. Specifically, correctly handle cases where an nt production has named patterns. --- .../redex-lib/redex/private/pat-unify.rkt | 48 ++++++++++++++----- .../redex-lib/redex/private/search.rkt | 24 ---------- .../redex-test/redex/tests/gen-test.rkt | 10 ++++ .../redex-test/redex/tests/unify-tests.rkt | 10 ++-- 4 files changed, 54 insertions(+), 38 deletions(-) diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt index f78a3e79bf..770d9bd29d 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt @@ -30,7 +30,10 @@ (struct-out unif-fail) not-failed? dq - predef-pat?) + predef-pat? + unique-name-nums + fresh-pat-vars + make-uid) ;; @@ -338,7 +341,7 @@ ;; which match both pat and pat*... ;; (those are the ones bind-names does nothing with) -;; bind-names : pat env lang -> pat* or #f +;; bind-names : pat env lang -> pat* or unif-fail (define (bind-names pat e L) (match pat [`(name ,name ,(bound)) @@ -383,7 +386,7 @@ [_ pat])) -;; unify* : pat* pat* env lang -> pat* or #f +;; unify* : pat* pat* env lang -> pat* or unif-fail (define (unify* t0 u0 e L) (define t (resolve t0 e)) (define u (resolve u0 e)) @@ -463,18 +466,18 @@ `(cstr ,nts ,res))])))) (define (u*-2nts n-t n-u e L) - (if (equal? n-t n-u) - (let ([n n-t]) - (if (hash-has-key? (compiled-lang-collapsible-nts L) n) - (hash-ref (compiled-lang-collapsible-nts L) n) - `(nt ,n))) - (u*-1nt n-t `(nt ,n-u) e L))) + (if (equal? n-t n-u) + `(nt ,n-t) + (u*-1nt n-t `(nt ,n-u) e L))) (define (u*-1nt p u e L) (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 ([p-bn (bind-names (fresh-pat-vars (hash-ref (compiled-lang-collapsible-nts L) p) (make-hash)) e L)]) + (and/fail + (not-failed? p-bn) + (unify* p-bn u e L))) (let ([res (unify* u u e L)]) ;; look at structure of nt here? (and/fail (not-failed? res) (when (lvar? res) @@ -762,4 +765,27 @@ (define empty-lang (compiled-lang #f #f #f #f #f #f #f #f #f #f '() #f (hash) - (lang-enumerators '()))) \ No newline at end of file + (lang-enumerators '()))) + +(define unique-name-nums (make-parameter 0)) + +;; TODO: compare with free-identifier=? so renaming is safe +;; w/r/t macro expansion +;; (use free-id-table) +(define (fresh-pat-vars pre-pat instantiations) + (match pre-pat + [`(name ,id ,pat) + (define new-id (hash-ref instantiations id + (λ () + (define unique-id (make-uid id)) + (hash-set! instantiations id unique-id) + unique-id))) + `(name ,new-id ,(fresh-pat-vars pat instantiations))] + [`(list ,pats ...) + `(list ,@(for/list ([p pats]) (fresh-pat-vars p instantiations)))] + [_ pre-pat])) + +(define (make-uid id) + (let ([uid-num (unique-name-nums)]) + (unique-name-nums (add1 uid-num)) + (string->symbol (string-append (symbol->string id) "_" (number->string uid-num))))) \ No newline at end of file diff --git a/pkgs/redex-pkgs/redex-lib/redex/private/search.rkt b/pkgs/redex-pkgs/redex-lib/redex/private/search.rkt index 002c8e34e5..915e62b925 100644 --- a/pkgs/redex-pkgs/redex-lib/redex/private/search.rkt +++ b/pkgs/redex-pkgs/redex-lib/redex/private/search.rkt @@ -215,29 +215,6 @@ (and (not-failed? u-res) (loop (p*e-e u-res) rest))]))] [else #f])])) - - - -;; TODO: compare with free-identifier=? so renaming is safe -;; w/r/t macro expansion -;; (use free-id-table) -(define (fresh-pat-vars pre-pat instantiations) - (match pre-pat - [`(name ,id ,pat) - (define new-id (hash-ref instantiations id - (λ () - (define unique-id (make-uid id)) - (hash-set! instantiations id unique-id) - unique-id))) - `(name ,new-id ,(fresh-pat-vars pat instantiations))] - [`(list ,pats ...) - `(list ,@(for/list ([p pats]) (fresh-pat-vars p instantiations)))] - [_ pre-pat])) - -(define (make-uid id) - (let ([uid-num (unique-name-nums)]) - (unique-name-nums (add1 uid-num)) - (string->symbol (string-append (symbol->string id) "_" (number->string uid-num))))) (define (fresh-clause-vars clause-raw) (define instantiations (make-hash)) @@ -276,7 +253,6 @@ (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 unique-name-nums (make-parameter 0)) (define generation-logger (make-logger 'generation-log (current-logger))) diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/gen-test.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/gen-test.rkt index 616b53cf60..b78c81fd53 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/gen-test.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/gen-test.rkt @@ -795,3 +795,13 @@ (test (gen-ith 0) 0) (test (gen-ith 1) 1))) +(let () + (define-language L + (e ::= (name aha! any))) + + (define-judgment-form L + #:mode (J I I) + [(J e e)]) + + (is-not-false + (generate-term L #:satisfying (J e_1 e_2) 10))) \ No newline at end of file diff --git a/pkgs/redex-pkgs/redex-test/redex/tests/unify-tests.rkt b/pkgs/redex-pkgs/redex-test/redex/tests/unify-tests.rkt index 1c8b1b0e9e..d4b116f889 100644 --- a/pkgs/redex-pkgs/redex-test/redex/tests/unify-tests.rkt +++ b/pkgs/redex-pkgs/redex-test/redex/tests/unify-tests.rkt @@ -587,8 +587,12 @@ (p*e 'variable (hash))) (check-equal? (unify/format `(nt y) 'any (hash) ntl) (p*e 'variable (hash))) + ;; asymmetry ok here - if the nt doesn't get unified against, + ;; it doesn't get collapsed (check-equal? (unify/format `(nt y) '(nt Q) (hash) ntl) - (p*e '(cstr (Q) variable) (hash))) + `(different-orders=>different-results + ,(p*e '(cstr (Q) variable) (env (hash) '())) + ,(p*e '(cstr (Q) (nt y)) (env (hash) '())))) ) @@ -820,7 +824,7 @@ (p*e `(list λ y (name e_2 ,(bound))) (m-hash (lvar 'e_2) `(cstr (e) 3)))) (u-test λn (λ x 3) (λ x e_2) (hash) (p*e `(list λ (name x ,(bound)) (name e_2 ,(bound))) - (m-hash (lvar 'e_2) `(cstr (e) 3) (lvar 'x) `variable-not-otherwise-mentioned))) + (m-hash (lvar 'e_2) `(cstr (e) 3) (lvar 'x) `(nt x)))) (u-fails λn (λ x 3) (e_1 e_2) (hash)) (u-test λn (e_1 e_2) ((λ x x) 3) (hash) (p*e `(list (name e_1 ,(bound)) (name e_2 ,(bound))) @@ -829,7 +833,7 @@ (lvar 'e_1) `(cstr (e) (list λ (name x ,(bound)) (name x ,(bound)))) (lvar 'x) - `variable-not-otherwise-mentioned))) + `(nt x)))) (define-language p-types (t (t -> t)