added 'boolean' pattern to Redex

closes PR 13330

collects/redex/examples/beginner.rkt

@@ -73,13 +73,13 @@ reflects the (broken) spec).
      non-struct-value)
   (non-struct-value number
                     list-value
-                    boolean
+                    bool
                     string
                     'x)
   (list-value empty
               (cons v list-value))
-  (boolean true
+  (bool true
-           false)
+        false)
   
   (maker (side-condition variable_1 (maker? (term variable_1))))
   

collects/redex/private/match-a-pattern.rkt

@@ -82,6 +82,7 @@ turns into this:
                   `natural
                   `integer
                   `real
+                  `boolean
                   `variable
                   `(variable-except ,var ...)
                   `(variable-prefix ,var)

collects/redex/private/matcher.rkt

@@ -247,6 +247,7 @@ See match-a-pattern.rkt for more details
       [`natural (void)]
       [`integer (void)]
       [`real (void)]
+      [`boolean (void)]
       [`variable (void)]
       [`(variable-except ,s ...) (void)]
       [`(variable-prefix ,s) (void)]
@@ -286,6 +287,7 @@ See match-a-pattern.rkt for more details
       [`natural pat]
       [`integer pat]
       [`real pat]
+      [`boolean pat]
       [`variable pat]
       [`(variable-except ,s ...) pat]
       [`(variable-prefix ,s) pat]
@@ -322,6 +324,7 @@ See match-a-pattern.rkt for more details
          [`natural #f]
          [`integer #f]
          [`real #f]
+         [`boolean #f]
          [`variable #f] 
          [`(variable-except ,vars ...) #f]
          [`(variable-prefix ,var) #f]
@@ -464,6 +467,7 @@ See match-a-pattern.rkt for more details
          [`natural untouched-pattern]
          [`integer untouched-pattern]
          [`real untouched-pattern]
+         [`boolean untouched-pattern]
          [`variable untouched-pattern] 
          [`(variable-except ,vars ...) untouched-pattern]
          [`(variable-prefix ,var) untouched-pattern]
@@ -569,6 +573,7 @@ See match-a-pattern.rkt for more details
       [`natural #f]
       [`integer #f]
       [`real #f]
+      [`boolean #f]
       [`variable #f]
       [`(variable-except ,vars ...) #f]
       [`(variable-prefix ,var) #f]
@@ -603,6 +608,7 @@ See match-a-pattern.rkt for more details
       [`natural #t]
       [`integer #t]
       [`real #t]
+      [`boolean #t]
       [`variable #t]
       [`(variable-except ,vars ...) #t]
       [`(variable-prefix ,prefix) #t]
@@ -764,6 +770,7 @@ See match-a-pattern.rkt for more details
       [`natural (simple-match exact-nonnegative-integer?)]
       [`integer (simple-match exact-integer?)]
       [`real (simple-match real?)]
+      [`boolean (simple-match boolean?)]
       [`variable (simple-match symbol?)]
       [`(variable-except ,vars ...)
        (simple-match
@@ -1816,6 +1823,7 @@ See match-a-pattern.rkt for more details
       [`natural ribs]
       [`integer ribs]
       [`real ribs]
+      [`boolean ribs]
       [`variable ribs]
       [`(variable-except ,vars ...) ribs]
       [`(variable-prefix ,vars) ribs]

collects/redex/private/pat-unify.rkt

@@ -24,7 +24,7 @@
          remove-empty-dqs)
 
 ;;
-;; atom := `any | `number | `string | `integer | `real | `variable | `variable-not-otherwise-mentioned
+;; atom := `any | `number | `string | `integer | `boolean | `real | `variable | `variable-not-otherwise-mentioned
 ;; var  := symbol?
 ;; nt   := symbol?
 ;; pat  := `(nt ,var) | `(list ,pat ...)  | atom | `(name ,var ,pat) | `(mismatch-name ,name ,pat)
@@ -50,7 +50,7 @@
 (struct env (eqs dqs) #:transparent)
 (define empty-env (env (hash) '()))
 
-(define predef-pats (set 'any 'number 'string 'integer 'real 'variable 'natural 'variable-not-otherwise-mentioned))
+(define predef-pats (set 'any 'number 'string 'integer 'boolean 'real 'variable 'natural 'variable-not-otherwise-mentioned))
 (define (predef-pat? a)
   (set-member? predef-pats a))
 (define (var? s)
@@ -67,6 +67,7 @@
        [`natural #t]
        [`integer #t]
        [`real #t]
+       [`boolean #t]
        [`variable #t]
        [`(variable-except ,vars ...) #f]
        [`(variable-prefix ,pfx) #f]
@@ -411,6 +412,17 @@
      (unify* u t e L)]
     [(`string (? string? s))
      s]
+    
+    ;; booleans
+    [(`boolean `boolean)
+     `boolean]
+    [(`string `boolean)
+     #f]
+    [(_ `boolean)
+     (unify* u t e L)]
+    [(`boolean (? boolean? b))
+     b]
+    
     ;; other
     [((? base-type? t) (? base-type? u))
      (and (equal? t u)
@@ -583,7 +595,7 @@
 
 (define (base-type? symbol)
   (member symbol
-          '(any number string natural integer real 
+          '(any number string natural integer real boolean
                 variable variable-not-otherwise-mentioned)))
 
 (define (lookup-pat id env)

collects/redex/private/rg.rkt

@@ -143,6 +143,9 @@
 (define (pick-real attempt [random generator-random])
   (pick-number attempt #:top-threshold real-threshold random))
 
+(define (pick-boolean attempt [random generator-random])
+  (zero? (random 2)))
+
 (define (pick-sequence-length size)
   (random-natural (expected-value->p size)))
 
@@ -286,6 +289,7 @@
           [`natural (values pat '())]
           [`integer (values pat '())]
           [`real (values pat '())]
+          [`boolean (values pat '())]
           [`variable (values pat '())]
           [`(variable-except ,vars ...) (values pat '())]
           [`(variable-prefix ,var) (values pat '())]
@@ -367,6 +371,7 @@
                 [`natural (generator/attempts (λ (a) ((next-natural-decision) a)))]
                 [`integer (generator/attempts (λ (a) ((next-integer-decision) a)))]
                 [`real (generator/attempts (λ (a) ((next-real-decision) a)))]
+                [`boolean (generator/attempts (λ (a) ((next-boolean-decision) a)))]
                 [`variable (generator/attempts (λ (a) ((next-variable-decision) lits a)))]
                 [`(variable-except ,vars ...)
                  (let ([g (recur 'variable)])
@@ -523,6 +528,7 @@
           [`natural (void)]
           [`integer (void)]
           [`real (void)]
+          [`boolean (void)]
           [`variable (void)]
           [`(variable-except ,vars ...) (void)]
           [`(variable-prefix ,var) (void)]
@@ -685,6 +691,7 @@
                        [`natural assignments]
                        [`integer assignments]
                        [`real assignments]
+                       [`boolean assignments]
                        [`variable assignments]
                        [`(variable-except ,vars ...) assignments]
                        [`(variable-prefix ,var) assignments]
@@ -740,6 +747,7 @@
    next-natural-decision
    next-integer-decision
    next-real-decision
+   next-boolean-decision
    next-non-terminal-decision
    next-sequence-decision
    next-any-decision
@@ -752,6 +760,7 @@
         (define (next-natural-decision) pick-natural)
         (define (next-integer-decision) pick-integer)
         (define (next-real-decision) pick-real)
+        (define (next-boolean-decision) pick-boolean)
         (define (next-non-terminal-decision) pick-nts)
         (define (next-sequence-decision) pick-sequence-length)
         (define (next-any-decision) pick-any)
@@ -770,7 +779,7 @@
          raise-gen-fail)
 
 (provide pick-from-list pick-sequence-length pick-nts
-         pick-char pick-var pick-string pick-any
+         pick-char pick-var pick-string pick-any pick-boolean
          pick-number pick-natural pick-integer pick-real
          unparse-pattern
          prepare-lang

collects/redex/scribblings/ref.scrbl

@@ -99,6 +99,7 @@ in the grammar are terminals.
             integer
             real
             string 
+            boolean
             variable 
             (variable-except <id> ...)
             (variable-prefix <id>)
@@ -162,6 +163,14 @@ were an implicit @pattech[name] @pattern) and match the portion
 before the underscore.
 }
 
+@item{The @defpattech[boolean] @pattern matches @racket[#true] and @racket[#false]
+(which are the same as @racket[#t] and @racket[#f], respectively).
+This @pattern may also be suffixed with an underscore and another
+identifier, in which case they bind the full name (as if it
+were an implicit @pattech[name] @pattern) and match the portion
+before the underscore.
+}
+
 @item{The @defpattech[variable] @pattern matches any symbol.
 This @pattern may also be suffixed with an underscore and another
 identifier, in which case they bind the full name (as if it

collects/redex/tests/matcher-test.rkt

@@ -52,6 +52,9 @@
     (test-empty 'real 'x #f)
     (test-empty 'real '() #f)
     (test-empty 'real 2+3i #f)
+    (test-empty 'boolean #t (list (make-test-mtch (make-bindings (list)) #t none)))
+    (test-empty 'boolean #f (list (make-test-mtch (make-bindings (list)) #f none)))
+    (test-empty 'boolean 'x #f)
     (test-empty '(name string string) "a" (list (make-test-mtch (make-bindings (list (make-bind 'string "a"))) "a" none)))
     (test-empty 'string 1 #f)
     (test-empty 'string '() #f)

collects/redex/tests/rg-test.rkt

@@ -1,4 +1,4 @@
-#lang scheme
+#lang racket
 
 (require "test-util.rkt"
          "../private/reduction-semantics.rkt"
@@ -117,6 +117,8 @@
 (test (pick-natural 224 (make-random 1/5)) 5)
 (test (pick-integer 900 (make-random 0 0 1/5)) -7)
 (test (pick-real 9000 (make-random 0 0 0 .5 1 1/8)) 11.0)
+(test (pick-boolean 9000 (make-random 1)) #f)
+(test (pick-boolean 9000 (make-random 0)) #t)
 
 (let* ([lits '("bcd" "cbd")])
   (test (pick-char 0 (make-random 0 0)) #\A)
@@ -166,6 +168,7 @@
                    #:nat [nat pick-natural]
                    #:int [int pick-integer]
                    #:real [real pick-real]
+                   #:bool [bool pick-boolean]
                    #:any [any pick-any]
                    #:seq [seq pick-sequence-length])
   (define-syntax decision
@@ -178,6 +181,7 @@
         (define next-natural-decision (decision nat))
         (define next-integer-decision (decision int))
         (define next-real-decision (decision real))
+        (define next-boolean-decision (decision bool))
         (define next-string-decision (decision str))
         (define next-any-decision (decision any))
         (define next-sequence-decision (decision seq))))
@@ -291,7 +295,8 @@
   (define-language L
     (n natural)
     (i integer)
-    (r real))
+    (r real)
+    (b boolean))
   (test (let ([n (generate-term L n 0 #:attempt-num 10000)])
           (and (integer? n)
                (exact? n)
@@ -1244,7 +1249,9 @@
    '(list (repeat (name x_1 (nt x)) ..._1 #f) (repeat (name x (nt x)) ..._2 #f) (repeat (name x_1 (nt x)) ..._2 #f))
    '((..._1 . ..._2)))
   (test-class-reassignments
-   '(list (repeat (name x_1 (nt x)) ..._1 #f) (repeat (name x_2 (nt x)) ..._2 #f) (repeat (list (name x_1 (nt x)) (name x_2 (nt x))) ..._3 #f))
+   '(list (repeat (name x_1 (nt x)) ..._1 #f)
+          (repeat (name x_2 (nt x)) ..._2 #f)
+          (repeat (list (name x_1 (nt x)) (name x_2 (nt x))) ..._3 #f))
    '((..._1 . ..._3) (..._2 . ..._3)))
   (test-class-reassignments
    '(list (repeat (list (repeat (name x_1 (nt x)) ..._1 #f)) ..._2 #f)

collects/redex/tests/unify-tests.rkt

@@ -316,6 +316,7 @@
   ['number 'number]
   ['real 'real]
   ['string 'string]
+  ['boolean 'boolean]
   ['variable 'variable]
   ['variable-not-otherwise-mentioned 'variable-not-otherwise-mentioned]
   [7 7]
@@ -331,6 +332,7 @@
   [7.5 7.5]
   ["a string" #f]
   ['string #f]
+  ['boolean #f]
   ['variable #f]
   ['variable-not-otherwise-mentioned #f]
   ['(list 1 2 3) #f]
@@ -343,6 +345,7 @@
   [7.5 #f]
   ["a string" #f]
   ['string #f]
+  ['boolean #f]
   ['variable #f]
   ['variable-not-otherwise-mentioned #f]
   ['(list 1 2 3) #f]
@@ -355,6 +358,7 @@
   [7.5 #f]
   ["a string" #f]
   ['string #f]
+  ['boolean #f]
   ['variable #f]
   ['variable-not-otherwise-mentioned #f]
   ['(list 1 2 3) #f]
@@ -367,6 +371,7 @@
   [7.5 7.5]
   ["a string" #f]
   ['string #f]
+  ['boolean #f]
   ['variable #f]
   ['variable-not-otherwise-mentioned #f]
   ['(list 1 2 3) #f]
@@ -377,6 +382,7 @@
  (['string 'string]
   ['variable #f]
   ['variable-not-otherwise-mentioned #f]
+  ['boolean #f]
   [7 #f]
   ["a string" "a string"]
   ['(list a b c) #f]
@@ -386,6 +392,7 @@
  'variable (hash)
  (['variable 'variable]
   ['x 'x]
+  ['boolean #f]
   ["a string" #f]
   ['(nt e) '(cstr (e) variable)]
   ['(list 1 2 3) #f]
@@ -395,6 +402,7 @@
  'variable-not-otherwise-mentioned (hash)
  (['variable-not-otherwise-mentioned 'variable-not-otherwise-mentioned]
   ['x 'x]
+  ['boolean #f]
   ["a string" #f]
   ['(nt e) '(cstr (e) variable-not-otherwise-mentioned)]
   ['(list 1 2 3) #f]
@@ -404,12 +412,20 @@
  '(nt e) (hash)
  ([5 '(cstr (e) 5)]
   ["a string" '(cstr (e) "a string")]
+  ['boolean '(cstr (e) boolean)]
   ['(nt q) '(cstr (e) (nt q))]))
 
+(unify-all/results/no-bindings
+ 'boolean (hash)
+ (['boolean 'boolean]
+  [`(list 1 2 3) #f]
+  ["abc" #f]))
+
 (unify-all/results
  '(name x any) (hash)
  ([5 `(name x ,(bound)) (hash (lvar 'x) 5)]
   [`(list 1 2 3) `(name x ,(bound)) (hash (lvar 'x) `(list 1 2 3))]
+  ['boolean `(name x ,(bound)) (hash (lvar 'x) `boolean)]
   ["a string" `(name x ,(bound)) (hash (lvar 'x) "a string")]))
 
 (unify-all/results/no-bindings
@@ -422,6 +438,7 @@
   ['natural 'natural]
   ['real 'real]
   ['string 'string]
+  ['boolean 'boolean]
   ['(list 1 2 3) '(list 1 2 3)]
   ['(mismatch-name y 5) 5]
   ['(nt e) '(cstr (e) any)]
@@ -463,6 +480,7 @@
   ['number `(cstr (e q) number) (make-hash)]
   ['real `(cstr (e q) real) (make-hash)]
   ['string `(cstr (e q) string) (make-hash)]
+  [`boolean `(cstr (e q) boolean) (make-hash)]
   ['variable `(cstr (e q) variable) (make-hash)]
   ['variable-not-otherwise-mentioned 
    `(cstr (e q) variable-not-otherwise-mentioned) (make-hash)]
@@ -481,6 +499,7 @@
   ['natural `(name x ,(bound)) (make-hash `((,(lvar 'x) . natural)))]
   ['real `(name x ,(bound)) (make-hash `((,(lvar 'x) . real)))]
   ['string `(name x ,(bound)) (make-hash `((,(lvar 'x) . string)))]
+  ['boolean `(name x ,(bound)) (make-hash `((,(lvar 'x) . boolean)))]
   ['variable `(name x ,(bound)) (make-hash `((,(lvar 'x) . variable)))]
   ['variable-not-otherwise-mentioned `(name x ,(bound)) (make-hash `((,(lvar 'x) . variable-not-otherwise-mentioned)))]
   ['(cstr (number) any) `(name x ,(bound)) (make-hash `((,(lvar 'x) . (cstr (number) any))))]

doc/release-notes/redex/HISTORY.txt

@@ -9,6 +9,8 @@ v5.3.2
   * added the option to use judgment-forms with only I mode
     positions in terms
 
+  * added 'boolean' as a new pattern
+
 v5.3.1
 
   * added optional #:lang keyword to term