--- a/NEWS Tue Apr 12 13:49:37 2016 +0200
+++ b/NEWS Tue Apr 12 14:38:57 2016 +0200
@@ -9,6 +9,13 @@
*** General ***
+* Type-inference improves sorts of newly introduced type variables for
+the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).
+Thus terms like "f x" or "\<And>x. P x" without any further syntactic context
+produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare
+INCOMPATIBILITY, need to provide explicit type constraints for Pure
+types where this is really intended.
+
* Mixfix annotations support general block properties, with syntax
"(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent",
"unbreakable", "markup". The existing notation "(DIGITS" is equivalent
--- a/src/HOL/Code_Evaluation.thy Tue Apr 12 13:49:37 2016 +0200
+++ b/src/HOL/Code_Evaluation.thy Tue Apr 12 14:38:57 2016 +0200
@@ -69,6 +69,7 @@
subsection \<open>Tools setup and evaluation\<close>
lemma eq_eq_TrueD:
+ fixes x y :: "'a::{}"
assumes "(x \<equiv> y) \<equiv> Trueprop True"
shows "x \<equiv> y"
using assms by simp
--- a/src/HOL/HOL.thy Tue Apr 12 13:49:37 2016 +0200
+++ b/src/HOL/HOL.thy Tue Apr 12 14:38:57 2016 +0200
@@ -747,7 +747,7 @@
lemma swap: "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"
by (rule classical) iprover
-lemma thin_refl: "\<And>X. \<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W" .
+lemma thin_refl: "\<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W" .
ML \<open>
structure Hypsubst = Hypsubst
@@ -1506,7 +1506,7 @@
unfolding induct_true_def
by (iprover intro: equal_intr_rule)
-lemma [induct_simp]: "(\<And>x. induct_true) \<equiv> Trueprop induct_true"
+lemma [induct_simp]: "(\<And>x::'a::{}. induct_true) \<equiv> Trueprop induct_true"
unfolding induct_true_def
by (iprover intro: equal_intr_rule)
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Tue Apr 12 13:49:37 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Tue Apr 12 14:38:57 2016 +0200
@@ -1052,7 +1052,7 @@
val deadfixed_T =
build_map lthy [] (mk_undefined o op -->) (apply2 tupleT_of_funT (param1_T, param2_T))
|> singleton (Type_Infer_Context.infer_types lthy)
- |> singleton (Type_Infer.fixate lthy)
+ |> singleton (Type_Infer.fixate lthy false)
|> type_of
|> dest_funT
|-> generalize_types 1
--- a/src/HOL/Tools/Function/function.ML Tue Apr 12 13:49:37 2016 +0200
+++ b/src/HOL/Tools/Function/function.ML Tue Apr 12 14:38:57 2016 +0200
@@ -80,11 +80,7 @@
fun prepare_function do_print prep fixspec eqns config lthy =
let
- val ((fixes0, spec0), ctxt') =
- lthy
- |> Proof_Context.set_object_logic_constraint
- |> prep fixspec eqns
- ||> Proof_Context.restore_object_logic_constraint lthy;
+ val ((fixes0, spec0), ctxt') = prep fixspec eqns lthy;
val fixes = map (apfst (apfst Binding.name_of)) fixes0;
val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Tue Apr 12 13:49:37 2016 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Tue Apr 12 14:38:57 2016 +0200
@@ -120,7 +120,7 @@
th RS @{thm eq_reflection}
| _ => th)
-val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
+val meta_fun_cong = @{lemma "\<And>f :: 'a::{} \<Rightarrow> 'b::{}.f == g ==> f x == g x" by simp}
fun full_fun_cong_expand th =
let
--- a/src/HOL/Tools/Transfer/transfer.ML Tue Apr 12 13:49:37 2016 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Tue Apr 12 14:38:57 2016 +0200
@@ -518,8 +518,7 @@
end
| go _ ctxt = dummy ctxt
in
- go t ctxt |> fst |> Syntax.check_term ctxt |>
- map_types (map_type_tfree (fn (a, _) => TFree (a, @{sort type})))
+ go t ctxt |> fst |> Syntax.check_term ctxt
end
(** Monotonicity analysis **)
--- a/src/HOL/Tools/record.ML Tue Apr 12 13:49:37 2016 +0200
+++ b/src/HOL/Tools/record.ML Tue Apr 12 14:38:57 2016 +0200
@@ -1063,7 +1063,7 @@
*)
val simproc =
Simplifier.make_simproc @{context} "record"
- {lhss = [@{term "x"}],
+ {lhss = [@{term "x::'a::{}"}],
proc = fn _ => fn ctxt => fn ct =>
let
val thy = Proof_Context.theory_of ctxt;
@@ -1147,7 +1147,7 @@
both a more update and an update to a field within it.*)
val upd_simproc =
Simplifier.make_simproc @{context} "record_upd"
- {lhss = [@{term "x"}],
+ {lhss = [@{term "x::'a::{}"}],
proc = fn _ => fn ctxt => fn ct =>
let
val thy = Proof_Context.theory_of ctxt;
@@ -1292,7 +1292,7 @@
P t > 0: split up to given bound of record extensions.*)
fun split_simproc P =
Simplifier.make_simproc @{context} "record_split"
- {lhss = [@{term x}],
+ {lhss = [@{term "x::'a::{}"}],
proc = fn _ => fn ctxt => fn ct =>
(case Thm.term_of ct of
Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
--- a/src/Pure/Isar/expression.ML Tue Apr 12 13:49:37 2016 +0200
+++ b/src/Pure/Isar/expression.ML Tue Apr 12 14:38:57 2016 +0200
@@ -175,7 +175,7 @@
val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types;
val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
val arg = type_parms @ map2 Type.constraint parm_types' insts';
- val res = Syntax.check_terms ctxt arg;
+ val res = Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt) arg;
val ctxt' = ctxt |> fold Variable.auto_fixes res;
(* instantiation *)
--- a/src/Pure/Isar/proof_context.ML Tue Apr 12 13:49:37 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Apr 12 14:38:57 2016 +0200
@@ -666,7 +666,7 @@
fun prepare_patterns ctxt =
let val Mode {pattern, ...} = get_mode ctxt in
- Type_Infer.fixate ctxt #>
+ Type_Infer.fixate ctxt pattern #>
pattern ? Variable.polymorphic ctxt #>
(map o Term.map_types) (prepare_patternT ctxt) #>
(if pattern then prepare_dummies else map (check_dummies ctxt))
--- a/src/Pure/Proof/extraction.ML Tue Apr 12 13:49:37 2016 +0200
+++ b/src/Pure/Proof/extraction.ML Tue Apr 12 14:38:57 2016 +0200
@@ -167,8 +167,9 @@
fun read_term ctxt T s =
let
val ctxt' = ctxt
- |> Config.put Type_Infer_Context.const_sorts false
- |> Proof_Context.set_defsort [];
+ |> Proof_Context.set_defsort []
+ |> Config.put Type_Infer.object_logic false
+ |> Config.put Type_Infer_Context.const_sorts false;
val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
in parse ctxt' s |> Type.constraint T |> Syntax.check_term ctxt' end;
--- a/src/Pure/Proof/proof_syntax.ML Tue Apr 12 13:49:37 2016 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Tue Apr 12 14:38:57 2016 +0200
@@ -215,7 +215,10 @@
|> Proof_Context.init_global
|> Proof_Context.allow_dummies
|> Proof_Context.set_mode Proof_Context.mode_schematic
- |> topsort ? (Config.put Type_Infer_Context.const_sorts false #> Proof_Context.set_defsort []);
+ |> topsort ?
+ (Proof_Context.set_defsort [] #>
+ Config.put Type_Infer.object_logic false #>
+ Config.put Type_Infer_Context.const_sorts false);
in
fn ty => fn s =>
(if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s
--- a/src/Pure/type_infer.ML Tue Apr 12 13:49:37 2016 +0200
+++ b/src/Pure/type_infer.ML Tue Apr 12 14:38:57 2016 +0200
@@ -16,7 +16,8 @@
val paramify_vars: typ -> typ
val deref: typ Vartab.table -> typ -> typ
val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list
- val fixate: Proof.context -> term list -> term list
+ val object_logic: bool Config.T
+ val fixate: Proof.context -> bool -> term list -> term list
end;
structure Type_Infer: TYPE_INFER =
@@ -99,14 +100,22 @@
(* fixate -- introduce fresh type variables *)
-fun fixate ctxt ts =
+val object_logic =
+ Config.bool (Config.declare ("Type_Infer.object_logic", @{here}) (K (Config.Bool true)));
+
+fun fixate ctxt pattern ts =
let
+ val base_sort = Object_Logic.get_base_sort ctxt;
+ val improve_sort =
+ if is_some base_sort andalso not pattern andalso Config.get ctxt object_logic
+ then fn [] => the base_sort | S => S else I;
+
fun subst_param (xi, S) (inst, used) =
if is_param xi then
let
val [a] = Name.invent used Name.aT 1;
val used' = Name.declare a used;
- in (((xi, S), TFree (a, S)) :: inst, used') end
+ in (((xi, S), TFree (a, improve_sort S)) :: inst, used') end
else (inst, used);
val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
--- a/src/Tools/induct.ML Tue Apr 12 13:49:37 2016 +0200
+++ b/src/Tools/induct.ML Tue Apr 12 14:38:57 2016 +0200
@@ -172,7 +172,7 @@
val rearrange_eqs_simproc =
Simplifier.make_simproc @{context} "rearrange_eqs"
- {lhss = [@{term "Pure.all(t)"}],
+ {lhss = [@{term "Pure.all (t :: 'a::{} \<Rightarrow> prop)"}],
proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct};
--- a/src/Tools/nbe.ML Tue Apr 12 13:49:37 2016 +0200
+++ b/src/Tools/nbe.ML Tue Apr 12 14:38:57 2016 +0200
@@ -544,7 +544,10 @@
val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt);
val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
fun type_infer t' =
- Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt)
+ Syntax.check_term
+ (ctxt
+ |> Config.put Type_Infer.object_logic false
+ |> Config.put Type_Infer_Context.const_sorts false)
(Type.constraint (fastype_of t_original) t');
fun check_tvars t' =
if null (Term.add_tvars t' []) then t'