DEFINITIONS
 // ProB external predicates and function for regular expression matching
 // Syntax used is the ECMAScript syntax: http://www.cplusplus.com/reference/regex/ECMAScript/
 
 // the following is the B version of the C++ function regex_match
 // http://www.cplusplus.com/reference/regex/regex_match/
 
 // check if a string matches (entirely) a regular expression
 EXTERNAL_PREDICATE_REGEX_MATCH == (STRING*STRING);
 REGEX_MATCH(re_str,re_pat) == (1=1);
 
 // check if a string is a valid regular expression
 EXTERNAL_PREDICATE_IS_REGEX == (STRING);
 IS_REGEX(re_pat) == (1=1);
 
 // replace all occurence of a regular expression pattern by a replacement string:
 EXTERNAL_FUNCTION_REGEX_REPLACE == (STRING*STRING*STRING --> STRING);
 REGEX_REPLACE(re_str,re_pat,re_subst) == re_str;
 
 // find first match of a regular expression pattern:
 EXTERNAL_FUNCTION_REGEX_SEARCH_STR == (STRING*STRING --> STRING);
 REGEX_SEARCH_STR(re_str,re_pat) == re_str;

 // find first match of a regular expression pattern, return result as a record:
 EXTERNAL_FUNCTION_REGEX_SEARCH == 
    (STRING*INTEGER*STRING --> struct(length:INTEGER,position:INTEGER,
                              string:STRING, submatches:seq(STRING)));
 REGEX_SEARCH(re_str,re_from,re_pat) == rec(length:0,position:0,string:"",submatches:[]);

 // find all matches of a regular expression pattern:
 EXTERNAL_FUNCTION_REGEX_SEARCH_ALL == (STRING*STRING --> seq(STRING));
 REGEX_SEARCH_ALL(re_str,re_pat) == []
