Unions

TYPE union{$s: type SUCH THAT distinct(identifiers(s))}
  -- A union type is a tagged disjoint union of a set of types.
  -- Two union 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{union{$s}}
  IMPORT identifiers identifier FROM field_names
  IMPORT distinct FROM sequence{identifier}

  MODEL(tag: identifier, value: any)
  INVARIANT ALL(u: union{$s} :: u.tag IN identifiers(s)),
    ALL(u: union{$s} :: u.value IN type_of(u.tag))

  MESSAGE create{id: identifier SUCH THAT id IN identifiers(s)}
              (x: any)
    -- Literal {t :: v} = create{t}(v).
    WHEN x IN type_of(id)
      REPLY(u: union{$s}) WHERE u.tag = id & u.value = x
    OTHERWISE REPLY EXCEPTION type_error

  MESSAGE is{id: identifier SUCH THAT id IN identifiers(s)}
            (u: oneof{$s})
    REPLY(b: boolean) WHERE b <=> u.tag = id
    -- Check if you have a given variant.

  MESSAGE "."{id: identifier SUCH THAT id IN identifiers(s)}
             (u: oneof{$s})
    -- "."{b}(a) is written a.b, projection.
    WHEN u.tag = id
      CHOOSE(rt: type SUCH THAT rt = type_of(id))
      REPLY(x: rt) WHERE x = u.value
    OTHERWISE REPLY EXCEPTION type_error
    -- Extract the value assuming a given variant,
    -- succeeds only if the tag matches the assumed variant.

  MESSAGE equal(u1 u2: union{$s})
    REPLY(b: boolean)
    WHERE b <=> u1.tag = u2.tag & u1.value = u2.value

  CONCEPT type_of(id: identifier SUCH THAT id IN identifiers(s))
    VALUE(t: type)
    -- The type corresponding to the id
    -- in the formal parameter list s.
      WHERE SOME(n: nat :: t = s[n] & id = identifiers(s)[n])
END