class BACKTRACKING_REGULAR_EXPRESSION

All features

matcher for regular expressions

Direct parents

conformant parents

BACKTRACKING, REGULAR_EXPRESSION

non-conformant parents

REGULAR_EXPRESSION_STRING_SCANNER

Summary

creation features

exported features

common

creation

backtracked search

context managment

group facilities

advancing the scan

advancing the scan

matching facilities

positionnal predicates

internal

Common client features

Control of the exploration

Internal

Specific to sequences

Specific to alternatives

internal: allocation and collection

the pools

matching capabilities

substitution capabilities

Error informations

make

basic

error managment

scanning

Details

make

Creation.

set_scanned_string (string: STRING)

Set 'scanned_string' to 'string'.

ensure

  • match_reset: not last_match_succeeded
  • has_no_error: not has_error
  • definition: scanned_string = string
  • at_the_begin: position = scanned_string.lower

last_match_succeeded: BOOLEAN

True if the last match (match_first or match_next) operation was a success.

group_count: INTEGER

The count of groups

invalidate_last_match

Used to prevent 2 substitutions without intermediate matching.

require

  • True
  • last_match_succeeded

ensure

  • not last_match_succeeded
  • not can_substitute

basic_match_first

Starts to match and try to find the first substring of 'scanned_string' that matches the regular expression.

require

  • scanned_string_not_void: scanned_string /= Void

ensure

  • scanned_string_remains: scanned_string = old scanned_string

basic_match_next

Continues to match and try to find the next substring of 'scanned_string' that matches the regular expression.

require

  • scanned_string_not_void: scanned_string /= Void
  • has_result: last_match_succeeded
  • at_good_position: position = last_match_last_index + 1

ensure

  • scanned_string_remains: scanned_string = old scanned_string

match_from (text: STRING, first_index: INTEGER): BOOLEAN

Returns True if Current regular_expression can match the text starting from first_index.

See also match, last_match_succeeded, last_match_first_index.

require

  • text /= Void
  • first_index.in_range(1, text.count + 1)
  • save_matching_text(text)

ensure

  • Result = last_match_succeeded
  • Result implies valid_substrings(text)
  • Result implies last_match_first_index >= first_index
  • Result implies last_match_first_index.in_range(text.lower, text.upper + 1)
  • Result implies last_match_first_index <= last_match_last_index + 1

matches_only_current_position: BOOLEAN

Does the matching occur only from current position? If that falg is True then:

  * if match succeeds then position is advanced
  * if match fails the position remains
see also 'goto_position'

set_matches_only_current_position (value: BOOLEAN)

Sets 'matches_only_current_position' to 'value'.

ensure

  • definition: matches_only_current_position = value

make

Creation.

set_pattern (pattern: BACKTRACKING_REGULAR_EXPRESSION_PATTERN)

Set the matched pattern.

require

  • valid_pattern: pattern.is_valid

ensure

  • value_set: root_node = pattern.root
  • group_count_set: group_count = pattern.group_count
  • match_reset: not last_match_succeeded

root_node: BACKTRACKING_NODE

The regular expression to be matched.

do_match

Main matching routine. Starting at the current position it tries to match the current scanned_string against the current regular expression.

require

  • scanned_string_not_void: scanned_string /= Void

context_type_frame: INTEGER
context_frame_cut: INTEGER
context: FAST_ARRAY [E_][INTEGER]
context_top: INTEGER
context_clear
context_push
context_restore
context_restore_and_pop
context_cut
set_group_first_index (group: INTEGER)

Records the beginning of a group.

require

  • valid_group: group.in_range(0, substrings_first_indexes.upper)

set_group_last_index (group: INTEGER)

Records the end of a group.

require

  • valid_group: group.in_range(0, substrings_last_indexes.upper)

clear_group (group: INTEGER)

Set 'group' to empty string.

clear_all_groups

Set all groups to empty string.

saved_look_position: INTEGER

the saved position for look ahead or look behind

begin_look_ahead

