equal
deleted
inserted
replaced
34 val report_path = report_file_name |> Path.explode |
34 val report_path = report_file_name |> Path.explode |
35 val _ = File.write report_path "" |
35 val _ = File.write report_path "" |
36 |
36 |
37 fun print s = File.append report_path (s ^ "\n") |
37 fun print s = File.append report_path (s ^ "\n") |
38 |
38 |
39 val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = default_params thy [] |
39 val {provers, max_facts, slice, type_enc, lam_trans, timeout, induction_rules, ...} = |
|
40 default_params thy [] |
40 val prover = hd provers |
41 val prover = hd provers |
41 val max_suggs = generous_max_suggestions (the max_facts) |
42 val max_suggs = generous_max_suggestions (the max_facts) |
|
43 val inst_inducts = induction_rules = SOME Instantiate |
42 |
44 |
43 val method_of_file_name = |
45 val method_of_file_name = |
44 perhaps (try (unsuffix "_suggestions")) o List.last o space_explode "/" |
46 perhaps (try (unsuffix "_suggestions")) o List.last o space_explode "/" |
45 |
47 |
46 val methods = "isar" :: map method_of_file_name file_names |
48 val methods = "isar" :: map method_of_file_name file_names |
51 fun pad lines = lines @ replicate (num_lines - length lines) "" |
53 fun pad lines = lines @ replicate (num_lines - length lines) "" |
52 |
54 |
53 val liness' = Ctr_Sugar_Util.transpose (map pad liness0) |
55 val liness' = Ctr_Sugar_Util.transpose (map pad liness0) |
54 |
56 |
55 val css = clasimpset_rule_table_of ctxt |
57 val css = clasimpset_rule_table_of ctxt |
56 val facts = all_facts ctxt true false Keyword.empty_keywords [] [] css |
58 val facts = all_facts ctxt true Keyword.empty_keywords [] [] css |
57 val name_tabs = build_name_tables nickname_of_thm facts |
59 val name_tabs = build_name_tables nickname_of_thm facts |
58 |
60 |
59 fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) |
61 fun with_index facts s = (find_index (curry (op =) s) facts + 1, s) |
60 fun index_str (j, s) = s ^ "@" ^ string_of_int j |
62 fun index_str (j, s) = s ^ "@" ^ string_of_int j |
61 val str_of_method = enclose " " ": " |
63 val str_of_method = enclose " " ": " |
120 |
122 |
121 val facts = |
123 val facts = |
122 suggs |
124 suggs |
123 |> find_suggested_facts ctxt facts |
125 |> find_suggested_facts ctxt facts |
124 |> map (fact_of_raw_fact #> nickify) |
126 |> map (fact_of_raw_fact #> nickify) |
125 |> maybe_instantiate_inducts ctxt hyp_ts concl_t |
127 |> inst_inducts ? instantiate_inducts ctxt hyp_ts concl_t |
126 |> take (the max_facts) |
128 |> take (the max_facts) |
127 |> map fact_of_raw_fact |
129 |> map fact_of_raw_fact |
128 val ctxt = ctxt |> set_file_name method prob_dir_name |
130 val ctxt = ctxt |> set_file_name method prob_dir_name |
129 val res as {outcome, ...} = run_prover_for_mash ctxt params prover name facts goal |
131 val res as {outcome, ...} = run_prover_for_mash ctxt params prover name facts goal |
130 val ok = if is_none outcome then 1 else 0 |
132 val ok = if is_none outcome then 1 else 0 |
139 map snd ress |
141 map snd ress |
140 end |
142 end |
141 else |
143 else |
142 zeros |
144 zeros |
143 |
145 |
144 val inst_inducts = Config.get ctxt instantiate_inducts |
|
145 val options = |
146 val options = |
146 ["prover = " ^ prover, |
147 ["prover = " ^ prover, |
147 "max_facts = " ^ string_of_int (the max_facts), |
148 "max_facts = " ^ string_of_int (the max_facts), |
148 "slice" |> not slice ? prefix "dont_", |
149 "slice" |> not slice ? prefix "dont_", |
149 "type_enc = " ^ the_default "smart" type_enc, |
150 "type_enc = " ^ the_default "smart" type_enc, |