merge aliased theorems in MaSh dependencies, modulo symmetry of equality
authorblanchet
Wed Dec 12 02:47:45 2012 +0100 (2012-12-12 ago)
changeset 504853c6ac2da2f45
parent 50484 8ec31bdb9d36
child 50486 d5dc28fafd9d
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
src/HOL/TPTP/atp_theory_export.ML
src/HOL/TPTP/mash_eval.ML
src/HOL/TPTP/mash_export.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Wed Dec 12 00:24:06 2012 +0100
     1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Wed Dec 12 02:47:45 2012 +0100
     1.3 @@ -136,13 +136,13 @@
     1.4      val atp_problem =
     1.5        atp_problem
     1.6        |> map (apsnd (filter_out (is_problem_line_tautology ctxt format)))
     1.7 -    val ths = facts |> map snd
     1.8 -    val all_names = ths |> map (rpair () o Thm.get_name_hint) |> Symtab.make
     1.9 +    val all_names = Sledgehammer_Fact.build_all_names Thm.get_name_hint facts
    1.10      val infers =
    1.11 -      facts |> map (fn (_, th) =>
    1.12 -                       (fact_name_of (Thm.get_name_hint th),
    1.13 -                        th |> Sledgehammer_Util.thms_in_proof (SOME all_names)
    1.14 -                           |> map fact_name_of))
    1.15 +      facts
    1.16 +      |> map (fn (_, th) =>
    1.17 +                 (fact_name_of (Thm.get_name_hint th),
    1.18 +                  th |> Sledgehammer_Util.thms_in_proof (SOME all_names)
    1.19 +                     |> map fact_name_of))
    1.20      val all_atp_problem_names =
    1.21        atp_problem |> maps (map ident_of_problem_line o snd)
    1.22      val infers =
     2.1 --- a/src/HOL/TPTP/mash_eval.ML	Wed Dec 12 00:24:06 2012 +0100
     2.2 +++ b/src/HOL/TPTP/mash_eval.ML	Wed Dec 12 02:47:45 2012 +0100
     2.3 @@ -24,8 +24,6 @@
     2.4  val MeShN = "MeSh"
     2.5  val IsarN = "Isar"
     2.6  
     2.7 -val all_names = map (rpair () o nickname_of) #> Symtab.make
     2.8 -
     2.9  fun evaluate_mash_suggestions ctxt params prob_dir_name sugg_file_name
    2.10                                report_file_name =
    2.11    let
    2.12 @@ -40,7 +38,7 @@
    2.13      val lines = sugg_path |> File.read_lines
    2.14      val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    2.15      val facts = all_facts ctxt true false Symtab.empty [] [] css
    2.16 -    val all_names = all_names (facts |> map snd)
    2.17 +    val all_names = build_all_names nickname_of facts
    2.18      val mepo_ok = Unsynchronized.ref 0
    2.19      val mash_ok = Unsynchronized.ref 0
    2.20      val mesh_ok = Unsynchronized.ref 0
     3.1 --- a/src/HOL/TPTP/mash_export.ML	Wed Dec 12 00:24:06 2012 +0100
     3.2 +++ b/src/HOL/TPTP/mash_export.ML	Wed Dec 12 02:47:45 2012 +0100
     3.3 @@ -28,11 +28,12 @@
     3.4  structure MaSh_Export : MASH_EXPORT =
     3.5  struct
     3.6  
     3.7 +open Sledgehammer_Fact
     3.8  open Sledgehammer_MePo
     3.9  open Sledgehammer_MaSh
    3.10  
    3.11  fun thy_map_from_facts ths =
    3.12 -  ths |> sort (thm_ord o swap o pairself snd)
    3.13 +  ths |> rev
    3.14        |> map (snd #> `(theory_of_thm #> Context.theory_name))
    3.15        |> AList.coalesce (op =)
    3.16        |> map (apsnd (map nickname_of))
    3.17 @@ -45,6 +46,7 @@
    3.18  fun all_facts ctxt =
    3.19    let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in
    3.20      Sledgehammer_Fact.all_facts ctxt true false Symtab.empty [] [] css
    3.21 +    |> sort (thm_ord o pairself snd)
    3.22    end
    3.23  
    3.24  fun add_thy_parent_facts thy_map thy =
    3.25 @@ -59,8 +61,6 @@
    3.26  val thy_name_of_fact = hd o Long_Name.explode
    3.27  fun thy_of_fact thy = Context.get_theory thy o thy_name_of_fact
    3.28  
    3.29 -val all_names = map (rpair () o nickname_of) #> Symtab.make
    3.30 -
    3.31  fun generate_accessibility ctxt thys include_thys file_name =
    3.32    let
    3.33      val path = file_name |> Path.explode
    3.34 @@ -110,18 +110,16 @@
    3.35      val path = file_name |> Path.explode
    3.36      val _ = File.write path ""
    3.37      val facts =
    3.38 -      all_facts ctxt
    3.39 -      |> not include_thys ? filter_out (has_thys thys o snd)
    3.40 -    val ths = facts |> map snd
    3.41 -    val all_names = all_names ths
    3.42 -    fun do_thm th =
    3.43 +      all_facts ctxt |> not include_thys ? filter_out (has_thys thys o snd)
    3.44 +    val all_names = build_all_names nickname_of facts
    3.45 +    fun do_fact (_, th) =
    3.46        let
    3.47          val name = nickname_of th
    3.48          val deps =
    3.49            isar_or_prover_dependencies_of ctxt params_opt facts all_names th
    3.50          val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n"
    3.51        in File.append path s end
    3.52 -  in List.app do_thm ths end
    3.53 +  in List.app do_fact facts end
    3.54  
    3.55  fun generate_isar_dependencies ctxt =
    3.56    generate_isar_or_prover_dependencies ctxt NONE
    3.57 @@ -134,10 +132,8 @@
    3.58      val path = file_name |> Path.explode
    3.59      val _ = File.write path ""
    3.60      val facts = all_facts ctxt
    3.61 -    val (new_facts, old_facts) =
    3.62 -      facts |> List.partition (has_thys thys o snd)
    3.63 -            |>> sort (thm_ord o pairself snd)
    3.64 -    val all_names = all_names (map snd facts)
    3.65 +    val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
    3.66 +    val all_names = build_all_names nickname_of facts
    3.67      fun do_fact ((_, stature), th) prevs =
    3.68        let
    3.69          val name = nickname_of th
    3.70 @@ -171,9 +167,7 @@
    3.71      val _ = File.write path ""
    3.72      val prover = hd provers
    3.73      val facts = all_facts ctxt
    3.74 -    val (new_facts, old_facts) =
    3.75 -      facts |> List.partition (has_thys thys o snd)
    3.76 -            |>> sort (thm_ord o pairself snd)
    3.77 +    val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
    3.78      fun do_fact (fact as (_, th)) old_facts =
    3.79        let
    3.80          val name = nickname_of th
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 00:24:06 2012 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 02:47:45 2012 +0100
     4.3 @@ -25,7 +25,8 @@
     4.4      -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
     4.5    val backquote_thm : Proof.context -> thm -> string
     4.6    val clasimpset_rule_table_of : Proof.context -> status Termtab.table
     4.7 -  val normalize_eq : term -> term
     4.8 +  val build_all_names :
     4.9 +    (thm -> string) -> ('a * thm) list -> string Symtab.table
    4.10    val maybe_instantiate_inducts :
    4.11      Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
    4.12      -> (((unit -> string) * 'a) * thm) list
    4.13 @@ -320,9 +321,25 @@
    4.14      else HOLogic.mk_Trueprop (HOLogic.mk_not (t0 $ t2 $ t1))
    4.15    | normalize_eq t = t
    4.16  
    4.17 -fun uniquify xs =
    4.18 +val normalize_eq_etc = normalize_eq o Term_Subst.zero_var_indexes
    4.19 +
    4.20 +fun if_thm_before th th' =
    4.21 +  if Theory.subthy (pairself Thm.theory_of_thm (th, th')) then th else th'
    4.22 +
    4.23 +fun build_all_names name_of facts =
    4.24 +  Termtab.fold
    4.25 +      (fn (_, aliases as main :: _) =>
    4.26 +          fold (fn alias =>
    4.27 +                   Symtab.update (name_of alias,
    4.28 +                                  name_of (if_thm_before main alias))) aliases)
    4.29 +      (fold_rev (fn (_, thm) =>
    4.30 +                    Termtab.cons_list (normalize_eq_etc (prop_of thm), thm))
    4.31 +            facts Termtab.empty)
    4.32 +      Symtab.empty
    4.33 +
    4.34 +fun uniquify facts =
    4.35    Termtab.fold (cons o snd)
    4.36 -      (fold (Termtab.default o `(normalize_eq o prop_of o snd)) xs
    4.37 +      (fold (Termtab.default o `(normalize_eq_etc o prop_of o snd)) facts
    4.38              Termtab.empty) []
    4.39  
    4.40  fun struct_induct_rule_on th =
    4.41 @@ -411,36 +428,37 @@
    4.42            I
    4.43          else
    4.44            let
    4.45 -            val multi = length ths > 1
    4.46 +            val n = length ths
    4.47 +            val multi = n > 1
    4.48              fun check_thms a =
    4.49                case try (Proof_Context.get_thms ctxt) a of
    4.50                  NONE => false
    4.51                | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
    4.52            in
    4.53 -            pair 1
    4.54 -            #> fold (fn th => fn (j, (multis, unis)) =>
    4.55 -                        (j + 1,
    4.56 -                         if not (member Thm.eq_thm_prop add_ths th) andalso
    4.57 -                            is_theorem_bad_for_atps ho_atp th then
    4.58 -                           (multis, unis)
    4.59 -                         else
    4.60 -                           let
    4.61 -                             val new =
    4.62 -                               (((fn () =>
    4.63 -                                     if name0 = "" then
    4.64 -                                       backquote_thm ctxt th
    4.65 -                                     else
    4.66 -                                       [Facts.extern ctxt facts name0,
    4.67 -                                        Name_Space.extern ctxt full_space name0]
    4.68 -                                       |> find_first check_thms
    4.69 -                                       |> the_default name0
    4.70 -                                       |> make_name reserved multi j),
    4.71 -                                  stature_of_thm global assms chained css name0
    4.72 -                                                 th), th)
    4.73 -                           in
    4.74 -                             if multi then (new :: multis, unis)
    4.75 -                             else (multis, new :: unis)
    4.76 -                           end)) ths
    4.77 +            pair n
    4.78 +            #> fold_rev (fn th => fn (j, (multis, unis)) =>
    4.79 +                   (j - 1,
    4.80 +                    if not (member Thm.eq_thm_prop add_ths th) andalso
    4.81 +                       is_theorem_bad_for_atps ho_atp th then
    4.82 +                      (multis, unis)
    4.83 +                    else
    4.84 +                      let
    4.85 +                        val new =
    4.86 +                          (((fn () =>
    4.87 +                                if name0 = "" then
    4.88 +                                  backquote_thm ctxt th
    4.89 +                                else
    4.90 +                                  [Facts.extern ctxt facts name0,
    4.91 +                                   Name_Space.extern ctxt full_space name0]
    4.92 +                                  |> find_first check_thms
    4.93 +                                  |> the_default name0
    4.94 +                                  |> make_name reserved multi j),
    4.95 +                             stature_of_thm global assms chained css name0 th),
    4.96 +                           th)
    4.97 +                      in
    4.98 +                        if multi then (new :: multis, unis)
    4.99 +                        else (multis, new :: unis)
   4.100 +                      end)) ths
   4.101              #> snd
   4.102            end)
   4.103    in
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Dec 12 00:24:06 2012 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Dec 12 02:47:45 2012 +0100
     5.3 @@ -54,9 +54,9 @@
     5.4    val features_of :
     5.5      Proof.context -> string -> theory -> stature -> term list
     5.6      -> (string * real) list
     5.7 -  val isar_dependencies_of : unit Symtab.table -> thm -> string list option
     5.8 +  val isar_dependencies_of : string Symtab.table -> thm -> string list option
     5.9    val prover_dependencies_of :
    5.10 -    Proof.context -> params -> string -> int -> fact list -> unit Symtab.table
    5.11 +    Proof.context -> params -> string -> int -> fact list -> string Symtab.table
    5.12      -> thm -> bool * string list option
    5.13    val weight_mash_facts : ('a * thm) list -> (('a * thm) * real) list
    5.14    val find_mash_suggestions :
    5.15 @@ -296,7 +296,7 @@
    5.16  
    5.17  local
    5.18  
    5.19 -val version = "*** MaSh version 20121205c ***"
    5.20 +val version = "*** MaSh version 20121212a ***"
    5.21  
    5.22  exception Too_New of unit
    5.23  
    5.24 @@ -836,7 +836,7 @@
    5.25  
    5.26  val commit_timeout = seconds 30.0
    5.27  
    5.28 -(* The timeout is understood in a very slack fashion. *)
    5.29 +(* The timeout is understood in a very relaxed fashion. *)
    5.30  fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover
    5.31                       auto_level run_prover learn_timeout facts =
    5.32    let
    5.33 @@ -844,9 +844,9 @@
    5.34      fun next_commit_time () =
    5.35        Time.+ (Timer.checkRealTimer timer, commit_timeout)
    5.36      val {fact_G, ...} = mash_get ctxt
    5.37 +    val facts = facts |> sort (thm_ord o pairself snd)
    5.38      val (old_facts, new_facts) =
    5.39        facts |> List.partition (is_fact_in_graph fact_G)
    5.40 -            ||> sort (thm_ord o pairself snd)
    5.41    in
    5.42      if null new_facts andalso (not run_prover orelse null old_facts) then
    5.43        if auto_level < 2 then
    5.44 @@ -861,9 +861,7 @@
    5.45          ""
    5.46      else
    5.47        let
    5.48 -        val all_names =
    5.49 -          Symtab.empty
    5.50 -          |> fold Symtab.update (facts |> map (rpair () o nickname_of o snd))
    5.51 +        val all_names = build_all_names nickname_of facts
    5.52          fun deps_of status th =
    5.53            if status = Non_Rec_Def orelse status = Rec_Def then
    5.54              SOME []
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Dec 12 00:24:06 2012 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Dec 12 02:47:45 2012 +0100
     6.3 @@ -17,7 +17,7 @@
     6.4    val parse_time_option : string -> string -> Time.time option
     6.5    val subgoal_count : Proof.state -> int
     6.6    val reserved_isar_keyword_table : unit -> unit Symtab.table
     6.7 -  val thms_in_proof : unit Symtab.table option -> thm -> string list
     6.8 +  val thms_in_proof : string Symtab.table option -> thm -> string list
     6.9    val thms_of_name : Proof.context -> string -> thm list
    6.10    val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
    6.11  end;
    6.12 @@ -97,7 +97,10 @@
    6.13    let
    6.14      val collect =
    6.15        case all_names of
    6.16 -        SOME names => (fn s => Symtab.defined names s ? insert (op =) s)
    6.17 +        SOME names =>
    6.18 +        (fn s => case Symtab.lookup names s of
    6.19 +                   SOME s' => insert (op =) s'
    6.20 +                 | NONE => I)
    6.21        | NONE => insert (op =)
    6.22      val names =
    6.23        [] |> fold_body_thms (Thm.get_name_hint th) collect [Thm.proof_body_of th]