Begins to look-ahead.

require

  • no_look_begun: saved_look_position = 0
  • valid_position: position > 0

ensure

  • look_ahead_begun: saved_look_position > 0
  • position_saved: position = saved_look_position

end_look_ahead

Terminates to look-ahead.

require

  • look_ahead_begun: saved_look_position > 0

ensure

  • position_restored: position = old saved_look_position
  • no_look_begun: saved_look_position = 0
  • valid_position: position > 0

begin_look_behind

Begins to look-behind.

require

  • no_look_begun: saved_look_position = 0
  • valid_position: position > 0

ensure

  • look_behind_begun: saved_look_position < 0
  • position_saved: old position = -saved_look_position
  • direction_changed: direction = -1

end_look_behind

Terminates to look-behind.

require

  • look_behind_begun: saved_look_position < 0

ensure

  • position_restored: position = - old saved_look_position
  • no_look_begun: saved_look_position = 0
  • valid_position: position > 0
  • direction_changed: direction = 1

direction: INTEGER

direction to advance (normal is +1, inverse is -1)

advance

Goes to the next character

require

  • not_at_end: not end_of_input

advance_end_of_line

Skips the end of line. Must be at end of a line.

require

  • at_end_of_line: end_of_input or else is_end_of_line

match_character (char: CHARACTER)

If the character 'char' matches then advance and continue else backtrack.

match_character_no_case (char: CHARACTER)

If the character 'char' matches then advance and continue else backtrack. Case does not care.

require

  • is_upper_character: char = char.to_upper

match_string (text: STRING)

If the string 'text' matches then advance and continue else backtrack.

match_string_no_case (text: STRING)

If the string 'text' matches then advance and continue else backtrack. Case does not care.

require

  • is_upper_string:

    all letters of 'text' are upper case

match_previous_group (group: INTEGER)

If the previous 'group' matches then advance and continue else backtrack.

match_previous_group_no_case (group: INTEGER)

If the previous 'group' matches then advance and continue else backtrack. Case does not care.

is_begin_of_text: BOOLEAN

True if at begin of the text

ensure

  • Result implies is_begin_of_line

is_end_of_text (really: BOOLEAN): BOOLEAN

True if at end of the text

ensure

  • Result implies is_end_of_line or else really and end_of_input

is_begin_of_line: BOOLEAN

True if at begin of a line

is_end_of_line: BOOLEAN

True if at end of a line

is_begin_of_word: BOOLEAN

True if at begin of a word

is_end_of_word: BOOLEAN

True if at end of a word

set_current_node (node: BACKTRACKING_NODE)

Set the next node of the BACKTRACKING_NODE graph to be evaluated.

ensure

  • definition: current_node = node

push_and (node: BACKTRACKING_NODE)

Pushes 'node' in front of the continuation path.

require

  • node_not_void: node /= Void

push_and_list (list: BACKTRACKING_NODE_AND_LIST)

Pushes 'list' in front of the continuation path.

require

  • list_not_void: list /= Void

push_or (node: BACKTRACKING_NODE)

Pushes 'node' in front of the possible alternatives.

require

  • node_not_void: node /= Void

push_or_list (list: BACKTRACKING_NODE_OR_LIST)

Pushes 'list' in front of the possible alternatives.

require

  • list_not_void: list /= Void

current_node: BACKTRACKING_NODE

Current node of the BACKTRACKING_NODE graph to be evaluated.

evaluate_current_state

That feature is called to evaluate the current state

search_first

Resets all and searchs the first solution. The current state must be set. It is the first state, the root of the search. When the feature returns, 'search_is_success' must be checked to know if a solution was found. When search_is_success=False, it means that there is no solution at all. Conversly, if search_is_success=True, then the first solution is found and 'search_next' can be called to get the next solution if it exists.

ensure

  • success_or_off: search_is_success and not is_off or is_off and not search_is_success

search_next

