summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML

author | blanchet |

Thu Nov 21 12:29:29 2013 +0100 (2013-11-21 ago) | |

changeset 54546 | 8b403a7a8c44 |

parent 54504 | 096f7d452164 |

child 54700 | 64177ce0a7bd |

permissions | -rw-r--r-- |

fixed spying so that the envirnoment variables are queried at run-time not at build-time

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

2 Author: Jasmin Blanchette, TU Muenchen

3 Author: Steffen Juilf Smolka, TU Muenchen

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

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

7 *)

9 signature SLEDGEHAMMER_TRY0 =

10 sig

11 type isar_proof = Sledgehammer_Proof.isar_proof

12 type preplay_interface = Sledgehammer_Preplay.preplay_interface

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

15 end;

17 structure Sledgehammer_Try0 : SLEDGEHAMMER_TRY0 =

18 struct

20 open Sledgehammer_Proof

21 open Sledgehammer_Preplay

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

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

25 let

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

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

28 (*fun step_without_facts method =

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

30 in

31 (* FIXME *)

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

33 the variants using no facts first. *)

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

35 end

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

38 | try0_step preplay_timeout ({preplay_quietly, get_preplay_time,

39 set_preplay_time, ...} : preplay_interface)

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

41 let

43 val timeout =

44 case get_preplay_time l of

45 (true, _) => preplay_timeout

46 | (false, t) => t

48 fun try_variant variant =

49 case preplay_quietly timeout variant of

50 (true, _) => NONE

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

53 in

54 case Par_List.get_some try_variant (variants step) of

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

56 | NONE => step

57 end

59 fun try0 preplay_timeout preplay_interface proof =

60 map_isar_steps (try0_step preplay_timeout preplay_interface) proof

62 end;