# HG changeset patch # User wenzelm # Date 1391276566 -3600 # Node ID 8d61b0aa7a0d44f49ae565fbf5d96cfdbea254ff # Parent 4b4627f5912bcfe3c96a5df15ea1bd11f7d2630e proper context for printing; diff -r 4b4627f5912b -r 8d61b0aa7a0d src/HOL/Tools/Meson/meson_clausify.ML --- a/src/HOL/Tools/Meson/meson_clausify.ML Sat Feb 01 18:41:48 2014 +0100 +++ b/src/HOL/Tools/Meson/meson_clausify.ML Sat Feb 01 18:42:46 2014 +0100 @@ -12,7 +12,7 @@ val is_zapped_var_name : string -> bool val is_quasi_lambda_free : term -> bool val introduce_combinators_in_cterm : cterm -> thm - val introduce_combinators_in_theorem : thm -> thm + val introduce_combinators_in_theorem : Proof.context -> thm -> thm val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool val ss_only : thm list -> Proof.context -> Proof.context val cnf_axiom : @@ -163,7 +163,7 @@ (introduce_combinators_in_cterm ct2) end -fun introduce_combinators_in_theorem th = +fun introduce_combinators_in_theorem ctxt th = if is_quasi_lambda_free (prop_of th) then th else @@ -173,7 +173,7 @@ in Thm.equal_elim eqth th end handle THM (msg, _, _) => (warning ("Error in the combinator translation of " ^ - Display.string_of_thm_without_context th ^ + Display.string_of_thm ctxt th ^ "\nException message: " ^ msg ^ "."); (* A type variable of sort "{}" will make "abstraction" fail. *) TrueI) @@ -387,7 +387,7 @@ (opt |> Option.map (I #>> singleton (Variable.export ctxt ctxt0) ##> (term_of #> HOLogic.dest_Trueprop #> singleton (Variable.export_terms ctxt ctxt0))), - cnf_ths |> map (combinators ? introduce_combinators_in_theorem + cnf_ths |> map (combinators ? introduce_combinators_in_theorem ctxt #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I)) |> Variable.export ctxt ctxt0 |> finish_cnf diff -r 4b4627f5912b -r 8d61b0aa7a0d src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Sat Feb 01 18:41:48 2014 +0100 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Sat Feb 01 18:42:46 2014 +0100 @@ -238,7 +238,7 @@ fun neg_clausify ctxt combinators = single #> Meson.make_clauses_unsorted ctxt - #> combinators ? map Meson_Clausify.introduce_combinators_in_theorem + #> combinators ? map (Meson_Clausify.introduce_combinators_in_theorem ctxt) #> Meson.finish_cnf fun preskolem_tac ctxt st0 = diff -r 4b4627f5912b -r 8d61b0aa7a0d src/HOL/Tools/TFL/casesplit.ML --- a/src/HOL/Tools/TFL/casesplit.ML Sat Feb 01 18:41:48 2014 +0100 +++ b/src/HOL/Tools/TFL/casesplit.ML Sat Feb 01 18:42:46 2014 +0100 @@ -128,8 +128,8 @@ (case find_thms_split splitths 1 th of NONE => (writeln (cat_lines - (["th:", Display.string_of_thm_without_context th, "split ths:"] @ - map Display.string_of_thm_without_context splitths @ ["\n--"])); + (["th:", Display.string_of_thm ctxt th, "split ths:"] @ + map (Display.string_of_thm ctxt) splitths @ ["\n--"])); error "splitto: cannot find variable to split on") | SOME v => let diff -r 4b4627f5912b -r 8d61b0aa7a0d src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Sat Feb 01 18:41:48 2014 +0100 +++ b/src/HOL/Tools/TFL/post.ML Sat Feb 01 18:42:46 2014 +0100 @@ -101,14 +101,12 @@ if (solved th) then (th::So, Si, St) else (So, th::Si, St)) nested_tcs ([],[],[]) val simplified' = map (join_assums ctxt) simplified - val dummy = (Prim.trace_thms "solved =" solved; - Prim.trace_thms "simplified' =" simplified') + val dummy = (Prim.trace_thms ctxt "solved =" solved; + Prim.trace_thms ctxt "simplified' =" simplified') val rewr = full_simplify (ctxt addsimps (solved @ simplified')); - val dummy = Prim.trace_thms "Simplifying the induction rule..." - [induction] + val dummy = Prim.trace_thms ctxt "Simplifying the induction rule..." [induction] val induction' = rewr induction - val dummy = Prim.trace_thms "Simplifying the recursion rules..." - [rules] + val dummy = Prim.trace_thms ctxt "Simplifying the recursion rules..." [rules] val rules' = rewr rules val _ = writeln "... Postprocessing finished"; in @@ -142,7 +140,7 @@ Prim.post_definition congs thy ctxt (def, pats) val {lhs=f,rhs} = USyntax.dest_eq (concl def) val (_,[R,_]) = USyntax.strip_comb rhs - val dummy = Prim.trace_thms "congs =" congs + val dummy = Prim.trace_thms ctxt "congs =" congs (*the next step has caused simplifier looping in some cases*) val {induction, rules, tcs} = proof_stage strict ctxt wfs thy diff -r 4b4627f5912b -r 8d61b0aa7a0d src/HOL/Tools/TFL/rules.ML --- a/src/HOL/Tools/TFL/rules.ML Sat Feb 01 18:41:48 2014 +0100 +++ b/src/HOL/Tools/TFL/rules.ML Sat Feb 01 18:42:46 2014 +0100 @@ -535,11 +535,11 @@ fun say s = if !tracing then writeln s else (); -fun print_thms s L = - say (cat_lines (s :: map Display.string_of_thm_without_context L)); +fun print_thms ctxt s L = + say (cat_lines (s :: map (Display.string_of_thm ctxt) L)); -fun print_cterm s ct = - say (cat_lines [s, Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct)]); +fun print_cterm ctxt s ct = + say (cat_lines [s, Syntax.string_of_term ctxt (Thm.term_of ct)]); (*--------------------------------------------------------------------------- @@ -656,20 +656,20 @@ let fun cong_prover ctxt thm = let val dummy = say "cong_prover:" val cntxt = Simplifier.prems_of ctxt - val dummy = print_thms "cntxt:" cntxt + val dummy = print_thms ctxt "cntxt:" cntxt val dummy = say "cong rule:" - val dummy = say (Display.string_of_thm_without_context thm) + val dummy = say (Display.string_of_thm ctxt thm) (* Unquantified eliminate *) fun uq_eliminate (thm,imp,thy) = let val tych = cterm_of thy - val dummy = print_cterm "To eliminate:" (tych imp) + val dummy = print_cterm ctxt "To eliminate:" (tych imp) val ants = map tych (Logic.strip_imp_prems imp) val eq = Logic.strip_imp_concl imp val lhs = tych(get_lhs eq) val ctxt' = Simplifier.add_prems (map ASSUME ants) ctxt val lhs_eq_lhs1 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used) ctxt' lhs handle Utils.ERR _ => Thm.reflexive lhs - val dummy = print_thms "proven:" [lhs_eq_lhs1] + val dummy = print_thms ctxt' "proven:" [lhs_eq_lhs1] val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1 val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq in @@ -738,7 +738,7 @@ fun restrict_prover ctxt thm = let val dummy = say "restrict_prover:" val cntxt = rev (Simplifier.prems_of ctxt) - val dummy = print_thms "cntxt:" cntxt + val dummy = print_thms ctxt "cntxt:" cntxt val thy = Thm.theory_of_thm thm val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm fun genl tm = let val vlist = subtract (op aconv) globals @@ -760,8 +760,8 @@ val antl = case rcontext of [] => [] | _ => [USyntax.list_mk_conj(map cncl rcontext)] val TC = genl(USyntax.list_mk_imp(antl, A)) - val dummy = print_cterm "func:" (cterm_of thy func) - val dummy = print_cterm "TC:" (cterm_of thy (HOLogic.mk_Trueprop TC)) + val dummy = print_cterm ctxt "func:" (cterm_of thy func) + val dummy = print_cterm ctxt "TC:" (cterm_of thy (HOLogic.mk_Trueprop TC)) val dummy = tc_list := (TC :: !tc_list) val nestedp = is_some (USyntax.find_term is_func TC) val dummy = if nestedp then say "nested" else say "not_nested" diff -r 4b4627f5912b -r 8d61b0aa7a0d src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Sat Feb 01 18:41:48 2014 +0100 +++ b/src/HOL/Tools/TFL/tfl.ML Sat Feb 01 18:42:46 2014 +0100 @@ -7,8 +7,8 @@ signature PRIM = sig val trace: bool Unsynchronized.ref - val trace_thms: string -> thm list -> unit - val trace_cterm: string -> cterm -> unit + val trace_thms: Proof.context -> string -> thm list -> unit + val trace_cterm: Proof.context -> string -> cterm -> unit type pattern val mk_functional: theory -> term list -> {functional: term, pats: pattern list} val wfrec_definition0: theory -> string -> term -> term -> theory * thm @@ -901,18 +901,19 @@ (Rules.MP rule tcthm, Rules.PROVE_HYP tcthm induction) -fun trace_thms s L = - if !trace then writeln (cat_lines (s :: map Display.string_of_thm_without_context L)) +fun trace_thms ctxt s L = + if !trace then writeln (cat_lines (s :: map (Display.string_of_thm ctxt) L)) else (); -fun trace_cterm s ct = +fun trace_cterm ctxt s ct = if !trace then - writeln (cat_lines [s, Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct)]) + writeln (cat_lines [s, Syntax.string_of_term ctxt (Thm.term_of ct)]) else (); fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} = -let val tych = Thry.typecheck theory +let val ctxt = Proof_Context.init_global theory; + val tych = Thry.typecheck theory; val prove = Rules.prove strict; (*--------------------------------------------------------------------- @@ -936,9 +937,9 @@ fun simplify_tc tc (r,ind) = let val tc1 = tych tc - val _ = trace_cterm "TC before simplification: " tc1 + val _ = trace_cterm ctxt "TC before simplification: " tc1 val tc_eq = simplifier tc1 - val _ = trace_thms "result: " [tc_eq] + val _ = trace_thms ctxt "result: " [tc_eq] in elim_tc (Rules.MATCH_MP Thms.eqT tc_eq) (r,ind) handle Utils.ERR _ => diff -r 4b4627f5912b -r 8d61b0aa7a0d src/HOL/Tools/numeral.ML --- a/src/HOL/Tools/numeral.ML Sat Feb 01 18:41:48 2014 +0100 +++ b/src/HOL/Tools/numeral.ML Sat Feb 01 18:42:46 2014 +0100 @@ -71,10 +71,10 @@ let fun dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... }) = 0 | dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... }) = 1 - | dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"; + | dest_bit _ = Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal bit"; fun dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = 1 | dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1 - | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term"; + | dest_num _ = Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term"; in if negative then ~ (dest_num t) else dest_num t end; fun pretty literals _ thm _ _ [(t, _)] = (Code_Printer.str o print literals o dest_numeral thm) t; diff -r 4b4627f5912b -r 8d61b0aa7a0d src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Sat Feb 01 18:41:48 2014 +0100 +++ b/src/HOL/Tools/sat_funcs.ML Sat Feb 01 18:42:46 2014 +0100 @@ -117,9 +117,9 @@ (* cterms. *) (* ------------------------------------------------------------------------- *) -fun resolve_raw_clauses [] = +fun resolve_raw_clauses _ [] = raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, []) - | resolve_raw_clauses (c::cs) = + | resolve_raw_clauses ctxt (c::cs) = let (* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *) fun merge xs [] = xs @@ -154,10 +154,10 @@ let val _ = if ! trace_sat then (* FIXME !? *) - tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^ + tracing ("Resolving clause: " ^ Display.string_of_thm ctxt c1 ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c1)) (Thm.hyps_of c1) - ^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^ + ^ ")\nwith clause: " ^ Display.string_of_thm ctxt c2 ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c2)) (Thm.hyps_of c2) ^ ")") else () @@ -178,7 +178,7 @@ val _ = if !trace_sat then - tracing ("Resolution theorem: " ^ Display.string_of_thm_without_context res_thm) + tracing ("Resolution theorem: " ^ Display.string_of_thm ctxt res_thm) else () (* Gamma1, Gamma2 |- False *) @@ -189,7 +189,7 @@ val _ = if !trace_sat then - tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^ + tracing ("Resulting clause: " ^ Display.string_of_thm ctxt c_new ^ " (hyps: " ^ ML_Syntax.print_list (Syntax.string_of_term_global (theory_of_thm c_new)) (Thm.hyps_of c_new) ^ ")") else () @@ -211,7 +211,7 @@ (* occur (as part of a literal) in 'clauses' to positive integers. *) (* ------------------------------------------------------------------------- *) -fun replay_proof atom_table clauses (clause_table, empty_id) = +fun replay_proof ctxt atom_table clauses (clause_table, empty_id) = let fun index_of_literal chyp = (case (HOLogic.dest_Trueprop o Thm.term_of) chyp of @@ -242,7 +242,7 @@ val _ = if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else () val ids = the (Inttab.lookup clause_table id) - val clause = resolve_raw_clauses (map prove_clause ids) + val clause = resolve_raw_clauses ctxt (map prove_clause ids) val _ = Array.update (clauses, id, RAW_CLAUSE clause) val _ = if !trace_sat then @@ -372,7 +372,7 @@ cnf_clauses 0 (* replay the proof to derive the empty clause *) (* [c_1 && ... && c_n] |- False *) - val raw_thm = replay_proof atom_table clause_arr (clause_table, empty_id) + val raw_thm = replay_proof ctxt atom_table clause_arr (clause_table, empty_id) in (* [c_1, ..., c_n] |- False *) Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm diff -r 4b4627f5912b -r 8d61b0aa7a0d src/HOL/Tools/string_code.ML --- a/src/HOL/Tools/string_code.ML Sat Feb 01 18:41:48 2014 +0100 +++ b/src/HOL/Tools/string_code.ML Sat Feb 01 18:42:46 2014 +0100 @@ -62,28 +62,28 @@ [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))])) end; -fun add_literal_char target = +fun add_literal_char target thy = let fun pretty literals _ thm _ _ [(t1, _), (t2, _)] = case decode_char (t1, t2) of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c - | NONE => Code_Printer.eqn_error thm "Illegal character expression"; + | NONE => Code_Printer.eqn_error thy thm "Illegal character expression"; in Code_Target.set_printings (Code_Symbol.Constant (@{const_name Char}, - [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))])) + [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))])) thy end; -fun add_literal_string target = +fun add_literal_string target thy = let fun pretty literals _ thm _ _ [(t, _)] = case List_Code.implode_list t of SOME ts => (case implode_string literals ts of SOME p => p - | NONE => Code_Printer.eqn_error thm "Illegal string literal expression") - | NONE => Code_Printer.eqn_error thm "Illegal string literal expression"; + | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression") + | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression"; in Code_Target.set_printings (Code_Symbol.Constant (@{const_name STR}, - [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))])) + [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))])) thy end; end; diff -r 4b4627f5912b -r 8d61b0aa7a0d src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Sat Feb 01 18:41:48 2014 +0100 +++ b/src/Tools/Code/code_printer.ML Sat Feb 01 18:42:46 2014 +0100 @@ -11,7 +11,7 @@ type const = Code_Thingol.const type dict = Code_Thingol.dict - val eqn_error: thm option -> string -> 'a + val eqn_error: theory -> thm option -> string -> 'a val @@ : 'a * 'a -> 'a list val @| : 'a list * 'a -> 'a list @@ -100,9 +100,9 @@ (** generic nonsense *) -fun eqn_error (SOME thm) s = - error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm) - | eqn_error NONE s = error s; +fun eqn_error thy (SOME thm) s = + error (s ^ ",\nin equation " ^ Display.string_of_thm_global thy thm) + | eqn_error _ NONE s = error s; val code_presentationN = "code_presentation"; val stmt_nameN = "stmt_name";