Searchs the next solution. When the feature returns, 'search_is_success' must be checked to know if a solution was found. When search_is_success=False at the end, it means that there is no more solution. Conversly, if search_is_success=True, then a solution is found and 'search_next' can be called again to get the next solution.

require

  • last_search_was_a_success: search_is_success

ensure

  • success_or_off: search_is_success and not is_off or is_off and not search_is_success

search_is_success: BOOLEAN

True when search is successfull

is_off: BOOLEAN

True when search is finished

ensure

  • definition: Result = not search_is_success

clear

Clears the current state to nothing.

ensure

  • cleared: is_cleared
  • no_solution: is_off

is_cleared: BOOLEAN

True if no partial data remain in the current state

ensure

  • no_solution_when_cleared: Result implies is_off

push_sequence (sequence: ABSTRACT_BACKTRACKING_SEQUENCE)

Pushs the 'sequence' in front of the continuation path.

require

  • sequence_not_void: sequence /= Void

ensure

  • is_on_top: top_sequence = sequence
  • is_first_continuation: current_continuation = sequence
  • previous_top_linked: top_sequence.previous = old top_sequence
  • previous_continuation_linked: top_sequence.continuation = old current_continuation

push_alternative (alternative: ABSTRACT_BACKTRACKING_ALTERNATIVE)

Pushs the 'alternative' before the continuation path.

require

  • alternative_not_void: alternative /= Void

ensure

  • is_on_top: top_alternative = alternative
  • previous_top_linked: top_alternative.previous = old top_alternative
  • top_sequence_recorded: top_alternative.top_sequence = old top_sequence
  • continuation_recorded: top_alternative.continuation = old current_continuation

continue

Continues the exploration of the current path.

backtrack

Stops the exploration of the current path and tries to explore the next alternative path.

push_cut_point

Inserts a cut point into the continuation path. The inserted cut point records the current to of the alternatives.

cut

Removes the alternatives until the one recorded by the next cut point in the continuation path.

cut_all

Cuts all alternatives.

stop_search_loop: BOOLEAN

True if at the end of a search

search

Common search loop to search_first and serch_next

ensure

  • stop_search_loop

cut_until (alternative: ABSTRACT_BACKTRACKING_ALTERNATIVE)

Cut all alternatives until 'alternative'. To cut an alternative is currently to remove it.

ensure

  • definition: top_alternative = alternative

top_sequence: ABSTRACT_BACKTRACKING_SEQUENCE

Stack of sequences represented by its top (can be Void)

current_continuation: ABSTRACT_BACKTRACKING_SEQUENCE

The current continuation path

pop_sequence

Removes the current sequence and replace it by the next sequence in the continuation path.

require

  • top_sequence /= Void
  • current_continuation /= Void

top_alternative: ABSTRACT_BACKTRACKING_ALTERNATIVE

Stack of alternatives represented by its top (can be Void)

continue_alternative

Returns to the alternative on the top of the stack and put its saved continuation path as the current continuation path.

require

  • top_alternative /= Void

ensure

  • alternative_remain: top_alternative = old top_alternative

pop_alternative

Returns to the alternative on the top of the stack and put its saved continuation path as the current continuation path. Remove the alternative from the stack of alternatives. Same as 'continue_alternative' but also removes the alternative.

require

  • top_alternative /= Void

ensure

  • alternative_poped: top_alternative = old top_alternative.previous
  • top_sequence_restored: top_sequence = old top_alternative.top_sequence
  • continuation_restored: current_continuation = old top_alternative.continuation

remove_top_sequence

Removes the top sequence.

require

  • top_sequence /= Void

ensure

  • top_sequence = old top_sequence.previous

remove_top_alternative

Removes the top alternative.

require

  • top_alternative /= Void

ensure

  • top_alternative = old top_alternative.previous

pool_of_cut_points: ABSTRACT_BACKTRACKING_POOL_OF_CUT_POINT

Bank of cut points

