Forlan Manual

The `PT` Module

Synopsis

signature PT structure PT :> PT

This module defines the abstract type of parse trees.

Interface

datatype concr = Node of Sym.sym * concr list option type pt val fromConcr : concr -> pt val toConcr : pt -> concr val fromString : string -> pt val input : string -> pt val toPP : pt -> PP.pp val toString : pt -> string val output : string * pt -> unit val validPath : pt * int list -> bool val height : pt -> int val size : pt -> int val numLeaves : pt -> int val selectPT : pt * int list -> pt option val update : pt * int list * pt -> pt val maximumLengthPath : pt -> int list val validLeafPath : pt * int list -> bool val compare : pt Sort.total_ordering val equal : pt * pt -> bool val cons : Sym.sym * pt list option -> pt val leaf : Sym.sym -> pt val decons : pt -> Sym.sym * pt list option val rootLabel : pt -> Sym.sym val yield : pt -> Str.str type pumping_division = (pt * int list) * (pt * int list) * pt val checkPumpingDivision : pumping_division -> unit val validPumpingDivision : pumping_division -> bool val strsOfValidPumpingDivision : pumping_division -> Str.str * Str.str * Str.str * Str.str * Str.str val pumpValidPumpingDivision : pumping_division * int -> pt val findValidPumpingDivision : pt -> pumping_division val findValidPumpingDivisionOpt : pt -> pumping_division option val jforlanNew : unit -> pt val jforlanEdit : pt -> pt val jforlanValidate : string -> unit val jforlanPretty : string -> unit

Description

datatype concr = Node of Sym.sym * concr list option

The concrete datatype of parse trees. If a is a symbol, then Node(a, NONE) is the parse tree whose root node is labeled by a, and which has a single child, labeled by %, with no children. And, if a is a symbol and pts is a list of parse trees, then Node(a, SOME pts) is the parse tree whose root node is labeled by a and whose children are the elements of pts, if any.

type pt

The abstract type of parse trees, consisting of the values of type concr.

fromConcr concr

returns concr.

toConcr pt

returns pt.

fromString s

inputs a parse tree from s.

input fil

inputs a parse tree from the file named by fil.

toPP pt

returns a pretty-printing expression for pt.

toString pt

pretty-prints pt to a string.

output(fil, pt)

pretty-prints pt to the file named by fil.

validPath(pt, ns)

tests whether ns is a valid path for pt.

height pt

returns the height of pt.

size pt

returns the size of pt.

numLeaves pt

returns the number of leaves of pt.

selectPT(pt, ns)

Suppose tr is the subtree of pt pointed to by ns. If tr is % (i.e., has a single node, labeled by %), then selectPT returns NONE. Otherwise, selectPT returns SOME tr. Issues an error message if ns isn't a valid path for pt.

