add a #:pre keyword to define-metafunction

The keyword allows the specification of contracts
that relate different arguments

closes PR 13617

collects/redex/private/judgment-form.rkt

@@ -393,13 +393,15 @@
        (with-syntax* ([((name trms ...) rest ...) (car pats)]
                       [(mode-stx ...) #`(#:mode (name I))]
                       [(ctc-stx ...) (if dom-ctcs 
-                                         (with-syntax ([(d-ctc ...) dom-ctcs])
+                                         #`(#:contract (name #,dom-ctcs)) 
-                                           #`(#:contract (name (d-ctc ...)))) 
                                          #'())]
                       [(clauses ...) pats]
                       [new-body #`(mode-stx ... ctc-stx ... clauses ...)])
                      (do-extended-judgment-form #'lang (syntax-e #'def-form-id) #'new-body #f stx #t)))]))
 
+;; if relation? is true, then the contract is a list of redex patterns
+;; if relation? is false, then the contract is a single redex pattern
+;;   (meant to match the actual argument as a sequence)
 (define-for-syntax (split-out-contract stx syn-error-name rest relation?)
   ;; initial test determines if a contract is specified or not
   (cond
@@ -427,7 +429,7 @@
                [(null? more)
                 (raise-syntax-error syn-error-name "expected an ->" stx)]
                [(eq? (syntax-e (car more)) '->)
-                (define-values (raw-clauses rev-codomains)
+                (define-values (raw-clauses rev-codomains pre-condition)
                   (let loop ([prev (car more)]
                              [more (cdr more)]
                              [codomains '()])
@@ -438,7 +440,7 @@
                        (define after-this-one (cdr more))
                        (cond
                          [(null? after-this-one)
-                          (values null (cons (car more) codomains))]
+                          (values null (cons (car more) codomains) #t)]
                          [else
                           (define kwd (cadr more))
                           (cond
@@ -446,12 +448,26 @@
                              (loop kwd 
                                    (cddr more)
                                    (cons (car more) codomains))]
+                            [(and (not relation?) (equal? (syntax-e kwd) '#:pre))
+                             (when (null? (cddr more)) 
+                               (raise-syntax-error 'define-metafunction 
+                                                   "expected an expression to follow #:pre keyword"
+                                                   kwd))
+                             (values (cdddr more)
+                                     (cons (car more) codomains)
+                                     (caddr more))]
                             [else
                              (values (cdr more)
-                                     (cons (car more) codomains))])])])))
+                                     (cons (car more) codomains)
+                                     #t)])])])))
                 (let ([doms (reverse dom-pats)]
                       [clauses (check-clauses stx syn-error-name raw-clauses relation?)])
-                  (values #'id doms (reverse rev-codomains) clauses))]
+                  (values #'id 
+                          (if relation?
+                              doms
+                              #`(side-condition #,doms (term #,pre-condition)))
+                          (reverse rev-codomains)
+                          clauses))]
                [else
                 (loop (cdr more) (cons (car more) dom-pats))]))])]
        [_

collects/redex/private/reduction-semantics.rkt

@@ -1143,7 +1143,7 @@
           prev-metafunction
           (λ ()
             (raise-syntax-error syn-error-name "expected a previously defined metafunction" orig-stx prev-metafunction))))
-       (let*-values ([(contract-name dom-ctcs codom-contracts pats)
+       (let*-values ([(contract-name dom-ctc codom-contracts pats)
                       (split-out-contract orig-stx syn-error-name #'rest #f)]
                      [(name _) (defined-name (list contract-name) pats orig-stx)])
          (when (and prev-metafunction (eq? (syntax-e #'name) (syntax-e prev-metafunction)))
@@ -1160,7 +1160,7 @@
                                                             #,prev-metafunction
                                                             name
                                                             name-predicate
-                                                            #,dom-ctcs
+                                                            #,dom-ctc
                                                             #,codom-contracts
                                                             #,pats
                                                             #,syn-error-name))
@@ -1204,9 +1204,9 @@
 
 (define-syntax (generate-metafunction stx)
   (syntax-case stx ()
-    [(_ orig-stx lang prev-metafunction name name-predicate dom-ctcs codom-contracts pats syn-error-name)
+    [(_ orig-stx lang prev-metafunction name name-predicate dom-ctc codom-contracts pats syn-error-name)
      (let ([prev-metafunction (and (syntax-e #'prev-metafunction) #'prev-metafunction)]
-           [dom-ctcs (syntax-e #'dom-ctcs)]
+           [dom-ctc (syntax-e #'dom-ctc)]
            [codom-contracts (syntax-e #'codom-contracts)]
            [pats (syntax-e #'pats)]
            [syn-error-name (syntax-e #'syn-error-name)])
@@ -1271,12 +1271,12 @@
                                                (syntax-column lhs)))
                                      pats)]
                                [(dom-side-conditions-rewritten dom-names dom-names/ellipses)
-                                (if dom-ctcs
+                                (if dom-ctc
                                     (rewrite-side-conditions/check-errs
                                      lang-nts
                                      syn-error-name
                                      #f
-                                     dom-ctcs)
+                                     dom-ctc)
                                     #'(any () ()))]
                                [((codom-side-conditions-rewritten codom-names codom-names/ellipses) ...)
                                 (map (λ (codom-contract)
@@ -1356,7 +1356,7 @@
                                      #`(extend-lhs-pats #,(term-fn-get-id (syntax-local-value prev-metafunction))
                                                         new-lhs-pats)
                                      #`new-lhs-pats)))
-                            #,(if dom-ctcs #'dsc #f)
+                            #,(if dom-ctc #'dsc #f)
                             `(codom-side-conditions-rewritten ...)
                             'name))))
                     'disappeared-use

collects/redex/private/rewrite-side-conditions.rkt

@@ -107,7 +107,9 @@
                                           (if line
                                               (format "~a:?" line)
                                               (syntax-position stx)))))])
-               (values (syntax/loc term
+               (values (syntax/loc (if (syntax? term)
+                                       term
+                                       (datum->syntax #f 'whatever #f))
                          (side-condition
                           pre-term
                           ,(lambda (bindings)

collects/redex/scribblings/ref.scrbl

@@ -1088,7 +1088,10 @@ reduce it further).
                [(name @#,ttpattern ...) @#,tttterm metafunction-extras ...] 
                ...)
              ([metafunction-contract (code:line) 
-                                     (code:line id : @#,ttpattern-sequence ... -> range)]
+                                     (code:line id : @#,ttpattern-sequence ... -> range
+                                                maybe-pre-condition)]
+              [maybe-pre-condition (code:line #:pre @#,tttterm)
+                                   (code:line)]
               [range @#,ttpattern
                      (code:line @#,ttpattern or range)
                      (code:line @#,ttpattern ∨ range)
@@ -1107,14 +1110,21 @@ 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|. 
 
+The contract, if present, is matched against every input to
+the metafunction and, if the match fails, an exception is raised.
+If present, the term inside the @racket[maybe-pre-condition] is evaluated
+after a successful match to the input pattern in the contract (with
+any variables from the input contract bound). If
+it returns @racket[#f], then the input contract is considered to not
+have matched and an error is also raised.
+
 The @racket[side-condition], @racket[hidden-side-condition],
 @racket[where], and @racket[where/hidden] clauses behave as
 in the @racket[reduction-relation] form.
 
-Raises an exception recognized by @racket[exn:fail:redex?] if
+The resulting metafunction raises an exception recognized by @racket[exn:fail:redex?] if
-no clauses match, if one of the clauses matches multiple ways
+no clauses match or if one of the clauses matches multiple ways
-(and that leads to different results for the different matches),
+(and that leads to different results for the different matches).
-or if the contract is violated.
 
 The @racket[side-condition] extra is evaluated after a successful match
 to the corresponding argument pattern. If it returns @racket[#f],
@@ -1227,7 +1237,7 @@ and @racket[#f] otherwise.
                rule rule ...)
              ([mode-spec (code:line #:mode (form-id pos-use ...))]
               [contract-spec (code:line) 
-                             (code:line #:contract (form-id @#,ttpattern ...))]
+                             (code:line #:contract (form-id @#,ttpattern-sequence ...))]
               [pos-use I
                        O]
               [rule [premise

collects/redex/tests/tl-test.rkt

@@ -1133,6 +1133,21 @@
                  x)
           '(2 1)))
   
+  (let ()
+    (define-metafunction empty-language
+      [(same any_1 any_1) #t]
+      [(same any_1 any_2) #f])
+    
+    (define-metafunction empty-language
+      m : any_1 any_2 -> any_3
+      #:pre (same any_1 any_2)
+      [(m any_x any_y) any_x])
+    
+    (test (term (m 1 1)) 1)
+    (test (with-handlers ((exn:fail:redex? exn-message))
+            (term (m 1 2)))
+          #rx"is not in my domain"))
+  
   (let ()
     (define-language L
       (n z (s n)))

doc/release-notes/redex/HISTORY.txt

@@ -11,6 +11,10 @@ v5.3.4
     pattern is more general than the contract would allow, that those
     terms are discarded instead of used as inputs to the predicate.
 
+  * Added the #:pre keyword to define-metafunction. It allows
+    contracts that have to relate different arguments to a
+    metafunction.
+
 v5.3.3
 
 No changes