pool_of_sequence: BACKTRACKING_POOL_OF_SEQUENCE
pool_of_sequence_list: BACKTRACKING_POOL_OF_SEQUENCE_LIST
pool_of_alternative: BACKTRACKING_POOL_OF_ALTERNATIVE
pool_of_alternative_list: BACKTRACKING_POOL_OF_ALTERNATIVE_LIST
match (text: STRING): BOOLEAN

Returns True if Current regular_expression can match the text.

See also match_next, match_from, last_match_succeeded, last_match_first_index.

require

  • text /= Void
  • save_matching_text(text)

ensure

  • Result = last_match_succeeded
  • Result implies valid_substrings(text)
  • Result implies last_match_first_index.in_range(text.lower, text.upper + 1)
  • Result implies last_match_first_index <= last_match_last_index + 1

match_next (text: STRING): BOOLEAN

Returns True if Current regular_expression can match the same text one more time. Must be called after a successful match or math_from or match_next using the same text.

See also match, match_from, last_match_succeeded.

require

  • text /= Void
  • last_match_succeeded
  • text.has_prefix(last_match_text)
  • save_matching_text(text)

ensure

  • Result = last_match_succeeded
  • Result implies valid_substrings(text)
  • Result implies last_match_first_index.in_range(text.lower, text.upper + 1)
  • Result implies last_match_first_index <= last_match_last_index + 1

last_match_first_index: INTEGER

The starting position in the text where starts the sub-string who is matching the whole pattern.

See also match, match_from.

require

  • last_match_succeeded

ensure

  • Result > 0

last_match_last_index: INTEGER

The last position in the text where starts the sub-string who is matching the whole pattern.

See also match, match_from.

require

  • last_match_succeeded

ensure

  • Result + 1 >= last_match_first_index

last_match_count: INTEGER

Length of the string matching the whole pattern.

See also last_match_first_index, last_match_last_index, match, match_from.

require

  • last_match_succeeded

ensure

  • Result >= 0
  • definition: Result = last_match_last_index - last_match_first_index + 1

ith_group_matched (i: INTEGER): BOOLEAN

Did the ith group matched during last match?

See also group_count, ith_group_first_index.

require

  • i.in_range(0, group_count)
  • last_match_succeeded

ith_group_first_index (i: INTEGER): INTEGER

First index in the last matching text of the ith group of Current.

See also group_count.

require

  • i.in_range(0, group_count)
  • last_match_succeeded
  • ith_group_matched(i)

ensure

  • Result.in_range(0, last_match_text.upper + 1)

ith_group_last_index (i: INTEGER): INTEGER

Last index in the last matching text of the ith group of Current.

See also ith_group_first_index, group_count.

require

  • i.in_range(0, group_count)
  • last_match_succeeded
  • ith_group_matched(i)

ensure

  • Result.in_range(ith_group_first_index(i) - 1, last_match_text.upper)

ith_group_count (i: INTEGER): INTEGER

Length of the ith group of Current in the last matching.

See also ith_group_first_index, append_ith_group, group_count.

require

  • i.in_range(0, group_count)
  • last_match_succeeded
  • ith_group_matched(i)

ensure

  • Result >= 0
  • Result = ith_group_last_index(i) - ith_group_first_index(i) + 1

append_heading_text (text: STRING, buffer: STRING)

Append in buffer the text before the matching area. text is the same as used in last matching.

See also append_pattern_text, append_tailing_text, append_ith_group.

require

  • text /= Void
  • buffer /= Void
  • last_match_succeeded
  • text.has_prefix(last_match_text)

ensure

  • buffer.count = old buffer.count + last_match_first_index - 1

append_pattern_text (text: STRING, buffer: STRING)

Append in buffer the text matching the pattern. text is the same as used in last matching.

See also append_heading_text, append_tailing_text, append_ith_group.

require

  • text /= Void
  • buffer /= Void
  • last_match_succeeded
  • text.has_prefix(last_match_text)

ensure

  • buffer.count = old buffer.count + last_match_count

append_tailing_text (text: STRING, buffer: STRING)

Append in buffer the text after the matching area. text is the same as used in last matching.

