proper context for printing;
authorwenzelm
Sat Feb 01 18:42:46 2014 +0100 (2014-02-01)
changeset 552368d61b0aa7a0d
parent 55235 4b4627f5912b
child 55237 1e341728bae9
proper context for printing;
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/TFL/casesplit.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/numeral.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/Tools/string_code.ML
src/Tools/Code/code_printer.ML
     1.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Sat Feb 01 18:41:48 2014 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Sat Feb 01 18:42:46 2014 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4    val is_zapped_var_name : string -> bool
     1.5    val is_quasi_lambda_free : term -> bool
     1.6    val introduce_combinators_in_cterm : cterm -> thm
     1.7 -  val introduce_combinators_in_theorem : thm -> thm
     1.8 +  val introduce_combinators_in_theorem : Proof.context -> thm -> thm
     1.9    val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
    1.10    val ss_only : thm list -> Proof.context -> Proof.context
    1.11    val cnf_axiom :
    1.12 @@ -163,7 +163,7 @@
    1.13                          (introduce_combinators_in_cterm ct2)
    1.14      end
    1.15  
    1.16 -fun introduce_combinators_in_theorem th =
    1.17 +fun introduce_combinators_in_theorem ctxt th =
    1.18    if is_quasi_lambda_free (prop_of th) then
    1.19      th
    1.20    else
    1.21 @@ -173,7 +173,7 @@
    1.22      in Thm.equal_elim eqth th end
    1.23      handle THM (msg, _, _) =>
    1.24             (warning ("Error in the combinator translation of " ^
    1.25 -                     Display.string_of_thm_without_context th ^
    1.26 +                     Display.string_of_thm ctxt th ^
    1.27                       "\nException message: " ^ msg ^ ".");
    1.28              (* A type variable of sort "{}" will make "abstraction" fail. *)
    1.29              TrueI)
    1.30 @@ -387,7 +387,7 @@
    1.31      (opt |> Option.map (I #>> singleton (Variable.export ctxt ctxt0)
    1.32                          ##> (term_of #> HOLogic.dest_Trueprop
    1.33                               #> singleton (Variable.export_terms ctxt ctxt0))),
    1.34 -     cnf_ths |> map (combinators ? introduce_combinators_in_theorem
    1.35 +     cnf_ths |> map (combinators ? introduce_combinators_in_theorem ctxt
    1.36                       #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
    1.37               |> Variable.export ctxt ctxt0
    1.38               |> finish_cnf
     2.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Sat Feb 01 18:41:48 2014 +0100
     2.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Sat Feb 01 18:42:46 2014 +0100
     2.3 @@ -238,7 +238,7 @@
     2.4  fun neg_clausify ctxt combinators =
     2.5    single
     2.6    #> Meson.make_clauses_unsorted ctxt
     2.7 -  #> combinators ? map Meson_Clausify.introduce_combinators_in_theorem
     2.8 +  #> combinators ? map (Meson_Clausify.introduce_combinators_in_theorem ctxt)
     2.9    #> Meson.finish_cnf
    2.10  
    2.11  fun preskolem_tac ctxt st0 =
     3.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Sat Feb 01 18:41:48 2014 +0100
     3.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Sat Feb 01 18:42:46 2014 +0100
     3.3 @@ -128,8 +128,8 @@
     3.4          (case find_thms_split splitths 1 th of
     3.5            NONE =>
     3.6             (writeln (cat_lines
     3.7 -            (["th:", Display.string_of_thm_without_context th, "split ths:"] @
     3.8 -              map Display.string_of_thm_without_context splitths @ ["\n--"]));
     3.9 +            (["th:", Display.string_of_thm ctxt th, "split ths:"] @
    3.10 +              map (Display.string_of_thm ctxt) splitths @ ["\n--"]));
    3.11              error "splitto: cannot find variable to split on")
    3.12          | SOME v =>
    3.13              let
     4.1 --- a/src/HOL/Tools/TFL/post.ML	Sat Feb 01 18:41:48 2014 +0100
     4.2 +++ b/src/HOL/Tools/TFL/post.ML	Sat Feb 01 18:42:46 2014 +0100
     4.3 @@ -101,14 +101,12 @@
     4.4                       if (solved th) then (th::So, Si, St)
     4.5                       else (So, th::Si, St)) nested_tcs ([],[],[])
     4.6                val simplified' = map (join_assums ctxt) simplified
     4.7 -              val dummy = (Prim.trace_thms "solved =" solved;
     4.8 -                           Prim.trace_thms "simplified' =" simplified')
     4.9 +              val dummy = (Prim.trace_thms ctxt "solved =" solved;
    4.10 +                           Prim.trace_thms ctxt "simplified' =" simplified')
    4.11                val rewr = full_simplify (ctxt addsimps (solved @ simplified'));
    4.12 -              val dummy = Prim.trace_thms "Simplifying the induction rule..."
    4.13 -                                          [induction]
    4.14 +              val dummy = Prim.trace_thms ctxt "Simplifying the induction rule..." [induction]
    4.15                val induction' = rewr induction
    4.16 -              val dummy = Prim.trace_thms "Simplifying the recursion rules..."
    4.17 -                                          [rules]
    4.18 +              val dummy = Prim.trace_thms ctxt "Simplifying the recursion rules..." [rules]
    4.19                val rules'     = rewr rules
    4.20                val _ = writeln "... Postprocessing finished";
    4.21            in
    4.22 @@ -142,7 +140,7 @@
    4.23             Prim.post_definition congs thy ctxt (def, pats)
    4.24         val {lhs=f,rhs} = USyntax.dest_eq (concl def)
    4.25         val (_,[R,_]) = USyntax.strip_comb rhs
    4.26 -       val dummy = Prim.trace_thms "congs =" congs
    4.27 +       val dummy = Prim.trace_thms ctxt "congs =" congs
    4.28         (*the next step has caused simplifier looping in some cases*)
    4.29         val {induction, rules, tcs} =
    4.30               proof_stage strict ctxt wfs thy
     5.1 --- a/src/HOL/Tools/TFL/rules.ML	Sat Feb 01 18:41:48 2014 +0100
     5.2 +++ b/src/HOL/Tools/TFL/rules.ML	Sat Feb 01 18:42:46 2014 +0100
     5.3 @@ -535,11 +535,11 @@
     5.4  
     5.5  fun say s = if !tracing then writeln s else ();
     5.6  
     5.7 -fun print_thms s L =
     5.8 -  say (cat_lines (s :: map Display.string_of_thm_without_context L));
     5.9 +fun print_thms ctxt s L =
    5.10 +  say (cat_lines (s :: map (Display.string_of_thm ctxt) L));
    5.11  
    5.12 -fun print_cterm s ct =
    5.13 -  say (cat_lines [s, Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct)]);
    5.14 +fun print_cterm ctxt s ct =
    5.15 +  say (cat_lines [s, Syntax.string_of_term ctxt (Thm.term_of ct)]);
    5.16  
    5.17  
    5.18  (*---------------------------------------------------------------------------
    5.19 @@ -656,20 +656,20 @@
    5.20       let fun cong_prover ctxt thm =
    5.21           let val dummy = say "cong_prover:"
    5.22               val cntxt = Simplifier.prems_of ctxt
    5.23 -             val dummy = print_thms "cntxt:" cntxt
    5.24 +             val dummy = print_thms ctxt "cntxt:" cntxt
    5.25               val dummy = say "cong rule:"
    5.26 -             val dummy = say (Display.string_of_thm_without_context thm)
    5.27 +             val dummy = say (Display.string_of_thm ctxt thm)
    5.28               (* Unquantified eliminate *)
    5.29               fun uq_eliminate (thm,imp,thy) =
    5.30                   let val tych = cterm_of thy
    5.31 -                     val dummy = print_cterm "To eliminate:" (tych imp)
    5.32 +                     val dummy = print_cterm ctxt "To eliminate:" (tych imp)
    5.33                       val ants = map tych (Logic.strip_imp_prems imp)
    5.34                       val eq = Logic.strip_imp_concl imp
    5.35                       val lhs = tych(get_lhs eq)
    5.36                       val ctxt' = Simplifier.add_prems (map ASSUME ants) ctxt
    5.37                       val lhs_eq_lhs1 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used) ctxt' lhs
    5.38                         handle Utils.ERR _ => Thm.reflexive lhs
    5.39 -                     val dummy = print_thms "proven:" [lhs_eq_lhs1]
    5.40 +                     val dummy = print_thms ctxt' "proven:" [lhs_eq_lhs1]
    5.41                       val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
    5.42                       val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
    5.43                    in
    5.44 @@ -738,7 +738,7 @@
    5.45          fun restrict_prover ctxt thm =
    5.46            let val dummy = say "restrict_prover:"
    5.47                val cntxt = rev (Simplifier.prems_of ctxt)
    5.48 -              val dummy = print_thms "cntxt:" cntxt
    5.49 +              val dummy = print_thms ctxt "cntxt:" cntxt
    5.50                val thy = Thm.theory_of_thm thm
    5.51                val Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ _ = Thm.prop_of thm
    5.52                fun genl tm = let val vlist = subtract (op aconv) globals
    5.53 @@ -760,8 +760,8 @@
    5.54                val antl = case rcontext of [] => []
    5.55                           | _   => [USyntax.list_mk_conj(map cncl rcontext)]
    5.56                val TC = genl(USyntax.list_mk_imp(antl, A))
    5.57 -              val dummy = print_cterm "func:" (cterm_of thy func)
    5.58 -              val dummy = print_cterm "TC:" (cterm_of thy (HOLogic.mk_Trueprop TC))
    5.59 +              val dummy = print_cterm ctxt "func:" (cterm_of thy func)
    5.60 +              val dummy = print_cterm ctxt "TC:" (cterm_of thy (HOLogic.mk_Trueprop TC))
    5.61                val dummy = tc_list := (TC :: !tc_list)
    5.62                val nestedp = is_some (USyntax.find_term is_func TC)
    5.63                val dummy = if nestedp then say "nested" else say "not_nested"
     6.1 --- a/src/HOL/Tools/TFL/tfl.ML	Sat Feb 01 18:41:48 2014 +0100
     6.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Sat Feb 01 18:42:46 2014 +0100
     6.3 @@ -7,8 +7,8 @@
     6.4  signature PRIM =
     6.5  sig
     6.6    val trace: bool Unsynchronized.ref
     6.7 -  val trace_thms: string -> thm list -> unit
     6.8 -  val trace_cterm: string -> cterm -> unit
     6.9 +  val trace_thms: Proof.context -> string -> thm list -> unit
    6.10 +  val trace_cterm: Proof.context -> string -> cterm -> unit
    6.11    type pattern
    6.12    val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
    6.13    val wfrec_definition0: theory -> string -> term -> term -> theory * thm
    6.14 @@ -901,18 +901,19 @@
    6.15     (Rules.MP rule tcthm, Rules.PROVE_HYP tcthm induction)
    6.16  
    6.17  
    6.18 -fun trace_thms s L =
    6.19 -  if !trace then writeln (cat_lines (s :: map Display.string_of_thm_without_context L))
    6.20 +fun trace_thms ctxt s L =
    6.21 +  if !trace then writeln (cat_lines (s :: map (Display.string_of_thm ctxt) L))
    6.22    else ();
    6.23  
    6.24 -fun trace_cterm s ct =
    6.25 +fun trace_cterm ctxt s ct =
    6.26    if !trace then
    6.27 -    writeln (cat_lines [s, Syntax.string_of_term_global (Thm.theory_of_cterm ct) (Thm.term_of ct)])
    6.28 +    writeln (cat_lines [s, Syntax.string_of_term ctxt (Thm.term_of ct)])
    6.29    else ();
    6.30  
    6.31  
    6.32  fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
    6.33 -let val tych = Thry.typecheck theory
    6.34 +let val ctxt = Proof_Context.init_global theory;
    6.35 +    val tych = Thry.typecheck theory;
    6.36      val prove = Rules.prove strict;
    6.37  
    6.38     (*---------------------------------------------------------------------
    6.39 @@ -936,9 +937,9 @@
    6.40  
    6.41     fun simplify_tc tc (r,ind) =
    6.42         let val tc1 = tych tc
    6.43 -           val _ = trace_cterm "TC before simplification: " tc1
    6.44 +           val _ = trace_cterm ctxt "TC before simplification: " tc1
    6.45             val tc_eq = simplifier tc1
    6.46 -           val _ = trace_thms "result: " [tc_eq]
    6.47 +           val _ = trace_thms ctxt "result: " [tc_eq]
    6.48         in
    6.49         elim_tc (Rules.MATCH_MP Thms.eqT tc_eq) (r,ind)
    6.50         handle Utils.ERR _ =>
     7.1 --- a/src/HOL/Tools/numeral.ML	Sat Feb 01 18:41:48 2014 +0100
     7.2 +++ b/src/HOL/Tools/numeral.ML	Sat Feb 01 18:42:46 2014 +0100
     7.3 @@ -71,10 +71,10 @@
     7.4        let
     7.5          fun dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... }) = 0
     7.6            | dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... }) = 1
     7.7 -          | dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
     7.8 +          | dest_bit _ = Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal bit";
     7.9          fun dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = 1
    7.10            | dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
    7.11 -          | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
    7.12 +          | dest_num _ = Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term";
    7.13        in if negative then ~ (dest_num t) else dest_num t end;
    7.14      fun pretty literals _ thm _ _ [(t, _)] =
    7.15        (Code_Printer.str o print literals o dest_numeral thm) t;
     8.1 --- a/src/HOL/Tools/sat_funcs.ML	Sat Feb 01 18:41:48 2014 +0100
     8.2 +++ b/src/HOL/Tools/sat_funcs.ML	Sat Feb 01 18:42:46 2014 +0100
     8.3 @@ -117,9 +117,9 @@
     8.4  (*      cterms.                                                              *)
     8.5  (* ------------------------------------------------------------------------- *)
     8.6  
     8.7 -fun resolve_raw_clauses [] =
     8.8 +fun resolve_raw_clauses _ [] =
     8.9        raise THM ("Proof reconstruction failed (empty list of resolvents)!", 0, [])
    8.10 -  | resolve_raw_clauses (c::cs) =
    8.11 +  | resolve_raw_clauses ctxt (c::cs) =
    8.12        let
    8.13          (* merges two sorted lists wrt. 'lit_ord', suppressing duplicates *)
    8.14          fun merge xs [] = xs
    8.15 @@ -154,10 +154,10 @@
    8.16            let
    8.17              val _ =
    8.18                if ! trace_sat then  (* FIXME !? *)
    8.19 -                tracing ("Resolving clause: " ^ Display.string_of_thm_without_context c1 ^
    8.20 +                tracing ("Resolving clause: " ^ Display.string_of_thm ctxt c1 ^
    8.21                    " (hyps: " ^ ML_Syntax.print_list
    8.22                      (Syntax.string_of_term_global (theory_of_thm c1)) (Thm.hyps_of c1)
    8.23 -                  ^ ")\nwith clause: " ^ Display.string_of_thm_without_context c2 ^
    8.24 +                  ^ ")\nwith clause: " ^ Display.string_of_thm ctxt c2 ^
    8.25                    " (hyps: " ^ ML_Syntax.print_list
    8.26                      (Syntax.string_of_term_global (theory_of_thm c2)) (Thm.hyps_of c2) ^ ")")
    8.27                else ()
    8.28 @@ -178,7 +178,7 @@
    8.29  
    8.30              val _ =
    8.31                if !trace_sat then
    8.32 -                tracing ("Resolution theorem: " ^ Display.string_of_thm_without_context res_thm)
    8.33 +                tracing ("Resolution theorem: " ^ Display.string_of_thm ctxt res_thm)
    8.34                else ()
    8.35  
    8.36              (* Gamma1, Gamma2 |- False *)
    8.37 @@ -189,7 +189,7 @@
    8.38  
    8.39              val _ =
    8.40                if !trace_sat then
    8.41 -                tracing ("Resulting clause: " ^ Display.string_of_thm_without_context c_new ^
    8.42 +                tracing ("Resulting clause: " ^ Display.string_of_thm ctxt c_new ^
    8.43                    " (hyps: " ^ ML_Syntax.print_list
    8.44                        (Syntax.string_of_term_global (theory_of_thm c_new)) (Thm.hyps_of c_new) ^ ")")
    8.45                else ()
    8.46 @@ -211,7 +211,7 @@
    8.47  (*      occur (as part of a literal) in 'clauses' to positive integers.      *)
    8.48  (* ------------------------------------------------------------------------- *)
    8.49  
    8.50 -fun replay_proof atom_table clauses (clause_table, empty_id) =
    8.51 +fun replay_proof ctxt atom_table clauses (clause_table, empty_id) =
    8.52    let
    8.53      fun index_of_literal chyp =
    8.54        (case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
    8.55 @@ -242,7 +242,7 @@
    8.56              val _ =
    8.57                if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else ()
    8.58              val ids = the (Inttab.lookup clause_table id)
    8.59 -            val clause = resolve_raw_clauses (map prove_clause ids)
    8.60 +            val clause = resolve_raw_clauses ctxt (map prove_clause ids)
    8.61              val _ = Array.update (clauses, id, RAW_CLAUSE clause)
    8.62              val _ =
    8.63                if !trace_sat then
    8.64 @@ -372,7 +372,7 @@
    8.65                  cnf_clauses 0
    8.66              (* replay the proof to derive the empty clause *)
    8.67              (* [c_1 && ... && c_n] |- False *)
    8.68 -            val raw_thm = replay_proof atom_table clause_arr (clause_table, empty_id)
    8.69 +            val raw_thm = replay_proof ctxt atom_table clause_arr (clause_table, empty_id)
    8.70            in
    8.71              (* [c_1, ..., c_n] |- False *)
    8.72              Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
     9.1 --- a/src/HOL/Tools/string_code.ML	Sat Feb 01 18:41:48 2014 +0100
     9.2 +++ b/src/HOL/Tools/string_code.ML	Sat Feb 01 18:42:46 2014 +0100
     9.3 @@ -62,28 +62,28 @@
     9.4        [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))]))
     9.5    end;
     9.6  
     9.7 -fun add_literal_char target =
     9.8 +fun add_literal_char target thy =
     9.9    let
    9.10      fun pretty literals _ thm _ _ [(t1, _), (t2, _)] =
    9.11        case decode_char (t1, t2)
    9.12         of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
    9.13 -        | NONE => Code_Printer.eqn_error thm "Illegal character expression";
    9.14 +        | NONE => Code_Printer.eqn_error thy thm "Illegal character expression";
    9.15    in
    9.16      Code_Target.set_printings (Code_Symbol.Constant (@{const_name Char},
    9.17 -      [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))]))
    9.18 +      [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))])) thy
    9.19    end;
    9.20  
    9.21 -fun add_literal_string target =
    9.22 +fun add_literal_string target thy =
    9.23    let
    9.24      fun pretty literals _ thm _ _ [(t, _)] =
    9.25        case List_Code.implode_list t
    9.26         of SOME ts => (case implode_string literals ts
    9.27               of SOME p => p
    9.28 -              | NONE => Code_Printer.eqn_error thm "Illegal string literal expression")
    9.29 -        | NONE => Code_Printer.eqn_error thm "Illegal string literal expression";
    9.30 +              | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression")
    9.31 +        | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression";
    9.32    in
    9.33      Code_Target.set_printings (Code_Symbol.Constant (@{const_name STR},
    9.34 -      [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
    9.35 +      [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))])) thy
    9.36    end;
    9.37  
    9.38  end;
    10.1 --- a/src/Tools/Code/code_printer.ML	Sat Feb 01 18:41:48 2014 +0100
    10.2 +++ b/src/Tools/Code/code_printer.ML	Sat Feb 01 18:42:46 2014 +0100
    10.3 @@ -11,7 +11,7 @@
    10.4    type const = Code_Thingol.const
    10.5    type dict = Code_Thingol.dict
    10.6  
    10.7 -  val eqn_error: thm option -> string -> 'a
    10.8 +  val eqn_error: theory -> thm option -> string -> 'a
    10.9  
   10.10    val @@ : 'a * 'a -> 'a list
   10.11    val @| : 'a list * 'a -> 'a list
   10.12 @@ -100,9 +100,9 @@
   10.13  
   10.14  (** generic nonsense *)
   10.15  
   10.16 -fun eqn_error (SOME thm) s =
   10.17 -      error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm)
   10.18 -  | eqn_error NONE s = error s;
   10.19 +fun eqn_error thy (SOME thm) s =
   10.20 +      error (s ^ ",\nin equation " ^ Display.string_of_thm_global thy thm)
   10.21 +  | eqn_error _ NONE s = error s;
   10.22  
   10.23  val code_presentationN = "code_presentation";
   10.24  val stmt_nameN = "stmt_name";