--- a/src/HOL/Tools/ATP/atp_problem.ML Wed Sep 07 13:51:39 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Sep 07 14:58:40 2011 +0200
@@ -236,6 +236,12 @@
| string_for_kind Hypothesis = "hypothesis"
| string_for_kind Conjecture = "conjecture"
+fun string_for_app format func args =
+ if is_format_thf format then
+ "(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")"
+ else
+ func ^ "(" ^ commas args ^ ")"
+
fun flatten_type (ATyAbs (tys, ty)) = ATyAbs (tys, flatten_type ty)
| flatten_type (ty as AFun (ty1 as AType _, ty2)) =
(case flatten_type ty2 of
@@ -247,16 +253,17 @@
| flatten_type _ =
raise Fail "unexpected higher-order type in first-order format"
-fun str_for_type ty =
+fun str_for_type format ty =
let
fun str _ (AType (s, [])) = s
| str _ (AType (s, tys)) =
- tys |> map (str false)
- |> (if s = tptp_product_type then
- space_implode (" " ^ tptp_product_type ^ " ")
- #> length tys > 1 ? enclose "(" ")"
- else
- commas #> enclose "(" ")" #> prefix s)
+ let val ss = tys |> map (str false) in
+ if s = tptp_product_type then
+ ss |> space_implode (" " ^ tptp_product_type ^ " ")
+ |> length ss > 1 ? enclose "(" ")"
+ else
+ string_for_app format s ss
+ end
| str rhs (AFun (ty1, ty2)) =
str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2
|> not rhs ? enclose "(" ")"
@@ -266,8 +273,8 @@
ss) ^ "]: " ^ str false ty
in str true ty end
-fun string_for_type (THF _) ty = str_for_type ty
- | string_for_type (TFF _) ty = str_for_type (flatten_type ty)
+fun string_for_type (format as THF _) ty = str_for_type format ty
+ | string_for_type (format as TFF _) ty = str_for_type format (flatten_type ty)
| string_for_type _ _ = raise Fail "unexpected type in untyped format"
fun string_for_quantifier AForall = tptp_forall
@@ -293,35 +300,27 @@
fun string_for_term _ (ATerm (s, [])) = s
| string_for_term format (ATerm (s, ts)) =
- if s = tptp_empty_list then
- (* used for lists in the optional "source" field of a derivation *)
- "[" ^ commas (map (string_for_term format) ts) ^ "]"
- else if is_tptp_equal s then
- space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
- |> is_format_thf format ? enclose "(" ")"
- else
- (case (s = tptp_ho_forall orelse s = tptp_ho_exists,
- s = tptp_choice andalso is_format_with_choice format, ts) of
- (true, _, [AAbs ((s', ty), tm)]) =>
- (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
- possible, to work around LEO-II 1.2.8 parser limitation. *)
- string_for_formula format
- (AQuant (if s = tptp_ho_forall then AForall else AExists,
- [(s', SOME ty)], AAtom tm))
- | (_, true, [AAbs ((s', ty), tm)]) =>
- (* There is code in "ATP_Translate" to ensure that "Eps" is always
- applied to an abstraction. *)
- tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
- string_for_term format tm ^ ""
- |> enclose "(" ")"
-
- | _ =>
- let val ss = map (string_for_term format) ts in
- if is_format_thf format then
- "(" ^ space_implode (" " ^ tptp_app ^ " ") (s :: ss) ^ ")"
- else
- s ^ "(" ^ commas ss ^ ")"
- end)
+ (if s = tptp_empty_list then
+ (* used for lists in the optional "source" field of a derivation *)
+ "[" ^ commas (map (string_for_term format) ts) ^ "]"
+ else if is_tptp_equal s then
+ space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts)
+ |> is_format_thf format ? enclose "(" ")"
+ else case (s = tptp_ho_forall orelse s = tptp_ho_exists,
+ s = tptp_choice andalso is_format_with_choice format, ts) of
+ (true, _, [AAbs ((s', ty), tm)]) =>
+ (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
+ possible, to work around LEO-II 1.2.8 parser limitation. *)
+ string_for_formula format
+ (AQuant (if s = tptp_ho_forall then AForall else AExists,
+ [(s', SOME ty)], AAtom tm))
+ | (_, true, [AAbs ((s', ty), tm)]) =>
+ (* There is code in "ATP_Translate" to ensure that "Eps" is always
+ applied to an abstraction. *)
+ tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^
+ string_for_term format tm ^ ""
+ |> enclose "(" ")"
+ | _ => string_for_app format s (map (string_for_term format) ts))
| string_for_term (format as THF _) (AAbs ((s, ty), tm)) =
"(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^
string_for_term format tm ^ ")"
--- a/src/HOL/Tools/ATP/atp_proof.ML Wed Sep 07 13:51:39 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Sep 07 14:58:40 2011 +0200
@@ -92,9 +92,6 @@
InternalError |
UnknownError of string
-fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
-val strip_spaces_except_between_ident_chars = strip_spaces true is_ident_char
-
fun elide_string threshold s =
if size s > threshold then
String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^
@@ -475,7 +472,7 @@
fun parse_line problem spass_names =
parse_tstp_line problem || parse_spass_line spass_names
fun parse_proof problem spass_names tstp =
- tstp |> strip_spaces_except_between_ident_chars
+ tstp |> strip_spaces_except_between_idents
|> raw_explode
|> Scan.finite Symbol.stopper
(Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Sep 07 13:51:39 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Sep 07 14:58:40 2011 +0200
@@ -152,7 +152,7 @@
union (op =) (resolve_fact facts_offset fact_names name)
| add_fact ctxt _ _ (Inference (_, _, deps)) =
if AList.defined (op =) deps leo2_ext then
- insert (op =) (ext_name ctxt, Extensionality)
+ insert (op =) (ext_name ctxt, General)
else
I
| add_fact _ _ _ _ = I
--- a/src/HOL/Tools/ATP/atp_systems.ML Wed Sep 07 13:51:39 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Sep 07 14:58:40 2011 +0200
@@ -403,11 +403,11 @@
prem_kind = Hypothesis,
best_slices = K [(1.0, (false, (200, format, type_enc, "")))]}
-val pff_format = TFF (TPTP_Polymorphic, TPTP_Implicit)
+val pff_format = TFF (TPTP_Polymorphic, TPTP_Explicit)
val pff_config = dummy_config pff_format "poly_simple"
val pff = (pffN, pff_config)
-val phf_format = THF (TPTP_Polymorphic, TPTP_Implicit, THF_With_Choice)
+val phf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice)
val phf_config = dummy_config phf_format "poly_simple_higher"
val phf = (phfN, phf_config)
--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Sep 07 13:51:39 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Sep 07 14:58:40 2011 +0200
@@ -16,24 +16,18 @@
type 'a problem = 'a ATP_Problem.problem
datatype locality =
- General | Helper | Induction | Extensionality | Intro | Elim | Simp |
- Local | Assum | Chained
+ General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
- datatype order = First_Order | Higher_Order
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
datatype soundness = Sound_Modulo_Infiniteness | Sound
- datatype uniformity = Uniform | Nonuniform
+ datatype heaviness = Heavy | Ann_Light | Arg_Light
datatype type_level =
All_Types |
- Noninf_Nonmono_Types of soundness * uniformity |
- Fin_Nonmono_Types of uniformity |
+ Noninf_Nonmono_Types of soundness * heaviness |
+ Fin_Nonmono_Types of heaviness |
Const_Arg_Types |
No_Types
-
- datatype type_enc =
- Simple_Types of order * polymorphism * type_level |
- Guards of polymorphism * type_level |
- Tags of polymorphism * type_level
+ type type_enc
val type_tag_idempotence : bool Config.T
val type_tag_arguments : bool Config.T
@@ -531,17 +525,16 @@
in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end
datatype locality =
- General | Helper | Induction | Extensionality | Intro | Elim | Simp |
- Local | Assum | Chained
+ General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
datatype order = First_Order | Higher_Order
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
datatype soundness = Sound_Modulo_Infiniteness | Sound
-datatype uniformity = Uniform | Nonuniform
+datatype heaviness = Heavy | Ann_Light | Arg_Light
datatype type_level =
All_Types |
- Noninf_Nonmono_Types of soundness * uniformity |
- Fin_Nonmono_Types of uniformity |
+ Noninf_Nonmono_Types of soundness * heaviness |
+ Fin_Nonmono_Types of heaviness |
Const_Arg_Types |
No_Types
@@ -561,9 +554,9 @@
| level_of_type_enc (Guards (_, level)) = level
| level_of_type_enc (Tags (_, level)) = level
-fun is_level_uniform (Noninf_Nonmono_Types (_, Nonuniform)) = false
- | is_level_uniform (Fin_Nonmono_Types Nonuniform) = false
- | is_level_uniform _ = true
+fun heaviness_of_level (Noninf_Nonmono_Types (_, heaviness)) = heaviness
+ | heaviness_of_level (Fin_Nonmono_Types heaviness) = heaviness
+ | heaviness_of_level _ = Heavy
fun is_type_level_quasi_sound All_Types = true
| is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
@@ -578,11 +571,25 @@
| is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true
| is_type_level_monotonicity_based _ = false
+(* "_query", "_bang", and "_at" are for the ASCII-challenged Metis and
+ Mirabelle. *)
+val queries = ["?", "_query"]
+val bangs = ["!", "_bang"]
+val ats = ["@", "_at"]
+
fun try_unsuffixes ss s =
fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
-val queries = ["?", "_query"]
-val bangs = ["!", "_bang"]
+fun try_nonmono constr suffixes fallback s =
+ case try_unsuffixes suffixes s of
+ SOME s =>
+ (case try_unsuffixes suffixes s of
+ SOME s => (constr Ann_Light, s)
+ | NONE =>
+ case try_unsuffixes ats s of
+ SOME s => (constr Arg_Light, s)
+ | NONE => (constr Heavy, s))
+ | NONE => fallback s
fun type_enc_from_string soundness s =
(case try (unprefix "poly_") s of
@@ -594,21 +601,9 @@
case try (unprefix "mono_") s of
SOME s => (SOME Mangled_Monomorphic, s)
| NONE => (NONE, s))
- ||> (fn s =>
- (* "_query" and "_bang" are for the ASCII-challenged Metis and
- Mirabelle. *)
- case try_unsuffixes queries s of
- SOME s =>
- (case try_unsuffixes queries s of
- SOME s => (Noninf_Nonmono_Types (soundness, Nonuniform), s)
- | NONE => (Noninf_Nonmono_Types (soundness, Uniform), s))
- | NONE =>
- case try_unsuffixes bangs s of
- SOME s =>
- (case try_unsuffixes bangs s of
- SOME s => (Fin_Nonmono_Types Nonuniform, s)
- | NONE => (Fin_Nonmono_Types Uniform, s))
- | NONE => (All_Types, s))
+ ||> (pair All_Types
+ |> try_nonmono Fin_Nonmono_Types bangs
+ |> try_nonmono (curry Noninf_Nonmono_Types soundness) queries)
|> (fn (poly, (level, core)) =>
case (core, (poly, level)) of
("simple", (SOME poly, _)) =>
@@ -616,7 +611,7 @@
(Polymorphic, All_Types) =>
Simple_Types (First_Order, Polymorphic, All_Types)
| (Mangled_Monomorphic, _) =>
- if is_level_uniform level then
+ if heaviness_of_level level = Heavy then
Simple_Types (First_Order, Mangled_Monomorphic, level)
else
raise Same.SAME
@@ -627,7 +622,7 @@
Simple_Types (Higher_Order, Polymorphic, All_Types)
| (_, Noninf_Nonmono_Types _) => raise Same.SAME
| (Mangled_Monomorphic, _) =>
- if is_level_uniform level then
+ if heaviness_of_level level = Heavy then
Simple_Types (Higher_Order, Mangled_Monomorphic, level)
else
raise Same.SAME
@@ -640,7 +635,7 @@
| ("erased", (NONE, All_Types (* naja *))) =>
Guards (Polymorphic, No_Types)
| _ => raise Same.SAME)
- handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
+ handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".")
fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
(Simple_Types (order, _, level)) =
@@ -1241,7 +1236,7 @@
| should_encode_type _ _ _ _ = false
fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
- (is_level_uniform level orelse should_guard_var ()) andalso
+ (heaviness_of_level level = Heavy orelse should_guard_var ()) andalso
should_encode_type ctxt mono level T
| should_guard_type _ _ _ _ _ = false
@@ -1258,7 +1253,7 @@
fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
| should_tag_with_type ctxt mono (Tags (_, level)) site u T =
- (if is_level_uniform level then
+ (if heaviness_of_level level = Heavy then
should_encode_type ctxt mono level T
else case (site, is_maybe_universal_var u) of
(Eq_Arg _, true) => should_encode_type ctxt mono level T
@@ -1366,21 +1361,21 @@
K (add_iterm_syms_to_table ctxt explicit_apply)
|> formula_fold NONE |> fact_lift
-val default_sym_tab_entries : (string * sym_info) list =
- (prefixed_predicator_name,
- {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
- (* FIXME: needed? *) ::
+fun default_sym_tab_entries type_enc =
(make_fixed_const NONE @{const_name undefined},
- {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
+ {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
([tptp_false, tptp_true]
|> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
([tptp_equal, tptp_old_equal]
|> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
+ |> not (is_type_enc_higher_order type_enc)
+ ? cons (prefixed_predicator_name,
+ {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
-fun sym_table_for_facts ctxt explicit_apply facts =
+fun sym_table_for_facts ctxt type_enc explicit_apply facts =
((false, []), Symtab.empty)
|> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
- |> fold Symtab.update default_sym_tab_entries
+ |> fold Symtab.update (default_sym_tab_entries type_enc)
fun min_ary_of sym_tab s =
case Symtab.lookup sym_tab s of
@@ -1657,7 +1652,8 @@
fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
| should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
- not (is_level_uniform level) andalso should_encode_type ctxt mono level T
+ heaviness_of_level level <> Heavy andalso
+ should_encode_type ctxt mono level T
| should_generate_tag_bound_decl _ _ _ _ _ = false
fun mk_aterm format type_enc name T_args args =
@@ -1877,8 +1873,8 @@
? (fold (add_fact_syms true) conjs
#> fold (add_fact_syms false) facts
#> (case type_enc of
- Simple_Types (_, poly, _) =>
- if poly = Polymorphic then add_TYPE_const () else I
+ Simple_Types (First_Order, Polymorphic, _) => add_TYPE_const ()
+ | Simple_Types _ => I
| _ => fold add_undefined_const (var_types ())))
end
@@ -2131,7 +2127,7 @@
type_enc n s)
end
| Tags (_, level) =>
- if is_level_uniform level then
+ if heaviness_of_level level = Heavy then
[]
else
let val n = length decls in
@@ -2209,11 +2205,13 @@
val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses) =
translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
hyp_ts concl_t facts
- val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
+ val sym_tab =
+ conjs @ facts |> sym_table_for_facts ctxt type_enc explicit_apply
val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
val firstorderize = firstorderize_fact thy format type_enc sym_tab
val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
- val sym_tab = conjs @ facts |> sym_table_for_facts ctxt (SOME false)
+ val sym_tab =
+ conjs @ facts |> sym_table_for_facts ctxt type_enc (SOME false)
val helpers =
sym_tab |> helper_facts_for_sym_table ctxt format type_enc
|> map firstorderize
--- a/src/HOL/Tools/ATP/atp_util.ML Wed Sep 07 13:51:39 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Wed Sep 07 14:58:40 2011 +0200
@@ -10,6 +10,7 @@
val hash_string : string -> int
val hash_term : term -> int
val strip_spaces : bool -> (char -> bool) -> string -> string
+ val strip_spaces_except_between_idents : string -> string
val nat_subscript : int -> string
val unyxml : string -> string
val maybe_quote : string -> string
@@ -88,6 +89,9 @@
fun strip_spaces skip_comments is_evil =
implode o strip_spaces_in_list skip_comments is_evil o String.explode
+fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
+val strip_spaces_except_between_idents = strip_spaces true is_ident_char
+
val subscript = implode o map (prefix "\<^isub>") o raw_explode (* FIXME Symbol.explode (?) *)
fun nat_subscript n =
n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
--- a/src/HOL/Tools/Metis/metis_translate.ML Wed Sep 07 13:51:39 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Sep 07 14:58:40 2011 +0200
@@ -59,8 +59,9 @@
((prefixed_predicator_name, 1), (K metis_predicator, false)),
((prefixed_app_op_name, 2), (K metis_app_op, false)),
((prefixed_type_tag_name, 2),
- (fn Tags (_, All_Types) => metis_systematic_type_tag
- | _ => metis_ad_hoc_type_tag, true))]
+ (fn type_enc =>
+ if level_of_type_enc type_enc = All_Types then metis_systematic_type_tag
+ else metis_ad_hoc_type_tag, true))]
fun old_skolem_const_name i j num_T_args =
old_skolem_const_prefix ^ Long_Name.separator ^
--- a/src/HOL/Tools/Nitpick/nitrox.ML Wed Sep 07 13:51:39 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitrox.ML Wed Sep 07 14:58:40 2011 +0200
@@ -21,8 +21,7 @@
exception SYNTAX of string
-fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
-val tptp_explode = raw_explode o strip_spaces true is_ident_char
+val tptp_explode = raw_explode o strip_spaces_except_between_idents
fun parse_file_path (c :: ss) =
if c = "'" orelse c = "\"" then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Sep 07 13:51:39 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Sep 07 14:58:40 2011 +0200
@@ -144,7 +144,6 @@
(j + 1,
((nth_name j,
if member Thm.eq_thm_prop chained_ths th then Chained
- else if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
else General), th) :: rest))
|> snd
end
@@ -576,7 +575,7 @@
| _ => SOME tab
in aux (prop_of th) [] end
-(* FIXME: This is currently only useful for polymorphic type systems. *)
+(* FIXME: This is currently only useful for polymorphic type encodings. *)
fun could_benefit_from_ext is_built_in_const facts =
fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty)
|> is_none
@@ -845,8 +844,7 @@
else if global then
case Termtab.lookup clasimpset_table (prop_of th) of
SOME loc => loc
- | NONE => if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality
- else General
+ | NONE => General
else if is_assum th then Assum else Local
fun is_good_unnamed_local th =
not (Thm.has_name_hint th) andalso
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Sep 07 13:51:39 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Sep 07 14:58:40 2011 +0200
@@ -19,6 +19,7 @@
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
struct
+open ATP_Util
open ATP_Systems
open ATP_Translate
open Sledgehammer_Util
@@ -151,13 +152,9 @@
error ("Unknown parameter: " ^ quote name ^ "."))
-(* Ensure that type systems such as "mono_simple?" and "mono_guards!!" are
- handled correctly. *)
-fun implode_param [s, "?"] = s ^ "?"
- | implode_param [s, "??"] = s ^ "??"
- | implode_param [s, "!"] = s ^ "!"
- | implode_param [s, "!!"] = s ^ "!!"
- | implode_param ss = space_implode " " ss
+(* Ensures that type encodings such as "mono_simple?" and "poly_guards!!" are
+ read correctly. *)
+val implode_param = strip_spaces_except_between_idents o space_implode " "
structure Data = Theory_Data
(