author blanchet Wed, 04 May 2011 15:35:05 +0200 changeset 42677 25496cd3c199 parent 42675 223153bb68a1 child 42678 593e375b939f
monotonic type inference in ATP Sledgehammer problems -- based on Claessen & al.'s CADE 2011 paper, Sect. 2.3.
```--- 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
+  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 @@

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
fact_lift (formula_fold
fun sym_decl_table_for_facts type_sys repaired_sym_tab facts =
Symtab.empty |> is_type_sys_fairly_sound type_sys
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
+
+        (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
+
+fun nonmonotonic_types_for_facts type_sys facts =
+  [] |> level_of_type_sys type_sys = Nonmonotonic_Types
+
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)
fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
+    formula_fold (K (add_term_weights weight)) phi
| add_problem_line_weights _ _ = I