# HG changeset patch # User blanchet # Date 1401445671 -7200 # Node ID 426ab5fabcae0f6fd04bb325b7c258957feff85c # Parent f8112c4b9cb86b95987dfea0a2b15fa715f23fe6 got rid of 'linearize' option diff -r f8112c4b9cb8 -r 426ab5fabcae src/HOL/TPTP/MaSh_Export.thy --- a/src/HOL/TPTP/MaSh_Export.thy Fri May 30 12:27:51 2014 +0200 +++ b/src/HOL/TPTP/MaSh_Export.thy Fri May 30 12:27:51 2014 +0200 @@ -34,7 +34,6 @@ val prover = hd provers val range = (1, (* ### NONE *) SOME 100) val step = 1 -val linearize = false val max_suggestions = 1024 val dir = "List" val prefix = "/tmp/" ^ dir ^ "/" @@ -47,21 +46,21 @@ () *} -ML {* Options.put_default @{system_option MaSh} "sml_knn" *} +ML {* Options.put_default @{system_option MaSh} "sml_nb" *} ML {* if do_it then - generate_mash_suggestions @{context} params (range, step) thys linearize max_suggestions + generate_mash_suggestions @{context} params (range, step) thys max_suggestions (prefix ^ "mash_sml_knn_suggestions") else () *} -ML {* Options.put_default @{system_option MaSh} "sml_nb" *} +ML {* Options.put_default @{system_option MaSh} "sml_knn" *} ML {* if do_it then - generate_mepo_suggestions @{context} params (range, step) thys linearize max_suggestions + generate_mepo_suggestions @{context} params (range, step) thys max_suggestions (prefix ^ "mash_sml_nb_suggestions") else () @@ -71,7 +70,7 @@ ML {* if do_it then - generate_mepo_suggestions @{context} params (range, step) thys linearize max_suggestions + generate_mepo_suggestions @{context} params (range, step) thys max_suggestions (prefix ^ "mepo_suggestions") else () @@ -79,7 +78,7 @@ ML {* if do_it then - generate_accessibility @{context} thys linearize (prefix ^ "mash_accessibility") + generate_accessibility @{context} thys (prefix ^ "mash_accessibility") else () *} @@ -93,14 +92,14 @@ ML {* if do_it then - generate_isar_dependencies @{context} range thys linearize (prefix ^ "mash_dependencies") + generate_isar_dependencies @{context} range thys (prefix ^ "mash_dependencies") else () *} ML {* if do_it then - generate_isar_commands @{context} prover (range, step) thys linearize max_suggestions + generate_isar_commands @{context} prover (range, step) thys max_suggestions (prefix ^ "mash_commands") else () @@ -108,7 +107,7 @@ ML {* if do_it then - generate_mepo_suggestions @{context} params (range, step) thys linearize max_suggestions + generate_mepo_suggestions @{context} params (range, step) thys max_suggestions (prefix ^ "mepo_suggestions") else () @@ -124,15 +123,14 @@ ML {* if do_it then - generate_prover_dependencies @{context} params range thys linearize - (prefix ^ "mash_prover_dependencies") + generate_prover_dependencies @{context} params range thys (prefix ^ "mash_prover_dependencies") else () *} ML {* if do_it then - generate_prover_commands @{context} params (range, step) thys linearize max_suggestions + generate_prover_commands @{context} params (range, step) thys max_suggestions (prefix ^ "mash_prover_commands") else () diff -r f8112c4b9cb8 -r 426ab5fabcae src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Fri May 30 12:27:51 2014 +0200 +++ b/src/HOL/TPTP/mash_export.ML Fri May 30 12:27:51 2014 +0200 @@ -9,20 +9,20 @@ sig type params = Sledgehammer_Prover.params - val generate_accessibility : Proof.context -> theory list -> bool -> string -> unit + val generate_accessibility : Proof.context -> theory list -> string -> unit val generate_features : Proof.context -> theory list -> string -> unit - val generate_isar_dependencies : Proof.context -> int * int option -> theory list -> bool -> + val generate_isar_dependencies : Proof.context -> int * int option -> theory list -> string -> + unit + val generate_prover_dependencies : Proof.context -> params -> int * int option -> theory list -> string -> unit - val generate_prover_dependencies : Proof.context -> params -> int * int option -> theory list -> - bool -> string -> unit val generate_isar_commands : Proof.context -> string -> (int * int option) * int -> theory list -> - bool -> int -> string -> unit + int -> string -> unit val generate_prover_commands : Proof.context -> params -> (int * int option) * int -> - theory list -> bool -> int -> string -> unit + theory list -> int -> string -> unit val generate_mepo_suggestions : Proof.context -> params -> (int * int option) * int -> - theory list -> bool -> int -> string -> unit + theory list -> int -> string -> unit val generate_mash_suggestions : Proof.context -> params -> (int * int option) * int -> - theory list -> bool -> int -> string -> unit + theory list -> int -> string -> unit val generate_mesh_suggestions : int -> string -> string -> string -> unit end; @@ -50,14 +50,13 @@ fun filter_accessible_from th = filter (fn (_, th') => thm_less (th', th)) -fun generate_accessibility ctxt thys linearize file_name = +fun generate_accessibility ctxt thys file_name = let - val path = file_name |> Path.explode + val path = Path.explode file_name val _ = File.write path "" fun do_fact (parents, fact) prevs = let - val parents = if linearize then prevs else parents val s = encode_str fact ^ ": " ^ encode_strs parents ^ "\n" val _ = File.append path s in [fact] end @@ -113,10 +112,10 @@ | NONE => (omitted_marker, [])) end -fun generate_isar_or_prover_dependencies ctxt params_opt range thys linearize file_name = +fun generate_isar_or_prover_dependencies ctxt params_opt range thys file_name = let - val path = file_name |> Path.explode - val facts = all_facts ctxt |> filter_out (has_thys thys o snd) + val path = Path.explode file_name + val facts = filter_out (has_thys thys o snd) (all_facts ctxt) val name_tabs = build_name_tables nickname_of_thm facts fun do_fact (j, (_, th)) = @@ -124,11 +123,11 @@ let val name = nickname_of_thm th val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name) - val access_facts = - if linearize then take (j - 1) facts else facts |> filter_accessible_from th - val (marker, deps) = - smart_dependencies_of ctxt params_opt access_facts name_tabs th NONE - in encode_str name ^ ": " ^ marker ^ " " ^ encode_strs deps ^ "\n" end + val access_facts = filter_accessible_from th facts + val (marker, deps) = smart_dependencies_of ctxt params_opt access_facts name_tabs th NONE + in + encode_str name ^ ": " ^ marker ^ " " ^ encode_strs deps ^ "\n" + end else "" @@ -149,8 +148,7 @@ null isar_deps orelse is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th) -fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys linearize max_suggs - file_name = +fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys max_suggs file_name = let val ho_atp = is_ho_atp ctxt prover val path = file_name |> Path.explode @@ -168,13 +166,10 @@ val goal_feats = features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature [prop_of th] |> sort_wrt fst - val access_facts = - (if linearize then take (j - 1) new_facts else new_facts |> filter_accessible_from th) @ - old_facts + val access_facts = filter_accessible_from th new_facts @ old_facts val (marker, deps) = - smart_dependencies_of ctxt params_opt access_facts name_tabs th - (SOME isar_deps) - val parents = if linearize then prevs else parents + smart_dependencies_of ctxt params_opt access_facts name_tabs th (SOME isar_deps) + val parents = parents fun extra_features_of (((_, stature), th), weight) = [prop_of th] |> features_of ctxt (theory_of_thm th) (num_old_facts + j) const_tab stature @@ -223,7 +218,7 @@ generate_isar_or_prover_commands ctxt prover (SOME params) fun generate_mepo_or_mash_suggestions mepo_or_mash_suggested_facts ctxt - (params as {provers = prover :: _, ...}) (range, step) thys linearize max_suggs file_name = + (params as {provers = prover :: _, ...}) (range, step) thys max_suggs file_name = let val ho_atp = is_ho_atp ctxt prover val path = file_name |> Path.explode @@ -246,7 +241,7 @@ let val suggs = old_facts - |> not linearize ? filter_accessible_from th + |> filter_accessible_from th |> mepo_or_mash_suggested_facts ctxt params max_suggs hyp_ts concl_t |> map (nickname_of_thm o snd) in