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 : bool * (reg * reg -> bool) -> reg -> bool
val globallySimplifyTrace : int option * bool * (reg * reg -> bool) -> reg -> bool * reg
val globallySimplify : int option * bool * (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

datatype concr
  = EmptyStr
  | EmptySet
  | Sym of Sym.sym
  | Closure of concr
  | Concat of concr * concr
  | Union of concr * concr
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:

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 (true, sub) reg
If sub is a conservative approximation to subset testing, then globallySimplified tests whether reg is distributively, globally simplified with respect to sub.

globallySimplified (false, sub) reg
If sub is a conservative approximation to subset testing, then globallySimplified tests whether reg is non-distributively, globally simplified with respect to sub.

globallySimplifyTrace (NONE, dist, 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 dist and sub. globallySimplifyTrace issues a series of tracing messages, explaining its operation.

globallySimplifyTrace (SOME n, dist, 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 dist and sub, except it curtails its search after considering n candidates, and full is true iff all n candidates were considered. 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 Version 4.12
Copyright © 2019 Alley Stoughton