Constraints on Type Declarations

The constraints on type declarations are discussed in detail in the reference manual. From the point of view of these constraints we consider the names of code types as though they are type names. Here we simply list them for convenience.

• If enumeration of atomics overlap then one must be completely contained in the other.
• Overlaps between constructor enumerated types are not allowed.
• The union of parameterized (polymorphic) types are not allowed.
• Enumerator values (or their functors in the case of constructor enumerations) can not be used as the names of types and visa a versa.

The following example, from the reference manual, shows how union types can be used when we want overlapping types.

  def digit ::= 0..9
  def range12 ::= 10..20
  def range21 ::= -10..-1
  def range1 == digit || range12
  def range2 == range21 || digit

Now range1 and range2 are essentially the same as the enumerated types 0..20 and -10..9 without breaking the above constraints.

The more strict constraint on constructor enumerations seems to be excessively strong but we believe that it will not come up often in practice. If it does we can define two constructor enumerations with different constructors and then write a converter relation as in the following example.

  def tree(T) ::= empty() | tr(tree(T),T,tree(T))
  def tree2(N,L) ::=  
  leaf(L) | none() | node(tree2(N,L), N, tree2(N,L))

  rel tree_to_tree2(!tree(T), ?tree2(T, T)),  
      tree_to_tree2(?tree(T), !tree2(T, T))
  tree_to_tree2(empty(), none())
  tree_to_tree2(tr(empty(), V, empty()), leaf(V)) :: true
  tree_to_tree2(tr(L, V, R), node(L2, V, R2)) <=
      tree_to_tree2(L, L2) &
      tree_to_tree2(R, R2)