The RegExp structure

Synopsis

signature REGEXP
structure RegExp : REGEXP


This structure defines regular expressions and some functions to manipulate them. To print regular expressions, see ppRegExp.

Interface

datatype
  'a
  re
  = Atom of 'a| Plus of 'a re list| Star of 'a re| Times of 'a re list| Var of int
val Unit : 'a re
val Zero : 'a re
val It : 'a re -> 'a re
val Power : 'a re -> int -> 'a re
val Powers : 'a re -> int -> 'a re
exception Undefined
val freeVars : 'a re -> int Set.t
val subst : (int * 'a re) list -> 'a re -> 'a re
val substExp : ''a re * ''a re -> ''a re -> ''a re
val varNum : 'a re -> int
val maxVar : 'a re -> int
val nf : ''a re -> ''a re
val dnf : ''a re -> ''a re
val factorizel : ''a re -> ''a re
val factorizer : ''a re -> ''a re


Description

datatype
  'a
  re
  = Atom of 'a| Plus of 'a re list| Star of 'a re| Times of 'a re list| Var of int


the parameter type 'a is the type of alphabet.

Unit

expression for the neutral element of Times

Zero

expression for the neutral element of Plus

It r

expression for a product of at least one factors r

Power r i

expression for a product of i many factors r

Powers r i

expression for the sum of all powers of r with at most i factors r

exception Undefined


freeVars r

returns the set of (indices of) free variables of r

subst l r

returns the result of simultaneously substituing in r the expression si for variable i, for all (i,si) in list l

substExp (r1, r2) r

returns the result of substituting all occurrences of r1 by r2 in r

varNum r

returns the number of a variable expression r

maxVar r

returns the maximal index of the variables in r

nf r

returns a (quasi) normal form of r, using idempotency of Plus, associativity of Plus and Times, neutrality of Zero and Unit, annihilation by Zero, reflexivity and transitivity of Star, i.e. (x* + y + 1)* = (x + y)*, and 1* = 1 = 0*.

dnf r

returns a distributive normal form of r. Subexpressions of the form (Star s) remain unchanged

factorizel r

returns a left factorization of r, if this is a Plus of expressions, otherwise returns r. A left factorization of Plus rs extracts common left factors of summands in rs, using distribution laws.

factorizer r

returns a right factorization of r, if this is a Plus of expressions, otherwise returns r.

See Also

ppRegExp