reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
authorblanchet
Sun May 01 18:37:24 2011 +0200 (2011-05-01)
changeset 4254475cb06eee990
parent 42543 f9d402d144d4
child 42545 a14b602fb3d5
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
src/HOL/Tools/Metis/metis_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
     1.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Sun May 01 18:37:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Sun May 01 18:37:24 2011 +0200
     1.3 @@ -66,6 +66,7 @@
     1.4      theory -> class list -> class list -> class_rel_clause list
     1.5    val make_arity_clauses :
     1.6      theory -> string list -> class list -> class list * arity_clause list
     1.7 +  val dest_combfun : combtyp -> combtyp * combtyp
     1.8    val combtyp_of : combterm -> combtyp
     1.9    val strip_combterm_comb : combterm -> combterm * combterm list
    1.10    val combtyp_from_typ : typ -> combtyp
    1.11 @@ -381,12 +382,12 @@
    1.12  (*********************************************************************)
    1.13  
    1.14  (*Result of a function type; no need to check that the argument type matches.*)
    1.15 -fun result_type (CombType (_, [_, tp2])) = tp2
    1.16 -  | result_type _ = raise Fail "non-function type"
    1.17 +fun dest_combfun (CombType (_, [ty1, ty2])) = (ty1, ty2)
    1.18 +  | dest_combfun _ = raise Fail "non-function type"
    1.19  
    1.20  fun combtyp_of (CombConst (_, tp, _)) = tp
    1.21    | combtyp_of (CombVar (_, tp)) = tp
    1.22 -  | combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1)
    1.23 +  | combtyp_of (CombApp (t1, _)) = snd (dest_combfun (combtyp_of t1))
    1.24  
    1.25  (*gets the head of a combinator application, along with the list of arguments*)
    1.26  fun strip_combterm_comb u =
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     2.3 @@ -341,11 +341,7 @@
     2.4      fun aux opt_T extra_us u =
     2.5        case u of
     2.6          ATerm (a, us) =>
     2.7 -        if a = boolify_name then
     2.8 -          aux (SOME @{typ bool}) [] (hd us)
     2.9 -        else if a = explicit_app_name then
    2.10 -          aux opt_T (nth us 1 :: extra_us) (hd us)
    2.11 -        else if a = type_tag_name then
    2.12 +        if a = type_tag_name then
    2.13            case us of
    2.14              [typ_u, term_u] =>
    2.15              aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u
    2.16 @@ -360,24 +356,29 @@
    2.17                list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
    2.18            end
    2.19          | SOME b =>
    2.20 -          let
    2.21 -            val (c, mangled_us) = b |> unmangled_const |>> invert_const
    2.22 -            val num_ty_args = num_atp_type_args thy type_sys c
    2.23 -            val (type_us, term_us) = chop num_ty_args us |>> append mangled_us
    2.24 -            (* Extra args from "hAPP" come after any arguments given directly to
    2.25 -               the constant. *)
    2.26 -            val term_ts = map (aux NONE []) term_us
    2.27 -            val extra_ts = map (aux NONE []) extra_us
    2.28 -            val T =
    2.29 -              case opt_T of
    2.30 -                SOME T => map fastype_of term_ts ---> T
    2.31 -              | NONE =>
    2.32 -                if num_type_args thy c = length type_us then
    2.33 -                  Sign.const_instance thy (c,
    2.34 -                      map (type_from_fo_term tfrees) type_us)
    2.35 -                else
    2.36 -                  HOLogic.typeT
    2.37 -          in list_comb (Const (c, T), term_ts @ extra_ts) end
    2.38 +          if b = boolify_base then
    2.39 +            aux (SOME @{typ bool}) [] (hd us)
    2.40 +          else if b = explicit_app_base then
    2.41 +            aux opt_T (nth us 1 :: extra_us) (hd us)
    2.42 +          else
    2.43 +            let
    2.44 +              val (c, mangled_us) = b |> unmangled_const |>> invert_const
    2.45 +              val num_ty_args = num_atp_type_args thy type_sys c
    2.46 +              val (type_us, term_us) = chop num_ty_args us |>> append mangled_us
    2.47 +              (* Extra args from "hAPP" come after any arguments given directly
    2.48 +                 to the constant. *)
    2.49 +              val term_ts = map (aux NONE []) term_us
    2.50 +              val extra_ts = map (aux NONE []) extra_us
    2.51 +              val T =
    2.52 +                case opt_T of
    2.53 +                  SOME T => map fastype_of term_ts ---> T
    2.54 +                | NONE =>
    2.55 +                  if num_type_args thy c = length type_us then
    2.56 +                    Sign.const_instance thy (c,
    2.57 +                        map (type_from_fo_term tfrees) type_us)
    2.58 +                  else
    2.59 +                    HOLogic.typeT
    2.60 +            in list_comb (Const (c, T), term_ts @ extra_ts) end
    2.61          | NONE => (* a free or schematic variable *)
    2.62            let
    2.63              val ts = map (aux NONE []) (us @ extra_us)
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
     3.3 @@ -21,14 +21,14 @@
     3.4  
     3.5    val fact_prefix : string
     3.6    val conjecture_prefix : string
     3.7 -  val boolify_name : string
     3.8 -  val explicit_app_name : string
     3.9 +  val boolify_base : string
    3.10 +  val explicit_app_base : string
    3.11    val is_type_system_sound : type_system -> bool
    3.12    val type_system_types_dangerous_types : type_system -> bool
    3.13    val num_atp_type_args : theory -> type_system -> string -> int
    3.14    val unmangled_const : string -> string * string fo_term list
    3.15    val translate_atp_fact :
    3.16 -    Proof.context -> type_system -> bool -> (string * 'a) * thm
    3.17 +    Proof.context -> bool -> (string * 'a) * thm
    3.18      -> translated_formula option * ((string * 'a) * thm)
    3.19    val prepare_atp_problem :
    3.20      Proof.context -> bool -> type_system -> bool -> term list -> term
    3.21 @@ -54,8 +54,8 @@
    3.22  val arity_clause_prefix = "arity_"
    3.23  val tfree_prefix = "tfree_"
    3.24  
    3.25 -val boolify_name = "hBOOL"
    3.26 -val explicit_app_name = "hAPP"
    3.27 +val boolify_base = "hBOOL"
    3.28 +val explicit_app_base = "hAPP"
    3.29  val type_pred_base = "is"
    3.30  val type_prefix = "ty_"
    3.31  
    3.32 @@ -100,9 +100,9 @@
    3.33    (member (op =) [@{const_name HOL.eq}] s orelse
    3.34     case type_sys of
    3.35       Many_Typed => false
    3.36 -   | Tags full_types => full_types
    3.37 -   | Args _ => false
    3.38 -   | Mangled _ => false
    3.39 +   | Tags full_types => full_types orelse s = explicit_app_base
    3.40 +   | Args _ => s = explicit_app_base
    3.41 +   | Mangled _ => s = explicit_app_base
    3.42     | No_Types => true)
    3.43  
    3.44  datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Types
    3.45 @@ -209,28 +209,10 @@
    3.46      (hd ss, map unmangled_type (tl ss))
    3.47    end
    3.48  
    3.49 -fun repair_combterm_consts type_sys =
    3.50 -  let
    3.51 -    fun aux (CombApp tmp) = CombApp (pairself aux tmp)
    3.52 -      | aux (CombConst (name as (s, _), ty, ty_args)) =
    3.53 -        (case strip_prefix_and_unascii const_prefix s of
    3.54 -           NONE => (name, ty_args)
    3.55 -         | SOME s'' =>
    3.56 -           let val s'' = invert_const s'' in
    3.57 -             case type_arg_policy type_sys s'' of
    3.58 -               No_Type_Args => (name, [])
    3.59 -             | Explicit_Type_Args => (name, ty_args)
    3.60 -             | Mangled_Types => (mangled_const_name ty_args name, [])
    3.61 -           end)
    3.62 -        |> (fn (name, ty_args) => CombConst (name, ty, ty_args))
    3.63 -      | aux tm = tm
    3.64 -  in aux end
    3.65 -
    3.66 -fun combformula_for_prop thy type_sys eq_as_iff =
    3.67 +fun combformula_for_prop thy eq_as_iff =
    3.68    let
    3.69      fun do_term bs t ts =
    3.70        combterm_from_term thy bs (Envir.eta_contract t)
    3.71 -      |>> repair_combterm_consts type_sys
    3.72        |>> AAtom ||> union (op =) ts
    3.73      fun do_quant bs q s T t' =
    3.74        let val s = Name.variant (map fst bs) s in
    3.75 @@ -336,7 +318,7 @@
    3.76    in t |> exists_subterm is_Var t ? aux end
    3.77  
    3.78  (* making fact and conjecture formulas *)
    3.79 -fun make_formula ctxt type_sys eq_as_iff presimp name kind t =
    3.80 +fun make_formula ctxt eq_as_iff presimp name kind t =
    3.81    let
    3.82      val thy = Proof_Context.theory_of ctxt
    3.83      val t = t |> Envir.beta_eta_contract
    3.84 @@ -350,21 +332,21 @@
    3.85                |> introduce_combinators_in_term ctxt kind
    3.86                |> kind <> Axiom ? freeze_term
    3.87      val (combformula, ctypes_sorts) =
    3.88 -      combformula_for_prop thy type_sys eq_as_iff t []
    3.89 +      combformula_for_prop thy eq_as_iff t []
    3.90    in
    3.91      {name = name, combformula = combformula, kind = kind,
    3.92       ctypes_sorts = ctypes_sorts}
    3.93    end
    3.94  
    3.95 -fun make_fact ctxt type_sys keep_trivial eq_as_iff presimp ((name, _), th) =
    3.96 +fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, _), th) =
    3.97    case (keep_trivial,
    3.98 -        make_formula ctxt type_sys eq_as_iff presimp name Axiom (prop_of th)) of
    3.99 +        make_formula ctxt eq_as_iff presimp name Axiom (prop_of th)) of
   3.100      (false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) =>
   3.101      NONE
   3.102    | (_, formula) => SOME formula
   3.103 -fun make_conjecture ctxt type_sys ts =
   3.104 +fun make_conjecture ctxt ts =
   3.105    let val last = length ts - 1 in
   3.106 -    map2 (fn j => make_formula ctxt type_sys true true (string_of_int j)
   3.107 +    map2 (fn j => make_formula ctxt true true (string_of_int j)
   3.108                                 (if j = last then Conjecture else Hypothesis))
   3.109           (0 upto last) ts
   3.110    end
   3.111 @@ -397,8 +379,7 @@
   3.112      fun dub c needs_full_types (th, j) =
   3.113        ((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""),
   3.114          false), th)
   3.115 -    fun make_facts eq_as_iff =
   3.116 -      map_filter (make_fact ctxt type_sys false eq_as_iff false)
   3.117 +    fun make_facts eq_as_iff = map_filter (make_fact ctxt false eq_as_iff false)
   3.118    in
   3.119      (metis_helpers
   3.120       |> filter (is_used o fst)
   3.121 @@ -423,8 +404,8 @@
   3.122         [])
   3.123    end
   3.124  
   3.125 -fun translate_atp_fact ctxt type_sys keep_trivial =
   3.126 -  `(make_fact ctxt type_sys keep_trivial true true)
   3.127 +fun translate_atp_fact ctxt keep_trivial =
   3.128 +  `(make_fact ctxt keep_trivial true true)
   3.129  
   3.130  fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts =
   3.131    let
   3.132 @@ -443,7 +424,7 @@
   3.133      val subs = tfree_classes_of_terms all_ts
   3.134      val supers = tvar_classes_of_terms all_ts
   3.135      val tycons = type_consts_of_terms thy all_ts
   3.136 -    val conjs = make_conjecture ctxt type_sys (hyp_ts @ [concl_t])
   3.137 +    val conjs = make_conjecture ctxt (hyp_ts @ [concl_t])
   3.138      val (supers', arity_clauses) =
   3.139        if type_sys = No_Types then ([], [])
   3.140        else make_arity_clauses thy tycons supers
   3.141 @@ -510,6 +491,23 @@
   3.142     ("c_implies", (2, ("c_fimplies", @{const_name Metis.fimplies}))),
   3.143     ("equal", (2, ("c_fequal", @{const_name Metis.fequal})))]
   3.144  
   3.145 +fun repair_combterm_consts type_sys =
   3.146 +  let
   3.147 +    fun aux (CombApp tmp) = CombApp (pairself aux tmp)
   3.148 +      | aux (CombConst (name as (s, _), ty, ty_args)) =
   3.149 +        (case strip_prefix_and_unascii const_prefix s of
   3.150 +           NONE => (name, ty_args)
   3.151 +         | SOME s'' =>
   3.152 +           let val s'' = invert_const s'' in
   3.153 +             case type_arg_policy type_sys s'' of
   3.154 +               No_Type_Args => (name, [])
   3.155 +             | Explicit_Type_Args => (name, ty_args)
   3.156 +             | Mangled_Types => (mangled_const_name ty_args name, [])
   3.157 +           end)
   3.158 +        |> (fn (name, ty_args) => CombConst (name, ty, ty_args))
   3.159 +      | aux tm = tm
   3.160 +  in aux end
   3.161 +
   3.162  fun pred_combtyp ty =
   3.163    case combtyp_from_typ @{typ "unit => bool"} of
   3.164      CombType (name, [_, bool_ty]) => CombType (name, [ty, bool_ty])
   3.165 @@ -637,9 +635,9 @@
   3.166  
   3.167  (** "hBOOL" and "hAPP" **)
   3.168  
   3.169 -type hrepair_info = {min_arity: int, max_arity: int, pred_sym: bool}
   3.170 +type repair_info = {pred_sym: bool, min_arity: int, max_arity: int}
   3.171  
   3.172 -fun consider_combterm_for_hrepair top_level tm =
   3.173 +fun consider_combterm_for_repair top_level tm =
   3.174    let val (head, args) = strip_combterm_comb tm in
   3.175      (case head of
   3.176         CombConst ((s, _), _, _) =>
   3.177 @@ -648,76 +646,50 @@
   3.178         else
   3.179           let val n = length args in
   3.180             Symtab.map_default
   3.181 -               (s, {min_arity = n, max_arity = 0, pred_sym = true})
   3.182 -               (fn {min_arity, max_arity, pred_sym} =>
   3.183 -                   {min_arity = Int.min (n, min_arity),
   3.184 -                    max_arity = Int.max (n, max_arity),
   3.185 -                    pred_sym = pred_sym andalso top_level})
   3.186 +               (s, {pred_sym = true, min_arity = n, max_arity = 0})
   3.187 +               (fn {pred_sym, min_arity, max_arity} =>
   3.188 +                   {pred_sym = pred_sym andalso top_level,
   3.189 +                    min_arity = Int.min (n, min_arity),
   3.190 +                    max_arity = Int.max (n, max_arity)})
   3.191          end
   3.192       | _ => I)
   3.193 -    #> fold (consider_combterm_for_hrepair false) args
   3.194 +    #> fold (consider_combterm_for_repair false) args
   3.195    end
   3.196  
   3.197 -fun consider_fact_for_hrepair ({combformula, ...} : translated_formula) =
   3.198 -  formula_fold (consider_combterm_for_hrepair true) combformula
   3.199 +fun consider_fact_for_repair ({combformula, ...} : translated_formula) =
   3.200 +  formula_fold (consider_combterm_for_repair true) combformula
   3.201  
   3.202  (* The "equal" entry is needed for helper facts if the problem otherwise does
   3.203 -   not involve equality. *)
   3.204 +   not involve equality. The "hBOOL" and "hAPP" entries are needed for symbol
   3.205 +   declarations. *)
   3.206  val default_entries =
   3.207 -  [("equal", {min_arity = 2, max_arity = 2, pred_sym = true}),
   3.208 -   (boolify_name, {min_arity = 1, max_arity = 1, pred_sym = true})]
   3.209 +  [("equal", {pred_sym = true, min_arity = 2, max_arity = 2}),
   3.210 +   (make_fixed_const boolify_base,
   3.211 +    {pred_sym = true, min_arity = 1, max_arity = 1}),
   3.212 +   (make_fixed_const explicit_app_base,
   3.213 +    {pred_sym = false, min_arity = 2, max_arity = 2})]
   3.214 +(* FIXME: last two entries needed? ### *)
   3.215  
   3.216 -fun hrepair_table_for_facts explicit_apply facts =
   3.217 +fun sym_table_for_facts explicit_apply facts =
   3.218    if explicit_apply then
   3.219      NONE
   3.220    else
   3.221      SOME (Symtab.empty |> fold Symtab.default default_entries
   3.222 -                       |> fold consider_fact_for_hrepair facts)
   3.223 -
   3.224 -fun min_arity_of thy type_sys NONE s =
   3.225 -    (if s = "equal" orelse s = type_tag_name orelse
   3.226 -        String.isPrefix type_const_prefix s orelse
   3.227 -        String.isPrefix class_prefix s then
   3.228 -       16383 (* large number *)
   3.229 -     else case strip_prefix_and_unascii const_prefix s of
   3.230 -       SOME s' => s' |> unmangled_const |> fst |> invert_const
   3.231 -                     |> num_atp_type_args thy type_sys
   3.232 -     | NONE => 0)
   3.233 -  | min_arity_of _ _ (SOME hrepairs) s =
   3.234 -    case Symtab.lookup hrepairs s of
   3.235 -      SOME ({min_arity, ...} : hrepair_info) => min_arity
   3.236 -    | NONE => 0
   3.237 -
   3.238 -fun full_type_of (ATerm ((s, _), [ty, _])) =
   3.239 -    if s = type_tag_name then SOME ty else NONE
   3.240 -  | full_type_of _ = NONE
   3.241 +                       |> fold consider_fact_for_repair facts)
   3.242  
   3.243 -fun list_hAPP_rev _ t1 [] = t1
   3.244 -  | list_hAPP_rev NONE t1 (t2 :: ts2) =
   3.245 -    ATerm (`I explicit_app_name, [list_hAPP_rev NONE t1 ts2, t2])
   3.246 -  | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
   3.247 -    case full_type_of t2 of
   3.248 -      SOME ty2 =>
   3.249 -      let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
   3.250 -                           [ty2, ty]) in
   3.251 -        ATerm (`I explicit_app_name,
   3.252 -               [tag_with_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
   3.253 -      end
   3.254 -    | NONE => list_hAPP_rev NONE t1 (t2 :: ts2)
   3.255 -
   3.256 -fun hrepair_applications_in_term thy type_sys hrepairs =
   3.257 -  let
   3.258 -    fun aux opt_ty (ATerm (name as (s, _), ts)) =
   3.259 -      if s = type_tag_name then
   3.260 -        case ts of
   3.261 -          [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
   3.262 -        | _ => raise Fail "malformed type tag"
   3.263 -      else
   3.264 -        let
   3.265 -          val ts = map (aux NONE) ts
   3.266 -          val (ts1, ts2) = chop (min_arity_of thy type_sys hrepairs s) ts
   3.267 -        in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
   3.268 -  in aux NONE end
   3.269 +fun min_arity_of _ _ (SOME sym_tab) s =
   3.270 +    (case Symtab.lookup sym_tab s of
   3.271 +       SOME ({min_arity, ...} : repair_info) => min_arity
   3.272 +     | NONE => 0)
   3.273 +  | min_arity_of thy type_sys NONE s =
   3.274 +    if s = "equal" orelse s = type_tag_name orelse
   3.275 +       String.isPrefix type_const_prefix s orelse
   3.276 +       String.isPrefix class_prefix s then
   3.277 +      16383 (* large number *)
   3.278 +    else case strip_prefix_and_unascii const_prefix s of
   3.279 +      SOME s' => s' |> unmangled_const |> fst |> invert_const
   3.280 +                    |> num_atp_type_args thy type_sys
   3.281 +    | NONE => 0
   3.282  
   3.283  (* True if the constant ever appears outside of the top-level position in
   3.284     literals, or if it appears with different arities (e.g., because of different
   3.285 @@ -726,88 +698,120 @@
   3.286  fun is_pred_sym NONE s =
   3.287      s = "equal" orelse s = "$false" orelse s = "$true" orelse
   3.288      String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s
   3.289 -  | is_pred_sym (SOME hrepairs) s =
   3.290 -    case Symtab.lookup hrepairs s of
   3.291 -      SOME {min_arity, max_arity, pred_sym} =>
   3.292 +  | is_pred_sym (SOME sym_tab) s =
   3.293 +    case Symtab.lookup sym_tab s of
   3.294 +      SOME {pred_sym, min_arity, max_arity} =>
   3.295        pred_sym andalso min_arity = max_arity
   3.296      | NONE => false
   3.297  
   3.298  val boolify_combconst =
   3.299 -  CombConst (`I boolify_name, combtyp_from_typ @{typ "bool => bool"}, [])
   3.300 +  CombConst (`make_fixed_const boolify_base,
   3.301 +             combtyp_from_typ @{typ "bool => bool"}, [])
   3.302  fun boolify tm = CombApp (boolify_combconst, tm)
   3.303  
   3.304 -fun hrepair_pred_syms_in_combterm hrepairs tm =
   3.305 +fun repair_pred_syms_in_combterm sym_tab tm =
   3.306    case strip_combterm_comb tm of
   3.307      (CombConst ((s, _), _, _), _) =>
   3.308 -    if is_pred_sym hrepairs s then tm else boolify tm
   3.309 +    if is_pred_sym sym_tab s then tm else boolify tm
   3.310    | _ => boolify tm
   3.311  
   3.312 -fun hrepair_apps_in_combterm hrepairs tm = tm
   3.313 +fun list_app head args = fold (curry (CombApp o swap)) args head
   3.314 +
   3.315 +val fun_name = `make_fixed_type_const @{type_name fun}
   3.316 +
   3.317 +fun explicit_app arg head =
   3.318 +  let
   3.319 +    val head_ty = combtyp_of head
   3.320 +    val (arg_ty, res_ty) = dest_combfun head_ty
   3.321 +    val explicit_app =
   3.322 +      CombConst (`make_fixed_const explicit_app_base,
   3.323 +                 CombType (fun_name, [head_ty, head_ty]), [arg_ty, res_ty])
   3.324 +  in list_app explicit_app [head, arg] end
   3.325 +fun list_explicit_app head args = fold explicit_app args head
   3.326  
   3.327 -fun hrepair_combterm type_sys hrepairs =
   3.328 -  (case type_sys of Tags _ => I | _ => hrepair_pred_syms_in_combterm hrepairs)
   3.329 -  #> hrepair_apps_in_combterm hrepairs
   3.330 -val hrepair_combformula = formula_map oo hrepair_combterm
   3.331 -val hrepair_fact = map_combformula oo hrepair_combformula
   3.332 +fun repair_apps_in_combterm thy type_sys sym_tab =
   3.333 +  let
   3.334 +    fun aux tm =
   3.335 +      case strip_combterm_comb tm of
   3.336 +        (head as CombConst ((s, _), _, _), args) =>
   3.337 +        args |> map aux
   3.338 +             |> chop (min_arity_of thy type_sys sym_tab s)
   3.339 +             |>> list_app head
   3.340 +             |-> list_explicit_app
   3.341 +      | (head, args) => list_explicit_app head (map aux args)
   3.342 +  in aux end
   3.343  
   3.344 -fun is_const_relevant type_sys hrepairs s =
   3.345 +fun repair_combterm thy type_sys sym_tab =
   3.346 +  (case type_sys of Tags _ => I | _ => repair_pred_syms_in_combterm sym_tab)
   3.347 +  #> repair_apps_in_combterm thy type_sys sym_tab
   3.348 +  #> repair_combterm_consts type_sys
   3.349 +val repair_combformula = formula_map ooo repair_combterm
   3.350 +val repair_fact = map_combformula ooo repair_combformula
   3.351 +
   3.352 +fun is_const_relevant type_sys sym_tab s =
   3.353    not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
   3.354 -  (type_sys = Many_Typed orelse not (is_pred_sym hrepairs s))
   3.355 +  (type_sys = Many_Typed orelse not (is_pred_sym sym_tab s))
   3.356  
   3.357 -fun consider_combterm_consts type_sys hrepairs tm =
   3.358 +fun consider_combterm_consts type_sys sym_tab tm =
   3.359    let val (head, args) = strip_combterm_comb tm in
   3.360      (case head of
   3.361         CombConst ((s, s'), ty, ty_args) =>
   3.362         (* FIXME: exploit type subsumption *)
   3.363 -       is_const_relevant type_sys hrepairs s
   3.364 +       is_const_relevant type_sys sym_tab s
   3.365         ? Symtab.insert_list (op =) (s, (s', ty_args, ty))
   3.366 -     | _ => I) (* FIXME: hAPP on var *)
   3.367 -    #> fold (consider_combterm_consts type_sys hrepairs) args
   3.368 +     | _ => I)
   3.369 +    #> fold (consider_combterm_consts type_sys sym_tab) args
   3.370    end
   3.371  
   3.372 -fun consider_fact_consts type_sys hrepairs
   3.373 +fun consider_fact_consts type_sys sym_tab
   3.374                           ({combformula, ...} : translated_formula) =
   3.375 -  formula_fold (consider_combterm_consts type_sys hrepairs) combformula
   3.376 +  formula_fold (consider_combterm_consts type_sys sym_tab) combformula
   3.377  
   3.378 -fun const_table_for_facts type_sys hrepairs facts =
   3.379 +fun const_table_for_facts type_sys sym_tab facts =
   3.380    Symtab.empty |> member (op =) [Many_Typed, Args true, Mangled true] type_sys
   3.381 -                  ? fold (consider_fact_consts type_sys hrepairs) facts
   3.382 +                  ? fold (consider_fact_consts type_sys sym_tab) facts
   3.383  
   3.384 -fun strip_and_map_combtyp f (ty as CombType ((s, _), tys)) =
   3.385 +fun strip_and_map_combtyp 0 f ty = ([], f ty)
   3.386 +  | strip_and_map_combtyp n f (ty as CombType ((s, _), tys)) =
   3.387      (case (strip_prefix_and_unascii type_const_prefix s, tys) of
   3.388         (SOME @{type_name fun}, [dom_ty, ran_ty]) =>
   3.389 -       strip_and_map_combtyp f ran_ty |>> cons (f dom_ty)
   3.390 +       strip_and_map_combtyp (n - 1) f ran_ty |>> cons (f dom_ty)
   3.391       | _ => ([], f ty))
   3.392 -  | strip_and_map_combtyp f ty = ([], f ty)
   3.393 +  | strip_and_map_combtyp _ _ _ = raise Fail "unexpected non-function"
   3.394  
   3.395 -fun sym_decl_line_for_const_entry ctxt type_sys hrepairs s (s', ty_args, ty) =
   3.396 -  if type_sys = Many_Typed then
   3.397 -    let
   3.398 -      val (arg_tys, res_ty) = strip_and_map_combtyp mangled_combtyp ty
   3.399 -      val (s, s') = (s, s') |> mangled_const_name ty_args
   3.400 -    in
   3.401 -      Decl (sym_decl_prefix ^ ascii_of s, (s, s'), arg_tys,
   3.402 -            if is_pred_sym hrepairs s then `I tff_bool_type else res_ty)
   3.403 -    end
   3.404 -  else
   3.405 -    let
   3.406 -      val (arg_tys, res_ty) = strip_and_map_combtyp I ty
   3.407 -      val bounds =
   3.408 -        map (`I o make_bound_var o string_of_int) (1 upto length arg_tys)
   3.409 -        ~~ map SOME arg_tys
   3.410 -      val bound_tms =
   3.411 -        map (fn (name, ty) => CombConst (name, the ty, [])) bounds
   3.412 -    in
   3.413 -      Formula (Fof, sym_decl_prefix ^ ascii_of s, Axiom,
   3.414 -               CombConst ((s, s'), ty, ty_args)
   3.415 -               |> fold (curry (CombApp o swap)) bound_tms
   3.416 -               |> type_pred_combatom type_sys res_ty
   3.417 -               |> mk_aquant AForall bounds
   3.418 -               |> formula_for_combformula ctxt type_sys,
   3.419 -               NONE, NONE)
   3.420 -    end
   3.421 -fun sym_decl_lines_for_const ctxt type_sys hrepairs (s, xs) =
   3.422 -  map (sym_decl_line_for_const_entry ctxt type_sys hrepairs s) xs
   3.423 +fun sym_decl_line_for_const_entry ctxt type_sys sym_tab s (s', ty_args, ty) =
   3.424 +  let
   3.425 +    val thy = Proof_Context.theory_of ctxt
   3.426 +    val arity = min_arity_of thy type_sys sym_tab s
   3.427 +  in
   3.428 +    if type_sys = Many_Typed then
   3.429 +      let
   3.430 +        val (arg_tys, res_ty) = strip_and_map_combtyp arity mangled_combtyp ty
   3.431 +        val (s, s') = (s, s') |> mangled_const_name ty_args
   3.432 +      in
   3.433 +        Decl (sym_decl_prefix ^ ascii_of s, (s, s'), arg_tys,
   3.434 +              if is_pred_sym sym_tab s then `I tff_bool_type else res_ty)
   3.435 +      end
   3.436 +    else
   3.437 +      let
   3.438 +        val (arg_tys, res_ty) = strip_and_map_combtyp arity I ty
   3.439 +        val bounds =
   3.440 +          map (`I o make_bound_var o string_of_int) (1 upto length arg_tys)
   3.441 +          ~~ map SOME arg_tys
   3.442 +        val bound_tms =
   3.443 +          map (fn (name, ty) => CombConst (name, the ty, [])) bounds
   3.444 +      in
   3.445 +        Formula (Fof, sym_decl_prefix ^ ascii_of s, Axiom,
   3.446 +                 CombConst ((s, s'), ty, ty_args)
   3.447 +                 |> fold (curry (CombApp o swap)) bound_tms
   3.448 +                 |> type_pred_combatom type_sys res_ty
   3.449 +                 |> mk_aquant AForall bounds
   3.450 +                 |> formula_for_combformula ctxt type_sys,
   3.451 +                 NONE, NONE)
   3.452 +      end
   3.453 +  end
   3.454 +fun sym_decl_lines_for_const ctxt type_sys sym_tab (s, xs) =
   3.455 +  map (sym_decl_line_for_const_entry ctxt type_sys sym_tab s) xs
   3.456  
   3.457  fun add_tff_types_in_formula (AQuant (_, xs, phi)) =
   3.458      union (op =) (map_filter snd xs) #> add_tff_types_in_formula phi
   3.459 @@ -827,7 +831,7 @@
   3.460    Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tff_type_of_types)
   3.461  
   3.462  val type_declsN = "Types"
   3.463 -val sym_declsN = "Symbols"
   3.464 +val sym_declsN = "Symbol types"
   3.465  val factsN = "Relevant facts"
   3.466  val class_relsN = "Class relationships"
   3.467  val aritiesN = "Arities"
   3.468 @@ -843,11 +847,13 @@
   3.469  fun prepare_atp_problem ctxt readable_names type_sys explicit_apply hyp_ts
   3.470                          concl_t facts =
   3.471    let
   3.472 +    val thy = Proof_Context.theory_of ctxt
   3.473      val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
   3.474        translate_formulas ctxt type_sys hyp_ts concl_t facts
   3.475 -    val hrepairs = hrepair_table_for_facts explicit_apply (conjs @ facts)
   3.476 -    val conjs = map (hrepair_fact type_sys hrepairs) conjs
   3.477 -    val facts = map (hrepair_fact type_sys hrepairs) facts
   3.478 +    val sym_tab = sym_table_for_facts explicit_apply (conjs @ facts)
   3.479 +    val conjs = map (repair_fact thy type_sys sym_tab) conjs
   3.480 +    val facts = map (repair_fact thy type_sys sym_tab) facts
   3.481 +    val sym_tab = sym_table_for_facts explicit_apply (conjs @ facts)
   3.482      (* Reordering these might confuse the proof reconstruction code or the SPASS
   3.483         Flotter hack. *)
   3.484      val problem =
   3.485 @@ -864,10 +870,10 @@
   3.486        problem |> maps (map_filter (fn Formula (_, _, _, phi, _, _) => SOME phi
   3.487                                      | _ => NONE) o snd)
   3.488                |> get_helper_facts ctxt type_sys
   3.489 -              |>> map (hrepair_fact type_sys hrepairs)
   3.490 -    val const_tab = const_table_for_facts type_sys hrepairs (conjs @ facts)
   3.491 +              |>> map (repair_fact thy type_sys sym_tab)
   3.492 +    val const_tab = const_table_for_facts type_sys sym_tab (conjs @ facts)
   3.493      val sym_decl_lines =
   3.494 -      Symtab.fold_rev (append o sym_decl_lines_for_const ctxt type_sys hrepairs)
   3.495 +      Symtab.fold_rev (append o sym_decl_lines_for_const ctxt type_sys sym_tab)
   3.496                        const_tab []
   3.497      val helper_lines =
   3.498        helper_facts
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:24 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:24 2011 +0200
     4.3 @@ -313,9 +313,9 @@
     4.4  fun untranslated_fact (Untranslated_Fact p) = p
     4.5    | untranslated_fact (ATP_Translated_Fact (_, p)) = p
     4.6    | untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th)
     4.7 -fun atp_translated_fact _ _ (ATP_Translated_Fact p) = p
     4.8 -  | atp_translated_fact ctxt type_sys fact =
     4.9 -    translate_atp_fact ctxt type_sys false (untranslated_fact fact)
    4.10 +fun atp_translated_fact _ (ATP_Translated_Fact p) = p
    4.11 +  | atp_translated_fact ctxt fact =
    4.12 +    translate_atp_fact ctxt false (untranslated_fact fact)
    4.13  fun smt_weighted_fact _ _ (SMT_Weighted_Fact p, _) = p
    4.14    | smt_weighted_fact thy num_facts (fact, j) =
    4.15      (untranslated_fact fact, j) |> weight_smt_fact thy num_facts
    4.16 @@ -415,7 +415,7 @@
    4.17                             ? filter_out (member (op =) blacklist o fst
    4.18                                           o untranslated_fact)
    4.19                          |> monomorphize ? monomorphize_facts
    4.20 -                        |> map (atp_translated_fact ctxt type_sys)
    4.21 +                        |> map (atp_translated_fact ctxt)
    4.22                  val real_ms = Real.fromInt o Time.toMilliseconds
    4.23                  val slice_timeout =
    4.24                    ((real_ms time_left
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sun May 01 18:37:24 2011 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Sun May 01 18:37:24 2011 +0200
     5.3 @@ -250,8 +250,7 @@
     5.4                (if monomorphize then
     5.5                   K (Untranslated_Fact o fst)
     5.6                 else
     5.7 -                 ATP_Translated_Fact
     5.8 -                 oo K (translate_atp_fact ctxt type_sys false o fst))
     5.9 +                 ATP_Translated_Fact oo K (translate_atp_fact ctxt false o fst))
    5.10                (K (K NONE)) atps
    5.11        fun launch_smts accum =
    5.12          if null smts then