# HG changeset patch
# User blanchet
# Date 1304267844 -7200
# Node ID 3d9930cb677021a04f31c0195298e0845ff061e6
# Parent  ae0deb39a254b0731936ef1b62f85fffcbf10b4d
cleaned up "explicit_apply" so that it shares most of its code path with the default mode of operation

diff -r ae0deb39a254 -r 3d9930cb6770 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
@@ -76,11 +76,13 @@
    combformula: (name, combtyp, combterm) formula,
    ctypes_sorts: typ list}
 
-fun map_combformula f
+fun update_combformula f
         ({name, kind, combformula, ctypes_sorts} : translated_formula) =
   {name = name, kind = kind, combformula = f combformula,
    ctypes_sorts = ctypes_sorts} : translated_formula
 
+fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
+
 datatype type_system =
   Many_Typed |
   Mangled of bool |
@@ -639,27 +641,32 @@
 
 type repair_info = {pred_sym: bool, min_arity: int, max_arity: int}
 
-fun consider_combterm_for_repair top_level tm =
-  let val (head, args) = strip_combterm_comb tm in
-    (case head of
-       CombConst ((s, _), _, _) =>
-       if String.isPrefix bound_var_prefix s then
-         I
-       else
-         let val n = length args in
-           Symtab.map_default
-               (s, {pred_sym = true, min_arity = n, max_arity = 0})
-               (fn {pred_sym, min_arity, max_arity} =>
-                   {pred_sym = pred_sym andalso top_level,
-                    min_arity = Int.min (n, min_arity),
-                    max_arity = Int.max (n, max_arity)})
-        end
-     | _ => I)
-    #> fold (consider_combterm_for_repair false) args
-  end
+fun consider_combterm_for_repair explicit_apply =
+  let
+    fun aux top_level tm =
+      let val (head, args) = strip_combterm_comb tm in
+        (case head of
+           CombConst ((s, _), _, _) =>
+           if String.isPrefix bound_var_prefix s then
+             I
+           else
+             let val arity = length args in
+               Symtab.map_default
+                   (s, {pred_sym = true,
+                        min_arity = if explicit_apply then 0 else arity,
+                        max_arity = 0})
+                   (fn {pred_sym, min_arity, max_arity} =>
+                       {pred_sym = pred_sym andalso top_level,
+                        min_arity = Int.min (arity, min_arity),
+                        max_arity = Int.max (arity, max_arity)})
+            end
+         | _ => I)
+        #> fold (aux false) args
+      end
+  in aux true end
 
-fun consider_fact_for_repair ({combformula, ...} : translated_formula) =
-  formula_fold (consider_combterm_for_repair true) combformula
+fun consider_fact_for_repair explicit_apply =
+  fact_lift (formula_fold (consider_combterm_for_repair explicit_apply))
 
 (* 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
@@ -673,20 +680,14 @@
     {pred_sym = true, min_arity = 1, max_arity = 1})]
 
 fun sym_table_for_facts explicit_apply facts =
-  if explicit_apply then
-    NONE
-  else
-    SOME (Symtab.empty |> fold Symtab.default default_sym_table_entries
-                       |> fold consider_fact_for_repair facts)
+  Symtab.empty |> fold Symtab.default default_sym_table_entries
+               |> fold (consider_fact_for_repair explicit_apply) facts
 
-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 NONE s =
-    if s = "equal" then
-      2
-    else case strip_prefix_and_unascii const_prefix s of
+fun min_arity_of sym_tab s =
+  case Symtab.lookup sym_tab s of
+    SOME ({min_arity, ...} : repair_info) => min_arity
+  | NONE =>
+    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
@@ -700,15 +701,11 @@
    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 (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)
+fun is_pred_sym 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
 
 val boolify_combconst =
   CombConst (`make_fixed_const boolify_base,
@@ -752,7 +749,7 @@
   #> repair_apps_in_combterm sym_tab
   #> repair_combterm_consts type_sys
 val repair_combformula = formula_map oo repair_combterm
-val repair_fact = map_combformula oo repair_combformula
+val repair_fact = update_combformula oo repair_combformula
 
 fun is_const_relevant type_sys sym_tab s =
   not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
@@ -769,9 +766,8 @@
     #> fold (consider_combterm_consts type_sys sym_tab) args
   end
 
-fun consider_fact_consts type_sys sym_tab
-                         ({combformula, ...} : translated_formula) =
-  formula_fold (consider_combterm_consts type_sys sym_tab) combformula
+fun consider_fact_consts type_sys sym_tab =
+  fact_lift (formula_fold (consider_combterm_consts type_sys sym_tab))
 
 (* FIXME: needed? *)
 fun const_table_for_facts type_sys sym_tab facts =