src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42520 d1f7c4a01dbe
parent 42449 494e4ac5b0f8
child 42521 02df3b78a438
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:05:09 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:23 2011 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4      Mangled |
     1.5      No_Types
     1.6  
     1.7 -  val precise_overloaded_args : bool Unsynchronized.ref
     1.8 +  val risky_overloaded_args : bool Unsynchronized.ref
     1.9    val fact_prefix : string
    1.10    val conjecture_prefix : string
    1.11    val is_type_system_sound : type_system -> bool
    1.12 @@ -44,7 +44,7 @@
    1.13  
    1.14  (* FIXME: Remove references once appropriate defaults have been determined
    1.15     empirically. *)
    1.16 -val precise_overloaded_args = Unsynchronized.ref false
    1.17 +val risky_overloaded_args = Unsynchronized.ref false
    1.18  
    1.19  val fact_prefix = "fact_"
    1.20  val conjecture_prefix = "conj_"
    1.21 @@ -81,7 +81,7 @@
    1.22  fun is_overloaded thy s =
    1.23    not (s = @{const_name HOL.eq}) andalso
    1.24    not (s = @{const_name Metis.fequal}) andalso
    1.25 -  (not (!precise_overloaded_args) orelse s = @{const_name finite} orelse
    1.26 +  (not (!risky_overloaded_args) orelse s = @{const_name finite} orelse
    1.27     length (Defs.specifications_of (Theory.defs_of thy) s) > 1)
    1.28  
    1.29  fun needs_type_args thy type_sys s =
    1.30 @@ -551,7 +551,7 @@
    1.31  
    1.32  (** "hBOOL" and "hAPP" **)
    1.33  
    1.34 -type const_info = {min_arity: int, max_arity: int, sub_level: bool}
    1.35 +type sym_info = {min_arity: int, max_arity: int, fun_sym: bool}
    1.36  
    1.37  fun consider_term top_level (ATerm ((s, _), ts)) =
    1.38    (if is_atp_variable s then
    1.39 @@ -559,11 +559,11 @@
    1.40     else
    1.41       let val n = length ts in
    1.42         Symtab.map_default
    1.43 -           (s, {min_arity = n, max_arity = 0, sub_level = false})
    1.44 -           (fn {min_arity, max_arity, sub_level} =>
    1.45 +           (s, {min_arity = n, max_arity = 0, fun_sym = false})
    1.46 +           (fn {min_arity, max_arity, fun_sym} =>
    1.47                 {min_arity = Int.min (n, min_arity),
    1.48                  max_arity = Int.max (n, max_arity),
    1.49 -                sub_level = sub_level orelse not top_level})
    1.50 +                fun_sym = fun_sym orelse not top_level})
    1.51       end)
    1.52    #> fold (consider_term (top_level andalso s = type_tag_name)) ts
    1.53  fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
    1.54 @@ -574,9 +574,9 @@
    1.55  fun consider_problem problem = fold (fold consider_problem_line o snd) problem
    1.56  
    1.57  (* needed for helper facts if the problem otherwise does not involve equality *)
    1.58 -val equal_entry = ("equal", {min_arity = 2, max_arity = 2, sub_level = false})
    1.59 +val equal_entry = ("equal", {min_arity = 2, max_arity = 2, fun_sym = false})
    1.60  
    1.61 -fun const_table_for_problem explicit_apply problem =
    1.62 +fun sym_table_for_problem explicit_apply problem =
    1.63    if explicit_apply then
    1.64      NONE
    1.65    else
    1.66 @@ -592,9 +592,9 @@
    1.67         s' |> unmangled_const |> fst |> invert_const
    1.68            |> num_atp_type_args thy type_sys
    1.69       | NONE => 0)
    1.70 -  | min_arity_of _ _ (SOME the_const_tab) s =
    1.71 -    case Symtab.lookup the_const_tab s of
    1.72 -      SOME ({min_arity, ...} : const_info) => min_arity
    1.73 +  | min_arity_of _ _ (SOME sym_tab) s =
    1.74 +    case Symtab.lookup sym_tab s of
    1.75 +      SOME ({min_arity, ...} : sym_info) => min_arity
    1.76      | NONE => 0
    1.77  
    1.78  fun full_type_of (ATerm ((s, _), [ty, _])) =
    1.79 @@ -614,7 +614,7 @@
    1.80        end
    1.81      | NONE => list_hAPP_rev NONE t1 (t2 :: ts2)
    1.82  
    1.83 -fun repair_applications_in_term thy type_sys const_tab =
    1.84 +fun repair_applications_in_term thy type_sys sym_tab =
    1.85    let
    1.86      fun aux opt_ty (ATerm (name as (s, _), ts)) =
    1.87        if s = type_tag_name then
    1.88 @@ -624,7 +624,7 @@
    1.89        else
    1.90          let
    1.91            val ts = map (aux NONE) ts
    1.92 -          val (ts1, ts2) = chop (min_arity_of thy type_sys const_tab s) ts
    1.93 +          val (ts1, ts2) = chop (min_arity_of thy type_sys sym_tab s) ts
    1.94          in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
    1.95    in aux NONE end
    1.96  
    1.97 @@ -634,37 +634,37 @@
    1.98     literals, or if it appears with different arities (e.g., because of different
    1.99     type instantiations). If false, the constant always receives all of its
   1.100     arguments and is used as a predicate. *)
   1.101 -fun is_predicate NONE s =
   1.102 +fun is_pred_sym NONE s =
   1.103      s = "equal" orelse s = "$false" orelse s = "$true" orelse
   1.104      String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s
   1.105 -  | is_predicate (SOME the_const_tab) s =
   1.106 -    case Symtab.lookup the_const_tab s of
   1.107 -      SOME {min_arity, max_arity, sub_level} =>
   1.108 -      not sub_level andalso min_arity = max_arity
   1.109 +  | is_pred_sym (SOME sym_tab) s =
   1.110 +    case Symtab.lookup sym_tab s of
   1.111 +      SOME {min_arity, max_arity, fun_sym} =>
   1.112 +      not fun_sym andalso min_arity = max_arity
   1.113      | NONE => false
   1.114  
   1.115 -fun repair_predicates_in_term pred_const_tab (t as ATerm ((s, _), ts)) =
   1.116 +fun repair_predicates_in_term pred_sym_tab (t as ATerm ((s, _), ts)) =
   1.117    if s = type_tag_name then
   1.118      case ts of
   1.119        [_, t' as ATerm ((s', _), _)] =>
   1.120 -      if is_predicate pred_const_tab s' then t' else boolify t
   1.121 +      if is_pred_sym pred_sym_tab s' then t' else boolify t
   1.122      | _ => raise Fail "malformed type tag"
   1.123    else
   1.124 -    t |> not (is_predicate pred_const_tab s) ? boolify
   1.125 +    t |> not (is_pred_sym pred_sym_tab s) ? boolify
   1.126  
   1.127 -fun repair_formula thy explicit_forall type_sys const_tab =
   1.128 +fun repair_formula thy explicit_forall type_sys sym_tab =
   1.129    let
   1.130 -    val pred_const_tab = case type_sys of Tags _ => NONE | _ => const_tab
   1.131 +    val pred_sym_tab = case type_sys of Tags _ => NONE | _ => sym_tab
   1.132      fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   1.133        | aux (AConn (c, phis)) = AConn (c, map aux phis)
   1.134        | aux (AAtom tm) =
   1.135 -        AAtom (tm |> repair_applications_in_term thy type_sys const_tab
   1.136 -                  |> repair_predicates_in_term pred_const_tab)
   1.137 +        AAtom (tm |> repair_applications_in_term thy type_sys sym_tab
   1.138 +                  |> repair_predicates_in_term pred_sym_tab)
   1.139    in aux #> explicit_forall ? close_universally end
   1.140  
   1.141 -fun repair_problem_line thy explicit_forall type_sys const_tab
   1.142 +fun repair_problem_line thy explicit_forall type_sys sym_tab
   1.143                          (Fof (ident, kind, phi, source)) =
   1.144 -  Fof (ident, kind, repair_formula thy explicit_forall type_sys const_tab phi,
   1.145 +  Fof (ident, kind, repair_formula thy explicit_forall type_sys sym_tab phi,
   1.146         source)
   1.147  fun repair_problem thy = map o apsnd o map ooo repair_problem_line thy
   1.148  
   1.149 @@ -698,15 +698,14 @@
   1.150         (helpersN, []),
   1.151         (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs),
   1.152         (free_typesN, problem_lines_for_free_types type_sys (facts @ conjs))]
   1.153 -    val const_tab = const_table_for_problem explicit_apply problem
   1.154 -    val problem =
   1.155 -      problem |> repair_problem thy explicit_forall type_sys const_tab
   1.156 +    val sym_tab = sym_table_for_problem explicit_apply problem
   1.157 +    val problem = problem |> repair_problem thy explicit_forall type_sys sym_tab
   1.158      val helper_lines =
   1.159        get_helper_facts ctxt explicit_forall type_sys
   1.160                         (maps (map (#3 o dest_Fof) o snd) problem)
   1.161        |>> map (pair 0
   1.162                 #> problem_line_for_fact ctxt helper_prefix type_sys
   1.163 -               #> repair_problem_line thy explicit_forall type_sys const_tab)
   1.164 +               #> repair_problem_line thy explicit_forall type_sys sym_tab)
   1.165        |> op @
   1.166      val (problem, pool) =
   1.167        problem |> AList.update (op =) (helpersN, helper_lines)