From ad308e32f1652cf4a12b4fc2e1c389cafd654de9 Mon Sep 17 00:00:00 2001
From: Casey Klein <clklein@racket-lang.org>
Date: Wed, 21 Jul 2010 08:34:55 -0500
Subject: [PATCH] Removes undocumented, unmaintained random testing form

---
 collects/redex/private/rg.rkt          | 33 +---------------
 collects/redex/reduction-semantics.rkt |  1 -
 collects/redex/tests/rg-test.rkt       | 53 --------------------------
 3 files changed, 2 insertions(+), 85 deletions(-)

diff --git a/collects/redex/private/rg.rkt b/collects/redex/private/rg.rkt
index f130453423..e65d0eb2a4 100644
--- a/collects/redex/private/rg.rkt
+++ b/collects/redex/private/rg.rkt
@@ -775,14 +775,14 @@
                           (and print? show)
                           fix
                           #:term-match term-match))
-                     #`(check-prop
+                     #`(check-one
                         #,(term-generator #'lang #'pat 'redex-check)
                         property att ret (and print? show) fix (and fix term-match)))))))))]))
 
 (define (format-attempts a)
   (format "~a attempt~a" a (if (= 1 a) "" "s")))
 
-(define (check-prop generator property attempts retries show term-fix term-match) 
+(define (check-one generator property attempts retries show term-fix term-match) 
   (let ([c (check generator property attempts retries show 
                   #:term-fix term-fix
                   #:term-match term-match)])
@@ -845,34 +845,6 @@
                       (pretty-print term (current-output-port)))
                     (make-counterexample term)))))))))
 
-(define-syntax (check-metafunction-contract stx)
-  (syntax-case stx ()
-    [(_ name . kw-args)
-     (identifier? #'name)
-     (with-syntax ([m (metafunc/err #'name stx)]
-                   [(attempts retries)
-                    (parse-kw-args `((#:attempts . ,#'default-check-attempts)
-                                     (#:retries . ,#'default-retries))
-                                   (syntax kw-args)
-                                   stx)]
-                   [show (show-message stx)])
-       (syntax/loc stx 
-        (let ([lang (metafunc-proc-lang m)]
-              [dom (metafunc-proc-dom-pat m)]
-              [att (assert-nat 'check-metafunction-contract attempts)])
-          (check-prop 
-           ((compile lang 'check-metafunction-contract)
-            (if dom dom '(any (... ...))))
-           (term-prop
-            (λ (t) 
-              (with-handlers ([exn:fail:redex? (λ (_) #f)])
-                (begin (term (name ,@t)) #t))))
-           att
-           retries
-           show
-           #f
-           #f))))]))
-
 (define (check-lhs-pats lang mf/rr prop attempts retries what show term-fix
                         #:term-match [term-match #f])
   (let ([lang-gen (compile lang what)])
@@ -999,7 +971,6 @@
 
 (provide redex-check
          generate-term
-         check-metafunction-contract
          check-reduction-relation
          check-metafunction
          exn:fail:redex:generation-failure?)
diff --git a/collects/redex/reduction-semantics.rkt b/collects/redex/reduction-semantics.rkt
index e58415cf84..78f97c49c7 100644
--- a/collects/redex/reduction-semantics.rkt
+++ b/collects/redex/reduction-semantics.rkt
@@ -48,7 +48,6 @@
 (provide redex-check
          generate-term
          check-metafunction
-         check-metafunction-contract
          check-reduction-relation
          exn:fail:redex:generation-failure?
          (struct-out exn:fail:redex:test)
diff --git a/collects/redex/tests/rg-test.rkt b/collects/redex/tests/rg-test.rkt
index 719729a236..578eb71730 100644
--- a/collects/redex/tests/rg-test.rkt
+++ b/collects/redex/tests/rg-test.rkt
@@ -747,59 +747,6 @@
        (--> (side-condition any #f) any impossible)
        #rx"^redex-check: unable to generate LHS of impossible in 42"))))
 
-;; check-metafunction-contract
-(let ()
-  (define-language L
-    (C hole (1 hole)))
-  
-  (define-metafunction L
-    f : (side-condition number_1 (odd? (term number_1))) -> number
-    [(f 1) 1]
-    [(f 3) 'NaN])
-  
-  (define-metafunction L
-    g : (1 1) -> C
-    [(g (in-hole C any)) C])
-  
-  (define-metafunction L
-    h : number -> number
-    [(h any) any])
-  
-  (define-metafunction L
-    [(i any ...) (any ...)])
-  
-  (define-metafunction L
-    j : (side-condition any #f) -> any
-    [(j any ...) (any ...)])
-  
-  ;; Dom(f) < Ctc(f)
-  (test (output 
-         (λ () 
-           (parameterize ([generation-decisions 
-                           (decisions #:num (list (λ _ 2) (λ _ 5)))])
-             (check-metafunction-contract f))))
-        #rx"check-metafunction-contract:.*counterexample found after 1 attempt:\n\\(5\\)\n")
-  ;; Rng(f) > Codom(f)
-  (test (output
-         (λ () 
-           (parameterize ([generation-decisions
-                           (decisions #:num (list (λ _ 3)))])
-             (check-metafunction-contract f))))
-        #rx"counterexample found after 1 attempt:\n\\(3\\)\n")
-  ;; LHS matches multiple ways
-  (test (output (λ () (check-metafunction-contract g)))
-        #rx"counterexample found after 1 attempt:\n\\(\\(1 1\\)\\)\n")
-  ;; OK -- generated from Dom(h)
-  (test (output (λ () (check-metafunction-contract h))) #rx"no counterexamples")
-  ;; OK -- generated from pattern (any ...)
-  (test (output (λ () (check-metafunction-contract i #:attempts 5))) #rx"no counterexamples")
-  
-  ;; Unable to generate domain
-  (test (raised-exn-msg
-         exn:fail:redex:generation-failure?
-         (check-metafunction-contract j #:attempts 1 #:retries 42))
-        #rx"^check-metafunction-contract: unable .* in 42"))
-
 ;; check-reduction-relation
 (let ()
   (define-language L