# HG changeset patch
# User blanchet
# Date 1304267844 -7200
# Node ID ae0deb39a254b0731936ef1b62f85fffcbf10b4d
# Parent  f65e5f0341b89603332c1de1dbe9636d9d0ce566
fixed min-arity computation when "explicit_apply" is specified

diff -r f65e5f0341b8 -r ae0deb39a254 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
@@ -119,10 +119,8 @@
     | _ => Explicit_Type_Args
 
 fun num_atp_type_args thy type_sys s =
-  if type_arg_policy type_sys s = Explicit_Type_Args then
-    if s = type_pred_base then 1 else num_type_args thy s
-  else
-    0
+  if type_arg_policy type_sys s = Explicit_Type_Args then num_type_args thy s
+  else 0
 
 fun atp_type_literals_for_types type_sys kind Ts =
   if type_sys = No_Types then
@@ -664,10 +662,13 @@
   formula_fold (consider_combterm_for_repair true) combformula
 
 (* The "equal" entry is needed for helper facts if the problem otherwise does
-   not involve equality. The "hBOOL" entry is needed to ensure that no "hAPP"s
-   are introduced for passing arguments to it. *)
-val default_entries =
+   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. *)
+val default_sym_table_entries =
   [("equal", {pred_sym = true, min_arity = 2, max_arity = 2}),
+   ("$false", {pred_sym = true, min_arity = 0, max_arity = 0}),
+   ("$true", {pred_sym = true, min_arity = 0, max_arity = 0}),
    (make_fixed_const boolify_base,
     {pred_sym = true, min_arity = 1, max_arity = 1})]
 
@@ -675,25 +676,23 @@
   if explicit_apply then
     NONE
   else
-    SOME (Symtab.empty |> fold Symtab.default default_entries
+    SOME (Symtab.empty |> fold Symtab.default default_sym_table_entries
                        |> fold consider_fact_for_repair facts)
 
-fun min_arity_of _ _ (SOME sym_tab) s =
+fun min_arity_of (SOME sym_tab) s =
     (case Symtab.lookup sym_tab s of
        SOME ({min_arity, ...} : repair_info) => min_arity
      | NONE => 0)
-  | min_arity_of thy type_sys NONE s =
-    if s = "equal" orelse s = type_tag_name orelse
-       String.isPrefix type_const_prefix s orelse
-       String.isPrefix class_prefix s then
-      16383 (* large number *)
+  | min_arity_of NONE s =
+    if s = "equal" then
+      2
     else case strip_prefix_and_unascii const_prefix s of
       SOME s =>
       let val s = s |> unmangled_const |> fst |> invert_const in
         if s = boolify_base then 1
         else if s = explicit_app_base then 2
         else if s = type_pred_base then 1
-        else num_atp_type_args thy type_sys s
+        else 0
       end
     | NONE => 0
 
@@ -701,14 +700,15 @@
    literals, or if it appears with different arities (e.g., because of different
    type instantiations). If false, the constant always receives all of its
    arguments and is used as a predicate. *)
-fun is_pred_sym NONE s =
-    s = "equal" orelse s = "$false" orelse s = "$true" orelse
-    String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s
-  | is_pred_sym (SOME sym_tab) s =
-    case Symtab.lookup sym_tab s of
-      SOME {pred_sym, min_arity, max_arity} =>
-      pred_sym andalso min_arity = max_arity
-    | NONE => false
+fun is_pred_sym (SOME sym_tab) s =
+    (case Symtab.lookup sym_tab s of
+       SOME {pred_sym, min_arity, max_arity} =>
+       pred_sym andalso min_arity = max_arity
+     | NONE => false)
+  | is_pred_sym NONE s =
+    (case AList.lookup (op =) default_sym_table_entries s of
+       SOME {pred_sym, ...} => pred_sym
+     | NONE => false)
 
 val boolify_combconst =
   CombConst (`make_fixed_const boolify_base,
@@ -735,24 +735,24 @@
   in list_app explicit_app [head, arg] end
 fun list_explicit_app head args = fold explicit_app args head
 
-fun repair_apps_in_combterm thy type_sys sym_tab =
+fun repair_apps_in_combterm sym_tab =
   let
     fun aux tm =
       case strip_combterm_comb tm of
         (head as CombConst ((s, _), _, _), args) =>
         args |> map aux
-             |> chop (min_arity_of thy type_sys sym_tab s)
+             |> chop (min_arity_of sym_tab s)
              |>> list_app head
              |-> list_explicit_app
       | (head, args) => list_explicit_app head (map aux args)
   in aux end
 
-fun repair_combterm thy type_sys sym_tab =
+fun repair_combterm type_sys sym_tab =
   repair_pred_syms_in_combterm sym_tab
-  #> repair_apps_in_combterm thy type_sys sym_tab
+  #> repair_apps_in_combterm sym_tab
   #> repair_combterm_consts type_sys
-val repair_combformula = formula_map ooo repair_combterm
-val repair_fact = map_combformula ooo repair_combformula
+val repair_combformula = formula_map oo repair_combterm
+val repair_fact = map_combformula oo repair_combformula
 
 fun is_const_relevant type_sys sym_tab s =
   not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
@@ -787,10 +787,7 @@
   | strip_and_map_combtyp _ _ _ = raise Fail "unexpected non-function"
 
 fun problem_line_for_typed_const ctxt type_sys sym_tab s j (s', ty_args, ty) =
-  let
-    val thy = Proof_Context.theory_of ctxt
-    val arity = min_arity_of thy type_sys sym_tab s
-  in
+  let val arity = min_arity_of sym_tab s in
     if type_sys = Many_Typed then
       let
         val (arg_tys, res_ty) = strip_and_map_combtyp arity mangled_combtyp ty
@@ -858,13 +855,11 @@
 fun prepare_atp_problem ctxt readable_names type_sys explicit_apply hyp_ts
                         concl_t facts =
   let
-    val thy = Proof_Context.theory_of ctxt
     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
       translate_formulas ctxt type_sys hyp_ts concl_t facts
     val sym_tab = sym_table_for_facts explicit_apply (conjs @ facts)
-    val conjs = map (repair_fact thy type_sys sym_tab) conjs
-    val facts = map (repair_fact thy type_sys sym_tab) facts
-    val sym_tab = sym_table_for_facts explicit_apply (conjs @ facts)
+    val conjs = map (repair_fact type_sys sym_tab) conjs
+    val facts = map (repair_fact type_sys sym_tab) facts
     (* Reordering these might confuse the proof reconstruction code or the SPASS
        Flotter hack. *)
     val problem =
@@ -881,7 +876,8 @@
       problem |> maps (map_filter (fn Formula (_, _, _, phi, _, _) => SOME phi
                                     | _ => NONE) o snd)
               |> get_helper_facts ctxt type_sys
-              |>> map (repair_fact thy type_sys sym_tab)
+              |>> map (repair_fact type_sys sym_tab)
+    val sym_tab = sym_table_for_facts explicit_apply (conjs @ facts)
     val const_tab = const_table_for_facts type_sys sym_tab (conjs @ facts)
     val sym_decl_lines =
       Symtab.fold_rev (append o problem_lines_for_const ctxt type_sys sym_tab)