Relations

TYPE relation{$s: type SUCH THAT distinct(identifiers(s))}
  -- Two relation 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{relation{$s}}
  INHERIT partial_order{relation{$s}}
    RENAME "<=" AS subset
    RENAME "<" AS proper_subset
  IMPORT distinct remove FROM sequence{identifier}
  IMPORT distinct FROM sequence{tuple{$s}}  -- distinct is overloaded
  IMPORT identifiers identifier FROM field_names
  IMPORT type_of FROM union{$s}

  MODEL(s: set{tuple{$s}})
  INVARIANT true

  MESSAGE create
    -- Literal { } = create.
    REPLY(r: relation{$s}) WHERE r.s = { }

  MESSAGE add(t: tuple{$s}, r1: relation{$s})
    -- Literal {t} = add(t, empty).
    -- Literal {t, $r} = add(t, r).
    REPLY(r2: relation{$s})
    WHERE r2.s = r1.s U {t}

  MESSAGE "IN"(x: tuple{$s}, r: relation{$s}) REPLY(b: boolean)
    WHERE b <=> x IN r.s

  MESSAGE domain{id: identifier SUCH THAT id IN identifiers(s)}
                (r: relation{$s})
    CHOOSE(ct: type SUCH THAT ct = type_of(id))
    REPLY(d: set{ct})
    WHERE ALL(x: ct :: x IN d <=>
              SOME(t: tuple{$s} :: t IN r & get{id}(t) = x) )
    -- The set of values that appear in a given column
    -- of the relation.
    -- Example: relation{a:: char, b:: nat}
    -- domain{a}({[a:: 'x', b:: 1],
    --            [a:: 'y', b:: 2],
    --            [a:: 'x', b:: 3] }) = {'x', 'y'}.

  MESSAGE select{id: identifier SUCH THAT
                 id IN identifiers(s) & ct = type_of(id) }
                (r1: relation{$s}, x: ct)
    REPLY(r2: relation{$ss})
    WHERE ss = remove(id, s),
      ALL(t2: tuple{$ss} :: t2 IN r2.s <=>
          SOME(t1: tuple{$s} :: t1 IN r1 & get{id}(t1) = x &
                                contains(t1, t2) ))
    -- Select all of the tuples with a given value
    -- in one of the columns.
    -- Example: relation{a:: char, b:: nat}
    -- select{a}({[a:: 'x', b:: 1],
    --            [a:: 'y', b:: 2],
    --            [a:: 'x', b:: 3] }, 'x') = {[b:: 1], [b:: 3]}.

  MESSAGE project{id: identifier SUCH THAT id IN identifiers(s)}
                 (r1: relation{$s})
    REPLY(r2: relation{$ss})
    WHERE ss = remove(id, s),
      ALL(t2: tuple{$ss} :: t2 IN r2.s <=>
        SOME(t1: tuple{$s} :: t1 IN r1 & contains(t1, t2)) )
    -- Ignore the information in one of the columns
    -- of the relation.
    -- Example: relation{a:: char, b:: nat}
    -- project{a}({[a:: 'x', b:: 1],
    --             [a:: 'y', b:: 2],
    --             [a:: 'x', b:: 3] }) =
    -- {[b:: 1], [b:: 2], [b:: 3]}.

  MESSAGE join{id: identifier SUCH THAT
               ALL(i: identifier :: i = id <=>
                   i IN identifiers(s) & i IN identifiers(ss) )}
              (r1: relation{$s}, r2: relation{$ss})
    REPLY(r3: relation{$sss})
    WHERE sss = remove(id, [$s, $ss]),
      ALL(t3: tuple{$sss} :: t3 IN r3.s <=>
        SOME(t1: tuple{$s}, t2: tuple{$ss} SUCH THAT
             t1 IN r1 & t2 IN r2 & get(t1, id) = get(t2, id) ::
             t3 = remove(id, t1) || remove(id, t2) ))
    -- Natural join from relational databases.

  MESSAGE "U"(r1 r2: relation{$s})
    -- Literal {$r1, $r2} = r1 U r2.
    REPLY(r3: relation{$s})
    WHERE ALL(x: tuple{$s} :: x IN r3 <=> (x IN r1 | x IN r2))

  MESSAGE "-"(r1 r2: relation{$s}) REPLY(r3: relation{$s})
    WHERE ALL(x: tuple{$s} :: x IN r3 <=> (x IN r1 & ~(x IN r2)))

  MESSAGE intersection(r1 r2: relation{$s})
    REPLY(r3: relation{$s})
    WHERE ALL(x: tuple{$s} :: x IN r3 <=> (x IN r1 & x IN r2))

  MESSAGE size(r: relation{$s})
    REPLY(n: nat)
    WHERE n = NUMBER(t: tuple{$s} SUCH THAT t IN s :: t)

  MESSAGE equal(r1 r2: relation{$s})
    REPLY(b: boolean)
    WHERE b <=> r1.s = r2.s

  MESSAGE subset(r1 r2: relation{$s}) REPLY(b: boolean)
    WHERE b <=> subset(r1.s, r2.s)

  MESSAGE scan(r: relation{$s})
    GENERATE(s: sequence{tuple{$s}})
    WHERE ALL(x: tuple{$s} :: x IN s <=> x IN r), distinct(s)
END