# HG changeset patch
# User blanchet
# Date 1304267844 -7200
# Node ID 93f58e6a6f3ea58495d4760aa8f1bce3fe92e752
# Parent  d40bdf941a9a4904d1fc5966662837cb0d8a2f35
proper handling of partially applied proxy symbols

diff -r d40bdf941a9a -r 93f58e6a6f3e src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
@@ -441,11 +441,29 @@
     (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
   end
 
-fun repair_combterm_consts type_sys =
+val introduce_proxies =
   let
     fun aux top_level (CombApp (tm1, tm2)) =
         CombApp (aux top_level tm1, aux false tm2)
-      | aux top_level (CombConst (name as (s, _), ty, ty_args)) =
+      | aux top_level (CombConst (name as (s, s'), ty, ty_args)) =
+        (case AList.lookup (op =) metis_proxies s of
+           SOME proxy_base =>
+           if top_level then
+             (case s of
+                "c_False" => ("$false", s')
+              | "c_True" => ("$true", s')
+              | _ => name, [])
+            else
+              (proxy_base |>> prefix const_prefix, ty_args)
+          | NONE => (name, ty_args))
+        |> (fn (name, ty_args) => CombConst (name, ty, ty_args))
+      | aux _ tm = tm
+  in aux true end
+
+fun impose_type_arg_policy type_sys =
+  let
+    fun aux (CombApp tmp) = CombApp (pairself aux tmp)
+      | aux (CombConst (name as (s, _), ty, ty_args)) =
         (case strip_prefix_and_unascii const_prefix s of
            NONE => (name, ty_args)
          | SOME s'' =>
@@ -455,20 +473,11 @@
              | Mangled_Types => (mangled_const_name ty_args name, [])
              | Explicit_Type_Args => (name, ty_args)
            end)
-        |> (fn (name as (s, s'), ty_args) =>
-               case AList.lookup (op =) metis_proxies s of
-                 SOME proxy_base =>
-                 if top_level then
-                   (case s of
-                      "c_False" => ("$false", s')
-                    | "c_True" => ("$true", s')
-                    | _ => name, [])
-                  else
-                    (proxy_base |>> prefix const_prefix, ty_args)
-                | NONE => (name, ty_args))
         |> (fn (name, ty_args) => CombConst (name, ty, ty_args))
-      | aux _ tm = tm
-  in aux true end
+      | aux tm = tm
+  in aux end
+val impose_type_arg_policy_on_fact =
+  update_combformula o formula_map o impose_type_arg_policy
 
 fun tag_with_type ty t = ATerm (`I type_tag_name, [ty, t])
 
@@ -510,7 +519,7 @@
 fun type_pred_combatom type_sys T tm =
   CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]),
            tm)
-  |> repair_combterm_consts type_sys
+  |> impose_type_arg_policy type_sys
   |> AAtom
 
 fun formula_from_combformula ctxt type_sys =
@@ -647,9 +656,9 @@
 val add_fact_to_sym_table = fact_lift o formula_fold o add_combterm_to_sym_table
 
 (* The "equal" entry is needed for helper facts if the problem otherwise does
-   not involve equality. The "$false" and $"true" entries are needed to ensure
-   that no "hBOOL" is introduced for them. The "hBOOL" entry is needed to ensure
-   that no "hAPP"s are introduced for passing arguments to it. *)
+   not involve equality (FIXME). The "$false" and $"true" entries are needed to
+   ensure that no "hBOOL" is introduced for them. The "hBOOL" entry is needed to
+   ensure that no "hAPP"s are introduced for passing arguments to it. *)
 val default_sym_table_entries =
   [("equal", {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
    (make_fixed_const boolify_base,
@@ -688,7 +697,7 @@
   CombConst (`make_fixed_const boolify_base, @{typ "bool => bool"}, [])
 fun boolify tm = CombApp (boolify_combconst, tm)
 
-fun repair_pred_syms_in_combterm sym_tab tm =
+fun introduce_boolifies_in_combterm sym_tab tm =
   case strip_combterm_comb tm of
     (CombConst ((s, _), _, _), _) =>
     if is_pred_sym sym_tab s then tm else boolify tm
@@ -706,7 +715,7 @@
   in list_app explicit_app [head, arg] end
 fun list_explicit_app head args = fold explicit_app args head
 
-fun repair_apps_in_combterm sym_tab =
+fun introduce_explicit_apps_in_combterm sym_tab =
   let
     fun aux tm =
       case strip_combterm_comb tm of
@@ -718,12 +727,12 @@
       | (head, args) => list_explicit_app head (map aux args)
   in aux end
 
-fun repair_combterm type_sys sym_tab =
-  repair_pred_syms_in_combterm sym_tab
-  #> repair_apps_in_combterm sym_tab
-  #> repair_combterm_consts type_sys
-val repair_combformula = formula_map oo repair_combterm
-val repair_fact = update_combformula oo repair_combformula
+fun firstorderize_combterm sym_tab =
+  introduce_explicit_apps_in_combterm sym_tab
+  #> introduce_boolifies_in_combterm sym_tab
+  #> introduce_proxies
+val firstorderize_fact =
+  update_combformula o formula_map o firstorderize_combterm
 
 fun is_const_relevant type_sys sym_tab s =
   not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
@@ -753,7 +762,7 @@
     strip_and_map_type (n - 1) f ran_T |>> cons (f dom_T)
   | strip_and_map_type _ _ _ = raise Fail "unexpected non-function"
 
-fun problem_line_for_typed_const ctxt type_sys sym_tab s j (s', ty_args, T) =
+fun problem_line_for_typed_const ctxt type_sys sym_tab s n j (s', ty_args, T) =
   let val ary = min_arity_of sym_tab s in
     if type_sys = Many_Typed then
       let val (arg_Ts, res_T) = strip_and_map_type ary mangled_type_name T in
@@ -768,8 +777,7 @@
           1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
         val bound_tms =
           bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
-        val bound_Ts =
-          arg_Ts |> map (case type_sys of Mangled _ => K NONE | _ => SOME)
+        val bound_Ts = arg_Ts |> map (if n > 1 then SOME else K NONE)
         val freshener =
           case type_sys of Args _ => string_of_int j ^ "_" | _ => ""
       in
@@ -783,8 +791,10 @@
       end
   end
 fun problem_lines_for_sym_decl ctxt type_sys sym_tab (s, xs) =
-  map2 (problem_line_for_typed_const ctxt type_sys sym_tab s)
-       (0 upto length xs - 1) xs
+  let val n = length xs in
+    map2 (problem_line_for_typed_const ctxt type_sys sym_tab s n)
+         (0 upto n - 1) xs
+  end
 fun problem_lines_for_sym_decls ctxt type_sys sym_tab typed_const_tab =
   Symtab.fold_rev (append o problem_lines_for_sym_decl ctxt type_sys sym_tab)
                   typed_const_tab []
@@ -826,15 +836,19 @@
     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
       translate_formulas ctxt type_sys hyp_ts concl_t facts
     val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply
-    val conjs = conjs |> map (repair_fact type_sys sym_tab)
-    val facts = facts |> map (repair_fact type_sys sym_tab)
+    val (conjs, facts) =
+      (conjs, facts) |> pairself (map (firstorderize_fact sym_tab))
+    val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply
+    val (conjs, facts) =
+      (conjs, facts) |> pairself (map (impose_type_arg_policy_on_fact type_sys))
     val sym_tab' = conjs @ facts |> sym_table_for_facts false
     val typed_const_tab =
       conjs @ facts |> typed_const_table_for_facts type_sys sym_tab'
     val sym_decl_lines =
       typed_const_tab |> problem_lines_for_sym_decls ctxt type_sys sym_tab'
     val helpers = helper_facts_for_sym_table ctxt type_sys sym_tab'
-                  |> map (repair_fact type_sys sym_tab')
+                  |> map (firstorderize_fact sym_tab
+                          #> impose_type_arg_policy_on_fact type_sys)
     (* Reordering these might confuse the proof reconstruction code or the SPASS
        Flotter hack. *)
     val problem =