Forlan Manual

The `Reg` Module

Synopsis

signature REG structure Reg :> REG

This module defines the abstract type of regular expressions.

Interface

datatype concr = EmptyStr | EmptySet | Sym of Sym.sym | Closure of concr | Concat of concr * concr | Union of concr * concr type reg val fromConcr : concr -> reg val toConcr : reg -> concr val inputFromLabToks : (int * Lex.tok) list -> reg * (int * Lex.tok) list val fromString : string -> reg val input : string -> reg val toPP : reg -> PP.pp val toString : reg -> string val output : string * reg -> unit val validPath : reg * int list -> bool val height : reg -> int val size : reg -> int val numLeaves : reg -> int val select : reg * int list -> reg val update : reg * int list * reg -> reg val maximumLengthPath : reg -> int list val validLeafPath : reg * int list -> bool val emptyStr : reg val emptySet : reg val fromSym : Sym.sym -> reg val closure : reg -> reg val concat : reg * reg -> reg val union : reg * reg -> reg val isEmptyStr : reg -> bool val isEmptySet : reg -> bool val isSym : reg -> bool val isClosure : reg -> bool val isConcat : reg -> bool val isUnion : reg -> bool val compare : reg Sort.total_ordering val equal : reg * reg -> bool val fromStr : Str.str -> reg val power : reg * int -> reg val alphabet : reg -> Sym.sym Set.set val split : reg -> Str.str * reg option val genConcat : reg list -> reg val genUnion : reg list -> reg val rightConcat : reg * reg -> reg val rightUnion : reg * reg -> reg val concatsToList : reg -> reg list val unionsToList : reg -> reg list val sortUnions : reg -> reg val allSym : Sym.sym Set.set -> reg val allStr : Sym.sym Set.set -> reg val fromStrSet : Str.str Set.set -> reg type cc val ccToList : cc -> int list val singCC : int -> cc val unionCC : cc * cc -> cc val succCC : cc -> cc val cc : reg -> cc val compareCC : cc Sort.total_ordering val numConcats : reg -> int val numSyms : reg -> int val standardized : reg -> bool val compareComplexity : reg * reg -> order val compareComplexityTotal : reg Sort.total_ordering val weaklySimplified : reg -> bool val weaklySimplify : reg -> reg val toStrSetOpt : reg -> Str.str Set.set option val toStrSet : reg -> Str.str Set.set val hasEmp : reg -> bool val hasSym : Sym.sym * reg -> bool val obviousSubset : reg * reg -> bool val localSimplificationRelations : reg * reg -> order val locallySimplified : (reg * reg -> bool) -> reg -> bool val locallySimplifyTrace : int option * (reg * reg -> bool) -> reg -> bool * reg val locallySimplify : int option * (reg * reg -> bool) -> reg -> bool * reg val globallySimplified : (reg * reg -> bool) -> reg -> bool val globallySimplifyTrace : int option * (reg * reg -> bool) -> reg -> bool * reg val globallySimplify : int option * (reg * reg -> bool) -> reg -> bool * reg val renameAlphabet : reg * SymRel.sym_rel -> reg val rev : reg -> reg val prefix : reg -> reg val jforlanNew : unit -> reg val jforlanEdit : reg -> reg val jforlanValidate : string -> unit val jforlanPretty : string -> unit

Description

The concrete datatype of regular expressions. EmptyStr is %, EmptySet is $, and, for all symbols a, Sym a is the one node tree whose label is a. For all regular expressions reg, Closure reg is the tree whose root node is labeled by "*" and whose only child is reg. And, for all regular expressions reg1 and reg2: Concat(reg1, reg2) is the tree whose root node is labeled by "@", with left child reg1 and right child reg2; and Union(reg1, reg2) is the tree whose root node is labeled by "+", with left child reg1 and right child reg2.

type reg

The abstract type of regular expressions, consisting of the values of type concr.

fromConcr concr

returns concr.

toConcr reg

returns reg.

inputFromLabToks lts

tries to input a regular expression from lts, consuming as much of lts as possible, and returning the pair of that regular expression and the rest of lts. Issues an error message if this can't be done. The labeled token list that is returned will never begin with "+" (Lex.Plus) or "(" (Lex.OpenPar). Either such a token will be consumed in the process of parsing a bigger regular expression, or an error will occur during the attempt to do so.

fromString s

inputs a regular expression from s.

input fil

inputs a regular expression from the file named by fil.

toPP reg

returns a pretty-printing expression for reg.

toString reg

pretty-prints reg to a string.

output reg

