# HG changeset patch
# User blanchet
# Date 1285927267 -7200
# Node ID 608b108ec9792c6e1fe3270002f6bc05bb7e659c
# Parent  c986fc8de255cd8eaede46b07377c3815577349d
compute quantifier dependency graph in new skolemizer

diff -r c986fc8de255 -r 608b108ec979 src/HOL/Tools/Sledgehammer/meson_clausify.ML
--- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Fri Oct 01 10:58:01 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML	Fri Oct 01 12:01:07 2010 +0200
@@ -12,7 +12,7 @@
   val introduce_combinators_in_cterm : cterm -> thm
   val introduce_combinators_in_theorem : thm -> thm
   val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
-  val cluster_for_zapped_var_name : string -> int * bool
+  val cluster_of_zapped_var_name : string -> (int * int) * bool
   val cnf_axiom :
     theory -> bool -> int -> thm -> (thm * term) option * thm list
   val meson_general_tac : Proof.context -> thm list -> int -> tactic
@@ -22,8 +22,9 @@
 structure Meson_Clausify : MESON_CLAUSIFY =
 struct
 
-val new_skolem_var_prefix = "SK?"
-val new_nonskolem_var_prefix = "V?"
+(* the extra "?" helps prevent clashes *)
+val new_skolem_var_prefix = "?SK"
+val new_nonskolem_var_prefix = "?V"
 
 (**** Transformation of Elimination Rules into First-Order Formulas****)
 
@@ -231,10 +232,10 @@
 
 fun zapped_var_name ax_no (cluster_no, skolem) s =
   (if skolem then new_skolem_var_prefix else new_nonskolem_var_prefix) ^
-  string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^ s
+  "_" ^ string_of_int ax_no ^ "_" ^ string_of_int cluster_no ^ "_" ^ s
 
-fun cluster_for_zapped_var_name s =
-  (nth (space_explode "_" s) 1 |> Int.fromString |> the,
+fun cluster_of_zapped_var_name s =
+  ((1, 2) |> pairself (the o Int.fromString o nth (space_explode "_" s)),
    String.isPrefix new_skolem_var_prefix s)
 
 fun zap_quantifiers ax_no =
diff -r c986fc8de255 -r 608b108ec979 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Oct 01 10:58:01 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Oct 01 12:01:07 2010 +0200
@@ -24,6 +24,9 @@
 open Metis_Translate
 open Metis_Reconstruct
 
+structure Int_Pair_Graph =
+  Graph(type key = int * int val ord = prod_ord int_ord int_ord)
+
 fun trace_msg msg = if !trace then tracing (msg ()) else ()
 
 val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true)
@@ -121,6 +124,8 @@
   in th |> Thm.instantiate (cinstT, []) |> Thm.instantiate ([], cinst) end
   handle Empty => th (* ### FIXME *)
 
+val cluster_ord = prod_ord (prod_ord int_ord int_ord) bool_ord
+
 (* Attempts to derive the theorem "False" from a theorem of the form
    "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
    specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
@@ -137,8 +142,8 @@
             Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
           val tsubst =
             tenv |> Vartab.dest
-                 |> sort (prod_ord int_ord bool_ord
-                          o pairself (Meson_Clausify.cluster_for_zapped_var_name
+                 |> sort (cluster_ord
+                          o pairself (Meson_Clausify.cluster_of_zapped_var_name
                                       o fst o fst))
                  |> map (Meson.term_pair_of
                          #> pairself (Envir.subst_term_types tyenv))
@@ -151,8 +156,36 @@
           end
         | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
                            [prem])
+      fun cluster_of_var_name skolem s =
+        let val (jj, skolem') = Meson_Clausify.cluster_of_zapped_var_name s in
+          if skolem' = skolem then SOME jj else NONE
+        end
+      fun clusters_in_term skolem t =
+        Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
+      fun deps_for_term_subst (var, t) =
+        case clusters_in_term false var of
+          [] => NONE
+        | [(ax_no, cluster_no)] =>
+          SOME ((ax_no, cluster_no),
+                clusters_in_term true t
+                |> cluster_no > 0 ? cons (ax_no, cluster_no - 1))
+        | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
       val prems = Logic.strip_imp_prems prems_imp_false_prop
       val substs = map2 subst_info_for_prem (0 upto length prems - 1) prems
+      val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs
+      val clusters = maps (op ::) depss
+      val ordered_clusters =
+        Int_Pair_Graph.empty
+        |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
+        |> fold Int_Pair_Graph.add_deps_acyclic depss
+        |> Int_Pair_Graph.topological_order
+        handle Int_Pair_Graph.CYCLES _ =>
+               error "Cannot replay Metis proof in Isabelle without axiom of \
+                     \choice."
+(*
+      val _ = tracing ("SUBSTS: " ^ PolyML.makestring substs)
+      val _ = tracing ("ORDERED: " ^ PolyML.makestring ordered_clusters)
+*)
     in
       Goal.prove ctxt [] [] @{prop False}
           (K (cut_rules_tac (map fst axioms) 1