wneuper/isa: src/HOL/Mirabelle/Tools/mirabelle

     1 (*  Title:      HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

     2     Author:     Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich

     3 *)

     5 structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =

     6 struct

     8 val proverK = "prover"

     9 val prover_timeoutK = "prover_timeout"

    10 val keepK = "keep"

    11 val full_typesK = "full_types"

    12 val type_sysK = "type_sys"

    13 val minimizeK = "minimize"

    14 val minimize_timeoutK = "minimize_timeout"

    15 val metis_ftK = "metis_ft"

    16 val reconstructorK = "reconstructor"

    18 fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "

    19 fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "

    20 fun reconstructor_tag reconstructor id =

    21   "#" ^ string_of_int id ^ " " ^ (!reconstructor) ^ " (sledgehammer): "

    23 val separator = "-----"

    26 datatype sh_data = ShData of {

    27   calls: int,

    28   success: int,

    29   nontriv_calls: int,

    30   nontriv_success: int,

    31   lemmas: int,

    32   max_lems: int,

    33   time_isa: int,

    34   time_prover: int,

    35   time_prover_fail: int}

    37 datatype re_data = ReData of {

    38   calls: int,

    39   success: int,

    40   nontriv_calls: int,

    41   nontriv_success: int,

    42   proofs: int,

    43   time: int,

    44   timeout: int,

    45   lemmas: int * int * int,

    46   posns: (Position.T * bool) list

    47   }

    49 datatype min_data = MinData of {

    50   succs: int,

    51   ab_ratios: int

    52   }

    54 fun make_sh_data

    55       (calls,success,nontriv_calls,nontriv_success,lemmas,max_lems,time_isa,

    56        time_prover,time_prover_fail) =

    57   ShData{calls=calls, success=success, nontriv_calls=nontriv_calls,

    58          nontriv_success=nontriv_success, lemmas=lemmas, max_lems=max_lems,

    59          time_isa=time_isa, time_prover=time_prover,

    60          time_prover_fail=time_prover_fail}

    62 fun make_min_data (succs, ab_ratios) =

    63   MinData{succs=succs, ab_ratios=ab_ratios}

    65 fun make_re_data (calls,success,nontriv_calls,nontriv_success,proofs,time,

    66                   timeout,lemmas,posns) =

    67   ReData{calls=calls, success=success, nontriv_calls=nontriv_calls,

    68          nontriv_success=nontriv_success, proofs=proofs, time=time,

    69          timeout=timeout, lemmas=lemmas, posns=posns}

    71 val empty_sh_data = make_sh_data (0, 0, 0, 0, 0, 0, 0, 0, 0)

    72 val empty_min_data = make_min_data (0, 0)

    73 val empty_re_data = make_re_data (0, 0, 0, 0, 0, 0, 0, (0,0,0), [])

    75 fun tuple_of_sh_data (ShData {calls, success, nontriv_calls, nontriv_success,

    76                               lemmas, max_lems, time_isa,

    77   time_prover, time_prover_fail}) = (calls, success, nontriv_calls,

    78   nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail)

    80 fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios)

    82 fun tuple_of_re_data (ReData {calls, success, nontriv_calls, nontriv_success,

    83   proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls,

    84   nontriv_success, proofs, time, timeout, lemmas, posns)

    87 datatype reconstructor_mode =

    88   Unminimized | Minimized | UnminimizedFT | MinimizedFT

    90 datatype data = Data of {

    91   sh: sh_data,

    92   min: min_data,

    93   re_u: re_data, (* reconstructor with unminimized set of lemmas *)

    94   re_m: re_data, (* reconstructor with minimized set of lemmas *)

    95   re_uft: re_data, (* reconstructor with unminimized set of lemmas and fully-typed *)

    96   re_mft: re_data, (* reconstructor with minimized set of lemmas and fully-typed *)

    97   mini: bool   (* with minimization *)

    98   }

   100 fun make_data (sh, min, re_u, re_m, re_uft, re_mft, mini) =

   101   Data {sh=sh, min=min, re_u=re_u, re_m=re_m, re_uft=re_uft, re_mft=re_mft,

   102     mini=mini}

   104 val empty_data = make_data (empty_sh_data, empty_min_data,

   105   empty_re_data, empty_re_data, empty_re_data, empty_re_data, false)

   107 fun map_sh_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =

   108   let val sh' = make_sh_data (f (tuple_of_sh_data sh))

   109   in make_data (sh', min, re_u, re_m, re_uft, re_mft, mini) end

   111 fun map_min_data f (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =

   112   let val min' = make_min_data (f (tuple_of_min_data min))

   113   in make_data (sh, min', re_u, re_m, re_uft, re_mft, mini) end

   115 fun map_re_data f m (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =

   116   let

   117     fun map_me g Unminimized   (u, m, uft, mft) = (g u, m, uft, mft)

   118       | map_me g Minimized     (u, m, uft, mft) = (u, g m, uft, mft)

   119       | map_me g UnminimizedFT (u, m, uft, mft) = (u, m, g uft, mft)

   120       | map_me g MinimizedFT   (u, m, uft, mft) = (u, m, uft, g mft)

   122     val f' = make_re_data o f o tuple_of_re_data

   124     val (re_u', re_m', re_uft', re_mft') =

   125       map_me f' m (re_u, re_m, re_uft, re_mft)

   126   in make_data (sh, min, re_u', re_m', re_uft', re_mft', mini) end

   128 fun set_mini mini (Data {sh, min, re_u, re_m, re_uft, re_mft, ...}) =

   129   make_data (sh, min, re_u, re_m, re_uft, re_mft, mini)

   131 fun inc_max (n:int) (s,sos,m) = (s+n, sos + n*n, Int.max(m,n));

   133 val inc_sh_calls =  map_sh_data

   134   (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)

   135     => (calls + 1, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail))

   137 val inc_sh_success = map_sh_data

   138   (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)

   139     => (calls, success + 1, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail))

   141 val inc_sh_nontriv_calls =  map_sh_data

   142   (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)

   143     => (calls, success, nontriv_calls + 1, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail))

   145 val inc_sh_nontriv_success = map_sh_data

   146   (fn (calls, success, nontriv_calls, nontriv_success, lemmas,max_lems, time_isa, time_prover, time_prover_fail)

   147     => (calls, success, nontriv_calls, nontriv_success + 1, lemmas,max_lems, time_isa, time_prover, time_prover_fail))

   149 fun inc_sh_lemmas n = map_sh_data

   150   (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)

   151     => (calls,success,nontriv_calls, nontriv_success, lemmas+n,max_lems,time_isa,time_prover,time_prover_fail))

   153 fun inc_sh_max_lems n = map_sh_data

   154   (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)

   155     => (calls,success,nontriv_calls, nontriv_success, lemmas,Int.max(max_lems,n),time_isa,time_prover,time_prover_fail))

   157 fun inc_sh_time_isa t = map_sh_data

   158   (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)

   159     => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa + t,time_prover,time_prover_fail))

   161 fun inc_sh_time_prover t = map_sh_data

   162   (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)

   163     => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover + t,time_prover_fail))

   165 fun inc_sh_time_prover_fail t = map_sh_data

   166   (fn (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail)

   167     => (calls,success,nontriv_calls, nontriv_success, lemmas,max_lems,time_isa,time_prover,time_prover_fail + t))

   169 val inc_min_succs = map_min_data

   170   (fn (succs,ab_ratios) => (succs+1, ab_ratios))

   172 fun inc_min_ab_ratios r = map_min_data

   173   (fn (succs, ab_ratios) => (succs, ab_ratios+r))

   175 val inc_reconstructor_calls = map_re_data

   176   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)

   177     => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))

   179 val inc_reconstructor_success = map_re_data

   180   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)

   181     => (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))

   183 val inc_reconstructor_nontriv_calls = map_re_data

   184   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)

   185     => (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns))

   187 val inc_reconstructor_nontriv_success = map_re_data

   188   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)

   189     => (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns))

   191 val inc_reconstructor_proofs = map_re_data

   192   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)

   193     => (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns))

   195 fun inc_reconstructor_time m t = map_re_data

   196  (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)

   197   => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) m

   199 val inc_reconstructor_timeout = map_re_data

   200   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)

   201     => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns))

   203 fun inc_reconstructor_lemmas m n = map_re_data

   204   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)

   205     => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) m

   207 fun inc_reconstructor_posns m pos = map_re_data

   208   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)

   209     => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) m

   211 local

   213 val str = string_of_int

   214 val str3 = Real.fmt (StringCvt.FIX (SOME 3))

   215 fun percentage a b = string_of_int (a * 100 div b)

   216 fun time t = Real.fromInt t / 1000.0

   217 fun avg_time t n =

   218   if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0

   220 fun log_sh_data log

   221     (calls, success, nontriv_calls, nontriv_success, lemmas, max_lems, time_isa, time_prover, time_prover_fail) =

   222  (log ("Total number of sledgehammer calls: " ^ str calls);

   223   log ("Number of successful sledgehammer calls: " ^ str success);

   224   log ("Number of sledgehammer lemmas: " ^ str lemmas);

   225   log ("Max number of sledgehammer lemmas: " ^ str max_lems);

   226   log ("Success rate: " ^ percentage success calls ^ "%");

   227   log ("Total number of nontrivial sledgehammer calls: " ^ str nontriv_calls);

   228   log ("Number of successful nontrivial sledgehammer calls: " ^ str nontriv_success);

   229   log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time time_isa));

   230   log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time time_prover));

   231   log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time time_prover_fail));

   232   log ("Average time for sledgehammer calls (Isabelle): " ^

   233     str3 (avg_time time_isa calls));

   234   log ("Average time for successful sledgehammer calls (ATP): " ^

   235     str3 (avg_time time_prover success));

   236   log ("Average time for failed sledgehammer calls (ATP): " ^

   237     str3 (avg_time time_prover_fail (calls - success)))

   238   )

   241 fun str_of_pos (pos, triv) =

   242   let val str0 = string_of_int o the_default 0

   243   in

   244     str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos) ^

   245     (if triv then "[T]" else "")

   246   end

   248 fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls,

   249      re_nontriv_success, re_proofs, re_time, re_timeout,

   250     (lemmas, lems_sos, lems_max), re_posns) =

   251  (log ("Total number of " ^ tag ^ "reconstructor calls: " ^ str re_calls);

   252   log ("Number of successful " ^ tag ^ "reconstructor calls: " ^ str re_success ^

   253     " (proof: " ^ str re_proofs ^ ")");

   254   log ("Number of " ^ tag ^ "reconstructor timeouts: " ^ str re_timeout);

   255   log ("Success rate: " ^ percentage re_success sh_calls ^ "%");

   256   log ("Total number of nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_calls);

   257   log ("Number of successful nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_success ^

   258     " (proof: " ^ str re_proofs ^ ")");

   259   log ("Number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lemmas);

   260   log ("SOS of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_sos);

   261   log ("Max number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_max);

   262   log ("Total time for successful " ^ tag ^ "reconstructor calls: " ^ str3 (time re_time));

   263   log ("Average time for successful " ^ tag ^ "reconstructor calls: " ^

   264     str3 (avg_time re_time re_success));

   265   if tag=""

   266   then log ("Proved: " ^ space_implode " " (map str_of_pos re_posns))

   267   else ()

   268  )

   270 fun log_min_data log (succs, ab_ratios) =

   271   (log ("Number of successful minimizations: " ^ string_of_int succs);

   272    log ("After/before ratios: " ^ string_of_int ab_ratios)

   273   )

   275 in

   277 fun log_data id log (Data {sh, min, re_u, re_m, re_uft, re_mft, mini}) =

   278   let

   279     val ShData {calls=sh_calls, ...} = sh

   281     fun app_if (ReData {calls, ...}) f = if calls > 0 then f () else ()

   282     fun log_re tag m =

   283       log_re_data log tag sh_calls (tuple_of_re_data m)

   284     fun log_reconstructor (tag1, m1) (tag2, m2) = app_if m1 (fn () =>

   285       (log_re tag1 m1; log ""; app_if m2 (fn () => log_re tag2 m2)))

   286   in

   287     if sh_calls > 0

   288     then

   289      (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n");

   290       log_sh_data log (tuple_of_sh_data sh);

   291       log "";

   292       if not mini

   293       then log_reconstructor ("", re_u) ("fully-typed ", re_uft)

   294       else

   295         app_if re_u (fn () =>

   296          (log_reconstructor ("unminimized ", re_u) ("unminimized fully-typed ", re_uft);

   297           log "";

   298           app_if re_m (fn () =>

   299             (log_min_data log (tuple_of_min_data min); log "";

   300              log_reconstructor ("", re_m) ("fully-typed ", re_mft))))))

   301     else ()

   302   end

   304 end

   307 (* Warning: we implicitly assume single-threaded execution here! *)

   308 val data = Unsynchronized.ref ([] : (int * data) list)

   310 fun init id thy = (Unsynchronized.change data (cons (id, empty_data)); thy)

   311 fun done id ({log, ...}: Mirabelle.done_args) =

   312   AList.lookup (op =) (!data) id

   313   |> Option.map (log_data id log)

   314   |> K ()

   316 fun change_data id f = (Unsynchronized.change data (AList.map_entry (op =) id f); ())

   319 fun get_prover ctxt args =

   320   let

   321     fun default_prover_name () =

   322       hd (#provers (Sledgehammer_Isar.default_params ctxt []))

   323       handle Empty => error "No ATP available."

   324     fun get_prover name =

   325       (name, Sledgehammer_Run.get_minimizing_prover ctxt false name)

   326   in

   327     (case AList.lookup (op =) args proverK of

   328       SOME name => get_prover name

   329     | NONE => get_prover (default_prover_name ()))

   330   end

   332 type locality = Sledgehammer_Filter.locality

   334 (* hack *)

   335 fun reconstructor_from_msg args msg =

   336   (case AList.lookup (op =) args reconstructorK of

   337     SOME name => name

   338   | NONE =>

   339     if String.isSubstring "metisFT" msg then "metisFT"

   340     else if String.isSubstring "metis" msg then "metis"

   341     else "smt")

   343 local

   345 datatype sh_result =

   346   SH_OK of int * int * (string * locality) list |

   347   SH_FAIL of int * int |

   348   SH_ERROR

   350 fun run_sh prover_name prover type_sys hard_timeout timeout dir st =

   351   let

   352     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st

   353     val i = 1

   354     fun change_dir (SOME dir) =

   355         Config.put Sledgehammer_Provers.dest_dir dir

   356         #> Config.put SMT_Config.debug_files

   357           (dir ^ "/" ^ Name.desymbolize false (ATP_Problem.timestamp ()) ^ "_"

   358           ^ serial_string ())

   359       | change_dir NONE = I

   360     val st' =

   361       st |> Proof.map_context

   362                 (change_dir dir

   363                  #> Config.put Sledgehammer_Provers.measure_run_time true)

   364     val params as {type_sys, relevance_thresholds, max_relevant, ...} =

   365       Sledgehammer_Isar.default_params ctxt

   366           [("verbose", "true"),

   367            ("type_sys", type_sys),

   368            ("timeout", string_of_int timeout)]

   369     val default_max_relevant =

   370       Sledgehammer_Provers.default_max_relevant_for_prover ctxt prover_name

   371     val is_built_in_const =

   372       Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name

   373     val relevance_fudge =

   374       Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name

   375     val relevance_override = {add = [], del = [], only = false}

   376     val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i

   377     val no_dangerous_types =

   378       Sledgehammer_ATP_Translate.types_dangerous_types type_sys

   379     val time_limit =

   380       (case hard_timeout of

   381         NONE => I

   382       | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))

   383     val ({outcome, message, used_facts, run_time_in_msecs}

   384          : Sledgehammer_Provers.prover_result,

   385         time_isa) = time_limit (Mirabelle.cpu_time (fn () =>

   386       let

   387         val facts =

   388           Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types

   389               relevance_thresholds

   390               (the_default default_max_relevant max_relevant) is_built_in_const

   391               relevance_fudge relevance_override chained_ths hyp_ts concl_t

   392         val problem =

   393           {state = st', goal = goal, subgoal = i,

   394            subgoal_count = Sledgehammer_Util.subgoal_count st,

   395            facts = facts |> map Sledgehammer_Provers.Untranslated_Fact,

   396            smt_filter = NONE}

   397       in prover params (K "") problem end)) ()

   398       handle TimeLimit.TimeOut =>

   399              ({outcome = SOME ATP_Proof.TimedOut, message = "", used_facts = [],

   400                run_time_in_msecs = NONE}, ~1)

   401     val time_prover = run_time_in_msecs |> the_default ~1

   402   in

   403     case outcome of

   404       NONE => (message, SH_OK (time_isa, time_prover, used_facts))

   405     | SOME _ => (message, SH_FAIL (time_isa, time_prover))

   406   end

   407   handle ERROR msg => ("error: " ^ msg, SH_ERROR)

   409 fun thms_of_name ctxt name =

   410   let

   411     val lex = Keyword.get_lexicons

   412     val get = maps (ProofContext.get_fact ctxt o fst)

   413   in

   414     Source.of_string name

   415     |> Symbol.source

   416     |> Token.source {do_recover=SOME false} lex Position.start

   417     |> Token.source_proper

   418     |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE

   419     |> Source.exhaust

   420   end

   422 in

   424 fun run_sledgehammer trivial args reconstructor named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =

   425   let

   426     val triv_str = if trivial then "[T] " else ""

   427     val _ = change_data id inc_sh_calls

   428     val _ = if trivial then () else change_data id inc_sh_nontriv_calls

   429     val (prover_name, prover) = get_prover (Proof.context_of st) args

   430     val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"

   431     val dir = AList.lookup (op =) args keepK

   432     val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)

   433     (* always use a hard timeout, but give some slack so that the automatic

   434        minimizer has a chance to do its magic *)

   435     val hard_timeout = SOME (2 * timeout)

   436     val (msg, result) =

   437       run_sh prover_name prover type_sys hard_timeout timeout dir st

   438   in

   439     case result of

   440       SH_OK (time_isa, time_prover, names) =>

   441         let

   442           fun get_thms (_, Sledgehammer_Filter.Chained) = NONE

   443             | get_thms (name, loc) =

   444               SOME ((name, loc), thms_of_name (Proof.context_of st) name)

   445         in

   446           change_data id inc_sh_success;

   447           if trivial then () else change_data id inc_sh_nontriv_success;

   448           change_data id (inc_sh_lemmas (length names));

   449           change_data id (inc_sh_max_lems (length names));

   450           change_data id (inc_sh_time_isa time_isa);

   451           change_data id (inc_sh_time_prover time_prover);

   452           reconstructor := reconstructor_from_msg args msg;

   453           named_thms := SOME (map_filter get_thms names);

   454           log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^

   455             string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg)

   456         end

   457     | SH_FAIL (time_isa, time_prover) =>

   458         let

   459           val _ = change_data id (inc_sh_time_isa time_isa)

   460           val _ = change_data id (inc_sh_time_prover_fail time_prover)

   461         in log (sh_tag id ^ triv_str ^ "failed: " ^ msg) end

   462     | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg)

   463   end

   465 end

   467 fun run_minimize args reconstructor named_thms id

   468         ({pre=st, log, ...}: Mirabelle.run_args) =

   469   let

   470     val ctxt = Proof.context_of st

   471     val n0 = length (these (!named_thms))

   472     val (prover_name, _) = get_prover ctxt args

   473     val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"

   474     val timeout =

   475       AList.lookup (op =) args minimize_timeoutK

   476       |> Option.map (fst o read_int o raw_explode)  (* FIXME Symbol.explode (?) *)

   477       |> the_default 5

   478     val params as {explicit_apply, ...} = Sledgehammer_Isar.default_params ctxt

   479       [("provers", prover_name),

   480        ("verbose", "true"),

   481        ("type_sys", type_sys),

   482        ("timeout", string_of_int timeout)]

   483     val minimize =

   484       Sledgehammer_Minimize.minimize_facts prover_name params

   485           (SOME explicit_apply) true 1 (Sledgehammer_Util.subgoal_count st)

   486     val _ = log separator

   487   in

   488     case minimize st (these (!named_thms)) of

   489       (SOME named_thms', msg) =>

   490         (change_data id inc_min_succs;

   491          change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));

   492          if length named_thms' = n0

   493          then log (minimize_tag id ^ "already minimal")

   494          else (reconstructor := reconstructor_from_msg args msg;

   495                named_thms := SOME named_thms';

   496                log (minimize_tag id ^ "succeeded:\n" ^ msg))

   497         )

   498     | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg)

   499   end

   502 fun run_reconstructor trivial full m name reconstructor named_thms id

   503     ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =

   504   let

   505     fun do_reconstructor thms ctxt =

   506       (if !reconstructor = "sledgehammer_tac" then

   507          (fn ctxt => fn thms =>

   508             Method.insert_tac thms THEN'

   509             Sledgehammer_Tactics.sledgehammer_as_unsound_oracle_tac ctxt)

   510        else if !reconstructor = "smt" then

   511          SMT_Solver.smt_tac

   512        else if full orelse !reconstructor = "metisFT" then

   513          Metis_Tactics.metisFT_tac

   514        else

   515          Metis_Tactics.metis_tac) ctxt thms

   516     fun apply_reconstructor thms =

   517       Mirabelle.can_apply timeout (do_reconstructor thms) st

   519     fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"

   520       | with_time (true, t) = (change_data id (inc_reconstructor_success m);

   521           if trivial then ()

   522           else change_data id (inc_reconstructor_nontriv_success m);

   523           change_data id (inc_reconstructor_lemmas m (length named_thms));

   524           change_data id (inc_reconstructor_time m t);

   525           change_data id (inc_reconstructor_posns m (pos, trivial));

   526           if name = "proof" then change_data id (inc_reconstructor_proofs m)

   527           else ();

   528           "succeeded (" ^ string_of_int t ^ ")")

   529     fun timed_reconstructor thms =

   530       (with_time (Mirabelle.cpu_time apply_reconstructor thms), true)

   531       handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m);

   532                ("timeout", false))

   533            | ERROR msg => ("error: " ^ msg, false)

   535     val _ = log separator

   536     val _ = change_data id (inc_reconstructor_calls m)

   537     val _ = if trivial then ()

   538             else change_data id (inc_reconstructor_nontriv_calls m)

   539   in

   540     maps snd named_thms

   541     |> timed_reconstructor

   542     |>> log o prefix (reconstructor_tag reconstructor id)

   543     |> snd

   544   end

   546 val try_timeout = seconds 5.0

   548 fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) =

   549   let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in

   550     if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal

   551     then () else

   552     let

   553       val reconstructor = Unsynchronized.ref ""

   554       val named_thms =

   555         Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)

   556       val minimize = AList.defined (op =) args minimizeK

   557       val metis_ft = AList.defined (op =) args metis_ftK

   558       val trivial = Try.invoke_try (SOME try_timeout) pre

   559         handle TimeLimit.TimeOut => false

   560       fun apply_reconstructor m1 m2 =

   561         if metis_ft

   562         then

   563           if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false

   564               (run_reconstructor trivial false m1 name reconstructor

   565                    (these (!named_thms))) id st)

   566           then

   567             (Mirabelle.catch_result (reconstructor_tag reconstructor) false

   568               (run_reconstructor trivial true m2 name reconstructor

   569                    (these (!named_thms))) id st; ())

   570           else ()

   571         else

   572           (Mirabelle.catch_result (reconstructor_tag reconstructor) false

   573             (run_reconstructor trivial false m1 name reconstructor

   574                  (these (!named_thms))) id st; ())

   575     in

   576       change_data id (set_mini minimize);

   577       Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor

   578                                                named_thms) id st;

   579       if is_some (!named_thms)

   580       then

   581        (apply_reconstructor Unminimized UnminimizedFT;

   582         if minimize andalso not (null (these (!named_thms)))

   583         then

   584          (Mirabelle.catch minimize_tag

   585               (run_minimize args reconstructor named_thms) id st;

   586           apply_reconstructor Minimized MinimizedFT)

   587         else ())

   588       else ()

   589     end

   590   end

   592 fun invoke args =

   593   let

   594     val _ = Sledgehammer_Isar.full_types := AList.defined (op =) args full_typesK

   595   in Mirabelle.register (init, sledgehammer_action args, done) end

   597 end

author	blanchet
	Wed, 09 Feb 2011 17:18:58 +0100
changeset 42613	11e862c68b40
parent 42612	839d1488045f
child 42623	949eaf045e00
permissions	-rw-r--r--