pretty-prints reg to the file named by fil.

validPath(reg, ns)

tests whether ns is a valid path for reg.

height reg

returns the height of reg.

size reg

returns the size of reg.

numLeaves reg

returns the number of leaves of reg.

select(reg, ns)

returns the subtree of reg pointed to by ns. Issues an error message if ns isn't a valid path for reg.

update(reg, ns, reg')

replaces the subtree of reg pointed to by ns with reg'. Issues an error message if ns isn't valid for reg.

maximumLengthPath reg

returns a leftmost, maximum length path for reg.

validLeafPath(reg, ns)

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

emptyStr

is EmptyStr.

emptySet

is EmptySet.

fromSym a

returns Sym a.

closure reg

returns Closure reg.

concat(reg1, reg2)

returns Concat(reg1, reg2).

union(reg1, reg2)

returns Union(reg1, reg2).

isEmptyStr reg

tests whether reg is EmptyStr.

isEmptySet reg

tests whether reg is EmptySet.

isSym reg

tests whether reg is a symbol.

isClosure reg

tests whether reg is a closure.

isConcat reg

tests whether reg is a concatenation.

isUnion reg

tests whether reg is a union.

compare(reg1, reg2)

is defined by:

  local
    fun kind EmptyStr    = 0
      | kind EmptySet    = 1
      | kind (Sym _)     = 2
      | kind (Closure _) = 3
      | kind (Concat _)  = 4
      | kind (Union _)   = 5
  in
    fun compare(reg, reg') =
          case Int.compare(kind reg, kind reg') of
               LESS    => LESS
             | EQUAL   =>
                 (case (reg, reg') of
                       (Sym a,              Sym a')               =>
                         Sym.compare(a, a')
                     | (Closure reg,        Closure reg')         =>
                         compare(reg, reg')
                     | (Concat(reg1, reg2), Concat(reg1', reg2')) =>
                         (case compare(reg1, reg1') of
                               LESS    => LESS
                             | EQUAL   => compare(reg2, reg2')
                             | GREATER => GREATER)
                     | (Union(reg1, reg2),  Union(reg1', reg2'))  =>
                         (case compare(reg1, reg1') of
                               LESS    => LESS
                             | EQUAL   => compare(reg2, reg2')
                             | GREATER => GREATER)
                     | _                                          => EQUAL)
             | GREATER => GREATER
  end

equal(reg1, reg2)

tests whether reg1 and reg2 are equal.

fromStr x

returns the regular expression that looks, in unabbreviated form, just like x. It's implemented by:

  fun fromStr nil       = EmptyStr
    | fromStr [b]       = Sym b
    | fromStr (b :: bs) = Concat(Sym b, fromStr bs)

power(reg, n)

raises reg to the power n. Issues an error message if n is negative.

alphabet reg

returns the alphabet of reg.

split

is defined by:

  local
    fun splt (Sym a)              = ([a], NONE)
      | splt (Concat(Sym a, reg)) =
          let val (bs, regOpt) = splt reg
          in (a :: bs, regOpt) end
      | splt reg                  = (nil, SOME reg)
  in
    fun split EmptyStr = (nil, NONE)
      | split reg      = splt reg
  end

genConcat

is defined by:

  fun genConcat nil           = EmptyStr
    | genConcat [reg]         = reg
    | genConcat (reg :: regs) = Concat(reg, genConcat regs)

genUnion

is defined by:

  fun genUnion nil           = EmptySet
    | genUnion [reg]         = reg
    | genUnion (reg :: regs) = Union(reg, genUnion regs)

rightConcat

is defined by:

  fun rightConcat(Concat(reg1, reg2), reg3) =
        Concat(reg1, rightConcat(reg2, reg3))
    | rightConcat(reg1, reg2)               = Concat(reg1, reg2)

rightUnion

is defined by:

  fun rightUnion(Union(reg1, reg2), reg3) =
        Union(reg1, rightUnion(reg2, reg3))
    | rightUnion(reg1, reg2)              = Union(reg1, reg2)

concatsToList

is defined by:

  fun concatsToList (Concat(reg1, reg2)) = reg1 :: concatsToList reg2
    | concatsToList reg                  = [reg]

unionsToList

is defined by:

  fun unionsToList (Union(reg1, reg2)) = reg1 :: unionsToList reg2
    | unionsToList reg                 = [reg]

sortUnions reg

returns genUnion regs, where regs is the result of sorting (using compare)

unionsToList
reg

into strictly ascending order (no duplicates).

allSym bs

returns the all symbols regular expression for bs.

allStr bs

returns the all strings regular expression for bs.

fromStrSet xs

returns

  genUnion(map fromStr (Set.toList xs))

type cc

The abstract type of closure complexities, consisting of nonempty lists of natural numbers sorted in (not necessarily strictly) descending order.

ccToList cc

returns cc.

singCC n

returns [n], if n is non-negative. Issues an error message, if n is negative.

unionCC(cc1, cc2)

returns the union of cc1 and cc2.

succCC cc

returns the successor of cc.

cc reg

returns the closure complexity of reg.

compareCC(cc1, cc2)

compares cc1 and cc2 in the total ordering on closure complexities.

numConcats reg

returns the number of concatenations in reg.

numSyms reg

returns the number of symbols in reg.

standardized reg

tests whether reg is standardized.

compareComplexity(reg1, reg2)

compares the complexities of reg1 and reg2: LESS means reg1 is strictly simpler (less complex) than reg2; EQUAL means reg1 and reg2 are equally simple/complex; and GREATER means reg1 is more complex (less simple) than reg2.

compareComplexityTotal(reg1, reg2)

returns

  case compareComplexity(reg1, reg2) of
       LESS    => LESS
     | EQUAL   => compare(reg1, reg2)
     | GREATER => GREATER

weaklySimplified reg

tests whether reg is weakly simplified.

weaklySimplify reg

returns the weak simplification of reg.

toStrSetOpt reg

returns SOME of the language generated by reg, if this language is finite, and NONE, if this language is infinite.

toStrSet reg

returns the language generated by reg. Issues an error message if the language generated by reg is infinite.

hasEmp reg

tests whether reg generates the empty string.

hasSym(a, reg)

tests whether reg generates [a].

obviousSubset(reg1, reg2)

tests whether reg1 is obviously a subset of reg2.

localSimplificationRelations(reg1, reg2)

returns:

LESS if reg1 is related to reg2 in the local simplification well-ordering;
EQUAL if reg1 is related to reg2 in the local simplification equivalence relation; and
GREATER if reg2 is related to reg1 in the local simplification well-ordering.

locallySimplified sub reg

If sub is a conservative approximation to subset testing, then locallySimplified tests whether reg is locallySimplified with respect to sub.

locallySimplifyTrace (NONE, sub) reg

If sub is a conservative approximation to subset testing, then locallySimplifyTrace returns the pair (true, reg'), where reg' is the local simplification of reg with respect to sub. locallySimplifyTrace issues a series of tracing messages, explaining its operation.

locallySimplifyTrace (SOME n, sub) reg

If sub is a conservative approximation to subset testing, then locallySimplifyTrace returns the pair (full, reg'), where reg' is the local simplification of reg with respect to sub, except that—at each recursive call of its principal function—it considers at most n structural reorganizations of its argument, and full will be true iff all structural reorganizations of reg' were considered, so that reg' is locally simplified. locallySimplifyTrace issues a series of tracing messages, explaining its operation. Issues an error message if n isn't at least 1.

locallySimplify

is like locallySimplifyTrace, except that no tracing messages are issued.

globallySimplified sub reg

If sub is a conservative approximation to subset testing, then globallySimplified tests whether reg is globally simplified with respect to sub.

globallySimplifyTrace (NONE, sub) reg

If sub is a conservative approximation to subset testing, then globallySimplifyTrace returns the pair (true, reg'), where reg' is the global simplification of reg with respect to sub. globallySimplifyTrace issues a series of tracing messages, explaining its operation.

globallySimplifyTrace (SOME n, sub) reg

If sub is a conservative approximation to subset testing, then globallySimplifyTrace returns the pair (full, reg'), where reg' is the global simplification of reg with respect to sub, except it curtails its search after considering n candidates, and full is true iff all candidates were considered, and so reg' is globally simplified. globallySimplifyTrace issues a series of tracing messages, explaining its operation. Issues an error message if n isn't at least 1.

globallySimplify

is like globallySimplifyTrace except that no tracing messages are issued.

renameAlphabet(reg, rel)

renames the alphabet of reg using the bijection rel. Issues an error message if rel is not a bijection from a superset of the alphabet of reg to some set.

rev reg

returns the reversal of reg.

prefix reg

returns the prefix-closure of reg.

jforlanNew()

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

jforlanEdit reg

invokes JForlan, letting the user edit reg, and returning the resulting regular expression 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

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

[ Top | Parent | Root | Contents | Index ]

Forlan Manual

The Reg Module

Synopsis

Interface

Description

The `Reg` Module