simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
authorblanchet
Sun Feb 02 20:53:51 2014 +0100 (2014-02-02)
changeset 5524412e1a5d8ee48
parent 55243 66709d41601e
child 55245 c402981f74c1
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.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 @@ -110,16 +110,16 @@
     1.4  type isar_params =
     1.5    bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
     1.6  
     1.7 -val arith_methodss =
     1.8 -  [[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
     1.9 -    Algebra_Method], [Metis_Method], [Meson_Method]]
    1.10 -val datatype_methodss = [[Simp_Method], [Simp_Size_Method]]
    1.11 -val metislike_methodss =
    1.12 -  [[Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
    1.13 -    Force_Method, Algebra_Method], [Meson_Method]]
    1.14 -val rewrite_methodss =
    1.15 -  [[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method], [Meson_Method]]
    1.16 -val skolem_methodss = [[Metis_Method, Blast_Method], [Meson_Method]]
    1.17 +val arith_methods =
    1.18 +  [Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
    1.19 +   Algebra_Method, Metis_Method, Meson_Method]
    1.20 +val datatype_methods = [Simp_Method, Simp_Size_Method]
    1.21 +val metislike_methods =
    1.22 +  [Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
    1.23 +   Force_Method, Algebra_Method, Meson_Method]
    1.24 +val rewrite_methods =
    1.25 +  [Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method, Meson_Method]
    1.26 +val skolem_methods = [Metis_Method, Blast_Method, Meson_Method]
    1.27  
    1.28  fun isar_proof_text ctxt debug isar_proofs isar_params
    1.29      (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
    1.30 @@ -158,12 +158,12 @@
    1.31            map_filter (get_role (curry (op =) Lemma)) atp_proof
    1.32            |> map (fn ((l, t), rule) =>
    1.33              let
    1.34 -              val (skos, methss) =
    1.35 -                if is_skolemize_rule rule then (skolems_of t, skolem_methodss)
    1.36 -                else if is_arith_rule rule then ([], arith_methodss)
    1.37 -                else ([], rewrite_methodss)
    1.38 +              val (skos, meths) =
    1.39 +                if is_skolemize_rule rule then (skolems_of t, skolem_methods)
    1.40 +                else if is_arith_rule rule then ([], arith_methods)
    1.41 +                else ([], rewrite_methods)
    1.42              in
    1.43 -              Prove ([], skos, l, t, [], (([], []), methss))
    1.44 +              Prove ([], skos, l, t, [], (([], []), meths))
    1.45              end)
    1.46  
    1.47          val bot = atp_proof |> List.last |> #1
    1.48 @@ -212,7 +212,7 @@
    1.49              accum
    1.50              |> (if tainted = [] then
    1.51                    cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
    1.52 -                               ((the_list predecessor, []), metislike_methodss)))
    1.53 +                               ((the_list predecessor, []), metislike_methods)))
    1.54                  else
    1.55                    I)
    1.56              |> rev
    1.57 @@ -227,18 +227,18 @@
    1.58                fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs
    1.59  
    1.60                val deps = fold add_fact_of_dependencies gamma no_facts
    1.61 -              val methss =
    1.62 -                if is_arith_rule rule then arith_methodss
    1.63 -                else if is_datatype_rule rule then datatype_methodss
    1.64 -                else metislike_methodss
    1.65 -              val by = (deps, methss)
    1.66 +              val meths =
    1.67 +                if is_arith_rule rule then arith_methods
    1.68 +                else if is_datatype_rule rule then datatype_methods
    1.69 +                else metislike_methods
    1.70 +              val by = (deps, meths)
    1.71              in
    1.72                if is_clause_tainted c then
    1.73                  (case gamma of
    1.74                    [g] =>
    1.75                    if skolem andalso is_clause_tainted g then
    1.76                      let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in
    1.77 -                      isar_steps outer (SOME l) [prove [subproof] (no_facts, skolem_methodss)] infs
    1.78 +                      isar_steps outer (SOME l) [prove [subproof] (no_facts, skolem_methods)] infs
    1.79                      end
    1.80                    else
    1.81                      do_rest l (prove [] by)
    1.82 @@ -256,7 +256,7 @@
    1.83                val step =
    1.84                  Prove (maybe_show outer c [], [], l, t,
    1.85                    map isar_case (filter_out (null o snd) cases),
    1.86 -                  ((the_list predecessor, []), metislike_methodss))
    1.87 +                  ((the_list predecessor, []), metislike_methods))
    1.88              in
    1.89                isar_steps outer (SOME l) (step :: accum) infs
    1.90              end
    1.91 @@ -286,7 +286,7 @@
    1.92  
    1.93          fun str_of_meth l meth =
    1.94            string_of_proof_method meth ^ " " ^ str_of_preplay_outcome (preplay_outcome l meth)
    1.95 -        fun comment_of l = map (map (str_of_meth l)) #> map commas #> space_implode "; "
    1.96 +        fun comment_of l = map (str_of_meth l) #> commas
    1.97  
    1.98          fun trace_isar_proof label proof =
    1.99            if trace then
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sun Feb 02 20:53:51 2014 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Sun Feb 02 20:53:51 2014 +0100
     2.3 @@ -79,15 +79,14 @@
     2.4      | _ => raise Fail "Sledgehammer_Isar_Compress: update_steps")
     2.5    end
     2.6  
     2.7 -(* Tries merging the first step into the second step.
     2.8 -   FIXME: Arbitrarily picks the second step's method. *)
     2.9 -fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), _)))
    2.10 -      (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), methss2))) =
    2.11 +(* Tries merging the first step into the second step. *)
    2.12 +fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), meths1)))
    2.13 +      (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), meths2))) =
    2.14      let
    2.15        val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
    2.16        val gfs = union (op =) gfs1 gfs2
    2.17      in
    2.18 -      SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), methss2)))
    2.19 +      SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meths2)))
    2.20      end
    2.21    | try_merge _ _ = NONE
    2.22  
    2.23 @@ -136,16 +135,16 @@
    2.24          end
    2.25  
    2.26        (* elimination of trivial, one-step subproofs *)
    2.27 -      fun elim_subproofs' time qs fix l t lfs gfs (methss as (meth :: _) :: _) subs nontriv_subs =
    2.28 +      fun elim_subproofs' time qs fix l t lfs gfs (meths as meth :: _) subs nontriv_subs =
    2.29          if null subs orelse not (compress_further ()) then
    2.30            (set_preplay_outcome l meth (Played time);
    2.31 -           Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), methss)))
    2.32 +           Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meths)))
    2.33          else
    2.34            (case subs of
    2.35              (sub as Proof (_, assms, sub_steps)) :: subs =>
    2.36              (let
    2.37                (* trivial subproofs have exactly one "Prove" step *)
    2.38 -              val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), (meth' :: _) :: _))) =
    2.39 +              val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), meth' :: _))) =
    2.40                  try the_single sub_steps
    2.41  
    2.42                (* only touch proofs that can be preplayed sucessfully *)
    2.43 @@ -155,7 +154,7 @@
    2.44                val subs'' = subs @ nontriv_subs
    2.45                val lfs'' = union (op =) lfs (subtract (op =) (map fst assms) lfs')
    2.46                val gfs'' = union (op =) gfs' gfs
    2.47 -              val by = ((lfs'', gfs''), methss(*FIXME*))
    2.48 +              val by = ((lfs'', gfs''), meths(*FIXME*))
    2.49                val step'' = Prove (qs, fix, l, t, subs'', by)
    2.50  
    2.51                (* check if the modified step can be preplayed fast enough *)
    2.52 @@ -164,20 +163,20 @@
    2.53              in
    2.54                decrement_step_count (); (* l' successfully eliminated! *)
    2.55                map (replace_successor l' [l]) lfs';
    2.56 -              elim_subproofs' time'' qs fix l t lfs'' gfs'' methss subs nontriv_subs
    2.57 +              elim_subproofs' time'' qs fix l t lfs'' gfs'' meths subs nontriv_subs
    2.58              end
    2.59              handle Bind =>
    2.60 -            elim_subproofs' time qs fix l t lfs gfs methss subs (sub :: nontriv_subs))
    2.61 +            elim_subproofs' time qs fix l t lfs gfs meths subs (sub :: nontriv_subs))
    2.62            | _ => raise Fail "Sledgehammer_Isar_Compress: elim_subproofs'")
    2.63  
    2.64        fun elim_subproofs (step as Let _) = step
    2.65          | elim_subproofs (step as Prove (qs, fix, l, t, subproofs,
    2.66 -            ((lfs, gfs), methss as (meth :: _) :: _))) =
    2.67 +            ((lfs, gfs), meths as meth :: _))) =
    2.68            if subproofs = [] then
    2.69              step
    2.70            else
    2.71              (case Lazy.force (preplay_outcome l meth) of
    2.72 -              Played time => elim_subproofs' time qs fix l t lfs gfs methss subproofs []
    2.73 +              Played time => elim_subproofs' time qs fix l t lfs gfs meths subproofs []
    2.74              | _ => step)
    2.75  
    2.76        (** top_level compression: eliminate steps by merging them into their successors **)
    2.77 @@ -211,11 +210,10 @@
    2.78  
    2.79            fun try_eliminate (i, l, _) succ_lbls steps =
    2.80              let
    2.81 -              val ((cand as Prove (_, _, l, _, _, ((lfs, _), (meth :: _) :: _))) :: steps') =
    2.82 -                drop i steps
    2.83 +              val ((cand as Prove (_, _, l, _, _, ((lfs, _), meth :: _))) :: steps') = drop i steps
    2.84  
    2.85                val succs = collect_successors steps' succ_lbls
    2.86 -              val succ_meths = map (hd o hd o snd o the o byline_of_isar_step) succs
    2.87 +              val succ_meths = map (hd o snd o the o byline_of_isar_step) succs
    2.88  
    2.89                (* only touch steps that can be preplayed successfully *)
    2.90                val Played time = Lazy.force (preplay_outcome l meth)
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Sun Feb 02 20:53:51 2014 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Sun Feb 02 20:53:51 2014 +0100
     3.3 @@ -28,11 +28,11 @@
     3.4  fun minimize_isar_step_dependencies (_ : isar_preplay_data) (step as Let _) = step
     3.5    | minimize_isar_step_dependencies
     3.6        {reset_preplay_outcomes, set_preplay_outcome, preplay_outcome, preplay_quietly, ...}
     3.7 -      (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss as (meth :: _) :: _))) =
     3.8 +      (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths as meth :: _))) =
     3.9      (case Lazy.force (preplay_outcome l meth) of
    3.10        Played time =>
    3.11        let
    3.12 -        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))
    3.13 +        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))
    3.14          val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
    3.15  
    3.16          fun minimize_facts _ time min_facts [] = (time, min_facts)
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sun Feb 02 20:53:51 2014 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Sun Feb 02 20:53:51 2014 +0100
     4.3 @@ -210,15 +210,15 @@
     4.4               Play_Failed)
     4.5  
     4.6        (* preplay steps treating exceptions like timeouts *)
     4.7 -      fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, (meth :: _) :: _))) =
     4.8 +      fun preplay_quietly timeout (step as Prove (_, _, _, _, _, (_, meth :: _))) =
     4.9            preplay true timeout meth step
    4.10          | preplay_quietly _ _ = Played Time.zeroTime
    4.11  
    4.12        val preplay_tab = Unsynchronized.ref Canonical_Label_Tab.empty
    4.13  
    4.14 -      fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, methss))) =
    4.15 -          preplay_tab := Canonical_Label_Tab.update (l, maps (map (fn meth =>
    4.16 -              (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step)))) methss)
    4.17 +      fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) =
    4.18 +          preplay_tab := Canonical_Label_Tab.update (l, map (fn meth =>
    4.19 +              (meth, Lazy.lazy (fn () => preplay false preplay_timeout meth step))) meths)
    4.20              (!preplay_tab)
    4.21          | reset_preplay_outcomes _ = ()
    4.22  
    4.23 @@ -236,7 +236,7 @@
    4.24  
    4.25        val _ = fold_isar_steps (K o reset_preplay_outcomes) (steps_of_proof proof) ()
    4.26  
    4.27 -      fun result_of_step (Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
    4.28 +      fun result_of_step (Prove (_, _, l, _, _, (_, meth :: _))) =
    4.29            Lazy.force (preplay_outcome l meth)
    4.30          | result_of_step _ = Played Time.zeroTime
    4.31  
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Sun Feb 02 20:53:51 2014 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Sun Feb 02 20:53:51 2014 +0100
     5.3 @@ -22,7 +22,7 @@
     5.4    and isar_step =
     5.5      Let of term * term |
     5.6      Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
     5.7 -      (facts * proof_method list list)
     5.8 +      (facts * proof_method list)
     5.9  
    5.10    val no_label : label
    5.11    val no_facts : facts
    5.12 @@ -35,7 +35,7 @@
    5.13    val steps_of_proof : isar_proof -> isar_step list
    5.14  
    5.15    val label_of_isar_step : isar_step -> label option
    5.16 -  val byline_of_isar_step : isar_step -> (facts * proof_method list list) option
    5.17 +  val byline_of_isar_step : isar_step -> (facts * proof_method list) option
    5.18  
    5.19    val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
    5.20    val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
    5.21 @@ -51,7 +51,7 @@
    5.22    val relabel_isar_proof_finally : isar_proof -> isar_proof
    5.23  
    5.24    val string_of_isar_proof : Proof.context -> string -> string -> int -> int ->
    5.25 -    (label -> proof_method list list -> string) -> isar_proof -> string
    5.26 +    (label -> proof_method list -> string) -> isar_proof -> string
    5.27  end;
    5.28  
    5.29  structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF =
    5.30 @@ -79,7 +79,7 @@
    5.31  and isar_step =
    5.32    Let of term * term |
    5.33    Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
    5.34 -    (facts * proof_method list list)
    5.35 +    (facts * proof_method list)
    5.36  
    5.37  val no_label = ("", ~1)
    5.38  val no_facts = ([],[])
    5.39 @@ -136,9 +136,9 @@
    5.40  fun chain_qs_lfs NONE lfs = ([], lfs)
    5.41    | chain_qs_lfs (SOME l0) lfs =
    5.42      if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
    5.43 -fun chain_isar_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))) =
    5.44 +fun chain_isar_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))) =
    5.45      let val (qs', lfs) = chain_qs_lfs lbl lfs in
    5.46 -      Prove (qs' @ qs, xs, l, t, map chain_isar_proof subproofs, ((lfs, gfs), methss))
    5.47 +      Prove (qs' @ qs, xs, l, t, map chain_isar_proof subproofs, ((lfs, gfs), meths))
    5.48      end
    5.49    | chain_isar_step _ step = step
    5.50  and chain_isar_steps _ [] = []
    5.51 @@ -340,7 +340,7 @@
    5.52          add_str (of_indent ind ^ "let ")
    5.53          #> add_term t1 #> add_str " = " #> add_term t2
    5.54          #> add_str "\n"
    5.55 -      | add_step ind (Prove (qs, xs, l, t, subproofs, ((ls, ss), methss as (meth :: _) :: _))) =
    5.56 +      | add_step ind (Prove (qs, xs, l, t, subproofs, ((ls, ss), meths as meth :: _))) =
    5.57          add_step_pre ind qs subproofs
    5.58          #> (case xs of
    5.59               [] => add_str (of_have qs (length subproofs) ^ " ")
    5.60 @@ -350,7 +350,7 @@
    5.61          #> add_term t
    5.62          #> add_str (" " ^
    5.63               of_method (sort_distinct label_ord ls) (sort_distinct string_ord ss) meth ^
    5.64 -             (case comment_of l methss of
    5.65 +             (case comment_of l meths of
    5.66                 "" => ""
    5.67               | comment => " (* " ^ comment ^ " *)") ^ "\n")
    5.68      and add_steps ind = fold (add_step ind)
    5.69 @@ -360,7 +360,7 @@
    5.70      (* One-step Metis proofs are pointless; better use the one-liner directly. *)
    5.71      (case proof of
    5.72        Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *)
    5.73 -    | Proof ([], [], [Prove (_, [], _, _, [], (_, (Metis_Method :: _) :: _))]) => ""
    5.74 +    | Proof ([], [], [Prove (_, [], _, _, [], (_, Metis_Method :: _))]) => ""
    5.75      | _ =>
    5.76        (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
    5.77        of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Sun Feb 02 20:53:51 2014 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML	Sun Feb 02 20:53:51 2014 +0100
     6.3 @@ -22,8 +22,8 @@
     6.4  open Sledgehammer_Isar_Proof
     6.5  open Sledgehammer_Isar_Preplay
     6.6  
     6.7 -fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, methss))) =
     6.8 -    map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [[meth]]))) (tl (flat methss))
     6.9 +fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, meths))) =
    6.10 +    map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [meth]))) (tl meths)
    6.11    | variants_of_step _ = raise Fail "Sledgehammer_Isar_Try0: variants_of_step"
    6.12  
    6.13  val slack = seconds 0.05
    6.14 @@ -31,7 +31,7 @@
    6.15  fun try0_step _ _ (step as Let _) = step
    6.16    | try0_step preplay_timeout
    6.17        ({preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : isar_preplay_data)
    6.18 -      (step as Prove (_, _, l, _, _, (_, (meth :: _) :: _))) =
    6.19 +      (step as Prove (_, _, l, _, _, (_, meth :: _))) =
    6.20      let
    6.21        val timeout =
    6.22          (case Lazy.force (preplay_outcome l meth) of
    6.23 @@ -45,7 +45,7 @@
    6.24      in
    6.25        (* FIXME: create variant after success *)
    6.26        (case Par_List.get_some try_variant (variants_of_step step) of
    6.27 -        SOME (step' as Prove (_, _, _, _, _, (_, (meth' :: _) :: _)), result) =>
    6.28 +        SOME (step' as Prove (_, _, _, _, _, (_, meth' :: _)), result) =>
    6.29          (set_preplay_outcome l meth' result; step')
    6.30        | NONE => step)
    6.31      end