17
18lemma_runtime_procedures(Result) :-
19 lemmatize_procedure(Lemmatization0),
20
21 lemmatize_dynamically_procedure(DynamicLemmatization),
22 lemmatize_statically_procedure(StaticLemmatization),
23 conjoin(DynamicLemmatization,StaticLemmatization,Lemmatization1),
24
25 conjoin(Lemmatization0,Lemmatization1,Lemmatization),
26
27 default_assumptions_procedure(DefaultHandler),
28
29 conjoin(Lemmatization,DefaultHandler,Result).
30
31lemmatize_procedure(Result) :-
32 lemma_handling_flag,
33 !,
34
35 36 ((static_lemma_flag;dystatic_lemma_flag) 37 ->
38 DefaultHandler = default_assumptions(ProofOut,ProofEnd,Ass);
39 40 DefaultHandler = true,
41 Ass = []
42 ),
43
44 45 (lemma_type_parameter(delta) ->
46 HeadD = lemmatize(default(N:(Gamma :- _)),Proof,ProofOut,ProofEnd),
47 48 (lemma_type_parameter(omega) ->
49 ReductionHandlerD = remove_reductions(Proof,ProofOut);
50 51 ReductionHandlerD = true,
52 ProofOut=Proof),
53 conjoin(ReductionHandlerD,DefaultHandler,BodyD1),
54 55 lemma_handler(gamma(N,Gamma),false,Ass,LemmaHandlerD),
56 conjoin(BodyD1,LemmaHandlerD,BodyD),
57 RuleD = (HeadD :- !,BodyD);
58 59 RuleD = true),
60
61 62 (lemma_type_parameter(omega) ->
63 HeadO = lemmatize(extension(_:Goal),Proof,ProofOut,ProofEnd),
64 65 ReductionHandlerO = skim_reductions(Goal,Proof,ProofOut,ProofEnd,Ancs),
66 conjoin(ReductionHandlerO,DefaultHandler,BodyO1),
67 68 lemma_handler(Goal,Ancs,Ass,LemmaHandler1),
69 (lemma_format_parameter(unit) ->
70 LemmaHandlerO = (Ancs=false -> LemmaHandler1 ; verbose(skipping:Goal:Ancs));
71 72 LemmaHandlerO = LemmaHandler1),
73 conjoin(BodyO1,LemmaHandlerO,BodyO),
74 RuleO = (HeadO :- !,BodyO);
75 76 RuleO = true),
77
78 79 HeadI = lemmatize(Inference,Proof,Proof,ProofEnd),
80 BodyI = verbose("'lemmatize/4: Ignoring inference'":Inference),
81 RuleI = (HeadI :- BodyI),
82
83 84 conjoin(RuleD,RuleO,Result1),
85 conjoin(Result1,RuleI,Result).
86lemmatize_procedure(Result) :-
87 88 Result = (lemmatize(_,_,_,_)).
89
90lemma_handler(Goal,Ancs,Ass,LemmaHandler) :-
91 ((dynamic_lemma_flag;dystatic_lemma_flag) ->
92 DynamicLemmaHandler = lemmatize_dynamically(Goal,Ancs,Ass);
93 94 DynamicLemmaHandler = true),
95 (static_lemma_flag ->
96 StaticLemmaHandler = lemmatize_statically(Goal,Ancs,Ass);
97 98 StaticLemmaHandler = true),
99 conjoin(DynamicLemmaHandler,StaticLemmaHandler,LemmaHandler).
100
101lemmatize_dynamically_procedure(Result) :-
102 lemma_handling_flag,
103 lemma_mode_parameter(Mode),
104 (Mode = dynamic ; Mode = dystatic),
105 !,
106
107 Head0 = lemmatize_dynamically(Goal,Ancestors,_),
108 Body0 = dynamic_lemma(Goal,Ancestors,_), % UNIFY ?!
109 Rule0 = (Head0 :- Body0, !),
110
111 (dystatic_lemma_flag ->
112
113 Head1 = lemmatize_dynamically(Goal,Ancestors,[]),
114 Body1A = assert(dynamic_lemma(Goal,Ancestors,[])),
115 Body1S = lemmatize_statically(Goal,Ancestors,[]),
116 Rule1 = (Head1 :- !, Body1A, Body1S),
117
118 Body2S = lemmatize_statically(Goal,Ancestors,Assumptions);
119
120 %true ->
121 Rule1 = true,
122 Body2S = true),
123
124 conjoin(Rule0,Rule1,Rule01),
125
126 Head2 = lemmatize_dynamically(Goal,Ancestors,Assumptions),
127 Body2A = assert(dynamic_lemma(Goal,Ancestors,Assumptions)),
128 Body2R = retract(dynamic_lemma(Goal,Ancestors,Assumptions)),
129 conjoin(Body2R,Body2S,Body2RS),
130 Rule2 = (Head2 :- Body2A ; (Body2RS, ! , fail)),
131
132 conjoin(Rule01,Rule2,Result).
133lemmatize_dynamically_procedure(Rule) :-
134 Head = lemmatize_dynamically(_,_,_),
135 Body = (write(lemmatize_dynamically*not_in_charge),nl,trace,fail),
136 Rule = (Head :- Body).
137
138lemmatize_statically_procedure(Result) :-
139 lemma_handling_flag,
140 lemma_mode_parameter(Mode),
141 (Mode = static ; Mode = dystatic),
142 !,
143
144 Head0 = lemmatize_statically(Goal,Ancestors,Assumptions),
145 Body0 = static_lemma(Goal,Ancestors,Assumptions), 146 Rule0 = (Head0 :- Body0, !),
147
148 Head1 = lemmatize_statically(Goal,Ancestors,Assumptions),
149 Body1A = assert(static_lemma(Goal,Ancestors,Assumptions)),
150 Rule1 = (Head1 :- Body1A),
151
152 Result = (Rule0,Rule1).
153lemmatize_statically_procedure(Rule) :-
154 Head = lemmatize_statically(_,_,_),
155 Body = (write(lemmatize_statically*not_in_charge),nl,trace,fail),
156 Rule = (Head :- Body).
157
158default_assumptions_procedure(Result) :-
159 lemma_handling_flag,
160 lemma_mode_parameter(Mode),
161 (Mode = static ; Mode = dystatic),
162 !,
163
164 Head0 = default_assumptions(Proof,ProofEnd,[]),
165 Body0 = (Proof == ProofEnd),
166 Rule0 = (Head0 :- Body0, !),
167
168 BodyR = default_assumptions(Proof,ProofEnd,Justs),
169
170 Body123 = (BodyR,combine_clauses(Just,Justs,Assumptions)),
171
172 Head1 = default_assumptions([default(_:(_ :- _: Just))|Proof],ProofEnd,Assumptions),
173 Head2 = default_assumptions([static_lemma(_ : Just) |Proof],ProofEnd,Assumptions),
174 Head3 = default_assumptions([dynamic_lemma(_ : Just) |Proof],ProofEnd,Assumptions),
175
176 Rule1 = (Head1 :- !, Body123),
177 conjoin(Rule0,Rule1,Rule01),
178
179 Rule2 = (Head2 :- !, Body123),
180 Rule3 = (Head3 :- !, Body123),
181 Rule23 = (Rule2,Rule3),
182 conjoin(Rule01,Rule23,Rule0123),
183
184 Head4 = default_assumptions([_|Proof],ProofEnd,Justs),
185 Rule4 = (Head4 :- BodyR),
186
187 conjoin(Rule0123,Rule4,Result).
188default_assumptions_procedure(Rule) :-
189 Head = default_assumptions(_,_,_),
190 Body = (write(default_assumptions*not_in_charge),nl,trace,fail),
191 Rule = (Head :- Body).
192
195
196compile_lemma_handling(Name) :-
197 lemma_runtime_procedures(LemmaProcs),
198 write_lem(Name,LemmaProcs),
199 compile_lem(Name).
200
201read_lem(Name,Wff) :-
202 concatenate(Name,'.lem',LFile),
203 read_clauses(LFile,Wff).
204write_lem(File,LemmaProcs) :-
205 concatenate(File,'.lem',LemmaFile),
206 open(LemmaFile,write,LemmaStream),
207 write_clauses(LemmaStream,LemmaProcs),
208 close(LemmaStream),
209 !.
210compile_lem(File) :-
211 concatenate(File,'.lem',KBFile),
212 compile(KBFile)