# HG changeset patch # User blanchet # Date 1286794934 -25200 # Node ID 11bfb7e7cc8660a2d3e22416904c01e695f4b4a1 # Parent c9cbc16e93ce0b2dca79b2bd881f359c482543bb added "trace_metis" configuration option, replacing old-fashioned references diff -r c9cbc16e93ce -r 11bfb7e7cc86 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Sun Oct 10 23:16:24 2010 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Oct 11 18:02:14 2010 +0700 @@ -11,7 +11,8 @@ sig type mode = Metis_Translate.mode - val trace : bool Unsynchronized.ref + val trace : bool Config.T + val trace_msg : Proof.context -> (unit -> string) -> unit val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a val untyped_aconv : term -> term -> bool val replay_one_inference : @@ -20,6 +21,7 @@ -> (Metis_Thm.thm * thm) list val discharge_skolem_premises : Proof.context -> (thm * term) option list -> thm -> thm + val setup : theory -> theory end; structure Metis_Reconstruct : METIS_RECONSTRUCT = @@ -27,8 +29,9 @@ open Metis_Translate -val trace = Unsynchronized.ref false -fun trace_msg msg = if !trace then tracing (msg ()) else () +val (trace, trace_setup) = Attrib.config_bool "trace_metis" (K false) + +fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else () datatype term_or_type = SomeTerm of term | SomeType of typ @@ -92,8 +95,8 @@ (*Maps metis terms to isabelle terms*) fun hol_term_from_metis_PT ctxt fol_tm = let val thy = ProofContext.theory_of ctxt - val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^ - Metis_Term.toString fol_tm) + val _ = trace_msg ctxt (fn () => "hol_term_from_metis_PT: " ^ + Metis_Term.toString fol_tm) fun tm_to_tt (Metis_Term.Var v) = (case strip_prefix_and_unascii tvar_prefix v of SOME w => SomeType (make_tvar w) @@ -160,8 +163,8 @@ (*Maps fully-typed metis terms to isabelle terms*) fun hol_term_from_metis_FT ctxt fol_tm = - let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^ - Metis_Term.toString fol_tm) + let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^ + Metis_Term.toString fol_tm) fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) = (case strip_prefix_and_unascii schematic_var_prefix v of SOME w => mk_var(w, dummyT) @@ -188,10 +191,12 @@ | NONE => (*Not a constant. Is it a fixed variable??*) case strip_prefix_and_unascii fixed_var_prefix x of SOME v => Free (v, dummyT) - | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x); - hol_term_from_metis_PT ctxt t)) - | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t); - hol_term_from_metis_PT ctxt t) + | NONE => (trace_msg ctxt (fn () => + "hol_term_from_metis_FT bad const: " ^ x); + hol_term_from_metis_PT ctxt t)) + | cvt t = (trace_msg ctxt (fn () => + "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t); + hol_term_from_metis_PT ctxt t) in fol_tm |> cvt end fun hol_term_from_metis FT = hol_term_from_metis_FT @@ -199,11 +204,12 @@ fun hol_terms_from_fol ctxt mode old_skolems fol_tms = let val ts = map (hol_term_from_metis mode ctxt) fol_tms - val _ = trace_msg (fn () => " calling type inference:") - val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts + val _ = trace_msg ctxt (fn () => " calling type inference:") + val _ = app (fn t => trace_msg ctxt + (fn () => Syntax.string_of_term ctxt t)) ts val ts' = ts |> map (reveal_old_skolem_terms old_skolems) |> infer_types ctxt - val _ = app (fn t => trace_msg + val _ = app (fn t => trace_msg ctxt (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ " of type " ^ Syntax.string_of_typ ctxt (type_of t))) ts' @@ -215,10 +221,10 @@ (*for debugging only*) (* -fun print_thpair (fth,th) = - (trace_msg (fn () => "============================================="); - trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth); - trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th)); +fun print_thpair ctxt (fth,th) = + (trace_msg ctxt (fn () => "============================================="); + trace_msg ctxt (fn () => "Metis: " ^ Metis_Thm.toString fth); + trace_msg ctxt (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th)); *) fun lookth thpairs (fth : Metis_Thm.thm) = @@ -264,12 +270,12 @@ val t = hol_term_from_metis mode ctxt y in SOME (cterm_of thy (Var v), t) end handle Option.Option => - (trace_msg (fn () => "\"find_var\" failed for " ^ x ^ - " in " ^ Display.string_of_thm ctxt i_th); + (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^ + " in " ^ Display.string_of_thm ctxt i_th); NONE) | TYPE _ => - (trace_msg (fn () => "\"hol_term_from_metis\" failed for " ^ x ^ - " in " ^ Display.string_of_thm ctxt i_th); + (trace_msg ctxt (fn () => "\"hol_term_from_metis\" failed for " ^ x ^ + " in " ^ Display.string_of_thm ctxt i_th); NONE) fun remove_typeinst (a, t) = case strip_prefix_and_unascii schematic_var_prefix a of @@ -277,14 +283,14 @@ | NONE => case strip_prefix_and_unascii tvar_prefix a of SOME _ => NONE (*type instantiations are forbidden!*) | NONE => SOME (a,t) (*internal Metis var?*) - val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) + val _ = trace_msg ctxt (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst) val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs) val tms = rawtms |> map (reveal_old_skolem_terms old_skolems) |> infer_types ctxt val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) val substs' = ListPair.zip (vars, map ctm_of tms) - val _ = trace_msg (fn () => + val _ = trace_msg ctxt (fn () => cat_lines ("subst_translations:" :: (substs' |> map (fn (x, y) => Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ @@ -375,8 +381,8 @@ let val thy = ProofContext.theory_of ctxt val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 - val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) - val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_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 (* Trivial cases where one operand is type info *) if Thm.eq_thm (TrueI, i_th1) then @@ -387,15 +393,15 @@ let val i_atm = singleton (hol_terms_from_fol ctxt mode old_skolems) (Metis_Term.Fn atm) - val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) + val _ = trace_msg ctxt (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) val prems_th1 = prems_of i_th1 val prems_th2 = prems_of i_th2 val index_th1 = literal_index (mk_not i_atm) prems_th1 handle Empty => raise Fail "Failed to find literal in th1" - val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1) + val _ = trace_msg ctxt (fn () => " index_th1: " ^ Int.toString index_th1) val index_th2 = literal_index i_atm prems_th2 handle Empty => raise Fail "Failed to find literal in th2" - val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2) + val _ = trace_msg ctxt (fn () => " index_th2: " ^ Int.toString index_th2) in resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2 end @@ -411,7 +417,7 @@ fun refl_inf ctxt mode old_skolems t = let val thy = ProofContext.theory_of ctxt val i_t = singleton (hol_terms_from_fol ctxt mode old_skolems) t - val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_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; @@ -430,7 +436,7 @@ let val thy = ProofContext.theory_of ctxt val m_tm = Metis_Term.Fn atm val [i_atm,i_tm] = hol_terms_from_fol ctxt mode old_skolems [m_tm, fr] - val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos) + 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 fun path_finder_FO tm [] = (tm, Bound 0) @@ -444,7 +450,7 @@ "equality_inf: " ^ Int.toString p ^ " adj " ^ Int.toString adjustment ^ " term " ^ Syntax.string_of_term ctxt tm) - val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^ + val _ = trace_msg ctxt (fn () => "path_finder: " ^ Int.toString p ^ " " ^ Syntax.string_of_term ctxt tm_p) val (r,t) = path_finder_FO tm_p ps in @@ -496,12 +502,12 @@ | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm val (tm_subst, body) = path_finder_lit i_atm fp val tm_abs = Abs ("x", type_of tm_subst, body) - val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) - val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) - val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) + val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) + val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) + val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*) val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) - val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst') + val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst') val eq_terms = map (pairself (cterm_of thy)) (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) in cterm_instantiate eq_terms subst' end; @@ -540,13 +546,13 @@ fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs = let - val _ = trace_msg (fn () => "=============================================") - val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) - val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) + val _ = trace_msg ctxt (fn () => "=============================================") + val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) + val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) val th = step ctxt mode old_skolems thpairs (fol_th, inf) |> flexflex_first_order - val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) - val _ = trace_msg (fn () => "=============================================") + val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) + val _ = trace_msg ctxt (fn () => "=============================================") val num_metis_lits = fol_th |> Metis_Thm.clause |> Metis_LiteralSet.toList |> count is_metis_literal_genuine @@ -556,8 +562,6 @@ else error "Cannot replay Metis proof in Isabelle: Out of sync." in (fol_th, th) :: thpairs end -(* FIXME ### GET RID OF skolem WRAPPER by looking at substitution *) - fun term_instantiate thy = cterm_instantiate o map (pairself (cterm_of thy)) (* In principle, it should be sufficient to apply "assume_tac" to unify the @@ -790,8 +794,10 @@ THEN ALLGOALS (fn i => rtac @{thm Meson.skolem_COMBK_I} i THEN rotate_tac (rotation_for_subgoal i) i - THEN PRIMITIVE (unify_first_prem_with_concl thy i) +(* THEN PRIMITIVE (unify_first_prem_with_concl thy i) ###*) THEN assume_tac i))) end +val setup = trace_setup + end; diff -r c9cbc16e93ce -r 11bfb7e7cc86 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Sun Oct 10 23:16:24 2010 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Mon Oct 11 18:02:14 2010 +0700 @@ -9,7 +9,6 @@ signature METIS_TACTICS = sig - val trace : bool Unsynchronized.ref val type_lits : bool Config.T val new_skolemizer : bool Config.T val metis_tac : Proof.context -> thm list -> int -> tactic @@ -24,8 +23,6 @@ open Metis_Translate open Metis_Reconstruct -fun trace_msg msg = if !trace then tracing (msg ()) else () - val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true) val (new_skolemizer, new_skolemizer_setup) = Attrib.config_bool "metis_new_skolemizer" (K false) @@ -67,21 +64,21 @@ (0 upto length ths0 - 1) ths0 val thss = map (snd o snd) th_cls_pairs val dischargers = map (fst o snd) th_cls_pairs - val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") - val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls - val _ = trace_msg (fn () => "THEOREM CLAUSES") - val _ = app (app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th))) thss + val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") + val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls + val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") + val _ = app (app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th))) thss val (mode, {axioms, tfrees, old_skolems}) = build_logic_map mode ctxt type_lits cls thss val _ = if null tfrees then () - else (trace_msg (fn () => "TFREE CLAUSES"); + else (trace_msg ctxt (fn () => "TFREE CLAUSES"); app (fn TyLitFree ((s, _), (s', _)) => - trace_msg (fn () => s ^ "(" ^ s' ^ ")")) tfrees) - val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS") + trace_msg ctxt (fn () => s ^ "(" ^ s' ^ ")")) tfrees) + val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS") val thms = map #1 axioms - val _ = app (fn th => trace_msg (fn () => Metis_Thm.toString th)) thms - val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode) - val _ = trace_msg (fn () => "START METIS PROVE PROCESS") + val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms + val _ = trace_msg ctxt (fn () => "mode = " ^ string_of_mode mode) + val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS") in case filter (is_false o prop_of) cls of false_th::_ => [false_th RS @{thm FalseE}] @@ -89,7 +86,7 @@ case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []} |> Metis_Resolution.loop of Metis_Resolution.Contradiction mth => - let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^ + let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ Metis_Thm.toString mth) val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt (*add constraints arising from converting goal to clause form*) @@ -97,8 +94,8 @@ val result = fold (replay_one_inference ctxt' mode old_skolems) proof axioms and used = map_filter (used_axioms axioms) proof - val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:") - val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used + 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 val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) => if have_common_thm used cls then NONE else SOME name) in @@ -113,12 +110,12 @@ (); case result of (_,ith)::_ => - (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith); + (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith); [discharge_skolem_premises ctxt dischargers ith]) - | _ => (trace_msg (fn () => "Metis: No result"); []) + | _ => (trace_msg ctxt (fn () => "Metis: No result"); []) end | Metis_Resolution.Satisfiable _ => - (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied"); + (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied"); []) end; @@ -150,7 +147,7 @@ fun generic_metis_tac mode ctxt ths i st0 = let - val _ = trace_msg (fn () => + val _ = trace_msg ctxt (fn () => "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) in if exists_type type_has_top_sort (prop_of st0) then