Tuples

TYPE tuple{$s: type SUCH THAT distinct(identifiers(s))}
  -- Two tuple types are the same if and only if they have
  -- the same actual parameters WITH THE SAME FIELD NAMES.
  -- Identifiers(s) is the sequence of identifiers used as
  -- field names in the actual parameter list.

  INHERIT equality{tuple{$s}}
  INHERIT partial_order{tuple{$s}}
    RENAME ">=" AS contains
    RENAME ">" AS properly_contains
  IMPORT identifiers identifier FROM field_names
  IMPORT distinct remove FROM sequence{identifier}

  MODEL(c: sequence{any})
  INVARIANT ALL(t: tuple{$s} :: t.c IN s)

  MESSAGE create($a: any)
    -- Literal [i1:: v1, ... , in:: vn] =
    -- create(i1:: v1, ... , in:: vn).
    WHEN a IN s & identifiers(a) = identifiers(s)
      REPLY(t: tuple{$s}) WHERE t.c = a
    OTHERWISE REPLY EXCEPTION type_error

  MESSAGE "."{id: identifier SUCH THAT id IN identifiers(s)}
             (t: tuple{$s})
    -- "."{b}(a) is written a.b, component selection.
    CHOOSE(k: nat, ct: type SUCH THAT
           identifiers(s)[k] = id & ct = s[k] )
    REPLY(x: ct) WHERE x = t.c[k]

  MESSAGE get(t: tuple{$s}, id: identifier)
    WHEN id IN identifiers(s)
      CHOOSE(n: nat, ct: type SUCH THAT ct = s[n])
      REPLY(x: ct) WHERE x = t.c[n]
    OTHERWISE REPLY EXCEPTION tuple_selection_error
    -- Get(t, "x") = t.x,
    -- this form allows the id to be calculated.

  MESSAGE "["(t: tuple{$s}, n: nat)
    -- "["(t, n) is written t[n].
    WHEN 1 <= n <= length(s)
      CHOOSE(ct: type SUCH THAT ct = s[n])
      REPLY(x: ct) WHERE x = t.c[n]
    OTHERWISE REPLY EXCEPTION tuple_selection_error

  MESSAGE remove(id: identifier, t1: tuple{$s})
    WHEN id IN identifiers(s)
      CHOOSE(n: nat, ss: sequence{type}
             SUCH THAT id = identifiers(s)[n] 
             & ss = s[1 .. n - 1] || s[n + 1 .. length(s)])
      REPLY(t2: tuple{$ss}) WHERE contains(t1, t2)
    OTHERWISE REPLY EXCEPTION tuple_selection_error

  MESSAGE "||"(t1: tuple{$s}, t2: tuple{$ss})  -- Concatenation.
    WHEN distinct(s || ss)
      REPLY(t3: tuple{$s, $ss}) WHERE t3.c = t1.c || t2.c
    OTHERWISE REPLY EXCEPTION type_error
    -- Tuple || is defined in terms of sequence ||.

  MESSAGE equal(t1 t2: tuple{$s})
    REPLY(b: boolean) WHERE b <=> t1.c = t2.c

  MESSAGE contains(t1: tuple{$s}, t2: tuple{$ss})
    REPLY(b: boolean)
      -- True if and only if t1 contains all of the components
      -- of t2.
    WHERE b <=> ALL(i: identifier SUCH THAT i IN identifiers(ss)
                    :: get(t1, i) = get(t2, i) )
END