16
17:- ensure_loaded(hooks). 18:- ensure_loaded(lemma). 19
20:- no_hook_handling,hook_configuration. 21
22:- no_lemma_handling,lemma_configuration. 23
24:- dynamic(delta_ordering/1). 25:- dynamic(verbose_flag/0). 26:- dynamic(compile_complete_search/0). 27
30
37
38do_compile_complete_search :-
39 retract(compile_complete_search),
40 fail.
41do_compile_complete_search :-
42 assert(compile_complete_search).
43
44dont_compile_complete_search :-
45 retract(compile_complete_search),
46 fail.
47dont_compile_complete_search.
48
49:- do_compile_complete_search. 50
57
58do_compile_proof_printing :- print_proof.
59dont_compile_proof_printing :- dont_print_proof.
60
61:- do_compile_proof_printing. 62
70
71do_compile_count_inferences :- count_inferences.
72dont_compile_count_inferences :- dont_count_inferences.
73
74:- dont_compile_count_inferences. 75
76pttp_configuration :-
77 nl,writeln('PTTP CONFIGURATION:'),nl,
78 (count_inferences_pred(true) ->
79 writeln('PTTP counts no inferences.');
80 writeln('PTTP counts inferences!')),
81 (trace_search_progress_pred(nop) ->
82 writeln('PTTP does not trace search progress.');
83 writeln('PTTP traces search progress!')),
84 (compile_proof_printing ->
85 writeln('PTTP compiles proof printing!');
86 writeln('PTTP does not compile proof printing.')),
87 (compile_complete_search ->
88 writeln('PTTP compiles complete search!');
89 writeln('PTTP does not compile complete search.')).
90
91:- pttp_configuration. 92
95
96xray_configuration :-
97 nl,write('XRay CONFIGURATION:'),nl,nl,
98
99 write(delta_ordering),
100 write(' = '),
101 (delta_ordering(O), write(O),write(' '),fail ; write('.')),
102 nl,
103
104 write(verbose_mode),
105 write(' = '),
106 (verbose_flag, write("on") ; write("off")),
107 nl.
108
112
113switch_delta_ordering :-
114 delta_ordering(compatibility>admissibility),
115 admissibility_first.
116switch_delta_ordering :-
117 delta_ordering(admissibility>compatibility),
118 compatibility_first.
119
120compatibility_first :- 121 retract(delta_ordering(_)),
122 fail.
123compatibility_first :-
124 assert(delta_ordering(compatibility>admissibility)).
125
126admissibility_first :- 127 retract(delta_ordering(_)),
128 fail.
129admissibility_first :-
130 assert(delta_ordering(admissibility>compatibility)).
131
132:- admissibility_first. 133
134
138
139verbose_mode :- 140 retract(verbose_flag),
141 fail.
142verbose_mode :-
143 assert(verbose_flag).
144
145no_verbose_mode :- 146 retract(verbose_flag),
147 fail.
148no_verbose_mode.
149
150:- verbose_mode. 151
153verbose(X) :-
154 verbose_flag ->
155 write(X),nl;
156 157 true.
158
161
162:- xray_configuration,nl. 163
164configuration :-
165 hook_configuration,
166 lemma_configuration,
167 pttp_configuration,
168 xray_configuration