From ddc5d91e24572e871d37d381bebdff37772d0fd3 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Sun, 14 Jun 2009 17:22:17 +0000 Subject: [PATCH] added a first attempt at define-relation svn: r15171 --- collects/redex/private/reduction-semantics.ss | 39 ++++++++++++--- collects/redex/private/tl-test.ss | 47 ++++++++++++++++++- collects/redex/redex.scrbl | 34 +++++++++++++- collects/redex/reduction-semantics.ss | 1 + 4 files changed, 111 insertions(+), 10 deletions(-) diff --git a/collects/redex/private/reduction-semantics.ss b/collects/redex/private/reduction-semantics.ss index f3da8a5bf6..8e0001be61 100644 --- a/collects/redex/private/reduction-semantics.ss +++ b/collects/redex/private/reduction-semantics.ss @@ -983,20 +983,26 @@ ; -(define-syntax-set (define-metafunction define-metafunction/extension) +(define-syntax-set (define-metafunction define-metafunction/extension define-relation) (define (define-metafunction/proc stx) (syntax-case stx () [(_ . rest) - (internal-define-metafunction stx #f #'rest)])) + (internal-define-metafunction stx #f #'rest #f)])) + + (define (define-relation/proc stx) + (syntax-case stx () + [(_ . rest) + ;; need to rule out the contracts for this one + (internal-define-metafunction stx #f #'rest #t)])) (define (define-metafunction/extension/proc stx) (syntax-case stx () [(_ prev . rest) (identifier? #'prev) - (internal-define-metafunction stx #'prev #'rest)])) + (internal-define-metafunction stx #'prev #'rest #f)])) - (define (internal-define-metafunction orig-stx prev-metafunction stx) + (define (internal-define-metafunction orig-stx prev-metafunction stx relation?) (syntax-case stx () [(lang . rest) (let ([syn-error-name (if prev-metafunction @@ -1140,7 +1146,8 @@ sc)) dsc `codom-side-conditions-rewritten - 'name))) + 'name + #,relation?))) (term-define-fn name name2)) 'disappeared-use (map syntax-local-introduce (syntax->list #'(original-names ...))))))))))))))] @@ -1260,7 +1267,7 @@ "expected a side-condition or where clause" (car stuff))])]))])))) -(define (build-metafunction lang patterns rhss old-cps old-rhss wrap dom-contract-pat codom-contract-pat name) +(define (build-metafunction lang patterns rhss old-cps old-rhss wrap dom-contract-pat codom-contract-pat name relation?) (let ([compiled-patterns (append old-cps (map (λ (pat) (compile-pattern lang pat #t)) patterns))] [dom-compiled-pattern (and dom-contract-pat (compile-pattern lang dom-contract-pat #f))] @@ -1284,7 +1291,11 @@ [num (- (length old-cps))]) (cond [(null? patterns) - (redex-error name "no clauses matched for ~s" `(,name . ,exp))] + (if relation? + (begin + (hash-set! cache exp #f) + #f) + (redex-error name "no clauses matched for ~s" `(,name . ,exp)))] [else (let ([pattern (car patterns)] [rhs (car rhss)]) @@ -1293,6 +1304,19 @@ [(not mtchs) (loop (cdr patterns) (cdr rhss) (+ num 1))] + [relation? + (let ([ans (ormap (λ (mtch) (rhs traced-metafunc (mtch-bindings mtch))) + mtchs)]) + (unless (match-pattern codom-compiled-pattern ans) + (redex-error name "codomain test failed for ~s, call was ~s" ans `(,name ,@exp))) + (cond + [ans + (hash-set! cache exp #t) + #t] + [else + (loop (cdr patterns) + (cdr rhss) + (+ num 1))]))] [(not (null? (cdr mtchs))) (redex-error name "~a matched ~s ~a different ways" (if (< num 0) @@ -1974,6 +1998,7 @@ define-metafunction define-metafunction/extension + define-relation (rename-out [metafunction-form metafunction]) metafunction? metafunction-proc diff --git a/collects/redex/private/tl-test.ss b/collects/redex/private/tl-test.ss index a1b345baf8..9f0748378e 100644 --- a/collects/redex/private/tl-test.ss +++ b/collects/redex/private/tl-test.ss @@ -611,9 +611,52 @@ (term (f 1))) (test (get-output-string sp) "|(f 1)\n|0\n"))) + +; +; +; +; +; +; +; ;; ;;; ;; ;; ;; ;; +; ;; ;;; ;; ;; ;;; ;; +; ;;;;; ;;;; ;;;;; ;; ;; ;;; ;;;; ;;;; ;;;; ;; ;;;; ;;;;; ;; ;;;; ;; ;;; +; ;;;;;; ;; ;; ;;;; ;; ;;;;;; ;; ;; ;;;; ;; ;; ;; ;; ;; ;;;; ;; ;;;;;; ;;;;;; +; ;;; ;; ;;;;;;;; ;; ;; ;; ;; ;;;;;;;;;;;; ;; ;;;;;;;; ;; ;;;; ;;; ;; ;;; ;;; ;; ;; +; ;;; ;; ;;; ;; ;; ;; ;; ;;; ;;;; ;; ;;; ;; ;;; ;; ;;; ;; ;;; ;;; ;; ;; +; ;;;;;; ;;; ;; ;; ;; ;; ;; ;;; ;; ;; ;;; ;; ;; ;;; ;; ;;;; ;; ;;;;;; ;; ;; +; ;;;;; ;;;; ;; ;; ;; ;; ;;;; ;; ;;;; ;; ;;;;;; ;;; ;; ;;;; ;; ;; +; +; +; -; -; + + (let () + (define-relation empty-language + [(<: any any) #t]) + + (test (term (<: 1 1)) #t) + (test (term (<: 1 2)) #f)) + + (let () + (define-relation empty-language + [(<: number_1 number_2) ,(< (term number_1) (term number_2))] + [(<: number_1 number_1) #t]) + + (test (term (<: 1 2)) #t) + (test (term (<: 1 1)) #t) + (test (term (<: 2 1)) #f)) + + (let () + (define-relation empty-language + [(<: number_1 ... number_2 number_3 ... number_2 number_4 ...) #t]) + + (test (term (<: 1 2 3 4)) #f) + (test (term (<: 1 1 2 3 4)) #t) + (test (term (<: 1 2 1 3 4)) #t) + (test (term (<: 1 2 3 1 4)) #t) + (test (term (<: 1 2 3 4 1)) #t)) + ; ;; ; ;; ; ; ; ; ; ; ; ;; ;; ;;; ;; ; ;; ;; ;;;; ;;;;; ;;; ;;; ;; ;; ;; ;; ;;; ; ;;; ;;;;; ;;; ;;; ;; ;; diff --git a/collects/redex/redex.scrbl b/collects/redex/redex.scrbl index 6ce31ca622..ed2eed7fbf 100644 --- a/collects/redex/redex.scrbl +++ b/collects/redex/redex.scrbl @@ -871,7 +871,7 @@ terminate (it does terminate if the only infinite reduction paths are cyclic). @scheme[reduction-relation]. A @scheme[with] form is an error elsewhere. } -@section{Metafunctions} +@section{Metafunctions and Relations} All of the exports in this section are provided both by @schememodname[redex/reduction-semantics] (which includes @@ -980,6 +980,38 @@ legtimate inputs according to @scheme[metafunction-name]'s contract, and @scheme[#f] otherwise. } +@defform/subs[#:literals () + (define-relation language-exp + [(name @#,ttpattern ...) @#,tttterm extras ...] + ...) + ([extras (side-condition scheme-expression) + (where tl-pat @#,tttterm)] + [tl-pat identifier (tl-pat-ele ...)] + [tl-pat-ele tl-pat (code:line tl-pat ... (code:comment "a literal ellipsis"))])]{ + +The @scheme[define-relation] form builds a relation on +sexpressions according to the pattern and right-hand-side +expressions. The first argument indicates the language used +to resolve non-terminals in the pattern expressions. Each of +the rhs-expressions is implicitly wrapped in @|tttterm|. + +If specified, the side-conditions are collected with +@scheme[and] and used as guards on the case being matched. The +argument to each side-condition should be a Scheme +expression, and the pattern variables in the @|ttpattern| are +bound in that expression. + +Unlike metafunctions, relations check all possible ways to match each +case, looking for a true result and if none of the clauses match, then +the result is @scheme[#f]. + +Note that relations are assumed to always return the same results +for the same inputs, and their results are cached, unless +@scheme[caching-enable?] is set to @scheme[#f]. Accordingly, if a +metafunction is called with the same inputs twice, then its body is +only evaluated a single time. +} + @defparam[current-traced-metafunctions traced-metafunctions (or/c 'all (listof symbol?))]{ Controls which metafunctions are currently being traced. If it is diff --git a/collects/redex/reduction-semantics.ss b/collects/redex/reduction-semantics.ss index 773dbaab19..f5de7804db 100644 --- a/collects/redex/reduction-semantics.ss +++ b/collects/redex/reduction-semantics.ss @@ -26,6 +26,7 @@ none? define-metafunction define-metafunction/extension + define-relation metafunction in-domain? caching-enabled?)