smolkas@52592

1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_try0.ML

smolkas@52592

2 
Author: Jasmin Blanchette, TU Muenchen

smolkas@52592

3 
Author: Steffen Juilf Smolka, TU Muenchen

smolkas@52592

4 

smolkas@52592

5 
Try replacing calls to metis with calls to other proof methods in order to

smolkas@52592

6 
speed up proofs, eliminate dependencies, and repair broken proof steps.

smolkas@52592

7 
*)

smolkas@52592

8 

smolkas@52592

9 
signature SLEDGEHAMMER_TRY0 =

smolkas@52592

10 
sig

smolkas@52592

11 
type isar_proof = Sledgehammer_Proof.isar_proof

smolkas@52592

12 
type preplay_interface = Sledgehammer_Preplay.preplay_interface

smolkas@52592

13 

smolkas@52592

14 
val try0 : Time.time > preplay_interface > isar_proof > isar_proof

blanchet@54504

15 
end;

smolkas@52592

16 

smolkas@52592

17 
structure Sledgehammer_Try0 : SLEDGEHAMMER_TRY0 =

smolkas@52592

18 
struct

smolkas@52592

19 

smolkas@52592

20 
open Sledgehammer_Proof

smolkas@52592

21 
open Sledgehammer_Preplay

smolkas@52592

22 

smolkas@52612

23 
fun variants (Let _) = raise Fail "Sledgehammer_Try0: variants"

smolkas@52612

24 
 variants (Prove (qs, xs, l, t, subproofs, By (facts, _))) =

smolkas@52592

25 
let

smolkas@52629

26 
val methods = [SimpM, FastforceM, AutoM, ArithM, ForceM, BlastM]

smolkas@52592

27 
fun step method = Prove (qs, xs, l, t, subproofs, By (facts, method))

smolkas@52612

28 
(*fun step_without_facts method =

smolkas@52612

29 
Prove (qs, xs, l, t, subproofs, By (no_facts, method))*)

smolkas@52592

30 
in

smolkas@52611

31 
(* FIXME *)

smolkas@52592

32 
(* There seems to be a bias for methods earlier in the list, so we put

smolkas@52592

33 
the variants using no facts first. *)

smolkas@52611

34 
(*map step_without_facts methods @*) map step methods

smolkas@52592

35 
end

smolkas@52592

36 

smolkas@52612

37 
fun try0_step _ _ (step as Let _) = step

smolkas@52626

38 
 try0_step preplay_timeout ({preplay_quietly, get_preplay_time,

smolkas@52626

39 
set_preplay_time, ...} : preplay_interface)

smolkas@52592

40 
(step as Prove (_, _, l, _, _, _)) =

smolkas@52592

41 
let

smolkas@52592

42 

smolkas@52626

43 
val timeout =

smolkas@52626

44 
case get_preplay_time l of

smolkas@52626

45 
(true, _) => preplay_timeout

smolkas@52626

46 
 (false, t) => t

smolkas@52592

47 

smolkas@52592

48 
fun try_variant variant =

smolkas@52592

49 
case preplay_quietly timeout variant of

smolkas@52592

50 
(true, _) => NONE

smolkas@52592

51 
 time as (false, _) => SOME (variant, time)

smolkas@52592

52 

smolkas@52592

53 
in

smolkas@52592

54 
case Par_List.get_some try_variant (variants step) of

smolkas@52626

55 
SOME (step, time) => (set_preplay_time l time; step)

smolkas@52626

56 
 NONE => step

smolkas@52592

57 
end

smolkas@52592

58 

smolkas@52626

59 
fun try0 preplay_timeout preplay_interface proof =

smolkas@52626

60 
map_isar_steps (try0_step preplay_timeout preplay_interface) proof

smolkas@52592

61 

blanchet@54504

62 
end;
