# HG changeset patch
# User blanchet
# Date 1282683442 -7200
# Node ID 0ce517c1970fed7f29f5470ec7c459530ac606cb
# Parent  bdcb237014483c6cef4b3330a6177f037073e193
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts

diff -r bdcb23701448 -r 0ce517c1970f src/HOL/Tools/Sledgehammer/metis_clauses.ML
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Aug 24 21:40:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Aug 24 22:57:22 2010 +0200
@@ -121,7 +121,7 @@
   Alphanumeric characters are left unchanged.
   The character _ goes to __
   Characters in the range ASCII space to / go to _A to _P, respectively.
-  Other printing characters go to _nnn where nnn is the decimal ASCII code.*)
+  Other characters go to _nnn where nnn is the decimal ASCII code.*)
 val A_minus_space = Char.ord #"A" - Char.ord #" ";
 
 fun stringN_of_int 0 _ = ""
@@ -132,9 +132,7 @@
   else if c = #"_" then "__"
   else if #" " <= c andalso c <= #"/"
        then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
-  else if Char.isPrint c
-       then ("_" ^ stringN_of_int 3 (Char.ord c))  (*fixed width, in case more digits follow*)
-  else ""
+  else ("_" ^ stringN_of_int 3 (Char.ord c))  (*fixed width, in case more digits follow*)
 
 val ascii_of = String.translate ascii_of_c;
 
diff -r bdcb23701448 -r 0ce517c1970f src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Aug 24 21:40:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Aug 24 22:57:22 2010 +0200
@@ -174,10 +174,9 @@
   Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
   |-- Scan.repeat parse_clause_formula_pair
 val extract_clause_formula_relation =
-  Substring.full
-  #> Substring.position set_ClauseFormulaRelationN
-  #> snd #> Substring.string #> strip_spaces #> explode
-  #> parse_clause_formula_relation #> fst
+  Substring.full #> Substring.position set_ClauseFormulaRelationN
+  #> snd #> Substring.string #> strip_spaces_except_between_ident_chars
+  #> explode #> parse_clause_formula_relation #> fst
 
 fun repair_conjecture_shape_and_theorem_names output conjecture_shape
                                               axiom_names =
diff -r bdcb23701448 -r 0ce517c1970f src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Aug 24 21:40:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Aug 24 22:57:22 2010 +0200
@@ -540,14 +540,14 @@
     (* Unnamed, not chained formulas with schematic variables are omitted,
        because they are rejected by the backticks (`...`) parser for some
        reason. *)
-    fun is_bad_unnamed_local th =
-      exists (fn (_, ths) => member Thm.eq_thm ths th) named_locals orelse
-      (exists_subterm is_Var (prop_of th) andalso not (is_chained th))
+    fun is_good_unnamed_local th =
+      forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals
+      andalso (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th))
     val unnamed_locals =
-      local_facts |> Facts.props |> filter_out is_bad_unnamed_local
+      local_facts |> Facts.props |> filter is_good_unnamed_local
                   |> map (pair "" o single)
     val full_space =
-      Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts);
+      Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
     fun add_valid_facts foldx facts =
       foldx (fn (name0, ths) =>
         if name0 <> "" andalso
@@ -563,6 +563,8 @@
             fun backquotify th =
               "`" ^ Print_Mode.setmp [Print_Mode.input]
                                  (Syntax.string_of_term ctxt) (prop_of th) ^ "`"
+              |> String.translate (fn c => if Char.isPrint c then str c else "")
+              |> simplify_spaces
             fun check_thms a =
               case try (ProofContext.get_thms ctxt) a of
                 NONE => false
diff -r bdcb23701448 -r 0ce517c1970f src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Aug 24 21:40:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Aug 24 22:57:22 2010 +0200
@@ -234,7 +234,7 @@
   fst o Scan.finite Symbol.stopper
             (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
                             (parse_lines pool)))
-  o explode o strip_spaces
+  o explode o strip_spaces_except_between_ident_chars
 
 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
 
diff -r bdcb23701448 -r 0ce517c1970f src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Aug 24 21:40:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Aug 24 22:57:22 2010 +0200
@@ -9,7 +9,8 @@
   val is_true_for : (string * bool) vector -> string -> bool
   val plural_s : int -> string
   val serial_commas : string -> string list -> string list
-  val strip_spaces : string -> string
+  val simplify_spaces : string -> string
+  val strip_spaces_except_between_ident_chars : string -> string
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time_option : string -> string -> Time.time option
   val scan_integer : string list -> int * string list
@@ -39,24 +40,27 @@
   | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
   | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
 
-fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
-
-fun strip_spaces_in_list [] = ""
-  | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
-  | strip_spaces_in_list [c1, c2] =
-    strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
-  | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
+fun strip_spaces_in_list _ [] = ""
+  | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then "" else str c1
+  | strip_spaces_in_list is_evil [c1, c2] =
+    strip_spaces_in_list is_evil [c1] ^ strip_spaces_in_list is_evil [c2]
+  | strip_spaces_in_list is_evil (c1 :: c2 :: c3 :: cs) =
     if Char.isSpace c1 then
-      strip_spaces_in_list (c2 :: c3 :: cs)
+      strip_spaces_in_list is_evil (c2 :: c3 :: cs)
     else if Char.isSpace c2 then
       if Char.isSpace c3 then
-        strip_spaces_in_list (c1 :: c3 :: cs)
+        strip_spaces_in_list is_evil (c1 :: c3 :: cs)
       else
-        str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
-        strip_spaces_in_list (c3 :: cs)
+        str c1 ^ (if forall is_evil [c1, c3] then " " else "") ^
+        strip_spaces_in_list is_evil (c3 :: cs)
     else
-      str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
-val strip_spaces = strip_spaces_in_list o String.explode
+      str c1 ^ strip_spaces_in_list is_evil (c2 :: c3 :: cs)
+fun strip_spaces is_evil = strip_spaces_in_list is_evil o String.explode
+
+val simplify_spaces = strip_spaces (K true)
+
+fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
+val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char
 
 fun parse_bool_option option name s =
   (case s of