Équivalence

VIRTUAL TYPE equivalence {t: type}
  INHERIT equality{t}
  INHERIT Mutable{t}
  IMPORT Immutable FROM type
  IMPORT Reflexive Symmetric Transitive FROM equal{t}
  IMPORT Deterministic FROM function{any, any}

  MESSAGE equivalent(x y: t)
    REPLY(b: boolean)
    WHERE Reflexive(equivalence), Symmetric(equivalence),
      Transitive(equivalence),
      ALL(a b: t :: a == b => same_state{t}(a, b))
  -- State equivalence: two distinct copies of the same object
  -- are equivalent but not equal.

  MESSAGE not_equivalent(x y: t)
    REPLY(b: boolean)
    WHERE b <=> ~equivalent(x, y)

  MESSAGE copy(x: t)
    REPLY(y: t) WHERE y == x, y ~= x
    TRANSITION new(y)

  CONCEPT same_state{t1:type}(x y: t1)
    VALUE(b: boolean)
    WHERE Immutable(t1) =>
          ALL(c d: t1 :: same_state{t1}(c, d) => c = d),
        -- For Immutable types equality and equivalence
        -- are the same.
      ALL(c d: t1, ts1 ts2: sequence{type}, s1: ts1, s2: ts2,
          range: type, f: function{$ts1, t1, $ts2, range}
          SUCH THAT f ~= equal@t1 & Deterministic(f) ::
          same_state{t1}(c, d) =>
            same_state{range}(f($s1, c, $s2), f($s1, d, $s2)) )
  -- Two equivalent objects can only be distinguished
  -- by the equal operation or applying a state changing
  -- operation to one of the objects.  This is a restriction
  -- on the functional operations of well formed mutable types.

  CONCEPT "=="(x y:t) VALUE(b: boolean)

  CONCEPT "~=="(x y:t) VALUE(b: boolean)
    WHERE b <=> ~(x == y)
END