Type type

TYPE type
  INHERIT equality{type} RENAME equal AS Equal
  IMPORT Partial_ordering FROM partial_order{type}
  EXPORT Has_operation Subtype Immutable Mutable
    Immutable_instances Static Indestructible Irreplaceable

  MESSAGE "IN"(x: any, t: type) REPLY(b: boolean)
    WHERE ALL(t: type, x: t :: x IN t), ALL(t: type :: ~(! IN t))
    -- True if x is a proper element of the data type t.
    -- The undefined element "!" can appear in of expressions
    -- of any type, but it is not proper a element of any type.

  MESSAGE "IN"(s1: sequence{any}, s2: sequence{type})
    REPLY(b: boolean)
      -- True if corresponding elements match.
      -- Example: [1.5, true] IN [real, boolean].
    WHERE b <=> length(s1) = length(s2) &
                ALL(n: nat SUCH THAT n IN domain(s1) ::
                    s1[n] IN s2[n] )

  MESSAGE Equal(t1 t2: type) REPLY(b: boolean)
    WHERE b <=> ALL(x: any :: x IN t1 <=> x IN t2) &
          ALL(ts: sequence{type}, f: function{$ts} 
              :: Has_operation{$ts}(t1, f) <=>
                 Has_operation{$ts}(t2, f) )
    -- Two types are equal if and only if they have
    -- the same elements and the same operations.

  CONCEPT Has_operation{ts: type_sequence}
                       (t: type, f: function{$ts})
    VALUE(b: boolean)
    -- True if the type t accepts the message f.

  CONCEPT Subtype(t1 t2: type) VALUE(b: boolean)
    WHERE ALL(t1 t2: type SUCH THAT
              Subtype(t1, t2) :: ALL(x: t1 :: x IN t2)),
      Partial_ordering(Subtype)
    -- True if t1 satisfies the specification of t2.

  CONCEPT Immutable(t: type) VALUE(b: boolean)
    -- True if the properties of the type cannot change.
    WHERE b <=> always(t = *t | *t = !),
        -- Always is a modal operator, which means that the
        -- enclosed predicate is true in all possible states.
        -- In the initial state *t = !.
      ALL(t: type :: Immutable(t) <=>
          Static(t) & Immutable_instances(t) )
        -- A type is immutable if the set of instances
        -- cannot change and the state of each
        -- individual instance cannot change.

  CONCEPT Mutable(t: type) VALUE(b: boolean)
    WHERE b <=> ~Immutable(t)

  CONCEPT Immutable_instances(t: type) VALUE(b: boolean)
    -- True if the states of the instances
    -- of the type cannot change.
    WHERE b <=> always(ALL(x: t :: x = *x | *x = !))

  CONCEPT Static(t: type) VALUE(b: boolean)
    -- True if the set of instances of the type cannot change.
    WHERE b <=> always(ALL(x: Completion{t} ::
                           x IN t <=> *x IN *t | *t = !) ),
      ALL(t: type :: Static(t) <=>
          Indestructible(t) & Irreplaceable(t) )

  CONCEPT Indestructible(t: type) VALUE(b: boolean)
      -- True if instances of the type t can never be destroyed.
    WHERE b <=> always(ALL(x: Completion{t} ::
                           (*x IN *t => x IN t) | *t = !) )

  CONCEPT Irreplaceable(t: type) VALUE(b: boolean)
      -- True if new instances of the type t
      -- can never be created.
    WHERE b <=> always(ALL(x: t ::
                           (x IN t => *x IN *t) | *t = !) )

  CONCEPT Completion{t1: type}: type
      -- The set of all present and future
      -- instances of the type t.
    WHERE ALL(x: any :: x IN Completion{t} <=> sometime(x IN t))
        -- Sometime is a modal operator, which means that the
        -- enclosed predicate is true now or
        -- in some future state.
END