69 fun add_chained [] t = t |
70 fun add_chained [] t = t |
70 | add_chained chained ((t as Const (@{const_name Pure.all}, _)) $ Abs (s, T, u)) = |
71 | add_chained chained ((t as Const (@{const_name Pure.all}, _)) $ Abs (s, T, u)) = |
71 t $ Abs (s, T, add_chained chained u) |
72 t $ Abs (s, T, add_chained chained u) |
72 | add_chained chained t = Logic.list_implies (chained, t) |
73 | add_chained chained t = Logic.list_implies (chained, t) |
73 |
74 |
74 fun play_one_line_proof minimize timeout used_facts state i (preferred_meth, methss) = |
75 fun play_one_line_proof minimize timeout used_facts0 state i (preferred_meth, methss) = |
75 if timeout = Time.zeroTime then |
76 let val used_facts = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts0 in |
76 (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) |
77 if timeout = Time.zeroTime then |
77 else |
78 (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) |
78 let |
79 else |
79 val ctxt = Proof.context_of state |
80 let |
80 |
81 val ctxt = Proof.context_of state |
81 val fact_names = map fst used_facts |
82 |
82 val {facts = chained, goal, ...} = Proof.goal state |
83 val fact_names = map fst used_facts |
83 val goal_t = Logic.get_goal (Thm.prop_of goal) i |
84 val {facts = chained, goal, ...} = Proof.goal state |
84 |> add_chained (map Thm.prop_of chained) |
85 val goal_t = Logic.get_goal (Thm.prop_of goal) i |
85 |
86 |> add_chained (map Thm.prop_of chained) |
86 fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) |
87 |
87 | try_methss ress [] = |
88 fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) |
88 (used_facts, |
89 | try_methss ress [] = |
89 (case AList.lookup (op =) ress preferred_meth of |
90 (used_facts, |
90 SOME play => (preferred_meth, play) |
91 (case AList.lookup (op =) ress preferred_meth of |
91 | NONE => hd (sort (play_outcome_ord o apply2 snd) (rev ress)))) |
92 SOME play => (preferred_meth, play) |
92 | try_methss ress (meths :: methss) = |
93 | NONE => hd (sort (play_outcome_ord o apply2 snd) (rev ress)))) |
93 let |
94 | try_methss ress (meths :: methss) = |
94 fun mk_step fact_names meths = |
95 let |
95 Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "") |
96 fun mk_step fact_names meths = |
96 in |
97 Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "") |
97 (case preplay_isar_step ctxt timeout [] (mk_step fact_names meths) of |
98 in |
98 (res as (meth, Played time)) :: _ => |
99 (case preplay_isar_step ctxt timeout [] (mk_step fact_names meths) of |
99 (* if a fact is needed by an ATP, it will be needed by "metis" *) |
100 (res as (meth, Played time)) :: _ => |
100 if not minimize orelse is_metis_method meth then |
101 (* if a fact is needed by an ATP, it will be needed by "metis" *) |
101 (used_facts, res) |
102 if not minimize orelse is_metis_method meth then |
102 else |
103 (used_facts, res) |
103 let |
104 else |
104 val (time', used_names') = |
105 let |
105 minimized_isar_step ctxt time (mk_step fact_names [meth]) |
106 val (time', used_names') = |
106 ||> (facts_of_isar_step #> snd) |
107 minimized_isar_step ctxt time (mk_step fact_names [meth]) |
107 val used_facts' = filter (member (op =) used_names' o fst) used_facts |
108 ||> (facts_of_isar_step #> snd) |
108 in |
109 val used_facts' = filter (member (op =) used_names' o fst) used_facts |
109 (used_facts', (meth, Played time')) |
110 in |
110 end |
111 (used_facts', (meth, Played time')) |
111 | ress' => try_methss (ress' @ ress) methss) |
112 end |
112 end |
113 | ress' => try_methss (ress' @ ress) methss) |
113 in |
114 end |
114 try_methss [] methss |
115 in |
115 end |
116 try_methss [] methss |
|
117 end |
|
118 end |
116 |
119 |
117 fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, minimize, timeout, |
120 fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, minimize, timeout, |
118 preplay_timeout, expect, ...}) mode output_result only learn |
121 preplay_timeout, expect, ...}) mode output_result only learn |
119 {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = |
122 {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name = |
120 let |
123 let |