# HG changeset patch # User wenzelm # Date 1436128334 -7200 # Node ID e007aa6a8aa23f374dd414c533d80f1449552eab # Parent 6c4550cd1b17d344aae12347cd99b6ca327b6656 more explicit use of context and elimination of Thm.theory_of_thm, although unclear (and untested?) situations remain; diff -r 6c4550cd1b17 -r e007aa6a8aa2 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Sun Jul 05 22:07:09 2015 +0200 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Sun Jul 05 22:32:14 2015 +0200 @@ -1029,12 +1029,14 @@ val thy = Proof_Context.theory_of ctxt val pannot = get_pannot_of_prob thy prob_name +(* FIXME !???! fun rtac_wrap thm_f i = fn st => let val thy = Thm.theory_of_thm st in rtac (thm_f thy) i st end +*) (*Some nodes don't have an inference name, such as the conjecture, definitions and axioms. Such nodes shouldn't appear in the @@ -1063,14 +1065,7 @@ let fun thm ctxt'' = prover_tac ctxt'' prob_name (hd skel |> stock_to_string) val reconstructed_inference = thm ctxt' - val rec_inf_tac = fn st => - let - val ctxt = - Thm.theory_of_thm st - |> Proof_Context.init_global - in - HEADGOAL (rtac (thm ctxt)) st - end + fun rec_inf_tac st = HEADGOAL (rtac (thm ctxt')) st in (reconstructed_inference, rec_inf_tac) end) @@ -1157,14 +1152,16 @@ else let val maybe_thm = ignore_interpretation_exn try_make_step ctxt +(* FIXME !???! val ctxt' = if is_some maybe_thm then the maybe_thm |> #1 |> Thm.theory_of_thm |> Proof_Context.init_global else ctxt +*) in - (maybe_thm, ctxt') + (maybe_thm, ctxt) end in (thm, (node, thm) :: memo, ctxt') end | SOME maybe_thm => (maybe_thm, memo, ctxt) @@ -1183,8 +1180,7 @@ (hd skel, Thm.prop_of (def_thm thy) |> SOME, - SOME (def_thm thy, - HEADGOAL (rtac_wrap def_thm))) :: rest memo ctxt + SOME (def_thm thy, HEADGOAL (rtac (def_thm thy)))) :: rest memo ctxt end | Axiom n => let diff -r 6c4550cd1b17 -r e007aa6a8aa2 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Sun Jul 05 22:07:09 2015 +0200 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Sun Jul 05 22:32:14 2015 +0200 @@ -329,10 +329,8 @@ *} ML {* -(*given a thm, show us the axioms in its thy*) -val axms_of_thy_of_thm = - Thm.theory_of_thm - #> ` Theory.axioms_of +val axms_of_thy = + `Theory.axioms_of #> apsnd cterm_of #> swap #> apsnd (map snd) @@ -351,14 +349,8 @@ *} ML {* -fun leo2_tac_wrap prob_name step i = fn st => - let - val ctxt = - Thm.theory_of_thm st - |> Proof_Context.init_global - in - rtac (interpret_leo2_inference ctxt prob_name step) i st - end +fun leo2_tac_wrap ctxt prob_name step i st = + rtac (interpret_leo2_inference ctxt prob_name step) i st *} (*FIXME move these examples elsewhere*) diff -r 6c4550cd1b17 -r e007aa6a8aa2 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy Sun Jul 05 22:07:09 2015 +0200 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy Sun Jul 05 22:32:14 2015 +0200 @@ -7,7 +7,7 @@ - Makes use of the PolyML structure. *) -theory TPTP_Proof_Reconstruction_Test +theory TPTP_Proof_Reconstruction_Test_Units imports TPTP_Test TPTP_Proof_Reconstruction begin @@ -482,16 +482,7 @@ (\ SEU602_2_bnd_in (SEU602_2_bnd_sK7_E SV49) SEU602_2_bnd_sK2_SY17)) = False" (*FIXME this (and similar) tests are getting the "Bad background theory of goal state" error since upgrading to Isabelle2013-2.*) -by (tactic {*fn thm => - let - val ctxt = - theory_of_thm thm - |> Context.Theory - |> Context.proof_of - in nonfull_extcnf_combined_tac ctxt [Extuni_Func, Existential_Var] thm - end*}) -(*by (tactic {*nonfull_extcnf_combined_tac @{context} [Extuni_Func, Existential_Var]*})*) -oops +by (tactic {*nonfull_extcnf_combined_tac @{context} [Extuni_Func, Existential_Var]*}) consts SEV405_5_bnd_sK1_SY2 :: "(TPTP_Interpret.ind \ bool) \ TPTP_Interpret.ind" diff -r 6c4550cd1b17 -r e007aa6a8aa2 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Sun Jul 05 22:07:09 2015 +0200 +++ b/src/HOL/TPTP/mash_export.ML Sun Jul 05 22:32:14 2015 +0200 @@ -263,8 +263,8 @@ val suggs = old_facts |> filter_accessible_from th - |> mepo_or_mash_suggested_facts ctxt (Thm.theory_of_thm th) params max_suggs hyp_ts - concl_t + |> mepo_or_mash_suggested_facts ctxt (Thm.theory_name_of_thm th) + params max_suggs hyp_ts concl_t |> map (nickname_of_thm ctxt o snd) in encode_str name ^ ": " ^ encode_strs suggs ^ "\n" @@ -290,11 +290,11 @@ (Options.put_default @{system_option MaSh} algorithm; Sledgehammer_MaSh.mash_unlearn (); generate_mepo_or_mash_suggestions - (fn ctxt => fn thy => fn params as {provers = prover :: _, ...} => fn max_suggs => fn hyp_ts => - fn concl_t => + (fn ctxt => fn thy_name => fn params as {provers = prover :: _, ...} => + fn max_suggs => fn hyp_ts => fn concl_t => tap (Sledgehammer_MaSh.mash_learn_facts ctxt params prover 2 false Sledgehammer_Util.one_year) - #> Sledgehammer_MaSh.mash_suggested_facts ctxt thy params max_suggs hyp_ts concl_t + #> Sledgehammer_MaSh.mash_suggested_facts ctxt thy_name params max_suggs hyp_ts concl_t #> fst)) fun generate_mesh_suggestions max_suggs mash_file_name mepo_file_name mesh_file_name = diff -r 6c4550cd1b17 -r e007aa6a8aa2 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Jul 05 22:07:09 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sun Jul 05 22:32:14 2015 +0200 @@ -66,7 +66,7 @@ val weight_facts_steeply : 'a list -> ('a * real) list val find_mash_suggestions : Proof.context -> int -> string list -> ('a * thm) list -> ('a * thm) list -> ('a * thm) list -> ('a * thm) list * ('a * thm) list - val mash_suggested_facts : Proof.context -> theory -> params -> int -> term list -> term -> + val mash_suggested_facts : Proof.context -> string -> params -> int -> term list -> term -> raw_fact list -> fact list * fact list val mash_unlearn : unit -> unit @@ -1145,9 +1145,8 @@ (mesh_facts (eq_snd (gen_eq_thm ctxt)) max_facts mess, unknown) end -fun mash_suggested_facts ctxt thy ({debug, ...} : params) max_suggs hyp_ts concl_t facts = +fun mash_suggested_facts ctxt thy_name ({debug, ...} : params) max_suggs hyp_ts concl_t facts = let - val thy_name = Context.theory_name thy val algorithm = the_mash_algorithm () val facts = facts @@ -1167,7 +1166,7 @@ peek_state ctxt val goal_feats0 = - features_of ctxt (Context.theory_name thy) (Local, General) (concl_t :: hyp_ts) + features_of ctxt thy_name (Local, General) (concl_t :: hyp_ts) val chained_feats = chained |> map (rpair 1.0) |> map (chained_or_extra_features_of chained_feature_factor) @@ -1513,7 +1512,7 @@ [("", [])] else let - val thy = Proof_Context.theory_of ctxt + val thy_name = Context.theory_name (Proof_Context.theory_of ctxt) fun maybe_launch_thread exact min_num_facts_to_learn = if not (Async_Manager_Legacy.has_running_threads MaShN) andalso @@ -1576,8 +1575,8 @@ |> weight_facts_steeply, []) fun mash () = - mash_suggested_facts ctxt thy params (generous_max_suggestions max_facts) hyp_ts concl_t - facts + mash_suggested_facts ctxt thy_name params + (generous_max_suggestions max_facts) hyp_ts concl_t facts |>> weight_facts_steeply val mess =