This file is indexed.

/usr/share/hol88-2.02.19940316/Library/trs/struct.ml is in hol88-library-source 2.02.19940316-19.

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
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
% struct.ml                                             (c) R.J.Boulton 1990 %
%----------------------------------------------------------------------------%


% Function to merge two association lists, failing if the lists are %
% inconsistent.                                                     %

% The first element of the pair at the head of l2 is looked-up in l1. If the %
% second element of the pair obtained is equal to the second element of the  %
% pair at the head of l2, then the head of l2 is discarded. Otherwise, the   %
% merge fails. If the look-up in l1 fails, the head of l2 is retained.       %

letrec merge l1 l2 =

   % : ((* # **) list -> (* # **) list -> (* # **) list) %

   if (null l2)
   then l1
   else ((let p = assoc (fst (hd l2)) l1
          in  if (snd p = snd (hd l2))
              then (merge l1 (tl l2))
              else failwith `merge`)

        ??[`assoc`] (hd l2).(merge l1 (tl l2))

        );;


% Function to merge two `match' lists. %

let join (avtl,attl) ((bvtl,bttl) : (term # term) list # (type # type) list) =

   % : ((term # term) list # (type # type) list ->   %
   %    (term # term) list # (type # type) list ->   %
   %    (term # term) list # (type # type) list    ) %

   (merge avtl bvtl,merge attl bttl) ??[`merge`] failwith `no match`;;


% Function to remove a bound-variable from a `match' list. %

% Any pairs in the variable-term association list which have the %
% bound-variable as their first element are filtered out.        %

let remove_bv bv ((vtl,ttl) : (term # term) list # (type # type) list) =

   % : (term -> (term # term) list # (type # type) list ->    %
   %                 (term # term) list # (type # type) list) %

   (filter (\x.not ((fst x) = bv)) vtl,ttl);;


% Function for matching two types. %

% The first type given, p, must be the more general.                         %

% If p is a simple polymorphic type (i.e. one containing no constructors)    %
% then it can match any type. A single item association list is constructed  %
% from the two types in such a case.                                         %

% If p is not a simple type, it is split up into a constructor and a list of %
% simpler types. An attempt is made to split t, also. If this fails, then no %
% match can be made. If the constructors obtained from p and t are different %
% then the match must fail. The lists of simpler types obtained from         %
% decomposing p and t are converted to a list of pairs, the match failing if %
% the original lists were not of the same length. The function is then       %
% applied recursively to each pair of the new list, and the results are      %
% merged. If merging fails, the whole match fails.                           %

letrec match_type p t =

   % : (type -> type -> (type # type) list) %

   if (is_vartype p)
   then [(p,t)]
   else let (pc,ptypl) = dest_type p
        and (tc,ttypl) = ((dest_type t) ? failwith `no match`)
        in  if (pc = tc)
            then ((itlist merge (map (\(x,y).match_type x y)
                                        (combine (ptypl,ttypl))) [])
                 ??[`merge`;`combine`] failwith `no match`
                 )
            else failwith `no match`;;


% Function for matching two terms. %

% The first term given, p, must be the more general.                        %

% The function consists of four cases.                                      %

% p is a constant. If t is not a constant, the match fails. If the names of %
% p and t are different, the match fails. Constants cannot be wildcards, so %
% only the types need adding to the `match' list. One might think the match %
% should fail if the types are different, but this is not the case.         %
% Consider the `=' function, for instance. The types must match, however.   %

% p is a variable. A variable can match any term, provided its type can be  %
% matched to that of the term.                                              %

% p is an abstraction. An abstraction can only match another abstraction.   %
% p and t are decomposed into their bound-variables and bodies. The bound-  %
% variables are matched to obtain the type matchings. The bodies are also   %
% matched. The resultant matchings are then merged, and the bound-variable  %
% is then removed from the variable-term list to allow for renaming of      %
% bound-variables. Note that the merge has to be done before the bound-var. %
% is removed to ensure the bound-variables correspond in the body.          %

% p is a combination. A combination can only match another combination.     %
% p and t are decomposed into their rators and rands. The two rators are    %
% matched against each other. The two rands are matched. Then the resulting %
% `match' lists are merged.                                                 %

letrec match_term p t =

   % : (term -> term -> (term # term) list # (type # type) list) %

   if (is_const p) then if (is_const t)
                        then if (fst (dest_const p) = fst (dest_const t))
                             then ([],match_type (type_of p) (type_of t))
                             else failwith `no match`
                        else failwith `no match`
   if (is_var p) then ([(p,t)],match_type (type_of p) (type_of t))
   if (is_abs p) then
     (let (pbv,pbody) = dest_abs p
      and (tbv,tbody) = ((dest_abs t) ? failwith `no match`)
      in  remove_bv pbv (join (match_term pbv tbv) (match_term pbody tbody)))
   if (is_comb p) then
     (let (prator,prand) = dest_comb p
      and (trator,trand) = ((dest_comb t) ? failwith `no match`)
      in  join (match_term prator trator) (match_term prand trand))
   else fail;;


% Function to match a term pattern inside a term %

% The function applies match_term to the pattern and the term. If this fails %
% the function is called recursively on any possible sub-terms of the term.  %
% If all these attempts to match fail, the whole evaluation fails.           %

letrec match_internal_term p t =

   % : (term -> term -> (term # term) list # (type # type) list) %

   match_term p t
   ??[`no match`]             (match_internal_term p (rator t))
   ??[`no match`;`dest_comb`] (match_internal_term p (rand t))
   ??[`no match`;`dest_comb`] (match_internal_term p (snd (dest_abs t)))
   ??[`no match`;`dest_abs`]  failwith `no match`;;


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


% Abstract datatype for wildcard variables to be used in pattern matching %

abstype wildvar = term

   % Function to convert a wildvar into a term %

   with show_wildvar w = rep_wildvar w

       % : (wildvar -> term) %

   % Function to make a wildvar from a term. The term must be a variable %

   and  make_wildvar t =

       % : (term -> wildvar) %

       if (is_var t)
       then (abs_wildvar t)
       else failwith `make_wildvar -- term is not a variable`;;


% Function to make a list of wildvars out of a list of terms %

let wildvarlist varl = map make_wildvar varl;;

   % : (term list -> wildvar list) %


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


% Abstract datatype for wildcard types to be used in pattern matching %

abstype wildtype = type

   % Function to convert a wildtype into a type %

   with show_wildtype w = rep_wildtype w

       % : (wildtype -> type) %

   % Function to make a wildtype from a type.         %
   % The type must be a `primitive' polymorphic type. %

   and  make_wildtype t =

       % : (type -> wildtype) %

       if (is_vartype t)
       then (abs_wildtype t)
       else failwith `make_wildtype -- type is not polymorphic`;;


% Function to make a list of wildtypes out of a list of types %

let wildtypelist typl = map make_wildtype typl;;

   % : (type list -> wildtype list) %


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


% Abstract datatype for patterns used to match terms %

abstype termpattern = term # wildvar list # wildtype list

   % Function to convert a termpattern to its representing type %

   with show_termpattern p = rep_termpattern p

       % : (termpattern -> (term # wildvar list # wildtype list)) %

   % Function to make a termpattern from a term, a list of wildcard variables %
   % and a list of wildcard types.                                            %

   and  make_termpattern (tm,wvl,wtl) =

       % : ((term # wildvar list # wildtype list) -> termpattern) %

       % Convert wildcard variables to their representing variables %

       let varl = map show_wildvar wvl

       % Convert wildcard types to their representing type %

       and typl = map show_wildtype wtl

       % Form a termpattern if and only if the lists of wildcard variables %
       % and wildcard types are sets (i.e. contain no repetitions) and all %
       % the wildcard variables specified are free variables in tm and all %
       % the wildcard types specified are `primitive' polymorphic types    %
       % occurring in tm.                                                  %

       in  if (no_rep varl) then
              if (no_rep typl) then
                 if (is_subset (get_freevars tm) varl) then
                    if (is_subset (get_primvartypes tm) typl) then

                       (abs_termpattern (tm,wvl,wtl))

                    else failwith `make_termpattern -- wildtype not in term`
                 else failwith `make_termpattern -- wildvar not in term`
              else failwith `make_termpattern -- duplicate wildtype`
           else failwith `make_termpattern -- duplicate wildvar`;;


% Function to convert a termpattern into its representing type, and the %
% wildvars and wildtypes within that to their representing types.       %
% So, function makes all of a termpattern visible.                      %

let show_full_termpattern p =

   % : (termpattern -> (term # term list # type list)) %

   let (tm,wvl,wtl) = show_termpattern p
   in  (tm,(map show_wildvar wvl),(map show_wildtype wtl));;


% Function to make a termpattern from a term, a list of terms, and a list of %
% types. The term represents the pattern. The list of terms represents the   %
% variables which are to be taken as wildcards, and the list of types        %
% represents the `primitive' polymorphic types which are to be taken as      %
% wildcards.                                                                 %

let make_full_termpattern (tm,terml,typel) =

   % : ((term # term list # type list) -> termpattern) %

   make_termpattern (tm,wildvarlist terml,wildtypelist typel);;


% Function to make a termpattern out of a term by using the free variables in %
% the term as wildvars and the `primitive' polymorphic types as wildtypes.    %

let autotermpattern t =

   % : (term -> termpattern) %

   make_full_termpattern (t,get_freevars t,get_primvartypes t);;


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


% Abstract datatype for the result of matching a termpattern against a term %

abstype matching = ((wildvar # term) list # (wildtype # type) list)

   % Function to convert a matching to its representing type %

   with show_matching m = rep_matching m

       % : (matching -> ((wildvar # term) list # (wildtype # type) list)) %

   % A matching with no bindings %

   and  null_matching = abs_matching ([],[])

       % : (matching) %

   % Function to form a matching from a termpattern and a term %

   and  make_matching p t =

       % : (termpattern -> term -> matching) %

           % Extract low-level components of termpattern %

           let (tm,varl,typl) = show_full_termpattern p

               % Use `match_term' to attempt a matching of the template tm  %
               % against the term t. If this fails, `make_matching' fails.  %
               % If it succeeds the (term # term) list # (type # type) list %
               % returned by `match_term' is bound to the pair (vpl,tpl)    %
               % for further analysis/processing.                           %

           in  let (vpl,tpl) = match_term tm t

               % The (term # term) list component returned by `match_term'   %
               % is a list of pairs such that the first element of the pair  %
               % is a variable in tm, and the second element of the pair is  %
               % the term in t that the variable has been matched to.        %

               % Bound-variables in tm do not appear in the result of        %
               % `match_term'. Some of the variables which do appear may not %
               % have been specified as wildvars. The match must fail if     %
               % such a variable does not (when its type has been            %
               % instantiated) match itself in the list returned by          %
               % `match_term'. The (type # type) list, returned by           %
               % `match_term' is used to perform the instantiation.          %

               % Types are dealt with similarly, except that there is no     %
               % equivalent action to instantiation.                         %

               % The matching we are trying to construct should look like    %
               % the result of `match_term' except that the variables and    %
               % types from tm should be converted to wildcards, and only    %
               % those of them that appear as wildcards in the termpattern   %
               % should be included.                                         %

               % Now we know what we are trying to achieve, let us define    %
               % some functions to help us.                                  %

               % f is used to convert the term or type which is representing %
               % a wildcard into the appropriate wildcard type.              %

               and f w (a,b) = ((w a),b)

                  % : ((* -> **) -> (* # ***) -> (** # ***)) %

               % `instant_type' instantiates the type of a variable using a  %
               % (type # type) list in which the first element of each pair  %
               % is a `primitive' type. The embedded function `change_type'  %
               % does the real work. `instant_type' splits the variable into %
               % its name and type, applies `change_type' to the type, and   %
               % then reconstructs the variable using the new type.          %

               and instant_type ttl v =

                  % : ((type # type) list -> term -> term) %

                  % `change_type' instantiates a type. If the type is        %
                  % `primitive', it is looked-up in the instantiation list.  %
                  % If found, the corresponding instance is returned. If not %
                  % the type itself is returned. If the type is              %
                  % not `primitive', it is decomposed into a constructor and %
                  % a list of simpler types. Each of the latter are then     %
                  % instantiated, and the type is reconstructed.             %

                 (letrec change_type ttl typ =

                     % : ((type # type) list -> type -> type) %

                     if (is_primtype typ)
                     then ((snd (assoc typ ttl)) ? typ)
                     else (let (s,l) = dest_type typ
                           in  mk_type (s,(map (change_type ttl) l)))
                  in (let (s,t) = dest_var v
                      in  mk_var (s,(change_type ttl t)))
                 )

                   % `build' filters xxl removing any pairs whose first  %
                   % element is not in xl. If lf applied to the first    %
                   % element of such a pair is not equal to the second   %
                   % element of the pair, then the match being performed %
                   % is failed.                                          %

                   % `build' is used to build a matching from a `match'  %
                   % list and a wildcard list. Any variable or type in   %
                   % the `match' list but not in the wildcard list must  %
                   % match itself (allowing for type instantiation -     %
                   % hence the need for lf), and will not be included in %
                   % the result.                                         %

               in (letrec build lf xl xxl =

                      % : ((* -> **) -> * list -> (* # **) list ->          %
                      %                                      (* # **) list) %

                      if (null xxl)
                      then []
                      else if (mem ((fst o hd) xxl) xl)
                           then (hd xxl).(build lf xl (tl xxl))
                           else if ((lf o fst o hd) xxl = (snd o hd) xxl)
                                then (build lf xl (tl xxl))
                                else failwith `no match`

                   % Note : assumes all variables which could be wildvars   %
                   %        appear in the matching returned by `match_term' %

                   in abs_matching (
                        (map (f make_wildvar)
                                (build (instant_type tpl) varl vpl)),
                        (map (f make_wildtype) (build (\x.x) typl tpl)))
                  )

   % Function to combine two (consistent) matchings into a single matching %

   % Split the two matchings into wildvar and wildtype `match' lists. Merge %
   % the two resulting wildvar lists and the two resulting wildtype lists.  %
   % If either merge fails, the match fails.                                %

   and  join_matchings m n =

       % : (matching -> matching -> matching) %

           let mwvl,mwtl = rep_matching m
           and nwvl,nwtl = rep_matching n
           in  abs_matching ((merge mwvl nwvl),(merge mwtl nwtl))
                  ?? [`merge`] failwith `no match`;;


% Function to convert a matching into its representing type, and the %
% wildvars and wildtypes within that to their representing types.    %
% So, function makes all of a matching visible.                      %

let show_full_matching m =

   % : (matching -> ((term # term) list # (type # type) list)) %

       let wvl,wtl = show_matching m
       and f (w,t) = ((show_wildvar w),t)
       and g (w,t) = ((show_wildtype w),t)
       in  ((map f wvl),(map g wtl));;


% Function to lookup a wildvar in a matching, and return the term to %
% which it is bound.                                                 %

let match_of_var m wv =

   % : (matching -> wildvar -> term) %

   (snd o (assoc wv) o fst o show_matching) m
   ?? [`assoc`]
      failwith `match_of_var -- unknown wildvar (variable)`;;


% Function to lookup a wildtype in a matching, and return the type to %
% which it is bound.                                                  %

let match_of_type m wt =

   % : (matching -> wildtype -> type) %

   (snd o (assoc wt) o snd o show_matching) m
   ?? [`assoc`]
      failwith `match_of_type -- unknown wildtype (polymorphic type)`;;


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


% Datatype for lazy evaluation of alternate matchings %

% Nomatch means there is no way to match.                                    %
% Match means there is at least one way to match, and specifies the matching %
% (which may be null). The second element of the pair is a function to       %
% generate any other matchings if they exist.                                %

rectype result_of_match = Nomatch
                        | Match of matching # (void -> result_of_match);;


% Abbreviation for a result_of_match which is a match with no bindings %

let Match_null = Match(null_matching,(\().Nomatch));;


% Function to append two lazy lists (`result_of_matches') %

% `approms' appends two `result_of_matches' which are essentially just lazy %
% lists of matchings. The result must be kept as lazy as possible. This     %
% function is also used to OR two `result_of_matches', since this operation %
% corresponds exactly to appending them.                                    %

% The arguments to `approms' are actually functions from void to a          %
% `result_of_match', so that as little evaluation as necessary is done.     %

% The function is defined in an analogous way to `append' on lists.         %

letrec approms rom1fn rom2fn () =

   % : ((void -> result_of_match) -> (void -> result_of_match) ->           %
   %                                             (void -> result_of_match)) %

   case (rom1fn ())
   of (Nomatch) . (rom2fn ())
    | (Match (m,romfn)) . (Match (m,approms romfn rom2fn));;


% Function to convert a Boolean value to a result_of_match %

let bool_to_rom b =

   % : (bool -> result_of_match) %

   if b
   then Match_null
   else Nomatch;;


% Function to convert a result_of_match to a Boolean value %

% Note that information may be thrown away in this process. %

let rom_to_bool r =

   % : (result_of_match -> bool) %

   not (r = Nomatch);;


% Abbreviation for the datatype representing side-conditions %

% When applied to a matching, a side-condition performs tests on the        %
% bindings in the matching, and returns a `lazy list' of any successful new %
% bindings.                                                                 %

lettype side_condition = matching -> result_of_match;;


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