use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
authorblanchet
Thu Apr 14 11:24:04 2011 +0200 (2011-04-14)
changeset 423390e5d1e5e1177
parent 42338 802f2fe7a0c9
child 42340 4e4f0665e5be
use the list of actually used axioms to (correctly) precompute the "outer params", not all axioms
src/HOL/Tools/Metis/metis_reconstruct.ML
     1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:04 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Apr 14 11:24:04 2011 +0200
     1.3 @@ -792,28 +792,38 @@
     1.4          handle Int_Pair_Graph.CYCLES _ =>
     1.5                 error "Cannot replay Metis proof in Isabelle without \
     1.6                       \\"Hilbert_Choice\"."
     1.7 -      val outer_param_names =
     1.8 -        [] |> fold (Term.add_var_names o snd) (map_filter I axioms)
     1.9 -           |> filter (Meson_Clausify.is_zapped_var_name o fst)
    1.10 -           |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
    1.11 -           |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
    1.12 -                         cluster_no = 0 andalso skolem)
    1.13 -           |> sort shuffle_ord |> map (fst o snd)
    1.14        val ax_counts =
    1.15          Int_Tysubst_Table.empty
    1.16          |> fold (fn (ax_no, (_, (tysubst, _))) =>
    1.17                      Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
    1.18                                                    (Integer.add 1)) substs
    1.19          |> Int_Tysubst_Table.dest
    1.20 +      val needed_axiom_props =
    1.21 +        0 upto length axioms - 1 ~~ axioms
    1.22 +        |> map_filter (fn (_, NONE) => NONE
    1.23 +                        | (ax_no, SOME (_, t)) =>
    1.24 +                          if exists (fn ((ax_no', _), n) =>
    1.25 +                                        ax_no' = ax_no andalso n > 0)
    1.26 +                                    ax_counts then
    1.27 +                            SOME t
    1.28 +                          else
    1.29 +                            NONE)
    1.30 +      val outer_param_names =
    1.31 +        [] |> fold Term.add_var_names needed_axiom_props
    1.32 +           |> filter (Meson_Clausify.is_zapped_var_name o fst)
    1.33 +           |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
    1.34 +           |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
    1.35 +                         cluster_no = 0 andalso skolem)
    1.36 +           |> sort shuffle_ord |> map (fst o snd)
    1.37  (* for debugging only:
    1.38        fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
    1.39          "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
    1.40          "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
    1.41          commas (map ((fn (s, t) => s ^ " |-> " ^ t)
    1.42                       o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
    1.43 -      val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)
    1.44        val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
    1.45        val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
    1.46 +      val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)
    1.47        val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
    1.48                         cat_lines (map string_for_subst_info substs))
    1.49  *)