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