|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: INNER | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object | +--xrel.analyzer.WellFormedness
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.
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 |
public WellFormedness()
Method Detail |
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:
while the following recursive definitions are correct:typedef X = a[],X | (); // self-recursive typedef Y = b[],Z | String; // mutually recursive with Z typedef Z = c[],Y | String; // '' '' with Y
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:
both y and z are reachable from the expansion of x.typedef x = y; typedef y = z;
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.
st
- the symbol tableroot
- the root node of the syntax treepublic 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:
BV(P) = {x,y}l1[T as x], (l2[] as y | l3[U as 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:
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
st
- the symbol tableroot
- the root node of the syntax tree
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: INNER | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |