Allow caching to be disabled for individual metafunctions.

pkgs/redex-pkgs/redex-doc/redex/scribblings/ref.scrbl

@@ -1095,9 +1095,12 @@ reduce it further).
                ...)
              ([metafunction-contract (code:line) 
                                      (code:line id : @#,ttpattern-sequence ... -> range
-                                                maybe-pre-condition)]
+                                                maybe-pre-condition
+                                                maybe-cache-poison)]
               [maybe-pre-condition (code:line #:pre @#,tttterm)
                                    (code:line)]
+              [maybe-cache-poison (code:line #:cache-poison)
+                                  (code:line)]
               [range @#,ttpattern
                      (code:line @#,ttpattern or range)
                      (code:line @#,ttpattern ∨ range)

pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt

@@ -403,7 +403,8 @@
      (begin
        (unless (identifier? #'lang)
          (raise-syntax-error #f "expected an identifier in the language position" stx #'lang))
-       (define-values (contract-name dom-ctcs codom-contracts pats)
+       ;; cache-poison? is not necessary for relations
+       (define-values (contract-name dom-ctcs codom-contracts pats _)
          (split-out-contract stx (syntax-e #'def-form-id) #'body #t))
        (with-syntax* ([((name trms ...) rest ...) (car pats)]
                       [(mode-stx ...) #`(#:mode (name I))]
@@ -417,11 +418,37 @@
 ;; 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)
+;; returns:
+;; * contract-name
+;; * domain contracts
+;; * codomain contracts
+;; * clauses
+;; * cache-poison?
 (define-for-syntax (split-out-contract stx syn-error-name rest relation?)
+  ;; extracts keywords (currently just #:cache-poison) from the rest of the syntax list
+  ;; returns (values raw-clauses cache-poison?))
+  ;; (Note that after keywords, all that must be left is clauses, hence "raw-clauses")
+  ;; If you wish to add more keywords, make this a loop which goes that extracts them all,
+  ;; then construct a list/struct of keywords and associated arguments (if any) and return
+  ;; that instead of "cache-poison?".  Also change the uses of extract-keywords accordingly.
+  (define (extract-keywords more)
+    (cond
+      ;; first thing is #:cache-poison
+      [(and (not (empty? more))
+            (equal? (syntax-e (car more)) '#:cache-poison))
+       (values (cdr more) #t)]
+      [else
+       (values more #f)]))
   ;; initial test determines if a contract is specified or not
   (cond
+    ;; If we don't have a contract, it must be the case that we have at least one clause;
+    ;; this is guaranteed by the use of split-out-contract in reduction-semantics.rkt
+    ;; Also, in this case we have no keywords
     [(pair? (syntax-e (car (syntax->list rest))))
-     (values #f #f (list #'any) (check-clauses stx syn-error-name (syntax->list rest) relation?))]
+     (values #f #f (list #'any) (check-clauses stx syn-error-name (syntax->list rest) relation?) #f)]
+    ;; This is not a viable way of matching anything more than the one keyword we have at the moment
+    [(equal? (syntax-e (car (syntax->list rest))) '#:cache-poison)
+     (values #f #f (list #'any) (check-clauses stx syn-error-name (cdr (syntax->list rest)) relation?) #t)]
     [else
      (syntax-case rest ()
        [(id separator more ...)
@@ -434,55 +461,63 @@
                (raise-syntax-error syn-error-name 
                                    "expected clause definitions to follow domain contract"
                                    stx))
-             (values #'id contract (list #'any) (check-clauses stx syn-error-name clauses #t)))]
+             (values #'id contract (list #'any) (check-clauses stx syn-error-name clauses #t) #f))]
+          ;; We're not dealing with a relation
           [else
            (unless (eq? ': (syntax-e #'separator))
              (raise-syntax-error syn-error-name "expected a colon to follow the meta-function's name" stx #'separator))
+           ;; Loop collecting the domain patterns
            (let loop ([more (syntax->list #'(more ...))]
                       [dom-pats '()])
              (cond
                [(null? more)
                 (raise-syntax-error syn-error-name "expected an ->" stx)]
+               ;; Split domain from codomain by ->
                [(eq? (syntax-e (car more)) '->)
-                (define-values (raw-clauses rev-codomains pre-condition)
-                  (let loop ([prev (car more)]
-                             [more (cdr more)]
-                             [codomains '()])
+                (when (null? (cdr more))
+                  (raise-syntax-error syn-error-name "expected a range contract to follow" stx (car more)))
+                ;; Process codomains
+                (define-values (after-codomains rev-codomains)
+                  (let loop ([more (cddr more)]
+                             [codomains (list (cadr more))])
                     (cond
                       [(null? more)
-                       (raise-syntax-error syn-error-name "expected a range contract to follow" stx prev)]
+                       (values null codomains)]
+                      ;; first thing is OR (i.e. this is a union pattern)
+                      [(member (syntax-e (car more)) '(or ∨ ∪))
+                       ; TODO: make sure there is a pattern after the OR symbol
+                       (loop (cddr more) ;; skip this pattern and the OR
+                             (cons (cadr more) codomains))]
                       [else
-                       (define after-this-one (cdr more))
-                       (cond
-                         [(null? after-this-one)
-                          (values null (cons (car more) codomains) #t)]
-                         [else
-                          (define kwd (cadr more))
-                          (cond
-                            [(member (syntax-e kwd) '(or ∨ ∪))
-                             (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)
-                                     #t)])])])))
+                       (values more codomains)])))
+                ;; Process the #:pre keyword if it's there
+                (define-values (after-pre pre-condition)
+                  (cond
+                    ;; first thing is #:pre
+                    [(and (not (empty? after-codomains))
+                          (equal? (syntax-e (car after-codomains)) '#:pre))
+                     (when (null? (cddr after-codomains)) 
+                       (raise-syntax-error 'define-metafunction 
+                                           "expected an expression to follow #:pre keyword"
+                                           (car after-codomains)))
+                     (values (cddr after-codomains)
+                             (cadr after-codomains))]
+                    [else
+                     (values after-codomains #t)]))
+                ;; Anything after #:cache-poison (if it exists) must be a clause
+                (define-values (raw-clauses cache-poison?)
+                  (extract-keywords after-pre))
+                ;; Finally, clean up components for return from split-out-contract
                 (let ([doms (reverse dom-pats)]
                       [clauses (check-clauses stx syn-error-name raw-clauses relation?)])
                   (values #'id 
                           (if relation?
                               doms
                               #`(side-condition #,doms (term #,pre-condition)))
                           (reverse rev-codomains)
-                          clauses))]
+                          clauses
+                          cache-poison?))]
+               ;; Continue processing the contract
                [else
                 (loop (cdr more) (cons (car more) dom-pats))]))])]
        [_

pkgs/redex-pkgs/redex-lib/redex/private/reduction-semantics.rkt

@@ -1163,7 +1163,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-ctcs codom-contracts pats cache-poison?)
                       (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)))
@@ -1182,6 +1182,7 @@
                                                             name-predicate
                                                             #,dom-ctcs
                                                             #,codom-contracts
+                                                            #,cache-poison?
                                                             #,pats
                                                             #,syn-error-name))
                                    (term-define-fn name name2))])
@@ -1224,12 +1225,13 @@
 
 (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-ctcs codom-contracts cache-poison? pats syn-error-name)
      (let ([prev-metafunction (and (syntax-e #'prev-metafunction) #'prev-metafunction)]
            [dom-ctcs (syntax-e #'dom-ctcs)]
            [codom-contracts (syntax-e #'codom-contracts)]
            [pats (syntax-e #'pats)]
-           [syn-error-name (syntax-e #'syn-error-name)])
+           [syn-error-name (syntax-e #'syn-error-name)]
+           [cache-poison? (syntax-e #'cache-poison?)])
        (define lang-nts
          (definition-nts #'lang #'orig-stx syn-error-name))
        (with-syntax ([(((original-names lhs-clauses ...) raw-rhses ...) ...) pats]
@@ -1371,9 +1373,11 @@
                                    [else
                                     #`(memoize0
                                        (λ ()
-                                         (add-mf-dqs #,(check-pats #'(list gen-clause ...)))))])))
+                                         (add-mf-dqs #,(check-pats #'(list gen-clause ...)))))])
+                               #,cache-poison?))
                             #,(if dom-ctcs #'dsc #f)
                             `(codom-side-conditions-rewritten ...)
+                            #,cache-poison?
                             'name))))
                     'disappeared-use
                     (map syntax-local-introduce 
@@ -1533,7 +1537,7 @@
    (syntax->list extras)))
 
 
-(define (build-metafunction lang cases parent-cases wrap dom-contract-pat codom-contract-pats name)
+(define (build-metafunction lang cases parent-cases wrap dom-contract-pat codom-contract-pats cache-poison? name)
   (let* ([dom-compiled-pattern (and dom-contract-pat (compile-pattern lang dom-contract-pat #f))]
          [codom-compiled-patterns (map (λ (codom-contract-pat) (compile-pattern lang codom-contract-pat #f))
                                        codom-contract-pats)]
@@ -1547,7 +1551,8 @@
                [cache-entries 0]
                [not-in-cache (gensym)]
                [cache-result (λ (arg res case)
-                               (when (caching-enabled?)
+                               (when (and (caching-enabled?)
+                                          (not (unbox (caching-poisoned?))))
                                  (when (>= cache-entries cache-size)
                                    (set! cache (make-hash))
                                    (set! cache-entries 0))
@@ -1566,8 +1571,12 @@
                [metafunc
                 (λ (exp)
                   (let ([cache-ref (hash-ref cache exp not-in-cache)])
+                    (when cache-poison?
+                      (set-box! (caching-poisoned?) #t))
                     (cond
-                      [(or (not (caching-enabled?)) (eq? cache-ref not-in-cache))
+                      [(or (not (caching-enabled?))
+                           (unbox (caching-poisoned?))
+                           (eq? cache-ref not-in-cache))
                        (when dom-compiled-pattern
                          (unless (match-pattern dom-compiled-pattern exp)
                            (redex-error name
@@ -1631,6 +1640,7 @@
                                       (parameterize ([current-trace-print-args
                                                       (λ (name args kws kw-args level)
                                                         (if (or (not (caching-enabled?))
+                                                                (unbox (caching-poisoned?))
                                                                 (eq? not-in-cache (hash-ref cache exp not-in-cache)))
                                                             (display " ")
                                                             (display "c"))
@@ -1640,6 +1650,8 @@
                                                         (display " ")
                                                         (otr name results level))]
                                                      [print-as-expression #f])
+                                        (when cache-poison?
+                                          (set-box! (caching-poisoned?) #t))
                                         (trace-call name metafunc exp))
                                       (metafunc exp)))])
         traced-metafunc))

pkgs/redex-pkgs/redex-lib/redex/private/term-fn.rkt

@@ -22,6 +22,7 @@
          metafunc-proc-dom-pat
          metafunc-proc-cases
          metafunc-proc-gen-clauses
+         metafunc-proc-cache-poison?
          metafunc-proc?
          make-metafunc-proc
 
@@ -77,7 +78,7 @@
                               variable-not-otherwise-mentioned hole symbol))
 
 (define-values (struct:metafunc-proc make-metafunc-proc metafunc-proc? metafunc-proc-ref metafunc-proc-set!)
-  (make-struct-type 'metafunc-proc #f 10 0 #f null (current-inspector) 0))
+  (make-struct-type 'metafunc-proc #f 11 0 #f null (current-inspector) 0))
 (define metafunc-proc-clause-names (make-struct-field-accessor metafunc-proc-ref 1))
 (define metafunc-proc-pict-info (make-struct-field-accessor metafunc-proc-ref 2))
 (define metafunc-proc-lang (make-struct-field-accessor metafunc-proc-ref 3))
@@ -87,6 +88,7 @@
 (define metafunc-proc-dom-pat (make-struct-field-accessor metafunc-proc-ref 7))
 (define metafunc-proc-cases (make-struct-field-accessor metafunc-proc-ref 8))
 (define metafunc-proc-gen-clauses (make-struct-field-accessor metafunc-proc-ref 9))
+(define metafunc-proc-cache-poison? (make-struct-field-accessor metafunc-proc-ref 10))
 
 
 (define (build-disappeared-use id-stx-table nt id-stx)

pkgs/redex-pkgs/redex-lib/redex/private/term.rkt

@@ -8,12 +8,13 @@
                      (only-in racket/list flatten)
                      "keyword-macros.rkt"
                      "matcher.rkt")
+         "term-fn.rkt"
          syntax/datum
          "error.rkt"
          "lang-struct.rkt"
          "matcher.rkt")
 
-(provide term term-let define-term
+(provide term term-let define-term caching-poisoned? term-nested?
          hole in-hole
          term-let/error-name term-let-fn term-define-fn
          (for-syntax term-rewrite
@@ -81,14 +82,28 @@
 (define-syntax (mf-apply stx)
   (syntax-case stx ()
     [(_ mf)
-     #'(λ (x) (mf x))]))
+     #'(λ (x) 
+         (begin
+           ;; The test macro used in redex-test causes mf-apply to be used on an ordinary procedure
+           ;; (not a metafunction), so we must check whether it is a metafunction before checking
+           ;; whether it poisons the cache.
+           (when (and (metafunc-proc? mf)
+                      (metafunc-proc-cache-poison? mf))
+             (set-box! (caching-poisoned?) #t))
+           (let [(ans (mf x))]
+             ans)))]))
 
 (define-syntax (jf-apply stx)
   (syntax-case stx ()
     [(_ jf)
      (judgment-form-id? #'jf)
      (judgment-form-term-proc (syntax-local-value #'jf (λ () #f)))]))
 
+;; Track whether a cache-poisoning metafunction has been used during evaluation of the current term
+(define caching-poisoned? (make-parameter (box #f)))
+;; Track whether the current term expression is nested inside another term expression
+(define term-nested? (make-parameter #f))
+
 (define-syntax (mf-map stx)
   (syntax-case stx ()
     [(_ inner-apps)
@@ -278,8 +293,18 @@
                  [(null? bs) (syntax t)]
                  [else (with-syntax ([rec (loop (cdr bs))]
                                      [fst (car bs)])
-                         (syntax (with-datum (fst)
-                                             rec)))]))))]))
+                         (syntax
+                          ;; If this is the outermost term, we reset the cache to non-poisoned and
+                          ;; remember that any terms we encounter during this are nested terms.
+                          (if (not (term-nested?))
+                              (parameterize [(caching-poisoned? (box #f))
+                                             (term-nested? #t)]
+                                (with-datum (fst)
+                                            rec))
+                              ;; Otherwise, this is a nested term. It inherits the poison tracking
+                              ;; from its enclosing term, so we do not need to re-parameterize.
+                              (with-datum (fst)
+                                          rec))))]))))]))
 
 (define-for-syntax (term-temp->pat t-t names)
   (syntax-case t-t (term-template)

pkgs/redex-pkgs/redex-test/redex/tests/cache-poisoning-test.rkt

@@ -0,0 +1,50 @@
+#lang racket/base
+(require rackunit
+         redex)
+
+(define-language L
+  (e integer)
+  (x variable-not-otherwise-mentioned))
+
+(define-metafunction L
+  [(dec e) ,(sub1 (term e))])
+
+(define-metafunction L
+  inc : e -> e
+  [(inc e) ,(add1 (term e))])
+
+(define-metafunction L
+  foo : any_0 -> x
+  #:pre ,(> (term any_0) 0)
+  [(foo any) ,(gensym)])
+
+(define-metafunction L
+  bar : any_1 -> any
+  #:cache-poison
+  [(bar e) ,(gensym)])
+
+(define-metafunction L
+  [(baz e) (foo e)
+           (side-condition (> (term e) 0))]
+  [(baz any) (bar any)])
+
+
+;; These should be equal (foo caches)
+(define foo1 (term (foo 3)))
+(define foo2 (term (foo 3)))
+(check-equal? foo1 foo2)
+
+;; These should not be equal (bar does not cache)
+(define bar1 (term (bar -3)))
+(define bar2 (term (bar -3)))
+(check-not-equal? bar1 bar2)
+
+;; These should be equal (baz will only call foo)
+(define baz1 (term (baz 4)))
+(define baz2 (term (baz 4)))
+(check-equal? baz1 baz2)
+
+;; These should not be equal (baz will call bar, which does not cache)
+(define baz3 (term (baz -4)))
+(define baz4 (term (baz -4)))
+(check-not-equal? baz3 baz4)