This file is indexed.

/usr/share/hol88-2.02.19940316/Library/trs/name.ml is in hol88-library-source 2.02.19940316-35.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below.

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
% name.ml                                               (c) R.J.Boulton 1990 %
%----------------------------------------------------------------------------%


% Abstract datatype for string wildcards %

abstype wildchar = string

   % Function to convert a wildchar into a string %

   with show_wildchar w = rep_wildchar w

      % : (wildchar -> string) %

   % Function to make a wildchar from a string %

   % A string can only be made into a wildchar if it is of length 1. %

   and  make_wildchar s =

      % : (string -> wildchar) %

      if (length o explode) s = 1
      then abs_wildchar s
      else failwith `make_wildchar -- wildchar must be a single character`;;


% Abstract type for patterns used to match theory names and theorem names %

% The string represents the pattern. The first of the wildchars is the    %
% character which is to be used to mean `match any character'. The second %
% wildchar is the character which is to be used to mean `match any number %
% of characters (including none)'.                                        %

abstype namepattern = string # wildchar # wildchar

   % Function to convert a namepattern into its representing type %

   with show_namepattern np = rep_namepattern np

      % : (namepattern -> string # wildchar # wildchar) %

   % Function to make a namepattern from a string and two wildchars %

   % This will only succeed if the two wildchars are different. The pattern %
   % is simplified here, so that it need not be done every time a match is  %
   % performed.                                                             %

   and make_namepattern (s,w1,wn) =

      % : (string # wildchar # wildchar -> namepattern) %

      % Function to simplify a pattern, so that matching is easier. %

      % For example with wild1 = `?` and wildn = `*`, the following %
      % transformations are made:                                   %
      %                                                             %
      % `a***b`   --> `a*b`                                         %
      % `a*?*b`   --> `a?*b`                                        %
      % `a**?*?`  --> `a??*`                                        %
      % `a?b?`    --> `a?b?`                                        %
      % `a*?**b*` --> `a?*b*`                                       %

     (let simplify wild1 wildn sp =

         % : (wildchar -> wildchar -> string -> string) %

         % Subsidiary function to do most of the work. %

         % The boolean value is used to keep track of whether or not a      %
         % `wildn' character has been encountered. While passing through a  %
         % sequence of wildcard characters, `b' will be set to true if a    %
         % `wildn' is encountered, and the `wildn' will be omitted. At the  %
         % end of the wildcard sequence, a `wildn' will be inserted and `b' %
         % will be reset to false.                                          %

        (letrec simplify' s1 sn b l =

            % : (string -> string -> bool -> string list -> string list) %

            if (null l)
            then if b then [sn] else []
            else if (hd l) = sn then simplify' s1 sn true (tl l)
                 if (hd l) = s1 then s1.(simplify' s1 sn b (tl l))
                 else if b
                      then sn.(hd l).(simplify' s1 sn false (tl l))
                      else (hd l).(simplify' s1 sn false (tl l))

         % Call subsidiary function with wildcards (converted to strings), %
         % `wildn' inactive, and with the pattern converted to a list of   %
         % single-character strings. Then convert the processed list back  %
         % to a string.                                                    %

         in implode (simplify' (show_wildchar wild1) (show_wildchar wildn)
                                                         false (explode sp))
        )

      in if w1 = wn
         then failwith `make_namepattern -- wildchars must be different`
         else abs_namepattern ((simplify w1 wn s),w1,wn)
     );;


% Function to convert a namepattern into the three strings representing it %

let show_full_namepattern np =

   % : (namepattern -> string # string # string) %

   let (s,w1,wn) = show_namepattern np
   in  (s,show_wildchar w1,show_wildchar wn);;


% Function to make a namepattern from three strings %

% The first string represents the pattern. The second is the wildcard        %
% character which means `match any character', and the third is the wildcard %
% character which means `match any number of characters (including none)'.   %

let make_full_namepattern (s,c1,cn) =

   % : (string # string # string -> namepattern) %

   make_namepattern (s,make_wildchar c1,make_wildchar cn);;


% Default values for wildcards in namepatterns %

let wildchar1 = `?`
and wildcharn = `*`;;


% Function to convert a string into a namepattern using the default %
% wildcard characters.                                              %

let autonamepattern s = 

   % : (string -> namepattern) %

   make_full_namepattern (s,wildchar1,wildcharn);;


% Function to match a namepattern against a string %

let namematch p s =

   % : (namepattern -> string -> bool) %

   % Extract components of namepattern. %

   let (spatt,wild1,wildn) = show_full_namepattern p

       % Function to perform the match %

       % The last two arguments are the pattern and string converted to  %
       % lists of single-character strings.                              %
       % The function has no data to return, so it either returns (),    %
       % or it fails. This is done rather than returning a boolean value %
       % so that exception handling can be used for backtracking.        %

       % If both the pattern and the string are exhausted, succeed.      %
       % If only the pattern is exhausted, fail.                         %
       % If the remainder of the pattern is `wildn' on its own, succeed. %
       % Any other pattern matched against a null string must fail.      %

       % If the first character in the pattern is `wildn', try matching  %
       % it against nothing, and if this fails, try matching it against  %
       % one or more characters of the string (by recursion).            %

       % If the first character of the pattern is `wild1', match it to   %
       % the first character of the string, and try to match the tails.  %
       % Do the same if the head of the pattern equals the head of the   %
       % string. If the heads differ, fail.                              %

       % Note that this function has been specially written to be        %
       % efficient for the pattern `wildn` (on its own), i.e. for the    %
       % pattern which means `match anything'.                           %

       % The function does not cater for quotation of the characters     %
       % used as wildcards.                                              %

   in  letrec stringmatch w1 wn pl sl =

          % : (string -> string -> string list -> string list -> void) %

          if (null pl)
          then if (null sl)
               then ()
               else failwith `no match`
          else if ((hd pl = wn) & (null (tl pl)))
               then ()
               else if (null sl)
                    then failwith `no match`
                    else if (hd pl) = wn then (  (stringmatch w1 wn (tl pl) sl)
                                              ?? [`no match`]
                                                 (stringmatch w1 wn pl (tl sl))
                                              )
                         if (hd pl) = w1 then
                               (stringmatch w1 wn (tl pl) (tl sl))
                         if (hd pl) = (hd sl) then
                               (stringmatch w1 wn (tl pl) (tl sl))
                         else failwith `no match`

       % Convert the pattern and the string to a list of        %
       % single-character strings, and attempt a match. If the  %
       % match succeeds return true. If it fails, return false. %

       in can (stringmatch wild1 wildn (explode spatt)) (explode s);;


%----------------------------------------------------------------------------%