#lang racket
;; =====================================================================
;; An example of using rewriting in symbolic computations.
;; Expansion of logical expressions to CNF an DNF.
;; =====================================================================
(require (planet "main.rkt" ("samsergey" "rewrite.plt" 1 0))
         rackunit)

;; declare this symbols to denote formal functions
(define-formal && || !)

;; =====================================================================
;; parsing infix notation
;; =====================================================================
(define infix->prefix
  (replace-all-repeated
   `(,a __1  <=> ,b __1) --> (&& `(,a => ,b) `(,b => ,a)) 
   `(,a __1  =>  ,b __1) --> (|| b (! a))       
   `(,a __1  ||  ,b __1) --> (|| a b)         
   `(,a __1  &&  ,b __1) --> (&& a b)                 
   `(,a) -->  a))

;; =====================================================================
;; simplification of expressions
;; =====================================================================
(define ordered?
  ; ordering of terms
  (replace
   (? symbol? x) (? symbol? y) --> (string<=? (symbol->string x) (symbol->string y)) 
   (? symbol?) (? pair?)  --> #t
   (cons a x) (cons a y) --> (ordered? x y) 
   (cons x _) (cons y _) --> (ordered? x y) 
   _ _ --> #f ))

(define simplify
  (replace-all-repeated
   ; exclusion of parenthesis
   `(,a) --> a 
   
   ; degenetare cases
   (|| a)  -->  a 
   (||)    --> 'F 
   (&& a)  -->  a 
   (&&)    --> 'T 
   
   ; negation propertyes
   (! (! a))  -->  a
   (! 'F)     --> 'T
   (! 'T)     --> 'F
   
   ; conjunction properties
   (&& _ ___ 'F _ ___)            --> 'F                   
   (&& x ___ 'T y ___)            --> `(&& ,@x ,@y)        
   (&& x ___ A y ___ A z ___)     --> `(&& ,@x ,A ,@y ,@z) 
   (&& _ ___ A _ ___ (! A) _ ___) --> 'F                   
   
   ; disjunction properties
   (|| _ ___ 'T _ ___)            --> 'T
   (|| x ___ 'F y ___)             --> `(|| ,@x ,@y)
   (|| x ___ A y ___ A z ___)     --> `(|| ,@x ,A ,@y ,@z)
   (|| _ ___ A _ ___ (! A) _ ___) --> 'T
   
   
   ; associativity
   (&& a ___ (&& b __1) c ___) --> `(&& ,@a ,@b ,@c) 
   (|| a ___ (|| b __1) c ___) --> `(|| ,@a ,@b ,@c)
   
   ; grouping of conjuncts
   (|| x ___ A y ___ (&& _ ___ A _ ___) z ___)     --> `(|| ,@x ,A ,@y ,@z)
   (|| x ___ A y ___ (&& p ___ (! A) q ___) z ___) --> `(|| ,@x ,A ,@y (&& ,@p ,@q) ,@z) 
   (|| x ___ (! A) y ___ (&& p ___ A q ___) z ___) --> `(|| ,@x (! ,A) ,@y (&& ,@p ,@q) ,@z) 
   
   ; grouping of disjuncts
   (&& x ___ A y ___ (|| _ ___ A _ ___) z ___) --> `(&& ,@x ,A ,@y ,@z) 
   (&& x ___ A y ___ (|| p ___ (! A) q ___) z ___) --> `(&& ,@x ,A ,@y (|| ,@p ,@q) ,@z) 
   (&& x ___ (! A) y ___ (|| p ___ A q ___) z ___) --> `(&& ,@x (! ,A) ,@y (|| ,@p ,@q) ,@z) 
   
   ; sorting terms to strength normalizing property of the rewriting system
   (cons op x) -->  (cons op (sort (map simplify x) ordered?))))

;; =====================================================================
;; Expansion to disjunctive normal form
;; =====================================================================
(define DNF
  (compose simplify
           (replace-all-repeated
            ; de Morgan's laws
            (! (|| a b __1))  --> (&& (! a) (! `(|| ,@b))) 
            (! (&& a b __1))  --> (|| (! a) (! `(&& ,@b))) 
            
            ; distributivity
            (&& a ___ (|| b bb __1) c ___) --> `(|| (&& ,@a ,b ,@c) 
                                                    (&& ,@a (|| ,@bb) ,@c)) 
            
            ; repeating of the expansion
            (cons op x) -->  (cons op (map DNF x)))))

;; =====================================================================
;; Expansion to conjunctive normal form
;; =====================================================================
(define CNF
  (compose simplify
           (replace-all-repeated
            ; de Morgan's laws
            (! (|| a b __1))  --> (&& (! a) (! `(|| ,@b))) 
            (! (&& a b __1))  --> (|| (! a) (! `(&& ,@b))) 
            
            ; distributivity
            (|| a ___ (&& b bb __1) c ___) --> `(&& (|| ,@a ,b ,@c) 
                                                    (|| ,@a (&& ,@bb) ,@c)) 
            
            ; repeating of the expansion
            (cons op x) --> (cons op (map CNF x)))))

(define expand (compose DNF CNF infix->prefix))

;; =====================================================================
;; Examples
;; =====================================================================

(check-equal? (expand '((A || B) && C))           '(|| (&& A C) (&& B C)))
(check-equal? (expand '((B || A) && (A || ! B)))  'A)
(check-equal? (expand '((A || B) && B))           'B)

(check-equal? (expand '((A => B) && A))      '(&& A B))
(check-equal? (expand '(A => ! A))           '(! A))

;; Tautology proving
(check-eq? 
 (expand '(A || ! A)) 
 'T)

(check-eq? 
 (expand '((A => B) <=> (! B => ! A)))
 'T)

(check-eq? 
 (expand '((! A => B) && (! A => ! B) => A))
 'T)

(check-eq? 
 (expand '((human => mortal) && (Socrates => human) => (Socrates => mortal))) 
 'T)

(check-eq? 
 (expand '((A || B) && (A => C) && (B => C) => C)) 
 'T)

(check-equal?
 (expand '(((P => Q) => P) => P))
 'T)

(check-equal? 
 (expand '((p || ! r) && s => (r && s => (p && q) || p))) 
 'T)

(check-equal?
 (expand '((A && B => C) <=> (A => (B => C))||(B => (A => C))))
 'T)

(check-equal? (expand '((A && B) => (A || B))) 'T)

(check-equal?
 (expand '(((A <=> B) <=> C) <=> (A <=> (B <=> C))))
 'T)

(check-equal?
 (expand '(((A || B => A || C) <=> (A || (B => C)))))
 'T)