unform treatment of preplay_timeout = 0 and > 0
authorblanchet
Sun Feb 02 20:53:51 2014 +0100 (2014-02-02)
changeset 55253cfd276a7dbeb
parent 55252 0dc4993b4f56
child 55254 2bc951e6761a
unform treatment of preplay_timeout = 0 and > 0
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Feb 02 20:53:51 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Feb 02 20:53:51 2014 +0100
     1.3 @@ -137,6 +137,7 @@
     1.4  
     1.5          val do_preplay = preplay_timeout <> Time.zeroTime
     1.6          val try0_isar = try0_isar andalso do_preplay
     1.7 +        val compress_isar = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress_isar
     1.8  
     1.9          val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
    1.10          fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
    1.11 @@ -279,8 +280,8 @@
    1.12            |> relabel_isar_proof_canonically
    1.13  
    1.14          val preplay_data as {preplay_outcome, overall_preplay_outcome, ...} =
    1.15 -          preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay
    1.16 -            preplay_timeout isar_proof
    1.17 +          preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans preplay_timeout
    1.18 +            isar_proof
    1.19  
    1.20          fun str_of_preplay_outcome outcome =
    1.21            if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
    1.22 @@ -299,8 +300,7 @@
    1.23          val (play_outcome, isar_proof) =
    1.24            isar_proof
    1.25            |> tap (trace_isar_proof "Original")
    1.26 -          |> compress_isar_proof (if isar_proofs = SOME true then compress_isar else 1000.0)
    1.27 -               preplay_data
    1.28 +          |> compress_isar_proof compress_isar preplay_data
    1.29            |> tap (trace_isar_proof "Compressed")
    1.30            |> try0_isar ? try0_isar_proof preplay_timeout preplay_data
    1.31            |> tap (trace_isar_proof "Tried0")
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sun Feb 02 20:53:51 2014 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sun Feb 02 20:53:51 2014 +0100
     2.3 @@ -21,7 +21,7 @@
     2.4       preplay_quietly: Time.time -> isar_step -> play_outcome,
     2.5       overall_preplay_outcome: isar_proof -> play_outcome}
     2.6  
     2.7 -  val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> bool -> Time.time ->
     2.8 +  val preplay_data_of_isar_proof : bool -> Proof.context -> string -> string -> Time.time ->
     2.9      isar_proof -> isar_preplay_data
    2.10  end;
    2.11  
    2.12 @@ -172,67 +172,60 @@
    2.13  
    2.14     Precondition: The proof must be labeled canonically; cf.
    2.15     "Slegehammer_Isar_Proof.relabel_isar_proof_canonically". *)
    2.16 -fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
    2.17 -  if not do_preplay then
    2.18 -    (* the "dont_preplay" option pretends that everything works just fine *)
    2.19 -    {set_preplay_outcomes = K (K ()),
    2.20 -     preplay_outcome = K (K (Lazy.value (Played Time.zeroTime))),
    2.21 -     preplay_quietly = K (K (Played Time.zeroTime)),
    2.22 -     overall_preplay_outcome = K (Played Time.zeroTime)} : isar_preplay_data
    2.23 -  else
    2.24 -    let
    2.25 -      val ctxt = enrich_context_with_local_facts proof ctxt
    2.26 +fun preplay_data_of_isar_proof debug ctxt type_enc lam_trans preplay_timeout proof =
    2.27 +  let
    2.28 +    val ctxt = enrich_context_with_local_facts proof ctxt
    2.29  
    2.30 -      fun preplay quietly timeout meth step =
    2.31 -        preplay_raw debug type_enc lam_trans ctxt timeout meth step
    2.32 -        handle exn =>
    2.33 -          if Exn.is_interrupt exn then
    2.34 -            reraise exn
    2.35 -          else
    2.36 -            (if not quietly andalso debug then
    2.37 -               warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n " ^ @{make_string} exn)
    2.38 -             else
    2.39 -               ();
    2.40 -             Play_Failed)
    2.41 +    fun preplay quietly timeout meth step =
    2.42 +      preplay_raw debug type_enc lam_trans ctxt timeout meth step
    2.43 +      handle exn =>
    2.44 +        if Exn.is_interrupt exn then
    2.45 +          reraise exn
    2.46 +        else
    2.47 +          (if not quietly andalso debug then
    2.48 +             warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n " ^ @{make_string} exn)
    2.49 +           else
    2.50 +             ();
    2.51 +           Play_Failed)
    2.52  
    2.53 -      (* preplay steps treating exceptions like timeouts *)
    2.54 -      fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, meth :: _))) =
    2.55 -          preplay true timeout meth step
    2.56 -        | preplay_quietly _ _ = Played Time.zeroTime
    2.57 +    (* preplay steps treating exceptions like timeouts *)
    2.58 +    fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, meth :: _))) =
    2.59 +        preplay true timeout meth step
    2.60 +      | preplay_quietly _ _ = Played Time.zeroTime
    2.61  
    2.62 -      val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty
    2.63 +    val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty
    2.64 +
    2.65 +    fun set_preplay_outcomes l meths_outcomes =
    2.66 +      preplay_tab := Canonical_Label_Tab.map_entry l (fold (AList.update (op =)) meths_outcomes)
    2.67 +        (!preplay_tab)
    2.68  
    2.69 -      fun set_preplay_outcomes l meths_outcomes =
    2.70 -        preplay_tab := Canonical_Label_Tab.map_entry l (fold (AList.update (op =)) meths_outcomes)
    2.71 -          (!preplay_tab)
    2.72 +    fun preplay_outcome l meth =
    2.73 +      (case Canonical_Label_Tab.lookup (!preplay_tab) l of
    2.74 +        SOME meths_outcomes =>
    2.75 +        (case AList.lookup (op =) meths_outcomes meth of
    2.76 +          SOME outcome => outcome
    2.77 +        | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
    2.78 +      | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
    2.79  
    2.80 -      fun preplay_outcome l meth =
    2.81 -        (case Canonical_Label_Tab.lookup (!preplay_tab) l of
    2.82 -          SOME meths_outcomes =>
    2.83 -          (case AList.lookup (op =) meths_outcomes meth of
    2.84 -            SOME outcome => outcome
    2.85 -          | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing method")
    2.86 -        | NONE => raise Fail "Sledgehammer_Isar_Preplay: missing label")
    2.87 -
    2.88 -      fun result_of_step (Prove (_, _, l, _, _, (_, meth :: _))) =
    2.89 -          Lazy.force (preplay_outcome l meth)
    2.90 -        | result_of_step _ = Played Time.zeroTime
    2.91 +    fun result_of_step (Prove (_, _, l, _, _, (_, meth :: _))) =
    2.92 +        Lazy.force (preplay_outcome l meth)
    2.93 +      | result_of_step _ = Played Time.zeroTime
    2.94  
    2.95 -      fun overall_preplay_outcome (Proof (_, _, steps)) =
    2.96 -        fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
    2.97 +    fun overall_preplay_outcome (Proof (_, _, steps)) =
    2.98 +      fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
    2.99  
   2.100 -      fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
   2.101 -          preplay_tab := Canonical_Label_Tab.update (l, map (fn meth =>
   2.102 -              (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step))) meths)
   2.103 -            (!preplay_tab)
   2.104 -        | reset_preplay_outcomes _ = ()
   2.105 +    fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
   2.106 +        preplay_tab := Canonical_Label_Tab.update (l, map (fn meth =>
   2.107 +            (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step))) meths)
   2.108 +          (!preplay_tab)
   2.109 +      | reset_preplay_outcomes _ = ()
   2.110  
   2.111 -      val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
   2.112 -    in
   2.113 -      {set_preplay_outcomes = set_preplay_outcomes,
   2.114 -       preplay_outcome = preplay_outcome,
   2.115 -       preplay_quietly = preplay_quietly,
   2.116 -       overall_preplay_outcome = overall_preplay_outcome}
   2.117 -    end
   2.118 +    val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
   2.119 +  in
   2.120 +    {set_preplay_outcomes = set_preplay_outcomes,
   2.121 +     preplay_outcome = preplay_outcome,
   2.122 +     preplay_quietly = preplay_quietly,
   2.123 +     overall_preplay_outcome = overall_preplay_outcome}
   2.124 +  end
   2.125  
   2.126  end;