;; lib/maude/tests/conditional.sx — Phase 4: conditional equations.

(define mct-pass 0)
(define mct-fail 0)
(define mct-failures (list))

(define
  mct-check!
  (fn
    (name got expected)
    (if
      (= got expected)
      (set! mct-pass (+ mct-pass 1))
      (do
        (set! mct-fail (+ mct-fail 1))
        (append!
          mct-failures
          (str name "  expected: " expected "  got: " got))))))

;; ---- gcd (equational guard, recursive) ----

(define
  mct-gcd
  (mau/parse-module
    "fmod GCD is\n  sorts Nat Bool .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op true : -> Bool .\n  op false : -> Bool .\n  op _>_ : Nat Nat -> Bool .\n  op _-_ : Nat Nat -> Nat .\n  op gcd : Nat Nat -> Nat .\n  vars X Y : Nat .\n  eq 0 > Y = false .\n  eq s X > 0 = true .\n  eq s X > s Y = X > Y .\n  eq X - 0 = X .\n  eq 0 - Y = 0 .\n  eq s X - s Y = X - Y .\n  eq gcd(X, 0) = X .\n  eq gcd(0, Y) = Y .\n  eq gcd(X, X) = X .\n  ceq gcd(X, Y) = gcd(X - Y, Y) if X > Y = true .\n  ceq gcd(X, Y) = gcd(Y, X) if Y > X = true .\nendfm"))

(mct-check!
  "gcd-6-4"
  (mau/creduce->str mct-gcd "gcd(s s s s s s 0, s s s s 0)")
  "s_(s_(0))")
(mct-check!
  "gcd-3-6"
  (mau/creduce->str mct-gcd "gcd(s s s 0, s s s s s s 0)")
  "s_(s_(s_(0)))")
(mct-check!
  "gcd-base-zero"
  (mau/creduce->str mct-gcd "gcd(s s 0, 0)")
  "s_(s_(0))")
(mct-check!
  "gcd-equal"
  (mau/creduce->str mct-gcd "gcd(s s 0, s s 0)")
  "s_(s_(0))")
(mct-check!
  "gcd-coprime"
  (mau/creduce->str mct-gcd "gcd(s s s 0, s s 0)")
  "s_(0)")
;; guard predicate reductions
(mct-check! "gt-true" (mau/creduce->str mct-gcd "s s 0 > s 0") "true")
(mct-check! "gt-false" (mau/creduce->str mct-gcd "s 0 > s s 0") "false")

;; ---- insertion sort (true/false guards) ----

(define
  mct-sort
  (mau/parse-module
    "fmod SORT is\n  sorts Nat List Bool .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op true : -> Bool .\n  op false : -> Bool .\n  op _<=_ : Nat Nat -> Bool .\n  op nil : -> List .\n  op _:_ : Nat List -> List .\n  op insert : Nat List -> List .\n  op sort : List -> List .\n  vars M N : Nat .\n  var L : List .\n  eq 0 <= N = true .\n  eq s M <= 0 = false .\n  eq s M <= s N = M <= N .\n  eq insert(N, nil) = N : nil .\n  ceq insert(N, M : L) = N : (M : L) if N <= M = true .\n  ceq insert(N, M : L) = M : insert(N, L) if N <= M = false .\n  eq sort(nil) = nil .\n  eq sort(N : L) = insert(N, sort(L)) .\nendfm"))

(mct-check!
  "sort-321"
  (mau/creduce->str mct-sort "sort(s s s 0 : (s 0 : (s s 0 : nil)))")
  "_:_(s_(0), _:_(s_(s_(0)), _:_(s_(s_(s_(0))), nil)))")
(mct-check! "sort-empty" (mau/creduce->str mct-sort "sort(nil)") "nil")
(mct-check!
  "sort-singleton"
  (mau/creduce->str mct-sort "sort(s s 0 : nil)")
  "_:_(s_(s_(0)), nil)")
(mct-check!
  "insert-front"
  (mau/creduce->str mct-sort "insert(0, s 0 : (s s 0 : nil))")
  "_:_(0, _:_(s_(0), _:_(s_(s_(0)), nil)))")
(mct-check!
  "insert-back"
  (mau/creduce->str mct-sort "insert(s s s 0, s 0 : (s s 0 : nil))")
  "_:_(s_(0), _:_(s_(s_(0)), _:_(s_(s_(s_(0))), nil)))")

;; ---- max (conditional simplification, both branches) ----

(define
  mct-max
  (mau/parse-module
    "fmod MAX is\n  sorts Nat Bool .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op true : -> Bool .\n  op false : -> Bool .\n  op _<=_ : Nat Nat -> Bool .\n  op max : Nat Nat -> Nat .\n  vars M N : Nat .\n  eq 0 <= N = true .\n  eq s M <= 0 = false .\n  eq s M <= s N = M <= N .\n  ceq max(M, N) = M if N <= M = true .\n  ceq max(M, N) = N if N <= M = false .\nendfm"))

(mct-check!
  "max-left"
  (mau/creduce->str mct-max "max(s s s 0, s 0)")
  "s_(s_(s_(0)))")
(mct-check!
  "max-right"
  (mau/creduce->str mct-max "max(s 0, s s 0)")
  "s_(s_(0))")
(mct-check!
  "max-equal"
  (mau/creduce->str mct-max "max(s s 0, s s 0)")
  "s_(s_(0))")

;; ---- boolean-kind condition (`if pred`) ----

(define
  mct-even
  (mau/parse-module
    "fmod EVEN is\n  sorts Nat Bool Tag .\n  op 0 : -> Nat .\n  op s_ : Nat -> Nat .\n  op true : -> Bool .\n  op false : -> Bool .\n  op even : Nat -> Bool .\n  op evn : -> Tag .\n  op odd : -> Tag .\n  op tag : Nat -> Tag .\n  var N : Nat .\n  eq even(0) = true .\n  eq even(s 0) = false .\n  eq even(s s N) = even(N) .\n  ceq tag(N) = evn if even(N) .\n  ceq tag(N) = odd if even(N) = false .\nendfm"))

(mct-check! "even-4" (mau/creduce->str mct-even "even(s s s s 0)") "true")
(mct-check! "even-3" (mau/creduce->str mct-even "even(s s s 0)") "false")
(mct-check! "tag-even-bool" (mau/creduce->str mct-even "tag(s s 0)") "evn")
(mct-check! "tag-odd" (mau/creduce->str mct-even "tag(s s s 0)") "odd")

(define mau-conditional-tests-run! (fn () {:failures mct-failures :total (+ mct-pass mct-fail) :passed mct-pass :failed mct-fail}))