#lang racket

; the magic toolbox
(require redex)

; syntax of the language
(define-language bool-lang
  [B t 
     f 
     (• B B)])

; some terms
(define B1 (term t))
(define B2 (term f))
(define B3 (term (• t f)))
(define B4 (term (• ,B2 ,B3)))

; examples of redex-match
(redex-match bool-lang B
             (term f))

(redex-match bool-lang B
             (term (• t t)))

(redex-match bool-lang (• t B) 
             (term (• t t)))

(redex-match bool-lang (• t B) 
             (term f))


; core reduction relation 
(define bool-red
  (reduction-relation 
   bool-lang
   (--> (• t B) t •-t)
   (--> (• f B) B •-f)))

; apply-reduction-relation
(apply-reduction-relation bool-red
                          (term (• t t)))

(apply-reduction-relation bool-red
                          (term (• f (• t t))))

; apply-reduction-relation*
(apply-reduction-relation* bool-red
                           (term (• f (• t t))))


; test-->
(test--> bool-red
         (term (• f (• t t)))
         (term (• t t)))

; test-->>
(test-->> bool-red
         (term (• f (• t t)))
         (term t))

(test-results)

; traces
#;(traces bool-red 
        (term (• f (• t f))))

; does not reduce!
#;(traces bool-red 
        (term (• (• f f) (• t t))))

; use compatible closure of bool-red
#;(traces (compatible-closure bool-red bool-lang B)
        (term (• (• f f) (• t t))))