src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42680 b6c27cf04fe9
parent 42677 25496cd3c199
child 42682 562046fd8e0c
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed May 04 18:48:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed May 04 19:35:48 2011 +0200
@@ -147,17 +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 =
+fun formula_fold pos f =
   let
     fun aux pos (AQuant (_, _, phi)) = aux pos phi
-      | aux pos (AConn (ANot, [phi])) = aux (not pos) phi
+      | aux pos (AConn (ANot, [phi])) = aux (Option.map 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 (Option.map not pos) phi1 #> aux pos phi2
+      | aux pos (AConn (AAnd, phis)) = fold (aux pos) phis
+      | aux pos (AConn (AOr, phis)) = fold (aux pos) phis
+      | aux _ (AConn (_, phis)) = fold (aux NONE) phis
       | aux pos (AAtom tm) = f pos tm
-  in aux true end
+  in aux (SOME pos) end
 
 type translated_formula =
   {name: string,
@@ -483,7 +483,7 @@
       end
   in aux true end
 fun add_fact_syms_to_table explicit_apply =
-  fact_lift (formula_fold (K (add_combterm_syms_to_table explicit_apply)))
+  fact_lift (formula_fold true (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}),
@@ -665,38 +665,66 @@
    unsound ATP proofs. The checks below are an (unsound) approximation of
    finiteness. *)
 
-fun is_dtyp_finite _ (Datatype_Aux.DtTFree _) = true
-  | is_dtyp_finite ctxt (Datatype_Aux.DtType (s, Us)) =
-    is_type_constr_finite ctxt s andalso forall (is_dtyp_finite ctxt) Us
-  | is_dtyp_finite _ (Datatype_Aux.DtRec _) = false
-and is_type_finite ctxt (Type (s, Ts)) =
-    is_type_constr_finite ctxt s andalso forall (is_type_finite ctxt) Ts
-  | is_type_finite _ _ = false
-and is_type_constr_finite ctxt s =
-  let val thy = Proof_Context.theory_of ctxt in
-    case Datatype_Data.get_info thy s of
-      SOME {descr, ...} =>
-      forall (fn (_, (_, _, constrs)) =>
-                 forall (forall (is_dtyp_finite ctxt) o snd) constrs) descr
-    | NONE =>
-      case Typedef.get_info ctxt s of
-        ({rep_type, ...}, _) :: _ => is_type_finite ctxt rep_type
-      | [] => true
-  end
+fun datatype_constrs thy (T as Type (s, Ts)) =
+    (case Datatype.get_info thy s of
+       SOME {index, descr, ...} =>
+       let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in
+         map (apsnd (fn Us => map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
+             constrs
+       end
+     | NONE => [])
+  | datatype_constrs _ _ = []
 
-fun should_encode_type _ All_Types _ = true
-  | should_encode_type ctxt Finite_Types T = is_type_finite ctxt T
-  | should_encode_type _ Nonmonotonic_Types _ =
-    error "Monotonicity inference not implemented yet."
-  | should_encode_type _ _ _ = false
+(* Similar to "Nitpick_HOL.bounded_exact_card_of_type".
+   0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means
+   cardinality 2 or more. The specified default cardinality is returned if the
+   cardinality of the type can't be determined. *)
+fun tiny_card_of_type ctxt default_card T =
+  let
+    val max = 2 (* 1 would be too small for the "fun" case *)
+    fun aux avoid T =
+      (if member (op =) avoid T then
+         0
+       else case T of
+         Type (@{type_name fun}, [T1, T2]) =>
+         (case (aux avoid T1, aux avoid T2) of
+            (_, 1) => 1
+          | (0, _) => 0
+          | (_, 0) => 0
+          | (k1, k2) =>
+            if k1 >= max orelse k2 >= max then max
+            else Int.min (max, Integer.pow k2 k1))
+       | Type _ =>
+         (case datatype_constrs (Proof_Context.theory_of ctxt) T of
+            [] => default_card
+          | constrs =>
+            let
+              val constr_cards =
+                map (Integer.prod o map (aux (T :: avoid)) o binder_types o snd)
+                    constrs
+            in
+              if exists (curry (op =) 0) constr_cards then 0
+              else Int.min (max, Integer.sum constr_cards)
+            end)
+       | _ => default_card)
+  in Int.min (max, aux [] T) end
 
-fun should_predicate_on_type ctxt (Preds (_, level)) T =
-    should_encode_type ctxt level T
-  | should_predicate_on_type _ _ _ = false
+fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0
+fun is_type_surely_infinite ctxt T = tiny_card_of_type ctxt 1 T = 0
 
-fun should_tag_with_type ctxt (Tags (_, level)) T =
-    should_encode_type ctxt level T
-  | should_tag_with_type _ _ _ = false
+fun should_encode_type _ _ All_Types _ = true
+  | should_encode_type ctxt _ Finite_Types T = is_type_surely_finite ctxt T
+  | should_encode_type _ nonmono_Ts Nonmonotonic_Types T =
+    exists (curry Type.raw_instance T) nonmono_Ts
+  | should_encode_type _ _ _ _ = false
+
+fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level)) T =
+    should_encode_type ctxt nonmono_Ts level T
+  | should_predicate_on_type _ _ _ _ = false
+
+fun should_tag_with_type ctxt nonmono_Ts (Tags (_, level)) T =
+    should_encode_type ctxt nonmono_Ts level T
+  | should_tag_with_type _ _ _ _ = false
 
 fun type_pred_combatom type_sys T tm =
   CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T]),
