# HG changeset patch # User Simon Wimmer # Date 1709038002 -3600 # Node ID 2746dfc9ceaea9b32fd36d68b340cb747f947326 # Parent 384d6d48a7d34e0ae8aa5229bec1ca1581dbce90 optional cartouche syntax and proper name printing in atp Isar output diff -r 384d6d48a7d3 -r 2746dfc9ceae src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Wed Mar 06 09:43:25 2024 +0100 +++ b/src/HOL/Tools/ATP/atp_util.ML Tue Feb 27 13:46:42 2024 +0100 @@ -6,6 +6,7 @@ signature ATP_UTIL = sig + val proof_cartouches: bool Config.T val timestamp : unit -> string val hashw : word * word -> word val hashw_string : string * word -> word @@ -18,7 +19,7 @@ val find_enclosed : string -> string -> string -> string list val nat_subscript : int -> string val unquote_tvar : string -> string - val maybe_quote : Keyword.keywords -> string -> string + val maybe_quote : Proof.context -> string -> string val string_of_ext_time : bool * Time.time -> string val string_of_time : Time.time -> string val type_instance : theory -> typ -> typ -> bool @@ -56,6 +57,8 @@ structure ATP_Util : ATP_UTIL = struct +val proof_cartouches = Attrib.setup_config_bool \<^binding>\atp_proof_cartouches\ (K false) + fun forall2 _ [] [] = true | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys | forall2 _ _ _ = false @@ -138,11 +141,15 @@ val unquery_var = perhaps (try (unprefix "?")) val is_long_identifier = forall Symbol_Pos.is_identifier o Long_Name.explode -fun maybe_quote keywords y = - let val s = YXML.content_of y in +fun maybe_quote ctxt y = + let + val s = YXML.content_of y + val is_literal = (Keyword.is_literal o Thy_Header.get_keywords') ctxt + val gen_quote = if Config.get ctxt proof_cartouches then cartouche else quote + in y |> ((not (is_long_identifier (unquote_tvar s)) andalso not (is_long_identifier (unquery_var s))) orelse - Keyword.is_literal keywords s) ? quote + is_literal s) ? gen_quote end fun string_of_ext_time (plus, time) = diff -r 384d6d48a7d3 -r 2746dfc9ceae src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Mar 06 09:43:25 2024 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Feb 27 13:46:42 2024 +0100 @@ -202,7 +202,6 @@ val time_start = Time.now () val thy = Proof.theory_of state val ctxt = Proof.context_of state - val keywords = Thy_Header.get_keywords thy val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths, boxes, finitizes, monos, wfs, sat_solver, falsify, debug, verbose, overlord, spy, user_axioms, assms, whacks, merge_type_vars, @@ -342,7 +341,7 @@ val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns fun monotonicity_message Ts extra = - let val pretties = map (pretty_maybe_quote keywords o pretty_for_type ctxt) Ts in + let val pretties = map (pretty_maybe_quote ctxt o pretty_for_type ctxt) Ts in Pretty.blk (0, Pretty.text ("The type" ^ plural_s_for_list pretties) @ [Pretty.brk 1] @ pretty_serial_commas "and" pretties @ [Pretty.brk 1] @ diff -r 384d6d48a7d3 -r 2746dfc9ceae src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Mar 06 09:43:25 2024 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Feb 27 13:46:42 2024 +0100 @@ -181,8 +181,8 @@ fun standard_blocks s = map (Pretty.block o cons (Pretty.str (s ^ " "))) val (primary_cards, secondary_cards, maxes, iters, miscs) = quintuple_for_scope - (fn ctxt => pretty_maybe_quote (Thy_Header.get_keywords' ctxt) o pretty_for_type ctxt) - (fn ctxt => pretty_maybe_quote (Thy_Header.get_keywords' ctxt) o Syntax.pretty_term ctxt) + (fn ctxt => pretty_maybe_quote ctxt o pretty_for_type ctxt) + (fn ctxt => pretty_maybe_quote ctxt o Syntax.pretty_term ctxt) Pretty.str scope in standard_blocks "card" primary_cards @ diff -r 384d6d48a7d3 -r 2746dfc9ceae src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Mar 06 09:43:25 2024 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Feb 27 13:46:42 2024 +0100 @@ -69,7 +69,7 @@ val eta_expand : typ list -> term -> int -> term val DETERM_TIMEOUT : Time.time -> tactic -> tactic val indent_size : int - val pretty_maybe_quote : Keyword.keywords -> Pretty.T -> Pretty.T + val pretty_maybe_quote : Proof.context -> Pretty.T -> Pretty.T val hash_term : term -> int val spying : bool -> (unit -> Proof.state * int * string) -> unit end; @@ -279,9 +279,9 @@ val maybe_quote = ATP_Util.maybe_quote -fun pretty_maybe_quote keywords pretty = +fun pretty_maybe_quote ctxt pretty = let val s = Pretty.unformatted_string_of pretty - in if maybe_quote keywords s = s then pretty else Pretty.quote pretty end + in if maybe_quote ctxt s = s then pretty else Pretty.quote pretty end val hashw = ATP_Util.hashw val hashw_string = ATP_Util.hashw_string diff -r 384d6d48a7d3 -r 2746dfc9ceae src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Wed Mar 06 09:43:25 2024 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Tue Feb 27 13:46:42 2024 +0100 @@ -373,7 +373,6 @@ fun string_of_isar_proof ctxt0 i n proof = let - val keywords = Thy_Header.get_keywords' ctxt0 (* Make sure only type constraints inserted by the type annotation code are printed. *) val ctxt = ctxt0 @@ -408,7 +407,7 @@ |> annotate_types_in_term ctxt |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of) |> simplify_spaces - |> maybe_quote keywords), + |> maybe_quote ctxt), ctxt |> perhaps (try (Proof_Context.augment term))) fun using_facts [] [] = "" @@ -425,8 +424,8 @@ end fun of_free (s, T) = - maybe_quote keywords s ^ " :: " ^ - maybe_quote keywords (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T)) + Proof_Context.print_name ctxt s ^ " :: " ^ + maybe_quote ctxt (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T)) fun add_frees xs (s, ctxt) = (s ^ space_implode " and " (map of_free xs), ctxt |> fold Proof_Context.augment (map Free xs)) diff -r 384d6d48a7d3 -r 2746dfc9ceae src/HOL/ex/Sketch_and_Explore.thy --- a/src/HOL/ex/Sketch_and_Explore.thy Wed Mar 06 09:43:25 2024 +0100 +++ b/src/HOL/ex/Sketch_and_Explore.thy Tue Feb 27 13:46:42 2024 +0100 @@ -18,7 +18,7 @@ in (fixes, assms, concl) end; fun maybe_quote ctxt = - ATP_Util.maybe_quote (Thy_Header.get_keywords' ctxt); + ATP_Util.maybe_quote ctxt; fun print_typ ctxt T = T