1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 12:40:48 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 12:40:48 2011 +0200
     1.3 @@ -483,13 +483,13 @@
     1.4  fun tiny_card_of_type ctxt default_card T =
     1.5    let
     1.6      val max = 2 (* 1 would be too small for the "fun" case *)
     1.7 -    fun aux avoid T =
     1.8 +    fun aux slack avoid T =
     1.9        (if member (op =) avoid T then
    1.10           0
    1.11         else case T of
    1.12           Type (@{type_name fun}, [T1, T2]) =>
    1.13 -         (case (aux avoid T1, aux avoid T2) of
    1.14 -            (_, 1) => 1
    1.15 +         (case (aux slack avoid T1, aux slack avoid T2) of
    1.16 +            (k, 1) => if slack andalso k = 0 then 0 else 1
    1.17            | (0, _) => 0
    1.18            | (_, 0) => 0
    1.19            | (k1, k2) =>
    1.20 @@ -504,7 +504,7 @@
    1.21               constrs as _ :: _ =>
    1.22               let
    1.23                 val constr_cards =
    1.24 -                 map (Integer.prod o map (aux (T :: avoid)) o binder_types
    1.25 +                 map (Integer.prod o map (aux slack (T :: avoid)) o binder_types
    1.26                        o snd) constrs
    1.27               in
    1.28                 if exists (curry (op =) 0) constr_cards then 0
    1.29 @@ -516,18 +516,26 @@
    1.30                 (* We cheat here by assuming that typedef types are infinite if
    1.31                    their underlying type is infinite. This is unsound in general
    1.32                    but it's hard to think of a realistic example where this would
    1.33 -                  not be the case. *)
    1.34 +                  not be the case. We are also slack with representation types:
    1.35 +                  If it has the form "sigma => tau", we consider it enough to
    1.36 +                  check "sigma" for infiniteness. (Look for "slack" in this
    1.37 +                  function.) *)
    1.38                 (case varify_and_instantiate_type ctxt
    1.39                           (Logic.varifyT_global abs_type) T
    1.40                           (Logic.varifyT_global rep_type)
    1.41 -                     |> aux avoid of
    1.42 +                     |> aux true avoid of
    1.43                    0 => 0
    1.44                  | 1 => 1
    1.45                  | _ => default_card)
    1.46               | [] => default_card
    1.47           end
    1.48 +       | TFree _ =>
    1.49 +         (* Very slightly unsound: Type variables are assumed not to be
    1.50 +            constrained to have cardinality 1. (In practice, the user would most
    1.51 +            likely have used "unit" directly in that case.) *)
    1.52 +         if default_card = 1 then 2 else default_card
    1.53         | _ => default_card)
    1.54 -  in Int.min (max, aux [] T) end
    1.55 +  in Int.min (max, aux false [] T) end
    1.56  
    1.57  fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt 0 T <> 0
    1.58  fun is_type_surely_infinite ctxt T = tiny_card_of_type ctxt 1 T = 0
    1.59 @@ -896,34 +904,30 @@
    1.60    not (String.isPrefix "$" s) andalso
    1.61    ((case type_sys of Simple _ => true | _ => false) orelse not pred_sym)
    1.62  
    1.63 -fun add_combterm_syms_to_decl_table type_sys repaired_sym_tab =
    1.64 +fun sym_decl_table_for_facts type_sys repaired_sym_tab (conjs, facts) =
    1.65    let
    1.66 -    fun declare_sym decl decls =
    1.67 -      case type_sys of
    1.68 -        Preds (Polymorphic, All_Types) => insert_type #3 decl decls
    1.69 -      | _ => insert (op =) decl decls
    1.70 -    and do_term tm =
    1.71 +    fun add_combterm in_conj tm =
    1.72        let val (head, args) = strip_combterm_comb tm in
    1.73          (case head of
    1.74             CombConst ((s, s'), T, T_args) =>
    1.75             let val pred_sym = is_pred_sym repaired_sym_tab s in
    1.76               if should_declare_sym type_sys pred_sym s then
    1.77                 Symtab.map_default (s, [])
    1.78 -                   (declare_sym (s', T_args, T, pred_sym, length args))
    1.79 +                   (insert_type #3 (s', T_args, T, pred_sym, length args,
    1.80 +                                    in_conj))
    1.81               else
    1.82                 I
    1.83             end
    1.84           | _ => I)
    1.85 -        #> fold do_term args
    1.86 +        #> fold (add_combterm in_conj) args
    1.87        end
    1.88 -  in do_term end
    1.89 -fun add_fact_syms_to_decl_table type_sys repaired_sym_tab =
    1.90 -  fact_lift (formula_fold true
    1.91 -      (K (add_combterm_syms_to_decl_table type_sys repaired_sym_tab)))
    1.92 -fun sym_decl_table_for_facts type_sys repaired_sym_tab facts =
    1.93 -  Symtab.empty |> is_type_sys_fairly_sound type_sys
    1.94 -                  ? fold (add_fact_syms_to_decl_table type_sys repaired_sym_tab)
    1.95 -                         facts
    1.96 +    fun add_fact in_conj =
    1.97 +      fact_lift (formula_fold true (K (add_combterm in_conj)))
    1.98 +  in
    1.99 +    Symtab.empty
   1.100 +    |> is_type_sys_fairly_sound type_sys
   1.101 +       ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
   1.102 +  end
   1.103  
   1.104  fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
   1.105      String.isPrefix bound_var_prefix s
   1.106 @@ -953,9 +957,9 @@
   1.107      n_ary_strip_type (n - 1) ran_T |>> cons dom_T
   1.108    | n_ary_strip_type _ _ = raise Fail "unexpected non-function"
   1.109  
   1.110 -fun result_type_of_decl (_, _, T, _, ary) = n_ary_strip_type ary T |> snd
   1.111 +fun result_type_of_decl (_, _, T, _, ary, _) = n_ary_strip_type ary T |> snd
   1.112  
   1.113 -fun decl_line_for_sym s (s', _, T, pred_sym, ary) =
   1.114 +fun decl_line_for_sym s (s', _, T, pred_sym, ary, _) =
   1.115    let val (arg_Ts, res_T) = n_ary_strip_type ary T in
   1.116      Decl (sym_decl_prefix ^ s, (s, s'), map mangled_type_name arg_Ts,
   1.117            if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T)
   1.118 @@ -964,7 +968,7 @@
   1.119  fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
   1.120  
   1.121  fun formula_line_for_sym_decl ctxt nonmono_Ts type_sys n s j
   1.122 -                              (s', T_args, T, _, ary) =
   1.123 +                              (s', T_args, T, _, ary, in_conj) =
   1.124    let
   1.125      val (arg_Ts, res_T) = n_ary_strip_type ary T
   1.126      val bound_names =
   1.127 @@ -976,7 +980,8 @@
   1.128                               else NONE)
   1.129    in
   1.130      Formula (sym_decl_prefix ^ s ^
   1.131 -             (if n > 1 then "_" ^ string_of_int j else ""), Axiom,
   1.132 +             (if n > 1 then "_" ^ string_of_int j else ""),
   1.133 +             if in_conj then Hypothesis else Axiom,
   1.134               CombConst ((s, s'), T, T_args)
   1.135               |> fold (curry (CombApp o swap)) bound_tms
   1.136               |> type_pred_combatom type_sys res_T
   1.137 @@ -1060,7 +1065,7 @@
   1.138      val helpers =
   1.139        repaired_sym_tab |> helper_facts_for_sym_table ctxt type_sys |> map repair
   1.140      val sym_decl_lines =
   1.141 -      conjs @ facts
   1.142 +      (conjs, facts) (* FIXME: what if "True_or_False" is among helpers? *)
   1.143        |> sym_decl_table_for_facts type_sys repaired_sym_tab
   1.144        |> problem_lines_for_sym_decl_table ctxt nonmono_Ts type_sys
   1.145      (* Reordering these might confuse the proof reconstruction code or the SPASS