xrel.analyzer
Class WellFormedness

java.lang.Object
  |
  +--xrel.analyzer.WellFormedness
All Implemented Interfaces:
SpecialNames

public class WellFormedness
extends java.lang.Object
implements SpecialNames

Provides some well-formedness checks on type expressions and patterns. Specifically:

N.B.: This is a static class, you will never need to allocate an object of this class.

Author:
Fabrizio Bisi

Fields inherited from interface xrel.parser.SpecialNames
AnyTagName, AnyTypeName, AutomatonPrefix, EmptyPatternName, ExportTypeName, ExpressionPrefix, PatternPrefix, SpecialPrefix, StringName, StringPatternName, StringTypeName, StrLiteralPrefix, StrLiteralSuffix, StrUnquotedPrefix, StrUnquotedSuffix
 
Constructor Summary
WellFormedness()
           
 
Method Summary
static boolean checkLinearity(SymTable st, SimpleNode root)
          Checks that all the patterns inside the program are linear.
static boolean disconnectedness(SymTable st, SimpleNode root)
          Checks that all the type declarations in the program don't have recursion at the top-level.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

WellFormedness

public WellFormedness()
Method Detail

disconnectedness

public static boolean disconnectedness(SymTable st,
                                       SimpleNode root)

Checks that all the type declarations in the program don't have recursion at the top-level. For example the following definitions are wrong:

 typedef X = a[],X | ();     // self-recursive
 typedef Y = b[],Z | String; // mutually recursive with Z
 typedef Z = c[],Y | String; //    ''        ''    with Y
while the following recursive definitions are correct:
 typedef A = a[B] | String;
 typedef B = b[A] | String;

N.B.:

Algorithm:

Let x,y,.. range over type names and let T,U,.. range over type expressions. For each type declaration in the program:

 typedef x = T;

we need to check that x don't recur neither directly inside T neither inside the expansion of a type name reachable at top-level from T. For expansion of a type name y we intend its related type expression U in the statement "typedef y = U". A type name y is reachable at top-level from a type expression T if it's possible to reach y from T by subsequent expansions. For example in:

 typedef x = y;
 typedef y = z;
both y and z are reachable from the expansion of x.

For each type declaration "typedef x = T" the main function calls a subroutine "dc" with parameters dc(emptySet,T,x) that checks that x is not reachable at top-level from T.

Here's a pseudo-code for the subroutine:

 boolean dc(sigma,T,x) {
   switch (kind of T) {
     case "|", ",": 
       return dc(sigma,T.child(1),x) && .. && dc(sigma,T.child(n),x);
     case empty,tag,literal: 
       return true;         // base case 1 (success)
     case x: return false;  // base case 2 (fails!)
     case y != x: 
       if (y is in sigma) return true;
       else return dc(sigma + {y},U,x); // "typedef y = U;"
   }
 }

The first argument "sigma" of the function is the set of type names we have already expanded (initially empty). We return immediately true when we found a string literal, an empty node or a tag (remember that we're searching only top-level recursion); conversely we return false when we found x. If we encounter another type name y different from x we return true if it's present in sigma (as this means we have already checked it), otherwise we recursively call dc with sigma = sigma + {y} checking if x is in the expansion of y.

Note that we don't need to check the export type as it can't be recursive.

Parameters:
st - the symbol table
root - the root node of the syntax tree
Returns:
true if all the type declarations are disconnected, false otherwise

checkLinearity

public static boolean checkLinearity(SymTable st,
                                     SimpleNode root)

Checks that all the patterns inside the program are linear. Remember that a pattern is linear if variables inside it are bound exactly once.

N.B.:

Algorithm:

Let BV(P) the set of variables bound in the pattern P. For example in the following pattern P:

 
 l1[T as x], (l2[] as y | l3[U as y])
BV(P) = {x,y}

Note that BV(P) is similar to the set of reachable type names at top-level in a type expression T (let we call it reach(T) now) with the following main differences:

For each pattern in the program (that of the import statement and patterns of the clauses in the typeswitch construct) we recursively check the followings:
 P = P1 as x     x is not in P1
 P = P1,P2       intersection(BV(P1),BV(P2)) = the empty set
 P = P1|P2       BV(P1) = BV(P2)
 P = P1*         BV(P1) = the empty set

Parameters:
st - the symbol table
root - the root node of the syntax tree
Returns:
true if all the patterns are linear, false otherwise