#lang racket/base

(require rackunit
         racket/math
         racket/set
         racket/flonum
         "mathsymbols.rkt")

;; Numerical operations
(check-true (≤ 1 1))
(check-true (≤ 1 2))
(check-false (≤ 2 1))

(check-true (≥ 1 1))
(check-true (≥ 2 1))
(check-false (≥ 1 2))

(check-true (≠ 1 2))
(check-false (≠ 2 2))

(check-eqv? (√ 4) 2)

;; Famous numbers
(check-eqv? π pi)
(check-true (> ∞ 1e12))
(check-true (< -∞ -1e12))

;; Logical operations
(check-true (∧ #t #t))
(check-false (∧ #t #f #t))
(check-false (∨ #f #f))
(check-true (∨ #f #t #f))

(check-true (¬ #f))
(check-false (¬ 'foo))

;; Implications: shortcutting where possible.
(check-false (⇒ #t #f))
(check-true (⇒ #f (error "shouldn't get here")))

(check-false (⇐ #f #t))
(check-true (⇐ #t (error "shouldn't get here")))

(check-true (⇔ 'foo 'bar)) ; both are TRUE considered as booleans
(check-false (⇔ 'foo #f))
(check-true (⇔ #f #f))

;; Function operations
(check-eqv? ((∘ √ -) 4) +2i)
(check-eqv? ((∘ - √) 4) -2)

;; Set operations
(check-true (∈ 2 (set 1 2 3)))
(check-false (∈ 2 ∅))

(check-equal? (∪ (set 1 2) (set 2 3)) (set 1 2 3))
(check-equal? (∩ (set 1 2) (set 2 3)) (set 2))
(check-true (⊆ (set 1 2) (set 1 2 3)))
(check-false (⊇ (set 1 2) (set 1 2 3)))
(check-true (⊆ ∅ ∅))
(check-false (⊂ ∅ ∅))


;; Some well-known comprehensions.
(check-false (∀ ((i (in-range 10))) (even? i)))
(check-true (∃ ((i (in-range 10))) (even? i)))
(check-true (∀ ((i (in-range 10)) (j (in-range 10))) (= i j)))
(check-false (∀* ((i (in-range 10)) (j (in-range 10))) (= i j)))
(check-true (∃* ((i (in-range 10)) (j (in-range 10))) (≠ i j)))

;; New comprehensions.
(check-eqv? (Σ ((i (in-range 10))) i) 45)
(check-eqv? (Σ ((i (in-range 3)) (j (in-range 3))) (+ i j)) 6)
(check-eqv? (Σ* ((i (in-range 3)) (j (in-range 3))) (+ i j)) 18)

(check-eqv? (Π ((i (in-range 1 3)) (j (in-range 1 3))) (+ i j)) 8)
(check-eqv? (Π* ((i (in-range 1 3)) (j (in-range 1 3))) (+ i j)) 72)

;; Flonum variants.
(check-eqv? (flΣ ((i (in-range 10))) (->fl i)) 45.0)
(check-eqv? (flΣ ((i (in-range 3)) (j (in-range 3))) (->fl (+ i j))) 6.0)
(check-eqv? (flΣ* ((i (in-range 3)) (j (in-range 3))) (->fl (+ i j))) 18.0)

(check-eqv? (flΠ ((i (in-range 1 3)) (j (in-range 1 3))) (->fl (+ i j))) 8.0)
(check-eqv? (flΠ* ((i (in-range 1 3)) (j (in-range 1 3))) (->fl (+ i j))) 72.0)

;; Some tautologies
(define (taut1 x A B)
  (⇔ (∈ x (∪ A B)) (∨ (∈ x A) (∈ x B))))

(define (taut2 x A B)
  (⇔ (∈ x (∩ A B)) (∧ (∈ x A) (∈ x B))))

(define sets (list ∅ (set 1) (set 2 3) (set 1 2 3)))

(check-true
  (∀* ((x (in-list '(1 2 3)))
       (A (in-list sets))
       (B (in-list sets)))
      (∧ (taut1 x A B) (taut2 x A B))))