154 Predicates Induced by Variants and Enums

Consider a variant type Shape:

value Point
{
    Real x;
    Real y;
}

value Circle
{
    Point centre;
    Real radius;
}

value Triangle
{
    Point vertex[3];
}

variant Shape
{
    Circle circle;
    Triangle triangle;
}

Path query expressions and their denotation into logic work on variants in the same way as entity and value types. For example, given a program variable s of type Shape, the following gives examples of query expressions:

            s.circle
        

            circle=C:Circle 
            where s.circle(C)
        

            s.circle.radius
        

            radius=R:Real
            where 
              ∃C:Circle
                s.circle(C) 
              ∧ C.radius(R)
        

Using attributes of the empty structural type in boolean contexts

The empty structural type is often useful in variant types, for example:

variant Tree
{
    {} empty;
    Tree child+;
}

In a Boolean context, a path with result type {} is treated by static elaboration, before denotation, as an existence test. The same rule applies to path expressions whose frame result has no attributes. Define:

asBoolean(E)
{
    if type(E) = Boolean
        return E

    if type(E) = {}
        return E.Σexists

    if resultAttributes(E) = ∅
        return E.Σexists

    otherwise
        raise error
}

Boolean contexts include filters, logical negation and connectives, constraints, and Boolean-valued function arguments. Each such context applies asBoolean to the expression it expects to be Boolean. The denotational rules therefore still receive an ordinary Boolean expression and do not need special cases for {} or empty result sets.

For example, given a variable t of type Tree, the path expression t.empty can be used instead of t.empty.Σexists in a filter.

Likewise, an empty projection such as s.supplier.() has no result attributes. In a Boolean context such as logical negation it is elaborated as an existence test, so:

¬(s.supplier.())

is elaborated as:

¬(s.supplier.().Σexists)

This does not make s.supplier.() a scalar Boolean result. Its short denotation may still be displayed as the formula alone, for example ∃S:Supplier (s.supplier(S)).

Enumerated types

enum Color
{
    red, green, blue
}

is syntactic sugar for:

variant Color
{
    {} red;
    {} green;
    {} blue;
}

The following query finds the red or green parts shipped by suppliers in London:

s.supplier.[city = 'London].shipment.part.[color.red ∨ color.green]