--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue May 31 16:38:36 2011 +0200
@@ -222,15 +222,16 @@
ATerm (fst (atp_name_from_metis s), map atp_term_from_metis tms)
| atp_term_from_metis (Metis_Term.Var s) = ATerm (s, [])
-fun hol_term_from_metis_New sym_tab ctxt =
+fun hol_term_from_metis_MX sym_tab ctxt =
let val thy = Proof_Context.theory_of ctxt in
- atp_term_from_metis #> term_from_atp thy false sym_tab [](*###tfrees*) NONE
+ atp_term_from_metis #> term_from_atp thy false sym_tab []
+ (* FIXME ### tfrees instead of []? *) NONE
end
fun hol_term_from_metis FO _ = hol_term_from_metis_PT
| hol_term_from_metis HO _ = hol_term_from_metis_PT
| hol_term_from_metis FT _ = hol_term_from_metis_FT
- | hol_term_from_metis New sym_tab = hol_term_from_metis_New sym_tab
+ | hol_term_from_metis MX sym_tab = hol_term_from_metis_MX sym_tab
fun hol_terms_from_metis ctxt mode old_skolems sym_tab fol_tms =
let val ts = map (hol_term_from_metis mode sym_tab ctxt) fol_tms
@@ -524,13 +525,13 @@
space_implode " " (map string_of_int ps) ^
" isa-term: " ^ Syntax.string_of_term ctxt tm ^
" fol-term: " ^ Metis_Term.toString t)
- fun path_finder_New tm [] _ = (tm, Bound 0)
- | path_finder_New tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
+ fun path_finder_MX tm [] _ = (tm, Bound 0)
+ | path_finder_MX tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
if s = metis_app_op (* FIXME ### mangled etc. *) then
let
val (tm1, tm2) = dest_comb tm in
- if p = 0 then path_finder_New tm1 ps (hd ts) ||> (fn y => y $ tm2)
- else path_finder_New tm2 ps (nth ts 1) ||> (fn y => tm1 $ y)
+ if p = 0 then path_finder_MX tm1 ps (hd ts) ||> (fn y => y $ tm2)
+ else path_finder_MX tm2 ps (nth ts 1) ||> (fn y => tm1 $ y)
end
else
let
@@ -546,11 +547,11 @@
val _ = trace_msg ctxt (fn () =>
"path_finder: " ^ string_of_int p ^ " " ^
Syntax.string_of_term ctxt tm_p)
- val (r, t) = path_finder_New tm_p ps (nth ts p)
+ val (r, t) = path_finder_MX tm_p ps (nth ts p)
in (r, list_comb (tm1, replace_item_list t p' args)) end
- | path_finder_New tm ps t =
+ | path_finder_MX tm ps t =
raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
- "equality_inf, path_finder_New: path = " ^
+ "equality_inf, path_finder_MX: path = " ^
space_implode " " (map string_of_int ps) ^
" isa-term: " ^ Syntax.string_of_term ctxt tm ^
" fol-term: " ^ Metis_Term.toString t)
@@ -573,7 +574,7 @@
| path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
(*if not equality, ignore head to skip the hBOOL predicate*)
| path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*)
- | path_finder New tm ps t = path_finder_New tm ps t
+ | path_finder MX tm ps t = path_finder_MX tm ps t
fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
in (tm, nt $ tm_rslt) end
--- a/src/HOL/Tools/Metis/metis_tactics.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue May 31 16:38:36 2011 +0200
@@ -36,12 +36,12 @@
fun method_binding_for_mode HO = @{binding metis}
| method_binding_for_mode FO = @{binding metisF}
| method_binding_for_mode FT = @{binding metisFT}
- | method_binding_for_mode New = @{binding metisX}
+ | method_binding_for_mode MX = @{binding metisX}
val metisN = Binding.qualified_name_of (method_binding_for_mode HO)
val metisF_N = Binding.qualified_name_of (method_binding_for_mode FO)
val metisFT_N = Binding.qualified_name_of (method_binding_for_mode FT)
-val metisX_N = Binding.qualified_name_of (method_binding_for_mode New)
+val metisX_N = Binding.qualified_name_of (method_binding_for_mode MX)
val new_skolemizer =
Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
@@ -184,7 +184,7 @@
val metisF_modes = [FO, FT]
val metisFT_modes = [FT]
val metisHO_modes = [HO]
-val metisX_modes = [New]
+val metisX_modes = [MX]
val metis_tac = generic_metis_tac metis_modes NONE
val metisF_tac = generic_metis_tac metisF_modes NONE
@@ -212,7 +212,7 @@
fun setup_method (modes as mode :: _) =
Method.setup (method_binding_for_mode mode)
- ((if mode = New then
+ ((if mode = MX then
Scan.lift (Scan.option (Args.parens Parse.short_ident))
else
Scan.succeed NONE)
--- a/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue May 31 16:38:36 2011 +0200
@@ -12,7 +12,7 @@
type type_literal = ATP_Translate.type_literal
type type_sys = ATP_Translate.type_sys
- datatype mode = FO | HO | FT | New
+ datatype mode = FO | HO | FT | MX
type metis_problem =
{axioms : (Metis_Thm.thm * thm) list,
@@ -111,13 +111,13 @@
(* HOL to FOL (Isabelle to Metis) *)
(* ------------------------------------------------------------------------- *)
-(* first-order, higher-order, fully-typed, new *)
-datatype mode = FO | HO | FT | New
+(* first-order, higher-order, fully-typed, mode X (fleXible) *)
+datatype mode = FO | HO | FT | MX
fun string_of_mode FO = "FO"
| string_of_mode HO = "HO"
| string_of_mode FT = "FT"
- | string_of_mode New = "New"
+ | string_of_mode MX = "MX"
fun fn_isa_to_met_sublevel "equal" = "c_fequal"
| fn_isa_to_met_sublevel "c_False" = "c_fFalse"
@@ -310,7 +310,7 @@
val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Light)
(* Function to generate metis clauses, including comb and type clauses *)
-fun prepare_metis_problem ctxt New type_sys conj_clauses fact_clauses =
+fun prepare_metis_problem ctxt MX type_sys conj_clauses fact_clauses =
let
val type_sys = type_sys |> the_default default_type_sys
val explicit_apply = NONE
@@ -322,7 +322,7 @@
atp_problem
|> maps (map_filter (try (metis_axiom_from_atp clauses)) o snd)
in
- (New, sym_tab,
+ (MX, sym_tab,
{axioms = axioms, tfrees = [], old_skolems = [] (* FIXME ### *)})
end
| prepare_metis_problem ctxt mode _ conj_clauses fact_clauses =