# HG changeset patch # User blanchet # Date 1272376820 -7200 # Node ID 1aba777a367f6eb08c92721b7900fc3b4cac39fb # Parent 71cc00ea576868d78a91bd15c2a9c45b73d13515 fix types of "fix" variables to help proof reconstruction and aid readability diff -r 71cc00ea5768 -r 1aba777a367f src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Tue Apr 27 14:55:10 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Tue Apr 27 16:00:20 2010 +0200 @@ -17,7 +17,7 @@ val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list val suppress_endtheory: bool Unsynchronized.ref (*for emergency use where endtheory causes problems*) - val strip_subgoal : thm -> int -> term list * term list * term + val strip_subgoal : thm -> int -> (string * typ) list * term list * term val neg_clausify: thm -> thm list val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list list * (string * typ) list @@ -463,7 +463,7 @@ val (t, frees) = Logic.goal_params (prop_of goal) i val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees) val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees - in (rev frees, hyp_ts, concl_t) end + in (rev (map dest_Free frees), hyp_ts, concl_t) end (*** Converting a subgoal into negated conjecture clauses. ***) diff -r 71cc00ea5768 -r 1aba777a367f src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Apr 27 14:55:10 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Apr 27 16:00:20 2010 +0200 @@ -33,6 +33,7 @@ structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = struct +open Sledgehammer_Util open Sledgehammer_FOL_Clause open Sledgehammer_Fact_Preprocessor @@ -480,7 +481,7 @@ datatype qualifier = Show | Then | Moreover | Ultimately datatype step = - Fix of term list | + Fix of (string * typ) list | Assume of label * term | Have of qualifier list * label * term * byline and byline = @@ -716,7 +717,7 @@ let val used_ls = using_of proof fun do_label l = if member (op =) used_ls l then l else no_label - fun kill (Fix ts) = Fix ts + fun kill (Fix xs) = Fix xs | kill (Assume (l, t)) = Assume (do_label l, t) | kill (Have (qs, l, t, by)) = Have (qs, do_label l, t, @@ -765,7 +766,13 @@ fun string_for_proof ctxt sorts i n = let + fun fix_print_mode f = + PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN) + (print_mode_value ())) f fun do_indent ind = replicate_string (ind * indent_size) " " + fun do_free (s, T) = + maybe_quote s ^ " :: " ^ + maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T) fun do_raw_label (s, j) = s ^ string_of_int j fun do_label l = if l = no_label then "" else do_raw_label l ^ ": " fun do_have qs = @@ -775,29 +782,25 @@ if member (op =) qs Show then "thus" else "hence" else if member (op =) qs Show then "show" else "have") - val do_term = - quote o PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN) - (print_mode_value ())) - (Syntax.string_of_term ctxt) + val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) fun do_using [] = "" | do_using ls = "using " ^ (space_implode " " (map do_raw_label ls)) ^ " " fun do_by_facts [] [] = "by blast" | do_by_facts _ [] = "by metis" | do_by_facts _ ss = "by (metis " ^ space_implode " " ss ^ ")" - fun do_facts ind (ls, ss) = - do_indent (ind + 1) ^ do_using ls ^ do_by_facts ls ss - and do_step ind (Fix ts) = - do_indent ind ^ "fix " ^ space_implode " and " (map do_term ts) ^ "\n" + fun do_facts (ls, ss) = do_using ls ^ do_by_facts ls ss + and do_step ind (Fix xs) = + do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" | do_step ind (Assume (l, t)) = do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n" | do_step ind (Have (qs, l, t, Facts facts)) = do_indent ind ^ do_have qs ^ " " ^ - do_label l ^ do_term t ^ "\n" ^ do_facts ind facts ^ "\n" + do_label l ^ do_term t ^ do_facts facts ^ "\n" | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) = space_implode (do_indent ind ^ "moreover\n") (map (do_block ind) proofs) ^ - do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ "\n" ^ - do_facts ind facts ^ "\n" + do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ + do_facts facts ^ "\n" and do_steps prefix suffix ind steps = let val s = implode (map (do_step ind) steps) in replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ diff -r 71cc00ea5768 -r 1aba777a367f src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Apr 27 14:55:10 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Apr 27 16:00:20 2010 +0200 @@ -14,6 +14,8 @@ val timestamp : unit -> string val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option + val unyxml : string -> string + val maybe_quote : string -> string end; structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = @@ -72,4 +74,16 @@ SOME (Time.fromMilliseconds msecs) end +fun plain_string_from_xml_tree t = + Buffer.empty |> XML.add_content t |> Buffer.content +val unyxml = plain_string_from_xml_tree o YXML.parse + +val is_long_identifier = forall Syntax.is_identifier o space_explode "." +fun maybe_quote y = + let val s = unyxml y in + y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso + not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse + OuterKeyword.is_keyword s) ? quote + end + end;