#lang racket
(require (planet "main.rkt" ("samsergey" "rewrite.plt" 1 0))
         rackunit)

;;;====================================================
;;; Definition of Peano axioms
;;;====================================================

;; Declare these functions to be formal
(define-formal 1+ Add Mul Sub Div)

;; Peano axioms
(define//. Peano
  ; definition of Peano numerals
  0 --> 0
  (? number? n) --> (1+ (- n 1))
  
  ; addition
  (Add x 0) --> x
  (Add x (1+ y)) --> (1+ (Add x y))
  
  ; multiplication
  (Mul _ 0) --> 0
  (Mul x (1+ y)) --> (Add x (Mul x y))
  
  ; subtitution
  (Sub x 0) --> x
  (Sub 0 _) --> 0
  (Sub (1+ x) (1+ y)) --> (Sub x y)
  
  ; division (quotient ceiling)
  (Div 0 _) --> 0
  (Div (1+ x) (1+ y)) --> (1+ (Div (Sub x y) (1+ y))))

(check-equal? (Peano 1) (1+ 0))
(check-equal? (Peano 3) (1+ (1+ (1+ 0))))
(check-equal? (Peano (Add 2 3)) (1+ (1+ (1+ (1+ (1+ 0))))))

;; interpretation of Peano numerals as regular numbers
(define//. interprete
  (1+ (? number? n)) --> (+ 1 n))

(check = (interprete 0) 0)
(check = (interprete (1+ 0)) 1)
(check = (interprete (1+ (1+ (1+ 0)))) 3)

;; Calculation in terms of Peano numerals
(define calculate (compose interprete Peano))

(check = (calculate (Add 2 2)) 4)
(check = (calculate (Add 3 0)) 3)
(check = (calculate (Add 0 0)) 0)
(check = (calculate (Mul 3 2)) 6)
(check = (calculate (Mul 2 3)) 6)
(check = (calculate (Mul 0 3)) 0)
(check = (calculate (Sub 2 2)) 0)
(check = (calculate (Sub 3 2)) 1)
(check = (calculate (Sub 1 2)) 0)
(check = (calculate (Div 4 2)) 2)
(check = (calculate (Div 2 4)) 1)
(check = (calculate (Div 15 3)) 5)
(check = (calculate (Div 15 4)) 4)
(check = (calculate (Div 16 3)) 6)
(check = (calculate (Mul (Add 2 3) (Sub 4 2))) 10)