added a first attempt at define-relation

svn: r15171

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

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))
+ 
 ;                    ;;                         ;                                        ;;                    ;                 
 ;                     ;                 ;                                                 ;            ;                         
 ;   ;; ;;   ;;;    ;; ; ;;  ;;   ;;;;  ;;;;;  ;;;     ;;;  ;; ;;          ;; ;;   ;;;     ;     ;;;   ;;;;;  ;;;     ;;;  ;; ;;  

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

collects/redex/reduction-semantics.ss

@@ -26,6 +26,7 @@
          none?
          define-metafunction
          define-metafunction/extension
+         define-relation
          metafunction
          in-domain?
          caching-enabled?)