src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42557 ae0deb39a254
parent 42556 f65e5f0341b8
child 42558 3d9930cb6770
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
     1.3 @@ -119,10 +119,8 @@
     1.4      | _ => Explicit_Type_Args
     1.5  
     1.6  fun num_atp_type_args thy type_sys s =
     1.7 -  if type_arg_policy type_sys s = Explicit_Type_Args then
     1.8 -    if s = type_pred_base then 1 else num_type_args thy s
     1.9 -  else
    1.10 -    0
    1.11 +  if type_arg_policy type_sys s = Explicit_Type_Args then num_type_args thy s
    1.12 +  else 0
    1.13  
    1.14  fun atp_type_literals_for_types type_sys kind Ts =
    1.15    if type_sys = No_Types then
    1.16 @@ -664,10 +662,13 @@
    1.17    formula_fold (consider_combterm_for_repair true) combformula
    1.18  
    1.19  (* The "equal" entry is needed for helper facts if the problem otherwise does
    1.20 -   not involve equality. The "hBOOL" entry is needed to ensure that no "hAPP"s
    1.21 -   are introduced for passing arguments to it. *)
    1.22 -val default_entries =
    1.23 +   not involve equality. The "$false" and $"true" entries are needed to ensure
    1.24 +   that no "hBOOL" is introduced for them. The "hBOOL" entry is needed to ensure
    1.25 +   that no "hAPP"s are introduced for passing arguments to it. *)
    1.26 +val default_sym_table_entries =
    1.27    [("equal", {pred_sym = true, min_arity = 2, max_arity = 2}),
    1.28 +   ("$false", {pred_sym = true, min_arity = 0, max_arity = 0}),
    1.29 +   ("$true", {pred_sym = true, min_arity = 0, max_arity = 0}),
    1.30     (make_fixed_const boolify_base,
    1.31      {pred_sym = true, min_arity = 1, max_arity = 1})]
    1.32  
    1.33 @@ -675,25 +676,23 @@
    1.34    if explicit_apply then
    1.35      NONE
    1.36    else
    1.37 -    SOME (Symtab.empty |> fold Symtab.default default_entries
    1.38 +    SOME (Symtab.empty |> fold Symtab.default default_sym_table_entries
    1.39                         |> fold consider_fact_for_repair facts)
    1.40  
    1.41 -fun min_arity_of _ _ (SOME sym_tab) s =
    1.42 +fun min_arity_of (SOME sym_tab) s =
    1.43      (case Symtab.lookup sym_tab s of
    1.44         SOME ({min_arity, ...} : repair_info) => min_arity
    1.45       | NONE => 0)
    1.46 -  | min_arity_of thy type_sys NONE s =
    1.47 -    if s = "equal" orelse s = type_tag_name orelse
    1.48 -       String.isPrefix type_const_prefix s orelse
    1.49 -       String.isPrefix class_prefix s then
    1.50 -      16383 (* large number *)
    1.51 +  | min_arity_of NONE s =
    1.52 +    if s = "equal" then
    1.53 +      2
    1.54      else case strip_prefix_and_unascii const_prefix s of
    1.55        SOME s =>
    1.56        let val s = s |> unmangled_const |> fst |> invert_const in
    1.57          if s = boolify_base then 1
    1.58          else if s = explicit_app_base then 2
    1.59          else if s = type_pred_base then 1
    1.60 -        else num_atp_type_args thy type_sys s
    1.61 +        else 0
    1.62        end
    1.63      | NONE => 0
    1.64  
    1.65 @@ -701,14 +700,15 @@
    1.66     literals, or if it appears with different arities (e.g., because of different
    1.67     type instantiations). If false, the constant always receives all of its
    1.68     arguments and is used as a predicate. *)
    1.69 -fun is_pred_sym NONE s =
    1.70 -    s = "equal" orelse s = "$false" orelse s = "$true" orelse
    1.71 -    String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s
    1.72 -  | is_pred_sym (SOME sym_tab) s =
    1.73 -    case Symtab.lookup sym_tab s of
    1.74 -      SOME {pred_sym, min_arity, max_arity} =>
    1.75 -      pred_sym andalso min_arity = max_arity
    1.76 -    | NONE => false
    1.77 +fun is_pred_sym (SOME sym_tab) s =
    1.78 +    (case Symtab.lookup sym_tab s of
    1.79 +       SOME {pred_sym, min_arity, max_arity} =>
    1.80 +       pred_sym andalso min_arity = max_arity
    1.81 +     | NONE => false)
    1.82 +  | is_pred_sym NONE s =
    1.83 +    (case AList.lookup (op =) default_sym_table_entries s of
    1.84 +       SOME {pred_sym, ...} => pred_sym
    1.85 +     | NONE => false)
    1.86  
    1.87  val boolify_combconst =
    1.88    CombConst (`make_fixed_const boolify_base,
    1.89 @@ -735,24 +735,24 @@
    1.90    in list_app explicit_app [head, arg] end
    1.91  fun list_explicit_app head args = fold explicit_app args head
    1.92  
    1.93 -fun repair_apps_in_combterm thy type_sys sym_tab =
    1.94 +fun repair_apps_in_combterm sym_tab =
    1.95    let
    1.96      fun aux tm =
    1.97        case strip_combterm_comb tm of
    1.98          (head as CombConst ((s, _), _, _), args) =>
    1.99          args |> map aux
   1.100 -             |> chop (min_arity_of thy type_sys sym_tab s)
   1.101 +             |> chop (min_arity_of sym_tab s)
   1.102               |>> list_app head
   1.103               |-> list_explicit_app
   1.104        | (head, args) => list_explicit_app head (map aux args)
   1.105    in aux end
   1.106  
   1.107 -fun repair_combterm thy type_sys sym_tab =
   1.108 +fun repair_combterm type_sys sym_tab =
   1.109    repair_pred_syms_in_combterm sym_tab
   1.110 -  #> repair_apps_in_combterm thy type_sys sym_tab
   1.111 +  #> repair_apps_in_combterm sym_tab
   1.112    #> repair_combterm_consts type_sys
   1.113 -val repair_combformula = formula_map ooo repair_combterm
   1.114 -val repair_fact = map_combformula ooo repair_combformula
   1.115 +val repair_combformula = formula_map oo repair_combterm
   1.116 +val repair_fact = map_combformula oo repair_combformula
   1.117  
   1.118  fun is_const_relevant type_sys sym_tab s =
   1.119    not (String.isPrefix bound_var_prefix s) andalso s <> "equal" andalso
   1.120 @@ -787,10 +787,7 @@
   1.121    | strip_and_map_combtyp _ _ _ = raise Fail "unexpected non-function"
   1.122  
   1.123  fun problem_line_for_typed_const ctxt type_sys sym_tab s j (s', ty_args, ty) =
   1.124 -  let
   1.125 -    val thy = Proof_Context.theory_of ctxt
   1.126 -    val arity = min_arity_of thy type_sys sym_tab s
   1.127 -  in
   1.128 +  let val arity = min_arity_of sym_tab s in
   1.129      if type_sys = Many_Typed then
   1.130        let
   1.131          val (arg_tys, res_ty) = strip_and_map_combtyp arity mangled_combtyp ty
   1.132 @@ -858,13 +855,11 @@
   1.133  fun prepare_atp_problem ctxt readable_names type_sys explicit_apply hyp_ts
   1.134                          concl_t facts =
   1.135    let
   1.136 -    val thy = Proof_Context.theory_of ctxt
   1.137      val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
   1.138        translate_formulas ctxt type_sys hyp_ts concl_t facts
   1.139      val sym_tab = sym_table_for_facts explicit_apply (conjs @ facts)
   1.140 -    val conjs = map (repair_fact thy type_sys sym_tab) conjs
   1.141 -    val facts = map (repair_fact thy type_sys sym_tab) facts
   1.142 -    val sym_tab = sym_table_for_facts explicit_apply (conjs @ facts)
   1.143 +    val conjs = map (repair_fact type_sys sym_tab) conjs
   1.144 +    val facts = map (repair_fact type_sys sym_tab) facts
   1.145      (* Reordering these might confuse the proof reconstruction code or the SPASS
   1.146         Flotter hack. *)
   1.147      val problem =
   1.148 @@ -881,7 +876,8 @@
   1.149        problem |> maps (map_filter (fn Formula (_, _, _, phi, _, _) => SOME phi
   1.150                                      | _ => NONE) o snd)
   1.151                |> get_helper_facts ctxt type_sys
   1.152 -              |>> map (repair_fact thy type_sys sym_tab)
   1.153 +              |>> map (repair_fact type_sys sym_tab)
   1.154 +    val sym_tab = sym_table_for_facts explicit_apply (conjs @ facts)
   1.155      val const_tab = const_table_for_facts type_sys sym_tab (conjs @ facts)
   1.156      val sym_decl_lines =
   1.157        Symtab.fold_rev (append o problem_lines_for_const ctxt type_sys sym_tab)