See also append_heading_text, append_pattern_text, append_ith_group.

require

  • text /= Void
  • buffer /= Void
  • last_match_succeeded
  • text.is_equal(last_match_text)

ensure

  • buffer.count = old buffer.count + text.count - last_match_last_index

append_ith_group (text: STRING, buffer: STRING, i: INTEGER)

Append in buffer the text of the ith group. text is the same as used in last matching.

See also append_pattern_text, group_count.

require

  • text /= Void
  • buffer /= Void
  • last_match_succeeded
  • text.is_equal(last_match_text)
  • i.in_range(0, group_count)
  • ith_group_matched(i)

ensure

  • buffer.count = old buffer.count + ith_group_count(i)

prepare_substitution (p: STRING)

Set pattern p for substitution. If pattern p is not compatible with the Current regular expression, the pattern_error_message is updated as well as pattern_error_position.

See also substitute_in, substitute_for, substitute_all_in, substitute_all_for.

require

  • p /= Void

ensure

  • substitution_pattern_ready implies valid_substitution
  • substitution_pattern_ready xor pattern_error_message /= Void

last_substitution: STRING

You need to copy this STRING if you want to keep it.

substitute_for (text: STRING)

This call has to be precedeed by a sucessful matching on the same text. Then the substitution is made on the matching part. The result is in last_substitution.

See also prepare_substitution, last_substitution, substitute_in.

require

  • can_substitute
  • text /= Void
  • text.is_equal(last_match_text)

ensure

  • last_substitution /= Void
  • substitution_pattern_ready
  • only_one_substitution_per_match: not can_substitute

substitute_in (text: STRING)

This call has to be precedeed by a sucessful matching on the same text. Then the substitution is made in text on the matching part (text is modified).

See also prepare_substitution, substitute_for.

require

  • can_substitute
  • text /= Void
  • text.is_equal(last_match_text)

ensure

  • substitution_pattern_ready
  • only_one_substitution_per_match: not can_substitute

substitute_all_for (text: STRING)

Every matching part is substituted. No preliminary matching is required. The result is in last_substitution.

See also prepare_substitution, last_substitution, substitute_all_in.

require

  • substitution_pattern_ready
  • text /= Void

ensure

  • last_substitution /= Void
  • substitution_pattern_ready

substitute_all_in (text: STRING)

Every matching part is substituted. No preliminary matching is required. text is modified according to the substitutions is any.

See also prepare_substitution, last_substitution, substitute_all_for.

require

  • substitution_pattern_ready
  • text /= Void

ensure

  • substitution_pattern_ready

can_substitute: BOOLEAN

Substitution is only allowed when some valid substitution pattern has been registered and after a sucessful pattern matching.

See also substitute_in, substitute_for.

ensure

  • definition: Result = (substitution_pattern_ready and last_match_succeeded)

substitution_pattern_ready: BOOLEAN

True if some valid substitution pattern has been registered.

pattern_error_message: STRING

Error message for the substitution pattern.

See also prepare_substitution.

pattern_error_position: INTEGER

Error position in the substitution pattern.

See also prepare_substitution.

save_matching_text (text: STRING): BOOLEAN

Used in assertion only. Side-effect: save the text

ensure

  • Result

    Assertion only feature

valid_substrings (text: STRING): BOOLEAN

Used in assertion only.

require

  • last_match_succeeded

ensure

  • Result

    Method for assertion only (error position is element item i)

valid_substitution: BOOLEAN

Used in assertion only.

ensure

  • Result

    Method for assertion only

substitute_all_without_tail (text: STRING): INTEGER

Substitute all matching parts from text. The resulting text is in last_substitution, excepted the end. The part of text from Result up to the end is not copied.

require

  • substitution_pattern_ready
  • text /= Void

ensure

  • last_substitution /= Void
  • substitution_pattern_ready

substrings_first_indexes: ARRAY [E_][INTEGER]

Item(0) is the starting position in the text where starts the substring who is matching the whole pattern. Next elements are the starting positions in the text of substrings matching sub-elements of the pattern.

