From fae02be9f06aefd55c65211d2e95a07041ebfede Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Wed, 8 Sep 2010 11:32:04 -0400 Subject: [PATCH 1/9] Add memory fns. --- collects/typed-scheme/private/base-env.rkt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/collects/typed-scheme/private/base-env.rkt b/collects/typed-scheme/private/base-env.rkt index bf36ecc594..dfa1362233 100644 --- a/collects/typed-scheme/private/base-env.rkt +++ b/collects/typed-scheme/private/base-env.rkt @@ -640,6 +640,8 @@ [exit (-> (Un))] [collect-garbage (-> -Void)] +[current-memory-use (-> -Nat)] +[dump-memory-stats (-> Univ)] [module->namespace (-> (-mu x (-lst (Un -Symbol -String -Nat x (-val #f)))) -Namespace)] [current-namespace (-Param -Namespace -Namespace)] From cfc289d806a4a71e34df8dc8b98b5024b66a4cff Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Wed, 8 Sep 2010 11:37:02 -0400 Subject: [PATCH 2/9] simplify --- collects/typed-scheme/utils/tc-utils.rkt | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/collects/typed-scheme/utils/tc-utils.rkt b/collects/typed-scheme/utils/tc-utils.rkt index 7ce94208f4..84cf64410c 100644 --- a/collects/typed-scheme/utils/tc-utils.rkt +++ b/collects/typed-scheme/utils/tc-utils.rkt @@ -6,10 +6,8 @@ don't depend on any other portion of the system |# (provide (all-defined-out)) -(require "syntax-traversal.rkt" - "utils.rkt" racket/dict - syntax/parse (for-syntax scheme/base syntax/parse) scheme/match unstable/debug - (for-syntax unstable/syntax)) +(require "syntax-traversal.rkt" racket/dict + syntax/parse (for-syntax scheme/base syntax/parse) scheme/match) ;; a parameter representing the original location of the syntax being currently checked (define current-orig-stx (make-parameter #'here)) @@ -138,13 +136,12 @@ don't depend on any other portion of the system ;; raise an internal error - typechecker bug! (define (int-err msg . args) - (parameterize ([custom-printer #t]) - (raise (make-exn:fail:tc (string-append "Internal Typechecker Error: " - (apply format msg args) - (format "\nwhile typechecking\n~aoriginally\n~a" - (syntax->datum (current-orig-stx)) - (syntax->datum (locate-stx (current-orig-stx))))) - (current-continuation-marks))))) + (raise (make-exn:fail:tc (string-append "Internal Typechecker Error: " + (apply format msg args) + (format "\nwhile typechecking\n~aoriginally\n~a" + (syntax->datum (current-orig-stx)) + (syntax->datum (locate-stx (current-orig-stx))))) + (current-continuation-marks)))) (define-syntax (nyi stx) (syntax-case stx () From 120a1d0d87824f90b153047cc3a5408a60753b65 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Wed, 8 Sep 2010 11:38:28 -0400 Subject: [PATCH 3/9] Load typechecker dynamically to reduce footprint. --- collects/typed-scheme/core.rkt | 69 +++++++ collects/typed-scheme/private/with-types.rkt | 188 +++++++++--------- .../typed-scheme/typecheck/def-export.rkt | 12 +- collects/typed-scheme/typecheck/renamer.rkt | 9 + collects/typed-scheme/typed-scheme.rkt | 71 +------ 5 files changed, 185 insertions(+), 164 deletions(-) create mode 100644 collects/typed-scheme/core.rkt create mode 100644 collects/typed-scheme/typecheck/renamer.rkt diff --git a/collects/typed-scheme/core.rkt b/collects/typed-scheme/core.rkt new file mode 100644 index 0000000000..04ac187929 --- /dev/null +++ b/collects/typed-scheme/core.rkt @@ -0,0 +1,69 @@ +#lang racket/base + +(require (rename-in "utils/utils.rkt" [infer r:infer]) + (for-syntax racket/base) + (for-template racket/base) + (private with-types type-contract) + (except-in syntax/parse id) + racket/match unstable/syntax unstable/match + (optimizer optimizer) + (types utils convenience) + (typecheck typechecker provide-handling tc-toplevel) + (env type-name-env type-alias-env) + (r:infer infer) + (rep type-rep) + (except-in (utils utils tc-utils) infer) + (only-in (r:infer infer-dummy) infer-param) + "tc-setup.rkt") + +(provide mb-core ti-core wt-core) + +(define (mb-core stx) + (syntax-parse stx + [(mb (~optional (~and #:optimize (~bind [opt? #'#t]))) forms ...) + (let ([pmb-form (syntax/loc stx (#%plain-module-begin forms ...))]) + (parameterize ([optimize? (or (optimize?) (attribute opt?))]) + (tc-setup + stx pmb-form 'module-begin new-mod tc-module after-code + (with-syntax* + (;; pmb = #%plain-module-begin + [(pmb . body2) new-mod] + ;; add in syntax property on useless expression to draw check-syntax arrows + [check-syntax-help (syntax-property #'(void) 'disappeared-use (type-name-references))] + ;; perform the provide transformation from [Culpepper 07] + [transformed-body (remove-provides #'body2)] + ;; add the real definitions of contracts on requires + [transformed-body (change-contract-fixups #'transformed-body)] + ;; potentially optimize the code based on the type information + [(optimized-body ...) + ;; do we optimize? + (if (optimize?) + (begin0 (map optimize-top (syntax->list #'transformed-body)) + (do-time "Optimized")) + #'transformed-body)]) + ;; reconstruct the module with the extra code + ;; use the regular %#module-begin from `racket/base' for top-level printing + #`(#%module-begin optimized-body ... #,after-code check-syntax-help)))))])) + +(define (ti-core stx) + (syntax-parse stx + [(_ . ((~datum module) . rest)) + #'(module . rest)] + [(_ . form) + (tc-setup + stx #'form 'top-level body2 tc-toplevel-form type + (syntax-parse body2 + ;; any of these do not produce an expression to be printed + [(head:invis-kw . _) body2] + [_ (let ([ty-str (match type + ;; don't print results of type void + [(tc-result1: (== -Void type-equal?)) #f] + [(tc-result1: t f o) + (format "- : ~a\n" t)] + [(tc-results: t) + (format "- : ~a\n" (cons 'Values t))] + [x (int-err "bad type result: ~a" x)])]) + (if ty-str + #`(let ([type '#,ty-str]) + (begin0 #,body2 (display type))) + body2))]))])) \ No newline at end of file diff --git a/collects/typed-scheme/private/with-types.rkt b/collects/typed-scheme/private/with-types.rkt index 601bdb38ee..a3eb62dc4e 100644 --- a/collects/typed-scheme/private/with-types.rkt +++ b/collects/typed-scheme/private/with-types.rkt @@ -1,11 +1,14 @@ #lang racket/base -(require racket/require racket/contract/regions racket/contract/base +(require racket/require + (for-template + (except-in racket/base for for*) + "prims.rkt" + (prefix-in c: (combine-in racket/contract/regions racket/contract/base))) "base-env.rkt" "base-special-env.rkt" "base-env-numeric.rkt" "base-env-indexing.rkt" "extra-procs.rkt" "prims.rkt" - (for-syntax - scheme/base syntax/parse racket/block racket/match - unstable/sequence unstable/debug "base-types-extra.rkt" + syntax/parse racket/block racket/match + unstable/sequence unstable/debug "base-types-extra.rkt" (except-in (path-up "env/type-name-env.rkt" "env/type-alias-env.rkt" "infer/infer-dummy.rkt" @@ -21,98 +24,97 @@ "types/convenience.rkt" "types/abbrev.rkt") ->) - (except-in (path-up "utils/utils.rkt") infer))) + (except-in (path-up "utils/utils.rkt") infer)) -(provide with-type) +(provide wt-core) -(define-for-syntax (with-type-helper stx body fvids fvtys exids extys resty expr? ctx) - (block - (define old-context (unbox typed-context?)) - (define ((no-contract t [stx stx])) - (tc-error/stx stx "Type ~a could not be converted to a contract." t)) - (set-box! typed-context? #t) - (define fv-types (for/list ([t (in-list (syntax->list fvtys))]) - (parse-type t))) - (define fv-cnts (for/list ([t (in-list fv-types)] - [stx (in-list (syntax->list fvtys))]) - (type->contract t #:typed-side #f (no-contract t)))) - (define ex-types (for/list ([t (syntax->list extys)]) - (parse-type t))) - (define ex-cnts (for/list ([t (in-list ex-types)] - [stx (in-list (syntax->list extys))]) - (type->contract t #:typed-side #t (no-contract t)))) - (define region-tc-result - (and expr? (parse-tc-results resty))) - (define region-cnts - (if region-tc-result - (match region-tc-result - [(tc-result1: t) - (list (type->contract t #:typed-side #t (no-contract t #'region-ty-stx)))] - [(tc-results: ts) - (for/list ([t (in-list ts)]) - (type->contract - t #:typed-side #t - (no-contract t #'region-ty-stx)))]) - null)) - (for ([i (in-list (syntax->list fvids))] - [ty (in-list fv-types)]) - (register-type i ty)) - (define expanded-body - (if expr? - (with-syntax ([body body]) - (local-expand #'(let () . body) ctx null)) - (with-syntax ([(body ...) body] - [(id ...) exids] - [(ty ...) extys]) - (local-expand #'(let () (begin (: id ty) ... body ... (values id ...))) ctx null)))) - (parameterize (;; disable fancy printing? - [custom-printer #t] - ;; a cheat to avoid units - [infer-param infer] - ;; do we report multiple errors - [delay-errors? #t] - ;; this parameter is just for printing types - ;; this is a parameter to avoid dependency issues - [current-type-names - (lambda () - (append - (type-name-env-map (lambda (id ty) - (cons (syntax-e id) ty))) - (type-alias-env-map (lambda (id ty) - (cons (syntax-e id) ty)))))] - ;; reinitialize seen type variables - [type-name-references null] - ;; for error reporting - [orig-module-stx stx] - [expanded-module-stx expanded-body]) - (tc-expr/check expanded-body (if expr? region-tc-result (ret ex-types)))) - (report-all-errors) - (set-box! typed-context? old-context) - ;; then clear the new entries from the env ht - (for ([i (in-list (syntax->list fvids))]) - (unregister-type i)) - (with-syntax ([(fv.id ...) fvids] - [(cnt ...) fv-cnts] - [(ex-id ...) exids] - [(ex-cnt ...) ex-cnts] - [(region-cnt ...) region-cnts] - [body expanded-body] - [check-syntax-help (syntax-property #'(void) 'disappeared-use (type-name-references))]) - (if expr? - (quasisyntax/loc stx - (begin check-syntax-help - (with-contract typed-region - #:results (region-cnt ...) - #:freevars ([fv.id cnt] ...) - body))) - (syntax/loc stx - (begin - (define-values () (begin check-syntax-help (values))) - (with-contract typed-region - ([ex-id ex-cnt] ...) - (define-values (ex-id ...) body)))))))) +(define (with-type-helper stx body fvids fvtys exids extys resty expr? ctx) + (define old-context (unbox typed-context?)) + (define ((no-contract t [stx stx])) + (tc-error/stx stx "Type ~a could not be converted to a contract." t)) + (set-box! typed-context? #t) + (define fv-types (for/list ([t (in-list (syntax->list fvtys))]) + (parse-type t))) + (define fv-cnts (for/list ([t (in-list fv-types)] + [stx (in-list (syntax->list fvtys))]) + (type->contract t #:typed-side #f (no-contract t)))) + (define ex-types (for/list ([t (syntax->list extys)]) + (parse-type t))) + (define ex-cnts (for/list ([t (in-list ex-types)] + [stx (in-list (syntax->list extys))]) + (type->contract t #:typed-side #t (no-contract t)))) + (define region-tc-result + (and expr? (parse-tc-results resty))) + (define region-cnts + (if region-tc-result + (match region-tc-result + [(tc-result1: t) + (list (type->contract t #:typed-side #t (no-contract t #'region-ty-stx)))] + [(tc-results: ts) + (for/list ([t (in-list ts)]) + (type->contract + t #:typed-side #t + (no-contract t #'region-ty-stx)))]) + null)) + (for ([i (in-list (syntax->list fvids))] + [ty (in-list fv-types)]) + (register-type i ty)) + (define expanded-body + (if expr? + (with-syntax ([body body]) + (local-expand #'(let () . body) ctx null)) + (with-syntax ([(body ...) body] + [(id ...) exids] + [(ty ...) extys]) + (local-expand #'(let () (begin (: id ty) ... body ... (values id ...))) ctx null)))) + (parameterize (;; disable fancy printing? + [custom-printer #t] + ;; a cheat to avoid units + [infer-param infer] + ;; do we report multiple errors + [delay-errors? #t] + ;; this parameter is just for printing types + ;; this is a parameter to avoid dependency issues + [current-type-names + (lambda () + (append + (type-name-env-map (lambda (id ty) + (cons (syntax-e id) ty))) + (type-alias-env-map (lambda (id ty) + (cons (syntax-e id) ty)))))] + ;; reinitialize seen type variables + [type-name-references null] + ;; for error reporting + [orig-module-stx stx] + [expanded-module-stx expanded-body]) + (tc-expr/check expanded-body (if expr? region-tc-result (ret ex-types)))) + (report-all-errors) + (set-box! typed-context? old-context) + ;; then clear the new entries from the env ht + (for ([i (in-list (syntax->list fvids))]) + (unregister-type i)) + (with-syntax ([(fv.id ...) fvids] + [(cnt ...) fv-cnts] + [(ex-id ...) exids] + [(ex-cnt ...) ex-cnts] + [(region-cnt ...) region-cnts] + [body expanded-body] + [check-syntax-help (syntax-property #'(void) 'disappeared-use (type-name-references))]) + (if expr? + (quasisyntax/loc stx + (begin check-syntax-help + (c:with-contract typed-region + #:results (region-cnt ...) + #:freevars ([fv.id cnt] ...) + body))) + (syntax/loc stx + (begin + (define-values () (begin check-syntax-help (values))) + (c:with-contract typed-region + ([ex-id ex-cnt] ...) + (define-values (ex-id ...) body))))))) -(define-syntax (with-type stx) +(define (wt-core stx) (define-syntax-class typed-id #:description "[id type]" [pattern (id ty)]) diff --git a/collects/typed-scheme/typecheck/def-export.rkt b/collects/typed-scheme/typecheck/def-export.rkt index acf624d6a2..16b7082302 100644 --- a/collects/typed-scheme/typecheck/def-export.rkt +++ b/collects/typed-scheme/typecheck/def-export.rkt @@ -1,16 +1,10 @@ #lang racket/base -(require racket/require - (for-syntax syntax/parse racket/base - (path-up "utils/tc-utils.rkt" "private/typed-renaming.rkt" "env/type-name-env.rkt"))) +(require racket/require (for-template "renamer.rkt") "renamer.rkt" + (for-syntax syntax/parse racket/base "renamer.rkt" + (path-up "utils/tc-utils.rkt" "env/type-name-env.rkt"))) (provide def-export) - -(define-for-syntax (renamer id #:alt [alt #f]) - (if alt - (make-typed-renaming (syntax-property id 'not-free-identifier=? #t) alt) - (make-rename-transformer (syntax-property id 'not-free-identifier=? #t)))) - (define-syntax (def-export stx) (syntax-parse stx [(def-export export-id:identifier id:identifier cnt-id:identifier) diff --git a/collects/typed-scheme/typecheck/renamer.rkt b/collects/typed-scheme/typecheck/renamer.rkt new file mode 100644 index 0000000000..a1f19cff32 --- /dev/null +++ b/collects/typed-scheme/typecheck/renamer.rkt @@ -0,0 +1,9 @@ +#lang racket/base + +(require "../private/typed-renaming.rkt") +(provide renamer) + +(define (renamer id #:alt [alt #f]) + (if alt + (make-typed-renaming (syntax-property id 'not-free-identifier=? #t) alt) + (make-rename-transformer (syntax-property id 'not-free-identifier=? #t)))) \ No newline at end of file diff --git a/collects/typed-scheme/typed-scheme.rkt b/collects/typed-scheme/typed-scheme.rkt index 6063fdfa91..88f1e416a4 100644 --- a/collects/typed-scheme/typed-scheme.rkt +++ b/collects/typed-scheme/typed-scheme.rkt @@ -1,21 +1,6 @@ #lang racket/base -(require (rename-in "utils/utils.rkt" [infer r:infer]) - (private with-types) - (for-syntax - (except-in syntax/parse id) - racket/match unstable/syntax racket/base unstable/match - (private type-contract) - (optimizer optimizer) - (types utils convenience) - (typecheck typechecker provide-handling tc-toplevel) - (env type-name-env type-alias-env) - (r:infer infer) - (utils tc-utils) - (rep type-rep) - (except-in (utils utils) infer) - (only-in (r:infer infer-dummy) infer-param) - "tc-setup.rkt")) +(require (for-syntax racket/base "typecheck/renamer.rkt")) (provide (rename-out [module-begin #%module-begin] [top-interaction #%top-interaction] @@ -25,54 +10,16 @@ with-type) (define-syntax (module-begin stx) - (syntax-parse stx - [(mb (~optional (~and #:optimize (~bind [opt? #'#t]))) forms ...) - (let ([pmb-form (syntax/loc stx (#%plain-module-begin forms ...))]) - (parameterize ([optimize? (or (optimize?) (attribute opt?))]) - (tc-setup - stx pmb-form 'module-begin new-mod tc-module after-code - (with-syntax* - (;; pmb = #%plain-module-begin - [(pmb . body2) new-mod] - ;; add in syntax property on useless expression to draw check-syntax arrows - [check-syntax-help (syntax-property #'(void) 'disappeared-use (type-name-references))] - ;; perform the provide transformation from [Culpepper 07] - [transformed-body (remove-provides #'body2)] - ;; add the real definitions of contracts on requires - [transformed-body (change-contract-fixups #'transformed-body)] - ;; potentially optimize the code based on the type information - [(optimized-body ...) - ;; do we optimize? - (if (optimize?) - (begin0 (map optimize-top (syntax->list #'transformed-body)) - (do-time "Optimized")) - #'transformed-body)]) - ;; reconstruct the module with the extra code - ;; use the regular %#module-begin from `racket/base' for top-level printing - #`(#%module-begin optimized-body ... #,after-code check-syntax-help)))))])) + (dynamic-require 'typed-scheme/private/base-env #f) + (dynamic-require 'typed-scheme/private/base-env-numeric #f) + (dynamic-require 'typed-scheme/private/base-env-indexing #f) + ((dynamic-require 'typed-scheme/core 'mb-core) stx)) (define-syntax (top-interaction stx) - (syntax-parse stx - [(_ . ((~datum module) . rest)) - #'(module . rest)] - [(_ . form) - (tc-setup - stx #'form 'top-level body2 tc-toplevel-form type - (syntax-parse body2 - ;; any of these do not produce an expression to be printed - [(head:invis-kw . _) body2] - [_ (let ([ty-str (match type - ;; don't print results of type void - [(tc-result1: (== -Void type-equal?)) #f] - [(tc-result1: t f o) - (format "- : ~a\n" t)] - [(tc-results: t) - (format "- : ~a\n" (cons 'Values t))] - [x (int-err "bad type result: ~a" x)])]) - (if ty-str - #`(let ([type '#,ty-str]) - (begin0 #,body2 (display type))) - body2))]))])) + ((dynamic-require 'typed-scheme/core 'ti-core) stx)) + +(define-syntax (with-type stx) + ((dynamic-require 'typed-scheme/core 'wt-core) stx)) From 837291a793bd9602af16404db1b4fc49e639021f Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Wed, 8 Sep 2010 11:38:59 -0400 Subject: [PATCH 4/9] simplify requires --- collects/typed-scheme/private/prims.rkt | 32 ++++++++++++------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/collects/typed-scheme/private/prims.rkt b/collects/typed-scheme/private/prims.rkt index 8abe9f8149..20573f352e 100644 --- a/collects/typed-scheme/private/prims.rkt +++ b/collects/typed-scheme/private/prims.rkt @@ -30,31 +30,31 @@ This file defines two sorts of primitives. All of them are provided into any mod (require "../utils/utils.rkt" racket/base mzlib/etc - (for-syntax + "../utils/require-contract.rkt" + "colon.rkt" + "../typecheck/internal-forms.rkt" + (rename-in racket/contract [-> c->]) + mzlib/struct + "base-types.rkt" + "base-types-extra.rkt" + (for-syntax syntax/parse syntax/private/util scheme/base - (rep type-rep) mzlib/match - "parse-type.rkt" "annotate-classes.rkt" + scheme/struct-info syntax/struct syntax/stx - scheme/struct-info - (private internal) - (except-in (utils utils tc-utils)) - (env type-name-env) + "../rep/type-rep.rkt" + "parse-type.rkt" + "annotate-classes.rkt" + "internal.rkt" + "../utils/utils.rkt" + "../utils/tc-utils.rkt" + "../env/type-name-env.rkt" "type-contract.rkt" "for-clauses.rkt")) -(require (utils require-contract) - "colon.rkt" - (typecheck internal-forms) - (except-in mzlib/contract ->) - (only-in mzlib/contract [-> c->]) - mzlib/struct - "base-types.rkt" - "base-types-extra.rkt") - (define-for-syntax (ignore stx) (syntax-property stx 'typechecker:ignore #t)) From f5482e57037d1959178bb56c75f8336c8ee31448 Mon Sep 17 00:00:00 2001 From: Steven Jaconette Date: Wed, 8 Sep 2010 10:15:21 -0500 Subject: [PATCH 5/9] Initial compiler model (includes low level pattern language model and redex to low level lanaguage compiler) --- collects/redex/private/compiler/match.rkt | 2782 +++++++++++++++++ .../redex/private/compiler/redextomatrix.rkt | 630 ++++ 2 files changed, 3412 insertions(+) create mode 100644 collects/redex/private/compiler/match.rkt create mode 100644 collects/redex/private/compiler/redextomatrix.rkt diff --git a/collects/redex/private/compiler/match.rkt b/collects/redex/private/compiler/match.rkt new file mode 100644 index 0000000000..e74fdf431e --- /dev/null +++ b/collects/redex/private/compiler/match.rkt @@ -0,0 +1,2782 @@ +#lang scheme +(require redex) +(require racket/set) +(provide red detect-hole detect-hole2 hole-table Get-Free-Name-Patterns + Build-Term-Let + Build-Cond + Cond-List + simplify + simple-swap) + +(define hole-table (make-hash)) + +(define the-hole (term hole)) + +(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 + list + andmap + no-match + cons? + number? + natural? + integer? + real? + string? + symbol? + context-match + or + set-union + set + set-from-list + set-map + curry + pair-path-append + path-append + ; we don't have these functions yet + variable-except? + variable-prefix? + ; + () + begin + ∪ + singleton + eqv? + set-empty? + ∅ + else + car + cdr + number + string + bool + cons + x + 'variable + 'any + variable-not-otherwise-mentioned + not + = + '() + ; ambiguous + term-let + ] + [bool #t + #f] + [Context + (cond [v v] ... + [v Context] + [v e] ...) + (cond [v v] ... + [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)] + [row ((p ... -> r) eqs ...)] + [eqs (pvar bool eq ...)] + [elip ,'...] + [eq id + (= pvar) + (car eq) + (cdr eq) + (cons eq eq) + (plug eq eq) + lit-hole] + (p (or p p) + lit-hole + (lit-in-hole p_1 p_2) + (lit-hide-hole p) + (lit-name variable p) + (lit-side-condition p any) + (nt id) + rep + scw) + (s lit-number + lit-natural + lit-integer + lit-real + lit-string + lit-variable + (lit-variable-except id ...) + (lit-variable-prefix id) + ) + (scw s + cw) + (cw c + wildcard) + (wildcard wc) + (c number + string + 'variable + '() + cp + #t + #f + ; no longer thought of as a constructor, at least for now... + ;(nt id) + ;lit-variable-not-otherwise-mentioned + ;context-match + ) + (cp (cons p p)) + (rep (repeat p rep) + (repeat p cp) + (repeat p '())) + ;(pvar (variable-prefix 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) + (cdr x) + (cons x x) + pvar) + (r any + (car any) + (cdr any)) + ((op replace) any)) + +(define red + (reduction-relation + L + + ; Top-Row-All-Wildcard + ; If the top row is all wildcard patterns, we're not inside a repeat, or in the non-terminal set mode, + ; replace the top row with a singleton of it's rhs, and union this with the matrix built from the remaining rows. + + (--> (in-hole Context (matrix (x_1 ...) + (((wildcard ... -> r_1) eqs_1 ...) + ((p_1 ... -> r_2) eqs_2 ...) + ...) + (pvar ...) + (pvar_3 ...) + 0 + bool)) + (in-hole Context + (begin (Build-Term-Let (eqs_1 ...) ;(set! results (cons + r_1 + ;results)) + ) + (matrix (x_1 ...) + (((p_1 ... -> r_2) eqs_2 ...) + ...) + (pvar ...) + (pvar_3 ...) + 0 + bool) + ) + ) + (side-condition (eqv? (length (term (x_1 ...))) (length (term (wildcard ...))))) + Top-Row-All-Wildcard) + + ; Top-Row-All-Wildcard in repeat + ; This is to support our hack of using the repeat matching function as a rhs to a matrix when matching repeats. + ; When we see a one rowed matrix, where the top row is all wildcards, replace with the rhs. + + (--> (in-hole Context (matrix (x_1 ...) + (((wildcard ... -> r_1) eqs_1 ...)) + (pvar ...) + (pvar_3 ...) + natural + bool)) + (in-hole Context r_1) + (side-condition (eqv? (length (term (x_1 ...))) (length (term (wildcard ...))))) + (side-condition (> (term natural) 0)) + Top-Row-All-Wildcard-in-repeat) + + ; Empty-Rows + ; Transform matrices with no rows into ∅. + + (--> (in-hole Context (matrix (x ...) + () + (pvar ...) + (pvar_3 ...) + natural + bool)) + (in-hole Context ∅) + Empty-Rows) + + ; Empty Variables + ; Transform matrices with no input variables into ∅. + (--> (in-hole Context (matrix () + (((p_1 p_2 ... -> r_1) eqs_1 ...) + ((p_3 p_4 ... -> r_2) eqs_2 ...) + ...) + (pvar ...) + (pvar_3 ...) + natural + bool)) + (in-hole Context ∅) + Empty-Variables) + + ; Drop-Front-Column-All-Wildcard + + (--> (in-hole Context + (matrix (x_1 x_2 ...) + (((wc p_2 ... -> r_1) eqs_1 ...) + ((wc p_4 ... -> r_2) eqs_2 ...) + ...) + (pvar ...) + (pvar_3 ...) + natural + bool)) + (in-hole Context + (matrix (x_2 ...) + (((p_2 ... -> r_1) eqs_1 ...) + ((p_4 ... -> r_2) eqs_2 ...) + ...) + (pvar ...) + (pvar_3 ...) + natural + bool)) + (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. + + (--> (in-hole Context + (matrix (x_1 ...) + (((p_1 p_2 ... -> r_1) eqs_1 ...) + ... + (((or p_3 p_4) p_5 ... -> r_2) eqs_2 ...) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...) + (pvar ...) + (pvar_3 ...) + natural + bool)) + (in-hole Context + (matrix (x_1 ...) + (((p_1 p_2 ... -> r_1) eqs_1 ...) + ... + ((p_3 p_5 ... -> r_2) eqs_2 ...) + ((p_4 p_5 ... -> r_2) eqs_2 ...) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...) + (pvar ...) + (pvar_3 ...) + natural + bool)) + (side-condition (andmap not-an-or? (term (p_1 ...)))) + Unroll-Or) + + ; binding-name + ; If the first pattern of a row in the matrix has is a name pattern where the id is not yet marked as bound, + ; and we're not inside a repeat, then mark the id as bound, replace the name with the pattern contained in it, + ; wrap the row in a let which binds the id to the current input variable, and union the result of the let with the matrix formed by the remaining rows. + + (--> (in-hole Context + (matrix (x_1 x_2 ...) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + (((lit-name pvar_1 p_3) p_5 ... -> r_2) (pvar_4 bool_4 eq_4 ...) ... (pvar_1 bool_1 eq_1 ...) (pvar_5 bool_5 eq_5 ...) ...) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...) + (pvar_2 ...) + (pvar_3 ...) + 0 + bool)) + (in-hole Context + (matrix (x_1 x_2 ...) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + ((p_3 p_5 ... -> r_2) (pvar_4 bool_4 eq_4 ...) ... (pvar_1 bool_1 ,@(remove-duplicates (term (x_1 eq_1 ...)))) (pvar_5 bool_5 eq_5 ...) ...) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...) + (pvar_2 ...) + (pvar_3 ...) + 0 + bool)) + binding-name) + + ; binding-name-repeat + ; If inside a repeat, there is a 1 row matrix with a name pattern in its front column, where the variable is not marked as bound in either place in the matrix, + ; replace the name with the pattern it matches, wrap the matrix inside a let which binds the id to the current input variable, + ; and mark the variable as bound in only the list of repeat variables. + + (--> (in-hole Context + (matrix (x_1 x_2 ...) + ((((lit-name pvar_1 p_3) p_5 ... -> r_2) eqs_1 ...)) + (pvar_2 ...) + (pvar_3 ...) + natural + bool)) + (in-hole Context + (let ((pvar_1 x_1)) + (matrix (x_1 x_2 ...) + (((p_3 p_5 ... -> r_2) eqs_1 ...)) + (pvar_2 ...) + (pvar_1 pvar_3 ...) + natural + bool))) + ;(side-condition (not (member (term pvar_1) (term (pvar_2 ...))))) + (side-condition (not (member (term pvar_1) (map (λ (x) (term (Get-Pvar ,x))) (append (term (Binding-Eqs (eqs_1 ...))) (append (term (True-Eqs (eqs_1 ...) ())) (term (pvar_3 ...)))) )))) + (side-condition (> (term natural) 0)) + binding-name-repeat) + + ; bound-name-from-outside-repeat + ; If a one rowed matrix inside a repeat begins with a name pattern where the identifier is marked as bound outside the repeat, + ; wrap the matrix in an equality test between the car of the already-bound value, and the current input variable, + ; then continue matching starting with the p from inside the name pattern. + ; We take the car because we know that all variables bound inside repeats will bind to lists, + ; so an existing binding is equal one inside a repeat if each element of the bindings is equal. + + (--> (in-hole Context + (matrix (x_1 x_2 ...) + ((((lit-name pvar_1 p_3) p_5 ... -> r_2) eqs_1 ...)) + (pvar_2 ...) + (pvar_3 ...) + natural + bool)) + (in-hole Context + (cond [(equal? (car ,(term pvar_1)) x_1) + (matrix (x_1 x_2 ...) + (((p_3 p_5 ... -> r_2) eqs_1 ...)) + (pvar_2 ...) + (pvar_3 ...) + natural + bool)] + #;[else ∅] + )) + (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) + + ; bound-name-from-inside-repeat + ; If a one rowed matrix inside a repeat begins with a name pattern where the identifier is marked as bound inside the repeat, + ; wrap the matrix in an equality test between the already-bound value and the current input variable, then continue matching starting with the p from inside the name pattern. + + (--> (in-hole Context + (matrix (x_1 x_2 ...) + ((((lit-name pvar_1 p_3) p_5 ... -> r_2) eqs_1 ...)) + (pvar_2 ...) + (pvar_3 ...) + natural + bool)) + (in-hole Context + (cond [(equal? pvar_1 x_1) + (matrix (x_1 x_2 ...) + (((p_3 p_5 ... -> r_2) eqs_1 ...)) + (pvar_2 ...) + (pvar_3 ...) + natural + bool) + ] + #;[else ∅] + )) + (side-condition (> (term natural) 0)) + (side-condition (member (term pvar_1) (map (λ (x) (term (Get-Pvar ,x))) (term (pvar_3 ...))))) + bound-name-from-inside-repeat) + + ; non-terminal + ; If a row in a matrix starts with a non-terminal which does not potentially contain a hole, wrap the row with a conditional + ; which calls the function wicth matches the non-terminal using boolean operations instead of sets where possible. Union this with the matrix formed by the remaining rows. + + (--> (in-hole Context + (matrix (x_1 x_2 ...) + (((cw_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 + bool)) + (in-hole Context + (begin + (cond ((,(string->symbol (format "~s~s" (term id) '-bool)) x_1) + (matrix (x_2 ...) + (((p_* ... -> r_*) eqs_* ...) ...) + (pvar_2 ...) + (pvar_3 ...) + natural + bool) + ) + #;(else ∅) + ) + (matrix (x_1 x_2 ...) + (((p_** ... -> r_**) eqs_** ...) ...) + (pvar_2 ...) + (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 ...) + ... + (((nt id) p_5 ... -> r_2) eqs_2 ...) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...)))) + (where (((p_** ... -> r_**) eqs_** ...) ...) (diff-starting-pattern (nt id) (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...))) + 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. + + (--> (in-hole Context + (matrix (x_1 x_2 ...) + (((wildcard_1 p_2 ... -> r_1) eqs_1 ...) + ... + ((c_1 p_3 ... -> r_2) eqs_2 ...) + ((cw_2 p_4 ... -> r_3) eqs_3 ...) + ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool)) + (in-hole Context + (Build-Cond ((Cond-List (simplify (c_1 cw_2 ...))) + (matrix (x_1 x_2 ...) + (((wildcard_1 p_2 ... -> r_1) eqs_1 ...) + ... + ((c_1 p_3 ... -> r_2) eqs_2 ...) + ((cw_2 p_4 ... -> r_3) eqs_3 ...) + ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool) carx cdrx))) + (fresh carx) + (fresh cdrx) + Constructor) + + ; hole + ; If a row in the matrix contains a lit-hole in its first column, and the flag for non-terminal-set is #f, + ; 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. Union this with the matrix formed by the remaining rows. + + (--> (in-hole Context + (matrix (x_1 x_2 ...) + (((cw_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 + bool)) + (in-hole Context + (begin + (cond [(or (context-match) (eqv? x_1 the-hole)) + (matrix (x_2 ...) + (((p_* ... -> r_*) eqs_* ...) ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool)] + #;(else ∅) + ) + (matrix (x_1 x_2 ...) + (((p_** ... -> r_**) eqs_** ...) ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool) + )) + + (where (((p_* ... -> r_*) eqs_* ...) ...) (drop-first-p (same-starting-pattern + lit-hole + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + ((lit-hole p_5 ... -> r_2) eqs_2 ...) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...)))) + (where (((p_** ... -> r_**) eqs_** ...) ...) (diff-starting-pattern lit-hole + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...))) + 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. + + (--> (in-hole Context + (matrix (x_1 x_2 ...) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + (((lit-in-hole 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 + (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)) + (side-condition (not (eqv? 1 (term (detect-hole2 0 p_3))))) + + in-hole-wrong-number-of-holes) + + ; in-hole (not base case) + ; If a row in a matrix begins with a lit-in-hole, and the number of holes in the first pattern is 1, then return the same matrix, + ; but change the in-hole pattern so that the pieces of the first pattern that don't contain the hole are shifted to the outside of the in-hole. + + (--> (in-hole Context + (matrix (x_1 x_2 ...) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + (((lit-in-hole 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 + (matrix (x_1 x_2 ...) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + (((move-hole-op-inward lit-in-hole p_4 p_3) p_5 ... -> r_2) eqs_2 ...) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool)) + + (side-condition (eqv? 1 (term (detect-hole2 0 p_3)))) + (side-condition (not-a-lit-name? (term p_3))) + in-hole-move-hole-op) + + (--> (in-hole Context + (matrix (x_1 x_2 ...) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + (((lit-in-hole (lit-name pvar 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 + (matrix (x_1 x_2 ...) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + (((lit-in-hole ,(car (term any_*)) p_4) p_5 ... -> r_2) ,@(cadr (term any_*))) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool)) + (fresh pvar-car) + (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) + ; If a row in a matrix begins with lit-in-hole, where the only thing in the first position is a non-terminal with 1 hole in it, + ; then transform the row into an expression to parameterize a new context, get back the set of pairs which match the non-terminal, + ; then test the cdr of each pair against the second pattern, and finally continue matching the row. Union this with the matrix formed by the remaining rows. + + (--> (in-hole Context + (matrix (x_1 x_2 ...) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + (((lit-in-hole (nt id) 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 + (for + ((rt (parameterize ((context-match in-context)) + (in-list (,(string->symbol (format "~s~s" (term id) '-list)) x_1))))) + (let ((cdr-rt (cdr rt))) + (matrix (cdr-rt x_2 ...) + (((p_* ... -> r_*) eqs_* ...) ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool)) + ) + (matrix (x_1 x_2 ...) + (((p_** ... -> r_**) eqs_** ...) ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool) + ) + ) + (side-condition (eqv? 1 (term (detect-hole2 0 (nt id))))) + + (where (((p_* ... -> r_*) eqs_* ...) ...) (replace-first-p p_4 + (same-starting-pattern + (lit-in-hole (nt id) p_4) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + (((lit-in-hole (nt id) p_4) p_5 ... -> r_2) eqs_2 ...) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...)))) + (where (((p_** ... -> r_**) eqs_** ...) ...) (diff-starting-pattern (lit-in-hole (nt id) p_4) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...))) + (fresh rt) + (fresh cdr-rt) + in-hole) + + (--> (in-hole Context + (matrix (x_1 x_2 ...) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + (((lit-in-hole (lit-name pvar (nt id)) p_4) p_5 ... -> r_2) (pvar_7 bool_7 eq_7 ...) ... (pvar bool_1 eq_1 ...) (pvar_8 bool_8 eq_8 ...) ...) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool)) + (in-hole Context + (begin + (for + ((rt (parameterize ((context-match in-context)) + (in-list (,(string->symbol (format "~s~s" (term id) '-list)) x_1))))) + (let ((car-rt (car rt)) + (cdr-rt (cdr rt))) + (matrix (cdr-rt x_2 ...) + (((p_4 p_5 ... -> r_2) (pvar_7 bool_7 eq_7 ...) ... (pvar bool_1 car-rt eq_1 ...) (pvar_8 bool_8 eq_8 ...) ...)) + (pvar_1 ...) + (pvar_3 ...) + natural + bool)) + ) + (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) + ) + ) + (fresh rt) + (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) + ; If a row in a matrix starts with a lit-hide-hole, replace the lit-hide-hole with a hide-hole where the patterns not containing holes have been shifted to the outside. + + (--> (in-hole Context + (matrix (x_1 x_2 ...) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + (((lit-hide-hole p_3) p_5 ... -> r_2) eqs_2 ...) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool)) + (in-hole Context + (matrix (x_1 x_2 ...) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + (((move-hole-op-inward lit-hide-hole 'lit-hole p_3) p_5 ... -> r_2) eqs_2 ...) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool)) + + hide-hole-move-hole-op) + + ; hide-hole (base case) + ; If a row in a matrix starts with a lit-hide-hole where the pattern is a non-terminal containing at least one hole, + ; wrap the row in an expression to parameterize the context to no-context, then match the non-terminal and the rest of the row. + ; Union the result with the rows formed by the rest of the matrix. + + (--> (in-hole Context + (matrix (x_1 x_2 ...) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + (((lit-hide-hole (nt id)) p_5 ... -> r_2) eqs_2 ...) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool)) + (in-hole Context + (begin + (parameterize ((context-match no-context)) + (matrix (x_1 x_2 ...) + (((p_* ... -> r_*) eqs_* ...) ...) #;(((nt id) p_5 ... -> r_2)) + (pvar_1 ...) + (pvar_3 ...) + natural + bool)) + (matrix (x_1 x_2 ...) + (((p_** ... -> r_**) eqs_** ...) ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool) + ) + ) + (side-condition (not (eqv? 0 (term (detect-hole2 0 (nt id)))))) + + (where (((p_* ... -> r_*) eqs_* ...) ...) (replace-first-p (nt id) + (same-starting-pattern + (lit-hide-hole (nt id)) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + (((lit-hide-hole (nt id)) p_5 ... -> r_2) eqs_2 ...) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...)))) + (where (((p_** ... -> r_**) eqs_** ...) ...) + (diff-starting-pattern + (lit-hide-hole (nt id)) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...))) + hide-hole-nt) + + ; hide-hole (hole) + (--> (in-hole Context + (matrix (x_1 x_2 ...) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + (((lit-hide-hole lit-hole) p_5 ... -> r_2) eqs_2 ...) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool)) + (in-hole Context + (begin + (parameterize ((context-match no-context)) + (matrix (x_1 x_2 ...) + (((p_* ... -> r_*) eqs_* ...) ...) #;(((nt id) p_5 ... -> r_2)) + (pvar_1 ...) + (pvar_3 ...) + natural + bool)) + (matrix (x_1 x_2 ...) + (((p_** ... -> r_**) eqs_** ...) ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool) + ) + ) + + (where (((p_* ... -> r_*) eqs_* ...) ...) (replace-first-p lit-hole + (same-starting-pattern + (lit-hide-hole lit-hole) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + (((lit-hide-hole lit-hole) p_5 ... -> r_2) eqs_2 ...) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...)))) + (where (((p_** ... -> r_**) eqs_** ...) ...) + (diff-starting-pattern + (lit-hide-hole lit-hole) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...))) + hide-hole) + + ; side-condition + (--> (in-hole Context + (matrix (x_1 x_2 ...) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + (((lit-side-condition p_3 any) p_4 ... -> r_2) eqs_2 ...) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool)) + (in-hole Context + (matrix (x_1 x_2 ...) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + ((p_3 p_4 ... -> (if any r_2 ∅)) eqs_2 ...) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool)) + + side-condition) + + ; Repeat + ; If a row in a matrix starts with (repeat p_1 p_2), first determine all the identifiers for name patterns in p_1. Call the ones which are not marked as bound in the matrix variable_1 ..., and the ones which are marked as bound in the matrix variable_2 ... + ; Seperate the matrix into the row with the repeat and all other rows, unioning the result together. Wrap the repeat row in a let expression to bind all the elements of variable_2 ... to fresh temporary variables. Inside this define a letrec called match-repeach as a function which takes a fresh variable z, variable_1 ..., and variable_2 ... as its arguments. variable_1 ... will be used to build up the bindings from inside the repeat, while variable_2 ... will be unwrapped to check that values already bound outside of the repeat match those inside the repeat. + ; Inside the function, union the results of two conditionals. The first is the "base case," where every element of variable_2 ... is equal to the empty list, and therefore the variable bound outside the repeat are correct inside the repeat. In this case, we return a matrix where the first input variable is z, the first pattern in the row is p_2, and the rest of the input/row are the same as before. We mark variable_1 ... as bound. This matrix is wrapped in a let expression which restores the values bound outside the repeat back from their temporary forms. + ; The second conditional checks if z and variable_2 ... are all cons?. If they are, it stores all the values for variable_1 ... as temporaries, then matches (car z) against p_1, with the righthand side equal to a call to match repeat with (cdr z), the cons of variable_1 ... the temporary values for variable_1 ..., and the cdr of all the elements of variable 2. (The new bindings are built up by one layer, and the ones bound outside of the repeat are "unwrapped" by one layer). In this one row, one pattern matrix, the natural indicating the depth of the repeat is incremented. + ; Finally, in the body of the letrec, all the elements of variable_1 ... are bound to empty, and there is the call (match-repeat x_1 variable_1 ... variable_2 ...). + (--> (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 + (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) + ) + ) + (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 (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 carz) + (fresh ((binding_temp ...) + (pvar_11 ...))) + (fresh ((single_binding_temp ...) + (pvar_11 ...))) + (fresh ((bound_temp ...) + (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 + (matrix (x_1 x_2 ...) + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + ((s p_5 ... -> r_2) eqs_2 ...) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...) + (pvar_2 ...) + (pvar_3 ...) + natural + bool)) + (in-hole Context + (begin + (cond ((Func-Replace (eqv? s x_1)) + (matrix (x_2 ...) + (((p_* ... -> r_*) eqs_* ...) ...) + (pvar_2 ...) + (pvar_3 ...) + natural + bool)) + (else ∅)) + (matrix (x_1 x_2 ...) + (((p_** ... -> r_**) eqs_** ...) ...) + (pvar_2 ...) + (pvar_3 ...) + natural + bool))) + (where (((p_* ... -> r_*) eqs_* ...) ...) (drop-first-p (same-starting-pattern + s + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + ((s p_5 ... -> r_2) eqs_2 ...) + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...)))) + (where (((p_** ... -> r_**) eqs_** ...) ...) (diff-starting-pattern s + (((cw_1 p_2 ... -> r_1) eqs_1 ...) + ... + ((p_6 p_7 ... -> r_3) eqs_3 ...) + ...))) + + #;(side-condition (andmap not-a-lit-name? (term (p_6 ...)))) + built-in-non-terminals) + )) + +(define not-a-wildcard? + (let ([wildcard? (redex-match L wildcard)]) + (λ (x) (not (wildcard? x))))) + +(define not-an-or? + (let ([or? (redex-match L (or p_1 p_2))]) + (λ (x) (not (or? x))))) + +(define not-a-lit-name? + (let ([lit-name? (redex-match L (lit-name variable p))]) + (λ (x) (not (lit-name? x))))) + +(define not-a-pvar? + (let ([pvar? (redex-match L pvar)]) + (λ (x) (not (pvar? x))))) + +(define not-a-rep? + (let ([rep? (redex-match L rep)]) + (λ (x) (not (rep? x))))) + +(define not-a-side-condition? + (let ([sc? (redex-match L (lit-side-condition p any))]) + (λ (x) (not (sc? x))))) + +(define not-a-cp? + (let ([cp? (redex-match L cp)]) + (λ (x) (not (cp? x))))) + +(define not-a-nt? + (let ([nt? (redex-match L (nt id))]) + (λ (x) (not (nt? x))))) + +(define not-a-lit-hole? + (let ([lit-hole? (redex-match L lit-hole)]) + (λ (x) (not (lit-hole? x))))) + +(define not-a-s? + (let ([s? (redex-match L s)]) + (λ (x) (not (s? x))))) + +(define not-an-id? + (let ([id? (redex-match L id)]) + (λ (x) (not (id? x))))) + +(define not-an-in-hole? + (let ([in-hole? (redex-match L (lit-in-hole p_1 p_2))]) + (λ (x) (not (in-hole? x))))) + +(define is-a-wc? + (let ([wc? (redex-match L wildcard)]) + (λ (x) (not (not (wc? x)))))) + +(define natural? + (λ (x) (and + (integer? x) + (not (negative? x))))) + +(define-metafunction L + ((Get-Pvar id) id) + ((Get-Pvar (pvar elip)) (Get-Pvar pvar)) + ((Get-Pvar pvar 0) + pvar) + ((Get-Pvar (pvar elip) natural) + (Get-Pvar pvar ,(- (term natural) 1))) + ((Get-Pvar id natural) + id) + ) + +(define-metafunction L + [(Add-Repeat-Vars ((pvar bool eq ...) eqs_2 ...) (pvar_1 ... pvar_3 pvar_2 ...)) + (Add-Repeat-Vars (eqs_2 ... (pvar bool ,@(remove-duplicates (term (pvar_3 eq ...))))) (pvar_1 ... pvar_2 ...)) + (side-condition (equal? (term pvar_3) (term (Get-Pvar pvar)))) + ] + [(Add-Repeat-Vars (eqs_1 ... (pvar bool eq ...) eqs_2 ...) (pvar_3 pvar_1 ...)) + (Add-Repeat-Vars (eqs_1 ... eqs_2 ... (pvar bool ,@(remove-duplicates (term (pvar_3 eq ...))))) (pvar_1 ...)) + (side-condition (equal? (term pvar_3) (term (Get-Pvar pvar)))) + ] + [(Add-Repeat-Vars (eqs ...) (pvar_1 ...)) + (eqs ...)]) + +(define-metafunction L + [(True-Eqs ((pvar #t eq ...) eqs_2 ...) (pvar_1 ...)) + (True-Eqs (eqs_2 ...) (pvar pvar_1 ...))] + [(True-Eqs ((pvar #f eq ...) eqs_2 ...) (pvar_1 ...)) + (True-Eqs (eqs_2 ...) (pvar_1 ...))] + [(True-Eqs () (pvar_1 ...)) + (pvar_1 ...)] + ) + +(define-metafunction L + [(Binding-Eqs ((pvar bool eq ... id eq ...) eqs_2 ...)) + (pvar pvar_* ...) + (where (pvar_* ...) (Binding-Eqs (eqs_2 ...)))] + [(Binding-Eqs ((pvar bool eq ...) eqs_2 ...)) + (pvar_* ...) + (where (pvar_* ...) (Binding-Eqs (eqs_2 ...)))] + [(Binding-Eqs (eqs ...)) + ()]) + +(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 ...))))] + [(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 ...)))] + [(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 ...))))] + [(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 ...))))] + [(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 ...)))) + (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 ...))))] + [(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 ...)))] + [(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) + [(Build-Let-Empty natural (pvar_1 ...) any) + (let ((pvar_1 '()) + ...) + any)]) + +(define-metafunction L + [(Build-Let any ()) + any] + [(Build-Let any (pvar_1 ...)) + (let ((pvar_1 (rev pvar_1)) + ...) + any)]) + +(define-metafunction L + ((Build-Temp-Let 0 () () any) + any) + [(Build-Temp-Let 0 (pvar_1 ...) (any_2 ...) any) + (let ((pvar_1 any_2) + ...) + any)] + ((Build-Temp-Let natural any_1 any_2 any_3) + any_3) + ((Build-Temp-Let () () any) + any) + [(Build-Temp-Let (pvar_1 ...) (any_2 ...) any) + (let ((pvar_1 any_2) + ...) + 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) ...)]) + +(define-metafunction L + [(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)) + +(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)) + natural) + ((detect-hole natural (or p_1 p_2)) + ,(+ (max (term (detect-hole 0 p_1)) (term (detect-hole 0 p_2))) (term natural))) + ((detect-hole natural (cons p_1 p_2)) + ,(+ (+ (term (detect-hole 0 p_1)) (term (detect-hole 0 p_2))) (term natural))) + ((detect-hole natural (repeat p_1 p_2)) + ,(+ (term (detect-hole 0 p_2)) (term natural))) + ((detect-hole natural (lit-name pvar p)) + ,(+ (term (detect-hole 0 p)) (term natural))) + ((detect-hole natural any) + natural)) + +(define-metafunction L + ((detect-hole2 natural lit-hole) + ,(+ 1 (term natural))) + ((detect-hole2 natural (nt id)) + ,(hash-ref hole-table (term id))) + ((detect-hole2 natural (lit-in-hole p_1 p_2)) + ,(+ (term natural) (term (detect-hole2 0 p_2)))) + ((detect-hole2 natural (lit-hide-hole p_1)) + natural) + ((detect-hole2 natural (or p_1 p_2)) + ,(+ (max (term (detect-hole2 0 p_1)) (term (detect-hole2 0 p_2))) (term natural))) + ((detect-hole2 natural (cons p_1 p_2)) + ,(+ (+ (term (detect-hole2 0 p_1)) (term (detect-hole2 0 p_2))) (term natural))) + ((detect-hole2 natural (repeat p_1 p_2)) + ,(+ (term (detect-hole2 0 p_2)) (term natural))) + ((detect-hole2 natural (lit-name pvar p)) + ,(+ (term (detect-hole2 0 p)) (term natural))) + ((detect-hole2 natural any) + 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) +(define-metafunction L + ((move-hole-op-inward lit-in-hole replace lit-hole) + replace) + ((move-hole-op-inward lit-hide-hole replace lit-hole) + (lit-hide-hole lit-hole)) + ((move-hole-op-inward lit-in-hole replace (nt id)) + (lit-in-hole (nt id) replace) + (side-condition (eqv? 1 (term (detect-hole2 0 (nt id)))))) + ((move-hole-op-inward lit-hide-hole replace (nt id)) + (nt id) + (side-condition (eqv? 0 (term (detect-hole2 0 (nt id)))))) + ((move-hole-op-inward lit-hide-hole replace (nt id)) + (lit-hide-hole (nt id))) + ((move-hole-op-inward lit-hide-hole replace (lit-in-hole p_1 p_2)) + (lit-in-hole p_1 p_2)) + ; context inside of context + ((move-hole-op-inward lit-in-hole replace (lit-in-hole p_1 p_2)) + (lit-in-hole p_1 (lit-in-hole p_2 replace)) + (side-condition (eqv? 1 (term (detect-hole2 0 p_2))))) + ((move-hole-op-inward op replace (lit-hide-hole p)) + (lit-hide-hole p)) + ((move-hole-op-inward lit-in-hole replace (lit-name pvar p)) + (lit-in-hole (lit-name pvar p) replace) + (side-condition (eqv? 1 (term (detect-hole2 0 (lit-name pvar p)))))) + ((move-hole-op-inward lit-in-hole replace (lit-name pvar p)) + (lit-name pvar p) + (side-condition (eqv? 0 (term (detect-hole2 0 (lit-name pvar p)))))) + ((move-hole-op-inward lit-hide-hole replace (lit-name pvar p)) + (lit-name pvar (lit-hide-hole p))) + ((move-hole-op-inward op replace (or p_1 p_2)) + (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 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 ...))) + ((push-name-downward (lit-name pvar lit-hole) (eqs_1 ... (pvar bool eq_1 ...) eqs_2 ...) pvar_fresh1 pvar_fresh2) + (lit-hole (eqs_1 ... (pvar bool lit-hole eq_1 ...) eqs_2 ...))) + ((push-name-downward (lit-name pvar (lit-name pvar_2 p_1)) (eqs_1 ... (pvar bool eq_1 ...) eqs_2 ...) pvar_fresh1 pvar_fresh2) + ((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 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-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)] + ) + +(define-metafunction L + [(simplify (cp_1 p_2 ...)) + ((cons '() '()) p_* ...) + (where (p_* ...) (simplify (p_2 ...)))] + [(simplify (wc p_2 ...)) + (p_* ...) + (where (p_* ...) (simplify (p_2 ...)))] + [(simplify (p_1 p_2 ...)) + (p_1 p_* ...) + (where (p_* ...) (simplify (p_2 ...)))] + [(simplify ()) + ()] + ) + +; Remove wc and all but one cp from the list of cw +(define-metafunction L + Cond-List : (cw ...) -> (cw ...) + [(Cond-List ()) ()] + [(Cond-List (cw_1 ... cw_2 cw_3 ... cw_2 cw_4 ...)) + (cw_* ...) + (where (cw_* ...) (Cond-List (cw_1 ... cw_2 cw_3 ... cw_4 ...)))] + [(Cond-List (c_1 ... wc c_2 ...)) + (cw_* ...) + (where (cw_* ...) (Cond-List (c_1 ... c_2 ...)))] + [(Cond-List (cw_1 ... cp_1 cw_2 ... cp_2 cw_3 ...)) + (cw_* ...) + (where (cw_* ...) (Cond-List (cp_1 cw_1 ... cw_2 ... cw_3 ...))) + (side-condition (andmap not-a-cp? (term (cw_1 ...)))) + (side-condition (andmap not-a-cp? (term (cw_2 ...))))] + [(Cond-List (cw_1 cw_2 ... cp_1 cw_3 ...)) + (cw_* ...) + (where (cw_* ...) (Cond-List (cp_1 cw_1 cw_2 ... cw_3 ...)))] + [(Cond-List (cw ...)) (cw ...)]) + +; Build a cond expression given constructors and a matrix +(define-metafunction L + Build-Cond : ((cw ...) m x x) -> e + [(Build-Cond ((cp_1 cw_1 ...) + (matrix (x_1 x_2 ...) + (((cw_2 p_2 ... -> r_1) eqs_1 ...) + ... + ((c_1 p_3 ... -> r_2) eqs_2 ...) + ((cw_3 p_4 ... -> r_3) eqs_3 ...) + ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool) + x_3 + x_4)) + (clean-up (∪ (cond + [(cons? x_1) + (let ((x_3 (car x_1)) + (x_4 (cdr x_1))) + (matrix (x_4 x_3 x_2 ...) + (SL (((cw_2 p_2 ... -> r_1) eqs_1 ...) + ... + ((c_1 p_3 ... -> r_2) eqs_2 ...) + ((cw_3 p_4 ... -> r_3) eqs_3 ...) + ...)) + (pvar_1 ...) + (pvar_3 ...) + natural + bool) + ) + ] + [(Func-Replace (eqv? cw_1 x_1)) + (matrix (x_2 ...) + (S cw_1 (((cw_2 p_2 ... -> r_1) eqs_1 ...) + ... + ((c_1 p_3 ... -> r_2) eqs_2 ...) + ((cw_3 p_4 ... -> r_3) eqs_3 ...) + ...)) + (pvar_1 ...) + (pvar_3 ...) + natural + bool) + ] + ... + #;(else ∅) + ) + (matrix (x_2 ...) + (D (((cw_2 p_2 ... -> r_1) eqs_1 ...) + ... + ((c_1 p_3 ... -> r_2) eqs_2 ...) + ((cw_3 p_4 ... -> r_3) eqs_3 ...) + ...)) + (pvar_1 ...) + (pvar_3 ...) + natural + bool) + )) + ] + [(Build-Cond ((cw_1 ...) + (matrix (x_1 x_2 ...) + (((cw_2 p_2 ... -> r_1) eqs_1 ...) + ... + ((c_1 p_3 ... -> r_2) eqs_2 ...) + ((cw_3 p_4 ... -> r_3) eqs_3 ...) + ...) + (pvar_1 ...) + (pvar_3 ...) + natural + bool) + x_3 + x_4)) + (clean-up (∪ (cond + [(Func-Replace (eqv? cw_1 x_1)) + (matrix (x_2 ...) + (S cw_1 (((cw_2 p_2 ... -> r_1) eqs_1 ...) + ... + ((c_1 p_3 ... -> r_2) eqs_2 ...) + ((cw_3 p_4 ... -> r_3) eqs_3 ...) + ...)) + (pvar_1 ...) + (pvar_3 ...) + natural + bool) + ] + ... + #;(else ∅) + ) + (matrix (x_2 ...) + (D (((cw_2 p_2 ... -> r_1) eqs_1 ...) + ... + ((c_1 p_3 ... -> r_2) eqs_2 ...) + ((cw_3 p_4 ... -> r_3) eqs_3 ...) + ...)) + (pvar_1 ...) + (pvar_3 ...) + natural + bool) + )) + ] + ) + +; S metafunction from the paper, applied to cons patterns +(define-metafunction L + SL : (row ...) -> (row ...) + [(SL ()) ()] + [(SL ((((cons p_1 p_2) p_3 ... -> r_1) eqs_1 ...) ((p ... -> r) eqs_2 ...) ...)) + (((p_2 p_1 p_3 ... -> r_1) eqs_1 ...) + ((p_* ... -> r_*) eqs_* ...) + ...) + (where (((p_* ... -> r_*) eqs_* ...) ...) + (SL (((p ... -> r) eqs_2 ...) ...)))] + [(SL (((wc p_2 ... -> r_1) eqs_1 ...) ((p ... -> r) eqs_2 ...) ...)) + (;(wc wc p_2 ... -> r_1) + ((p_* ... -> r_*) eqs_* ...) + ...) + (where (((p_* ... -> r_*) eqs_* ...) ...) + (SL (((p ... -> r) eqs_2 ...) ...)))] + [(SL (((p_1 ... -> r_1) eqs_1 ...) ((p ... -> r) eqs_2 ...) ...)) + (((p_* ... -> r_*) eqs_* ...) + ...) + (where (((p_* ... -> r_*) eqs_* ...) ...) + (SL (((p ... -> r) eqs_2 ...) ...)))]) + +; S metafunction from the paper +(define-metafunction L + S : cw (row ...) -> (row ...) + [(S cw ()) ()] + [(S wc (((p ... -> r) eqs_1 ...) ...)) ()] + [(S c_1 (((c_1 p_2 ... -> r_1) eqs_1 ...) ((p ... -> r) eqs_2 ...) ...)) + (((p_2 ... -> r_1) eqs_1 ...) + ((p_* ... -> r_*) eqs_* ...) + ...) + (where (((p_* ... -> r_*) eqs_* ...) ...) + (S c_1 (((p ... -> r) eqs_2 ...) ...)))] + [(S cw (((p_1 p_2 ... -> r_1) eqs_1 ...) ((p ... -> r) eqs_2 ...) ...)) + (((p_* ... -> r_*) eqs_* ...) + ...) + (where (((p_* ... -> r_*) eqs_* ...) ...) + (S cw (((p ... -> r) eqs_2 ...) ...)))] + [(S cw (((p_1 ... -> r_1) eqs_1 ...) ((p ... -> r) eqs_2 ...) ...)) + (((p_* ... -> r_*) eqs_* ...) + ...) + (where (((p_* ... -> r_*) eqs_* ...) ...) + (S cw (((p ... -> r) eqs_2 ...) ...)))]) + +; D metafunction from the paper +(define-metafunction L + D : (row ...) -> (row ...) + [(D ()) ()] + [(D (((wc p_2 ... -> r_1) eqs_1 ...) ((p ... -> r) eqs_2 ...) ...)) + (((p_2 ... -> r_1) eqs_1 ...) + ((p_* ... -> r_*) eqs_* ...) + ...) + (where (((p_* ... -> r_*) eqs_* ...) ...) + (D (((p ... -> r) eqs_2 ...) ...)))] + [(D (((p_1 p_2 ... -> r_1) eqs_1 ...) ((p ... -> r) eqs_2 ...) ...)) + (((p_* ... -> r_*) eqs_* ...) + ...) + (where (((p_* ... -> r_*) eqs_* ...) ...) + (D (((p ... -> r) eqs_2 ...) ...)))]) + +(define-metafunction L + drop-first-p : (row ...) -> (row ...) + ((drop-first-p (((p_1 p_2 ... -> r) eqs_1 ...) ...)) + (((p_2 ... -> r) eqs_1 ...) ...)) + ) + + +(define-metafunction L + replace-first-p : p (row ...) -> (row ...) + ((replace-first-p p_1 (((p_2 p_3 ... -> r) eqs_1 ...) ...)) + (((p_1 p_3 ... -> r) eqs_1 ...) ...)) + ) + +(define-metafunction L + same-starting-pattern : p (row ...) -> (row ...) + ((same-starting-pattern p_1 (((p_1 p_3 ... -> r) eqs_1 ...) row ...)) + (((p_1 p_3 ... -> r) eqs_1 ...) row_* ...) + (where (row_* ...) + (same-starting-pattern p_1 (row ...)))) + ((same-starting-pattern (name p_1 p_!_1) (((p_!_1 p_3 ... -> r) eqs_1 ...) row ...)) + (row_* ...) + (where (row_* ...) + (same-starting-pattern p_1 (row ...)))) + ((same-starting-pattern p_1 ()) ()) + ) + +(define-metafunction L + diff-starting-pattern : p (row ...) -> (row ...) + ((diff-starting-pattern p_1 (((p_1 p_3 ... -> r) eqs_1 ...) row ...)) + (diff-starting-pattern p_1 (row ...))) + ((diff-starting-pattern (name p_1 p_!_1) ((((name p_2 p_!_1) p_3 ... -> r) eqs_1 ...) row ...)) + (((p_2 p_3 ... -> r) eqs_1 ...) row_* ...) + (where (row_* ...) + (diff-starting-pattern p_1 (row ...)))) + ((diff-starting-pattern p_1 ()) ()) + ) + +(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)) + ()) + ) + + +(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)) + (Build-Term-Let (eqs_2 ... (pvar #t eq_1 ... eq_2 ...)) r)) + (side-condition (andmap not-an-id? (term (eq_1 ...))))) + + ((Build-Term-Let ((pvar #f eq_1 ... id eq_2 ...) eqs_2 ...) r) + (term-let ((pvar id)) + (Build-Term-Let (eqs_2 ... (pvar #t eq_1 ... eq_2 ...)) r)) + (side-condition (andmap not-an-id? (term (eq_1 ...))))) + + ((Build-Term-Let ((pvar #t eq_1 ... id eq_2 ...) eqs_2 ...) r) + (if (equal? (term pvar) id) + (Build-Term-Let (eqs_2 ... (pvar #t eq_1 ... eq_2 ...)) r) + ∅) + (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)) + (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 ...))))) + + ((Build-Term-Let ((pvar #t eq ... (= pvar_3) eq_2 ...) eqs_2 ... (pvar_3 #t eq_3 ...) eqs_3 ...) r) + (if (equal? (term 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 ...))))) + + ((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)) + (side-condition (or (and (term bool_1) + (not (term bool_2))) + (and (not (term bool_1)) + (term bool_2)) + (and (not (term bool_1)) + (not (term bool_2)))))) + + ((Build-Term-Let ((pvar #t eq ... (cons pvar_1 pvar_3) eq_3 ...) eqs_2 ... (pvar_1 #t eq_1 ...) eqs_3 ... (pvar_3 #t eq_4 ...) eqs_4 ...) r) + (if (and (cons? (term pvar)) + (equal? (car (term pvar)) (term pvar_1)) + (equal? (cdr (term pvar)) (term pvar_3))) + (Build-Term-Let (eqs_2 ... (pvar_1 #t eq_1 ...) eqs_3 ... (pvar_3 #t eq_4 ...) eqs_4 ... (pvar #t eq ... eq_3 ...)) r) + ∅) + (side-condition (and (term pvar) + (term pvar_1) + (term pvar_3) + (andmap (λ (x) (not (redex-match L (cons pvar_11 pvar_12) x))) (term (eq ...)))))) + + ((Build-Term-Let ((pvar bool (cons pvar_1 pvar_3) eq_3 ...) eqs_2 ... (pvar_1 bool_1 eq_1 ...) eqs_3 ... (pvar_3 bool_3 eq_4 ...) eqs_4 ...) r) + (Build-Term-Let (eqs_2 ... (pvar_1 bool_1 eq_1 ...) eqs_3 ... (pvar_3 bool_3 eq_4 ...) eqs_4 ... (pvar bool eq_3 ... (cons pvar_1 pvar_3))) r) + (side-condition (or (not (term bool_1)) + (not (term bool_3))))) + + ((Build-Term-Let ((pvar #f eq ... (cons pvar_1 pvar_3) eq_3 ...) eqs_2 ... (pvar_1 #t eq_1 ...) eqs_3 ... (pvar_3 #t eq_4 ...) eqs_4 ...) r) + (term-let ((pvar (cons (term pvar_1) (term pvar_3)))) + (Build-Term-Let (eqs_2 ... (pvar_1 #t eq_1 ...) eqs_3 ... (pvar_3 #t eq_4 ...) eqs_4 ... (pvar #t eq ... eq_3 ...)) r)) + (side-condition (andmap (λ (x) (not (redex-match L (cons pvar_11 pvar_12) x))) (term (eq ...))))) + + ((Build-Term-Let ((pvar #t eq ... (plug pvar_1 pvar_3) eq_3 ...) eqs_2 ... (pvar_1 #t eq_1 ...) eqs_3 ... (pvar_3 #t eq_4 ...) eqs_4 ...) r) + (if (equal? (term pvar) (plug (term pvar_1) (term pvar_3))) + (Build-Term-Let (eqs_2 ... (pvar_1 #t eq_1 ...) eqs_3 ... (pvar_3 #t eq_4 ...) eqs_4 ... (pvar #t eq ... eq_3 ...)) r) + ∅) + (side-condition (andmap (λ (x) (not (redex-match L (plug pvar_11 pvar_12) x))) (term (eq ...))))) + + ((Build-Term-Let ((pvar #f eq ... (plug pvar_1 pvar_3) eq_3 ...) eqs_2 ... (pvar_1 #t eq_1 ...) eqs_3 ... (pvar_3 #t eq_4 ...) eqs_4 ...) r) + (term-let ((pvar (plug (term pvar_1) (term pvar_3)))) + (Build-Term-Let (eqs_2 ... (pvar_1 #t eq_1 ...) eqs_3 ... (pvar_3 #t eq_4 ...) eqs_4 ... (pvar #t eq ... eq_3 ...)) r)) + (side-condition (andmap (λ (x) (not (redex-match L (plug pvar_11 pvar_12) x))) (term (eq ...))))) + + ((Build-Term-Let ((pvar bool (plug pvar_1 pvar_3) eq_3 ...) eqs_2 ...) r) + (Build-Term-Let (eqs_2 ... (pvar bool eq_3 ... (plug pvar_1 pvar_3))) r)) + + ((Build-Term-Let ((pvar #t eq ... (cons pvar_1 pvar_3) eq_3 ...) eqs_2 ... (pvar_3 #t eq_1 ...) eqs_3 ... (pvar_1 #t eq_4 ...) eqs_4 ...) r) + (if (and (cons? (term pvar)) + (equal? (car (term pvar)) (term pvar_1)) + (equal? (cdr (term pvar)) (term pvar_3))) + (Build-Term-Let (eqs_2 ... (pvar_3 #t eq_1 ...) eqs_3 ... (pvar_1 #t eq_4 ...) eqs_4 ... (pvar #t eq ... eq_3 ...)) r) + ∅) + (side-condition (and (term pvar) + (term pvar_1) + (term pvar_3) + (andmap (λ (x) (not (redex-match L (cons pvar_11 pvar_12) x))) (term (eq ...)))))) + + ((Build-Term-Let ((pvar bool (cons pvar_1 pvar_3) eq_3 ...) eqs_2 ... (pvar_3 bool_1 eq_1 ...) eqs_3 ... (pvar_1 bool_3 eq_4 ...) eqs_4 ...) r) + (Build-Term-Let (eqs_2 ... (pvar_3 bool_1 eq_1 ...) eqs_3 ... (pvar_1 bool_3 eq_4 ...) eqs_4 ... (pvar bool eq_3 ... (cons pvar_1 pvar_3))) r) + (side-condition (or (not (term bool_1)) + (not (term bool_3))))) + + ((Build-Term-Let ((pvar #f eq ... (cons pvar_1 pvar_3) eq_3 ...) eqs_2 ... (pvar_3 #t eq_1 ...) eqs_3 ... (pvar_1 #t eq_4 ...) eqs_4 ...) r) + (term-let ((pvar (cons (term pvar_1) (term pvar_3)))) + (Build-Term-Let (eqs_2 ... (pvar_3 #t eq_1 ...) eqs_3 ... (pvar_1 #t eq_4 ...) eqs_4 ... (pvar #t eq ... eq_3 ...)) r)) + (side-condition (andmap (λ (x) (not (redex-match L (cons pvar_11 pvar_12) x))) (term (eq ...))))) + + ((Build-Term-Let ((pvar #t eq ... (plug pvar_1 pvar_3) eq_3 ...) eqs_2 ... (pvar_3 #t eq_1 ...) eqs_3 ... (pvar_1 #t eq_4 ...) eqs_4 ...) r) + (if (equal? (term pvar) (plug (term pvar_1) (term pvar_3))) + (Build-Term-Let (eqs_2 ... (pvar_3 #t eq_1 ...) eqs_3 ... (pvar_1 #t eq_4 ...) eqs_4 ... (pvar #t eq ... eq_3 ...)) r) + ∅) + (side-condition (andmap (λ (x) (not (redex-match L (plug pvar_11 pvar_12) x))) (term (eq ...))))) + + ((Build-Term-Let ((pvar #f eq ... (plug pvar_1 pvar_3) eq_3 ...) eqs_2 ... (pvar_3 #t eq_1 ...) eqs_3 ... (pvar_1 #t eq_4 ...) eqs_4 ...) r) + (term-let ((pvar (plug (term pvar_1) (term pvar_3)))) + (Build-Term-Let (eqs_2 ... (pvar_3 #t eq_1 ...) eqs_3 ... (pvar_1 #t eq_4 ...) eqs_4 ... (pvar #t eq ... eq_3 ...)) r)) + (side-condition (andmap (λ (x) (not (redex-match L (plug pvar_11 pvar_12) x))) (term (eq ...))))) + + ((Build-Term-Let ((pvar bool (plug pvar_1 pvar_3) eq_3 ...) eqs_2 ...) r) + (Build-Term-Let (eqs_2 ... (pvar bool eq_3 ... (plug pvar_1 pvar_3))) r)) + + ((Build-Term-Let ((pvar #t eq_1 ... lit-hole eq_2 ...) eqs_2 ...) r) + (if (equal? (term pvar) the-hole) + (Build-Term-Let (eqs_2 ... (pvar #t eq_1 ... eq_2 ...)) r) + ∅) + (side-condition (andmap not-a-lit-hole? (term (eq_1 ...))))) + + ((Build-Term-Let ((pvar bool eq ...) ...) (matrix (x_1 ...) (((p_1 ... -> r) eqs_2 ...)) (pvar_1 ...) (pvar_2 ...) natural bool_0)) + ,(begin (set! new-var-list (term ((pvar bool eq ...) ...))) + (term (matrix (x_1 ...) (((p_1 ... -> r) (pvar bool eq ...) ...)) (pvar_1 ...) (pvar_2 ...) natural bool_0))) + (side-condition (andmap (λ (x) + (or (eqv? 2 (length x)) + (not (or + (redex-match L (pvar_10 bool_10 eq_10 ... id eq_11 ...) x) + (redex-match L (pvar_10 bool_10 eq_10 ... lit-hole eq_11 ...) x) + (redex-match L (pvar_10 bool_10 eq_10 ... (= (side-condition eq_2 (redex-match L (eqs_4 ... (,(term eq_2) #t eq_4 ...) eqs_5 ...) (term ((pvar bool eq ...) ...))))) eq_11 ...) x) + (redex-match L (pvar_10 bool_10 eq_10 ... (cons + (side-condition eq_2 (redex-match L (eqs_4 ... (,(term eq_2) #t eq_4 ...) eqs_5 ...) (term ((pvar bool eq ...) ...)))) + (side-condition eq_6 (redex-match L (eqs_6 ... (,(term eq_6) #t eq_6 ...) eqs_7 ...) (term ((pvar bool eq ...) ...)))) + ) + eq_11 ...) x) + (redex-match L (pvar_10 bool_10 eq_10 ... (plug + (side-condition eq_2 (redex-match L (eqs_4 ... (,(term eq_2) #t eq_4 ...) eqs_5 ...) (term ((pvar bool eq ...) ...)))) + (side-condition eq_6 (redex-match L (eqs_6 ... (,(term eq_6) #t eq_6 ...) eqs_7 ...) (term ((pvar bool eq ...) ...)))) + ) + eq_11 ...) x) + ) + + + )) + ) (term ((pvar bool eq ...) ...))))) + + ((Build-Term-Let ((pvar bool eq ...) ...) r) + ,(begin (set! new-var-list (term ((pvar bool eq ...) ...))) (term r)) + (side-condition (andmap (λ (x) + (or (eqv? 2 (length x)) + (not (or + (redex-match L (pvar_10 bool_10 eq_10 ... id eq_11 ...) x) + (redex-match L (pvar_10 bool_10 eq_10 ... lit-hole eq_11 ...) x) + (redex-match L (pvar_10 bool_10 eq_10 ... (= (side-condition eq_2 (redex-match L (eqs_4 ... (,(term eq_2) #t eq_4 ...) eqs_5 ...) (term ((pvar bool eq ...) ...))))) eq_11 ...) x) + (redex-match L (pvar_10 bool_10 eq_10 ... (cons + (side-condition eq_2 (redex-match L (eqs_4 ... (,(term eq_2) #t eq_4 ...) eqs_5 ...) (term ((pvar bool eq ...) ...)))) + (side-condition eq_6 (redex-match L (eqs_6 ... (,(term eq_6) #t eq_6 ...) eqs_7 ...) (term ((pvar bool eq ...) ...)))) + ) + eq_11 ...) x) + (redex-match L (pvar_10 bool_10 eq_10 ... (plug + (side-condition eq_2 (redex-match L (eqs_4 ... (,(term eq_2) #t eq_4 ...) eqs_5 ...) (term ((pvar bool eq ...) ...)))) + (side-condition eq_6 (redex-match L (eqs_6 ... (,(term eq_6) #t eq_6 ...) eqs_7 ...) (term ((pvar bool eq ...) ...)))) + ) + eq_11 ...) x) + ) + + + )) + ) (term ((pvar bool eq ...) ...))))) + + ((Build-Term-Let ((pvar bool eq ...) eqs ...) r) + (Build-Term-Let (eqs ... (pvar bool eq ...)) r)) + + #;((Build-Term-Let ((pvar #t eq_1 eq_2 ...) eqs_2 ... (eq_1 #t eq_3 ...) eqs_3 ...) r) + (if (equal? (term pvar) (term eq_1)) + (Build-Term-Let ((pvar #t eq_2 ...) eqs_2 ... (eq_1 #t eq_3 ...) eqs_3 ...) r) + ∅)) + + #;((Build-Term-Let ((pvar #t) (pvar_2 #t) ... (pvar_3 #f) eqs ...) r) + (Build-Term-Let (eqs ... (pvar_3 #f)) r)) + + + + ; if a one-rowed matrix is the the result, assume that the matching isn't over and just update the eqs + #;((Build-Term-Let (eqs ...) (matrix (x_1 ...) (((p_1 ... -> r) eqs_2 ...)) (pvar_1 ...) (pvar_2 ...) natural bool)) + (matrix (x_1 ...) (((p_1 ... -> r) eqs ...)) (pvar_1 ...) (pvar_2 ...) natural bool)) + + #;((Build-Term-Let (eqs ...) r) + 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) + ) + +; 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) diff --git a/collects/redex/private/compiler/redextomatrix.rkt b/collects/redex/private/compiler/redextomatrix.rkt new file mode 100644 index 0000000000..8ed0a2b677 --- /dev/null +++ b/collects/redex/private/compiler/redextomatrix.rkt @@ -0,0 +1,630 @@ +#lang racket +(require redex) +(require "match.rkt") +(require racket/set) +(require profile) + +(define lit-table (make-hash)) +(define or-table (make-hash)) +(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) + ,non-terms ...) + (map (λ (x) (car x)) + non-terms)] + [_ + 'error])) + +(define (compile-define-language-lit dl nts) + (match dl + [`(define-language ,(? symbol? name) + ,non-terms ...) + (map (λ (x) (extract-literals/pat nts (cdr x) lit-table)) + non-terms)] + [_ + 'error])) + +(define (extract-literals/pat nts pat ht) + (let loop ([pat pat]) + (match pat + [`any (void)] + [`number (void)] + [`string (void)] + [`natural (void)] + [`integer (void)] + [`real (void)] + [`variable (void)] + [`(variable-except ,s ...) (void)] + [`(variable-prefix ,s) (void)] + [`variable-not-otherwise-mentioned (void)] + [`hole (void)] + [(? symbol? s) + (unless (regexp-match #rx"_" (symbol->string s)) + (unless (regexp-match #rx"^\\.\\.\\." (symbol->string s)) + (unless (memq s nts) + (hash-set! ht s #t) + )))] + [`(name ,name ,pat) (loop pat)] + [`(in-hole ,p1 ,p2) + (loop p1) + (loop p2)] + [`(hide-hole ,p) (loop p)] + [`(side-condition ,p ,g ,e) + (loop p)] + [`(cross ,s) (void)] + [_ + (let l-loop ([l-pat pat]) + (when (pair? l-pat) + (loop (car l-pat)) + (l-loop (cdr l-pat))))]))) + +(define (compile-define-language-or dl nts) + (match dl + [`(define-language ,(? symbol? name) + ,non-terms ...) + (map (λ (x) (hash-set! or-table (car x) (build-or (cdr x) nts (hash-map lit-table (λ (x y) x)) #t))) + non-terms)] + [_ + 'error])) + +(define (build-or pat-l nts syms dl) + (let loop ([pat-l pat-l] + [nts nts] + [syms syms]) + (if (pair? pat-l) + (if (eqv? (length pat-l) 1) + (translate-redex (car pat-l) nts syms dl) + `(or ,(translate-redex (car pat-l) nts syms dl) + ,(loop (cdr pat-l) nts syms))) + (translate-redex pat-l nts syms dl)))) + +(define (translate-redex pat nts syms dl) + (let loop ([pat pat]) + (match pat + [`(,repeated ,(? (λ (x) (eq? x '...)) ep)) + `(repeat ,(loop repeated) '())] + [`(,repeated ,(? (λ (x) (eq? x '...)) ep) ,next ...) + `(repeat ,(loop repeated) ,(loop next))] + [`any (if dl 'wc '(lit-name any wc))] + [`number (if dl 'lit-number '(lit-name number lit-number))] + [`string (if dl 'lit-string '(lit-name string lit-string))] + [`natural (if dl 'lit-natural '(lit-name natural lit-natural))] + [`integer (if dl 'lit-integer '(lit-name integer lit-integer))] + [`real (if dl 'lit-real '(lit-name real lit-real))] + [`variable (if dl 'lit-variable '(lit-name variable lit-variable))] + [`(variable-except ,s ...) `(lit-variable-except ,@s)] + [`(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 + `(nt ,s) + `(lit-name ,s (nt ,s))) + (if (has-underscore? s) + (let ((split (split-underscore s))) + (cond + ((equal? split 'any) `(lit-name ,s wc)) + ((equal? split 'number) `(lit-name ,s lit-number)) + ((equal? split 'string) `(lit-name ,s lit-string)) + ((equal? split 'natural) `(lit-name ,s lit-natural)) + ((equal? split 'integer) `(lit-name ,s lit-integer)) + ((equal? split 'real) `(lit-name ,s lit-real)) + ((equal? split 'variable) `(lit-name ,s lit-variable)) + ((equal? split 'variable-not-otherwise-mentioned) `(lit-name ,s (lit-variable-except ,@syms))) + ((equal? split 'hole) `(lit-name ,s lit-hole)) + (else `(lit-name ,s (nt ,split))) + ) + ) + `',s))] + [`(name ,name ,pat) `(lit-name ,name ,(loop pat))] + [`(in-hole ,p1 ,p2) + `(lit-in-hole + ,(loop p1) + ,(loop p2))] + [`(hide-hole ,p) `(lit-hide-hole ,(loop p))] + [`(side-condition ,p #;,g ,e) + `(lit-side-condition ,(loop p) ,e)] + [`(cross ,s) (void)] + [e + (if (pair? pat) + `(cons ,(loop (car pat)) + ,(loop (cdr pat))) + (if (empty? pat) + ''() + e))] + ))) + +;; split-underscore : symbol -> symbol +;; returns the text before the underscore in a symbol (as a symbol) +;; raise an error if there is more than one underscore in the input +(define (split-underscore sym) + (let ([str (symbol->string sym)]) + (cond + [(regexp-match #rx"^([^_]*)_[^_]*$" str) + => + (λ (m) (string->symbol (cadr m)))] + [(regexp-match #rx"^([^_]*)_!_[^_]*$" str) + => + (λ (m) (string->symbol (cadr m)))] + [else + (error 'compile-pattern "found a symbol with multiple underscores: ~s" sym)]))) + +;; has-underscore? : symbol -> boolean +(define (has-underscore? sym) + (memq #\_ (string->list (symbol->string sym)))) + +(define build-hole-table + (λ (old-ht) + (unless (equal? hole-table old-ht) + (let ((prev (make-hash))) + (hash-for-each + hole-table + (λ (key val) + (hash-set! prev key val))) + (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)))) + ) + +(define state '()) +(define hole-var '()) +(define nt-func '()) + +(define wrap-production-with-name + (λ (x) + (set! state x) + (set! hole-var '()) + (set! nt-func '()) + (wrap-production-with-name-helper x) + ) + ) + +(define wrap-production-with-name-helper + (λ (exp) + (match exp + [`(cons ,(? (λ (x) (eqv? 1 (term (detect-hole2 0 ,x)))) p1) + ,(? (λ (x) (eqv? 0 (term (detect-hole2 0 ,x)))) p2)) + `(cons ,(wrap-production-with-name-helper p1) ,(wrap-production-with-name-helper p2))] + [`(cons ,(? (λ (x) (eqv? 0 (term (detect-hole2 0 ,x)))) p1) + ,(? (λ (x) (eqv? 1 (term (detect-hole2 0 ,x)))) p2)) + `(cons ,(wrap-production-with-name-helper p1) ,(wrap-production-with-name-helper p2))] + [`(cons ,(? (λ (x) (eqv? 0 (term (detect-hole2 0 ,x)))) p1) + ,(? (λ (x) (eqv? 0 (term (detect-hole2 0 ,x)))) p2)) + (let ((x (variable-not-in state 'x))) + (set! state (cons x state)) + `(lit-name ,x (cons ,p1 ,p2)))] + [`(lit-name ,id ,(? (λ (x) (eqv? 1 (term (detect-hole2 0 ,x)))) p)) + `(lit-name ,id ,(wrap-production-with-name-helper p))] + [`(lit-name ,id ,(? (λ (x) (eqv? 0 (term (detect-hole2 0 ,x)))) p)) + `(lit-name ,id ,p)] + [`(lit-side-condition ,(? (λ (x) (eqv? 0 (term (detect-hole2 0 ,x)))) p) ,any) + (let ((x (variable-not-in state 'x))) + (set! state (cons x state)) + `(lit-name ,x (lit-side-condition ,p ,any)) + )] + [`(lit-side-condition ,(? (λ (x) (eqv? 1 (term (detect-hole2 0 ,x)))) p) ,any) + (wrap-production-with-name-helper p)] + [`(repeat ,p1 ,(? (λ (x) (eqv? 0 (term (detect-hole2 0 ,x)))) p2)) + (let ((x (variable-not-in state 'x))) + (set! state (cons x state)) + `(lit-name ,x (repeat ,p1 ,p2)) + )] + [`(repeat ,p1 ,(? (λ (x) (eqv? 1 (term (detect-hole2 0 ,x)))) p2)) + (let ((x (variable-not-in state 'x))) + (set! state (cons x state)) + `(repeat (lit-name ,x ,p1) ,(wrap-production-with-name-helper p2)) + )] + [`(lit-in-hole ,p1 ,(? (λ (x) (eqv? 0 (term (detect-hole2 0 ,x)))) p2)) + (let ((x (variable-not-in state 'x))) + (set! state (cons x state)) + `(lit-name ,x (lit-in-hole ,p1 ,p2)) + )] + [`(lit-in-hole ,p1 ,(? (λ (x) (eqv? 1 (term (detect-hole2 0 ,x)))) p2)) + (let ((x (variable-not-in state 'x))) + (set! state (cons x state)) + (let ((y (variable-not-in state 'y))) + (set! hole-var y) + `(lit-in-hole (lit-name ,x ,p1) (lit-name ,y ,p2)) + ) + )] + ['lit-hole + (let ((x (variable-not-in state 'x))) + (set! state (cons x state)) + (set! hole-var x) + `(lit-name ,x lit-hole) + )] + [`(nt ,id) + (if (eqv? 1 (term (detect-hole2 0 (nt ,id)))) + (let ((x (variable-not-in state 'x))) + (set! state (cons x state)) + (set! hole-var x) + (set! nt-func id) + `(lit-name ,x wc) + ) + (let ((x (variable-not-in state 'x))) + (set! state (cons x state)) + `(lit-name ,x (nt ,id)) + ) + )] + [`',(? (λ (x) (or (symbol? x) (equal? '() x))) ex) + exp] + [_ (if (or (number? exp) (string? exp) (boolean? exp)) + exp + (let ((x (variable-not-in state 'x))) + (set! state (cons x state)) + `(lit-name ,x ,exp) + ))]) + ) + ) + +(define build-right-hand-side + (λ (x) + (if (equal? nt-func '()) + (if (equal? hole-var '()) + `(set! results (cons (cons ,(build-right-hand-side-helper x) '()) results)) + `(set! results (cons (cons ,(build-right-hand-side-helper x) (term ,hole-var)) results)) + ) + `(for ((,hole-var (in-list (,(string->symbol (format "~s~s" nt-func '-list)) (term ,hole-var))))) + (set! results (cons (cons ,(build-right-hand-side-helper x) (cdr ,hole-var)) results)) + ) + ) + ) + ) + +(define build-right-hand-side-helper + (λ (exp) + (match exp + [`(lit-name ,(? (λ (x) (not (equal? hole-var x))) x) ,p) + (if (or (not (cons? p)) (and (cons? p) (not (equal? (car p) 'lit-name)))) + `(term ,x) + (build-right-hand-side-helper p))] + [`(lit-name ,(? (λ (x) (equal? hole-var x)) x) lit-hole) + 'the-hole] + [`(lit-name ,(? (λ (x) (equal? hole-var x)) x) wc) + `(car ,hole-var)] + [`(lit-name ,(? (λ (x) (equal? hole-var x)) x) ,p) + `(term ,x)] + [`(cons ,p1 ,p2) + `(cons ,(build-right-hand-side-helper p1) ,(build-right-hand-side-helper p2))] + [`(lit-in-hole ,p1 ,p2) + (build-right-hand-side-helper p1)] + [`(repeat ,p1 ,p2) + `(append ,(build-right-hand-side-helper p1) ,(build-right-hand-side-helper p2))] + [_ + exp] + ))) + +(define make-or-list + (λ (exp) + (match exp + [`(or ,pro1 ,pro2) + (cons pro1 (make-or-list pro2))] + [_ (cons exp '())] + ) + ) + ) + +(define-namespace-anchor here) + +(define (compile-dl lang) + (let* ([lang lang] + [nts (compile-define-language-nts lang)] + [lit-table lit-table] + [or-table or-table] + [nt-table nt-table] + [hole-table hole-table]) + + + (compile-define-language-lit lang nts) + (compile-define-language-or lang nts) + (caching-enabled? #f) + ; Initialize the hole table + (hash-for-each + or-table + (λ (key val) + (hash-set! hole-table key (term (detect-hole 0 ,val))) + )) + + (build-hole-table '()) + (caching-enabled? #t) + + (printf "~a\n ~a\n ~a\n ~a\n\n\n" nts lit-table or-table hole-table) + (hash-for-each + or-table + (λ (key val) + (let ((val val)) + (printf "non-terminal: ~a\n" key) + + (printf "~a\n~a\n\n" + `(term (matrix (a) + ( + ((,val -> (set! results (cons #t results))) ,@(map (λ (x) (list x #f)) (remove-duplicates (term (Get-Free-Name-Patterns ,val () ()))))) + ) + () + () + 0 + #f)) + `(term (matrix (a) + ( ,@(map (λ (x) + (let ((row (wrap-production-with-name x))) + `((,row -> ,(build-right-hand-side row)) + + ,@(map (λ (x) (list x #f)) (remove-duplicates (term (Get-Free-Name-Patterns ,row () ()))))))) + (make-or-list val))) + () + () + 0 + #f))) + (let ((compiled-bool (car (apply-reduction-relation* red + (term (matrix (a) + ( + ((,val -> (set! results (cons #t results))) ,@(map (λ (x) (list x #f)) (remove-duplicates (term (Get-Free-Name-Patterns ,val () ()))))) + ) + () + () + 0 + #f))))) + (compiled-set (car (apply-reduction-relation* red + (term (matrix (a) + ( ,@(map (λ (x) + (let ((row (wrap-production-with-name x))) + (printf "Row: ~a Wrapped: ~a\n" x row) + `((,row -> ,(build-right-hand-side row)) + + ,@(map (λ (x) (list x #f)) (remove-duplicates (term (Get-Free-Name-Patterns ,row () ()))))))) + (make-or-list val))) + () + () + 0 + #f)))) + )) + (printf "compiled bool: ~a\n\n" compiled-bool) + (printf "compiled set: ~a\n\n" compiled-set) + (hash-set! nt-table + key + (make-nt-struct + (term (define ,(string->symbol (format "~s~s" key '-bool)) + (λ (a) + (let ((results (list))) + ,compiled-bool + (and (andmap values results) (positive? (length results)))) + ) + ) + ) + (term (define ,(string->symbol (format "~s~s" key '-list)) + (λ (a) + (let ((results (list))) + ,compiled-set + results + ) + ) + )) + )) + )))) + #;(let ((rr (compile-reduction-relation lang-rr nts (hash-map lit-table (λ (x y) x))))) + (print rr) + (apply-reduction-relation* red rr)) + ) + ) + +(define (compile-reduction-relation rr nts syms) + (let* ([lit-table lit-table] + [or-table or-table] + [nt-table nt-table] + [hole-table hole-table] + [e rr]) + (let loop ([e e]) + (match e + [`(reduction-relation ,L ,rules ...) + (term (matrix (a) ,(map loop rules) () () 0 #f))] + [`(--> ,pat ,t) + (let ((p (translate-redex pat nts syms #f))) + (printf "Left hand side: ~a\n\n" p) + (printf "Right hand side: ~a\n\n" t) + `((,p -> (set! results (cons (term ,t) results))) ,@(map (λ (x) (list x #f)) (remove-duplicates (term (Get-Free-Name-Patterns ,p () ()))))) + )]) + ))) + +(compile-dl lang) + +(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) + ))) + +(caching-enabled? #f) + +(define ∅ #f) +(define ∪ set-union) +(define singleton set) + +(define no-context #f) + +(define in-context #t) + +(define context-match (make-parameter no-context)) + +(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)) From 14ceb68b92823170e52d1e938dc8a5919d609949 Mon Sep 17 00:00:00 2001 From: Casey Klein Date: Wed, 8 Sep 2010 14:01:27 -0500 Subject: [PATCH 6/9] Adds functions for testing pattern compiler --- collects/redex/private/compiler/match.rkt | 13 +- .../redex/private/compiler/redextomatrix.rkt | 170 ++++++++---------- 2 files changed, 89 insertions(+), 94 deletions(-) diff --git a/collects/redex/private/compiler/match.rkt b/collects/redex/private/compiler/match.rkt index e74fdf431e..e25ae41c28 100644 --- a/collects/redex/private/compiler/match.rkt +++ b/collects/redex/private/compiler/match.rkt @@ -6,7 +6,8 @@ Build-Cond Cond-List simplify - simple-swap) + simple-swap + compile) (define hole-table (make-hash)) @@ -2376,6 +2377,16 @@ ((simple-swap any) any) ) +(define-namespace-anchor here) + +(define/contract (compile m) + (-> (redex-match L m) (-> any/c any/c)) + (eval `(λ ,(second m) + (let ([results '()]) + ,(car (apply-reduction-relation* red m)) + results)) + (namespace-anchor->namespace here))) + ; TEST CASES (define ∅ (set)) diff --git a/collects/redex/private/compiler/redextomatrix.rkt b/collects/redex/private/compiler/redextomatrix.rkt index 8ed0a2b677..2e359970e1 100644 --- a/collects/redex/private/compiler/redextomatrix.rkt +++ b/collects/redex/private/compiler/redextomatrix.rkt @@ -4,6 +4,9 @@ (require racket/set) (require profile) +(provide test-red-rel + test-non-term) + (define lit-table (make-hash)) (define or-table (make-hash)) (define nt-table (make-hash)) @@ -14,7 +17,7 @@ (define-struct nt-struct (match-bool match-set)) -(define lang '(define-language T +#;(define lang '(define-language T (n (number_1 ... number_1 ...)) (m ((number_1 number_1) ...)) (o ((number_1 ... number_1 ...) ...)) @@ -470,6 +473,7 @@ (define-namespace-anchor here) +;; compile-dl : sexp[lang] -> (listof sexp[def]) (define (compile-dl lang) (let* ([lang lang] [nts (compile-define-language-nts lang)] @@ -492,104 +496,84 @@ (build-hole-table '()) (caching-enabled? #t) - (printf "~a\n ~a\n ~a\n ~a\n\n\n" nts lit-table or-table hole-table) (hash-for-each or-table (λ (key val) - (let ((val val)) - (printf "non-terminal: ~a\n" key) - - (printf "~a\n~a\n\n" - `(term (matrix (a) - ( - ((,val -> (set! results (cons #t results))) ,@(map (λ (x) (list x #f)) (remove-duplicates (term (Get-Free-Name-Patterns ,val () ()))))) - ) - () - () - 0 - #f)) - `(term (matrix (a) - ( ,@(map (λ (x) - (let ((row (wrap-production-with-name x))) - `((,row -> ,(build-right-hand-side row)) - - ,@(map (λ (x) (list x #f)) (remove-duplicates (term (Get-Free-Name-Patterns ,row () ()))))))) - (make-or-list val))) - () - () - 0 - #f))) - (let ((compiled-bool (car (apply-reduction-relation* red - (term (matrix (a) - ( - ((,val -> (set! results (cons #t results))) ,@(map (λ (x) (list x #f)) (remove-duplicates (term (Get-Free-Name-Patterns ,val () ()))))) - ) - () - () - 0 - #f))))) - (compiled-set (car (apply-reduction-relation* red - (term (matrix (a) - ( ,@(map (λ (x) - (let ((row (wrap-production-with-name x))) - (printf "Row: ~a Wrapped: ~a\n" x row) - `((,row -> ,(build-right-hand-side row)) - - ,@(map (λ (x) (list x #f)) (remove-duplicates (term (Get-Free-Name-Patterns ,row () ()))))))) - (make-or-list val))) - () - () - 0 - #f)))) - )) - (printf "compiled bool: ~a\n\n" compiled-bool) - (printf "compiled set: ~a\n\n" compiled-set) - (hash-set! nt-table - key - (make-nt-struct - (term (define ,(string->symbol (format "~s~s" key '-bool)) - (λ (a) - (let ((results (list))) - ,compiled-bool - (and (andmap values results) (positive? (length results)))) - ) - ) - ) - (term (define ,(string->symbol (format "~s~s" key '-list)) - (λ (a) - (let ((results (list))) - ,compiled-set - results - ) - ) - )) - )) - )))) - #;(let ((rr (compile-reduction-relation lang-rr nts (hash-map lit-table (λ (x y) x))))) - (print rr) - (apply-reduction-relation* red rr)) - ) - ) + (let ((compiled-bool (car (apply-reduction-relation* red + (term (matrix (a) + ( + ((,val -> (set! results (cons #t results))) ,@(map (λ (x) (list x #f)) (remove-duplicates (term (Get-Free-Name-Patterns ,val () ()))))) + ) + () + () + 0 + #f))))) + (compiled-set (car (apply-reduction-relation* red + (term (matrix (a) + ( ,@(map (λ (x) + (let ((row (wrap-production-with-name x))) + `((,row -> ,(build-right-hand-side row)) + + ,@(map (λ (x) (list x #f)) (remove-duplicates (term (Get-Free-Name-Patterns ,row () ()))))))) + (make-or-list val))) + () + () + 0 + #f)))) + )) + (hash-set! nt-table + key + (make-nt-struct + (term (define ,(string->symbol (format "~s~s" key '-bool)) + (λ (a) + (let ((results (list))) + ,compiled-bool + (and (andmap values results) (positive? (length results))))))) + (term (define ,(string->symbol (format "~s~s" key '-list)) + (λ (a) + (let ((results (list))) + ,compiled-set + results))))))))) + + (append (hash-map nt-table (λ (_ n) (nt-struct-match-bool n))) + (hash-map nt-table (λ (_ n) (nt-struct-match-set n)))))) +; compile-reduction-relation: sexp[reduction-relation] (listof symbol[non-terminals]) (listof symbols) -> sexp[def] (define (compile-reduction-relation rr nts syms) - (let* ([lit-table lit-table] - [or-table or-table] - [nt-table nt-table] - [hole-table hole-table] - [e rr]) - (let loop ([e e]) - (match e - [`(reduction-relation ,L ,rules ...) - (term (matrix (a) ,(map loop rules) () () 0 #f))] - [`(--> ,pat ,t) - (let ((p (translate-redex pat nts syms #f))) - (printf "Left hand side: ~a\n\n" p) - (printf "Right hand side: ~a\n\n" t) - `((,p -> (set! results (cons (term ,t) results))) ,@(map (λ (x) (list x #f)) (remove-duplicates (term (Get-Free-Name-Patterns ,p () ()))))) - )]) - ))) + `(λ (a) + (let ([results '()]) + ,(car + (apply-reduction-relation* + red + (let loop ([e rr]) + (match e + [`(reduction-relation ,L ,rules ...) + (term (matrix (a) ,(map loop rules) () () 0 #f))] + [`(--> ,pat ,t) + (let ((p (translate-redex pat nts syms #f))) + `((,p -> (set! results (cons (term ,t) results))) + ,@(map (λ (x) (list x #f)) + (remove-duplicates (term (Get-Free-Name-Patterns ,p () ()))))))])))) + results))) -(compile-dl lang) +;; make-lang-namespace: sexp[lang] -> namespace +(define (make-lang-namespace lang) + (define lang-defs (compile-dl lang)) + (define namespace (namespace-anchor->namespace here)) + (for-each (curryr eval namespace) lang-defs) + namespace) + +;; 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) + (eval (compile-reduction-relation rel 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 From 8fae368376d020d93e8b9ef6387fb884ec9b49c5 Mon Sep 17 00:00:00 2001 From: Casey Klein Date: Wed, 8 Sep 2010 14:11:36 -0500 Subject: [PATCH 7/9] Ignores prototype Redex pattern compiler --- collects/meta/props | 2 ++ 1 file changed, 2 insertions(+) diff --git a/collects/meta/props b/collects/meta/props index d27313574d..c580da6e65 100755 --- a/collects/meta/props +++ b/collects/meta/props @@ -1201,6 +1201,8 @@ path/s is either such a string or a list of them. "collects/redex/main.rkt" drdr:command-line (gracket-text "-t" *) "collects/redex/pict.rkt" drdr:command-line (gracket-text "-t" *) "collects/redex/private/arrow.rkt" drdr:command-line (gracket-text "-t" *) +"collects/redex/private/compiler/match.rkt" drdr:command-line #f +"collects/redex/private/compiler/redextomatrix.rkt" drdr:command-line #f "collects/redex/private/core-layout.rkt" drdr:command-line (gracket-text "-t" *) "collects/redex/private/dot.rkt" drdr:command-line (gracket-text "-t" *) "collects/redex/private/pict.rkt" drdr:command-line (gracket-text "-t" *) From 41e4470f232b8378e48dfce8b7fef539db35a2b3 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Wed, 8 Sep 2010 17:02:29 -0500 Subject: [PATCH 8/9] closes PR 11134 --- collects/drracket/private/language-configuration.rkt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/collects/drracket/private/language-configuration.rkt b/collects/drracket/private/language-configuration.rkt index e676ea650a..d7e308bbcd 100644 --- a/collects/drracket/private/language-configuration.rkt +++ b/collects/drracket/private/language-configuration.rkt @@ -1826,7 +1826,7 @@ [min-height (floor (/ (send plt-logo-shiny get-height) 2))]) (new canvas-message% (parent racketeer-panel) - (label sc-use-language-in-source) + (label (string-constant use-language-in-source)) (color (send the-color-database find-color "blue")) (callback (λ () (change-current-lang-to (λ (x) (is-a? x drracket:module-language:module-language<%>))))) (font (get-font #:underlined #t)))) From 93ee20e290ba111528b553d163566a8a8399bc7b Mon Sep 17 00:00:00 2001 From: John Clements Date: Wed, 8 Sep 2010 16:55:18 -0700 Subject: [PATCH 9/9] mods to sndfile.rkt --- collects/ffi/examples/sndfile.rkt | 37 +++++++++++++------------------ 1 file changed, 16 insertions(+), 21 deletions(-) diff --git a/collects/ffi/examples/sndfile.rkt b/collects/ffi/examples/sndfile.rkt index 7083f56814..32a4640a93 100644 --- a/collects/ffi/examples/sndfile.rkt +++ b/collects/ffi/examples/sndfile.rkt @@ -460,32 +460,27 @@ (define (write-sound* file data meta) (write-sound-internal/lists file data meta)) -;; an rsound (racket sound) provides a representation for sounds -;; that leaves them packed as C data. For the moment, it's -;; 2-channel float only. Also, it discards all meta-information -;; except length and sample-rate. -;; a rsound is (rsound _cpointer nat nat) -(provide (struct-out rsound)) -(struct rsound (data frames sample-rate)) +;; here's a simplified interface that leaves sounds packed as +;; C data. It's 2-channel 32-bit float only. Also, it discards +;; all meta-information except length and sample-rate. -;; these readers and writers short-cut the translation to/from lists. - -;; read-rsound : path-string -> rsound -;; read the file into a rsound -(provide read-rsound) -(define (read-rsound file) +;; read-sound/floatblock : path-string -> (list/c _pointer nat nat) +;; read the file into a buffer, return the data, the number of frames, +;; and the sample rate. +(provide read-sound/floatblock) +(define (read-sound/floatblock file) (parameterize ([sample-type 'float]) (let*-values ([(cblock meta) (read-sound-internal file #:split #f)]) - (rsound cblock (cadr (assq 'frames meta)) (cadr (assq 'samplerate meta)))))) + (list cblock (cadr (assq 'frames meta)) (cadr (assq 'samplerate meta)))))) -;; write-rsound : rsound path-string -> (void) -;; write the rsound to the given file as a wav. -(provide write-rsound) -(define (write-rsound sound file) - (write-sound-internal/cblock file (rsound-data sound) '(wav float file) - (rsound-sample-rate sound) - (rsound-frames sound) +;; write-sound/floatblock : _pointer nat nat path-string -> (void) +;; write the floatblock sound to the given file as a wav. +(provide write-sound/floatblock) +(define (write-sound/floatblock data frames sample-rate file) + (write-sound-internal/cblock file data '(wav float file) + sample-rate + frames 2 'float ;; for now, no meta-data possible.