src/HOL/Tools/ATP/atp_problem_generate.ML
changeset 47932 ce4178e037a7
parent 47925 481e5379c4ef
child 47935 631ea563c20a
     1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 16 18:16:51 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed May 16 18:16:51 2012 +0200
     1.3 @@ -539,11 +539,14 @@
     1.4    [new_skolem_const_prefix, s, string_of_int num_T_args]
     1.5    |> Long_Name.implode
     1.6  
     1.7 +val alpha_to_beta = Logic.varifyT_global @{typ "'a => 'b"}
     1.8 +val alpha_to_beta_to_alpha_to_beta = alpha_to_beta --> alpha_to_beta
     1.9 +
    1.10  fun robust_const_type thy s =
    1.11    if s = app_op_name then
    1.12 -    Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
    1.13 +    alpha_to_beta_to_alpha_to_beta
    1.14    else if String.isPrefix lam_lifted_prefix s then
    1.15 -    Logic.varifyT_global @{typ "'a => 'b"}
    1.16 +    alpha_to_beta
    1.17    else
    1.18      (* Old Skolems throw a "TYPE" exception here, which will be caught. *)
    1.19      s |> Sign.the_const_type thy
    1.20 @@ -929,6 +932,7 @@
    1.21    | add_iterm_vars bounds (IVar (name, T)) =
    1.22      not (member (op =) bounds name) ? insert (op =) (name, SOME T)
    1.23    | add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
    1.24 +
    1.25  fun close_iformula_universally phi = close_universally add_iterm_vars phi
    1.26  
    1.27  val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
    1.28 @@ -1442,7 +1446,7 @@
    1.29    Sufficient_App_Op_And_Predicator |
    1.30    Full_App_Op_And_Predicator
    1.31  
    1.32 -fun sym_table_for_facts ctxt type_enc app_op_level conjs facts =
    1.33 +fun add_iterm_syms_to_sym_table ctxt app_op_level conj_fact =
    1.34    let
    1.35      val thy = Proof_Context.theory_of ctxt
    1.36      fun consider_var_ary const_T var_T max_ary =
    1.37 @@ -1478,80 +1482,85 @@
    1.38          end
    1.39        else
    1.40          accum
    1.41 -      fun add_iterm_syms conj_fact top_level tm
    1.42 -                         (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
    1.43 -        let val (head, args) = strip_iterm_comb tm in
    1.44 -          (case head of
    1.45 -             IConst ((s, _), T, _) =>
    1.46 -             if String.isPrefix bound_var_prefix s orelse
    1.47 -                String.isPrefix all_bound_var_prefix s then
    1.48 -               add_universal_var T accum
    1.49 -             else if String.isPrefix exist_bound_var_prefix s then
    1.50 -               accum
    1.51 -             else
    1.52 -               let val ary = length args in
    1.53 -                 ((bool_vars, fun_var_Ts),
    1.54 -                  case Symtab.lookup sym_tab s of
    1.55 -                    SOME {pred_sym, min_ary, max_ary, types, in_conj} =>
    1.56 -                    let
    1.57 -                      val pred_sym =
    1.58 -                        pred_sym andalso top_level andalso not bool_vars
    1.59 -                      val types' = types |> insert_type thy I T
    1.60 -                      val in_conj = in_conj orelse conj_fact
    1.61 -                      val min_ary =
    1.62 -                        if (app_op_level = Sufficient_App_Op orelse
    1.63 -                            app_op_level = Sufficient_App_Op_And_Predicator)
    1.64 -                           andalso not (pointer_eq (types', types)) then
    1.65 -                          fold (consider_var_ary T) fun_var_Ts min_ary
    1.66 -                        else
    1.67 -                          min_ary
    1.68 -                    in
    1.69 -                      Symtab.update (s, {pred_sym = pred_sym,
    1.70 -                                         min_ary = Int.min (ary, min_ary),
    1.71 -                                         max_ary = Int.max (ary, max_ary),
    1.72 -                                         types = types', in_conj = in_conj})
    1.73 -                                    sym_tab
    1.74 -                    end
    1.75 -                  | NONE =>
    1.76 -                    let
    1.77 -                      val pred_sym = top_level andalso not bool_vars
    1.78 -                      val ary =
    1.79 -                        case unprefix_and_unascii const_prefix s of
    1.80 -                          SOME s =>
    1.81 -                          (if String.isSubstring uncurried_alias_sep s then
    1.82 -                             ary
    1.83 -                           else case try (robust_const_ary thy
    1.84 -                                          o invert_const o hd
    1.85 -                                          o unmangled_const_name) s of
    1.86 -                             SOME ary0 => Int.min (ary0, ary)
    1.87 -                           | NONE => ary)
    1.88 -                        | NONE => ary
    1.89 -                      val min_ary =
    1.90 -                        case app_op_level of
    1.91 -                          Min_App_Op => ary
    1.92 -                        | Full_App_Op_And_Predicator => 0
    1.93 -                        | _ => fold (consider_var_ary T) fun_var_Ts ary
    1.94 -                    in
    1.95 -                      Symtab.update_new (s,
    1.96 -                          {pred_sym = pred_sym, min_ary = min_ary,
    1.97 -                           max_ary = ary, types = [T], in_conj = conj_fact})
    1.98 -                          sym_tab
    1.99 -                    end)
   1.100 -               end
   1.101 -           | IVar (_, T) => add_universal_var T accum
   1.102 -           | IAbs ((_, T), tm) =>
   1.103 -             accum |> add_universal_var T |> add_iterm_syms conj_fact false tm
   1.104 -           | _ => accum)
   1.105 -          |> fold (add_iterm_syms conj_fact false) args
   1.106 -        end
   1.107 +    fun add_iterm_syms top_level tm
   1.108 +                       (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
   1.109 +      let val (head, args) = strip_iterm_comb tm in
   1.110 +        (case head of
   1.111 +           IConst ((s, _), T, _) =>
   1.112 +           if String.isPrefix bound_var_prefix s orelse
   1.113 +              String.isPrefix all_bound_var_prefix s then
   1.114 +             add_universal_var T accum
   1.115 +           else if String.isPrefix exist_bound_var_prefix s then
   1.116 +             accum
   1.117 +           else
   1.118 +             let val ary = length args in
   1.119 +               ((bool_vars, fun_var_Ts),
   1.120 +                case Symtab.lookup sym_tab s of
   1.121 +                  SOME {pred_sym, min_ary, max_ary, types, in_conj} =>
   1.122 +                  let
   1.123 +                    val pred_sym =
   1.124 +                      pred_sym andalso top_level andalso not bool_vars
   1.125 +                    val types' = types |> insert_type thy I T
   1.126 +                    val in_conj = in_conj orelse conj_fact
   1.127 +                    val min_ary =
   1.128 +                      if (app_op_level = Sufficient_App_Op orelse
   1.129 +                          app_op_level = Sufficient_App_Op_And_Predicator)
   1.130 +                         andalso not (pointer_eq (types', types)) then
   1.131 +                        fold (consider_var_ary T) fun_var_Ts min_ary
   1.132 +                      else
   1.133 +                        min_ary
   1.134 +                  in
   1.135 +                    Symtab.update (s, {pred_sym = pred_sym,
   1.136 +                                       min_ary = Int.min (ary, min_ary),
   1.137 +                                       max_ary = Int.max (ary, max_ary),
   1.138 +                                       types = types', in_conj = in_conj})
   1.139 +                                  sym_tab
   1.140 +                  end
   1.141 +                | NONE =>
   1.142 +                  let
   1.143 +                    val pred_sym = top_level andalso not bool_vars
   1.144 +                    val ary =
   1.145 +                      case unprefix_and_unascii const_prefix s of
   1.146 +                        SOME s =>
   1.147 +                        (if String.isSubstring uncurried_alias_sep s then
   1.148 +                           ary
   1.149 +                         else case try (robust_const_ary thy
   1.150 +                                        o invert_const o hd
   1.151 +                                        o unmangled_const_name) s of
   1.152 +                           SOME ary0 => Int.min (ary0, ary)
   1.153 +                         | NONE => ary)
   1.154 +                      | NONE => ary
   1.155 +                    val min_ary =
   1.156 +                      case app_op_level of
   1.157 +                        Min_App_Op => ary
   1.158 +                      | Full_App_Op_And_Predicator => 0
   1.159 +                      | _ => fold (consider_var_ary T) fun_var_Ts ary
   1.160 +                  in
   1.161 +                    Symtab.update_new (s,
   1.162 +                        {pred_sym = pred_sym, min_ary = min_ary,
   1.163 +                         max_ary = ary, types = [T], in_conj = conj_fact})
   1.164 +                        sym_tab
   1.165 +                  end)
   1.166 +             end
   1.167 +         | IVar (_, T) => add_universal_var T accum
   1.168 +         | IAbs ((_, T), tm) =>
   1.169 +           accum |> add_universal_var T |> add_iterm_syms false tm
   1.170 +         | _ => accum)
   1.171 +        |> fold (add_iterm_syms false) args
   1.172 +      end
   1.173 +  in add_iterm_syms end
   1.174 +
   1.175 +fun sym_table_for_facts ctxt type_enc app_op_level conjs facts =
   1.176 +  let
   1.177 +    fun add_iterm_syms conj_fact =
   1.178 +      add_iterm_syms_to_sym_table ctxt app_op_level conj_fact true
   1.179      fun add_fact_syms conj_fact =
   1.180 -      K (add_iterm_syms conj_fact true) |> formula_fold NONE |> fact_lift
   1.181 +      K (add_iterm_syms conj_fact) |> formula_fold NONE |> fact_lift
   1.182    in
   1.183      ((false, []), Symtab.empty)
   1.184      |> fold (add_fact_syms true) conjs
   1.185      |> fold (add_fact_syms false) facts
   1.186 -    |> snd
   1.187 -    |> fold Symtab.update (default_sym_tab_entries type_enc)
   1.188 +    ||> fold Symtab.update (default_sym_tab_entries type_enc)
   1.189    end
   1.190  
   1.191  fun min_ary_of sym_tab s =
   1.192 @@ -1637,6 +1646,8 @@
   1.193     (("COMBC", false), @{thms Meson.COMBC_def}),
   1.194     (("COMBS", false), @{thms Meson.COMBS_def}),
   1.195     ((predicator_name, false), [not_ffalse, ftrue]),
   1.196 +   (* FIXME: Metis doesn't like existentials in helpers *)
   1.197 +   ((app_op_name, true), [@{lemma "EX x. ~ f x = g x | f = g" by blast}]),
   1.198     (("fFalse", false), [not_ffalse]),
   1.199     (("fFalse", true), @{thms True_or_False}),
   1.200     (("fTrue", false), [ftrue]),
   1.201 @@ -1708,14 +1719,19 @@
   1.202          (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
   1.203          (if needs_fairly_sound then typed_helper_suffix
   1.204           else untyped_helper_suffix)
   1.205 -      fun dub_and_inst needs_fairly_sound (th, j) =
   1.206 -        let val t = th |> prop_of in
   1.207 -          if should_specialize_helper type_enc t then
   1.208 -            map (fn T => specialize_type thy (invert_const unmangled_s, T) t)
   1.209 -                types
   1.210 -          else
   1.211 -            [t]
   1.212 -        end
   1.213 +      fun specialize_helper t T =
   1.214 +        if unmangled_s = app_op_name then
   1.215 +          let
   1.216 +            val tyenv =
   1.217 +              Sign.typ_match thy (alpha_to_beta, domain_type T) Vartab.empty
   1.218 +          in monomorphic_term tyenv t end
   1.219 +        else
   1.220 +          specialize_type thy (invert_const unmangled_s, T) t
   1.221 +      fun dub_and_inst needs_fairly_sound (t, j) =
   1.222 +        (if should_specialize_helper type_enc t then
   1.223 +           map (specialize_helper t) types
   1.224 +         else
   1.225 +           [t])
   1.226          |> tag_list 1
   1.227          |> map (fn (k, t) => ((dub needs_fairly_sound j k, (Global, Def)), t))
   1.228        val make_facts = map_filter (make_fact ctxt format type_enc false)
   1.229 @@ -1727,7 +1743,7 @@
   1.230                   I
   1.231                 else
   1.232                   ths ~~ (1 upto length ths)
   1.233 -                 |> maps (dub_and_inst needs_fairly_sound)
   1.234 +                 |> maps (dub_and_inst needs_fairly_sound o apfst prop_of)
   1.235                   |> make_facts
   1.236                   |> union (op = o pairself #iformula))
   1.237             helper_table
   1.238 @@ -1779,7 +1795,7 @@
   1.239        (head |> dest_Const |> fst,
   1.240         fold_rev (fn t as Var ((s, _), T) =>
   1.241                      (fn u => Abs (s, T, abstract_over (t, u)))
   1.242 -                  | _ => raise Fail "expected Var") args u)
   1.243 +                  | _ => raise Fail "expected \"Var\"") args u)
   1.244      end
   1.245    | extract_lambda_def _ = raise Fail "malformed lifted lambda"
   1.246  
   1.247 @@ -2611,7 +2627,8 @@
   1.248           lifted) =
   1.249        translate_formulas ctxt prem_kind format type_enc lam_trans preproc hyp_ts
   1.250                           concl_t facts
   1.251 -    val sym_tab0 = sym_table_for_facts ctxt type_enc app_op_level conjs facts
   1.252 +    val (_, sym_tab0) =
   1.253 +      sym_table_for_facts ctxt type_enc app_op_level conjs facts
   1.254      val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
   1.255      val (polym_constrs, monom_constrs) =
   1.256        all_constrs_of_polymorphic_datatypes thy
   1.257 @@ -2620,16 +2637,21 @@
   1.258        firstorderize_fact thy monom_constrs type_enc sym_tab0
   1.259                           (uncurried_aliases andalso not in_helper)
   1.260      val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false))
   1.261 -    val sym_tab = sym_table_for_facts ctxt type_enc Min_App_Op conjs facts
   1.262 +    val (ho_stuff, sym_tab) =
   1.263 +      sym_table_for_facts ctxt type_enc Min_App_Op conjs facts
   1.264 +    val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
   1.265 +      uncurried_alias_lines_for_sym_table ctxt monom_constrs mono type_enc
   1.266 +                                          uncurried_aliases sym_tab0 sym_tab
   1.267 +    val (_, sym_tab) =
   1.268 +      (ho_stuff, sym_tab)
   1.269 +      |> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false)
   1.270 +              uncurried_alias_eq_tms
   1.271      val helpers =
   1.272        sym_tab |> helper_facts_for_sym_table ctxt format type_enc
   1.273                |> map (firstorderize true)
   1.274      val mono_Ts =
   1.275        helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc
   1.276      val class_decl_lines = decl_lines_for_classes type_enc classes
   1.277 -    val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) =
   1.278 -      uncurried_alias_lines_for_sym_table ctxt monom_constrs mono type_enc
   1.279 -                                          uncurried_aliases sym_tab0 sym_tab
   1.280      val sym_decl_lines =
   1.281        (conjs, helpers @ facts, uncurried_alias_eq_tms)
   1.282        |> sym_decl_table_for_facts thy type_enc sym_tab