# HG changeset patch # User blanchet # Date 1304267843 -7200 # Node ID d1f7c4a01dbe33f99235a61c5311e931ba7d25de # Parent 8ac7e96f913b33dcc27e092e8a2c8a032e52abfd renamings diff -r 8ac7e96f913b -r d1f7c4a01dbe src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:05:09 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sun May 01 18:37:23 2011 +0200 @@ -18,7 +18,7 @@ Mangled | No_Types - val precise_overloaded_args : bool Unsynchronized.ref + val risky_overloaded_args : bool Unsynchronized.ref val fact_prefix : string val conjecture_prefix : string val is_type_system_sound : type_system -> bool @@ -44,7 +44,7 @@ (* FIXME: Remove references once appropriate defaults have been determined empirically. *) -val precise_overloaded_args = Unsynchronized.ref false +val risky_overloaded_args = Unsynchronized.ref false val fact_prefix = "fact_" val conjecture_prefix = "conj_" @@ -81,7 +81,7 @@ fun is_overloaded thy s = not (s = @{const_name HOL.eq}) andalso not (s = @{const_name Metis.fequal}) andalso - (not (!precise_overloaded_args) orelse s = @{const_name finite} orelse + (not (!risky_overloaded_args) orelse s = @{const_name finite} orelse length (Defs.specifications_of (Theory.defs_of thy) s) > 1) fun needs_type_args thy type_sys s = @@ -551,7 +551,7 @@ (** "hBOOL" and "hAPP" **) -type const_info = {min_arity: int, max_arity: int, sub_level: bool} +type sym_info = {min_arity: int, max_arity: int, fun_sym: bool} fun consider_term top_level (ATerm ((s, _), ts)) = (if is_atp_variable s then @@ -559,11 +559,11 @@ else let val n = length ts in Symtab.map_default - (s, {min_arity = n, max_arity = 0, sub_level = false}) - (fn {min_arity, max_arity, sub_level} => + (s, {min_arity = n, max_arity = 0, fun_sym = false}) + (fn {min_arity, max_arity, fun_sym} => {min_arity = Int.min (n, min_arity), max_arity = Int.max (n, max_arity), - sub_level = sub_level orelse not top_level}) + fun_sym = fun_sym orelse not top_level}) end) #> fold (consider_term (top_level andalso s = type_tag_name)) ts fun consider_formula (AQuant (_, _, phi)) = consider_formula phi @@ -574,9 +574,9 @@ fun consider_problem problem = fold (fold consider_problem_line o snd) problem (* needed for helper facts if the problem otherwise does not involve equality *) -val equal_entry = ("equal", {min_arity = 2, max_arity = 2, sub_level = false}) +val equal_entry = ("equal", {min_arity = 2, max_arity = 2, fun_sym = false}) -fun const_table_for_problem explicit_apply problem = +fun sym_table_for_problem explicit_apply problem = if explicit_apply then NONE else @@ -592,9 +592,9 @@ s' |> unmangled_const |> fst |> invert_const |> num_atp_type_args thy type_sys | NONE => 0) - | min_arity_of _ _ (SOME the_const_tab) s = - case Symtab.lookup the_const_tab s of - SOME ({min_arity, ...} : const_info) => min_arity + | min_arity_of _ _ (SOME sym_tab) s = + case Symtab.lookup sym_tab s of + SOME ({min_arity, ...} : sym_info) => min_arity | NONE => 0 fun full_type_of (ATerm ((s, _), [ty, _])) = @@ -614,7 +614,7 @@ end | NONE => list_hAPP_rev NONE t1 (t2 :: ts2) -fun repair_applications_in_term thy type_sys const_tab = +fun repair_applications_in_term thy type_sys sym_tab = let fun aux opt_ty (ATerm (name as (s, _), ts)) = if s = type_tag_name then @@ -624,7 +624,7 @@ else let val ts = map (aux NONE) ts - val (ts1, ts2) = chop (min_arity_of thy type_sys const_tab s) ts + val (ts1, ts2) = chop (min_arity_of thy type_sys sym_tab s) ts in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end in aux NONE end @@ -634,37 +634,37 @@ literals, or if it appears with different arities (e.g., because of different type instantiations). If false, the constant always receives all of its arguments and is used as a predicate. *) -fun is_predicate NONE s = +fun is_pred_sym NONE s = s = "equal" orelse s = "$false" orelse s = "$true" orelse String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s - | is_predicate (SOME the_const_tab) s = - case Symtab.lookup the_const_tab s of - SOME {min_arity, max_arity, sub_level} => - not sub_level andalso min_arity = max_arity + | is_pred_sym (SOME sym_tab) s = + case Symtab.lookup sym_tab s of + SOME {min_arity, max_arity, fun_sym} => + not fun_sym andalso min_arity = max_arity | NONE => false -fun repair_predicates_in_term pred_const_tab (t as ATerm ((s, _), ts)) = +fun repair_predicates_in_term pred_sym_tab (t as ATerm ((s, _), ts)) = if s = type_tag_name then case ts of [_, t' as ATerm ((s', _), _)] => - if is_predicate pred_const_tab s' then t' else boolify t + if is_pred_sym pred_sym_tab s' then t' else boolify t | _ => raise Fail "malformed type tag" else - t |> not (is_predicate pred_const_tab s) ? boolify + t |> not (is_pred_sym pred_sym_tab s) ? boolify -fun repair_formula thy explicit_forall type_sys const_tab = +fun repair_formula thy explicit_forall type_sys sym_tab = let - val pred_const_tab = case type_sys of Tags _ => NONE | _ => const_tab + val pred_sym_tab = case type_sys of Tags _ => NONE | _ => sym_tab fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) | aux (AConn (c, phis)) = AConn (c, map aux phis) | aux (AAtom tm) = - AAtom (tm |> repair_applications_in_term thy type_sys const_tab - |> repair_predicates_in_term pred_const_tab) + AAtom (tm |> repair_applications_in_term thy type_sys sym_tab + |> repair_predicates_in_term pred_sym_tab) in aux #> explicit_forall ? close_universally end -fun repair_problem_line thy explicit_forall type_sys const_tab +fun repair_problem_line thy explicit_forall type_sys sym_tab (Fof (ident, kind, phi, source)) = - Fof (ident, kind, repair_formula thy explicit_forall type_sys const_tab phi, + Fof (ident, kind, repair_formula thy explicit_forall type_sys sym_tab phi, source) fun repair_problem thy = map o apsnd o map ooo repair_problem_line thy @@ -698,15 +698,14 @@ (helpersN, []), (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs), (free_typesN, problem_lines_for_free_types type_sys (facts @ conjs))] - val const_tab = const_table_for_problem explicit_apply problem - val problem = - problem |> repair_problem thy explicit_forall type_sys const_tab + val sym_tab = sym_table_for_problem explicit_apply problem + val problem = problem |> repair_problem thy explicit_forall type_sys sym_tab val helper_lines = get_helper_facts ctxt explicit_forall type_sys (maps (map (#3 o dest_Fof) o snd) problem) |>> map (pair 0 #> problem_line_for_fact ctxt helper_prefix type_sys - #> repair_problem_line thy explicit_forall type_sys const_tab) + #> repair_problem_line thy explicit_forall type_sys sym_tab) |> op @ val (problem, pool) = problem |> AList.update (op =) (helpersN, helper_lines)