--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Sep 07 17:03:34 2011 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Wed Sep 07 17:42:57 2011 +0200
@@ -628,7 +628,9 @@
val dummy_case_term = IVar NONE;
(*assumption: dummy values are not relevant for serialization*)
val (unitt, unitT) = case lookup_const naming @{const_name Unity}
- of SOME unit' => (IConst (unit', (([], []), [])), the (lookup_tyco naming @{type_name unit}) `%% [])
+ of SOME unit' =>
+ let val unitT = the (lookup_tyco naming @{type_name unit}) `%% []
+ in (IConst (unit', ((([], []), ([], unitT)), false)), unitT) end
| NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
| dest_abs (t, ty) =
@@ -645,13 +647,13 @@
val ((v, ty), t) = dest_abs (t2, ty2);
in ICase (((force t1, ty), [(IVar v, tr_bind' t)]), dummy_case_term) end
and tr_bind' t = case unfold_app t
- of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bind c
+ of (IConst (c, ((_, (ty1 :: ty2 :: _, _)), _)), [x1, x2]) => if is_bind c
then tr_bind'' [(x1, ty1), (x2, ty2)]
else force t
| _ => force t;
fun imp_monad_bind'' ts = (SOME dummy_name, unitT) `|=> ICase (((IVar (SOME dummy_name), unitT),
[(unitt, tr_bind'' ts)]), dummy_case_term)
- fun imp_monad_bind' (const as (c, (_, tys))) ts = if is_bind c then case (ts, tys)
+ fun imp_monad_bind' (const as (c, ((_, (tys, _)), _))) ts = if is_bind c then case (ts, tys)
of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
| ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
| (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
--- a/src/HOL/Tools/ATP/atp_problem.ML Wed Sep 07 17:03:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Sep 07 17:42:57 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 17:03:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Sep 07 17:42:57 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 17:03:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Sep 07 17:42:57 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 17:03:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Sep 07 17:42:57 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 17:03:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Sep 07 17:42:57 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 17:03:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Wed Sep 07 17:42:57 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 17:03:34 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Sep 07 17:42:57 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 17:03:34 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitrox.ML Wed Sep 07 17:42:57 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 17:03:34 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Sep 07 17:42:57 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 17:03:34 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Sep 07 17:42:57 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
(
--- a/src/Tools/Code/code_haskell.ML Wed Sep 07 17:03:34 2011 +0200
+++ b/src/Tools/Code/code_haskell.ML Wed Sep 07 17:42:57 2011 +0200
@@ -25,7 +25,7 @@
(** Haskell serializer **)
fun print_haskell_stmt labelled_name class_syntax tyco_syntax const_syntax
- reserved deresolve contr_classparam_typs deriving_show =
+ reserved deresolve deriving_show =
let
fun class_name class = case class_syntax class
of NONE => deresolve class
@@ -75,20 +75,14 @@
then print_case tyvars some_thm vars fxy cases
else print_app tyvars some_thm vars fxy c_ts
| NONE => print_case tyvars some_thm vars fxy cases)
- and print_app_expr tyvars some_thm vars ((c, (_, function_typs)), ts) = case contr_classparam_typs c
- of [] => (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
- | fingerprint => let
- val ts_fingerprint = ts ~~ take (length ts) fingerprint;
- val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
- (not o Code_Thingol.locally_monomorphic) t) ts_fingerprint;
- fun print_term_anno (t, NONE) _ = print_term tyvars some_thm vars BR t
- | print_term_anno (t, SOME _) ty =
- brackets [print_term tyvars some_thm vars NOBR t, str "::", print_typ tyvars NOBR ty];
- in
- if needs_annotation then
- (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) function_typs)
- else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
- end
+ and print_app_expr tyvars some_thm vars ((c, ((_, (function_typs, body_typ)), annotate)), ts) =
+ let
+ val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (function_typs, body_typ)
+ fun put_annotation c = brackets [c, str "::", print_typ tyvars NOBR ty]
+ in
+ ((if annotate then put_annotation else I)
+ ((str o deresolve) c)) :: map (print_term tyvars some_thm vars BR) ts
+ end
and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
@@ -230,14 +224,14 @@
]
| SOME k =>
let
- val (c, (_, tys)) = const;
+ val (c, ((_, tys), _)) = const; (* FIXME: pass around the need annotation flag here? *)
val (vs, rhs) = (apfst o map) fst
(Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
val s = if (is_some o const_syntax) c
then NONE else (SOME o Long_Name.base_name o deresolve) c;
val vars = reserved
|> intro_vars (map_filter I (s :: vs));
- val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
+ val lhs = IConst (classparam, ((([], []), tys), false (* FIXME *))) `$$ map IVar vs;
(*dictionaries are not relevant at this late stage*)
in
semicolon [
@@ -304,7 +298,6 @@
labelled_name module_alias module_prefix (Name.make_context reserved) program;
(* print statements *)
- val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
fun deriving_show tyco =
let
fun deriv _ "fun" = false
@@ -320,7 +313,7 @@
in deriv [] tyco end;
fun print_stmt deresolve = print_haskell_stmt labelled_name
class_syntax tyco_syntax const_syntax (make_vars reserved)
- deresolve contr_classparam_typs
+ deresolve
(if string_classes then deriving_show else K false);
(* print modules *)
--- a/src/Tools/Code/code_ml.ML Wed Sep 07 17:03:34 2011 +0200
+++ b/src/Tools/Code/code_ml.ML Wed Sep 07 17:42:57 2011 +0200
@@ -117,7 +117,7 @@
then print_case is_pseudo_fun some_thm vars fxy cases
else print_app is_pseudo_fun some_thm vars fxy c_ts
| NONE => print_case is_pseudo_fun some_thm vars fxy cases)
- and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), function_typs)), ts)) =
+ and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (function_typs, _)), _)), ts)) =
if is_cons c then
let val k = length function_typs in
if k < 2 orelse length ts = k
@@ -417,7 +417,7 @@
then print_case is_pseudo_fun some_thm vars fxy cases
else print_app is_pseudo_fun some_thm vars fxy c_ts
| NONE => print_case is_pseudo_fun some_thm vars fxy cases)
- and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
+ and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (tys, _)), _)), ts)) =
if is_cons c then
let val k = length tys in
if length ts = k
--- a/src/Tools/Code/code_printer.ML Wed Sep 07 17:03:34 2011 +0200
+++ b/src/Tools/Code/code_printer.ML Wed Sep 07 17:42:57 2011 +0200
@@ -315,7 +315,7 @@
|-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
- (app as ((c, (_, function_typs)), ts)) =
+ (app as ((c, ((_, (function_typs, _)), _)), ts)) =
case const_syntax c of
NONE => brackify fxy (print_app_expr some_thm vars app)
| SOME (Plain_const_syntax (_, s)) =>
--- a/src/Tools/Code/code_scala.ML Wed Sep 07 17:03:34 2011 +0200
+++ b/src/Tools/Code/code_scala.ML Wed Sep 07 17:42:57 2011 +0200
@@ -72,7 +72,7 @@
else print_app tyvars is_pat some_thm vars fxy c_ts
| NONE => print_case tyvars some_thm vars fxy cases)
and print_app tyvars is_pat some_thm vars fxy
- (app as ((c, ((arg_typs, _), function_typs)), ts)) =
+ (app as ((c, (((arg_typs, _), (function_typs, _)), _)), ts)) =
let
val k = length ts;
val arg_typs' = if is_pat orelse
@@ -265,7 +265,7 @@
let
val tyvars = intro_tyvars vs reserved;
val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
- fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
+ fun print_classparam_instance ((classparam, const as (_, ((_, (tys, _)), _))), (thm, _)) =
let
val aux_tys = Name.invent_names (snd reserved) "a" tys;
val auxs = map fst aux_tys;
--- a/src/Tools/Code/code_thingol.ML Wed Sep 07 17:03:34 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML Wed Sep 07 17:42:57 2011 +0200
@@ -22,7 +22,7 @@
datatype itype =
`%% of string * itype list
| ITyVar of vname;
- type const = string * ((itype list * dict list list) * itype list)
+ type const = string * (((itype list * dict list list) * (itype list * itype)) * bool)
(* f [T1..Tn] {dicts} (_::S1) .. (_..Sm) =^= (f, (([T1..Tn], dicts), [S1..Sm]) *)
datatype iterm =
IConst of const
@@ -55,7 +55,6 @@
val is_IAbs: iterm -> bool
val eta_expand: int -> const * iterm list -> iterm
val contains_dict_var: iterm -> bool
- val locally_monomorphic: iterm -> bool
val add_constnames: iterm -> string list -> string list
val add_tyconames: iterm -> string list -> string list
val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
@@ -88,7 +87,6 @@
val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
val is_cons: program -> string -> bool
val is_case: stmt -> bool
- val contr_classparam_typs: program -> string -> itype option list
val labelled_name: theory -> program -> string -> string
val group_stmts: theory -> program
-> ((string * stmt) list * (string * stmt) list
@@ -145,7 +143,8 @@
`%% of string * itype list
| ITyVar of vname;
-type const = string * ((itype list * dict list list) * itype list (*types of arguments*))
+type const = string * (((itype list * dict list list) *
+ (itype list (*types of arguments*) * itype (*body type*))) * bool (*requires type annotation*))
datatype iterm =
IConst of const
@@ -198,7 +197,7 @@
fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys
| add_tycos (ITyVar _) = I;
-val add_tyconames = fold_constexprs (fn (_, ((tys, _), _)) => fold add_tycos tys);
+val add_tyconames = fold_constexprs (fn (_, (((tys, _), _), _)) => fold add_tycos tys);
fun fold_varnames f =
let
@@ -240,7 +239,7 @@
val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
-fun eta_expand k (c as (name, (_, tys)), ts) =
+fun eta_expand k (c as (name, ((_, (tys, _)), _)), ts) =
let
val j = length ts;
val l = k - j;
@@ -256,18 +255,12 @@
fun cont_dict (Dict (_, d)) = cont_plain_dict d
and cont_plain_dict (Dict_Const (_, dss)) = (exists o exists) cont_dict dss
| cont_plain_dict (Dict_Var _) = true;
- fun cont_term (IConst (_, ((_, dss), _))) = (exists o exists) cont_dict dss
+ fun cont_term (IConst (_, (((_, dss), _), _))) = (exists o exists) cont_dict dss
| cont_term (IVar _) = false
| cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
| cont_term (_ `|=> t) = cont_term t
| cont_term (ICase (_, t)) = cont_term t;
in cont_term t end;
-
-fun locally_monomorphic (IConst _) = false
- | locally_monomorphic (IVar _) = true
- | locally_monomorphic (t `$ _) = locally_monomorphic t
- | locally_monomorphic (_ `|=> t) = locally_monomorphic t
- | locally_monomorphic (ICase ((_, ds), _)) = exists (locally_monomorphic o snd) ds;
(** namings **)
@@ -480,28 +473,6 @@
(fn (_, (Classinst ((class, _), (_, (param_insts, _))), _)) =>
Option.map (fn ((const, _), _) => (class, const))
(find_first (fn ((_, (inst_const, _)), _) => inst_const = name) param_insts) | _ => NONE)
-
-fun contr_classparam_typs program name =
- let
- fun contr_classparam_typs' (class, name) =
- let
- val Class (_, (_, (_, params))) = Graph.get_node program class;
- val SOME ty = AList.lookup (op =) params name;
- val (tys, res_ty) = unfold_fun ty;
- fun no_tyvar (_ `%% tys) = forall no_tyvar tys
- | no_tyvar (ITyVar _) = false;
- in if no_tyvar res_ty
- then map (fn ty => if no_tyvar ty then NONE else SOME ty) tys
- else []
- end
- in
- case Graph.get_node program name
- of Classparam (_, class) => contr_classparam_typs' (class, name)
- | Fun (c, _) => (case lookup_classparam_instance program name
- of NONE => []
- | SOME (class, name) => the_default [] (try contr_classparam_typs' (class, name)))
- | _ => []
- end;
fun labelled_name thy program name =
let val ctxt = Proof_Context.init_global thy in
@@ -608,6 +579,42 @@
(err_typ ^ "\n" ^ err_class)
end;
+(* inference of type annotations for disambiguation with type classes *)
+
+fun annotate_term (Const (c', T'), Const (c, T)) tvar_names =
+ let
+ val tvar_names' = Term.add_tvar_namesT T' tvar_names
+ in
+ (Const (c, if eq_set (op =) (tvar_names, tvar_names') then T else Type("", [T])), tvar_names')
+ end
+ | annotate_term (t1 $ u1, t $ u) tvar_names =
+ let
+ val (u', tvar_names') = annotate_term (u1, u) tvar_names
+ val (t', tvar_names'') = annotate_term (t1, t) tvar_names'
+ in
+ (t' $ u', tvar_names'')
+ end
+ | annotate_term (Abs (_, _, t1) , Abs (x, T, t)) tvar_names =
+ apfst (fn t => Abs (x, T, t)) (annotate_term (t1, t) tvar_names)
+ | annotate_term (_, t) tvar_names = (t, tvar_names)
+
+fun annotate_eqns thy eqns =
+ let
+ val ctxt = ProofContext.init_global thy |> Config.put Type_Infer_Context.const_sorts false
+ val erase = map_types (fn _ => Type_Infer.anyT [])
+ val reinfer = singleton (Type_Infer_Context.infer_types ctxt)
+ fun add_annotations ((args, (rhs, some_abs)), (SOME th, proper)) =
+ let
+ val (lhs, drhs) = Logic.dest_equals (prop_of (Thm.unvarify_global th))
+ val drhs' = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase drhs))))
+ val (rhs', _) = annotate_term (drhs', rhs) []
+ in
+ ((args, (rhs', some_abs)), (SOME th, proper))
+ end
+ | add_annotations eqn = eqn
+ in
+ map add_annotations eqns
+ end;
(* translation *)
@@ -633,11 +640,12 @@
fun stmt_fun cert =
let
val ((vs, ty), eqns) = Code.equations_of_cert thy cert;
+ val eqns' = annotate_eqns thy eqns
val some_case_cong = Code.get_case_cong thy c;
in
fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
##>> translate_typ thy algbr eqngr permissive ty
- ##>> translate_eqns thy algbr eqngr permissive eqns
+ ##>> translate_eqns thy algbr eqngr permissive eqns'
#>> (fn info => Fun (c, (info, some_case_cong)))
end;
val stmt_const = case Code.get_type_of_constr_or_abstr thy c
@@ -748,15 +756,17 @@
then translation_error thy permissive some_thm
"Abstraction violation" ("constant " ^ Code.string_of_const thy c)
else ()
- val arg_typs = Sign.const_typargs thy (c, ty);
+ val (annotate, ty') = (case ty of Type("", [ty']) => (true, ty') | ty' => (false, ty'))
+ val arg_typs = Sign.const_typargs thy (c, ty');
val sorts = Code_Preproc.sortargs eqngr c;
- val function_typs = Term.binder_types ty;
+ val (function_typs, body_typ) = Term.strip_type ty';
in
ensure_const thy algbr eqngr permissive c
##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
- ##>> fold_map (translate_typ thy algbr eqngr permissive) function_typs
- #>> (fn (((c, arg_typs), dss), function_typs) => IConst (c, ((arg_typs, dss), function_typs)))
+ ##>> fold_map (translate_typ thy algbr eqngr permissive) (body_typ :: function_typs)
+ #>> (fn (((c, arg_typs), dss), body_typ :: function_typs) =>
+ IConst (c, (((arg_typs, dss), (function_typs, body_typ)), annotate)))
end
and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)
@@ -801,7 +811,7 @@
val ts_clause = nth_drop t_pos ts;
val clauses = if null case_pats
then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
- else maps (fn ((constr as IConst (_, (_, tys)), n), t) =>
+ else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) =>
mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
(constrs ~~ ts_clause);
in ((t, ty), clauses) end;
--- a/src/Tools/nbe.ML Wed Sep 07 17:03:34 2011 +0200
+++ b/src/Tools/nbe.ML Wed Sep 07 17:42:57 2011 +0200
@@ -315,7 +315,7 @@
let
val (t', ts) = Code_Thingol.unfold_app t
in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
- and of_iapp match_cont (IConst (c, ((_, dss), _))) ts = constapp c dss ts
+ and of_iapp match_cont (IConst (c, (((_, dss), _), _))) ts = constapp c dss ts
| of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
| of_iapp match_cont ((v, _) `|=> t) ts =
nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
@@ -425,7 +425,7 @@
val params = Name.invent Name.context "d" (length names);
fun mk (k, name) =
(name, ([(v, [])],
- [([IConst (class, (([], []), [])) `$$ map (IVar o SOME) params],
+ [([IConst (class, ((([], []), ([], ITyVar "")), false)) `$$ map (IVar o SOME) params],
IVar (SOME (nth params k)))]));
in map_index mk names end
| eqns_of_stmt (_, Code_Thingol.Classrel _) =
@@ -433,8 +433,8 @@
| eqns_of_stmt (_, Code_Thingol.Classparam _) =
[]
| eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) =
- [(inst, (arity_args, [([], IConst (class, (([], []), [])) `$$
- map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances
+ [(inst, (arity_args, [([], IConst (class, ((([], []), ([], ITyVar "")), false)) `$$
+ map (fn (_, (_, (inst, dss))) => IConst (inst, ((([], dss), ([], ITyVar "")), false))) super_instances
@ map (IConst o snd o fst) classparam_instances)]))];