1signature regexpSyntax =
2sig
3  include Abbrev
4
5  val charset_ty : hol_type
6  val regexp_ty  : hol_type
7
8  val chset_tm   : term
9  val cat_tm     : term
10  val star_tm    : term
11  val or_tm      : term
12  val neg_tm     : term
13  val and_tm     : term
14
15  val mk_chset   : term -> term
16  val mk_star    : term -> term
17  val mk_neg     : term -> term
18  val mk_cat     : term * term -> term
19  val mk_or      : term list -> term
20  val mk_and     : term * term -> term
21
22  val dest_chset : term -> term
23  val dest_cat   : term -> term * term
24  val dest_star  : term -> term
25  val dest_neg   : term -> term
26  val dest_or    : term -> term list
27  val dest_and   : term -> term * term
28
29  val is_chset   : term -> bool
30  val is_cat     : term -> bool
31  val is_star    : term -> bool
32  val is_neg     : term -> bool
33  val is_or      : term -> bool
34  val is_and     : term -> bool
35
36  val vector_tm  : term
37  val mk_vector  : term -> term
38  val dest_vector : term -> term
39
40  val regexp_matcher_tm   : term
41  val mk_regexp_matcher   : term * term -> term
42  val dest_regexp_matcher : term -> term * term
43  val is_regexp_matcher   : term -> bool
44
45  val charset_to_term  : Regexp_Type.charset -> term
46  val term_to_charset  : term -> Regexp_Type.charset
47  val mk_regexp        : Regexp_Type.regexp -> term
48  val dest_regexp      : term -> Regexp_Type.regexp
49
50  val charset_empty_tm : term
51  val charset_full_tm  : term
52  val empty_tm         : term
53  val sigma_tm         : term
54  val epsilon_tm       : term
55  val sigmastar_tm     : term
56
57end
58