# HG changeset patch
# User blanchet
# Date 1369565797 -7200
# Node ID 41c885784e04e14ff52ed82cd0e8ec86ed8bdb44
# Parent  32b1dbda331c2a286b0c91838e81e6150ff4faab
handle lambda-lifted problems in Isar construction code

diff -r 32b1dbda331c -r 41c885784e04 src/HOL/Tools/Metis/metis_generate.ML
--- a/src/HOL/Tools/Metis/metis_generate.ML	Sun May 26 11:56:55 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Sun May 26 12:56:37 2013 +0200
@@ -111,14 +111,14 @@
                    t
                | t => t)
 
-fun reveal_lam_lifted lambdas =
+fun reveal_lam_lifted lifted =
   map_aterms (fn t as Const (s, _) =>
                  if String.isPrefix lam_lifted_prefix s then
-                   case AList.lookup (op =) lambdas s of
+                   case AList.lookup (op =) lifted s of
                      SOME t =>
                      Const (@{const_name Metis.lambda}, dummyT)
                      $ map_types (map_type_tvar (K dummyT))
-                                 (reveal_lam_lifted lambdas t)
+                                 (reveal_lam_lifted lifted t)
                    | NONE => t
                  else
                    t
diff -r 32b1dbda331c -r 41c885784e04 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 26 11:56:55 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 26 12:56:37 2013 +0200
@@ -912,7 +912,7 @@
     fun export (_, (output, _, _, _, _)) =
       if dest_dir = "" then ()
       else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
-    val ((_, (_, pool, fact_names, _, sym_tab)),
+    val ((_, (_, pool, fact_names, lifted, sym_tab)),
          (output, run_time, used_from, atp_proof, outcome)) =
       with_cleanup clean_up run () |> tap export
     val important_message =
@@ -951,7 +951,7 @@
                     ()
                 val isar_params =
                   (debug, verbose, preplay_timeout, preplay_trace, isar_compress,
-                   pool, fact_names, sym_tab, atp_proof, goal)
+                   pool, fact_names, lifted, sym_tab, atp_proof, goal)
                 val one_line_params =
                   (preplay, proof_banner mode name, used_facts,
                    choose_minimize_command ctxt params minimize_command name
diff -r 32b1dbda331c -r 41c885784e04 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun May 26 11:56:55 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun May 26 12:56:37 2013 +0200
@@ -24,7 +24,8 @@
     play * string * (string * stature) list * minimize_command * int * int
   type isar_params =
     bool * bool * Time.time option * bool * real * string Symtab.table
-    * (string * stature) list vector * int Symtab.table * string proof * thm
+    * (string * stature) list vector * (string * term) list * int Symtab.table
+    * string proof * thm
 
   val smtN : string
   val string_of_reconstructor : reconstructor -> string
@@ -323,12 +324,25 @@
       | aux t = t
   in aux end
 
-fun decode_line ctxt sym_tab (name, role, u, rule, deps) =
+fun unlift_term lifted =
+  map_aterms (fn t as Const (s, _) =>
+                 if String.isPrefix lam_lifted_prefix s then
+                   case AList.lookup (op =) lifted s of
+                     SOME t =>
+                     (* FIXME: do something about the types *)
+                     unlift_term lifted t
+                   | NONE => t
+                 else
+                   t
+               | t => t)
+
+fun decode_line ctxt lifted sym_tab (name, role, u, rule, deps) =
   let
     val thy = Proof_Context.theory_of ctxt
     val t =
       u |> prop_of_atp ctxt true sym_tab
         |> uncombine_term thy
+        |> unlift_term lifted
         |> infer_formula_types ctxt
   in (name, role, t, rule, deps) end
 
@@ -627,11 +641,12 @@
 
 type isar_params =
   bool * bool * Time.time option * bool * real * string Symtab.table
-  * (string * stature) list vector * int Symtab.table * string proof * thm
+  * (string * stature) list vector * (string * term) list * int Symtab.table
+  * string proof * thm
 
 fun isar_proof_text ctxt isar_proofs
     (debug, verbose, preplay_timeout, preplay_trace, isar_compress, pool,
-     fact_names, sym_tab, atp_proof, goal)
+     fact_names, lifted, sym_tab, atp_proof, goal)
     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   let
     val ((params, hyp_ts, concl_t), ctxt) = strip_subgoal goal subgoal ctxt
@@ -649,7 +664,7 @@
           |> clean_up_atp_proof_dependencies
           |> nasty_atp_proof pool
           |> map_term_names_in_atp_proof repair_name
-          |> map (decode_line ctxt sym_tab)
+          |> map (decode_line ctxt lifted sym_tab)
           |> repair_waldmeister_endgame
           |> rpair [] |-> fold_rev (add_line fact_names)
           |> rpair [] |-> fold_rev add_nontrivial_line