# HG changeset patch
# User blanchet
# Date 1304516105 -7200
# Node ID 25496cd3c199a10a010e52efe5f4eb58ef24a086
# Parent  223153bb68a1927dd5d4d771b3397090c937f4ff
monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.

diff -r 223153bb68a1 -r 25496cd3c199 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed May 04 11:49:46 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed May 04 15:35:05 2011 +0200
@@ -147,9 +147,17 @@
   | formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
   | formula_map f (AAtom tm) = AAtom (f tm)
 
-fun formula_fold f (AQuant (_, _, phi)) = formula_fold f phi
-  | formula_fold f (AConn (_, phis)) = fold (formula_fold f) phis
-  | formula_fold f (AAtom tm) = f tm
+fun formula_fold f =
+  let
+    fun aux pos (AQuant (_, _, phi)) = aux pos phi
+      | aux pos (AConn (ANot, [phi])) = aux (not pos) phi
+      | aux pos (AConn (AImplies, [phi1, phi2])) =
+        aux (not pos) phi1 #> aux pos phi2
+      | aux pos (AConn (c, phis)) =
+        if member (op =) [AAnd, AOr] c then fold (aux pos) phis
+        else raise Fail "unexpected connective with unknown polarities"
+      | aux pos (AAtom tm) = f pos tm
+  in aux true end
 
 type translated_formula =
   {name: string,
@@ -174,7 +182,7 @@
       Tags (_, All_Types) => true
     | _ => polymorphism_of_type_sys type_sys <> Mangled_Monomorphic andalso
            member (op =) boring_consts s))
-  
+
 datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Type_Args
 
 fun general_type_arg_policy type_sys =
@@ -475,7 +483,7 @@
       end
   in aux true end
 fun add_fact_syms_to_table explicit_apply =
-  fact_lift (formula_fold (add_combterm_syms_to_table explicit_apply))
+  fact_lift (formula_fold (K (add_combterm_syms_to_table explicit_apply)))
 
 val default_sym_table_entries : (string * sym_info) list =
   [("equal", {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
@@ -814,6 +822,12 @@
 
 (** Symbol declarations **)
 
+fun insert_type get_T x xs =
+  let val T = get_T x in
+    if exists (curry Type.raw_instance T o get_T) xs then xs
+    else x :: filter_out ((fn T' => Type.raw_instance (T', T)) o get_T) xs
+  end
+
 fun should_declare_sym type_sys pred_sym s =
   not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
   not (String.isPrefix "$" s) andalso
@@ -821,13 +835,10 @@
 
 fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab =
   let
-    fun declare_sym (decl as (_, _, T, _, _)) decls =
+    fun declare_sym decl decls =
+      (* FIXME: use "insert_type" in all cases? *)
       case type_sys of
-        Preds (Polymorphic, All_Types) =>
-        if exists (curry Type.raw_instance T o #3) decls then
-          decls
-        else
-          decl :: filter_out ((fn T' => Type.raw_instance (T', T)) o #3) decls
+        Preds (Polymorphic, All_Types) => insert_type #3 decl decls
       | _ => insert (op =) decl decls
     fun do_term tm =
       let val (head, args) = strip_combterm_comb tm in
@@ -846,12 +857,30 @@
   in do_term end
 fun add_fact_syms_to_decl_table type_sys repaired_sym_tab =
   fact_lift (formula_fold
-      (add_combterm_syms_to_decl_table type_sys repaired_sym_tab))
+      (K (add_combterm_syms_to_decl_table type_sys repaired_sym_tab)))
 fun sym_decl_table_for_facts type_sys repaired_sym_tab facts =
   Symtab.empty |> is_type_sys_fairly_sound type_sys
                   ? fold (add_fact_syms_to_decl_table type_sys repaired_sym_tab)
                          facts
 
+(* FIXME: use CombVar not CombConst for bound variables? *)
+fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
+    String.isPrefix bound_var_prefix s
+  | is_var_or_bound_var (CombVar _) = true
+  | is_var_or_bound_var _ = false
+
+fun add_combterm_nonmonotonic_types true
+        (CombApp (CombConst (("equal", _), Type (_, [T, _]), _),
+                  CombApp (tm1, tm2))) =
+    exists is_var_or_bound_var [tm1, tm2] ? insert_type I T
+  | add_combterm_nonmonotonic_types _ _ = I
+
+val add_fact_nonmonotonic_types =
+  fact_lift (formula_fold add_combterm_nonmonotonic_types)
+fun nonmonotonic_types_for_facts type_sys facts =
+  [] |> level_of_type_sys type_sys = Nonmonotonic_Types
+        ? fold add_fact_nonmonotonic_types facts
+
 fun n_ary_strip_type 0 T = ([], T)
   | n_ary_strip_type n (Type (@{type_name fun}, [dom_T, ran_T])) =
     n_ary_strip_type (n - 1) ran_T |>> cons dom_T
@@ -956,14 +985,17 @@
     val sym_tab = conjs @ facts |> sym_table_for_facts explicit_apply
     val (conjs, facts) =
       (conjs, facts) |> pairself (map (repair_fact type_sys sym_tab))
-    val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false
+    val conjs_and_facts = conjs @ facts
+    val repaired_sym_tab = conjs_and_facts |> sym_table_for_facts false
     val sym_decl_lines =
-      conjs @ facts
+      conjs_and_facts
       |> sym_decl_table_for_facts type_sys repaired_sym_tab
       |> problem_lines_for_sym_decl_table ctxt type_sys
     val helpers =
       helper_facts_for_sym_table ctxt type_sys repaired_sym_tab
       |> map (repair_fact type_sys sym_tab)
+    val nonmonotonic_Ts =
+      nonmonotonic_types_for_facts type_sys (helpers @ conjs_and_facts)
     (* Reordering these might confuse the proof reconstruction code or the SPASS
        Flotter hack. *)
     val problem =
@@ -1009,7 +1041,7 @@
   (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
   #> fold (add_term_weights weight) tms
 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
-    formula_fold (add_term_weights weight) phi
+    formula_fold (K (add_term_weights weight)) phi
   | add_problem_line_weights _ _ = I
 
 fun add_conjectures_weights [] = I