#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))))

; define the compatible closure of bool-red
(define bool-red-compat  
  (compatible-closure bool-red bool-lang B))

; use compatible closure
(traces bool-red-compat
        (term (• (• f f) (• t t))))

; property: it seems that reducing a term always
; yields exactly one result, which is either t or f
(define (progress? t)
  (define final (apply-reduction-relation* bool-red-compat t))
  (and (equal? (length final) 1)
       (or (equal? (first final) (term t))
           (equal? (first final) (term f)))))

; let's random-check that it holds
(redex-check bool-lang B
             (progress? (term B)))