class BACKTRACKING_REGULAR_EXPRESSION

Features exported to REGULAR_EXPRESSION_ITEM

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

context managment

group facilities

advancing the scan

advancing the scan

matching facilities

positionnal predicates

Common client features

Control of the exploration

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)

ensure

  • Result = last_match_succeeded
  • 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

  • group_count_set: group_count = pattern.group_count
  • match_reset: not last_match_succeeded

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

    set_group_last_index (group: INTEGER)

    Records the end of a group.

    require

      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

        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

        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

          push_alternative (alternative: ABSTRACT_BACKTRACKING_ALTERNATIVE)

          Pushs the 'alternative' before the continuation path.

          require

          • alternative_not_void: alternative /= Void

          ensure

            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.

            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

            ensure

            • Result = last_match_succeeded
            • 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

            ensure

            • Result = last_match_succeeded
            • 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

              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

                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

                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

                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

                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
                • 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 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

                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

                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.

                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