centralized term printing code
authorblanchet
Mon Nov 12 11:52:37 2012 +0100 (2012-11-12 ago)
changeset 50048fb024bbf4b65
parent 50047 45684acf0b94
child 50049 dd6a4655cd72
centralized term printing code
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Nov 12 11:32:22 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Nov 12 11:52:37 2012 +0100
     1.3 @@ -231,12 +231,8 @@
     1.4      exists_low_level_class_const t orelse is_that_fact th
     1.5    end
     1.6  
     1.7 -fun hackish_string_for_term ctxt t =
     1.8 -  Print_Mode.setmp
     1.9 -    (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ()))
    1.10 -    (Syntax.string_of_term ctxt) t
    1.11 -  |> String.translate (fn c => if Char.isPrint c then str c else "")
    1.12 -  |> simplify_spaces
    1.13 +fun hackish_string_for_term ctxt =
    1.14 +  with_vanilla_print_mode (Syntax.string_of_term ctxt) #> repair_printed_term
    1.15  
    1.16  (* This is a terrible hack. Free variables are sometimes coded as "M__" when
    1.17     they are displayed as "M" and we want to avoid clashes with these. But
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Nov 12 11:32:22 2012 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Nov 12 11:52:37 2012 +0100
     2.3 @@ -625,13 +625,11 @@
     2.4  
     2.5  fun string_for_proof ctxt type_enc lam_trans i n =
     2.6    let
     2.7 -    fun fix_print_mode f x =
     2.8 -      Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
     2.9 -                               (print_mode_value ())) f x
    2.10      fun do_indent ind = replicate_string (ind * indent_size) " "
    2.11      fun do_free (s, T) =
    2.12        maybe_quote s ^ " :: " ^
    2.13 -      maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
    2.14 +      maybe_quote (repair_printed_term (with_vanilla_print_mode
    2.15 +        (Syntax.string_of_typ ctxt) T))
    2.16      fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
    2.17      fun do_have qs =
    2.18        (if member (op =) qs Moreover then "moreover " else "") ^
    2.19 @@ -641,8 +639,10 @@
    2.20         else
    2.21           if member (op =) qs Show then "show" else "have")
    2.22      val do_term =
    2.23 -      maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
    2.24 -      o annotate_types ctxt
    2.25 +      annotate_types ctxt
    2.26 +      #> with_vanilla_print_mode (Syntax.string_of_term ctxt)
    2.27 +      #> repair_printed_term
    2.28 +      #> maybe_quote
    2.29      val reconstr = Metis (type_enc, lam_trans)
    2.30      fun do_facts ind (ls, ss) =
    2.31        "\n" ^ do_indent (ind + 1) ^
    2.32 @@ -780,7 +780,7 @@
    2.33  
    2.34      (* proof references *)
    2.35      fun refs (Prove (_, _, _, By_Metis (refs, _))) =
    2.36 -      map (the o Label_Table.lookup label_index_table) refs
    2.37 +        map (the o Label_Table.lookup label_index_table) refs
    2.38        | refs _ = []
    2.39      val refed_by_vect =
    2.40        Vector.tabulate (n, (fn _ => []))
    2.41 @@ -791,7 +791,6 @@
    2.42         algorithm) *)
    2.43      fun cost (Prove (_, _ , t, _)) = Term.size_of_term t
    2.44        | cost _ = 0
    2.45 -    val cand_ord =  rev_order o prod_ord int_ord int_ord
    2.46      val cand_tab =
    2.47        v_fold_index
    2.48          (fn (i, [_]) => cons (get i proof_vect |> the |> cost, i)
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Nov 12 11:32:22 2012 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Nov 12 11:52:37 2012 +0100
     3.3 @@ -18,6 +18,8 @@
     3.4    val subgoal_count : Proof.state -> int
     3.5    val reserved_isar_keyword_table : unit -> unit Symtab.table
     3.6    val thms_in_proof : unit Symtab.table option -> thm -> string list
     3.7 +  val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
     3.8 +  val repair_printed_term : string -> string
     3.9  end;
    3.10  
    3.11  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    3.12 @@ -101,4 +103,12 @@
    3.13        [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]
    3.14    in names end
    3.15  
    3.16 +fun with_vanilla_print_mode f x =
    3.17 +  Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
    3.18 +                           (print_mode_value ())) f x
    3.19 +
    3.20 +val repair_printed_term =
    3.21 +  String.translate (fn c => if Char.isPrint c then str c else "")
    3.22 +  #> simplify_spaces
    3.23 +
    3.24  end;