fix types of "fix" variables to help proof reconstruction and aid readability
authorblanchet
Tue Apr 27 16:00:20 2010 +0200 (2010-04-27 ago)
changeset 364781aba777a367f
parent 36477 71cc00ea5768
child 36479 fcbf412c560f
fix types of "fix" variables to help proof reconstruction and aid readability
src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Tue Apr 27 14:55:10 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Tue Apr 27 16:00:20 2010 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list
     1.5    val suppress_endtheory: bool Unsynchronized.ref
     1.6      (*for emergency use where endtheory causes problems*)
     1.7 -  val strip_subgoal : thm -> int -> term list * term list * term
     1.8 +  val strip_subgoal : thm -> int -> (string * typ) list * term list * term
     1.9    val neg_clausify: thm -> thm list
    1.10    val neg_conjecture_clauses:
    1.11      Proof.context -> thm -> int -> thm list list * (string * typ) list
    1.12 @@ -463,7 +463,7 @@
    1.13      val (t, frees) = Logic.goal_params (prop_of goal) i
    1.14      val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees)
    1.15      val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees
    1.16 -  in (rev frees, hyp_ts, concl_t) end
    1.17 +  in (rev (map dest_Free frees), hyp_ts, concl_t) end
    1.18  
    1.19  (*** Converting a subgoal into negated conjecture clauses. ***)
    1.20  
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Apr 27 14:55:10 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Apr 27 16:00:20 2010 +0200
     2.3 @@ -33,6 +33,7 @@
     2.4  structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
     2.5  struct
     2.6  
     2.7 +open Sledgehammer_Util
     2.8  open Sledgehammer_FOL_Clause
     2.9  open Sledgehammer_Fact_Preprocessor
    2.10  
    2.11 @@ -480,7 +481,7 @@
    2.12  datatype qualifier = Show | Then | Moreover | Ultimately
    2.13  
    2.14  datatype step =
    2.15 -  Fix of term list |
    2.16 +  Fix of (string * typ) list |
    2.17    Assume of label * term |
    2.18    Have of qualifier list * label * term * byline
    2.19  and byline =
    2.20 @@ -716,7 +717,7 @@
    2.21    let
    2.22      val used_ls = using_of proof
    2.23      fun do_label l = if member (op =) used_ls l then l else no_label
    2.24 -    fun kill (Fix ts) = Fix ts
    2.25 +    fun kill (Fix xs) = Fix xs
    2.26        | kill (Assume (l, t)) = Assume (do_label l, t)
    2.27        | kill (Have (qs, l, t, by)) =
    2.28          Have (qs, do_label l, t,
    2.29 @@ -765,7 +766,13 @@
    2.30  
    2.31  fun string_for_proof ctxt sorts i n =
    2.32    let
    2.33 +    fun fix_print_mode f =
    2.34 +      PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN)
    2.35 +                      (print_mode_value ())) f
    2.36      fun do_indent ind = replicate_string (ind * indent_size) " "
    2.37 +    fun do_free (s, T) =
    2.38 +      maybe_quote s ^ " :: " ^
    2.39 +      maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
    2.40      fun do_raw_label (s, j) = s ^ string_of_int j
    2.41      fun do_label l = if l = no_label then "" else do_raw_label l ^ ": "
    2.42      fun do_have qs =
    2.43 @@ -775,29 +782,25 @@
    2.44           if member (op =) qs Show then "thus" else "hence"
    2.45         else
    2.46           if member (op =) qs Show then "show" else "have")
    2.47 -    val do_term =
    2.48 -      quote o PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN)
    2.49 -                                      (print_mode_value ()))
    2.50 -                              (Syntax.string_of_term ctxt)
    2.51 +    val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
    2.52      fun do_using [] = ""
    2.53        | do_using ls = "using " ^ (space_implode " " (map do_raw_label ls)) ^ " "
    2.54      fun do_by_facts [] [] = "by blast"
    2.55        | do_by_facts _ [] = "by metis"
    2.56        | do_by_facts _ ss = "by (metis " ^ space_implode " " ss ^ ")"
    2.57 -    fun do_facts ind (ls, ss) =
    2.58 -      do_indent (ind + 1) ^ do_using ls ^ do_by_facts ls ss
    2.59 -    and do_step ind (Fix ts) =
    2.60 -        do_indent ind ^ "fix " ^ space_implode " and " (map do_term ts) ^ "\n"
    2.61 +    fun do_facts (ls, ss) = do_using ls ^ do_by_facts ls ss
    2.62 +    and do_step ind (Fix xs) =
    2.63 +        do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
    2.64        | do_step ind (Assume (l, t)) =
    2.65          do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
    2.66        | do_step ind (Have (qs, l, t, Facts facts)) =
    2.67          do_indent ind ^ do_have qs ^ " " ^
    2.68 -        do_label l ^ do_term t ^ "\n" ^ do_facts ind facts ^ "\n"
    2.69 +        do_label l ^ do_term t ^ do_facts facts ^ "\n"
    2.70        | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
    2.71          space_implode (do_indent ind ^ "moreover\n")
    2.72                        (map (do_block ind) proofs) ^
    2.73 -        do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ "\n" ^
    2.74 -        do_facts ind facts ^ "\n"
    2.75 +        do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^
    2.76 +        do_facts facts ^ "\n"
    2.77      and do_steps prefix suffix ind steps =
    2.78        let val s = implode (map (do_step ind) steps) in
    2.79          replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Apr 27 14:55:10 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Apr 27 16:00:20 2010 +0200
     3.3 @@ -14,6 +14,8 @@
     3.4    val timestamp : unit -> string
     3.5    val parse_bool_option : bool -> string -> string -> bool option
     3.6    val parse_time_option : string -> string -> Time.time option
     3.7 +  val unyxml : string -> string
     3.8 +  val maybe_quote : string -> string
     3.9  end;
    3.10   
    3.11  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    3.12 @@ -72,4 +74,16 @@
    3.13          SOME (Time.fromMilliseconds msecs)
    3.14      end
    3.15  
    3.16 +fun plain_string_from_xml_tree t =
    3.17 +  Buffer.empty |> XML.add_content t |> Buffer.content
    3.18 +val unyxml = plain_string_from_xml_tree o YXML.parse
    3.19 +
    3.20 +val is_long_identifier = forall Syntax.is_identifier o space_explode "."
    3.21 +fun maybe_quote y =
    3.22 +  let val s = unyxml y in
    3.23 +    y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
    3.24 +           not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
    3.25 +           OuterKeyword.is_keyword s) ? quote
    3.26 +  end
    3.27 +
    3.28  end;