hol88-library-source 2.02.19940316-35 / usr / share / hol88-2.02.19940316 / Library / trs / sidecond.ml

This file is indexed.

/usr/share/hol88-2.02.19940316/Library/trs/sidecond.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
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
% sidecond.ml                                           (c) R.J.Boulton 1990 %
%----------------------------------------------------------------------------%


% Function to create a `result_of_match' of all the ways of matching a %
% termpattern within a term.                                           %

% The function tries to match the termpattern against the term. If this is %
% successful the resulting matching is made the first item of the          %
% `result_of_match'. The rest of the `result_of_match' will be null if `t' %
% is a variable or a constant, since `t' cannot be split in such cases.    %

% If `t' is an abstraction, a match is tried against the body. If `t' is a %
% combination, matches are tried against both the rator and the rand. Both %
% these return `result_of_matches' which have to be appended using the     %
% function `approms'.                                                      %

% Note that the function requires a null argument before it actually does  %
% any evaluation. This is to keep the computation as lazy as possible.     %

letrec containsfn p t () =

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

   let rest () =
      if (is_const t) then Nomatch
      if (is_var t) then Nomatch
      if (is_abs t) then (containsfn p ((snd o dest_abs) t) () )
      if (is_comb t) then (approms
                             (containsfn p (rator t))
                             (containsfn p (rand t))
                             ()
                          )
      else fail
   in (Match (make_matching p t,rest)) ??[`no match`] (rest ());;


% Functions which make theorem patterns which are side-conditions %

% `Contains' looks up its first argument in the matching given as argument  %
% to the side-condition. A `result_of_match' is formed from the termpattern %
% and the term bound to `w', by testing the termpattern for containment     %
% within the term.                                                          %

ml_curried_infix `Contains`;;

let w Contains p =

   % : (wildvar -> termpattern -> thmpattern) %

   Side (\m . containsfn p (match_of_var m w) () );;


% `contains' behaves as for `Contains' except that its arguments are given %
% as terms rather than as a wildvar and a termpattern. The terms are made  %
% into a wildvar and a termpattern using default wildcards.                %

ml_curried_infix `contains`;;

