# HG changeset patch # User blanchet # Date 1306852716 -7200 # Node ID 269300fb83d0efa64a6bdc4ae9474f50268d0f58 # Parent 40e50afbc20308e530b98868788f15146b39d701 more work on new Metis diff -r 40e50afbc203 -r 269300fb83d0 src/HOL/Tools/ATP/atp_reconstruct.ML --- 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), diff -r 40e50afbc203 -r 269300fb83d0 src/HOL/Tools/Metis/metis_reconstruct.ML --- 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 diff -r 40e50afbc203 -r 269300fb83d0 src/HOL/Tools/Metis/metis_tactics.ML --- 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 diff -r 40e50afbc203 -r 269300fb83d0 src/HOL/Tools/Metis/metis_translate.ML --- 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;