@@ -704,7 +732,7 @@
   |> impose_type_arg_policy_in_combterm type_sys
   |> AAtom
 
-fun formula_from_combformula ctxt type_sys =
+fun formula_from_combformula ctxt nonmono_Ts type_sys =
   let
     fun tag_with_type type_sys T tm =
       CombConst (`make_fixed_const type_tag_name, T --> T, [T])
@@ -723,7 +751,8 @@
                           map (do_term false) args)
         val T = combtyp_of u
       in
-        t |> (if not top_level andalso should_tag_with_type ctxt type_sys T then
+        t |> (if not top_level andalso
+                should_tag_with_type ctxt nonmono_Ts type_sys T then
                 tag_with_type type_sys T
               else
                 I)
@@ -731,7 +760,7 @@
     val do_bound_type =
       if type_sys = Many_Typed then SOME o mangled_type_name else K NONE
     fun do_out_of_bound_type (s, T) =
-      if should_predicate_on_type ctxt type_sys T then
+      if should_predicate_on_type ctxt nonmono_Ts type_sys T then
         type_pred_combatom type_sys T (CombVar (s, T))
         |> do_formula |> SOME
       else
@@ -748,11 +777,11 @@
       | do_formula (AAtom tm) = AAtom (do_term true tm)
   in do_formula end
 
-fun formula_for_fact ctxt type_sys
+fun formula_for_fact ctxt nonmono_Ts type_sys
                      ({combformula, atomic_types, ...} : translated_formula) =
   mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
                 (atp_type_literals_for_types type_sys Axiom atomic_types))
-           (formula_from_combformula ctxt type_sys
+           (formula_from_combformula ctxt nonmono_Ts type_sys
                 (close_combformula_universally combformula))
   |> close_formula_universally
 
@@ -761,13 +790,12 @@
 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
    of monomorphization). The TPTP explicitly forbids name clashes, and some of
    the remote provers might care. *)
-fun formula_line_for_fact ctxt prefix type_sys
+fun formula_line_for_fact ctxt prefix nonmono_Ts type_sys
                           (j, formula as {name, locality, kind, ...}) =
-  Formula (prefix ^
-           (if polymorphism_of_type_sys type_sys = Polymorphic then ""
-            else string_of_int j ^ "_") ^
+  Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then ""
+                     else string_of_int j ^ "_") ^
            ascii_of name,
-           kind, formula_for_fact ctxt type_sys formula, NONE,
+           kind, formula_for_fact ctxt nonmono_Ts type_sys formula, NONE,
            if generate_useful_info then
              case locality of
                Intro => useful_isabelle_info "intro"
@@ -800,10 +828,10 @@
                          (fo_literal_from_arity_literal conclLit))
            |> close_formula_universally, NONE, NONE)
 
-fun formula_line_for_conjecture ctxt type_sys
+fun formula_line_for_conjecture ctxt nonmono_Ts type_sys
         ({name, kind, combformula, ...} : translated_formula) =
   Formula (conjecture_prefix ^ name, kind,
-           formula_from_combformula ctxt type_sys
+           formula_from_combformula ctxt nonmono_Ts type_sys
                                     (close_combformula_universally combformula)
            |> close_formula_universally, NONE, NONE)
 
@@ -856,30 +884,34 @@
       end
   in do_term end
 fun add_fact_syms_to_decl_table type_sys repaired_sym_tab =
-  fact_lift (formula_fold
+  fact_lift (formula_fold true
       (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 add_combterm_nonmonotonic_types _ (SOME false) _ = I
+  | add_combterm_nonmonotonic_types ctxt _
+        (CombApp (CombApp (CombConst (("equal", _), Type (_, [T, _]), _), tm1),
+                  tm2)) =
+    (exists is_var_or_bound_var [tm1, tm2] andalso
+     not (is_type_surely_infinite ctxt T)) ? insert_type I T
+  | add_combterm_nonmonotonic_types _ _ _ = I
+fun add_fact_nonmonotonic_types ctxt ({kind, combformula, ...}
+                                      : translated_formula) =
+  formula_fold (kind <> Conjecture) (add_combterm_nonmonotonic_types ctxt)
+               combformula
+fun add_nonmonotonic_types_for_facts ctxt type_sys facts =
+  level_of_type_sys type_sys = Nonmonotonic_Types
+  ? fold (add_fact_nonmonotonic_types ctxt) facts
 
 fun n_ary_strip_type 0 T = ([], T)
   | n_ary_strip_type n (Type (@{type_name fun}, [dom_T, ran_T])) =
@@ -896,7 +928,8 @@
 
 fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
 
-fun formula_line_for_sym_decl ctxt type_sys n s j (s', T_args, T, _, ary) =
+fun formula_line_for_sym_decl ctxt nonmono_Ts type_sys n s j
+                              (s', T_args, T, _, ary) =
   let
     val (arg_Ts, res_T) = n_ary_strip_type ary T
     val bound_names =
@@ -913,12 +946,12 @@
              |> fold (curry (CombApp o swap)) bound_tms
              |> type_pred_combatom type_sys res_T
              |> mk_aquant AForall (bound_names ~~ bound_Ts)
-             |> formula_from_combformula ctxt type_sys
+             |> formula_from_combformula ctxt nonmono_Ts type_sys
              |> close_formula_universally,
              NONE, NONE)
   end
 
-fun problem_lines_for_sym_decls ctxt type_sys (s, decls) =
+fun problem_lines_for_sym_decls ctxt nonmono_Ts type_sys (s, decls) =
   if type_sys = Many_Typed then
     map (decl_line_for_sym_decl s) decls
   else
@@ -936,15 +969,16 @@
         | _ => decls
       val n = length decls
       val decls =
-        decls |> filter (should_predicate_on_type ctxt type_sys
+        decls |> filter (should_predicate_on_type ctxt nonmono_Ts type_sys
                          o result_type_of_decl)
     in
-      map2 (formula_line_for_sym_decl ctxt type_sys n s)
+      map2 (formula_line_for_sym_decl ctxt nonmono_Ts type_sys n s)
            (0 upto length decls - 1) decls
     end
 
-fun problem_lines_for_sym_decl_table ctxt type_sys sym_decl_tab =
-  Symtab.fold_rev (append o problem_lines_for_sym_decls ctxt type_sys)
+fun problem_lines_for_sym_decl_table ctxt nonmono_Ts type_sys sym_decl_tab =
+  Symtab.fold_rev (append o problem_lines_for_sym_decls ctxt nonmono_Ts
+                                                        type_sys)
                   sym_decl_tab []
 
 fun add_tff_types_in_formula (AQuant (_, xs, phi)) =
@@ -985,33 +1019,35 @@
     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 conjs_and_facts = conjs @ facts
-    val repaired_sym_tab = conjs_and_facts |> sym_table_for_facts false
-    val sym_decl_lines =
-      conjs_and_facts
-      |> sym_decl_table_for_facts type_sys repaired_sym_tab
-      |> problem_lines_for_sym_decl_table ctxt type_sys
+    val repaired_sym_tab = conjs @ facts |> sym_table_for_facts false
     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)
+    val nonmono_Ts =
+      [] |> fold (add_nonmonotonic_types_for_facts ctxt type_sys)
+                 [facts, conjs, helpers]
+    val sym_decl_lines =
+      conjs @ facts
+      |> sym_decl_table_for_facts type_sys repaired_sym_tab
+      |> problem_lines_for_sym_decl_table ctxt nonmono_Ts type_sys
     (* Reordering these might confuse the proof reconstruction code or the SPASS
        Flotter hack. *)
     val problem =
       [(sym_declsN, sym_decl_lines),
-       (factsN, map (formula_line_for_fact ctxt fact_prefix type_sys)
+       (factsN, map (formula_line_for_fact ctxt fact_prefix nonmono_Ts type_sys)
                     (0 upto length facts - 1 ~~ facts)),
        (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
        (aritiesN, map formula_line_for_arity_clause arity_clauses),
-       (helpersN, map (formula_line_for_fact ctxt helper_prefix type_sys)
+       (helpersN, map (formula_line_for_fact ctxt helper_prefix nonmono_Ts
+                                             type_sys)
                       (0 upto length helpers - 1 ~~ helpers)
                   |> (case type_sys of
                         Tags (Polymorphic, level) =>
                         member (op =) [Finite_Types, Nonmonotonic_Types] level
                         ? cons (ti_ti_helper_fact ())
                       | _ => I)),
-       (conjsN, map (formula_line_for_conjecture ctxt type_sys) conjs),
+       (conjsN, map (formula_line_for_conjecture ctxt nonmono_Ts type_sys)
+                    conjs),
        (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
     val problem =
       problem
@@ -1041,7 +1077,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 (K (add_term_weights weight)) phi
+    formula_fold true (K (add_term_weights weight)) phi
   | add_problem_line_weights _ _ = I
 
 fun add_conjectures_weights [] = I