make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
authorblanchet
Tue Aug 24 22:57:22 2010 +0200 (2010-08-24)
changeset 387380ce517c1970f
parent 38737 bdcb23701448
child 38739 8b8ed80b5699
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
src/HOL/Tools/Sledgehammer/metis_clauses.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Aug 24 21:40:03 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Aug 24 22:57:22 2010 +0200
     1.3 @@ -121,7 +121,7 @@
     1.4    Alphanumeric characters are left unchanged.
     1.5    The character _ goes to __
     1.6    Characters in the range ASCII space to / go to _A to _P, respectively.
     1.7 -  Other printing characters go to _nnn where nnn is the decimal ASCII code.*)
     1.8 +  Other characters go to _nnn where nnn is the decimal ASCII code.*)
     1.9  val A_minus_space = Char.ord #"A" - Char.ord #" ";
    1.10  
    1.11  fun stringN_of_int 0 _ = ""
    1.12 @@ -132,9 +132,7 @@
    1.13    else if c = #"_" then "__"
    1.14    else if #" " <= c andalso c <= #"/"
    1.15         then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
    1.16 -  else if Char.isPrint c
    1.17 -       then ("_" ^ stringN_of_int 3 (Char.ord c))  (*fixed width, in case more digits follow*)
    1.18 -  else ""
    1.19 +  else ("_" ^ stringN_of_int 3 (Char.ord c))  (*fixed width, in case more digits follow*)
    1.20  
    1.21  val ascii_of = String.translate ascii_of_c;
    1.22  
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Aug 24 21:40:03 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Aug 24 22:57:22 2010 +0200
     2.3 @@ -174,10 +174,9 @@
     2.4    Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
     2.5    |-- Scan.repeat parse_clause_formula_pair
     2.6  val extract_clause_formula_relation =
     2.7 -  Substring.full
     2.8 -  #> Substring.position set_ClauseFormulaRelationN
     2.9 -  #> snd #> Substring.string #> strip_spaces #> explode
    2.10 -  #> parse_clause_formula_relation #> fst
    2.11 +  Substring.full #> Substring.position set_ClauseFormulaRelationN
    2.12 +  #> snd #> Substring.string #> strip_spaces_except_between_ident_chars
    2.13 +  #> explode #> parse_clause_formula_relation #> fst
    2.14  
    2.15  fun repair_conjecture_shape_and_theorem_names output conjecture_shape
    2.16                                                axiom_names =
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Aug 24 21:40:03 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Aug 24 22:57:22 2010 +0200
     3.3 @@ -540,14 +540,14 @@
     3.4      (* Unnamed, not chained formulas with schematic variables are omitted,
     3.5         because they are rejected by the backticks (`...`) parser for some
     3.6         reason. *)
     3.7 -    fun is_bad_unnamed_local th =
     3.8 -      exists (fn (_, ths) => member Thm.eq_thm ths th) named_locals orelse
     3.9 -      (exists_subterm is_Var (prop_of th) andalso not (is_chained th))
    3.10 +    fun is_good_unnamed_local th =
    3.11 +      forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals
    3.12 +      andalso (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th))
    3.13      val unnamed_locals =
    3.14 -      local_facts |> Facts.props |> filter_out is_bad_unnamed_local
    3.15 +      local_facts |> Facts.props |> filter is_good_unnamed_local
    3.16                    |> map (pair "" o single)
    3.17      val full_space =
    3.18 -      Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts);
    3.19 +      Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
    3.20      fun add_valid_facts foldx facts =
    3.21        foldx (fn (name0, ths) =>
    3.22          if name0 <> "" andalso
    3.23 @@ -563,6 +563,8 @@
    3.24              fun backquotify th =
    3.25                "`" ^ Print_Mode.setmp [Print_Mode.input]
    3.26                                   (Syntax.string_of_term ctxt) (prop_of th) ^ "`"
    3.27 +              |> String.translate (fn c => if Char.isPrint c then str c else "")
    3.28 +              |> simplify_spaces
    3.29              fun check_thms a =
    3.30                case try (ProofContext.get_thms ctxt) a of
    3.31                  NONE => false
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Aug 24 21:40:03 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Aug 24 22:57:22 2010 +0200
     4.3 @@ -234,7 +234,7 @@
     4.4    fst o Scan.finite Symbol.stopper
     4.5              (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
     4.6                              (parse_lines pool)))
     4.7 -  o explode o strip_spaces
     4.8 +  o explode o strip_spaces_except_between_ident_chars
     4.9  
    4.10  (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
    4.11  
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Aug 24 21:40:03 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Aug 24 22:57:22 2010 +0200
     5.3 @@ -9,7 +9,8 @@
     5.4    val is_true_for : (string * bool) vector -> string -> bool
     5.5    val plural_s : int -> string
     5.6    val serial_commas : string -> string list -> string list
     5.7 -  val strip_spaces : string -> string
     5.8 +  val simplify_spaces : string -> string
     5.9 +  val strip_spaces_except_between_ident_chars : string -> string
    5.10    val parse_bool_option : bool -> string -> string -> bool option
    5.11    val parse_time_option : string -> string -> Time.time option
    5.12    val scan_integer : string list -> int * string list
    5.13 @@ -39,24 +40,27 @@
    5.14    | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
    5.15    | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
    5.16  
    5.17 -fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
    5.18 -
    5.19 -fun strip_spaces_in_list [] = ""
    5.20 -  | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
    5.21 -  | strip_spaces_in_list [c1, c2] =
    5.22 -    strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
    5.23 -  | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
    5.24 +fun strip_spaces_in_list _ [] = ""
    5.25 +  | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then "" else str c1
    5.26 +  | strip_spaces_in_list is_evil [c1, c2] =
    5.27 +    strip_spaces_in_list is_evil [c1] ^ strip_spaces_in_list is_evil [c2]
    5.28 +  | strip_spaces_in_list is_evil (c1 :: c2 :: c3 :: cs) =
    5.29      if Char.isSpace c1 then
    5.30 -      strip_spaces_in_list (c2 :: c3 :: cs)
    5.31 +      strip_spaces_in_list is_evil (c2 :: c3 :: cs)
    5.32      else if Char.isSpace c2 then
    5.33        if Char.isSpace c3 then
    5.34 -        strip_spaces_in_list (c1 :: c3 :: cs)
    5.35 +        strip_spaces_in_list is_evil (c1 :: c3 :: cs)
    5.36        else
    5.37 -        str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
    5.38 -        strip_spaces_in_list (c3 :: cs)
    5.39 +        str c1 ^ (if forall is_evil [c1, c3] then " " else "") ^
    5.40 +        strip_spaces_in_list is_evil (c3 :: cs)
    5.41      else
    5.42 -      str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
    5.43 -val strip_spaces = strip_spaces_in_list o String.explode
    5.44 +      str c1 ^ strip_spaces_in_list is_evil (c2 :: c3 :: cs)
    5.45 +fun strip_spaces is_evil = strip_spaces_in_list is_evil o String.explode
    5.46 +
    5.47 +val simplify_spaces = strip_spaces (K true)
    5.48 +
    5.49 +fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
    5.50 +val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char
    5.51  
    5.52  fun parse_bool_option option name s =
    5.53    (case s of