16
17:- dynamic(dynamic_lemma/3). 18:- dynamic(static_lemma/3). 19
20:- dynamic(lemma_handling_flag/0). 21
22:- dynamic(lemma_mode_parameter/1). 23:- dynamic(lemma_format_parameter/1). 24:- dynamic(lemma_type_parameter/1). 25
28
29lemma_configuration :-
30 nl,write('LEMMA CONFIGURATION:'),nl,nl,
31
32 write("Lemma handling"),
33 write(' = '),
34 (lemma_handling_flag ->
35 write(on),
36 nl,nl,
37
38 write(lemma_format),
39 write(' = '),
40 (lemma_format_parameter(P), write(P),write(' '),fail ; write('.')),
41 nl,
42
43 write(lemma_mode),
44 write(' = '),
45 (lemma_mode_parameter(M), write(M),write(' '),fail ; write('.')),
46 nl,
47
48 write(lemma_type),
49 write(' = '),
50 (lemma_type_parameter(T), write(T),write(' '),fail ; write('.')),
51 nl;
52 53 write(off)),
54 nl.
55
58
59lemma_handling :- 60 retract(lemma_handling_flag),
61 fail.
62lemma_handling :-
63 assert(lemma_handling_flag).
64
65no_lemma_handling :- 66 retract(lemma_handling_flag),
67 fail.
68no_lemma_handling.
69
74
75lemma_mode(dynamic) :- 76 retract(lemma_mode_parameter(_)),
77 fail.
78lemma_mode(dynamic) :-
79 assert(lemma_mode_parameter(dynamic)).
80
81lemma_mode(dystatic) :- 82 retract(lemma_mode_parameter(_)),
83 fail.
84lemma_mode(dystatic) :-
85 assert(lemma_mode_parameter(dystatic)).
86
87lemma_mode(static) :- 88 retract(lemma_mode_parameter(_)),
89 fail.
90lemma_mode(static) :-
91 assert(lemma_mode_parameter(static)).
92
95
96dynamic_lemmas :- lemma_mode(dynamic). 97
98add_dynamic_lemmas :- 99 retract(lemma_mode_parameter(dynamic)),
100 fail.
101add_dynamic_lemmas :-
102 assert(lemma_mode_parameter(dynamic)).
103
104no_dynamic_lemmas :- 105 retract(lemma_mode_parameter(dynamic)),
106 fail.
107no_dynamic_lemmas.
108
111
112static_lemmas :- lemma_mode(static). 113
114add_static_lemmas :- 115 retract(lemma_mode_parameter(static)),
116 fail.
117add_static_lemmas :-
118 assert(lemma_mode_parameter(static)).
119
120no_static_lemmas :- 121 retract(lemma_mode_parameter(static)),
122 fail.
123no_static_lemmas.
124
128
129dystatic_lemmas :- lemma_mode(dystatic). 130
131add_dystatic_lemmas :- 132 retract(lemma_mode_parameter(dystatic)),
133 fail.
134add_dystatic_lemmas :-
135 assert(lemma_mode_parameter(dystatic)).
136
137no_dystatic_lemmas :- 138 retract(lemma_mode_parameter(dystatic)),
139 fail.
140no_dystatic_lemmas.
141
143
144lemma_flag :- lemma_mode_parameter(X).
145dynamic_lemma_flag :- lemma_mode_parameter(dynamic).
146static_lemma_flag :- lemma_mode_parameter(static).
147dystatic_lemma_flag :- lemma_mode_parameter(dystatic).
148
149no_lemmas :- no_dynamic_lemmas,no_static_lemmas,no_dystatic_lemmas.
150
158
159lemma_type(delta) :- 160 retract(lemma_type_parameter(_)),
161 fail.
162lemma_type(delta) :-
163 assert(lemma_type_parameter(delta)).
164
165lemma_type(omega) :- 166 retract(lemma_type_parameter(_)),
167 fail.
168lemma_type(omega) :-
169 assert(lemma_type_parameter(omega)).
170
171lemma_type(all) :- 172 retract(lemma_type_parameter(_)),
173 fail.
174lemma_type(all) :-
175 assert(lemma_type_parameter(delta)),
176 assert(lemma_type_parameter(omega)).
177
180
181add_delta_lemmas :- 182 retract(lemma_type_parameter(delta)),
183 fail.
184add_delta_lemmas :-
185 assert(lemma_type_parameter(delta)).
186
187no_delta_lemmas :- 188 retract(lemma_type_parameter(delta)),
189 fail.
190no_delta_lemmas.
191
194
195add_omega_lemmas :- 196 retract(lemma_type_parameter(omega)),
197 fail.
198add_omega_lemmas :-
199 assert(lemma_type_parameter(omega)).
200
201no_omega_lemmas :- 202 retract(lemma_type_parameter(omega)),
203 fail.
204no_omega_lemmas.
205
208
209lemma_format(unit) :- 210 retract(lemma_format_parameter(_)),
211 fail.
212lemma_format(unit) :-
213 assert(lemma_format_parameter(unit)).
214
215lemma_format(disj) :- 216 retract(lemma_format_parameter(_)),
217 fail.
218lemma_format(disj) :-
219 assert(lemma_format_parameter(disj)).
220
223
224:- compile(lemma_config). 225
228
232
233add_lemmatization((Head :- Body),(Head1 :- Body1)) :-
234 lemma_handling_flag,
235 !,
236 Head =.. L,
237 append(L,[ProofOut,ProofEnd],L1),
238 Head1 =.. L1,
239 add_lemmatization_args(Body,Proof,ProofEnd,Body2,Lemma),
240 (Lemma = true ->
241 Body1 = Body2,
242 ProofOut = Proof;
243 add_lemmatization_p(Head :- Body) ->
244 Lemmatization =.. [lemmatize,Lemma,Proof,ProofOut,ProofEnd],
245 conjoin(Body2,Lemmatization,Body1),
246 verbose("Lemmatization ":Lemma);
247 248 Body1 = Body2,
249 ProofOut = Proof).
250add_lemmatization((Head :- Body),(Head :- Body)).
251
252add_lemmatization_p(Head :- Body) :-
253 lemma_flag,
254 !,
255 (functor(Head,query,_) -> fail;
256 functor(Head,alpha,_) -> fail;
257 functor(Head,gamma,_) -> lemma_type_parameter(delta);
258 true -> lemma_type_parameter(omega)).
259
260add_lemmatization_args(Body,Proof,ProofEnd,Body1,Lemma) :-
261 Body = (A , B) ->
262 add_lemmatization_args(A,Proof,Proof1,A1,L1),
263 add_lemmatization_args(B,Proof1,ProofEnd,B1,L2),
264 conjoin(A1,B1,Body1),
265 conjoin(L1,L2,Lemma);
266 Body = (A ; B) ->
267 add_lemmatization_args(A,Proof,ProofEnd,A1,L1),
268 add_lemmatization_args(B,Proof,ProofEnd,B1,L2),
269 disjoin(A1,B1,Body1),
270 conjoin(L1,L2,Lemma);
271 Body = infer_by(X) ->
272 add_lemmatization_inference(X,Proof,ProofEnd,Record,Lemma),
273 conjoin(Body,Record,Body1);
274 Body =.. [search,Goal|L] ->
275 add_lemmatization_args(Goal,Proof,ProofEnd,Goal1),
276 Body1 =.. [search,Goal1|L],
277 Lemma = true;
278 Body = fail ->
279 Body1 = Body,
280 Lemma = true;
281 builtin(Body) ->
282 Proof = ProofEnd,
283 Body1 = Body,
284 Lemma = true;
285 286 Body =.. L,
287 append(L,[Proof,ProofEnd],L1),
288 Body1 =.. L1,
289 Lemma = true.
290
291add_lemmatization_inference(Inference,Proof,ProofEnd,Record,Lemma) :-
292 Inference = reduction(_) ->
293 294 Lemma = true,
295 (lemma_type_parameter(omega) ->
296 Record = (Proof = [Inference|ProofEnd]);
297 298 Proof = ProofEnd,
299 Record = true);
300 Inference = extension(_) ->
301 302 Proof = ProofEnd,
303 Record = true,
304 (lemma_type_parameter(omega) ->
305 Lemma = Inference;
306 307 Lemma = true);
308 Inference = default(_) ->
309 310 Lemma = Inference,
311 ((static_lemma_flag;dystatic_lemma_flag) ->
312 Record = (Proof = [Inference|ProofEnd]);
313 314 Proof = ProofEnd,
315 Record =true);
316 Inference = static_lemma(_) ->
317 318 Record = (Proof = [Inference|ProofEnd]),
319 Lemma = true;
320 Inference = dynamic_lemma(_) ->
321 322 Lemma = true,
323 ((static_lemma_flag;dystatic_lemma_flag) ->
324 Record = (Proof = [Inference|ProofEnd]);
325 326 Proof = ProofEnd,
327 Record =true);
328 329 330 Proof = ProofEnd,
331 Record = true,
332 Lemma = true.
333
334
335lemma_tests_p(P,N) :-
336 lemma_handling_flag, (dynamic_lemma_test_p(P,N) ; static_lemma_test_p(P,N)).
337
338dynamic_lemma_test_p(P,N) :-
339 (dynamic_lemma_flag;dystatic_lemma_flag),
340 !,
341 (P == query -> fail;
342 P == alpha -> fail;
343 P == gamma -> lemma_type_parameter(delta);
344 true -> lemma_type_parameter(omega)).
345
346static_lemma_test_p(P,N) :-
347 (static_lemma_flag;dystatic_lemma_flag),
348 !,
349 (P == query -> fail;
350 P == alpha -> fail;
351 P == gamma -> lemma_type_parameter(delta);
352 true -> lemma_type_parameter(omega)).
353
354lemma_tests(P,N,Result) :-
355 lemma_handling_flag,
356 lemma_tests_p(P,N), 357 !,
358 N3 is N - 3, 359 functor(Head3,P,N3),
360 Head3 =.. [P|Args1],
361 append(Args1,[_,_,_],Args),
362 Head =.. [P|Args],
363
364 (dynamic_lemma_test_p(P,N) ->
365 dynamic_lemma_test(Head,Head3,DynamicLemmaBody);
366 367 DynamicLemmaBody=true),
368
369 (static_lemma_test_p(P,N) ->
370 static_lemma_test(Head,Head3,StaticLemmaBody);
371 372 StaticLemmaBody=true),
373
374 conjoin(DynamicLemmaBody,StaticLemmaBody,Result).
375lemma_tests(_,_,true).
376
377dynamic_lemma_test(Head,Head3,Test) :-
378 lemma_format_parameter(unit) ->
379 ((static_lemma_flag;dystatic_lemma_flag) ->
380 Body = (infer_by(dynamic_lemma(Head3:Assumptions)),
381 dynamic_lemma(Head3,false,Assumptions)) ;
382 383 Body = (infer_by(dynamic_lemma(Head3)),
384 dynamic_lemma(Head3,false,[]))),
385 Test = (Head :- Body,!); 386 lemma_format_parameter(disj) ->
387 388 not_yet_implemented.
389
390static_lemma_test(Head,Head3,Test) :-
391 lemma_format_parameter(unit) ->
392 Body = (infer_by(static_lemma(Head3:Assumptions)),
393 static_lemma(Head3,false,Assumptions),
394 justification(Assumptions)),
395 Test = (Head :- Body);
396 lemma_format_parameter(disj) ->
397 398 not_yet_implemented.
399
402
403lemmatize(default(N:(Gamma :- _)),Proof,ProofOut,ProofEnd) :-
404 verbose("Using static lemma code: ":lemmatize),
405 !,
406 remove_reductions(Proof,ProofOut),
407 default_assumptions(ProofOut,ProofEnd,Ass),
408 lemmatize_dynamically(gamma(N,Gamma),false,Ass).
410lemmatize(extension(_N:Goal),Proof,ProofOut,ProofEnd) :-
411 verbose("Using static lemma code: ":lemmatize),
412 !,
413 skim_reductions(Goal,Proof,ProofOut,ProofEnd,Ancs),
414 default_assumptions(ProofOut,ProofEnd,Ass),
415 lemmatize_dynamically(Goal,Ancs,Ass).
417lemmatize(_Lemmatization,_Proof,_ProofOut,_ProofEnd) :-
418 error_in_lemmatize.
419
420lemmatize_statically(Goal,Ancestors,Assumptions) :-
421 static_lemma(Goal,Ancestors,Assumptions), 422 !.
423lemmatize_statically(Goal,Ancestors,Assumptions) :-
424 assert(static_lemma(Goal,Ancestors,Assumptions)),
425 verbose(static_lemma(Goal,Ancestors,Assumptions)).
426
427lemmatize_dynamically(Goal,Ancestors,_) :-
428 dynamic_lemma(Goal,Ancestors,_), 429 !.
435lemmatize_dynamically(Goal,Ancestors,Assumptions) :-
436 (assert(dynamic_lemma(Goal,Ancestors,Assumptions)),
437 verbose(activated:(dynamic_lemma(Goal,Ancestors,[Assumptions])));
438 retract(dynamic_lemma(Goal,Ancestors,Assumptions)),
439 verbose(deactivated:(dynamic_lemma(Goal,Ancestors,[Assumptions]))),
441 !,
442 fail).
443
446
447remove_reductions([default(X)|Proof],[default(X)|Proof]) :-
448 !.
449remove_reductions([static_lemma(X)|Proof],[static_lemma(X)|ProofOut]) :-
450 !,
451 remove_reductions(Proof,ProofOut).
452remove_reductions([dynamic_lemma(X)|Proof],[dynamic_lemma(X)|ProofOut]) :-
453 454 !,
455 remove_reductions(Proof,ProofOut).
456remove_reductions(Proof,ProofOut) :-
457 Proof = [_|RestProof],
458 remove_reductions(RestProof,ProofOut).
459
460skim_reductions(_Goal,Proof,Proof,ProofEnd,false) :-
461 Proof == ProofEnd,
462 !.
463skim_reductions(_Goal,Proof,Proof,_ProofEnd,false) :-
464 Proof = [default(_)|_],
465 !.
466skim_reductions(Goal,[reduction(Anc)|Proof],Proof1,ProofEnd,Ancs) :-
467 Goal == Anc,
468 skim_reductions(Goal,Proof,Proof1,ProofEnd,Ancs),
469 !.
470skim_reductions(Goal,[reduction(Anc)|Proof],[reduction(Anc)|Proof1],ProofEnd,Ancs1) :-
471 !,
472 skim_reductions(Goal,Proof,Proof1,ProofEnd,Ancs),
473 disjoin1(Anc,Ancs,Ancs1).
474skim_reductions(Goal,[static_lemma(X)|Proof],[static_lemma(X)|Proof1],ProofEnd,Ancs) :-
475 skim_reductions(Goal,Proof,Proof1,ProofEnd,Ancs).
476skim_reductions(Goal,[dynamic_lemma(X)|Proof],[dynamic_lemma(X)|Proof1],ProofEnd,Ancs) :-
477 478 skim_reductions(Goal,Proof,Proof1,ProofEnd,Ancs).
479
484
485default_assumptions(Proof,ProofEnd,[]) :-
486 Proof == ProofEnd,
487 !.
488default_assumptions([default(_N:(_ :- _ : Just))|Proof],ProofEnd,Assumptions) :-
489 !,
490 default_assumptions(Proof,ProofEnd,Justs),
491 combine_clauses(Just,Justs,Assumptions).
492default_assumptions([static_lemma(_ : Just)|Proof],ProofEnd,Assumptions) :-
493 !,
494 default_assumptions(Proof,ProofEnd,Justs),
495 combine_clauses(Just,Justs,Assumptions).
496default_assumptions([dynamic_lemma(_ : Just)|Proof],ProofEnd,Assumptions) :-
497 498 !,
499 default_assumptions(Proof,ProofEnd,Justs),
500 combine_clauses(Just,Justs,Assumptions).
501default_assumptions([_|Proof],ProofEnd,Wff) :-
502 default_assumptions(Proof,ProofEnd,Wff).
503
506
507disjoin1(A,B,C) :-
508 disjoin2(A,B,C1),
509 disjoin(A,C1,C).
510
511disjoin2(A,(B ; C),D) :-
512 !,
513 disjoin2(A,B,B1),
514 disjoin2(A,C,C1),
515 disjoin(B1,C1,D).
516disjoin2(A,B,false) :-
517 A == B,
518 !.
519disjoin2(_,B,B).
520
521
524
525write_lemmas(File) :-
526 concatenate(File,'.lem',LFile),
527 open(LFile,write,LStream),
528 !,
529 (static_lemma(X,Y,Z),
530 write_clauses(LStream,static_lemma(X,Y,Z)),
531 fail;
532 close(LStream)).
533
534show_lemmas :-
535 show_dynamic_lemmas,fail;
536 nl,show_static_lemmas.
537
538show_dynamic_lemmas :-
539 (dynamic_lemma(X,Y,Z),
540 write(dynamic_lemma(X,Y,Z)),
541 nl,
542 fail;
543 true).
544show_static_lemmas :-
545 (static_lemma(X,Y,Z),
546 write(static_lemma(X,Y,Z)),
547 nl,
548 fail;
549 true).
550
551remove_lemmas :-
552 remove_static_lemmas,
553 remove_dynamic_lemmas.
554remove_dynamic_lemmas :-
555 retract_all(dynamic_lemma(_,_,_)).
556remove_static_lemmas :-
557 retract_all(static_lemma(_,_,_))