Elements before item(0) refers to positions in the substitution_pattern. They are stored in reverse order, the first verbatim string beeing at index -1, the second one at index -2...

substrings_last_indexes: ARRAY [E_][INTEGER]

The ending position of the string starting at position found in matching_position at the same index.

substitution_pattern: STRING
compiled_substitution_pattern: FAST_ARRAY [E_][INTEGER]

This array describe the substitution text as a suite of strings from substrings_first_indexes.

substitution_buffer: STRING
last_match_text: STRING

For assertion only.

last_match_text_memory: STRING

For assertion only.

make

Initialise the attributes.

scanned_string: STRING

The expression being currently build.

set_scanned_string (string: STRING)

Set the 'scanned_string' with 'string'.

ensure

  • has_no_error: not has_error
  • definition: scanned_string = string
  • at_the_begin: position = scanned_string.lower

has_error: BOOLEAN

True when an error was encountered

clear_error

Remove the error flag

ensure

  • has_no_error: not has_error

last_error: STRING

Returns a string recorded for the error.

require

  • has_error: has_error

ensure

  • not_void: Result /= Void

set_error (message: STRING)

Set has_error and last_error. The explaining error string 'last_error' is created as follow: "Error at position 'position': 'message'.".

require

  • message_not_void: message /= Void
  • has_no_error: not has_error

ensure

  • has_error: has_error

position: INTEGER

The scanned position. It is the position of 'last_character'.

last_character: CHARACTER

The scanned character. The last character readden from 'scanned_string'.

valid_last_character: BOOLEAN

True when 'last_character' is valid. Is like 'scanned_string.valid_index(position)'

valid_previous_character: BOOLEAN

True if the position-1 is a valid position.

require

  • scanned_string /= Void

ensure

  • definition: Result = scanned_string.valid_index(position - 1)

previous_character: CHARACTER

The character at position-1.

require

  • valid_previous_character

ensure

  • definition: Result = scanned_string.item(position - 1)

valid_next_character: BOOLEAN

True if the position+1 is a valid position.

require

  • scanned_string /= Void

ensure

  • definition: Result = scanned_string.valid_index(position + 1)

next_character: CHARACTER

The character at position+1.

require

  • valid_next_character

ensure

  • definition: Result = scanned_string.item(position + 1)

end_of_input: BOOLEAN

True when all the characters of 'scanned_string' are scanned.

ensure

  • implies_last_character_not_valid: Result implies not valid_last_character

goto_position (pos: INTEGER)

Change the currently scanned position to 'pos'. Updates 'last_character' and 'valid_last_character' to reflect the new position value.

require

  • has_no_error: not has_error
  • scanned_string /= Void

ensure

  • has_no_error: not has_error
  • position_set: position = pos
  • validity_updated: valid_last_character = scanned_string.valid_index(position)
  • character_updated: valid_last_character implies last_character = scanned_string.item(position)

read_character

Reads the next character.

require

  • has_no_error: not has_error
  • not_at_end: not end_of_input

ensure

  • next_position: position > old position
  • has_no_error: not has_error

read_integer

Reads an integer value beginning at the currently scanned position. The readen value is stored in 'last_integer'.

require

  • has_no_error: not has_error
  • not_at_end: not end_of_input
  • begin_with_a_digit: last_character.is_decimal_digit

ensure

  • has_no_error: not has_error
  • digits_eaten: end_of_input or else not last_character.is_decimal_digit

saved_position: INTEGER

The saved position (only one is currently enougth).

save_position

Saves the current scanning position.

require

  • not_at_end: not end_of_input

ensure

  • not_at_end: not end_of_input
  • position_kept: position = old position
  • saved_position_set: saved_position = position

restore_saved_position

Restore the scanning position to the last saved one.

ensure

  • position_restored: position = old saved_position
  • not_at_end: not end_of_input

last_string: STRING

A string buffer.

last_integer: INTEGER

An integer buffer.

Class invariant