let t contains t' =

   % : (term -> term -> thmpattern) %

   (make_wildvar t) Contains (autotermpattern t');;


% `Matches' looks up its first argument in the matching given as argument     %
% to the side-condition. A `result_of_match' is formed from the termpattern   %
% and the term bound to `w', by testing the termpattern against the term. If  %
% the match is successful, the matching becomes the first and only element of %
% the `result_of_match'. If not the `result_of_match' is `Nomatch'.           %

ml_curried_infix `Matches`;;

let w Matches p =

   % : (wildvar -> termpattern -> thmpattern) %

   Side (\m . (  Match (make_matching p (match_of_var m w), (\().Nomatch))
              ?? [`no match`] Nomatch
              )
        );;


% `matches' behaves as for `Matches' except that its arguments are given as   %
% terms rather than as a wildvar and a termpattern. The terms are made into a %
% wildvar and a termpattern using default wildcards.                          %

ml_curried_infix `matches`;;

let t matches t' =

   % : (term -> term -> thmpattern) %

   (make_wildvar t) Matches (autotermpattern t');;


% Function to split a bound term into the bound variable and the body %

% The bindings are represented by applications of function constants to     %
% lambda-abstractions. Hence the need to destroy a combination, followed by %
% (if the operator is a binder) destruction of an abstraction.              %

let dest_binder t =

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

   (let (t1,t2) = dest_comb t
    in  if (is_binder (fst (dest_const t1)))
        then dest_abs t2
        else fail
   ) ? failwith `dest_binder`;;


% Function to strip all binders from the beginning of a term %

% The function repeatedly strips one binder until the process fails. %

letrec strip_binders t =

   % : (term -> term) %

   ((strip_binders o snd o dest_binder) t) ? t;;


% `Has_body' looks up its first argument in the matching given as argument    %
% to the side-condition. The bound term then has any binders stripped from    %
% the front of it. A `result_of_match' is formed from the termpattern and the %
% processed term by testing the termpattern against the term. If the match is %
% successful, the matching becomes the first and only element of the          %
% `result_of_match'. If not the `result_of_match' is `Nomatch'.               %

ml_curried_infix `Has_body`;;

let w Has_body p =

   % : (wildvar -> termpattern -> thmpattern) %

   Side (\m . (  Match (make_matching p (strip_binders (match_of_var m w)),
                    (\().Nomatch))
              ?? [`no match`] Nomatch
              )
        );;


% `has_body' behaves as for `Has_body' except that its arguments are given %
% as terms rather than as a wildvar and a termpattern. The terms are made  %
% into a wildvar and a termpattern using default wildcards.                %

ml_curried_infix `has_body`;;

let t has_body t' =

   % : (term -> term -> thmpattern) %

   (make_wildvar t) Has_body (autotermpattern t');;


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


% Functions which construct a side-condition as a theorem pattern %


% This one builds a side-condition which looks up the binding of `w' in the %
% matching given as argument to the side-condition. It then applies `f' to  %
% the bound `term', and converts the resulting Boolean value to a value of  %
% type `result_of_match'. The latter becomes the result of the              %
% side-condition test.                                                      %

let Test1term f w =

   % : ((term -> bool) -> wildvar -> thmpattern) %

   Side (\m . (bool_to_rom o f) (match_of_var m w));;


% `test1term' behaves as for `Test1term' except that its second argument is %
% given as a `term'. The `term' is automatically converted to a `wildvar'.  %

let test1term f t =

   % : ((term -> bool) -> term -> thmpattern) %

   Test1term f (make_wildvar t);;


% This one builds a side-condition which looks up the binding of `w' in the %
% matching given as argument to the side-condition. It then applies `f' to  %
% the bound `type', and converts the resulting Boolean value to a value of  %
% type `result_of_match'. The latter becomes the result of the              %
% side-condition test.                                                      %

let Test1type f w =

   % : ((type -> bool) -> wildtype -> thmpattern) %

   Side (\m . (bool_to_rom o f) (match_of_type m w));;


% `test1type' behaves as for `Test1type' except that its second argument is %
% given as a `type'. The `type' is automatically converted to a `wildtype'. %

let test1type f t =

   % : ((type -> bool) -> type -> thmpattern) %

   Test1type f (make_wildtype t);;


% This one builds a side-condition which looks up the bindings of `w1' and  %
% `w2' in the matching given as argument to the side-condition. It then     %
% applies `f' to the two bound `terms', and converts the resulting Boolean  %
% value to a value of type `result_of_match'. The latter becomes the result %
% of the side-condition test.                                               %

let Test2terms f w1 w2 =

   % : ((term -> term -> bool) -> wildvar -> wildvar -> thmpattern) %

   Side (\m . bool_to_rom (f (match_of_var m w1) (match_of_var m w2)));;


% `test2terms' behaves as for `Test2terms' except that its second and third %
% arguments are given as `terms'. The `terms' are automatically converted   %
% to `wildvars'.                                                            %

let test2terms f t1 t2 =

   % : ((term -> term -> bool) -> term -> term -> thmpattern) %

   Test2terms f (make_wildvar t1) (make_wildvar t2);;


% This one builds a side-condition which looks up the bindings of `w1' and  %
% `w2' in the matching given as argument to the side-condition. It then     %
% applies `f' to the two bound `types', and converts the resulting Boolean  %
% value to a value of type `result_of_match'. The latter becomes the result %
% of the side-condition test.                                               %

let Test2types f w1 w2 =

   % : ((type -> type -> bool) -> wildtype -> wildtype -> thmpattern) %

   Side (\m . bool_to_rom (f (match_of_type m w1) (match_of_type m w2)));;


% `test2types' behaves as for `Test2types' except that its second and third %
% arguments are given as `types'. The `types' are automatically converted   %
% to `wildtypes'.                                                           %

let test2types f t1 t2 =

   % : ((type -> type -> bool) -> type -> type -> thmpattern) %

   Test2types f (make_wildtype t1) (make_wildtype t2);;


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

APT Browse - Built by Thomas Orozco.