#lang racket
(require redex)

;;;; definition with contexts
; syntax of the language
(define-language bool-lang-c
  [B t 
     f 
     (• B B)]
  [C (• C B)
     (• B C)
     hole]
  ;; contexts specialized for left hand-side
  [E (• E B)
     hole])

(define bool-comp
  (reduction-relation
   bool-lang-c
   (--> (in-hole C (• t B))
        (in-hole C t))
   (--> (in-hole C (• f B))
        (in-hole C B))))

; standard reduction relation: holes only on the left hand-side
; (makes evaluation steps deterministic)
(define bool-std
  (reduction-relation
   bool-lang-c
   (--> (in-hole E (• t B))
        (in-hole E t))
   (--> (in-hole E (• f B))
        (in-hole E B))))


#;(traces bool-comp 
          (term (• (• f f) (• t t))))
#;(traces bool-std 
          (term (• (• f f) (• t t))))

;; theorem: compatible reduction and standard reduction coincide
(define (same-answer? t)
  (define compat-answers 
    (apply-reduction-relation* bool-comp t))
  (define std-answers
    (apply-reduction-relation* bool-std t))
  (and (equal? (length compat-answers) 1)
       (equal? (length std-answers) 1)
       (equal? (first compat-answers)
               (first std-answers))))

(redex-check bool-lang-c B (same-answer? (term B)))

;; try to introduce (subtle) bugs in the definitions and find them with redex-check!

;; alternative definition of contextual reduction
;; - start with the notion of reduction (here 'r')
;; - define reduction relation (-->) in terms of r and contexts
(define bool-comp-2
  (reduction-relation
   bool-lang-c
   (r (• t B) t •-t)
   (r (• f B) B •-f)
   with
   [(--> (in-hole C B_1) (in-hole C B_2))
    (r B_1 B_2)]))