--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Tue May 31 16:38:36 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Tue May 31 16:38:36 2011 +0200
@@ -8,6 +8,7 @@
signature ATP_RECONSTRUCT =
sig
+ type 'a fo_term = 'a ATP_Problem.fo_term
type 'a proof = 'a ATP_Proof.proof
type locality = ATP_Translate.locality
type type_system = ATP_Translate.type_system
@@ -42,6 +43,9 @@
val uses_typed_helpers : int list -> 'a proof -> bool
val reconstructor_name : reconstructor -> string
val one_line_proof_text : one_line_params -> string
+ val term_from_atp :
+ theory -> bool -> int Symtab.table -> (string * sort) list -> typ option
+ -> string fo_term -> term
val isar_proof_text :
Proof.context -> bool -> isar_params -> one_line_params -> string
val proof_text :
@@ -393,7 +397,7 @@
| add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl)
| add_type_constraint _ _ = I
-fun repair_tptp_variable_name f s =
+fun repair_variable_name f s =
let
fun subscript_name s n = s ^ nat_subscript n
val s = String.map f s
@@ -412,8 +416,10 @@
(* First-order translation. No types are known for variables. "HOLogic.typeT"
should allow them to be inferred. *)
-fun term_from_atp thy sym_tab tfrees =
+fun term_from_atp thy textual sym_tab tfrees =
let
+ (* see also "mk_var" in "Metis_Reconstruct" *)
+ val var_index = if textual then 0 else 1
fun do_term extra_us opt_T u =
case u of
ATerm (a, us) =>
@@ -421,7 +427,8 @@
@{const True} (* ignore TPTP type information *)
else if a = tptp_equal then
let val ts = map (do_term [] NONE) us in
- if length ts = 2 andalso hd ts aconv List.last ts then
+ if textual andalso length ts = 2 andalso
+ hd ts aconv List.last ts then
(* Vampire is keen on producing these. *)
@{const True}
else
@@ -473,22 +480,18 @@
SOME b => Free (b, T)
| NONE =>
case strip_prefix_and_unascii schematic_var_prefix a of
- SOME b => Var ((b, 0), T)
+ SOME b => Var ((b, var_index), T)
| NONE =>
- if is_tptp_variable a then
- Var ((repair_tptp_variable_name Char.toLower a, 0), T)
- else
- (* Skolem constants? *)
- Var ((repair_tptp_variable_name Char.toUpper a, 0), T)
+ Var ((repair_variable_name Char.toLower a, var_index), T)
in list_comb (t, ts) end
in do_term [] end
-fun term_from_atom thy sym_tab tfrees pos (u as ATerm (s, _)) =
+fun term_from_atom thy textual sym_tab tfrees pos (u as ATerm (s, _)) =
if String.isPrefix class_prefix s then
add_type_constraint pos (type_constraint_from_term tfrees u)
#> pair @{const True}
else
- pair (term_from_atp thy sym_tab tfrees (SOME @{typ bool}) u)
+ pair (term_from_atp thy textual sym_tab tfrees (SOME @{typ bool}) u)
val combinator_table =
[(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
@@ -533,7 +536,7 @@
(* Interpret an ATP formula as a HOL term, extracting sort constraints as they
appear in the formula. *)
-fun prop_from_formula thy sym_tab tfrees phi =
+fun prop_from_formula thy textual sym_tab tfrees phi =
let
fun do_formula pos phi =
case phi of
@@ -544,7 +547,7 @@
#>> quantify_over_var (case q of
AForall => forall_of
| AExists => exists_of)
- (repair_tptp_variable_name Char.toLower s)
+ (repair_variable_name Char.toLower s)
| AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not
| AConn (c, [phi1, phi2]) =>
do_formula (pos |> c = AImplies ? not) phi1
@@ -557,7 +560,7 @@
| AIff => s_iff
| ANotIff => s_not o s_iff
| _ => raise Fail "unexpected connective")
- | AAtom tm => term_from_atom thy sym_tab tfrees pos tm
+ | AAtom tm => term_from_atom thy textual sym_tab tfrees pos tm
| _ => raise FORMULA [phi]
in repair_tvar_sorts (do_formula true phi Vartab.empty) end
@@ -574,11 +577,11 @@
fun decode_line sym_tab tfrees (Definition (name, phi1, phi2)) ctxt =
let
val thy = Proof_Context.theory_of ctxt
- val t1 = prop_from_formula thy sym_tab tfrees phi1
+ val t1 = prop_from_formula thy true sym_tab tfrees phi1
val vars = snd (strip_comb t1)
val frees = map unvarify_term vars
val unvarify_args = subst_atomic (vars ~~ frees)
- val t2 = prop_from_formula thy sym_tab tfrees phi2
+ val t2 = prop_from_formula thy true sym_tab tfrees phi2
val (t1, t2) =
HOLogic.eq_const HOLogic.typeT $ t1 $ t2
|> unvarify_args |> uncombine_term thy |> check_formula ctxt
@@ -590,7 +593,7 @@
| decode_line sym_tab tfrees (Inference (name, u, deps)) ctxt =
let
val thy = Proof_Context.theory_of ctxt
- val t = u |> prop_from_formula thy sym_tab tfrees
+ val t = u |> prop_from_formula thy true sym_tab tfrees
|> uncombine_term thy |> check_formula ctxt
in
(Inference (name, t, deps),
--- 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
@@ -20,7 +20,7 @@
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
val untyped_aconv : term -> term -> bool
val replay_one_inference :
- Proof.context -> mode -> (string * term) list
+ Proof.context -> mode -> (string * term) list -> int Symtab.table
-> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
-> (Metis_Thm.thm * thm) list
val discharge_skolem_premises :
@@ -30,7 +30,9 @@
structure Metis_Reconstruct : METIS_RECONSTRUCT =
struct
+open ATP_Problem
open ATP_Translate
+open ATP_Reconstruct
open Metis_Translate
exception METIS of string * string
@@ -69,9 +71,9 @@
fun infer_types ctxt =
Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt);
-(*We use 1 rather than 0 because variable references in clauses may otherwise conflict
- with variable constraints in the goal...at least, type inference often fails otherwise.
- SEE ALSO axiom_inf below.*)
+(* We use 1 rather than 0 because variable references in clauses may otherwise
+ conflict with variable constraints in the goal...at least, type inference
+ often fails otherwise. See also "axiom_inf" below. *)
fun mk_var (w, T) = Var ((w, 1), T)
(*include the default sort, if available*)
@@ -80,8 +82,8 @@
in TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end;
(*Remove the "apply" operator from an HO term*)
-fun strip_happ args (Metis_Term.Fn(".",[t,u])) = strip_happ (u::args) t
- | strip_happ args x = (x, args);
+fun strip_happ args (Metis_Term.Fn (".", [t, u])) = strip_happ (u :: args) t
+ | strip_happ args x = (x, args)
fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
@@ -112,13 +114,13 @@
| NONE => SomeTerm (mk_var (v, HOLogic.typeT)))
(*Var from Metis with a name like _nnn; possibly a type variable*)
| tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*)
- | tm_to_tt (t as Metis_Term.Fn (".",_)) =
- let val (rator,rands) = strip_happ [] t
- in case rator of
- Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
- | _ => case tm_to_tt rator of
- SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands)))
- | _ => raise Fail "tm_to_tt: HO application"
+ | tm_to_tt (t as Metis_Term.Fn (".", _)) =
+ let val (rator,rands) = strip_happ [] t in
+ case rator of
+ Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
+ | _ => case tm_to_tt rator of
+ SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands)))
+ | _ => raise Fail "tm_to_tt: HO application"
end
| tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args)
and applic_to_tt ("=",ts) =
@@ -191,7 +193,7 @@
case strip_prefix_and_unascii fixed_var_prefix x of
SOME v => Free (v, hol_type_from_metis_term ctxt ty)
| NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
- | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".",[tm1,tm2]), _])) =
+ | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".", [tm1,tm2]), _])) =
cvt tm1 $ cvt tm2
| cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*)
cvt tm1 $ cvt tm2
@@ -212,13 +214,26 @@
hol_term_from_metis_PT ctxt t)
in fol_tm |> cvt 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 = ###*)
+fun atp_name_from_metis s =
+ case AList.find (op =) metis_name_table s of
+ [(s', ary)] => (s', SOME ary)
+ | _ => (s, NONE)
+fun atp_term_from_metis (Metis_Term.Fn (s, tms)) =
+ 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_terms_from_metis ctxt mode old_skolems fol_tms =
- let val ts = map (hol_term_from_metis mode ctxt) fol_tms
+fun hol_term_from_metis_New 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
+ 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
+
+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
val _ = trace_msg ctxt (fn () => " calling type inference:")
val _ = app (fn t => trace_msg ctxt
(fn () => Syntax.string_of_term ctxt t)) ts
@@ -242,8 +257,8 @@
trace_msg ctxt (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
*)
-fun lookth thpairs (fth : Metis_Thm.thm) =
- the (AList.lookup (uncurry Metis_Thm.equal) thpairs fth)
+fun lookth th_pairs fth =
+ the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth)
handle Option.Option =>
raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
@@ -251,8 +266,9 @@
(* INFERENCE RULE: AXIOM *)
-fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
- (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
+(* This causes variables to have an index of 1 by default. See also "mk_var"
+ above. *)
+fun axiom_inf th_pairs th = Thm.incr_indexes 1 (lookth th_pairs th)
(* INFERENCE RULE: ASSUME *)
@@ -264,10 +280,10 @@
val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
in cterm_instantiate substs th end;
-fun assume_inf ctxt mode skolem_params atm =
+fun assume_inf ctxt mode old_skolems sym_tab atm =
inst_excluded_middle
(Proof_Context.theory_of ctxt)
- (singleton (hol_terms_from_metis ctxt mode skolem_params)
+ (singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab)
(Metis_Term.Fn atm))
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
@@ -275,15 +291,15 @@
sorts. Instead we try to arrange that new TVars are distinct and that types
can be inferred from terms. *)
-fun inst_inf ctxt mode old_skolems thpairs fsubst th =
+fun inst_inf ctxt mode old_skolems sym_tab th_pairs fsubst th =
let val thy = Proof_Context.theory_of ctxt
- val i_th = lookth thpairs th
+ val i_th = lookth th_pairs th
val i_th_vars = Term.add_vars (prop_of i_th) []
fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
fun subst_translation (x,y) =
let val v = find_var x
(* We call "reveal_old_skolem_terms" and "infer_types" below. *)
- val t = hol_term_from_metis mode ctxt y
+ val t = hol_term_from_metis mode sym_tab ctxt y
in SOME (cterm_of thy (Var v), t) end
handle Option.Option =>
(trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
@@ -400,10 +416,10 @@
(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
val select_literal = negate_head oo make_last
-fun resolve_inf ctxt mode skolem_params thpairs atm th1 th2 =
+fun resolve_inf ctxt mode old_skolems sym_tab th_pairs atm th1 th2 =
let
val thy = Proof_Context.theory_of ctxt
- val (i_th1, i_th2) = pairself (lookth thpairs) (th1, th2)
+ val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2)
val _ = trace_msg ctxt (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
val _ = trace_msg ctxt (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
in
@@ -415,7 +431,7 @@
else
let
val i_atm =
- singleton (hol_terms_from_metis ctxt mode skolem_params)
+ singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab)
(Metis_Term.Fn atm)
val _ = trace_msg ctxt (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
val prems_th1 = prems_of i_th1
@@ -441,12 +457,13 @@
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
-fun refl_inf ctxt mode skolem_params t =
- let val thy = Proof_Context.theory_of ctxt
- val i_t = singleton (hol_terms_from_metis ctxt mode skolem_params) t
- val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
- val c_t = cterm_incr_types thy refl_idx i_t
- in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
+fun refl_inf ctxt mode old_skolems sym_tab t =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val i_t = singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab) t
+ val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
+ val c_t = cterm_incr_types thy refl_idx i_t
+ in cterm_instantiate [(refl_x, c_t)] REFL_THM end
(* INFERENCE RULE: EQUALITY *)
@@ -461,10 +478,11 @@
(num_type_args thy s handle TYPE _ => 0)
| get_ty_arg_size _ _ = 0
-fun equality_inf ctxt mode skolem_params (pos, atm) fp fr =
+fun equality_inf ctxt mode old_skolems sym_tab (pos, atm) fp fr =
let val thy = Proof_Context.theory_of ctxt
val m_tm = Metis_Term.Fn atm
- val [i_atm,i_tm] = hol_terms_from_metis ctxt mode skolem_params [m_tm, fr]
+ val [i_atm, i_tm] =
+ hol_terms_from_metis ctxt mode old_skolems sym_tab [m_tm, fr]
val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
fun replace_item_list lx 0 (_::ls) = lx::ls
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
@@ -472,7 +490,7 @@
| path_finder_FO tm (p::ps) =
let val (tm1,args) = strip_comb tm
val adjustment = get_ty_arg_size thy tm1
- val p' = if adjustment > p then p else p-adjustment
+ val p' = if adjustment > p then p else p - adjustment
val tm_p = nth args p'
handle Subscript =>
raise METIS ("equality_inf",
@@ -506,6 +524,32 @@
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)) =
+ let
+ val (tm1, args) = strip_comb tm
+ val adjustment =
+ case atp_name_from_metis s of
+ (_, SOME _) => 0
+ | (s', NONE) =>
+ length ts - the_default 0 (Symtab.lookup sym_tab s')
+ val p' = if adjustment > p then p else p - adjustment
+ val tm_p = nth args p'
+ handle Subscript =>
+ raise METIS ("equality_inf",
+ string_of_int p ^ " adj " ^
+ string_of_int adjustment ^ " term " ^
+ Syntax.string_of_term ctxt tm)
+ 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 t
+ in (r, list_comb (tm1, replace_item_list t p' args)) end
+ | path_finder_New tm ps t =
+ raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^
+ "equality_inf, path_finder_New: path = " ^
+ space_implode " " (map string_of_int ps) ^
+ " isa-term: " ^ Syntax.string_of_term ctxt tm ^
+ " fol-term: " ^ Metis_Term.toString t)
fun path_finder FO tm ps _ = path_finder_FO tm ps
| path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
(*equality: not curried, as other predicates are*)
@@ -517,15 +561,15 @@
(Metis_Term.Fn ("=", [t1,t2])) =
(*equality: not curried, as other predicates are*)
if p=0 then path_finder_FT tm (0::1::ps)
- (Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2]))
+ (Metis_Term.Fn (metis_app_op, [Metis_Term.Fn (metis_app_op, [metis_eq,t1]), t2]))
(*select first operand*)
else path_finder_FT tm (p::ps)
- (Metis_Term.Fn (".", [metis_eq,t2]))
+ (Metis_Term.Fn (metis_app_op, [metis_eq, t2]))
(*1 selects second operand*)
| 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 HO tm ps t (* ### *)
+ | path_finder New tm ps t = path_finder_New 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
@@ -542,19 +586,21 @@
(ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
in cterm_instantiate eq_terms subst' end;
-val factor = Seq.hd o distinct_subgoals_tac;
+val factor = Seq.hd o distinct_subgoals_tac
-fun step ctxt mode skolem_params thpairs p =
+fun one_step ctxt mode old_skolems sym_tab th_pairs p =
case p of
- (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
- | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode skolem_params f_atm
+ (fol_th, Metis_Proof.Axiom _) => axiom_inf th_pairs fol_th |> factor
+ | (_, Metis_Proof.Assume f_atm) =>
+ assume_inf ctxt mode old_skolems sym_tab f_atm
| (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
- factor (inst_inf ctxt mode skolem_params thpairs f_subst f_th1)
+ inst_inf ctxt mode old_skolems sym_tab th_pairs f_subst f_th1 |> factor
| (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
- factor (resolve_inf ctxt mode skolem_params thpairs f_atm f_th1 f_th2)
- | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode skolem_params f_tm
+ resolve_inf ctxt mode old_skolems sym_tab th_pairs f_atm f_th1 f_th2
+ |> factor
+ | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems sym_tab f_tm
| (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
- equality_inf ctxt mode skolem_params f_lit f_p f_r
+ equality_inf ctxt mode old_skolems sym_tab f_lit f_p f_r
fun flexflex_first_order th =
case Thm.tpairs_of th of
@@ -602,12 +648,13 @@
end
end
-fun replay_one_inference ctxt mode skolem_params (fol_th, inf) thpairs =
- if not (null thpairs) andalso prop_of (snd (hd thpairs)) aconv @{prop False} then
+fun replay_one_inference ctxt mode old_skolems sym_tab (fol_th, inf) th_pairs =
+ if not (null th_pairs) andalso
+ prop_of (snd (hd th_pairs)) aconv @{prop False} then
(* Isabelle sometimes identifies literals (premises) that are distinct in
Metis (e.g., because of type variables). We give the Isabelle proof the
benefice of the doubt. *)
- thpairs
+ th_pairs
else
let
val _ = trace_msg ctxt
@@ -616,14 +663,14 @@
(fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
val _ = trace_msg ctxt
(fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
- val th = step ctxt mode skolem_params thpairs (fol_th, inf)
+ val th = one_step ctxt mode old_skolems sym_tab th_pairs (fol_th, inf)
|> flexflex_first_order
|> resynchronize ctxt fol_th
val _ = trace_msg ctxt
(fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
val _ = trace_msg ctxt
(fn () => "=============================================")
- in (fol_th, th) :: thpairs end
+ in (fol_th, th) :: th_pairs end
(* It is normally sufficient to apply "assume_tac" to unify the conclusion with
one of the premises. Unfortunately, this sometimes yields "Variable
--- 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
@@ -84,7 +84,7 @@
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
- val (mode, {axioms, old_skolems, ...}) =
+ val (mode, sym_tab, {axioms, old_skolems, ...}) =
prepare_metis_problem ctxt mode cls ths
val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
val thms = map #1 axioms
@@ -103,8 +103,9 @@
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
(*add constraints arising from converting goal to clause form*)
val proof = Metis_Proof.proof mth
- val result = fold (replay_one_inference ctxt' mode old_skolems)
- proof axioms
+ val result =
+ fold (replay_one_inference ctxt' mode old_skolems sym_tab)
+ proof axioms
and used = map_filter (used_axioms axioms) proof
val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
--- 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
@@ -14,15 +14,20 @@
datatype mode = FO | HO | FT | New
type metis_problem =
- {axioms: (Metis_Thm.thm * thm) list,
- tfrees: type_literal list,
- old_skolems: (string * term) list}
+ {axioms : (Metis_Thm.thm * thm) list,
+ tfrees : type_literal list,
+ old_skolems : (string * term) list}
+ val metis_equal : string
+ val metis_predicator : string
+ val metis_app_op : string
val metis_generated_var_prefix : string
+ val metis_name_table : ((string * int) * string) list
val reveal_old_skolem_terms : (string * term) list -> term -> term
val string_of_mode : mode -> string
val prepare_metis_problem :
- Proof.context -> mode -> thm list -> thm list -> mode * metis_problem
+ Proof.context -> mode -> thm list -> thm list
+ -> mode * int Symtab.table * metis_problem
end
structure Metis_Translate : METIS_TRANSLATE =
@@ -31,8 +36,17 @@
open ATP_Problem
open ATP_Translate
+val metis_equal = "="
+val metis_predicator = "{}"
+val metis_app_op = "."
val metis_generated_var_prefix = "_"
+val metis_name_table =
+ [((tptp_equal, 2), metis_equal),
+ ((tptp_old_equal, 2), metis_equal),
+ ((predicator_name, 1), metis_predicator),
+ ((app_op_name, 2), metis_app_op)]
+
fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
| predicate_of thy (t, pos) =
(combterm_from_term thy [] (Envir.eta_contract t), pos)
@@ -113,7 +127,7 @@
| fn_isa_to_met_sublevel "c_implies" = "c_fimplies"
| fn_isa_to_met_sublevel x = x
-fun fn_isa_to_met_toplevel "equal" = "="
+fun fn_isa_to_met_toplevel "equal" = metis_equal
| fn_isa_to_met_toplevel x = x
fun metis_lit b c args = (b, (c, args));
@@ -138,10 +152,10 @@
| _ => raise Fail "non-first-order combterm"
fun hol_term_to_fol_HO (CombConst ((a, _), _, Ts)) =
- Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_typ Ts)
+ Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_typ Ts)
| hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s
| hol_term_to_fol_HO (CombApp (tm1, tm2)) =
- Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
+ Metis_Term.Fn (metis_app_op, map hol_term_to_fol_HO [tm1, tm2])
(*The fully-typed translation, to avoid type errors*)
fun tag_with_type tm T =
@@ -152,8 +166,9 @@
| hol_term_to_fol_FT (CombConst ((a, _), ty, _)) =
tag_with_type (Metis_Term.Fn (fn_isa_to_met_sublevel a, [])) ty
| hol_term_to_fol_FT (tm as CombApp (tm1,tm2)) =
- tag_with_type (Metis_Term.Fn (".", map hol_term_to_fol_FT [tm1, tm2]))
- (combtyp_of tm)
+ tag_with_type
+ (Metis_Term.Fn (metis_app_op, map hol_term_to_fol_FT [tm1, tm2]))
+ (combtyp_of tm)
fun hol_literal_to_fol FO (pos, tm) =
let
@@ -164,13 +179,13 @@
| hol_literal_to_fol HO (pos, tm) =
(case strip_combterm_comb tm of
(CombConst(("equal", _), _, _), tms) =>
- metis_lit pos "=" (map hol_term_to_fol_HO tms)
- | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm]) (*hBOOL*)
+ metis_lit pos metis_equal (map hol_term_to_fol_HO tms)
+ | _ => metis_lit pos metis_predicator [hol_term_to_fol_HO tm])
| hol_literal_to_fol FT (pos, tm) =
(case strip_combterm_comb tm of
(CombConst(("equal", _), _, _), tms) =>
- metis_lit pos "=" (map hol_term_to_fol_FT tms)
- | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
+ metis_lit pos metis_equal (map hol_term_to_fol_FT tms)
+ | _ => metis_lit pos metis_predicator [hol_term_to_fol_FT tm])
fun literals_of_hol_term thy mode t =
let val (lits, types_sorts) = literals_of_term thy t in
@@ -217,9 +232,9 @@
(* ------------------------------------------------------------------------- *)
type metis_problem =
- {axioms: (Metis_Thm.thm * thm) list,
- tfrees: type_literal list,
- old_skolems: (string * term) list}
+ {axioms : (Metis_Thm.thm * thm) list,
+ tfrees : type_literal list,
+ old_skolems : (string * term) list}
fun is_quasi_fol_clause thy =
Meson.is_fol_term thy o snd o conceal_old_skolem_terms ~1 [] o prop_of
@@ -266,16 +281,16 @@
val class_rel_clauses = make_class_rel_clauses thy subs supers'
in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses end
-fun metis_name_from_atp s =
- if is_tptp_equal s then "="
- else if s = predicator_name then "{}"
- else if s = app_op_name then "."
- else s
+fun metis_name_from_atp s ary =
+ AList.lookup (op =) metis_name_table (s, ary) |> the_default s
fun metis_term_from_atp (ATerm (s, tms)) =
- if is_tptp_variable s then Metis_Term.Var s
- else Metis_Term.Fn (metis_name_from_atp s, map metis_term_from_atp tms)
+ if is_tptp_variable s then
+ Metis_Term.Var s
+ else
+ Metis_Term.Fn (metis_name_from_atp s (length tms),
+ map metis_term_from_atp tms)
fun metis_atom_from_atp (AAtom (ATerm (s, tms))) =
- (metis_name_from_atp s, map metis_term_from_atp tms)
+ (metis_name_from_atp s (length tms), map metis_term_from_atp tms)
| metis_atom_from_atp _ = raise Fail "not CNF -- expected atom"
fun metis_literal_from_atp (AConn (ANot, [phi])) =
(false, metis_atom_from_atp phi)
@@ -294,10 +309,10 @@
(* Function to generate metis clauses, including comb and type clauses *)
fun prepare_metis_problem ctxt New conj_clauses fact_clauses =
let
- val type_sys = Preds (Polymorphic, (* Nonmonotonic_Types FIXME ### *) No_Types, Light)
+ val type_sys = Preds (Polymorphic, (* Nonmonotonic_Types FIXME ### *) Const_Arg_Types, Light)
val explicit_apply = NONE
val clauses = conj_clauses @ fact_clauses
- val (atp_problem, pool, _, _, _, _, sym_tab) =
+ val (atp_problem, _, _, _, _, _, sym_tab) =
prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys
explicit_apply false (map prop_of clauses)
@{prop False} []
@@ -305,7 +320,10 @@
val axioms =
atp_problem
|> maps (map_filter (try (metis_axiom_from_atp clauses)) o snd)
- in (New, {axioms = axioms, tfrees = [], old_skolems = [] (* FIXME ### *)}) end
+ in
+ (New, sym_tab,
+ {axioms = axioms, tfrees = [], old_skolems = [] (* FIXME ### *)})
+ end
| prepare_metis_problem ctxt mode conj_clauses fact_clauses =
let
val thy = Proof_Context.theory_of ctxt
@@ -361,6 +379,6 @@
else map prepare_helper thms)
in problem |> fold (add_thm false) helper_ths end
val type_ths = type_ext thy (map prop_of (conj_clauses @ fact_clauses))
- in (mode, fold add_type_thm type_ths problem) end
+ in (mode, Symtab.empty, fold add_type_thm type_ths problem) end
end;