1(*---------------------------------------------------------------------------*)
2(* Regular expressions and a regexp matcher.                                 *)
3(* Originated from Konrad Slind, tweaked by MJCG for Accellera PSL SEREs     *)
4(* An automata-based matcher added by Joe Hurd                               *)
5(*---------------------------------------------------------------------------*)
6
7signature regexpTools =
8sig
9
10(******************************************************************************
11* The trace levels of the regular expression library:
12* 0: silent
13* 1: 1 character (either - or +) for each list element processed
14* 2: matches as they are discovered
15* 3: transitions as they are calculated
16* 4: internal state of the automata
17******************************************************************************)
18
19val EVAL_BIGLIST : Thm.thm -> Thm.thm list
20
21(* Evaluating the Prefix operator on set regexps (like in Sugar) *)
22val set_sat_conv : Abbrev.conv
23
24(* Evaluating the Prefix operator on character regexps *)
25val chr_sat_conv : Abbrev.conv
26
27(* Set this to a SAT solver for evaluating the Prefix operator *)
28val prefix_sat_conv : Abbrev.conv ref        (* by default = set_sat_conv *)
29
30(* Exporting state machines
31val export_dfa : Term.term list -> Term.term -> (int * bool * int list) list
32
33val export_set_dfa :
34  Term.term list -> Term.term ->
35  (Term.term * bool) list list * (int * bool * int list) list
36*)
37
38datatype 'a condition =
39  Leaf of 'a
40| Branch of string * 'a condition * 'a condition
41
42val extract_dfa :
43  Term.term list -> Term.term ->
44  (int * Term.term * (bool * Thm.thm) * (int * Thm.thm) condition) list
45
46val LINE_LENGTH : int ref
47
48val verilog_dfa :
49  {name : string, alphabet : Term.term list, regexp : Term.term} -> string
50
51end
52