update(pt, ns, pt')

returns the result of replacing the subtree of pt pointed to by ns with pt'. Issues an error message if ns isn't valid for pt.

maximumLengthPath pt

returns a leftmost, maximum length path for pt.

validLeafPath(pt, ns)

tests whether ns is a valid path for pt that points to a leaf of pt, i.e., to a subtree with no children.

compare

is defined by:

  fun compare(Node(a1, SOME pt1s), Node(a2, SOME pt2s)) =
        (case Sym.compare(a1, a2) of
              LESS    => LESS
            | EQUAL   => Set.compareList compare (pt1s, pt2s)
            | GREATER => GREATER)
    | compare(Node(a1, NONE),      Node(a2, NONE))      = Sym.compare(a1, a2)
    | compare(Node(_, SOME _),     Node(_, NONE))       = LESS
    | compare(Node(_, NONE),       Node(_, SOME _))     = GREATER

equal(pt1, pt2)

tests whether pt1 and pt2 are equal.

cons(a, ptsOpt)

returns Node(a, ptsOpt).

leaf a

returns the tree with a single node labeled a.

decons pt

returns (a, ptsOpt), where a and ptsOpt are unique such that pt is equal to Node(a, ptsOpt).

rootLabel pt

returns the root label of pt.

yield pt

returns the yield of pt.

type pumping_division = (pt * int list) * (pt * int list) * pt

The following functions on pumping divisions can be used to experiment with the pumping lemma for context-free languages.

A pumping division ((pt1, path1), (pt2, path2), path3) is valid iff:

path1 is a valid path for pt1, pointing to a leaf whose label isn't %;
path2 is a valid path for pt2, pointing to a leaf whose label isn't %;
the label of the leaf of pt1 pointed to by path1 is equal to the root label of pt2;
the label of the leaf of pt2 pointed to by path2 is equal to the root label of pt2;
the root label of pt3 is equal to the root label of pt2;
the yield of pt2 has at least two symbols;
the yield of pt1 has only one occurrence of the root label of pt2;
the yield of pt2 has only one occurrence of the root label of pt2; and
the yield of pt3 does not contain the root label of pt2.

checkPumpingDivision pd

checks whether pd is valid, silently returning (), if it is, and issuing an error message explaining why it's not, if it's not.

validPumpingDivision pd

tests whether pd is valid.

strsOfValidPumpingDivision((pt1, path1), (pt2, path2), pt3)

returns (u, v, w, x, y), where:

u is the prefix of yield pt1 that precedes the unique occurrence of the root label of pt2;
v is the prefix of yield pt2 that precedes the unique occurrence of the root label of pt2;
w is the yield of pt3;
x is the suffix of yield pt2 that follows the unique occurrence of the root label of pt2; and
y is the suffix of yield pt1 that follows the unique occurrence of the root label of pt2.

Issues an error message if the pumping division isn't valid.

pumpValidPumpingDivision(((pt1, path1), (pt2, path2), pt3), n)

returns

  let fun pow 0 = pt3
        | pow n = update(pt2, path2, pow(n - 1))
  in update(pt1, path1, pow n) end

Issues an error message if the pumping division isn't valid, or if n is negative.

findValidPumpingDivision pt

tries to find a valid pumping division pd such that pumpValidPumpingDivision(pd, 1) is pt. It works as follows. First, the leftmost, maximum length path path through pt is found. If this path points to %, then an error message is issued. Otherwise, findValidPumpingDivision generates the following list of variables paired with prefixes of path:

the root label of the subtree pointed to by the path consisting of all but the last element of path, paired with that path;
the root label of the subtree pointed to by the path consisting of all but the last two elements of path, paired with that path;
...;
the root label of the subtree pointed to by the path consisting of the first element of path, paired with that path; and
the root label of the subtree pointed to by [], paired with [].

(Of course, the left-hand side of the last of these pairs is the root label of pt.) As it works through these pairs, it looks for the first repetition of variables. If there is no such repetition, it issues an error message. Otherwise, suppose that:

q was the first repeated variable;
path1 was the path paired with q at the point of the first repetition; and
path' was the path paired with q when it was first seen.

Now, it lets:

path2 be the result of dropping path1 from the beginning of path';
pt1 be update(pt, path1, Leaf q);
pt' be the subtree of pt pointed to by path1;
pt2 be update(pt', path2, Leaf q);
pt3 be the subtree of pt' pointed to by path2; and
pd be ((pt1, path1), (pt2, path2), pt3).

If pd is a valid pumping division (only the last four conditions of the definition of validity remain to be checked), it is returned by findValidPumpingDivision. Otherwise, an error message is issued.

findValidPumpingDivisionOpt pt

behaves like findValidPumpingDivision pt, except that:

if findValidPumpingDivision pt returns normally, then findValidPumpingDivisionOpt returns SOME of what it returns; and
if findValidPumpingDivision pt issues an error message, then findValidPumpingDivisionOpt silently returns NONE.

jforlanNew()

invokes JForlan, and returns the parse tree that the user creates and commits. Issues an error message if the user aborts, instead.

jforlanEdit pt

invokes JForlan, letting the user edit pt, and returning the resulting parse tree that the user commits. Issues an error message if the user aborts, instead.

jforlanValidate

is a low-level function used by JForlan. See the code for more information.

jforlanPretty