From 7169c0e53e35d6a504fcd17d7973baf1b200ef0e Mon Sep 17 00:00:00 2001 From: Steven Jaconette Date: Mon, 20 Sep 2010 09:25:07 -0500 Subject: [PATCH] Second patch for redex compiler -Fixes some bugs in the model -Cleans up some unused code -Adds the test cases --- collects/redex/private/compiler/match.rkt | 1380 +++-------------- .../redex/private/compiler/redextomatrix.rkt | 290 ++-- .../redex/tests/compiler/matrix-tests.rkt | 193 +++ collects/redex/tests/compiler/redex-tests.rkt | 876 +++++++++++ collects/redex/tests/matcher-test.rkt | 4 + 5 files changed, 1352 insertions(+), 1391 deletions(-) create mode 100644 collects/redex/tests/compiler/matrix-tests.rkt create mode 100644 collects/redex/tests/compiler/redex-tests.rkt diff --git a/collects/redex/private/compiler/match.rkt b/collects/redex/private/compiler/match.rkt index e25ae41c28..fc75214b05 100644 --- a/collects/redex/private/compiler/match.rkt +++ b/collects/redex/private/compiler/match.rkt @@ -6,29 +6,41 @@ Build-Cond Cond-List simplify - simple-swap - compile) + compile + Get-Pvar) (define hole-table (make-hash)) (define the-hole (term hole)) +(define no-context #f) +(define in-context #t) +(define ∅ #f) +(define context-match (make-parameter no-context)) +(define (variable-prefix? x y) + (let* ([prefix-str (symbol->string x)] + [prefix-len (string-length prefix-str)]) + (and (symbol? y) + (let ([str (symbol->string y)]) + (and ((string-length str) . >= . prefix-len) + (string=? (substring str 0 prefix-len) prefix-str)))))) +(define rev (λ (x) + (if (cons? x) + (reverse x) + x))) (define new-var-list '()) (define-language L [e (cond [e e] ...) (let ((x e) ...) e) - ;(term-let ((x e) ...) e) (e e ...) m b] [v (cond [v v] ...) (let ((x v) ...) v) - ;(term-let ((x v) ...) v) (v v ...) b] [b empty - plug reverse append @@ -51,10 +63,8 @@ curry pair-path-append path-append - ; we don't have these functions yet variable-except? variable-prefix? - ; () begin ∪ @@ -72,13 +82,11 @@ x 'variable 'any - variable-not-otherwise-mentioned not = '() - ; ambiguous term-let - ] + variable-not-otherwise-mentioned] [bool #t #f] [Context @@ -89,7 +97,6 @@ [Context e] [e e] ...) (let ((x v) ...) v ... Context e ...) - ;(term-let ((x v) ...) v ... Context e ...) (v ... Context e ...) hole] [m (matrix (x ...) (row ...) (pvar ...) (pvar ...) natural bool)] @@ -102,6 +109,7 @@ (cdr eq) (cons eq eq) (plug eq eq) + (append eq eq) lit-hole] (p (or p p) lit-hole @@ -119,8 +127,7 @@ lit-string lit-variable (lit-variable-except id ...) - (lit-variable-prefix id) - ) + (lit-variable-prefix id)) (scw s cw) (cw c @@ -132,25 +139,15 @@ '() cp #t - #f - ; no longer thought of as a constructor, at least for now... - ;(nt id) - ;lit-variable-not-otherwise-mentioned - ;context-match - ) + #f) (cp (cons p p)) - (rep (repeat p rep) - (repeat p cp) - (repeat p '())) - ;(pvar (variable-prefix p)) + (rep (repeat p p)) (id variable) ((match-repeat z) variable-not-otherwise-mentioned) (pvar variable-not-otherwise-mentioned (pvar pvar) (pvar elip)) - (x #;(side-condition (name x variable-not-otherwise-mentioned) - (not (regexp-match #rx"^[pm]" (format "~a" (term x))))) - (car x) + (x (car x) (cdr x) (cons x x) pvar) @@ -176,9 +173,8 @@ 0 bool)) (in-hole Context - (begin (Build-Term-Let (eqs_1 ...) ;(set! results (cons + (begin (Build-Term-Let (eqs_1 ...) r_1 - ;results)) ) (matrix (x_1 ...) (((p_1 ... -> r_2) eqs_2 ...) @@ -255,79 +251,6 @@ (side-condition (ormap not-a-wildcard? (term (p_2 ...)))) Drop-Front-Column-All-Wildcard) - #;(--> (in-hole Context - (matrix (x_1 x_2 ... x_3 x_4 ...) - ( - ((p_1 p_2 ... p_3 p_4 ... -> r_1) eqs_1 ...) - ...) - (pvar ...) - (pvar_3 ...) - natural - bool)) - (in-hole Context - (matrix (x_3 x_2 ... x_1 x_4 ...) - ( - ((p_3 p_2 ... p_1 p_4 ... -> r_1) eqs_1 ...) - ...) - (pvar ...) - (pvar_3 ...) - natural - bool)) - - (side-condition - (apply = - (append (list (length (term (x_2 ...))) - (length (term (x_2 ...)))) - (map length (term ((p_2 ...) ...)))))) - (side-condition - (apply = - (append (list (length (term (x_4 ...))) - (length (term (x_4 ...)))) - (map length (term ((p_4 ...) ...)))))) - (side-condition (> (length (remove-duplicates (term (simplify (p_1 ...))))) (length (remove-duplicates (term (simplify (p_3 ...))))))) - simple-swap) - - ; ; Front-Column-All-Wildcard (now force a swap with the backmost non-wildcard column to decrease branching) - ; ; When the front column of a matrix is all wildcard patterns, swap it with another column with at least one non-wildcard pattern. - ; - ; (--> (in-hole Context - ; (matrix (x_1 x_2 ... x_3 x_4 ...) - ; ((wc p_2 ... p_3 wildcard_1 ... -> r_1) - ; (wc p_5 ... p_6 wildcard_2 ... -> r_2) - ; ...) - ; (pvar ...) - ; (pvar_3 ...) - ; natural - ; bool)) - ; (in-hole Context - ; (matrix (x_3 x_2 ... x_1 x_4 ...) - ; ((p_3 p_2 ... wc wildcard_1 ... -> r_1) - ; (p_6 p_5 ... wc wildcard_2 ... -> r_2) - ; ...) - ; (pvar ...) - ; (pvar_3 ...) - ; natural - ; bool)) - ; (side-condition - ; (eqv? (length (term (x_2 ...))) - ; (length (term (p_2 ...))))) - ; (side-condition - ; (eqv? (length (term (x_4 ...))) - ; (length (term (wildcard_1 ...))))) - ; (side-condition - ; (apply = - ; (append (list (length (term (x_2 ...))) - ; (length (term (x_2 ...)))) - ; (map length (term ((p_5 ...) ...)))))) - ; (side-condition - ; (apply = - ; (append (list (length (term (x_4 ...))) - ; (length (term (x_4 ...)))) - ; (map length (term ((wildcard_2 ...) ...)))))) - ; #;(side-condition (not-a-wildcard? (term p_3))) - ; (side-condition (or (not-a-wildcard? (term p_3)) (ormap not-a-wildcard? (term (p_6 ...))))) - ; Front-Column-All-Wildcard) - ; Unroll-Or ; If the first pattern of a row in the matrix is an or pattern, duplicate the row for each branch of the or. @@ -426,15 +349,15 @@ natural bool)) (in-hole Context - (cond [(equal? (car ,(term pvar_1)) x_1) + (cond [(equal? (car pvar_11) x_1) (matrix (x_1 x_2 ...) (((p_3 p_5 ... -> r_2) eqs_1 ...)) (pvar_2 ...) (pvar_3 ...) natural bool)] - #;[else ∅] )) + (where pvar_11 (Get-Temp-Name pvar_1 (pvar_2 ...))) (side-condition (> (term natural) 0)) (side-condition (member (term pvar_1) (map (λ (x) (term (Get-Pvar ,x))) (append (term (Binding-Eqs (eqs_1 ...))) (term (True-Eqs (eqs_1 ...) ())) )))) bound-name-from-outside-repeat) @@ -498,9 +421,6 @@ (pvar_3 ...) natural bool))) - - - ;(side-condition (eqv? (hash-ref hole-table (term id)) 0)) (where (((p_* ... -> r_*) eqs_* ...) ...) (drop-first-p (same-starting-pattern (nt id) (((cw_1 p_2 ... -> r_1) eqs_1 ...) @@ -514,59 +434,6 @@ ...))) non-terminal) - ; non-terminal (set) - ; If the flag for the special "non-terminal returns a set" mode is true, and a row in the matrix begins with a non-terminal which contains a hole, - ; wrap the row in a let, which binds the result of calling the "set" function which matches the non-terminal to a special value called nt-val. - ; Inside the let but outside the matrix is a conditional to check if nt-val is not the empty set. The rest of the patterns in the row remain the same, - ; but the right hand side is adjusted to add in the results of nt-val. Union the let with the matrix formed by the other rows. - - #;(--> (in-hole Context - (matrix (x_1 x_2 ...) - (((p_1 p_2 ... -> r_1) eqs_1 ...) - ... - (((nt id) p_5 ... -> r_2) eqs_2 ...) - ((p_6 p_7 ... -> r_3) eqs_3 ...) - ...) - (pvar_2 ...) - (pvar_3 ...) - natural - #t)) - (in-hole Context - (begin - (let ((nt-val (,(string->symbol (format "~s~s" (term id) '-list)) x_1))) - (cond ((not (set-empty? nt-val)) - (matrix (x_2 ...) - (((p_* ... -> r_*) eqs_* ...) ...)#;((p_5 ... -> (set-union (set-from-list (set-map nt-val (curry pair-path-append (quote x_1)))) r_2))) - (pvar_2 ...) - (pvar_3 ...) - natural - #t)) - (else ∅))) - (matrix (x_1 x_2 ...) - (((p_** ... -> r_**) eqs_** ...) ...)#;((p_1 p_2 ... -> r_1) - ... - (p_6 p_7 ... -> r_3) - ...) - (pvar_2 ...) - (pvar_3 ...) - natural - #t))) - (side-condition (andmap not-a-nt? (term (p_1 ...)))) - ;(side-condition (> (hash-ref hole-table (term id)) 0)) - (fresh nt-val) - (where (((p_* ... -> r_*) eqs_* ...) ...) (drop-first-p (same-starting-pattern - (nt id) - (((p_1 p_2 ... -> r_1 #;(set-union (set-from-list (set-map nt-val (curry pair-path-append (quote x_1)))) r_1)) eqs_1 ...) - ... - (((nt id) p_5 ... -> r_2 #;(set-union (set-from-list (set-map nt-val (curry pair-path-append (quote x_1)))) r_2)) eqs_2 ...) - ((p_6 p_7 ... -> r_3 #;(set-union (set-from-list (set-map nt-val (curry pair-path-append (quote x_1)))) r_3)) eqs_3 ...) - ...)))) - (where (((p_** ... -> r_**) eqs_** ...) ...) (diff-starting-pattern (nt id) (((p_1 p_2 ... -> r_1) eqs_1 ...) - ... - ((p_6 p_7 ... -> r_3) eqs_3 ...) - ...))) - non-terminal-set) - ; Constructor ; If the front column is all either "constructor" patterns, or wildcard patterns, with at least one non-wildcard, then specialize the matrix based on the constructors. @@ -646,54 +513,6 @@ ...))) hole) - ; hole (non-terminal) - ; If a row in the matrix contains a lit-hole in its first column, and the flag for non-terminal-set is #t, - ; then separate the row from the rest of the matrix, replacing hole with "context-match," which will subsequently - ; be transformed into a conditional based on whether or not there is a current context. Additionally, transform the - ; right-hand-side into a pair of the quote the input variable (the "path"), and the input variable. Union this with the matrix formed by the remaining rows. - - #;(--> (in-hole Context - (matrix (x_1 x_2 ...) - (((p_1 p_2 ... -> r_1) eqs_1 ...) - ... - ((lit-hole p_5 ... -> r_2) eqs_2 ...) - ((p_6 p_7 ... -> r_3) eqs_3 ...) - ...) - (pvar_1 ...) - (pvar_3 ...) - natural - #t)) - (in-hole Context - (begin - (cond [(or (context-match) (eqv? x_1 the-hole)) - (matrix (x_2 ...) - (((p_* ... -> r_*) eqs_* ...) ...);((context-match p_5 ... -> (set (cons (quote x_1) x_1)))) - (pvar_1 ...) - (pvar_3 ...) - natural - #t)] - (else ∅)) - (matrix (x_1 x_2 ...) - (((p_** ... -> r_**) eqs_** ...) ...) - (pvar_1 ...) - (pvar_3 ...) - natural - #t))) - (side-condition (andmap not-a-lit-hole? (term (p_1 ...)))) - (where (((p_* ... -> r_*) eqs_* ...) ...) (drop-first-p (same-starting-pattern - lit-hole - (((p_1 p_2 ... -> (set (cons (quote x_1) x_1))) eqs_1 ...) - ... - ((lit-hole p_5 ... -> (set (cons (quote x_1) x_1))) eqs_2 ...) - ((p_6 p_7 ... -> (set (cons (quote x_1) x_1))) eqs_3 ...) - ...)))) - (where (((p_** ... -> r_**) eqs_** ...) ...) (diff-starting-pattern lit-hole - (((p_1 p_2 ... -> r_1) eqs_1 ...) - ... - ((p_6 p_7 ... -> r_3) eqs_3 ...) - ...))) - hole-non-terminal) - ; in-hole (wrong number of holes) ; If a row in a matrix begins with a lit-in-hole, but the number of holes in the first pattern is 0 or > 1, eliminate the row. @@ -747,7 +566,7 @@ (pvar_1 ...) (pvar_3 ...) natural - bool)) + bool)) (side-condition (eqv? 1 (term (detect-hole2 0 p_3)))) (side-condition (not-a-lit-name? (term p_3))) @@ -779,9 +598,6 @@ (fresh pvar-cdr) (where any_* (push-name-downward (lit-name pvar p_3) (eqs_2 ...) pvar-car pvar-cdr)) (side-condition (not-a-nt? (term p_3))) - - ;(where p_* ,(car (term any_*))) - ;(where (eqs_* ...) ,(cdr (term any_*))) in-hole-name) ; in-hole (base case) @@ -880,7 +696,6 @@ (fresh car-rt) (fresh cdr-rt) (side-condition (eqv? 1 (term (detect-hole2 0 (nt id))))) - in-hole-nt-name) ; hide-hole (not base case) @@ -1054,60 +869,68 @@ natural bool)) (in-hole Context - (begin (in-hole any_term-let - (letrec ((match-repeat - (λ ,(append (append (list (term z)) (term (binding_temp ...))) (term (bound_temp ...)) ) - (begin - (cond - ((andmap empty? ,(append (list 'list) (term (bound_temp ...)))) - (Build-Let ;reverse - (matrix (z x_2 ...) - (((p_4 p_5 ... -> r_2) ,@(term (Add-Repeat-Vars (eqs_* ...) (binding_temp ...))))) - (pvar_1 ...) - () - natural - bool) - (binding_temp ...))) - ) - (cond - ((andmap cons? ,(append (list 'list) (append (list (term z)) (term (bound_temp ...))) )) - (Build-Temp-Let - (binding_temp ...) - (single_binding_temp ...) - (let ((carz (car z))) - (matrix (carz) - (((p_3 -> (match-repeat ,@(append - (append (list (term (cdr z))) - (term (Build-Temp-Cons (binding_temp ...) (single_binding_temp ...)))) - (term (Build-Cdr (bound_temp ...)) )))) - eqs_* ...)) - (pvar_1 ...) - (pvar_3 ...) - ,(+ 1 (term natural)) - bool))) - ) - (else ∅) - ) - ) - ))) - (Build-Let-Empty natural ,(map (λ (x) (term (Get-Pvar ,x))) (term (binding_temp ...))) - (match-repeat ,@(if (> (term natural) 0) - (append (append (list (term x_1)) (term (binding_temp ...)) (map (λ (x) `(term ,x)) (term (pvar_22 ...))))) - (append (append (list (term x_1)) (term (binding_temp ...)) (term (bound_temp ...)))) - )) - ) - ) - ) - (matrix (x_1 x_2 ...) - (((cw_1 p_2 ... -> r_1) eqs_1 ...) - ... - ((p_6 p_7 ... -> r_3) eqs_3 ...) - ...) - (pvar_1 ...) - (pvar_3 ...) - natural - bool) - ) + (begin + (in-hole any_term-let + (letrec ((match-repeat + (λ ,(append (append (list (term z)) (term (binding_temp ...))) (term (bound_temp ...)) ) + (begin + (cond + ((andmap empty? ,(append (list 'list) (term (bound_temp ...)))) + (Build-Let ;reverse + (Build-Temp-Let + (pvar_11 ...) + (binding_temp ...) + (matrix (z x_2 ...) + (((p_4 p_5 ... -> r_2) ,@(term (Add-Repeat-Vars (eqs_* ...) (pvar_11 ...) (binding_temp ...))))) + (((Get-Pvar pvar_22) bound_temp) ...) + () + natural + bool)) + (binding_temp ...))) + ) + (cond + ((andmap cons? ,(append (list 'list) (append (list (term z)) (term (bound_temp ...))) )) + ;(Build-Temp-Let + ;(single_binding_temp ...) + ;(binding_temp ...) + (let ((carz (car z))) + (matrix (carz) + (((p_3 -> (match-repeat ,@(append + (append (list (term (cdr z))) + (term (Build-Temp-Cons (pvar_11 ...) (binding_temp ...) #;(single_binding_temp ...)))) + (term (Build-Cdr (bound_temp ...)) )))) + eqs_* ...)) + (((Get-Pvar pvar_22) bound_temp) ...) + (pvar_3 ...) + ,(+ 1 (term natural)) + bool)) + ;) + ) + (else ∅) + ) + ) + ))) + (Build-Temp-Let natural + (bound_temp ...) + (pvar_22 ...) + (Build-Let-Empty natural ,(map (λ (x) (term (Get-Pvar ,x))) (term (binding_temp ...))) + (match-repeat ,@(if (> (term natural) 0) + (append (append (list (term x_1)) (term (binding_temp ...)) (term ((Get-Pvar pvar_22) ...)) #;(map (λ (x) `(term ,x)) (term (pvar_22 ...))) )) + (append (append (list (term x_1)) (term (binding_temp ...)) (term (bound_temp ...))))) + ) + )) + ) + ) + (matrix (x_1 x_2 ...) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool) + ) ) (where any_term-let ,(if (eqv? 0 (term natural)) (begin (set! new-var-list (term (eqs_2 ...))) (let ((r (term (Build-Term-Let (eqs_2 ...) hole)))) #;(set! new-var-list (term (eqs_2 ...))) r)) @@ -1120,9 +943,9 @@ p_3 ,(map (λ (x) (term (Get-Pvar ,x))) (append (term (Binding-Eqs (eqs_* ...))) (term (True-Eqs (eqs_* ...) ())) )) ()))))) (where (pvar_22 ...) ,(begin - ;(printf "~a\n" (remove-duplicates (map (λ (x) (term (Get-Pvar ,x 0))) (append (term (Binding-Eqs (eqs_* ...))) (term (True-Eqs (eqs_* ...) ())))) )) - (remove-duplicates (map (λ (x) (term (Get-Pvar ,x 0))) (append (term (Binding-Eqs (eqs_* ...))) (term (True-Eqs (eqs_* ...) ())))) ) - )) + ;(printf "~a\n" (remove-duplicates (map (λ (x) (term (Get-Pvar ,x 0))) (append (term (Binding-Eqs (eqs_* ...))) (term (True-Eqs (eqs_* ...) ())))) )) + (remove-duplicates (map (λ (x) (term (Get-Pvar ,x 0))) (append (term (Binding-Eqs (eqs_* ...))) (term (True-Eqs (eqs_* ...) ())))) ) + )) (fresh match-repeat) (fresh z) (fresh carz) @@ -1131,129 +954,9 @@ (fresh ((single_binding_temp ...) (pvar_11 ...))) (fresh ((bound_temp ...) - (pvar_22 ...))) + (pvar_22 ...))) Repeat) -; (--> (in-hole Context -; (matrix (x_1 x_2 ...) -; (((cw_1 p_2 ... -> r_1) eqs_1 ...) -; ... -; (((repeat p_3 p_4) p_5 ... -> r_2) eqs_2 ...) -; ((p_6 p_7 ... -> r_3) eqs_3 ...) -; ...) -; (pvar_1 ...) -; (pvar_3 ...) -; natural -; bool)) -; (in-hole Context -; (begin (in-hole any_term-let -; (Build-Temp-Let -; natural -; (bound-temp ...) -; ,(map (λ (x) (list 'term x)) -; (term (pvar_22 ...))) -; ;) -; (letrec ((match-repeat -; (λ ,(append (append (list (term z)) (term (pvar_11 ...))) (map (λ (x) (term (Get-Pvar ,x))) (term (pvar_22 ...))) ) -; (begin -; (cond -; ((andmap empty? ,(append (list 'list) (map (λ (x) (term (Get-Pvar ,x))) (term (pvar_22 ...))) )) -; (Build-Let -; (Restore-Temp natural (pvar_22 ...) (bound-temp ...) -; (matrix (z x_2 ...) -; (((p_4 p_5 ... -> r_2) ,@(term (Add-Repeat-Vars (eqs_* ...) (pvar_11 ...))))) -; (pvar_1 ...) -; () -; natural -; bool) -; ) -; -; (pvar_11 ...))) -; #;(else ∅) -; ) -; -; (cond -; ((andmap cons? ,(append (list 'list) (append (list (term z)) (map (λ (x) (term (Get-Pvar ,x))) (term (pvar_22 ...))) ))) -; (Build-Temp-Let -; (binding-temp ...) -; (pvar_11 ...) -; (matrix ((car z)) -; (((p_3 -> (match-repeat ,@(append -; (append (list (term (cdr z))) -; (term (Build-Temp-Cons (pvar_11 ...) (binding-temp ...)))) -; (term (Build-Cdr ,(map (λ (x) (term (Get-Pvar ,x))) (term (pvar_22 ...))) ))))) -; eqs_* ...)) -; (pvar_1 ...) -; (pvar_3 ...) -; ,(+ 1 (term natural)) -; bool)) -; ) -; (else ∅) -; ) -; ) -; ))) -; (Build-Let-Empty natural ,(map (λ (x) (term (Get-Pvar ,x))) (term (pvar_11 ...))) -; (match-repeat ,@(if (> (term natural) 0) -; (append (append (list (term x_1)) (map (λ (x) (term (Get-Pvar ,x))) (term (pvar_11 ...))) ) (map (λ (x) (term (Get-Pvar ,x))) (term (pvar_22 ...)))) -; (append (append (list (term x_1)) (map (λ (x) (term (Get-Pvar ,x))) (term (pvar_11 ...))) ) (term (bound-temp ...))) -; ;(map (λ (x) (list 'term x)) (term (pvar_22 ...)))) -; ;(map (λ (x) (term (Get-Pvar ,x)))#;(λ (x) (list 'term x)) (term (pvar_22 ...))) -; )) -; ) -; )) -; ) -; (matrix (x_1 x_2 ...) -; (((cw_1 p_2 ... -> r_1) eqs_1 ...) -; ... -; ((p_6 p_7 ... -> r_3) eqs_3 ...) -; ...) -; (pvar_1 ...) -; (pvar_3 ...) -; natural -; bool) -; ) -; ) -; (where any_term-let ,(if (eqv? 0 (term natural)) -; (begin (set! new-var-list (term (eqs_2 ...))) (let ((r (term (Build-Term-Let (eqs_2 ...) hole)))) (set! new-var-list (term (eqs_2 ...))) r)) -; (begin (set! new-var-list (term (eqs_2 ...))) -; (term hole)))) -; #;(where any_term-let ,(begin (set! new-var-list (term (eqs_2 ...))) (term (Build-Term-Let (eqs_2 ...) hole)) -; )) -; #;(if (> -1 (term natural)) -; (begin (printf "1 ~a ~a\n\n" (term (eqs_2 ...)) new-var-list) (term (Build-Term-Let (eqs_2 ...) hole))) -; (begin (printf "2 ~a ~a\n\n" (term (eqs_2 ...)) new-var-list) (set! new-var-list (term (eqs_2 ...))) -; (printf "3 ~a ~a\n\n" (term (eqs_2 ...)) new-var-list) -; (term hole))) -; (where (eqs_* ...) ,new-var-list) -; (where (pvar_11 ...) ,(remove-duplicates (map (λ (x) (term (Get-Pvar ,x))) -; (term -; (Get-Free-Name-Patterns -; p_3 -; ,(map (λ (x) (term (Get-Pvar ,x))) (append (term (Binding-Eqs (eqs_* ...))) (term (True-Eqs (eqs_* ...) ())) )) ()))))) -; (where (pvar_22 ...) , -; (begin -; ;(printf "~a\n" (remove-duplicates (map (λ (x) (term (Get-Pvar ,x 0))) (append (term (Binding-Eqs (eqs_* ...))) (term (True-Eqs (eqs_* ...) ())))) )) -; (remove-duplicates (map (λ (x) (term (Get-Pvar ,x 0))) (append (term (Binding-Eqs (eqs_* ...))) (term (True-Eqs (eqs_* ...) ())))) ) -; )) -; (fresh match-repeat) -; (fresh z) -; ;(fresh ((pvar_11 ...) (pvar_111 ...))) -; ;(fresh ((pvar_22 ...) (pvar_222 ...))) -; (fresh ((binding-temp ...) -; (pvar_11 ...))) -; (fresh ((bound-temp ...) -; (pvar_22 ...))) -; -; ; (side-condition (andmap not-a-lit-hole? (term (p_1 ...)))) -; ; (side-condition (andmap not-a-lit-name? (term (p_1 ...)))) -; ; (side-condition (andmap not-an-in-hole? (term (p_1 ...)))) -; ; (side-condition (andmap not-a-s? (term (p_1 ...)))) -; ; (side-condition (andmap not-a-rep? (term (p_1 ...)))) -; ; (side-condition (andmap not-a-nt? (term (p_1 ...)))) -; ; (side-condition (andmap not-a-side-condition? (term (p_1 ...)))) -; -; Repeat) - ; built-in non-terminals (--> (in-hole Context @@ -1354,7 +1057,7 @@ (define natural? (λ (x) (and - (integer? x) + (exact-integer? x) (not (negative? x))))) (define-metafunction L @@ -1378,6 +1081,18 @@ (side-condition (equal? (term pvar_3) (term (Get-Pvar pvar)))) ] [(Add-Repeat-Vars (eqs ...) (pvar_1 ...)) + (eqs ...)] + [(Add-Repeat-Vars ((pvar bool eq ...) eqs_2 ...) (pvar_1 ... pvar_3 pvar_2 ...) (pvar_11 ... pvar_33 pvar_22 ...)) + (Add-Repeat-Vars (eqs_2 ... (pvar bool ,@(remove-duplicates (term (pvar_33 eq ...))))) (pvar_1 ... pvar_2 ...) (pvar_11 ... pvar_22 ...)) + (side-condition (equal? (term pvar_3) (term (Get-Pvar pvar)))) + (side-condition (and (equal? (length (term (pvar_1 ...))) (length (term (pvar_11 ...)))) + (equal? (length (term (pvar_2 ...))) (length (term (pvar_22 ...)))))) + ] + [(Add-Repeat-Vars (eqs_1 ... (pvar bool eq ...) eqs_2 ...) (pvar_3 pvar_1 ...) (pvar_33 pvar_11 ...)) + (Add-Repeat-Vars (eqs_1 ... eqs_2 ... (pvar bool ,@(remove-duplicates (term (pvar_33 eq ...))))) (pvar_1 ...) (pvar_11 ...)) + (side-condition (equal? (term pvar_3) (term (Get-Pvar pvar)))) + ] + [(Add-Repeat-Vars (eqs ...) (pvar_1 ...) (pvar_11 ...)) (eqs ...)]) (define-metafunction L @@ -1399,76 +1114,58 @@ [(Binding-Eqs (eqs ...)) ()]) +(define-metafunction L + [(Minimize-Names (pvar pvar_2 ... pvar_3 pvar_4 ...)) + (pvar_* ...) + (where (pvar_* ...) (Minimize-Names (pvar pvar_2 ... pvar_4 ...))) + (side-condition (and (equal? (term (Get-Pvar pvar)) (term (Get-Pvar pvar_3))) (<= (term (Depth pvar)) (term (Depth pvar_3)) ))) + (side-condition (andmap (λ (x) (not (equal? (term (Get-Pvar pvar)) (term (Get-Pvar ,x))))) (term (pvar_2 ...))))] + [(Minimize-Names (pvar pvar_2 ... pvar_3 pvar_4 ...)) + (pvar_* ...) + (where (pvar_* ...) (Minimize-Names (pvar_3 pvar_2 ... pvar_4 ...))) + (side-condition (and (equal? (term (Get-Pvar pvar)) (term (Get-Pvar pvar_3))) (> (term (Depth pvar)) (term (Depth pvar_3)) ))) + (side-condition (andmap (λ (x) (not (equal? (term (Get-Pvar pvar)) (term (Get-Pvar ,x))))) (term (pvar_2 ...))))] + [(Minimize-Names (pvar pvar_2 ...)) + (pvar pvar_* ...) + (where (pvar_* ...) (Minimize-Names (pvar_2 ...))) + ] + [(Minimize-Names ()) + ()] + ) + +(define-metafunction L + [(Depth (pvar elip)) + ,(+ 1 (term (Depth pvar)))] + [(Depth pvar) + 0] + ) + (define-metafunction L - ; Get-Name-Patterns - ;(lit-in-hole p_1 p_2) ? - ;(lit-hide-hole p) ? [(Get-Free-Name-Patterns (lit-in-hole p_1 p_2) (pvar_1 ...) (pvar_2 ...)) - ,(append (term (Get-Free-Name-Patterns p_1 (pvar_1 ...) ())) - (append (term (Get-Free-Name-Patterns p_2 (pvar_1 ...) ())) - (term (pvar_2 ...))))] + (Minimize-Names ,(append (term (Get-Free-Name-Patterns p_1 (pvar_1 ...) ())) + (append (term (Get-Free-Name-Patterns p_2 (pvar_1 ...) ())) + (term (pvar_2 ...)))))] [(Get-Free-Name-Patterns (lit-hide-hole p_1) (pvar_1 ...) (pvar_2 ...)) - ,(append (term (Get-Free-Name-Patterns p_1 (pvar_1 ...) ())) (term (pvar_2 ...)))] + (Minimize-Names ,(append (term (Get-Free-Name-Patterns p_1 (pvar_1 ...) ())) (term (pvar_2 ...))))] [(Get-Free-Name-Patterns (or p_1 p_2) (pvar_1 ...) (pvar_2 ...)) - ,(append (term (Get-Free-Name-Patterns p_1 (pvar_1 ...) ())) - (append (term (Get-Free-Name-Patterns p_2 (pvar_1 ...) ())) - (term (pvar_2 ...))))] + (Minimize-Names ,(append (term (Get-Free-Name-Patterns p_1 (pvar_1 ...) ())) + (append (term (Get-Free-Name-Patterns p_2 (pvar_1 ...) ())) + (term (pvar_2 ...)))))] [(Get-Free-Name-Patterns (cons p_1 p_2) (pvar_1 ...) (pvar_2 ...)) - ,(append (term (Get-Free-Name-Patterns p_1 (pvar_1 ...) ())) - (append (term (Get-Free-Name-Patterns p_2 (pvar_1 ...) ())) - (term (pvar_2 ...))))] + (Minimize-Names ,(append (term (Get-Free-Name-Patterns p_1 (pvar_1 ...) ())) + (append (term (Get-Free-Name-Patterns p_2 (pvar_1 ...) ())) + (term (pvar_2 ...)))))] [(Get-Free-Name-Patterns (lit-name id p) (pvar_1 ...) (pvar_2 ...)) - ,(append (term (Get-Free-Name-Patterns p (pvar_1 ...) ())) (append (list (term id)) (term (pvar_2 ...)))) + (Minimize-Names ,(append (term (Get-Free-Name-Patterns p (pvar_1 ...) ())) (append (list (term id)) (term (pvar_2 ...))))) (side-condition (andmap (λ (x) (not (eqv? (term id) x))) (term (pvar_1 ...))))] [(Get-Free-Name-Patterns (repeat p_1 p_2) (pvar_1 ...) (pvar_2 ...)) - ,(append (map (λ (x) `(,x ...)) (remove-duplicates (term (Get-Free-Name-Patterns p_1 (pvar_1 ...) ())))) - (append (term (Get-Free-Name-Patterns p_2 (pvar_1 ...) ())) - (term (pvar_2 ...))))] + (Minimize-Names ,(append (map (λ (x) `(,x ...)) (remove-duplicates (term (Get-Free-Name-Patterns p_1 (pvar_1 ...) ())))) + (append (term (Get-Free-Name-Patterns p_2 (pvar_1 ...) ())) + (term (pvar_2 ...)))))] [(Get-Free-Name-Patterns (lit-side-condition p_1 any) (pvar_1 ...) (pvar_2 ...)) - ,(append (term (Get-Free-Name-Patterns p_1 (pvar_1 ...) ())) (term (pvar_2 ...)))] + (Minimize-Names ,(append (term (Get-Free-Name-Patterns p_1 (pvar_1 ...) ())) (term (pvar_2 ...))))] [(Get-Free-Name-Patterns any (pvar_1 ...) (pvar_2 ...)) ()]) -(term (Get-Free-Name-Patterns 1 () ())) -(term (Get-Free-Name-Patterns (lit-name a wc) () ())) -(term (Get-Free-Name-Patterns (lit-name a wc) (a) ())) -(term (Get-Free-Name-Patterns (lit-name a wc) () (b))) -(term (Get-Free-Name-Patterns (lit-name a wc) (a) (b))) -(term (Get-Free-Name-Patterns (cons (lit-name a lit-natural) (cons (lit-name b wc) '())) () ())) -(term (Get-Free-Name-Patterns (or (lit-name x lit-natural) (lit-name y wc)) () ())) -(term (Get-Free-Name-Patterns (or (lit-name x wc) (lit-name z (cons (lit-name y wc) '()))) (y) ())) - -(define-metafunction L - ; Get-Name-Patterns - ;(lit-in-hole p_1 p_2) ? - ;(lit-hide-hole p) ? - [(Get-Bound-Name-Patterns (or p_1 p_2) (pvar_1 ...) (pvar_2 ...)) - ,(append (term (Get-Bound-Name-Patterns p_1 (pvar_1 ...) ())) - (append (term (Get-Bound-Name-Patterns p_2 (pvar_1 ...) ())) - (term (pvar_2 ...))))] - [(Get-Bound-Name-Patterns (cons p_1 p_2) (pvar_1 ...) (pvar_2 ...)) - ,(append (term (Get-Bound-Name-Patterns p_1 (pvar_1 ...) ())) - (append (term (Get-Bound-Name-Patterns p_2 (pvar_1 ...) ())) - (term (pvar_2 ...))))] - [(Get-Bound-Name-Patterns (lit-name id p) (pvar_1 ...) (pvar_2 ...)) - ,(append (term (Get-Bound-Name-Patterns p (pvar_1 ...) ())) (append (list (term id)) (term (pvar_2 ...)))) - (side-condition (ormap (λ (x) (eqv? (term id) x)) (term (pvar_1 ...))))] - [(Get-Bound-Name-Patterns (repeat p_1 p_2) (pvar_1 ...) (pvar_2 ...)) - ,(append (term ((,@(term (Get-Bound-Name-Patterns p_1 (pvar_1 ...) ())) ,'...))) - (append (term (Get-Bound-Name-Patterns p_2 (pvar_1 ...) ())) - (term (pvar_2 ...))))] - [(Get-Bound-Name-Patterns (lit-side-condition p_1 any) (pvar_1 ...) (pvar_2 ...)) - ,(append (term (Get-Bound-Name-Patterns p_1 (pvar_1 ...) ())) (term (pvar_2 ...)))] - [(Get-Bound-Name-Patterns any (pvar_1 ...) (pvar_2 ...)) ()]) - -(term (Get-Bound-Name-Patterns 1 () ())) -(term (Get-Bound-Name-Patterns (lit-name a wc) () ())) -(term (Get-Bound-Name-Patterns (lit-name a wc) (a) ())) -(term (Get-Bound-Name-Patterns (lit-name a wc) () (b))) -(term (Get-Bound-Name-Patterns (lit-name a wc) (a) (b))) -(term (Get-Bound-Name-Patterns (cons (lit-name a lit-natural) (cons (lit-name b wc) '())) () ())) -(term (Get-Bound-Name-Patterns (or (lit-name x lit-natural) (lit-name y wc)) () ())) -(term (Get-Bound-Name-Patterns (or (lit-name x wc) (lit-name z (cons (lit-name y wc) '()))) (y) ())) - (define-metafunction L ((Build-Let-Empty natural () any) any) @@ -1489,7 +1186,7 @@ ((Build-Temp-Let 0 () () any) any) [(Build-Temp-Let 0 (pvar_1 ...) (any_2 ...) any) - (let ((pvar_1 any_2) + (let ((pvar_1 (term any_2)) ...) any)] ((Build-Temp-Let natural any_1 any_2 any_3) @@ -1501,22 +1198,6 @@ ...) any)]) -(define-metafunction L - ((Restore-Temp () () any) - any) - [(Restore-Temp (pvar_1 ...) (any_2 ...) any) - (term-let ((pvar_1 any_2) - ...) - any)] - ((Restore-Temp 0 () () any) - any) - [(Restore-Temp 0 (pvar_1 ...) (any_2 ...) any) - (term-let ((pvar_1 any_2) - ...) - any)] - ((Restore-Temp natural any_1 any_2 any_3) - any_3)) - (define-metafunction L [(Build-Temp-Cons (pvar_1 ...) (pvar_2 ...)) ((cons pvar_1 pvar_2) ...)]) @@ -1525,21 +1206,13 @@ [(Build-Cdr (pvar_1 ...)) ((cdr pvar_1) ...)]) -(term (Build-Let-Empty - 0 - (Get-Free-Name-Patterns (or (lit-name x wc) (lit-name z (cons (lit-name y wc) '()))) (y) ()) - 'body-goes-here)) - +; first pass hole detection assumes non-terminals contain no holes (define-metafunction L - ; ((detect-hole natural lit-hole) ,(+ 1 (term natural))) - ; assume we have table of non-terminals ((detect-hole natural (nt id)) 0) - ; ,(+ (term natural) (nt-struct-number-of-holes (hash-ref nt-table (term 'id))))) - ((detect-hole natural (lit-in-hole p_1 p_2)) ,(+ (term natural) (term (detect-hole 0 p_2)))) ((detect-hole natural (lit-hide-hole p_1)) @@ -1555,6 +1228,7 @@ ((detect-hole natural any) natural)) +; detect holes using a table with a hole count for each non-terminal (define-metafunction L ((detect-hole2 natural lit-hole) ,(+ 1 (term natural))) @@ -1576,13 +1250,6 @@ natural) ) -(term (detect-hole 0 lit-hole)) -(term (detect-hole 0 (or lit-hole lit-hole))) -(term (detect-hole 0 (cons lit-hole (cons (lit-hide-hole lit-hole) '())))) -(term (detect-hole 0 (repeat lit-number (cons lit-hole '())))) -(term (detect-hole 0 (cons lit-hole (cons (lit-in-hole lit-hole lit-hole) '())))) -(term (detect-hole 0 (cons 1 '()))) - ; op is either lit-in-hole or lit-hide-hole ; replace is either p_2 from (lit-in-hole p_1 p_2) or 'lit-hole ; pattern is either p_1 from (lit-in-hole p_1 p_2) or p from (lit-hide-hole p) @@ -1619,14 +1286,13 @@ (or (move-hole-op-inward op replace p_1) (move-hole-op-inward op replace p_2))) ((move-hole-op-inward op replace (cons p_1 p_2)) (cons (move-hole-op-inward op replace p_1) (move-hole-op-inward op replace p_2))) + ((move-hole-op-inward op replace (repeat p_1 p_2)) + (repeat p_1 (move-hole-op-inward op replace p_2)) + (side-condition (eqv? 1 (term (detect-hole2 0 p_2))))) ((move-hole-op-inward op replace any) any) ) -(term (move-hole-op-inward lit-in-hole (cons 1 '()) (cons 1 (cons 2 (cons lit-hole '()))))) -#;(term (move-hole-op-inward lit-in-hole (cons 1 '()) (cons 1 (cons (nt A) '())))) -#;(term (move-hole-op-inward lit-in-hole (cons 1 '()) (cons 1 (cons (nt A) (cons 4 (cons 5 '())))))) - (define-metafunction L ((push-name-downward (lit-name pvar (cons p_1 p_2)) (eqs_1 ... (pvar bool eq_1 ...) eqs_2 ...) pvar_fresh1 pvar_fresh2) ((cons (lit-name pvar_fresh1 p_1) (lit-name pvar_fresh2 p_2)) (eqs_1 ... (pvar bool (cons pvar_fresh1 pvar_fresh2) eq_1 ...) (pvar_fresh1 #f) (pvar_fresh2 #f) eqs_2 ...))) @@ -1636,49 +1302,24 @@ ((lit-name pvar_2 p_1) (eqs_1 ... (pvar bool (= pvar_2) eq_1 ...) eqs_2 ...))) ((push-name-downward (lit-name pvar (lit-in-hole p_1 p_2)) (eqs_1 ... (pvar bool eq_1 ...) eqs_2 ...) pvar_fresh1 pvar_fresh2) ((lit-in-hole (lit-name pvar_fresh1 p_1) (lit-name pvar_fresh2 p_2)) (eqs_1 ... (pvar bool (plug pvar_fresh1 pvar_fresh2) eq_1 ...) (pvar_fresh1 #f) (pvar_fresh2 #f) eqs_2 ...))) + ((push-name-downward (lit-name pvar (repeat p_1 p_2)) (eqs_1 ... (pvar bool eq_1 ...) eqs_2 ...) pvar_fresh1 pvar_fresh2) + ((repeat (lit-name pvar_fresh1 p_1) (lit-name pvar_fresh2 p_2)) (eqs_1 ... (pvar bool (cons pvar_fresh1 pvar_fresh2) eq_1 ...) (pvar_fresh1 #f) (pvar_fresh2 #f) eqs_2 ...))) ((push-name-downward any_1 any_2 any_3 any_4) (any_1 any_2)) ) ; Replace (eqv? c x) with (another-function x) where appropriate. (define-metafunction L - ;Func-Replace : (eqv? c x) -> - [(Func-Replace (eqv? number x)) (eqv? number x)] - [(Func-Replace (eqv? 'variable x)) (eqv? 'variable x)] - [(Func-Replace (eqv? '() x)) (eqv? '() x)] - ; these are probably wrong now! example rows: (5 -> 1) (lit-number -> 2) will return (set 1)! [(Func-Replace (eqv? lit-number x)) (number? x)] [(Func-Replace (eqv? lit-natural x)) (natural? x)] - [(Func-Replace (eqv? lit-integer x)) (integer? x)] + [(Func-Replace (eqv? lit-integer x)) (exact-integer? x)] [(Func-Replace (eqv? lit-real x)) (real? x)] [(Func-Replace (eqv? lit-string x)) (string? x)] [(Func-Replace (eqv? lit-variable x)) (symbol? x)] - ; temporarily added - [(Func-Replace (eqv? cp x)) #t] - - ; These are functions which need to be written [(Func-Replace (eqv? (lit-variable-except variable ...) x)) (and (symbol? x) (andmap (λ (y) (not (equal? y x))) (quote (variable ...))))] - [(Func-Replace (eqv? (lit-variable-prefix variable) x)) (variable-prefix? variable x)] - ;[(Func-Replace (eqv? lit-variable-not-otherwise-mentioned x)) (variable-not-otherwise-mentioned? x)] - ;[(Func-Replace (eqv? context-match x)) (or (context-match) (eqv? x 'lit-hole))] - ;[(Func-Replace (eqv? (rep-match (pvar ...)) x)) (and (not (set-empty? (match-repeat x pvar ...))) (print (match-repeat x pvar ...)))] - - ; Function given to us by define-language - [(Func-Replace (eqv? (nt id) x)) (set-member? (,(string->symbol (format "~s~s" (term id) '-list)) x) 'MATCHED)] - ) - - -(define-metafunction L - [(clean-up (∪ any ∅)) any] - [(clean-up (∪ any (matrix (any_1 ...) () (any_2 ...) (any_3 ...) natural bool))) any] - [(clean-up any) any] - ) - -(define-metafunction L - [(add-nt-to-result x ((nt id) p ... -> r)) - ((nt id) p ... -> (set-union (,(string->symbol (format "~s~s" (term id) '-list)) x) r))] - [(add-nt-to-result x (p_1 p_2 ... -> r)) - (p_1 p_2 ... -> r)] + [(Func-Replace (eqv? (lit-variable-prefix variable) x)) (variable-prefix? 'variable x)] + [(Func-Replace (eqv? string x)) (equal? string x)] + [(Func-Replace (eqv? any x)) (eqv? any x)] ) (define-metafunction L @@ -1731,7 +1372,7 @@ bool) x_3 x_4)) - (clean-up (∪ (cond + (begin (cond [(cons? x_1) (let ((x_3 (car x_1)) (x_4 (cdr x_1))) @@ -1772,7 +1413,7 @@ (pvar_3 ...) natural bool) - )) + ) ] [(Build-Cond ((cw_1 ...) (matrix (x_1 x_2 ...) @@ -1787,7 +1428,7 @@ bool) x_3 x_4)) - (clean-up (∪ (cond + (begin (cond [(Func-Replace (eqv? cw_1 x_1)) (matrix (x_2 ...) (S cw_1 (((cw_2 p_2 ... -> r_1) eqs_1 ...) @@ -1813,7 +1454,7 @@ (pvar_3 ...) natural bool) - )) + ) ] ) @@ -1915,253 +1556,15 @@ ) (define-metafunction L - def-no-overlap? : p_1 p_2 -> bool - ((def-no-overlap? p_1 p_1) #f) - ((def-no-overlap? p_1 wc) #f) - ((def-no-overlap? wc p_2) #f) - ((def-no-overlap? (cons p_1 p_2) (cons p_3 p_4)) - ,(or (term (def-no-overlap? p_1 p_3)) - (term (def-no-overlap? p_2 p_4)))) - ) - -(define no-context (λ (x) (cond ((eqv? 'lit-hole x) #t) - (else #f)))) - -(define in-context (λ (x) #t)) - -(define context-match (make-parameter no-context)) - -(define rev (λ (x) - (if (cons? x) - (reverse x) - x))) - -(define-metafunction L - default-rows : (row ...) -> (row ...) - ((default-rows ((wc p_3 ... -> r) row ...)) - ((wc p_3 ... -> r) row_* ...) - (where (row_* ...) - (default-rows (row ...)))) - ((default-rows (((nt id) p_3 ... -> r) row ...)) - (((nt id) p_3 ... -> r) row_* ...) - (where (row_* ...) - (default-rows (row ...)))) - ((default-rows ((lit-hole p_3 ... -> r) row ...)) - ((lit-hole p_3 ... -> r) row_* ...) - (where (row_* ...) - (default-rows (row ...)))) - ((default-rows (((repeat p_1 p_2) p_3 ... -> r) row ...)) - (((repeat p_1 p_2) p_3 ... -> r) row_* ...) - (where (row_* ...) - (default-rows (row ...)))) - ((default-rows ((p_1 p_3 ... -> r) row ...)) - (default-rows (row ...))) - ((default-rows ()) ()) - ) - -(define-metafunction L - Build-Default : m -> e - ((Build-Default (matrix (x_1 x_2 ...) - ((p_1 p_2 ... -> r_1) - ...) - (pvar ...) - (pvar_2 ...) - natural - bool)) - (∪ - m_default - (cond - ((number? x_1) - m_number) - ((cons? x_1) - m_cons) - ((symbol? x_1) - m_variable) - ((string? x_1) - m_string) - (else ∅)) - ) - (where m_default - (matrix (x_1 x_2 ...) - (default-rows - ((p_1 p_2 ... -> r_1) - ...) - ) - (pvar ...) - (pvar_2 ...) - natural - bool)) - (where m_number - (matrix (x_1 x_2 ...) - (number-rows - ((p_1 p_2 ... -> r_1) - ...) - ) - (pvar ...) - (pvar_2 ...) - natural - bool)) - (where m_cons - (matrix ((car x_1) (cdr x_1) x_2 ...) - (cons-rows - ((p_1 p_2 ... -> r_1) - ...) - ) - (pvar ...) - (pvar_2 ...) - natural - bool)) - (where m_variable - (matrix (x_1 x_2 ...) - (variable-rows - ((p_1 p_2 ... -> r_1) - ...) - ) - (pvar ...) - (pvar_2 ...) - natural - bool)) - (where m_string - (matrix (x_1 x_2 ...) - (string-rows - ((p_1 p_2 ... -> r_1) - ...) - ) - (pvar ...) - (pvar_2 ...) - natural - bool)) - )) - -(define-metafunction L - number-rows : (row ...) -> (row ...) - ((number-rows ((lit-number p_3 ... -> r) row ...)) - ((wc p_3 ... -> r) row_* ...) - (where (row_* ...) - (number-rows (row ...)))) - ((number-rows ((lit-real p_3 ... -> r) row ...)) - ((lit-real p_3 ... -> r) row_* ...) - (where (row_* ...) - (number-rows (row ...)))) - ((number-rows ((lit-integer p_3 ... -> r) row ...)) - ((lit-integer p_3 ... -> r) row_* ...) - (where (row_* ...) - (number-rows (row ...)))) - ((number-rows ((lit-natural p_3 ... -> r) row ...)) - ((lit-natural p_3 ... -> r) row_* ...) - (where (row_* ...) - (number-rows (row ...)))) - ((number-rows ((number p_3 ... -> r) row ...)) - ((number p_3 ... -> r) row_* ...) - (where (row_* ...) - (number-rows (row ...)))) - ((number-rows ((p_1 p_3 ... -> r) row ...)) - (number-rows (row ...))) - ((number-rows ()) ()) - ) - -(define-metafunction L - cons-rows : (row ...) -> (row ...) - ((cons-rows (((cons p_1 p_2) p_3 ... -> r) row ...)) - ((p_1 p_2 p_3 ... -> r) row_* ...) - (where (row_* ...) - (cons-rows (row ...)))) - ((cons-rows ((p_1 p_3 ... -> r) row ...)) - (cons-rows (row ...))) - ((cons-rows ()) ()) - ) - -(define-metafunction L - variable-rows : (row ...) -> (row ...) - ((variable-rows ((lit-variable p_3 ... -> r) row ...)) - ((wc p_3 ... -> r) row_* ...) - (where (row_* ...) - (variable-rows (row ...)))) - ((variable-rows (((lit-variable-except id ...) p_3 ... -> r) row ...)) - (((lit-variable-except id ...) p_3 ... -> r) row_* ...) - (where (row_* ...) - (variable-rows (row ...)))) - ((variable-rows (((lit-variable-prefix id) p_3 ... -> r) row ...)) - (((lit-variable-prefix id) p_3 ... -> r) row_* ...) - (where (row_* ...) - (variable-rows (row ...)))) - ((variable-rows (('variable p_3 ... -> r) row ...)) - (('variable p_3 ... -> r) row_* ...) - (where (row_* ...) - (variable-rows (row ...)))) - ((variable-rows ((p_1 p_3 ... -> r) row ...)) - (variable-rows (row ...))) - ((variable-rows ()) ()) - ) - -(define-metafunction L - string-rows : (row ...) -> (row ...) - ((string-rows ((lit-string p_3 ... -> r) row ...)) - ((wc p_3 ... -> r) row_* ...) - (where (row_* ...) - (string-rows (row ...)))) - ((string-rows ((string p_3 ... -> r) row ...)) - ((string p_3 ... -> r) row_* ...) - (where (row_* ...) - (string-rows (row ...)))) - ((string-rows ((p_1 p_3 ... -> r) row ...)) - (string-rows (row ...))) - ((string-rows ()) ()) - ) - -(define-metafunction L - ;specialize : m -> (e ...) - ((specialize - (matrix (x_1 x_2 ...) - ((c_1 p_2 ... -> r_1) - (p_3 p_4 ... -> r_2) - ...) - (pvar ...) - (pvar_2 ...) - natural - bool)) - (((Func-Replace (eqv? c_1 x_1)) - (matrix (x_2 ...) - (drop-first-p - (same-starting-pattern - c_1 - ((c_1 p_2 ... -> r_1) - (p_3 p_4 ... -> r_2) - ...))) - (pvar ...) - (pvar_2 ...) - natural - bool)) - any_* ...) - (where (any_* ...) (specialize - (matrix (x_1 x_2 ...) - (diff-starting-pattern - c_1 - ((c_1 p_2 ... -> r_1) - (p_3 p_4 ... -> r_2) - ...)) - (pvar ...) - (pvar_2 ...) - natural - bool))) - ) - ((specialize (matrix (x_1 x_2 ...) - () - (pvar ...) - (pvar_2 ...) - natural - bool)) + ((Get-Temp-Name pvar_1 ((pvar_1 pvar_2) pvar_3 ...)) + pvar_2) + ((Get-Temp-Name pvar_1 ((pvar_1 pvar_2) pvar_3 ...)) + (Get-Temp-Name pvar (pvar_3 ...)) + (side-condition (not (equal? (term pvar) (term pvar_1))))) + ((Get-Temp-Name pvar_1 (pvar_3 ...)) ()) ) - -(define-metafunction L - ((fix-cond (any ...)) - (cond - any - ... - (else ∅)))) - (define-metafunction L ((Build-Term-Let ((pvar #f eq_1 ... lit-hole eq_2 ...) eqs_2 ...) r) (term-let ((pvar the-hole)) @@ -2180,7 +1583,7 @@ (side-condition (andmap not-an-id? (term (eq_1 ...))))) ((Build-Term-Let ((pvar #f eq ... (= pvar_3) eq_2 ...) eqs_2 ... (pvar_3 #t eq_3 ...) eqs_3 ...) r) - (term-let ((pvar pvar_3)) + (term-let ((pvar (term pvar_3))) (Build-Term-Let (eqs_2 ... (pvar_3 #t eq_3 ...) eqs_3 ... (pvar #t eq ... eq_2 ...)) r)) (side-condition (andmap (λ (x) (not (redex-match L (= pvar_11) x))) (term (eq ...))))) @@ -2191,7 +1594,7 @@ (side-condition (andmap (λ (x) (not (redex-match L (= pvar_11) x))) (term (eq ...))))) ((Build-Term-Let ((pvar bool_1 (= pvar_3) eq_2 ...) eqs_2 ... (pvar_3 bool_2 eq_3 ...) eqs_3 ...) r) - (term (Build-Term-Let (eqs_2 ... (pvar_3 bool_2 eq_3 ...) eqs_3 ... (pvar bool_1 eq_2 ... (= pvar_3))) r)) + (Build-Term-Let (eqs_2 ... (pvar_3 bool_2 eq_3 ...) eqs_3 ... (pvar bool_1 eq_2 ... (= pvar_3))) r) (side-condition (or (and (term bool_1) (not (term bool_2))) (and (not (term bool_1)) @@ -2345,449 +1748,12 @@ r) ) - -(define-metafunction L - ((simple-swap (matrix (x_1 x_2 ... x_3 x_4 ...) - ( - ((p_1 p_2 ... p_3 p_4 ... -> r_1) eqs_1 ...) - ...) - (pvar ...) - (pvar_3 ...) - natural - bool)) - (matrix (x_3 x_2 ... x_1 x_4 ...) - ( - ((p_3 p_2 ... p_1 p_4 ... -> r_1) eqs_1 ...) - ...) - (pvar ...) - (pvar_3 ...) - natural - bool) - (side-condition - (apply = - (append (list (length (term (x_2 ...))) - (length (term (x_2 ...)))) - (map length (term ((p_2 ...) ...)))))) - (side-condition - (apply = - (append (list (length (term (x_4 ...))) - (length (term (x_4 ...)))) - (map length (term ((p_4 ...) ...)))))) - (side-condition (> (length (remove-duplicates (term (simplify (p_1 ...))))) (length (remove-duplicates (term (simplify (p_3 ...)))))))) - ((simple-swap any) any) - ) - (define-namespace-anchor here) (define/contract (compile m) (-> (redex-match L m) (-> any/c any/c)) - (eval `(λ ,(second m) + (eval `(λ (a) (let ([results '()]) ,(car (apply-reduction-relation* red m)) results)) - (namespace-anchor->namespace here))) - -; TEST CASES - -(define ∅ (set)) -(define singleton set) -(define ∪ set-union) - -(test--> - red - (term - (matrix (a b c) - () - () - () - 0 - #f)) - (term ∅)) - -#;(test--> - red - (term - (matrix () - (('a 'b 1 -> 1)) - () - () - 0 - #f)) - (term ∅)) - -(test--> - red - (term - (matrix () - (((-> 1))) - () - () - 0 - #f)) - (term (∪ (singleton 1) - (matrix () - () - () - () - 0 - #f)))) - -(test--> - red - (term (matrix (a) - (((wc -> 1))) - () - () - 0 - #f)) - (term (∪ (singleton 1) - (matrix (a) - () - () - () - 0 - #f)))) - -(test--> - red - (term (matrix (a b) - (((wc wc -> 1)) - ((wc 12 -> 2))) - () - () - 0 - #f)) - (term (∪ (singleton 1) - (matrix (a b) - (((wc 12 -> 2))) - () - () - 0 - #f)))) - -(test--> - red - (term (matrix (x y z) - (((wc wc wc -> 1)) - ((wc wc wc -> 2)) - ((wc wc wc -> 3))) - () - () - 0 - #f)) - #;(term (matrix (y x z) - ((wc wc wc -> 1) - (wc wc wc -> 2) - (wc wc wc -> 3)) - () - )) - #;(term (matrix (z y x) - ((wc wc wc -> 1) - (wc wc wc -> 2) - (wc wc wc -> 3)) - ())) - (term (∪ (singleton 1) - (matrix (x y z) - (((wc wc wc -> 2)) - ((wc wc wc -> 3))) - () - () - 0 - #f)))) - -(test--> - red - (term (matrix (a b c) - (((wc 'y 'z -> 1)) - ((wc 'q 'r -> 2)) - ((wc 'b 'c -> 3))) - () - () - 0 - #f)) - #;(term (matrix (b a c) - (('y wc 'z -> 1) - ('q wc 'r -> 2) - ('b wc 'c -> 3)) - () - )) - (term (matrix (b c) - ((('y 'z -> 1)) - (('q 'r -> 2)) - (('b 'c -> 3))) - () - () - 0 - #f))) - -(test--> - red - (term - (matrix (ee a b) - ((('k 'a 'b -> 1)) - (((or 'ww 'ee) 'j 'k -> 2)) - (('d 'c 'e -> 3))) - () - () - 0 - #f)) - (term - (matrix (ee a b) - ((('k 'a 'b -> 1)) - (('ww 'j 'k -> 2)) - (('ee 'j 'k -> 2)) - (('d 'c 'e -> 3))) - () - () - 0 - #f))) - -#;(test--> - red - (term (matrix (a b) - ((px 1 2 -> 1) - (wc 3 4 -> 2)) - ())) - (term (∪ (let - ((px a)) - (matrix (b) - ((1 2 -> 1)) - (px))) - (matrix (a b) - ((wc 3 4 -> 2)) - ())))) - -(test--> - red - (term (matrix (a b c) - ((((lit-name px wc) 1 2 -> 1) (px #f)) - ((wc 3 4 -> 2))) - () - () - 0 - #f)) - (term (matrix (a b c) - (((wc 1 2 -> 1) (px #f a)) - ((wc 3 4 -> 2))) - () - () - 0 - #f))) - -(test--> - red - (term (matrix (a b c) - ((((lit-name px lit-number) 1 2 -> 1) (px #f)) - (((lit-name py lit-variable) 3 4 -> 2) (py #f))) - () - () - 0 - #f)) - (term (matrix (a b c) - (((lit-number 1 2 -> 1) (px #f a)) - (((lit-name py lit-variable) 3 4 -> 2) (py #f))) - () - () - 0 - #f))) - -#;(test--> - red - (term (matrix (a b c) - (((lit-name px wc) 1 2 -> 1) - ((lit-name py wc) 3 4 -> 2)) - (px) - () - 0 - #f)) - (term (∪ (cond ((equal? px a) - (matrix (a b c) - ((wc 1 2 -> 1)) - (px) - () - 0 - #f)) - (else ∅)) - (matrix (a b c) - (((lit-name py wc) 3 4 -> 2)) - (px) - () - 0 - #f)))) - -(test--> - red - (term (matrix (x y z) - ((('x 'y 'z -> 1)) - ((1 2 'h -> 2))) - () - () - 0 - #f)) - (term (∪ (cond ((eqv? 'x x) - (matrix (y z) - ((('y 'z -> 1))) - () - () - 0 - #f)) - ((eqv? 1 x) - (matrix (y z) - (((2 'h -> 2))) - () - () - 0 - #f)) - (else ∅)) - (matrix (y z) - () - () - () - 0 - #f)))) - -(test--> - red - (term (matrix (a b c) - ((((cons 'x (cons 'y '())) 'y 'z -> 1)) - ((1 2 'h -> 2)) - ((wc 9 'g -> 3))) - () - () - 0 - #f)) - (term (∪ (cond - ((cons? a) - (matrix ((car a) (cdr a) b c) - ((('x (cons 'y '()) 'y 'z -> 1))) - () - () - 0 - #f)) - ((eqv? 1 a) - (matrix (b c) - (((2 'h -> 2))) - () - () - 0 - #f)) - (else ∅)) - (matrix (b c) - (((9 'g -> 3))) - () - () - 0 - #f)))) - -; Contexts -(test--> - red - (term - (∪ (matrix () - (((-> 1))) - () - () - 0 - #f))) - (term (∪ - (∪ (singleton 1) - (matrix () - () - () - () - 0 - #f))))) - -(test--> - red - (term - (let ((px 1)) (matrix () - (((-> 1))) - () - () - 0 - #f))) - (term (let ((px 1)) - (∪ (singleton 1) - (matrix () - () - () - () - 0 - #f))))) - -(test--> - red - (term - (cond [(cons? a) (matrix () - (((-> 1))) - () - () - 0 - #f)])) - (term - (cond [(cons? a) - (∪ (singleton 1) - (matrix () - () - () - () - 0 - #f))]))) - -(test--> - red - (term - (cond [(cons? a) (matrix () - (((-> 1))) - () - () - 0 - #f)])) - (term - (cond [(cons? a) - (∪ (singleton 1) - (matrix () - () - () - () - 0 - #f))]))) - -(test--> - red - (term (cond [(cons? a) - (singleton 1)] - [(eqv? 1 a) - (matrix () - (((-> 2))) - () - () - 0 - #f)] - [(eqv? 2 b) - (matrix () - (((-> 3))) - () - () - 0 - #f)])) - (term (cond [(cons? a) - (singleton 1)] - [(eqv? 1 a) - (∪ (singleton 2) - (matrix () - () - () - () - 0 - #f))] - [(eqv? 2 b) - (matrix () - (((-> 3))) - () - () - 0 - #f)]))) - -(test-results) + (namespace-anchor->namespace here))) \ No newline at end of file diff --git a/collects/redex/private/compiler/redextomatrix.rkt b/collects/redex/private/compiler/redextomatrix.rkt index 2e359970e1..7d919fc4e3 100644 --- a/collects/redex/private/compiler/redextomatrix.rkt +++ b/collects/redex/private/compiler/redextomatrix.rkt @@ -1,173 +1,40 @@ #lang racket -(require redex) +(require (except-in redex make-bind plug)) (require "match.rkt") (require racket/set) (require profile) +(require (only-in "../../private/matcher.rkt" + make-bindings + make-bind + make-mtch + build-flat-context + the-hole + ) + (lib "list.ss")) + +(define plug (λ (x y) + (cond + ((cons? x) + (cons (plug (car x) y) (plug (cdr x) y))) + ((or (equal? x the-hole) (equal? x (term hole))) + y) + (else x)))) (provide test-red-rel - test-non-term) + test-non-term + test-redex-match) +; holds symbols for language (define lit-table (make-hash)) + +; holds or pattern versions of the input (define or-table (make-hash)) + +; holds compiled code (define nt-table (make-hash)) -(define set-from-list - (λ (lst) - (apply set lst))) - (define-struct nt-struct (match-bool match-set)) -#;(define lang '(define-language T - (n (number_1 ... number_1 ...)) - (m ((number_1 number_1) ...)) - (o ((number_1 ... number_1 ...) ...)) - (q ((number_1 ... number_1 ...) ... (number_1 ... number_1 ...) ...)) - )) - -#;(define lang '(define-language T - (e (e e ...) (if0 e e e) x v) - (v (λ (x ...) e) number * +) - (E (v ... E e ...) (if0 E e e) hole) - (x (variable-except if0 λ * +))) - ) - -#;(define lang-rr - '(reduction-relation T - (--> (in-hole C (and false B)) - (in-hole C false) - ) - (--> (in-hole C (and true B)) - (in-hole C B) - ) - (--> (in-hole C (or false B)) - (in-hole C B)) - (--> (in-hole C (or true B)) - (in-hole C true)) - )) - -#;(define-metafunction λv - subst-vars : ((x any) ... any) -> any - [(subst-vars ((x_1 any_1) x_1)) any_1] - [(subst-vars ((x_1 any_1) (any_2 ...))) - ((subst-vars ((x_1 any_1) any_2)) ...)] - [(subst-vars (side-condition - ((x_1 any_1) any_2) - (not (eq? (term x_1) (term any_2))))) - any_2] - [(subst-vars ((x_1 any_1) (x_2 any_2) ... any_3)) - (subst-vars ((x_1 any_1) (subst-vars ((x_2 any_2) ... any_3))))] - [(subst-vars (any)) any]) - -(define lang-rr - '(reduction-relation - λv - (--> ((x_1 any_1) x_1) - any_1) - (--> ((x_1 any_1) (any_2 ...)) - ,(map subst-vars (term (((x_1 any_1) any_2) ...))) ) - (--> (side-condition - ((x_1 any_1) any_2) - (and (not (list? any_2)) - (not (eq? (term x_1) (term any_2))))) - any_2) - (--> ((x_1 any_1) (x_2 any_2) (x_3 any_3) ... any_4) - ,(subst-vars (term ((x_1 any_1) ,(subst-vars (term ((x_2 any_2) (x_3 any_3) ... any_4))))))) - (--> (any) - any) - ) - ) - - -#;(define-metafunction λv - subst : (x any any) -> any - ;; 1. x_1 bound, so don't continue in λ body - [(subst (x_1 any_1 (λ (x_2 ... x_1 x_3 ...) any_2))) - (λ (x_2 ... x_1 x_3 ...) any_2)] - ;; 2. general purpose capture avoiding case - [(subst (side-condition - (x_1 any_1 (λ (x_2 ...) any_2)) - (not (memq (term x_1) (term (x_2 ...)))))) - ,(term-let ([(x_new ...) (variables-not-in (term (x_1 any_1 any_2)) (term (x_2 ...)))]) - (term - (λ (x_new ...) (subst (x_1 any_1 (subst-vars ((x_2 x_new) ... any_2)))))))] - ;; 3. replace x_1 with e_1 - [(subst (x_1 any_1 x_1)) any_1] - ;; 4. x_1 and x_2 are different, so don't replace - [(subst (side-condition - (x_1 any_1 x_2) - (not (eq? (term x_1) (term x_2))))) - x_2] - ;; the last cases cover all other expressions - [(subst (x any (e_1 e_2 ...))) - (,(subst (x any e_1)) (subst (x any e_2)) ...)] - - [(subst (x any (if0 e_1 e_2 e_3))) - (if0 (subst (x any e_1)) (subst (x any e_2)) (subst (x any e_3)))] - [(subst (x any number)) number] - [(subst (x any +)) +] - [(subst (x any *)) *]) - -#;(define lang-rr - '(reduction-relation - λv - (--> (x_1 any_1 (λ (x_2 ... x_1 x_3 ...) any_2)) - (λ (x_2 ... x_1 x_3 ...) any_2)) - (--> (side-condition - (x_1 any_1 (λ (x_2 ...) any_2)) - (not (memq (term x_1) (term (x_2 ...))))) - ,(term-let ([(x_new ...) (variables-not-in (term (x_1 any_1 any_2)) (term (x_2 ...)))]) - (term - (λ (x_new ...) ,(subst (term (x_1 any_1 ,(subst-vars (term ((x_2 x_new) ... any_2))))) )))) ) - (--> (x_1 any_1 x_1) - any_1) - (--> (side-condition - (x_1 any_1 x_2) - (not (eq? (term x_1) (term x_2)))) - x_2) - (--> (x any (e_1 e_2 ...)) - (,(subst (term (x any e_1))) ,@(map subst (term ((x any e_2) ...)))) ) - (--> (x any (if0 e_1 e_2 e_3)) - (if0 ,(subst (term (x any e_1))) ,(subst (term (x any e_2))) ,(subst (term (x any e_3))))) - (--> (x any number) - number) - (--> (x any +) - +) - (--> (x any *) - *) - ) - ) - -#;(define-metafunction λv - subst-n : ((x any) ... any) -> any - [(subst-n ((x_1 any_1) (x_2 any_2) ... any_3)) - (subst (x_1 any_1 (subst-n (x_2 any_2) ... any_3)))] - [(subst-n (any_3)) any_3]) - -#;(define lang-rr '(reduction-relation - λv - (--> ((x_1 any_1) (x_2 any_2) ... any_3) - ,(subst (term (x_1 any_1 ,(subst-n (term ((x_2 any_2) ... any_3))))))) - (--> (any_3) - any_3) - ) - ) - -#;(define lang-rr '(reduction-relation - λv - (--> (in-hole E (* number_1 number_2)) - (in-hole E ,(* (term number_1) (term number_2)))) - (--> (in-hole E (+ number_1 number_2)) - (in-hole E ,(+ (term number_1) (term number_2)))) - (--> (in-hole E (if0 0 e_1 e_2)) - (in-hole E e_1)) - (--> (in-hole E (if0 (side-condition number_1 (not (zero? (term number_1)))) e_1 e_2)) - (in-hole E e_2)) - (--> (in-hole E (side-condition ((λ (x ...) e) v ...) - (= (length (term (x ...))) - (length (term (v ...)))))) - (in-hole E ,(subst-n (term ((x v) ... e)))))) - ) - (define (compile-define-language-nts dl) (match dl [`(define-language ,(? symbol? name) @@ -258,7 +125,6 @@ [`(variable-prefix ,s) `(lit-variable-prefix ,s)] [`variable-not-otherwise-mentioned (if dl `(lit-variable-except ,@syms) `(lit-name variable-not-otherwise-mentioned (lit-variable-except ,@syms)))] [`hole 'lit-hole] - ; for now if it has an underscore assume it's a non-terminal [(? symbol? s) (if (memq s nts) (if dl @@ -286,8 +152,10 @@ ,(loop p1) ,(loop p2))] [`(hide-hole ,p) `(lit-hide-hole ,(loop p))] - [`(side-condition ,p #;,g ,e) + [`(side-condition ,p ,e) `(lit-side-condition ,(loop p) ,e)] + [`(side-condition ,p ,e ,e2) + `(lit-side-condition ,(loop p) (,e ,e2))] [`(cross ,s) (void)] [e (if (pair? pat) @@ -328,7 +196,6 @@ (hash-for-each or-table (λ (key val) - ;(printf "~a: ~a\n" key `(term (detect-hole2 0 ,val))) (hash-set! hole-table key (term (detect-hole2 0 ,val))))) (build-hole-table prev)))) ) @@ -556,6 +423,59 @@ (remove-duplicates (term (Get-Free-Name-Patterns ,p () ()))))))])))) results))) +(define (make-test-mtch a b c) (make-mtch a (build-flat-context b) c)) + +; compile-redex-match: sexp[pattern] (listof symbol[non-terminals]) (listof symbols) -> sexp[def] +(define (compile-redex-match pat nts syms) + ; prints for debuging + #;(printf "~a\n\n" + `(matrix (a) (,(let ((p (translate-redex pat nts syms #f))) + `((,p -> + (set! results (cons (make-test-mtch (make-bindings (list ,@(map (λ (x) `(make-bind ',(string->symbol (format "~s" (term (Get-Pvar ,x)))) (term ,x))) + (remove-duplicates (term (Get-Free-Name-Patterns ,p () ())))) )) + a + 'none) + results)) + ) + ,@(map (λ (x) (list x #f)) (remove-duplicates (term (Get-Free-Name-Patterns ,p () ()))))) + ) + ) () () 0 #f) + ) + #;(printf "~a\n\n" + (apply-reduction-relation* + red + `(matrix (a) (,(let ((p (translate-redex pat nts syms #f))) + `((,p -> + (set! results (cons (make-test-mtch (make-bindings (list ,@(map (λ (x) `(make-bind ',(string->symbol (format "~s" (term (Get-Pvar ,x)))) (term ,x))) + (remove-duplicates (term (Get-Free-Name-Patterns ,p () ())))) )) + a + 'none) + results)) + ) + ,@(map (λ (x) (list x #f)) (remove-duplicates (term (Get-Free-Name-Patterns ,p () ()))))) + ) + ) () () 0 #f)) + ) + `(λ (a) + (let ([results '()]) + ,(begin + (car + (apply-reduction-relation* + red + `(matrix (a) (,(let ((p (translate-redex pat nts syms #f))) + `((,p -> + (set! results (cons (make-test-mtch (make-bindings (list ,@(map (λ (x) `(make-bind ',(string->symbol (format "~s" (term (Get-Pvar ,x)))) (term ,x))) + (remove-duplicates (term (Get-Free-Name-Patterns ,p () ())))) )) + a + 'none) + results)) + ) + ,@(map (λ (x) (list x #f)) (remove-duplicates (term (Get-Free-Name-Patterns ,p () ()))))) + ) + ) () () 0 #f) + ))) + results))) + ;; make-lang-namespace: sexp[lang] -> namespace (define (make-lang-namespace lang) (define lang-defs (compile-dl lang)) @@ -566,30 +486,24 @@ ;; test-red-rel: sexp[lang] -> sexp[red-rel] (listof sexp[nts]) (listof symbol) -> sexp[term] -> sexp[term] (define (test-red-rel lang) (define namespace (make-lang-namespace lang)) - (λ (rel nts syms) + (define nts (compile-define-language-nts lang)) + (define syms (compile-define-language-lit lang nts)) + (λ (rel) (eval (compile-reduction-relation rel nts syms) namespace))) +;; test-red-match: sexp[lang] -> sexp[pat] (listof sexp[nts]) (listof symbol) -> sexp[term] -> sexp[term] +(define (test-redex-match lang) + (define namespace (make-lang-namespace lang)) + (define nts (compile-define-language-nts lang)) + (define syms (compile-define-language-lit lang nts)) + (λ (pat) + (eval (compile-redex-match pat nts syms) namespace))) + ;; sexp[lang] -> sexp[non-terminal] -> sexp[term] -> boolean (define (test-non-term lang) (define namespace (make-lang-namespace lang)) (λ (nt) - (eval `(λ (t) (,(string->symbol (format "~s-bool" nt)) t)) namespace))) - -(define-language T - (B true - false - (and B B)) - (C (and C B) - hole)) - -(define bool-red-test - (reduction-relation T - (--> (in-hole C (and false B)) - (in-hole C false) - ) - (--> (in-hole C (and true B)) - (in-hole C B) - ))) + (eval `(λ (t) (,(string->symbol (format "~s-bool" nt)) t)) namespace))) (caching-enabled? #f) @@ -597,6 +511,19 @@ (define ∪ set-union) (define singleton set) +(define natural? + (λ (x) (and + (exact-integer? x) + (not (negative? x))))) + +(define (variable-prefix? x y) + (let* ([prefix-str (symbol->string x)] + [prefix-len (string-length prefix-str)]) + (and (symbol? y) + (let ([str (symbol->string y)]) + (and ((string-length str) . >= . prefix-len) + (string=? (substring str 0 prefix-len) prefix-str)))))) + (define no-context #f) (define in-context #t) @@ -606,9 +533,4 @@ (define rev (λ (x) (if (cons? x) (reverse x) - x))) -(define or-fun (λ (x ...) (or x ...))) - -(define sing-fun (λ (x) #t)) - -(define the-hole (term hole)) + x))) \ No newline at end of file diff --git a/collects/redex/tests/compiler/matrix-tests.rkt b/collects/redex/tests/compiler/matrix-tests.rkt new file mode 100644 index 0000000000..1245c98069 --- /dev/null +++ b/collects/redex/tests/compiler/matrix-tests.rkt @@ -0,0 +1,193 @@ +#lang racket +(require redex) +(require racket/set) +(require "../../private/compiler/match.rkt") +(require "../../private/compiler/redextomatrix.rkt") + +(define the-hole (term hole)) +(define no-context #f) +(define in-context #t) +(define ∅ #f) +(define context-match (make-parameter no-context)) +(define (variable-prefix? x y) + (let* ([prefix-str (symbol->string x)] + [prefix-len (string-length prefix-str)]) + (and (symbol? y) + (let ([str (symbol->string y)]) + (and ((string-length str) . >= . prefix-len) + (string=? (substring str 0 prefix-len) prefix-str)))))) + +(define (m-test matrix input expected) + (let ((r ((compile matrix) input))) + (unless (equal? (apply set r) (apply set expected)) (printf "Matrix: ~s Input: ~s ==> Expected: ~s Got: ~s\n" matrix input expected r)))) + +(define (compiled-test func f-name input expected) + (let ((r (func input))) + (unless (equal? (apply set r) (apply set expected)) (printf "Func: ~s Input: ~s ==> Expected: ~s Got: ~s\n" f-name input expected r)))) + +(define number-f (compile `(matrix (a) (((lit-number -> (set! results (cons 1 results))))) () () 0 #f))) +(define real-f (compile `(matrix (a) (((lit-real -> (set! results (cons 1 results))))) () () 0 #f))) +(define integer-f (compile `(matrix (a) (((lit-integer -> (set! results (cons 1 results))))) () () 0 #f))) +(define natural-f (compile `(matrix (a) (((lit-natural -> (set! results (cons 1 results))))) () () 0 #f))) +(define nine-f (compile `(matrix (a) (((9 -> (set! results (cons 1 results))))) () () 0 #f))) +(define numbers-f (compile `(matrix (a) (((lit-number -> (set! results (cons 1 results)))) + ((lit-real -> (set! results (cons 2 results)))) + ((lit-integer -> (set! results (cons 3 results)))) + ((lit-natural -> (set! results (cons 4 results)))) + ((9 -> (set! results (cons 5 results))))) () () 0 #f))) +(define list-of-any-3-f (compile `(matrix (a) ((((cons wc (cons wc (cons wc '()))) -> (set! results (cons 1 results))))) () () 0 #f))) +(define variable-f (compile `(matrix (a) (((lit-variable -> (set! results (cons 1 results))))) () () 0 #f))) +(define empty-f (compile `(matrix (a) ((('() -> (set! results (cons 1 results))))) () () 0 #f))) +(define x-f (compile `(matrix (a) ((('x -> (set! results (cons 1 results))))) () () 0 #f))) +(define string-x-f (compile `(matrix (a) ((("x" -> (set! results (cons 1 results))))) () () 0 #f))) +(define string-f (compile `(matrix (a) (((lit-string -> (set! results (cons 1 results))))) () () 0 #f))) +(define hole-f (compile `(matrix (a) (((lit-hole -> (set! results (cons 1 results))))) () () 0 #f))) +(define in-hole-f (compile `(matrix (a) ((((lit-in-hole (cons lit-number (cons lit-hole '())) lit-number) -> (set! results (cons 1 results))))) () () 0 #f))) +(define hide-hole-f (compile `(matrix (a) ((((lit-in-hole (cons (lit-hide-hole lit-hole) (cons lit-hole '())) lit-number) -> (set! results (cons 1 results))))) () () 0 #f))) +(define repeat-number-f (compile `(matrix (a) ((((repeat lit-number '()) -> (set! results (cons 1 results))))) () () 0 #f))) +(define repeat-number-number-f (compile `(matrix (a) ((((repeat (cons lit-number (cons lit-number '())) '()) -> (set! results (cons 1 results))))) () () 0 #f))) +(define number_1-number_1-f (compile `(matrix (a) ((((cons (lit-name number_1 lit-number) (cons (lit-name number_1 lit-number) '())) -> (set! results (cons 1 results))) (number_1 #f))) () () 0 #f))) +(define repeat-number-repeat-any-f (compile `(matrix (a) ((((repeat lit-number (repeat wc '())) -> (set! results (cons 1 results))))) () () 0 #f))) +(define repeat-repeat-number_1-f (compile `(matrix (a) ((((repeat (repeat (lit-name number_1 lit-number) '()) '()) -> (set! results (cons 1 results))) (((number_1 ,'...) ,'...) #f))) () () 0 #f))) +(define true-false-f (compile `(matrix (a) (((#t -> (set! results (cons 1 results)))) + ((#f -> (set! results (cons 2 results))))) () () 0 #f))) +(define variable-prefix-x-f (compile `(matrix (a) ((((lit-variable-prefix x) -> (set! results (cons 1 results))))) () () 0 #f))) +(define variable-except-x-y-z-f (compile `(matrix (a) ((((lit-variable-except x y z) -> (set! results (cons 1 results))))) () () 0 #f))) + +(define (test) + (compiled-test number-f 'number-f 'x '()) + (compiled-test real-f 'real-f 'x '()) + (compiled-test integer-f 'integer-f 'x '()) + (compiled-test natural-f 'natural-f 'x '()) + (compiled-test nine-f 'nine-f 'x '()) + (compiled-test numbers-f 'numbers-f 'x '()) + + (compiled-test number-f 'number-f 0+4/5i '(1)) + (compiled-test real-f 'real-f 0+4/5i '()) + (compiled-test integer-f 'integer-f 0+4/5i '()) + (compiled-test natural-f 'natural-f 0+4/5i '()) + (compiled-test nine-f 'nine-f 0+4/5i '()) + (compiled-test numbers-f 'numbers-f 0+4/5i '(1)) + + (compiled-test number-f 'number-f 9.0 '(1)) + (compiled-test real-f 'real-f 9.0 '(1)) + (compiled-test integer-f 'integer-f 9.0 '()) + (compiled-test natural-f 'natural-f 9.0 '()) + (compiled-test nine-f 'nine-f 9.0 '()) + (compiled-test numbers-f 'numbers-f 9.0 '(1 2)) + + (compiled-test number-f 'number-f -1 '(1)) + (compiled-test real-f 'real-f -1 '(1)) + (compiled-test integer-f 'integer-f -1 '(1)) + (compiled-test natural-f 'natural-f -1 '()) + (compiled-test nine-f 'nine-f -1 '()) + (compiled-test numbers-f 'numbers-f -1 '(1 2 3)) + + (compiled-test number-f 'number-f 6 '(1)) + (compiled-test real-f 'real-f 6 '(1)) + (compiled-test integer-f 'integer-f 6 '(1)) + (compiled-test natural-f 'natural-f 6 '(1)) + (compiled-test nine-f 'nine-f 6 '()) + (compiled-test numbers-f 'numbers-f 6 '(1 2 3 4)) + + (compiled-test number-f 'number-f 9 '(1)) + (compiled-test real-f 'real-f 9 '(1)) + (compiled-test integer-f 'integer-f 9 '(1)) + (compiled-test natural-f 'natural-f 9 '(1)) + (compiled-test nine-f 'nine-f 9 '(1)) + (compiled-test numbers-f 'numbers-f 9 '(1 2 3 4 5)) + + (compiled-test list-of-any-3-f 'list-of-any-3-f 'a '()) + (compiled-test list-of-any-3-f 'list-of-any-3-f '(() () ()) '(1)) + (compiled-test list-of-any-3-f 'list-of-any-3-f '(1 2 3) '(1)) + (compiled-test list-of-any-3-f 'list-of-any-3-f '(1 (2 3) ((4))) '(1)) + + (compiled-test variable-f 'variable-f '() '()) + (compiled-test variable-f 'variable-f 'x '(1)) + (compiled-test variable-f 'variable-f '|x y x| '(1)) + (compiled-test variable-f 'variable-f '\|x '(1)) + + (compiled-test empty-f 'empty-f '() '(1)) + (compiled-test empty-f 'empty-f (list '()) '()) + (compiled-test empty-f 'empty-f 'x '()) + (compiled-test empty-f 'empty-f 9 '()) + (compiled-test empty-f 'empty-f '(1 2 3) '()) + + (compiled-test x-f 'x-f 'x '(1)) + (compiled-test x-f 'x-f 'y '()) + (compiled-test x-f 'x-f '() '()) + (compiled-test x-f 'x-f 9 '()) + (compiled-test x-f 'x-f '(1 2 3) '()) + + (compiled-test string-x-f 'string-x-f "x" '(1)) + (compiled-test string-x-f 'string-x-f "y" '()) + (compiled-test string-x-f 'string-x-f 'x '()) + (compiled-test string-x-f 'string-x-f 'y '()) + (compiled-test string-x-f 'string-x-f '() '()) + (compiled-test string-x-f 'string-x-f 9 '()) + (compiled-test string-x-f 'string-x-f '(1 2 3) '()) + + (compiled-test string-f 'string-f "x" '(1)) + (compiled-test string-f 'string-f "zyx" '(1)) + (compiled-test string-f 'string-f 'x '()) + (compiled-test string-f 'string-f 'y '()) + (compiled-test string-f 'string-f '() '()) + (compiled-test string-f 'string-f 9 '()) + (compiled-test string-f 'string-f '(1 2 3) '()) + + (compiled-test hole-f 'hole-f the-hole '(1)) + (compiled-test hole-f 'hole-f 'hole '()) + + (compiled-test in-hole-f 'in-hole-f '(1 2) '(1)) + (compiled-test in-hole-f 'in-hole-f (term (1 hole)) '()) + (compiled-test in-hole-f 'in-hole-f '(1 x) '()) + + (compiled-test hide-hole-f 'hide-hole-f (term (hole 2)) '(1)) + (compiled-test hide-hole-f 'hide-hole-f '(1 2) '()) + (compiled-test hide-hole-f 'hide-hole-f (term (1 hole)) '()) + (compiled-test hide-hole-f 'hide-hole-f '(1 x) '()) + + (compiled-test repeat-number-f 'repeat-number-f '() '(1)) + (compiled-test repeat-number-f 'repeat-number-f '(9) '(1)) + (compiled-test repeat-number-f 'repeat-number-f '(x) '()) + (compiled-test repeat-number-f 'repeat-number-f 9 '()) + (compiled-test repeat-number-f 'repeat-number-f '(1 2 3 4 5) '(1)) + (compiled-test repeat-number-f 'repeat-number-f '(1 2 3 4 y) '()) + (compiled-test repeat-number-f 'repeat-number-f '(1 2 3 4 ()) '()) + + (compiled-test repeat-number-number-f 'repeat-number-number-f '() '(1)) + (compiled-test repeat-number-number-f 'repeat-number-number-f '((1 2)) '(1)) + (compiled-test repeat-number-number-f 'repeat-number-number-f '((1 2) (4 5)) '(1)) + (compiled-test repeat-number-number-f 'repeat-number-number-f '((1 2) (1 1) (1 2 3)) '()) + (compiled-test repeat-number-number-f 'repeat-number-number-f '((1 2) (x 9)) '()) + (compiled-test repeat-number-number-f 'repeat-number-number-f '(()) '()) + + (compiled-test number_1-number_1-f 'number_1-number_1-f '(-1 -1) '(1)) + (compiled-test number_1-number_1-f 'number_1-number_1-f '(-1 1) '()) + + (compiled-test repeat-number-repeat-any-f 'repeat-number-repeat-any-f '(1 2 3 4 5) '(1)) + (compiled-test repeat-number-repeat-any-f 'repeat-number-repeat-any-f '(1 2 x 4 5) '(1)) + (compiled-test repeat-number-repeat-any-f 'repeat-number-repeat-any-f '(x 2 3 4 5) '(1)) + (compiled-test repeat-number-repeat-any-f 'repeat-number-repeat-any-f '() '(1)) + (compiled-test repeat-number-repeat-any-f 'repeat-number-repeat-any-f '(1 2 (3 4 5)) '(1)) + (compiled-test repeat-number-repeat-any-f 'repeat-number-repeat-any-f '1 '()) + + (compiled-test repeat-repeat-number_1-f 'repeat-repeat-number_1-f '() '(1)) + (compiled-test repeat-repeat-number_1-f 'repeat-repeat-number_1-f '(()) '(1)) + (compiled-test repeat-repeat-number_1-f 'repeat-repeat-number_1-f '(() ()) '(1)) + + (compiled-test true-false-f 'true-false-f #t '(1)) + (compiled-test true-false-f 'true-false-f #f '(2)) + (compiled-test true-false-f 'true-false-f 'true '()) + + (compiled-test variable-prefix-x-f 'variable-prefix-x-f 'x '(1)) + (compiled-test variable-prefix-x-f 'variable-prefix-x-f 'xyz '(1)) + (compiled-test variable-prefix-x-f 'variable-prefix-x-f 'zyx '()) + + (compiled-test variable-except-x-y-z-f 'variable-except-x-y-z-f 'x '()) + (compiled-test variable-except-x-y-z-f 'variable-except-x-y-z-f 'y '()) + (compiled-test variable-except-x-y-z-f 'variable-except-x-y-z-f 'z '()) + (compiled-test variable-except-x-y-z-f 'variable-except-x-y-z-f 'xyz '(1)) + ) + +(test) \ No newline at end of file diff --git a/collects/redex/tests/compiler/redex-tests.rkt b/collects/redex/tests/compiler/redex-tests.rkt new file mode 100644 index 0000000000..916a608c24 --- /dev/null +++ b/collects/redex/tests/compiler/redex-tests.rkt @@ -0,0 +1,876 @@ +#lang racket +(require (only-in redex term)) +(require "../../private/matcher.ss" + (only-in "../test-util.ss" equal/bindings?) + (lib "list.ss")) +(require "../../private/compiler/match.rkt") +(require "../../private/compiler/redextomatrix.rkt") + +(define (make-test-mtch a b c) (make-mtch a (build-flat-context b) c)) + +(define (build-context c) + (let loop ([c c]) + (cond + [(eq? c the-hole) the-hole] + [(pair? c) (build-cons-context (loop (car c)) (loop (cdr c)))] + [(or (null? c) + (number? c) + (symbol? c)) + (build-flat-context c)] + [else (error 'build-context "unknown ~s" c)]))) + +(define no-context #f) +(define in-context #t) +(define context-match (make-parameter no-context)) + +(define natural? + (λ (x) (and + (exact-integer? x) + (not (negative? x))))) + +(define (variable-prefix? x y) + (let* ([prefix-str (symbol->string x)] + [prefix-len (string-length prefix-str)]) + (and (symbol? y) + (let ([str (symbol->string y)]) + (and ((string-length str) . >= . prefix-len) + (string=? (substring str 0 prefix-len) prefix-str)))))) + +(define (run-match-test xs ys) + (cond + [(and (not xs) (not ys)) #t] + [(and (list? xs) + (list? ys)) + (and (andmap (λ (x) (memf (λ (y) (equal/bindings? x y)) ys)) xs) + (andmap (λ (y) (memf (λ (x) (equal/bindings? x y)) xs)) ys) + (= (length xs) (length ys)))] + [else #f])) + +(define empty-lang (test-redex-match '(define-language empty))) +(define x-lang (test-redex-match '(define-language x-lang (x (variable-except x))))) +(define ab-lang (test-redex-match '(define-language ab-lang (aa a) (bb b)))) +(define xab-lang (test-redex-match '(define-language xab-lang + (exp (+ exp exp) + number) + (ctxt (+ ctxt exp) + (+ exp ctxt) + hole) + (ec-one (+ (hole xx) exp) + (+ exp (hole xx))) + (same-in-nt ((name x any) (name x any))) + (forever-list (forever-list forever-list ...) + x) + (lsts () + (x) + x + #f) + (split-out split-out2) + (split-out2 number) + (simple simple-rhs) + (nesting-names (a (name x nesting-names)) + b) + (var variable-not-otherwise-mentioned) + (underscore exp_1) + ) + )) +(define nany-lang (test-redex-match '(define-language nany (n any number)))) + +; test-empty : sexp[pattern] sexp[term] answer -> void +;; returns #t if pat matching exp with the empty language produces ans. +(define (test-empty pat exp ans) + (let ((a ((empty-lang pat) exp))) + (unless (run-match-test ans (if (empty? a) #f a)) (printf "Pattern: ~s Input: ~s ==> Got: ~s Expected: ~s\n" pat exp a ans)) + ) + ) + +;; test-x : sexp[pattern] sexp[term] answer -> void +;; returns #t if pat matching exp with the x language produces ans. +(define (test-x pat exp ans) + (let ((a ((x-lang pat) exp))) + (unless (run-match-test ans (if (empty? a) #f a)) (printf "Pattern: ~s Input: ~s ==> Got: ~s Expected: ~s\n" pat exp a ans)) + ) + ) + +;; test-ab : sexp[pattern] sexp[term] answer -> void +;; returns #t if pat matching exp with the ab language produces ans. +(define (test-ab pat exp ans) + (let ((a ((ab-lang pat) exp))) + (unless (run-match-test ans (if (empty? a) #f a)) (printf "Pattern: ~s Input: ~s ==> Got: ~s Expected: ~s\n" pat exp a ans)) + ) + ) + +;; test-xab : sexp[pattern] sexp[term] answer -> void +;; returns #t if pat matching exp with the xab language produces ans. +(define (test-xab pat exp ans) + (let ((a ((xab-lang pat) exp))) + (unless (run-match-test ans (if (empty? a) #f a)) (printf "Pattern: ~s Input: ~s ==> Got:\n~s\nExpected:\n~s\n\n" pat exp a ans)) + ) + ) + +(define (test-nany pat exp ans) + (let ((a ((nany-lang pat) exp))) + (unless (run-match-test ans (if (empty? a) #f a)) (printf "Pattern: ~s Input: ~s ==> Got:\n~s\nExpected:\n~s\n\n" pat exp a ans)) + ) + ) + +(define (test) + (print-struct #t) + (test-empty 'any 1 (list (make-test-mtch (make-bindings (list (make-bind 'any 1))) 1 'none))) + (test-empty 'any 'true (list (make-test-mtch (make-bindings (list (make-bind 'any 'true))) 'true 'none))) + (test-empty 'any "a" (list (make-test-mtch (make-bindings (list (make-bind 'any "a"))) "a" 'none))) + (test-empty 'any '(a b) (list (make-test-mtch (make-bindings (list (make-bind 'any '(a b)))) '(a b) 'none))) + (test-empty 'any #t (list (make-test-mtch (make-bindings (list (make-bind 'any #t))) #t 'none))) + (test-empty 1 1 (list (make-test-mtch (make-bindings null) 1 'none))) + (test-empty 1 '() #f) + (test-empty 99999999999999999999999999999999999999999999999 + 99999999999999999999999999999999999999999999999 + (list (make-test-mtch (make-bindings null) + 99999999999999999999999999999999999999999999999 + 'none))) + (test-empty 99999999999999999999999999999999999999999999999 + '() + #f) + (test-empty 'x 'x (list (make-test-mtch (make-bindings null) 'x 'none))) + (test-empty 'x '() #f) + (test-empty 1 2 #f) + (test-empty "a" "b" #f) + (test-empty "a" '(x) #f) + (test-empty "a" '() #f) + (test-empty "a" "a" (list (make-test-mtch (make-bindings null) "a" 'none))) + (test-empty 'number 1 (list (make-test-mtch (make-bindings (list (make-bind 'number 1))) 1 'none))) + (test-empty 'number 'x #f) + (test-empty 'number '() #f) + (test-empty 'natural 1 (list (make-test-mtch (make-bindings (list (make-bind 'natural 1))) 1 'none))) + (test-empty 'natural 'x #f) + (test-empty 'natural '() #f) + (test-empty 'natural -1 #f) + (test-empty 'natural 1.0 #f) + (test-empty 'integer -1 (list (make-test-mtch (make-bindings (list (make-bind 'integer -1))) -1 'none))) + (test-empty 'integer 'x #f) + (test-empty 'integer '() #f) + (test-empty 'integer 1.0 #f) + (test-empty 'real 1.1 (list (make-test-mtch (make-bindings (list (make-bind 'real 1.1))) 1.1 'none))) + (test-empty 'real 'x #f) + (test-empty 'real '() #f) + (test-empty 'real 2+3i #f) + (test-empty 'string "a" (list (make-test-mtch (make-bindings (list (make-bind 'string "a"))) "a" 'none))) + (test-empty 'string 1 #f) + (test-empty 'string '() #f) + (test-empty 'variable 'x (list (make-test-mtch (make-bindings (list (make-bind 'variable 'x))) 'x 'none))) + (test-empty 'variable 1 #f) + (test-empty '(variable-except x) 1 #f) + (test-empty '(variable-except x) 'x #f) + (test-empty '(variable-except x) 'y (list (make-test-mtch (make-bindings null) 'y 'none))) + + (test-x 'x 'y (list (make-mtch (make-bindings (list (make-bind 'x 'y))) 'y 'none))) + ; added to replace: + #;(test-lang 'x 'y (list (make-mtch (make-bindings (list (make-bind 'x 'y))) 'y 'none)) + (list (make-nt 'x (list (make-rhs '(variable-except x)))))) + + (test-empty '(variable-prefix x:) 'x: (list (make-test-mtch (make-bindings null) 'x: 'none))) + (test-empty '(variable-prefix x:) 'x:x (list (make-test-mtch (make-bindings null) 'x:x 'none))) + (test-empty '(variable-prefix x:) ': #f) + (test-empty '(variable-prefix x:) '() #f) + (test-empty 'hole 1 #f) + (test-empty `hole + the-hole + (list (make-test-mtch (make-bindings (list)) the-hole 'none))) + (test-empty '(in-hole (hole 2) 1) + '(1 2) + (list (make-test-mtch (make-bindings (list)) `(1 2) 'none))) + + (test-empty '(in-hole (name E_1 ((hide-hole hole) hole)) x) + `(,the-hole x) + (list (make-test-mtch (make-bindings (list (make-bind 'E_1 `(,the-not-hole ,the-hole)))) + `(,the-hole x) + 'none))) + (test-empty '(name x number) 1 (list (make-test-mtch (make-bindings (list (make-bind 'x 1) (make-bind 'number 1))) 1 'none))) + (test-empty 'number_x 1 (list (make-test-mtch (make-bindings (list (make-bind 'number_x 1))) 1 'none))) + (test-empty 'string_y "b" (list (make-test-mtch (make-bindings (list (make-bind 'string_y "b"))) "b" 'none))) + (test-empty 'any_z '(a b) (list (make-test-mtch (make-bindings (list (make-bind 'any_z '(a b)))) '(a b) 'none))) + + ; We don't have _!_ yet + + ; (test-empty '(name x_!_1 number) 1 (list (make-test-mtch (make-bindings (list (make-bind 'number 1))) 1 'none))) + ; (test-empty '((name x_!_1 number) (name x_!_1 number)) '(1 1) #f) + ; (test-empty '((name x_!_1 number_a) (name x_!_1 number_b)) '(1 2) + ; (list (make-test-mtch (make-bindings (list (make-bind 'number_a 1) + ; (make-bind 'number_b 2))) + ; '(1 2) + ; 'none))) + ; (test-empty '(number_!_1 number_!_1) '(1 1) #f) + ; (test-empty '(number_!_1 number_!_1) '(1 2) (list (make-test-mtch (make-bindings (list)) '(1 2) 'none))) + ; (test-empty '(number_!_1 ...) '(1 2) (list (make-test-mtch (make-bindings (list)) '(1 2) 'none))) + ; (test-empty '(number_!_1 ...) '(1 2 3 4 5) (list (make-test-mtch (make-bindings (list)) '(1 2 3 4 5) 'none))) + ; (test-empty '(number_!_1 ...) '(1 2 3 1 5) (list (make-test-mtch (make-bindings (list)) '(1 2 3 1 5) 'none))) + ; (test-empty '((number_!_1 ...) (number_!_1 ...)) + ; '((1 2 3 1 5) (1 2 3 1 5)) + ; #f) + ; (test-empty '((number_!_1 ...) (number_!_1 ...)) + ; '((17 2 3 1 5) (1 2 3 1 5)) + ; (list (make-test-mtch (make-bindings (list)) '((17 2 3 1 5) (1 2 3 1 5)) 'none))) + ; (test-empty '((number_!_1 number_!_1) ... number_!_1 ...) '((1 1) (2 2) 1 3) #f) + ; (test-empty '((number_!_1 number_!_1) ... number_!_1 ...) '((1 1) (2 3) 1 2) #f) + ; (test-empty '((number_!_1 number_!_1) ... number_!_1 ...) + ; '((1 1) (2 3) 1 4) + ; (list (make-test-mtch (make-bindings (list)) '((1 1) (2 3) 1 4) 'none))) + + ; cases based on "test-ellipses" + ; (test-ellipses '(a) '(a)) + (test-empty '(a) '(a) (list (make-test-mtch (make-bindings null) '(a) 'none))) + + ; (test-ellipses '(a ...) `(,(make-repeat 'a '() #f #f))) + (test-empty '(a ...) '() (list (make-test-mtch (make-bindings null) '() 'none))) + (test-empty '(a ...) '(a) (list (make-test-mtch (make-bindings null) '(a) 'none))) + (test-empty '(a ...) '(a a a) (list (make-test-mtch (make-bindings null) '(a a a) 'none))) + (test-empty '(a ...) '(a b a) #f) + + ; (test-ellipses '((a ...) ...) `(,(make-repeat '(a ...) '() #f #f))) + (test-empty '((a ...) ...) '() (list (make-test-mtch (make-bindings null) '() 'none))) + (test-empty '((a ...) ...) '(()) (list (make-test-mtch (make-bindings null) '(()) 'none))) + (test-empty '((a ...) ...) '(() (a) (a a a)) (list (make-test-mtch (make-bindings null) '(() (a) (a a a)) 'none))) + (test-empty '((a ...) ...) '((a a a a a) () () (a a)) (list (make-test-mtch (make-bindings null) '((a a a a a) () () (a a)) 'none))) + (test-empty '((a ...) ...) '((a a a a a) () () (b a)) #f) + + ; (test-ellipses '(a ... b c ...) `(,(make-repeat 'a '() #f #f) b ,(make-repeat 'c '() #f #f))) + (test-empty '(a ... b c ...) '(b) (list (make-test-mtch (make-bindings null) '(b) 'none))) + (test-empty '(a ... b c ...) '(a b) (list (make-test-mtch (make-bindings null) '(a b) 'none))) + (test-empty '(a ... b c ...) '(b c) (list (make-test-mtch (make-bindings null) '(b c) 'none))) + (test-empty '(a ... b c ...) '(a a a b) (list (make-test-mtch (make-bindings null) '(a a a b) 'none))) + (test-empty '(a ... b c ...) '(b c c c) (list (make-test-mtch (make-bindings null) '(b c c c) 'none))) + (test-empty '(a ... b c ...) '(a a a b c c) (list (make-test-mtch (make-bindings null) '(a a a b c c) 'none))) + (test-empty '(a ... b c ...) '(a a a b b c c) #f) + + ; (test-ellipses '((name x a) ...) `(,(make-repeat '(name x a) (list (make-bind 'x '())) #f #f))) + (test-empty '((name x a) ...) '() (list (make-test-mtch (make-bindings (list (make-bind 'x '()))) '() 'none))) + (test-empty '((name x a) ...) '(a) (list (make-test-mtch (make-bindings (list (make-bind 'x '(a)))) '(a) 'none))) + (test-empty '((name x a) ...) '(a a a) (list (make-test-mtch (make-bindings (list (make-bind 'x '(a a a)))) '(a a a) 'none))) + (test-empty '((name x a) ...) '(a b a) #f) + + ; (test-ellipses '((name x (a ...)) ...) + ; `(,(make-repeat '(name x (a ...)) (list (make- bind 'x '())) #f #f))) + (test-empty '((name x (a ...)) ...) '() (list (make-test-mtch (make-bindings (list (make-bind 'x '()))) '() 'none))) + (test-empty '((name x (a ...)) ...) '(()) (list (make-test-mtch (make-bindings (list (make-bind 'x '(())))) '(()) 'none))) + (test-empty '((name x (a ...)) ...) '(() (a) (a a a)) (list (make-test-mtch (make-bindings (list (make-bind 'x '(() (a) (a a a))))) '(() (a) (a a a)) 'none))) + (test-empty '((name x (a ...)) ...) '((a a a a a) () () (a a)) (list (make-test-mtch (make-bindings (list (make-bind 'x '((a a a a a) () () (a a))))) '((a a a a a) () () (a a)) 'none))) + (test-empty '((name x (a ...)) ...) '((a a a a a) () () (b a)) #f) + + ; (test-ellipses '(((name x a) ...) ...) + ; `(,(make-repeat '((name x a) ...) (list (make-bind 'x '())) #f #f))) + (test-empty '(((name x a) ...) ...) '() (list (make-test-mtch (make-bindings (list (make-bind 'x '()))) '() 'none))) + (test-empty '(((name x a) ...) ...) '(()) (list (make-test-mtch (make-bindings (list (make-bind 'x '(())))) '(()) 'none))) + (test-empty '(((name x a) ...) ...) '(() (a) (a a a)) (list (make-test-mtch (make-bindings (list (make-bind 'x '(() (a) (a a a))))) '(() (a) (a a a)) 'none))) + (test-empty '(((name x a) ...) ...) '((a a a a a) () () (a a)) (list (make-test-mtch (make-bindings (list (make-bind 'x '((a a a a a) () () (a a))))) '((a a a a a) () () (a a)) 'none))) + (test-empty '(((name x a) ...) ...) '((a a a a a) () () (b a)) #f) + + ; (test-ellipses '((1 (name x a)) ...) + ; `(,(make-repeat '(1 (name x a)) (list (make-bind 'x '())) #f #f))) + (test-empty '((1 (name x a)) ...) '() (list (make-test-mtch (make-bindings (list (make-bind 'x '()))) '() 'none))) + (test-empty '((1 (name x a)) ...) '((1 a)) (list (make-test-mtch (make-bindings (list (make-bind 'x '(a)))) '((1 a)) 'none))) + (test-empty '((1 (name x a)) ...) '((1 a) (1 a) (1 a)) (list (make-test-mtch (make-bindings (list (make-bind 'x '(a a a)))) '((1 a) (1 a) (1 a)) 'none))) + (test-empty '((1 (name x a)) ...) '((1 a) (2 a) (1 a)) #f) + (test-empty '((1 (name x a)) ...) '((1 a) (1 b) (1 a)) #f) + + ; (test-ellipses '((any (name x a)) ...) + ; `(,(make-repeat '(any (name x a)) (list (make-bind 'any '()) + ; (make-bind 'x '())) + ; #f #f))) + (test-empty '((any (name x a)) ...) '() (list (make-test-mtch (make-bindings (list (make-bind 'any '()) (make-bind 'x '()))) '() 'none))) + (test-empty '((any (name x a)) ...) '((b a)) (list (make-test-mtch (make-bindings (list (make-bind 'any '(b)) (make-bind 'x '(a)))) '((b a)) 'none))) + (test-empty '((any (name x a)) ...) '((1 a) (2 a) (3 a)) (list (make-test-mtch (make-bindings (list (make-bind 'any '(1 2 3)) (make-bind 'x '(a a a)))) '((1 a) (2 a) (3 a)) 'none))) + (test-empty '((any (name x a)) ...) '((1 a) (2 b) (3 a)) #f) + + ; (test-ellipses '((number (name x a)) ...) + ; `(,(make-repeat '(number (name x a)) (list (make-bind 'number '()) + ; (make-bind 'x '())) + ; #f #f))) + (test-empty '((number (name x a)) ...) '() (list (make-test-mtch (make-bindings (list (make-bind 'number '()) (make-bind 'x '()))) '() 'none))) + (test-empty '((number (name x a)) ...) '((2 a)) (list (make-test-mtch (make-bindings (list (make-bind 'number '(2)) (make-bind 'x '(a)))) '((2 a)) 'none))) + (test-empty '((number (name x a)) ...) '((1 a) (2 a) (3 a)) (list (make-test-mtch (make-bindings (list (make-bind 'number '(1 2 3)) (make-bind 'x '(a a a)))) '((1 a) (2 a) (3 a)) 'none))) + (test-empty '((number (name x a)) ...) '((1 a) (2 b) (3 a)) #f) + (test-empty '((number (name x a)) ...) '((1 a) (b a) (3 a)) #f) + + ; (test-ellipses '((variable (name x a)) ...) + ; `(,(make-repeat '(variable (name x a)) (list (make-bind 'variable '()) + ; (make-bind 'x '())) + ; #f #f))) + (test-empty '((variable (name x a)) ...) '() (list (make-test-mtch (make-bindings (list (make-bind 'variable '()) (make-bind 'x '()))) '() 'none))) + (test-empty '((variable (name x a)) ...) '((x a)) (list (make-test-mtch (make-bindings (list (make-bind 'variable '(x)) (make-bind 'x '(a)))) '((x a)) 'none))) + (test-empty '((variable (name x a)) ...) '((x a) (y a) (z a)) (list (make-test-mtch (make-bindings (list (make-bind 'variable '(x y z)) (make-bind 'x '(a a a)))) '((x a) (y a) (z a)) 'none))) + (test-empty '((variable (name x a)) ...) '((x a) (y b) (z a)) #f) + (test-empty '((variable (name x a)) ...) '((1 a) (b a) (c a)) #f) + + ; (test-ellipses '(((name x a) (name y b)) ...) + ; `(,(make-repeat '((name x a) (name y b)) (list (make-bind 'x '()) (make-bind 'y '())) #f #f))) + (test-empty '(((name x a) (name y b)) ...) '() (list (make-test-mtch (make-bindings (list (make-bind 'y '()) (make-bind 'x '()))) '() 'none))) + (test-empty '(((name x a) (name y b)) ...) '((a b)) (list (make-test-mtch (make-bindings (list (make-bind 'y '(b)) (make-bind 'x '(a)))) '((a b)) 'none))) + (test-empty '(((name x a) (name y b)) ...) '((a b) (a b)) (list (make-test-mtch (make-bindings (list (make-bind 'y '(b b)) (make-bind 'x '(a a)))) '((a b) (a b)) 'none))) + (test-empty '(((name x a) (name y b)) ...) '((a b) (b a)) #f) + (test-empty '(((name x a) (name y b)) ...) '(a b) #f) + (test-empty '(((name x a) (name y b)) ...) '(a b a b) #f) + (test-empty '(((name x a) (name y b)) ...) '(a c) #f) + + ; (test-ellipses '((name x (name y b)) ...) + ; `(,(make-repeat '(name x (name y b)) (list (make-bind 'x '()) (make-bind 'y '())) #f #f))) + (test-empty '((name x (name y b)) ...) '() (list (make-test-mtch (make-bindings (list (make-bind 'y '()) (make-bind 'x '()))) '() 'none))) + (test-empty '((name x (name y b)) ...) '(b) (list (make-test-mtch (make-bindings (list (make-bind 'y '(b)) (make-bind 'x '(b)))) '(b) 'none))) + (test-empty '((name x (name y b)) ...) '(b b b) (list (make-test-mtch (make-bindings (list (make-bind 'y '(b b b)) (make-bind 'x '(b b b)))) '(b b b) 'none))) + (test-empty '((name x (name y b)) ...) '(b b a) #f) + + ; (test-ellipses '((in-hole (name x a) (name y b)) ...) + ; `(,(make-repeat '(in-hole (name x a) (name y b)) + ; (list (make-bind 'y '()) (make-bind 'x '())) #f #f))) + (test-empty '((in-hole (name x a) (name y b)) ...) '() (list (make-test-mtch (make-bindings (list (make-bind 'y '()) (make-bind 'x '()))) '() 'none))) + (test-empty '((in-hole (name x a) (name y b)) ...) '(a) #f) + + ; We don't have ..._ or ..._!_ yet + ; (test-ellipses '(a ..._1) + ; `(,(make-repeat 'a (list) '..._1 #f))) + ; (test-ellipses '(a ..._!_1) + ; `(,(make-repeat 'a (list) '..._!_1 #t))) + + + (test-empty '(((name x 5) (name y 5)) ...) '() (list (make-test-mtch (make-bindings (list (make-bind 'x '()) (make-bind 'y '()))) '() 'none))) + (test-empty '(((name x 5) (name y 5)) ...) '((5 5)) (list (make-test-mtch (make-bindings (list (make-bind 'x '(5)) (make-bind 'y '(5)))) '((5 5)) 'none))) + (test-empty '(((name x 5) (name y 5)) ...) '((5 5) (5 5) (5 5)) (list (make-test-mtch (make-bindings (list (make-bind 'y '(5 5 5)) (make-bind 'x '(5 5 5)))) '((5 5) (5 5) (5 5)) 'none))) + (test-empty '(((name x 5) (name y 5)) ...) '((5 6)) #f) + + (test-empty '((number number) ...) '() (list (make-test-mtch (make-bindings (list (make-bind 'number '()))) '() 'none))) + (test-empty '((number number) ...) '((5 5)) (list (make-test-mtch (make-bindings (list (make-bind 'number '(5)))) '((5 5)) 'none))) + (test-empty '((number number) ...) '((1 1) (2 2) (3 3)) (list (make-test-mtch (make-bindings (list (make-bind 'number '(1 2 3)))) '((1 1) (2 2) (3 3)) 'none))) + (test-empty '((number number) ...) '((1 2)) #f) + + (test-empty '(number ... number ...) '() (list (make-test-mtch (make-bindings (list (make-bind 'number '()))) '() 'none))) + (test-empty '(number ... number ...) '(1 1) (list (make-test-mtch (make-bindings (list (make-bind 'number '(1)))) '(1 1) 'none))) + (test-empty '(number ... number ...) '(1 2 1 2) (list (make-test-mtch (make-bindings (list (make-bind 'number '(1 2)))) '(1 2 1 2) 'none))) + (test-empty '(number ... number ...) '(1 2) #f) + + (test-empty '((number ... number ...) ...) '() (list (make-test-mtch (make-bindings (list (make-bind 'number '()))) '() 'none))) + (test-empty '((number ... number ...) ...) '(()) (list (make-test-mtch (make-bindings (list (make-bind 'number '(())))) '(()) 'none))) + (test-empty '((number ... number ...) ...) '((1 1)) (list (make-test-mtch (make-bindings (list (make-bind 'number '((1))))) '((1 1)) 'none))) + (test-empty '((number ... number ...) ...) '((1 1) (2 2) (1 2 3 1 2 3) (4 5 6 4 5 6)) (list (make-test-mtch (make-bindings + (list (make-bind 'number '((1) (2) (1 2 3) (4 5 6))))) + '((1 1) (2 2) (1 2 3 1 2 3) (4 5 6 4 5 6)) + 'none))) + (test-empty '((number ... number ...) ...) '((1 1) (2 2) (1 2 3 1 2 3) (4 5 6 4 5 -6)) #f) + + (test-empty '((name number any) (number ... number ...) ...) '(()) (list (make-test-mtch (make-bindings (list (make-bind 'any '()) (make-bind 'number '()))) '(()) 'none))) + (test-empty '((name number any) (number ... number ...) ...) '(((1)) (1 1)) (list (make-test-mtch (make-bindings (list (make-bind 'any '((1))) (make-bind 'number '((1))))) '(((1)) (1 1)) 'none))) + (test-empty '((name number any) (number ... number ...) ...) '(((1)) (1 2)) #f) + (test-empty '((name number any) (number ... number ...) ...) '(((2)) (1 1)) #f) + + (test-empty '((number ... number ...) ... (name number any)) '(()) (list (make-test-mtch (make-bindings (list (make-bind 'any '()) (make-bind 'number '()))) '(()) 'none))) + (test-empty '((number ... number ...) ... (name number any)) '((1 1) ((1))) (list (make-test-mtch (make-bindings (list (make-bind 'any '((1))) (make-bind 'number '((1))))) '((1 1) ((1))) 'none))) + (test-empty '((number ... number ...) ... (name number any)) '((1 2) ((1))) #f) + (test-empty '((number ... number ...) ... (name number any)) '((1 1) ((2))) #f) + + ; causes an error + #;(test-empty '((number ... number ...) ... (number ... number ...) ...) '() (list (make-test-mtch (make-bindings (list (make-bind 'number '()))) '() 'none))) + + (test-empty '() '() (list (make-test-mtch (make-bindings null) '() 'none))) + (test-empty '(a) '(a) (list (make-test-mtch (make-bindings null) '(a) 'none))) + (test-empty '(a) '(b) #f) + (test-empty '(a b) '(a b) (list (make-test-mtch (make-bindings null) '(a b) 'none))) + (test-empty '(a b) '(a c) #f) + (test-empty '() 1 #f) + (test-empty '(#f x) '(#f x) (list (make-test-mtch (make-bindings null) '(#f x) 'none))) + (test-empty '(#f (name y any)) '(#f) #f) + (test-empty '(in-hole (z hole) a) '(z a) (list (make-test-mtch (make-bindings (list)) '(z a) 'none))) + (test-empty '(in-hole (z hole) (in-hole (x hole) a)) + '(z (x a)) + (list (make-test-mtch (make-bindings (list)) '(z (x a)) 'none))) + + #;(run-test/cmp 'in-hole-zero-holes + (with-handlers ([exn:fail? (λ (e) (regexp-match #rx"zero holes" (exn-message e)))]) + (test-empty '(in-hole (1 2) 2) '(1 2) 'never-gets-here) + 'should-have-raised-an-exception) + '("zero holes") + equal?) + + + (test-empty '(in-hole (in-hole (x hole) hole) y) + '(x y) + (list (make-test-mtch (make-bindings (list)) '(x y) 'none))) + + (test-empty '(number number) '(1 1) (list (make-test-mtch (make-bindings (list (make-bind 'number 1))) '(1 1) 'none))) + (test-empty '((name x number) (name x number)) '(1 1) (list (make-test-mtch (make-bindings (list (make-bind 'x 1) (make-bind 'number 1))) '(1 1) 'none))) + (test-empty '((name x number_q) (name x number_r)) '(1 1) (list (make-test-mtch (make-bindings (list (make-bind 'x 1) + (make-bind 'number_q 1) + (make-bind 'number_r 1))) + '(1 1) + 'none))) + (test-empty '(number number) '(1 2) #f) + (test-empty '((name x number) (name x number)) '(1 2) #f) + (test-empty '((name x number_q) (name x number_r)) '(1 2) #f) + + (test-empty '(a ...) '() (list (make-test-mtch (make-bindings empty) '() 'none))) + (test-empty '(a ...) '(a) (list (make-test-mtch (make-bindings empty) '(a) 'none))) + (test-empty '(a ...) '(a a) (list (make-test-mtch (make-bindings empty) '(a a) 'none))) + (test-empty '((name x a) ...) '() (list (make-test-mtch (make-bindings (list (make-bind 'x '()))) '() 'none))) + (test-empty '((name x a) ...) '(a) (list (make-test-mtch (make-bindings (list (make-bind 'x '(a)))) '(a) 'none))) + (test-empty '((name x a) ...) '(a a) (list (make-test-mtch (make-bindings (list (make-bind 'x '(a a)))) '(a a) 'none))) + (test-empty '(hole ...) '() (list (make-test-mtch (make-bindings empty) '() 'none))) + (test-empty '(b ... a ...) '() (list (make-test-mtch (make-bindings empty) '() 'none))) + (test-empty '(b ... a ...) '(a) (list (make-test-mtch (make-bindings empty) '(a) 'none))) + (test-empty '(b ... a ...) '(b) (list (make-test-mtch (make-bindings empty) '(b) 'none))) + (test-empty '(b ... a ...) '(b a) (list (make-test-mtch (make-bindings empty) '(b a) 'none))) + (test-empty '(b ... a ...) '(b b a a) (list (make-test-mtch (make-bindings empty) '(b b a a) 'none))) + (test-empty '(b ... a ...) '(a a) (list (make-test-mtch (make-bindings empty) '(a a) 'none))) + (test-empty '(b ... a ...) '(b b) (list (make-test-mtch (make-bindings empty) '(b b) 'none))) + + ; (test-empty '(a ..._1 a ..._2) + ; '(a) + ; (list (make-test-mtch (make-bindings (list (make-bind '..._1 1) (make-bind '..._2 0))) '(a) 'none) + ; (make-test-mtch (make-bindings (list (make-bind '..._1 0) (make-bind '..._2 1))) '(a) 'none))) + ; (test-empty '(a ..._1 a ..._1) '(a) #f) + ; (test-empty '(a ..._1 a ..._1) + ; '(a a) + ; (list (make-test-mtch (make-bindings (list (make-bind '..._1 1))) '(a a) 'none))) + ; + ; (test-empty '((name x a) ..._!_1 (name y a) ..._!_1) + ; '(a a) + ; (list (make-test-mtch (make-bindings (list (make-bind 'x '()) (make-bind 'y '(a a)))) '(a a) 'none) + ; (make-test-mtch (make-bindings (list (make-bind 'x '(a a)) (make-bind 'y '()))) '(a a) 'none))) + ; + ; (test-empty '((name y b) ... (name x a) ...) '() + ; (list (make-test-mtch (make-bindings (list (make-bind 'x '()) + ; (make-bind 'y '()))) + ; '() + ; 'none))) + ; (test-empty '((name y b) ... (name x a) ...) '(a) + ; (list (make-test-mtch (make-bindings (list (make-bind 'x '(a)) + ; (make-bind 'y '()))) + ; '(a) + ; 'none))) + ; (test-empty '((name y b) ... (name x a) ...) '(b) + ; (list (make-test-mtch (make-bindings (list (make-bind 'x '()) + ; (make-bind 'y '(b)))) + ; '(b) + ; 'none))) + ; (test-empty '((name y b) ... (name x a) ...) '(b b a a) + ; (list (make-test-mtch (make-bindings (list (make-bind 'x '(a a)) + ; (make-bind 'y '(b b)))) + ; '(b b a a) + ; 'none))) + ; (test-empty '((name y a) ... (name x a) ...) '(a) + ; (list (make-test-mtch (make-bindings (list (make-bind 'x '()) + ; (make-bind 'y '(a)))) + ; '(a) + ; 'none) + ; (make-test-mtch (make-bindings (list (make-bind 'x '(a)) + ; (make-bind 'y '()))) + ; '(a) + ; 'none))) + ; (test-empty '((name y a) ... (name x a) ...) '(a a) + ; (list (make-test-mtch (make-bindings (list (make-bind 'x '()) + ; (make-bind 'y '(a a)))) + ; '(a a) + ; 'none) + ; (make-test-mtch (make-bindings (list (make-bind 'x '(a)) + ; (make-bind 'y '(a)))) + ; '(a a) + ; 'none) + ; (make-test-mtch (make-bindings (list (make-bind 'x '(a a)) + ; (make-bind 'y '()))) + ; '(a a) + ; 'none))) + #;(test-ab '(bb_y ... aa_x ...) '() + (list (make-test-mtch (make-bindings (list (make-bind 'aa_x '()) + (make-bind 'bb_y '()))) + '() + 'none))) + #;(test-ab '(bb_y ... aa_x ...) '(a) + (list (make-test-mtch (make-bindings (list (make-bind 'aa_x '(a)) + (make-bind 'bb_y '()))) + '(a) + 'none))) + #;(test-ab '(bb_y ... aa_x ...) '(b) + (list (make-test-mtch (make-bindings (list (make-bind 'aa_x '()) + (make-bind 'bb_y '(b)))) + '(b) + 'none))) + #;(test-ab '(bb_y ... aa_x ...) '(b b a a) + (list (make-test-mtch (make-bindings (list (make-bind 'aa_x '(a a)) + (make-bind 'bb_y '(b b)))) + '(b b a a) + 'none))) + #;(test-ab '(aa_y ... aa_x ...) '(a) + (list (make-test-mtch (make-bindings (list (make-bind 'aa_x '()) + (make-bind 'aa_y '(a)))) + '(a) + 'none) + (make-test-mtch (make-bindings (list (make-bind 'aa_x '(a)) + (make-bind 'aa_y '()))) + '(a) + 'none))) + #;(test-ab '(aa_y ... aa_x ...) '(a a) + (list (make-test-mtch (make-bindings (list (make-bind 'aa_x '()) + (make-bind 'aa_y '(a a)))) + '(a a) + 'none) + (make-test-mtch (make-bindings (list (make-bind 'aa_x '(a)) + (make-bind 'aa_y '(a)))) + '(a a) + 'none) + (make-test-mtch (make-bindings (list (make-bind 'aa_x '(a a)) + (make-bind 'aa_y '()))) + '(a a) + 'none))) + + (test-empty '((name x number) ...) '(1 2) (list (make-test-mtch (make-bindings (list (make-bind 'x '(1 2)) (make-bind 'number '(1 2)))) '(1 2) 'none))) + + (test-empty '(a ...) '(b) #f) + (test-empty '(a ... b ...) '(c) #f) + (test-empty '(a ... b) '(b c) #f) + (test-empty '(a ... b) '(a b c) #f) + + + (test-nany '(n n ...) '((1 1) 1 1) (list (make-test-mtch (make-bindings (list (make-bind 'n '(1 1)))) '((1 1) 1 1) 'none))) + (test-nany '(n (n ...)) '((1 1) (1 1)) (list (make-test-mtch (make-bindings (list (make-bind 'n '(1 1)))) '((1 1) (1 1)) 'none))) + (test-empty '((name x any) + ((name x number) ...)) + '((1 1) (1 1)) + (list (make-test-mtch (make-bindings (list (make-bind 'x '(1 1)) + (make-bind 'any '(1 1)) + (make-bind 'number '(1 1)))) + '((1 1) (1 1)) + 'none))) + + (test-empty '((variable_1 variable_1) ...) + '((x y)) + #f) + + + (test-empty '(number ...) '() + (list (make-test-mtch (make-bindings (list (make-bind 'number '()))) '() 'none))) + (test-ab '(aa ...) '() + (list (make-test-mtch (make-bindings (list (make-bind 'aa '()))) '() 'none))) + + + ;; testing block-in-hole + (test-empty '(hide-hole a) 'b #f) + (test-empty '(hide-hole a) 'a (list (make-test-mtch (make-bindings '()) 'a 'none))) + (test-empty '(hide-hole a) '(block-in-hole a) #f) + (test-empty '(in-hole (x (hide-hole hole)) 1) '(x 1) #f) + (test-empty '(in-hole (x hole) 1) '(x 1) (list (make-test-mtch (make-bindings '()) '(x 1) 'none))) + (test-empty '(in-hole ((hole #f) (hide-hole hole)) junk) + '(junk junk2) + #f) + + (test-xab 'lsts '() (list (make-test-mtch (make-bindings (list (make-bind 'lsts '()))) '() 'none))) + (test-xab 'lsts '(x) (list (make-test-mtch (make-bindings (list (make-bind 'lsts '(x)))) '(x) 'none))) + (test-xab 'lsts 'x (list (make-test-mtch (make-bindings (list (make-bind 'lsts 'x))) 'x 'none))) + (test-xab 'lsts #f (list (make-test-mtch (make-bindings (list (make-bind 'lsts #f))) #f 'none))) + (test-xab 'split-out '1 (list (make-test-mtch (make-bindings (list (make-bind 'split-out 1))) '1 'none))) + + (test-xab 'exp 1 (list (make-test-mtch (make-bindings (list (make-bind 'exp 1))) 1 'none))) + (test-xab 'exp '(+ 1 2) (list (make-test-mtch (make-bindings (list (make-bind 'exp '(+ 1 2)))) '(+ 1 2) 'none))) + (test-xab '(in-hole ctxt any) + '1 + (list (make-test-mtch (make-bindings (list (make-bind 'ctxt the-hole) (make-bind 'any 1))) 1 'none))) + (test-xab '(in-hole ctxt (name x any)) + '1 + (list (make-test-mtch (make-bindings (list (make-bind 'ctxt the-hole) (make-bind 'x 1) (make-bind 'any 1))) 1 'none))) + + (test-xab '(in-hole (name c ctxt) (name x any)) + '(+ 1 2) + (list (make-test-mtch (make-bindings (list (make-bind 'ctxt (build-context the-hole)) + (make-bind 'c (build-context the-hole)) + (make-bind 'x '(+ 1 2)) + (make-bind 'any '(+ 1 2)))) + '(+ 1 2) 'none) + (make-test-mtch (make-bindings (list (make-bind 'ctxt (build-context `(+ ,the-hole 2))) + (make-bind 'c (build-context `(+ ,the-hole 2))) + (make-bind 'x 1) + (make-bind 'any 1))) + '(+ 1 2) 'none) + (make-test-mtch (make-bindings (list (make-bind 'ctxt (build-context `(+ 1 ,the-hole))) + (make-bind 'c (build-context `(+ 1 ,the-hole))) + (make-bind 'x 2) + (make-bind 'any 2))) + '(+ 1 2) 'none))) + (test-xab '(in-hole (name c ctxt) (name i (+ number_1 number_2))) + '(+ (+ 1 2) (+ 3 4)) + (list (make-test-mtch + (make-bindings (list (make-bind 'i '(+ 1 2)) + (make-bind 'number_1 1) + (make-bind 'number_2 2) + (make-bind 'ctxt (build-context `(+ ,the-hole (+ 3 4)))) + (make-bind 'c (build-context `(+ ,the-hole (+ 3 4)))))) + '(+ (+ 1 2) (+ 3 4)) + 'none) + (make-test-mtch (make-bindings (list (make-bind 'i '(+ 3 4)) + (make-bind 'number_1 3) + (make-bind 'number_2 4) + (make-bind 'ctxt `(+ (+ 1 2) ,the-hole)) + (make-bind 'c `(+ (+ 1 2) ,the-hole)))) + '(+ (+ 1 2) (+ 3 4)) + 'none))) + + (test-empty '(in-hole ((z hole)) (name x any)) + '((z a)) + (list (make-test-mtch (make-bindings (list (make-bind 'x 'a) (make-bind 'any 'a))) '((z a)) 'none))) + ; in-hole-name bug + (test-empty '(in-hole (name c (z ... hole z ...)) any) + '(z z) + (list + (make-test-mtch (make-bindings (list (make-bind 'c `(z ,the-hole)) (make-bind 'any 'z))) '(z z) 'none) + (make-test-mtch (make-bindings (list (make-bind 'c `(,the-hole z)) (make-bind 'any 'z))) '(z z) 'none))) + (test-empty '(in-hole (name c (z ... hole z ...)) any) + '(z z z) + (list + (make-test-mtch (make-bindings (list (make-bind 'c `(z z ,the-hole)) (make-bind 'any 'z))) '(z z z) 'none) + (make-test-mtch (make-bindings (list (make-bind 'c `(z ,the-hole z)) (make-bind 'any 'z))) '(z z z) 'none) + (make-test-mtch (make-bindings (list (make-bind 'c `(,the-hole z z)) (make-bind 'any 'z))) '(z z z) 'none))) + + (test-empty '(z (in-hole (name c (z hole)) a)) + '(z (z a)) + (list + (make-test-mtch (make-bindings (list (make-bind 'c `(z ,the-hole)))) + '(z (z a)) + 'none))) + + (test-empty '(a (in-hole (name c1 (b (in-hole (name c2 (c hole)) d) hole)) e)) + '(a (b (c d) e)) + (list + (make-test-mtch (make-bindings (list (make-bind 'c2 `(c ,the-hole)) + (make-bind 'c1 `(b (c d) ,the-hole)))) + '(a (b (c d) e)) + 'none))) + + (test-empty '(in-hole (in-hole hole hole) a) + 'a + (list (make-test-mtch (make-bindings (list)) 'a 'none))) + + (test-empty '(a (b (in-hole (name c1 (in-hole (name c2 (c hole)) (d hole))) e))) + '(a (b (c (d e)))) + (list + (make-test-mtch (make-bindings (list (make-bind 'c1 `(c (d ,the-hole))) + (make-bind 'c2 `(c ,the-hole)))) + '(a (b (c (d e)))) + 'none))) + + (test-empty '(in-hole (name c1 (in-hole (name c2 (c hole)) (d hole))) e) + '(c (d e)) + (list + (make-test-mtch (make-bindings (list (make-bind 'c1 `(c (d ,the-hole))) + (make-bind 'c2 `(c ,the-hole)))) + '(c (d e)) + 'none))) + + (test-empty '(in-hole (in-hole (c hole) (d hole)) e) + '(c (d e)) + (list (make-test-mtch (make-bindings null) '(c (d e)) 'none))) + + (test-empty `(+ 1 (side-condition any (lambda (bindings) #t) #t)) + '(+ 1 b) + (list (make-test-mtch (make-bindings (list (make-bind 'any 'b))) '(+ 1 b) 'none))) + (test-empty `(+ 1 (side-condition any (lambda (bindings) #f) #f)) + '(+ 1 b) + #f) + + (test-empty `(+ 1 (side-condition b (lambda (bindings) #t) #t)) + '(+ 1 b) + (list (make-test-mtch (make-bindings '()) '(+ 1 b) 'none))) + (test-empty `(+ 1 (side-condition a (lambda (bindings) #t)) #t) + '(+ 1 b) + #f) + + (test-empty `(side-condition (name x any) (lambda (bindings) (eq? (term x) #;(lookup-binding bindings 'x) 'a)) (eq? (term x) 'a)) + 'a + (list + (make-test-mtch (make-bindings (list (make-bind 'x 'a) + (make-bind 'any 'a))) + 'a + 'none))) + + (test-empty `(+ 1 (side-condition (name x any) (lambda (bindings) (eq? (term x) #;(lookup-binding bindings 'x) 'a)) (eq? (term x) 'a))) + '(+ 1 a) + (list + (make-test-mtch (make-bindings (list (make-bind 'x 'a) + (make-bind 'any 'a))) + '(+ 1 a) + 'none))) + + (test-empty `(side-condition (name x any) (lambda (bindings) (eq? (term x) #;(lookup-binding bindings 'x) 'a)) (eq? (term x) 'a)) + 'b + #f) + + (test-empty `(+ 1 (side-condition (name x any) (lambda (bindings) (eq? (term x) #;(lookup-binding bindings 'x) 'a)) (eq? (term x) 'a))) + '(+ 1 b) + #f) + + #;(test-empty `(side-condition ((any_1 ..._a) (any_2 ..._a)) + (lambda (bindings) (error 'should-not-be-called)) + (error 'should-not-be-called)) + '((1 2 3) (4 5)) + #f) + + (test-xab 'exp_1 + '(+ 1 2) + (list (make-test-mtch (make-bindings (list (make-bind 'exp_1 '(+ 1 2)))) '(+ 1 2) 'none))) + (test-xab '(exp_1 exp_2) + '((+ 1 2) (+ 3 4)) + (list (make-test-mtch (make-bindings (list (make-bind 'exp_1 '(+ 1 2)) (make-bind 'exp_2 '(+ 3 4)))) + '((+ 1 2) (+ 3 4)) + 'none))) + (test-xab '(exp_1 exp_1) + '((+ 1 2) (+ 3 4)) + #f) + (test-xab 'nesting-names + 'b + (list (make-test-mtch (make-bindings (list (make-bind 'nesting-names 'b))) 'b 'none))) + (test-xab 'nesting-names + '(a b) + (list (make-test-mtch (make-bindings (list (make-bind 'nesting-names '(a b)))) '(a b) 'none))) + (test-xab 'nesting-names + '(a (a b)) + (list (make-test-mtch (make-bindings (list (make-bind 'nesting-names '(a (a b))))) '(a (a b)) 'none))) + (test-xab '((name x a) nesting-names) + '(a (a (a b))) + (list (make-test-mtch (make-bindings (list (make-bind 'x 'a) + (make-bind 'nesting-names '(a (a b))))) + '(a (a (a b))) 'none))) + (test-xab 'nesting-names + '(a (a (a (a b)))) + (list (make-test-mtch (make-bindings (list (make-bind 'nesting-names '(a (a (a (a b))))))) + '(a (a (a (a b)))) 'none))) + + (test-xab 'same-in-nt + '(x x) + (list (make-test-mtch (make-bindings (list (make-bind 'same-in-nt '(x x)))) '(x x) 'none))) + (test-xab 'same-in-nt + '(x y) + #f) + + ; We don't have cross yet + + ; (test-xab '(in-hole (cross forever-list) 1) + ; '(a b c) + ; #f) + ; + ; (test-xab '(in-hole (cross forever-list) 1) + ; '(1 x x) + ; (list (make-test-mtch (make-bindings '()) '(1 x x) 'none))) + ; + ; (test-xab '(in-hole (cross forever-list) 1) + ; '(x 1 x) + ; (list (make-test-mtch (make-bindings '()) '(x 1 x) 'none))) + ; + ; + ; (test-xab '(in-hole (cross simple) g) + ; 'g + ; (list (make-mtch (make-bindings (list)) 'g 'none))) + + (test-xab 'var '+ #f) + (test-xab 'var 'anunusedvariable (list (make-mtch (make-bindings (list (make-bind 'var 'anunusedvariable))) 'anunusedvariable 'none))) + (test-xab 'var 'exp (list (make-mtch (make-bindings (list (make-bind 'var 'exp))) 'exp 'none))) + (test-xab 'var 'exp_x (list (make-mtch (make-bindings (list (make-bind 'var 'exp_x))) 'exp_x 'none))) + + (test-xab 'underscore '(+ 1 2) (list (make-mtch (make-bindings (list (make-bind 'underscore '(+ 1 2)))) '(+ 1 2) 'none))) + (test-xab 'underscore '2 (list (make-mtch (make-bindings (list (make-bind 'underscore 2))) 2 'none))) + +; ; simple boolean language +; (define bool +; '(define-language bool +; (B true +; false +; (and B B) +; (or B B)) +; (C (and C B) +; (or C B) +; hole)) +; +; (define bool-rr +; '(reduction-relation bool +; (--> (in-hole C (and false B)) +; (in-hole C false) +; ) +; (--> (in-hole C (and true B)) +; (in-hole C B) +; ) +; (--> (in-hole C (or false B)) +; (in-hole C B)) +; (--> (in-hole C (or true B)) +; (in-hole C true)) +; )) +; +; ; metafunction-less λv language: +; +; ; define-language +; (define λv '(define-language λv +; (e (e e ...) (if0 e e e) x v) +; (v (λ (x ...) e) number * +) +; (E (v ... E e ...) (if0 E e e) hole) +; (x (variable-except if0 λ * +)))) +; +; ; converted metafunctions +; (define subst-vars-rr +; '(reduction-relation +; λv +; (--> ((x_1 any_1) x_1) +; any_1) +; (--> ((x_1 any_1) (any_2 ...)) +; ,(map subst-vars (term (((x_1 any_1) any_2) ...))) ) +; (--> (side-condition +; ((x_1 any_1) any_2) +; (and (not (list? any_2)) +; (not (eq? (term x_1) (term any_2))))) +; any_2) +; (--> ((x_1 any_1) (x_2 any_2) (x_3 any_3) ... any_4) +; ,(subst-vars (term ((x_1 any_1) ,(subst-vars (term ((x_2 any_2) (x_3 any_3) ... any_4))))))) +; (--> (any) +; any))) +; +; (define subst-rr +; '(reduction-relation +; λv +; (--> (x_1 any_1 (λ (x_2 ... x_1 x_3 ...) any_2)) +; (λ (x_2 ... x_1 x_3 ...) any_2)) +; (--> (side-condition +; (x_1 any_1 (λ (x_2 ...) any_2)) +; (not (memq (term x_1) (term (x_2 ...))))) +; ,(term-let ([(x_new ...) (variables-not-in (term (x_1 any_1 any_2)) (term (x_2 ...)))]) +; (term +; (λ (x_new ...) ,(subst (term (x_1 any_1 ,(subst-vars (term ((x_2 x_new) ... any_2))))) )))) ) +; (--> (x_1 any_1 x_1) +; any_1) +; (--> (side-condition +; (x_1 any_1 x_2) +; (not (eq? (term x_1) (term x_2)))) +; x_2) +; (--> (x any (e_1 e_2 ...)) +; (,(subst (term (x any e_1))) ,@(map subst (term ((x any e_2) ...)))) ) +; (--> (x any (if0 e_1 e_2 e_3)) +; (if0 ,(subst (term (x any e_1))) ,(subst (term (x any e_2))) ,(subst (term (x any e_3))))) +; (--> (x any number) +; number) +; (--> (x any +) +; +) +; (--> (x any *) +; *))) +; +; (define subst-n-rr '(reduction-relation +; λv +; (--> ((x_1 any_1) (x_2 any_2) ... any_3) +; ,(subst (term (x_1 any_1 ,(subst-n (term ((x_2 any_2) ... any_3))))))) +; (--> (any_3) +; any_3))) +; +; ; reduction-relation +; (define λv-rr '(reduction-relation +; λv +; (--> (in-hole E (* number_1 number_2)) +; (in-hole E ,(* (term number_1) (term number_2)))) +; (--> (in-hole E (+ number_1 number_2)) +; (in-hole E ,(+ (term number_1) (term number_2)))) +; (--> (in-hole E (if0 0 e_1 e_2)) +; (in-hole E e_1)) +; (--> (in-hole E (if0 (side-condition number_1 (not (zero? (term number_1)))) e_1 e_2)) +; (in-hole E e_2)) +; (--> (in-hole E (side-condition ((λ (x ...) e) v ...) +; (= (length (term (x ...))) +; (length (term (v ...)))))) +; (in-hole E ,(subst-n (term ((x v) ... e))))))) + ) + (test) \ No newline at end of file diff --git a/collects/redex/tests/matcher-test.rkt b/collects/redex/tests/matcher-test.rkt index 3e4eeac33f..8e58fc8450 100644 --- a/collects/redex/tests/matcher-test.rkt +++ b/collects/redex/tests/matcher-test.rkt @@ -302,6 +302,10 @@ (test-empty '(a ... b) '(b c) #f) (test-empty '(a ... b) '(a b c) #f) + (test-lang '(n n ...) '((1 1) 1 1) (list (make-mtch (make-bindings (list (make-bind 'n '(1 1)))) '((1 1) 1 1) none)) + (list (make-nt 'n (list (make-rhs 'any) (make-rhs 'number))))) + (test-lang '(n (n ...)) '((1 1) (1 1)) (list (make-mtch (make-bindings (list (make-bind 'n '(1 1)))) '((1 1) (1 1)) none)) + (list (make-nt 'n (list (make-rhs 'any) (make-rhs 'number))))) (test-empty '((name x any) ((name x number) ...)) '((1 1) (1 1))