131 val rm_simpset = (fn () => include_simpset:=false); |
131 val rm_simpset = (fn () => include_simpset:=false); |
132 val rm_claset = (fn () => include_claset:=false); |
132 val rm_claset = (fn () => include_claset:=false); |
133 val rm_clasimp = (fn () => (include_simpset:=false;include_claset:=false)); |
133 val rm_clasimp = (fn () => (include_simpset:=false;include_claset:=false)); |
134 val rm_atpset = (fn () => include_atpset:=false); |
134 val rm_atpset = (fn () => include_atpset:=false); |
135 |
135 |
136 (*** paths for HOL helper files ***) |
|
137 fun full_typed_comb_inclS () = |
|
138 helper_path "E_HOME" "additionals/full_comb_inclS" |
|
139 handle _ => helper_path "VAMPIRE_HOME" "additionals/full_comb_inclS"; |
|
140 |
|
141 fun full_typed_comb_noS () = |
|
142 helper_path "E_HOME" "additionals/full_comb_noS" |
|
143 handle _ => helper_path "VAMPIRE_HOME" "additionals/full_comb_noS"; |
|
144 |
|
145 fun partial_typed_comb_inclS () = |
|
146 helper_path "E_HOME" "additionals/par_comb_inclS" |
|
147 handle _ => helper_path "VAMPIRE_HOME" "additionals/par_comb_inclS"; |
|
148 |
|
149 fun partial_typed_comb_noS () = |
|
150 helper_path "E_HOME" "additionals/par_comb_noS" |
|
151 handle _ => helper_path "VAMPIRE_HOME" "additionals/par_comb_noS"; |
|
152 |
|
153 fun const_typed_comb_inclS () = |
|
154 helper_path "E_HOME" "additionals/const_comb_inclS" |
|
155 handle _ => helper_path "VAMPIRE_HOME" "additionals/const_comb_inclS"; |
|
156 |
|
157 fun const_typed_comb_noS () = |
|
158 helper_path "E_HOME" "additionals/const_comb_noS" |
|
159 handle _ => helper_path "VAMPIRE_HOME" "additionals/const_comb_noS"; |
|
160 |
|
161 fun untyped_comb_inclS () = |
|
162 helper_path "E_HOME" "additionals/u_comb_inclS" |
|
163 handle _ => helper_path "VAMPIRE_HOME" "additionals/u_comb_inclS"; |
|
164 |
|
165 fun untyped_comb_noS () = |
|
166 helper_path "E_HOME" "additionals/u_comb_noS" |
|
167 handle _ => helper_path "VAMPIRE_HOME" "additionals/u_comb_noS"; |
|
168 |
|
169 fun full_typed_HOL_helper1 () = |
|
170 helper_path "E_HOME" "additionals/full_helper1" |
|
171 handle _ => helper_path "VAMPIRE_HOME" "additionals/full_helper1"; |
|
172 |
|
173 fun partial_typed_HOL_helper1 () = |
|
174 helper_path "E_HOME" "additionals/par_helper1" |
|
175 handle _ => helper_path "VAMPIRE_HOME" "additionals/par_helper1"; |
|
176 |
|
177 fun const_typed_HOL_helper1 () = |
|
178 helper_path "E_HOME" "additionals/const_helper1" |
|
179 handle _ => helper_path "VAMPIRE_HOME" "additionals/const_helper1"; |
|
180 |
|
181 fun untyped_HOL_helper1 () = |
|
182 helper_path "E_HOME" "additionals/u_helper1" |
|
183 handle _ => helper_path "VAMPIRE_HOME" "additionals/u_helper1"; |
|
184 |
|
185 fun get_full_typed_helpers () = |
|
186 (full_typed_HOL_helper1 (), full_typed_comb_noS (), full_typed_comb_inclS ()); |
|
187 |
|
188 fun get_partial_typed_helpers () = |
|
189 (partial_typed_HOL_helper1 (), partial_typed_comb_noS (), partial_typed_comb_inclS ()); |
|
190 |
|
191 fun get_const_typed_helpers () = |
|
192 (const_typed_HOL_helper1 (), const_typed_comb_noS (), const_typed_comb_inclS ()); |
|
193 |
|
194 fun get_untyped_helpers () = |
|
195 (untyped_HOL_helper1 (), untyped_comb_noS (), untyped_comb_inclS ()); |
|
196 |
|
197 fun get_all_helpers () = |
|
198 (get_full_typed_helpers (), get_partial_typed_helpers (), get_const_typed_helpers (), get_untyped_helpers ()); |
|
199 |
|
200 |
136 |
201 (**** relevance filter ****) |
137 (**** relevance filter ****) |
202 val run_relevance_filter = ref true; |
138 val run_relevance_filter = ref true; |
203 |
139 |
204 (******************************************************************) |
140 (******************************************************************) |
345 val linkup_logic_mode = ref Auto; |
281 val linkup_logic_mode = ref Auto; |
346 |
282 |
347 fun tptp_writer logic goals filename (axioms,classrels,arities) = |
283 fun tptp_writer logic goals filename (axioms,classrels,arities) = |
348 if is_fol_logic logic |
284 if is_fol_logic logic |
349 then ResClause.tptp_write_file goals filename (axioms, classrels, arities) |
285 then ResClause.tptp_write_file goals filename (axioms, classrels, arities) |
350 else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) |
286 else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities); |
351 (get_all_helpers()); |
|
352 |
287 |
353 (*2006-04-07: not working: goals has type thm list (not term list as above) and |
288 (*2006-04-07: not working: goals has type thm list (not term list as above) and |
354 axioms has type ResClause.clause list (not (thm * (string * int)) list as above)*) |
289 axioms has type ResClause.clause list (not (thm * (string * int)) list as above)*) |
355 fun dfg_writer logic goals filename (axioms,classrels,arities) = |
290 fun dfg_writer logic goals filename (axioms,classrels,arities) = |
356 if is_fol_logic logic |
291 if is_fol_logic logic |