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