no needless "fequal" proxies if "explicit_apply" is set + always have readable names
authorblanchet
Sun May 01 18:37:24 2011 +0200 (2011-05-01)
changeset 425687b9801a34836
parent 42567 d012947edd36
child 42569 5737947e4c77
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     1.3 @@ -359,7 +359,7 @@
     1.4            end
     1.5          | SOME b =>
     1.6            let val (b, mangled_us) = b |> unmangled_const |>> invert_const in
     1.7 -            if b = boolify_base then
     1.8 +            if b = predicator_base then
     1.9                aux (SOME @{typ bool}) [] (hd us)
    1.10              else if b = explicit_app_base then
    1.11                aux opt_T (nth us 1 :: extra_us) (hd us)
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
     2.3 @@ -19,9 +19,10 @@
     2.4      Tags of bool |
     2.5      No_Types
     2.6  
     2.7 +  val readable_names : bool Unsynchronized.ref
     2.8    val fact_prefix : string
     2.9    val conjecture_prefix : string
    2.10 -  val boolify_base : string
    2.11 +  val predicator_base : string
    2.12    val explicit_app_base : string
    2.13    val type_pred_base : string
    2.14    val tff_type_prefix : string
    2.15 @@ -33,7 +34,7 @@
    2.16      Proof.context -> bool -> (string * 'a) * thm
    2.17      -> translated_formula option * ((string * 'a) * thm)
    2.18    val prepare_atp_problem :
    2.19 -    Proof.context -> bool -> type_system -> bool -> term list -> term
    2.20 +    Proof.context -> type_system -> bool -> term list -> term
    2.21      -> (translated_formula option * ((string * 'a) * thm)) list
    2.22      -> string problem * string Symtab.table * int * int
    2.23         * (string * 'a) list vector
    2.24 @@ -47,6 +48,10 @@
    2.25  open Metis_Translate
    2.26  open Sledgehammer_Util
    2.27  
    2.28 +(* Readable names are often much shorter, especially if types are mangled in
    2.29 +   names. For that reason, they are on by default. *)
    2.30 +val readable_names = Unsynchronized.ref true
    2.31 +
    2.32  val type_decl_prefix = "type_"
    2.33  val sym_decl_prefix = "sym_"
    2.34  val fact_prefix = "fact_"
    2.35 @@ -56,16 +61,18 @@
    2.36  val arity_clause_prefix = "arity_"
    2.37  val tfree_prefix = "tfree_"
    2.38  
    2.39 -val boolify_base = "hBOOL"
    2.40 +val predicator_base = "hBOOL"
    2.41  val explicit_app_base = "hAPP"
    2.42  val type_pred_base = "is"
    2.43  val tff_type_prefix = "ty_"
    2.44  
    2.45  fun make_tff_type s = tff_type_prefix ^ ascii_of s
    2.46  
    2.47 -(* official TPTP TFF syntax *)
    2.48 -val tff_type_of_types = "$tType"
    2.49 -val tff_bool_type = "$o"
    2.50 +(* official TPTP syntax *)
    2.51 +val tptp_tff_type_of_types = "$tType"
    2.52 +val tptp_tff_bool_type = "$o"
    2.53 +val tptp_false = "$false"
    2.54 +val tptp_true = "$true"
    2.55  
    2.56  (* Freshness almost guaranteed! *)
    2.57  val sledgehammer_weak_prefix = "Sledgehammer:"
    2.58 @@ -214,11 +221,31 @@
    2.59      (hd ss, map unmangled_type (tl ss))
    2.60    end
    2.61  
    2.62 +val introduce_proxies =
    2.63 +  let
    2.64 +    fun aux top_level (CombApp (tm1, tm2)) =
    2.65 +        CombApp (aux top_level tm1, aux false tm2)
    2.66 +      | aux top_level (CombConst (name as (s, s'), ty, ty_args)) =
    2.67 +        (case AList.lookup (op =) metis_proxies s of
    2.68 +           SOME proxy_base =>
    2.69 +           if top_level then
    2.70 +             (case s of
    2.71 +                "c_False" => (tptp_false, s')
    2.72 +              | "c_True" => (tptp_true, s')
    2.73 +              | _ => name, [])
    2.74 +            else
    2.75 +              (proxy_base |>> prefix const_prefix, ty_args)
    2.76 +          | NONE => (name, ty_args))
    2.77 +        |> (fn (name, ty_args) => CombConst (name, ty, ty_args))
    2.78 +      | aux _ tm = tm
    2.79 +  in aux true end
    2.80 +
    2.81  fun combformula_from_prop thy eq_as_iff =
    2.82    let
    2.83 -    fun do_term bs t ts =
    2.84 +    fun do_term bs t atomic_types =
    2.85        combterm_from_term thy bs (Envir.eta_contract t)
    2.86 -      |>> AAtom ||> union (op =) ts
    2.87 +      |>> (introduce_proxies #> AAtom)
    2.88 +      ||> union (op =) atomic_types
    2.89      fun do_quant bs q s T t' =
    2.90        let val s = Name.variant (map fst bs) s in
    2.91          do_formula ((s, T) :: bs) t'
    2.92 @@ -443,25 +470,6 @@
    2.93      (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
    2.94    end
    2.95  
    2.96 -val introduce_proxies =
    2.97 -  let
    2.98 -    fun aux top_level (CombApp (tm1, tm2)) =
    2.99 -        CombApp (aux top_level tm1, aux false tm2)
   2.100 -      | aux top_level (CombConst (name as (s, s'), ty, ty_args)) =
   2.101 -        (case AList.lookup (op =) metis_proxies s of
   2.102 -           SOME proxy_base =>
   2.103 -           if top_level then
   2.104 -             (case s of
   2.105 -                "c_False" => ("$false", s')
   2.106 -              | "c_True" => ("$true", s')
   2.107 -              | _ => name, [])
   2.108 -            else
   2.109 -              (proxy_base |>> prefix const_prefix, ty_args)
   2.110 -          | NONE => (name, ty_args))
   2.111 -        |> (fn (name, ty_args) => CombConst (name, ty, ty_args))
   2.112 -      | aux _ tm = tm
   2.113 -  in aux true end
   2.114 -
   2.115  fun impose_type_arg_policy type_sys =
   2.116    let
   2.117      fun aux (CombApp tmp) = CombApp (pairself aux tmp)
   2.118 @@ -657,20 +665,16 @@
   2.119  
   2.120  val add_fact_to_sym_table = fact_lift o formula_fold o add_combterm_to_sym_table
   2.121  
   2.122 -(* The "equal" entry is needed for helper facts if the problem otherwise does
   2.123 -   not involve equality (FIXME). The "$false" and $"true" entries are needed to
   2.124 -   ensure that no "hBOOL" is introduced for them. The "hBOOL" entry is needed to
   2.125 -   ensure that no "hAPP"s are introduced for passing arguments to it. *)
   2.126  val default_sym_table_entries =
   2.127    [("equal", {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
   2.128 -   (make_fixed_const boolify_base,
   2.129 +   (make_fixed_const predicator_base,
   2.130      {pred_sym = true, min_ary = 1, max_ary = 1, typ = NONE})] @
   2.131 -  (["$false", "$true"]
   2.132 +  ([tptp_false, tptp_true]
   2.133     |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, typ = NONE}))
   2.134  
   2.135  fun sym_table_for_facts explicit_apply facts =
   2.136 -  Symtab.empty |> fold (add_fact_to_sym_table explicit_apply) facts
   2.137 -               |> fold Symtab.default default_sym_table_entries
   2.138 +  Symtab.empty |> fold Symtab.default default_sym_table_entries
   2.139 +               |> fold (add_fact_to_sym_table explicit_apply) facts
   2.140  
   2.141  fun min_arity_of sym_tab s =
   2.142    case Symtab.lookup sym_tab s of
   2.143 @@ -679,7 +683,7 @@
   2.144      case strip_prefix_and_unascii const_prefix s of
   2.145        SOME s =>
   2.146        let val s = s |> unmangled_const_name |> invert_const in
   2.147 -        if s = boolify_base then 1
   2.148 +        if s = predicator_base then 1
   2.149          else if s = explicit_app_base then 2
   2.150          else if s = type_pred_base then 1
   2.151          else 0
   2.152 @@ -695,15 +699,15 @@
   2.153      SOME {pred_sym, min_ary, max_ary, ...} => pred_sym andalso min_ary = max_ary
   2.154    | NONE => false
   2.155  
   2.156 -val boolify_combconst =
   2.157 -  CombConst (`make_fixed_const boolify_base, @{typ "bool => bool"}, [])
   2.158 -fun boolify tm = CombApp (boolify_combconst, tm)
   2.159 +val predicator_combconst =
   2.160 +  CombConst (`make_fixed_const predicator_base, @{typ "bool => bool"}, [])
   2.161 +fun predicator tm = CombApp (predicator_combconst, tm)
   2.162  
   2.163 -fun introduce_boolifies_in_combterm sym_tab tm =
   2.164 +fun introduce_predicators_in_combterm sym_tab tm =
   2.165    case strip_combterm_comb tm of
   2.166      (CombConst ((s, _), _, _), _) =>
   2.167 -    if is_pred_sym sym_tab s then tm else boolify tm
   2.168 -  | _ => boolify tm
   2.169 +    if is_pred_sym sym_tab s then tm else predicator tm
   2.170 +  | _ => predicator tm
   2.171  
   2.172  fun list_app head args = fold (curry (CombApp o swap)) args head
   2.173  
   2.174 @@ -731,8 +735,7 @@
   2.175  
   2.176  fun firstorderize_combterm sym_tab =
   2.177    introduce_explicit_apps_in_combterm sym_tab
   2.178 -  #> introduce_boolifies_in_combterm sym_tab
   2.179 -  #> introduce_proxies
   2.180 +  #> introduce_predicators_in_combterm sym_tab
   2.181  val firstorderize_fact =
   2.182    update_combformula o formula_map o firstorderize_combterm
   2.183  
   2.184 @@ -770,7 +773,7 @@
   2.185        let val (arg_Ts, res_T) = strip_and_map_type ary mangled_type_name T in
   2.186          Decl (sym_decl_prefix ^ ascii_of s, (s, s'), arg_Ts,
   2.187                (* ### FIXME: put that in typed_const_tab *)
   2.188 -              if is_pred_sym sym_tab s then `I tff_bool_type else res_T)
   2.189 +              if is_pred_sym sym_tab s then `I tptp_tff_bool_type else res_T)
   2.190        end
   2.191      else
   2.192        let
   2.193 @@ -816,7 +819,7 @@
   2.194    fold (fold add_tff_types_in_problem_line o snd) problem []
   2.195  
   2.196  fun decl_line_for_tff_type (s, s') =
   2.197 -  Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tff_type_of_types)
   2.198 +  Decl (type_decl_prefix ^ ascii_of s, (s, s'), [], `I tptp_tff_type_of_types)
   2.199  
   2.200  val type_declsN = "Types"
   2.201  val sym_declsN = "Symbol types"
   2.202 @@ -832,8 +835,7 @@
   2.203      if heading = needle then j
   2.204      else offset_of_heading_in_problem needle problem (j + length lines)
   2.205  
   2.206 -fun prepare_atp_problem ctxt readable_names type_sys explicit_apply hyp_ts
   2.207 -                        concl_t facts =
   2.208 +fun prepare_atp_problem ctxt type_sys explicit_apply hyp_ts concl_t facts =
   2.209    let
   2.210      val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
   2.211        translate_formulas ctxt type_sys hyp_ts concl_t facts
   2.212 @@ -872,7 +874,7 @@
   2.213                    map decl_line_for_tff_type (tff_types_in_problem problem))
   2.214            else
   2.215              I)
   2.216 -    val (problem, pool) = problem |> nice_atp_problem readable_names
   2.217 +    val (problem, pool) = problem |> nice_atp_problem (!readable_names)
   2.218    in
   2.219      (problem,
   2.220       case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:24 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:24 2011 +0200
     3.3 @@ -382,7 +382,6 @@
     3.4        | [] =>
     3.5          if File.exists command then
     3.6            let
     3.7 -            val readable_names = debug andalso overlord
     3.8              (* If slicing is disabled, we expand the last slice to fill the
     3.9                 entire time available. *)
    3.10              val actual_slices = get_slices slicing (slices ())
    3.11 @@ -439,8 +438,8 @@
    3.12                      ()
    3.13                  val (atp_problem, pool, conjecture_offset, facts_offset,
    3.14                       fact_names) =
    3.15 -                  prepare_atp_problem ctxt readable_names type_sys
    3.16 -                                      explicit_apply hyp_ts concl_t facts
    3.17 +                  prepare_atp_problem ctxt type_sys explicit_apply hyp_ts
    3.18 +                                      concl_t facts
    3.19                  fun weights () = atp_problem_weights atp_problem
    3.20                  val core =
    3.21                    File.shell_path command ^ " " ^