# HG changeset patch # User blanchet # Date 1342593844 -7200 # Node ID f1d135d0ea69d1b1c9e6aebd9494c3df9bf22bdb # Parent 6cf5e58f11850d9768c75de31ffab02146f34ab5 improved MaSh string escaping and make more operations string-based diff -r 6cf5e58f1185 -r f1d135d0ea69 src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Wed Jul 18 08:44:04 2012 +0200 @@ -29,8 +29,6 @@ | un accum (c :: cs) = un (c :: accum) cs in un [] o String.explode end -val of_fact_name = unescape_meta - val isarN = "Isa" val iterN = "Iter" val mashN = "MaSh" @@ -55,7 +53,7 @@ fun find_sugg facts sugg = find_first (fn (_, th) => Thm.get_name_hint th = sugg) facts fun sugg_facts hyp_ts concl_t facts = - map_filter (find_sugg facts o of_fact_name) + map_filter (find_sugg facts) #> take (max_facts_slack * the max_facts) #> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t fun mesh_facts fsp = @@ -103,7 +101,6 @@ in str_of_res heading facts res end fun solve_goal j name suggs = let - val name = of_fact_name name val th = case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of SOME (_, th) => th @@ -128,10 +125,12 @@ isar_s] |> cat_lines |> tracing end - val explode_suggs = space_explode " " #> filter_out (curry (op =) "") + val explode_suggs = + space_explode " " #> filter_out (curry (op =) "") #> map unescape_meta fun do_line (j, line) = case space_explode ":" line of - [goal_name, suggs] => solve_goal j goal_name (explode_suggs suggs) + [goal_name, suggs] => + solve_goal j (unescape_meta goal_name) (explode_suggs suggs) | _ => () fun total_of heading ok n = " " ^ heading ^ ": " ^ string_of_int (!ok) ^ " (" ^ diff -r 6cf5e58f1185 -r f1d135d0ea69 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/TPTP/mash_export.ML Wed Jul 18 08:44:04 2012 +0200 @@ -36,16 +36,16 @@ val feats = features_of thy status [prop_of th] val deps = isabelle_dependencies_of all_names th val kind = Thm.legacy_get_kind th - val name = fact_name_of name val core = space_implode " " prevs ^ "; " ^ space_implode " " feats val query = if kind <> "" then "? " ^ core ^ "\n" else "" val update = - "! " ^ name ^ ": " ^ core ^ "; " ^ space_implode " " deps ^ "\n" + "! " ^ escape_meta name ^ ": " ^ core ^ "; " ^ + space_implode " " deps ^ "\n" val _ = File.append path (query ^ update) in [name] end - val thy_ths = old_facts |> thms_by_thy - val parents = parent_facts thy_ths thy + val thy_facts = old_facts |> thy_facts_from_thms + val parents = parent_facts thy thy_facts in fold do_fact new_facts parents; () end fun generate_iter_suggestions ctxt (params as {provers, ...}) thy max_relevant @@ -71,9 +71,9 @@ old_facts |> Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params (hd provers) max_relevant NONE hyp_ts concl_t - |> map (fn ((name, _), _) => fact_name_of (name ())) + |> map (fn ((name, _), _) => name ()) |> sort string_ord - val s = fact_name_of name ^ ": " ^ space_implode " " suggs ^ "\n" + val s = escape_meta name ^ ": " ^ escape_metas suggs ^ "\n" in File.append path s end else () diff -r 6cf5e58f1185 -r f1d135d0ea69 src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:03 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML Wed Jul 18 08:44:04 2012 +0200 @@ -14,14 +14,15 @@ type relevance_fudge = Sledgehammer_Provers.relevance_fudge type prover_result = Sledgehammer_Provers.prover_result - val fact_name_of : string -> string + val escape_meta : string -> string + val escape_metas : string list -> string val all_non_tautological_facts_of : theory -> status Termtab.table -> fact list val theory_ord : theory * theory -> order val thm_ord : thm * thm -> order - val thms_by_thy : ('a * thm) list -> (string * thm list) list + val thy_facts_from_thms : ('a * thm) list -> string list Symtab.table val has_thy : theory -> thm -> bool - val parent_facts : (string * thm list) list -> theory -> string list + val parent_facts : theory -> string list Symtab.table -> string list val features_of : theory -> status -> term list -> string list val isabelle_dependencies_of : string list -> thm -> string list val goal_of_thm : theory -> thm -> thm @@ -80,16 +81,14 @@ "\\" ^ stringN_of_int 3 (Char.ord c) val escape_meta = String.translate escape_meta_char +val escape_metas = map escape_meta #> space_implode " " -val thy_prefix = "y_" +val thy_feature_prefix = "y_" -val fact_name_of = escape_meta -val thy_name_of = prefix thy_prefix o escape_meta -val const_name_of = prefix const_prefix o escape_meta -val type_name_of = prefix type_const_prefix o escape_meta -val class_name_of = prefix class_prefix o escape_meta - -val thy_name_of_thm = theory_of_thm #> Context.theory_name +val thy_feature_name_of = prefix thy_feature_prefix +val const_name_of = prefix const_prefix +val type_name_of = prefix type_const_prefix +val class_name_of = prefix class_prefix local @@ -191,25 +190,26 @@ val thm_ord = theory_ord o pairself theory_of_thm -fun thms_by_thy ths = - ths |> map (snd #> `thy_name_of_thm) +(* ### FIXME: optimize *) +fun thy_facts_from_thms ths = + ths |> map (snd #> `(theory_of_thm #> Context.theory_name)) |> AList.group (op =) |> sort (int_ord o pairself (length o Theory.ancestors_of o theory_of_thm o hd o snd)) - |> map (apsnd (sort thm_ord)) + |> map (apsnd (sort (rev_order o thm_ord) #> map Thm.get_name_hint)) + |> Symtab.make -fun has_thy thy th = (Context.theory_name thy = thy_name_of_thm th) +fun has_thy thy th = + Context.theory_name thy = Context.theory_name (theory_of_thm th) -fun add_last_thms thy_ths thy = - case AList.lookup (op =) thy_ths (Context.theory_name thy) of - SOME (ths as _ :: _) => insert Thm.eq_thm (List.last ths) - | _ => add_parent_thms thy_ths thy -and add_parent_thms thy_ths thy = - fold (add_last_thms thy_ths) (Theory.parents_of thy) - -fun parent_facts thy_ths thy = - add_parent_thms thy_ths thy [] - |> map (fact_name_of o Thm.get_name_hint) +fun parent_facts thy thy_facts = + let + fun add_last thy = + case Symtab.lookup thy_facts (Context.theory_name thy) of + SOME (last_fact :: _) => insert (op =) last_fact + | _ => add_parent thy + and add_parent thy = fold add_last (Theory.parents_of thy) + in add_parent thy [] end fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1}) @@ -218,7 +218,7 @@ (* TODO: Generate type classes for types? *) fun features_of thy status ts = - thy_name_of (Context.theory_name thy) :: + thy_feature_name_of (Context.theory_name thy) :: interesting_terms_types_and_classes term_max_depth type_max_depth ts |> exists (not o is_lambda_free) ts ? cons "lambdas" |> exists (exists_Const is_exists) ts ? cons "skolems" @@ -233,8 +233,7 @@ | Def => cons "def") fun isabelle_dependencies_of all_facts = - thms_in_proof (SOME all_facts) - #> map fact_name_of #> sort string_ord + thms_in_proof (SOME all_facts) #> sort string_ord val freezeT = Type.legacy_freeze_type @@ -258,27 +257,45 @@ Sledgehammer_Provers.Normal (hd provers) in prover params (K (K (K ""))) problem end +(* ### +fun compute_accessibility thy thy_facts = + let + fun add_facts (f :: fs) prevs = (f, prevs) :: add_facts fs [th] + fun add_thy facts = + let + val thy = theory_of_thm (hd facts) + val parents = parent_facts thy_facts thy + in add_thms facts parents end + in fold (add_thy o snd) thy_facts end +*) + +fun accessibility_of thy thy_facts = + case Symtab.lookup thy_facts (Context.theory_name thy) of + SOME (fact :: _) => [fact] + | _ => parent_facts thy thy_facts + +fun theory_of_fact thy fact = + Context.this_theory thy (hd (Long_Name.explode fact)) + fun generate_accessibility ctxt thy include_thy file_name = let val path = file_name |> Path.explode val _ = File.write path "" - val css_table = clasimpset_rule_table_of ctxt - fun do_thm th prevs = + fun do_fact fact prevs = let - val s = th ^ ": " ^ space_implode " " prevs ^ "\n" + val s = escape_meta fact ^ ": " ^ escape_metas prevs ^ "\n" val _ = File.append path s - in [th] end - val thy_ths = - all_non_tautological_facts_of thy css_table + in [fact] end + val thy_facts = + all_non_tautological_facts_of thy Termtab.empty |> not include_thy ? filter_out (has_thy thy o snd) - |> thms_by_thy - fun do_thy ths = + |> thy_facts_from_thms + fun do_thy facts = let - val thy = theory_of_thm (hd ths) - val parents = parent_facts thy_ths thy - val ths = ths |> map (fact_name_of o Thm.get_name_hint) - in fold do_thm ths parents; () end - in List.app (do_thy o snd) thy_ths end + val thy = theory_of_fact thy (hd facts) + val parents = parent_facts thy thy_facts + in fold do_fact facts parents; () end + in Symtab.fold (fn (_, facts) => K (do_thy facts)) thy_facts () end fun generate_features ctxt thy include_thy file_name = let @@ -292,7 +309,7 @@ let val name = Thm.get_name_hint th val feats = features_of (theory_of_thm th) status [prop_of th] - val s = fact_name_of name ^ ": " ^ space_implode " " feats ^ "\n" + val s = escape_meta name ^ ": " ^ escape_metas feats ^ "\n" in File.append path s end in List.app do_fact facts end @@ -300,9 +317,8 @@ let val path = file_name |> Path.explode val _ = File.write path "" - val css_table = clasimpset_rule_table_of ctxt val ths = - all_non_tautological_facts_of thy css_table + all_non_tautological_facts_of thy Termtab.empty |> not include_thy ? filter_out (has_thy thy o snd) |> map snd val all_names = ths |> map Thm.get_name_hint @@ -310,7 +326,7 @@ let val name = Thm.get_name_hint th val deps = isabelle_dependencies_of all_names th - val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n" + val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" in File.append path s end in List.app do_thm ths end @@ -319,13 +335,12 @@ let val path = file_name |> Path.explode val _ = File.write path "" - val css_table = clasimpset_rule_table_of ctxt val facts = - all_non_tautological_facts_of thy css_table + all_non_tautological_facts_of thy Termtab.empty |> not include_thy ? filter_out (has_thy thy o snd) val ths = facts |> map snd val all_names = ths |> map Thm.get_name_hint - fun is_dep dep (_, th) = fact_name_of (Thm.get_name_hint th) = dep + fun is_dep dep (_, th) = Thm.get_name_hint th = dep fun add_isa_dep facts dep accum = if exists (is_dep dep) accum then accum @@ -333,7 +348,7 @@ SOME ((name, status), th) => accum @ [((name, status), th)] | NONE => accum (* shouldn't happen *) fun fix_name ((_, stature), th) = - ((fn () => th |> Thm.get_name_hint |> fact_name_of, stature), th) + ((fn () => th |> Thm.get_name_hint, stature), th) fun do_thm th = let val name = Thm.get_name_hint th @@ -358,7 +373,7 @@ used_facts |> map fst |> sort string_ord | _ => isa_deps end - val s = fact_name_of name ^ ": " ^ space_implode " " deps ^ "\n" + val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" in File.append path s end in List.app do_thm ths end @@ -368,16 +383,14 @@ fun mash_RESET () = (warning "MaSh RESET"; File.rm (mk_path model_file)) fun mash_ADD fact access feats deps = - warning ("MaSh ADD " ^ fact ^ ": " ^ space_implode " " access ^ "; " ^ - space_implode " " feats ^ "; " ^ space_implode " " deps) + warning ("MaSh ADD " ^ fact ^ ": " ^ escape_metas access ^ "; " ^ + escape_metas feats ^ "; " ^ escape_metas deps) fun mash_DEL facts feats = - warning ("MaSh DEL " ^ space_implode " " facts ^ "; " ^ - space_implode " " feats) + warning ("MaSh DEL " ^ escape_metas facts ^ "; " ^ escape_metas feats) fun mash_SUGGEST access feats = - (warning ("MaSh SUGGEST " ^ space_implode " " access ^ "; " ^ - space_implode " " feats); + (warning ("MaSh SUGGEST " ^ escape_metas access ^ "; " ^ escape_metas feats); []) @@ -422,8 +435,8 @@ fun mash_save ({fresh, completed_thys, thy_facts} : mash_state) = let val path = mk_path state_file - val comp_line = (completed_thys |> Symtab.keys |> space_implode " ") ^ "\n" - fun fact_line_for (thy, facts) = space_implode " " (thy :: facts) ^ "\n" + val comp_line = (completed_thys |> Symtab.keys |> escape_metas) ^ "\n" + fun fact_line_for (thy, facts) = escape_metas (thy :: facts) ^ "\n" in File.write path (string_of_int fresh ^ "\n" ^ comp_line); Symtab.fold (fn thy_fact => fn () => @@ -451,13 +464,6 @@ fun mash_can_suggest_facts () = not (Symtab.is_empty (#thy_facts (mash_value ()))) -fun accessibility_of thy thy_facts = - let - val _ = 0 - in - [] (*###*) - end - fun mash_suggest_facts ctxt params prover max_facts hyp_ts concl_t facts = let val thy = Proof_Context.theory_of ctxt @@ -479,7 +485,7 @@ val fact = fresh_fact_prefix ^ string_of_int fresh val access = accessibility_of thy thy_facts val feats = features_of thy General [t] - val deps = ths |> map (fact_name_of o Thm.get_name_hint) + val deps = ths |> map Thm.get_name_hint in mash_ADD fact access feats deps; {fresh = fresh + 1, completed_thys = completed_thys,