--- a/NEWS Tue Apr 12 11:18:29 2016 +0200
+++ b/NEWS Tue Apr 12 15:01:06 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 11:18:29 2016 +0200
+++ b/src/HOL/Code_Evaluation.thy Tue Apr 12 15:01:06 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 11:18:29 2016 +0200
+++ b/src/HOL/HOL.thy Tue Apr 12 15:01:06 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/Library/Quotient_List.thy Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Library/Quotient_List.thy Tue Apr 12 15:01:06 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Quotient infrastructure for the list type\<close>
theory Quotient_List
-imports Main Quotient_Set Quotient_Product Quotient_Option
+imports Quotient_Set Quotient_Product Quotient_Option
begin
subsection \<open>Rules for the Quotient package\<close>
--- a/src/HOL/Library/Quotient_Option.thy Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Library/Quotient_Option.thy Tue Apr 12 15:01:06 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Quotient infrastructure for the option type\<close>
theory Quotient_Option
-imports Main Quotient_Syntax
+imports Quotient_Syntax
begin
subsection \<open>Rules for the Quotient package\<close>
--- a/src/HOL/Library/Quotient_Product.thy Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Library/Quotient_Product.thy Tue Apr 12 15:01:06 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Quotient infrastructure for the product type\<close>
theory Quotient_Product
-imports Main Quotient_Syntax
+imports Quotient_Syntax
begin
subsection \<open>Rules for the Quotient package\<close>
--- a/src/HOL/Library/Quotient_Set.thy Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Library/Quotient_Set.thy Tue Apr 12 15:01:06 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Quotient infrastructure for the set type\<close>
theory Quotient_Set
-imports Main Quotient_Syntax
+imports Quotient_Syntax
begin
subsection \<open>Contravariant set map (vimage) and set relator, rules for the Quotient package\<close>
--- a/src/HOL/Library/Quotient_Sum.thy Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Library/Quotient_Sum.thy Tue Apr 12 15:01:06 2016 +0200
@@ -5,7 +5,7 @@
section \<open>Quotient infrastructure for the sum type\<close>
theory Quotient_Sum
-imports Main Quotient_Syntax
+imports Quotient_Syntax
begin
subsection \<open>Rules for the Quotient package\<close>
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML Tue Apr 12 15:01:06 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 11:18:29 2016 +0200
+++ b/src/HOL/Tools/Function/function.ML Tue Apr 12 15:01:06 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 11:18:29 2016 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Tue Apr 12 15:01:06 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/Quotient/quotient_def.ML Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Tue Apr 12 15:01:06 2016 +0200
@@ -134,18 +134,14 @@
val (opt_var, ctxt) =
(case raw_var of
NONE => (NONE, lthy)
- | SOME var =>
- Proof_Context.set_object_logic_constraint lthy
- |> prep_var var
- ||> Proof_Context.restore_object_logic_constraint lthy
- |>> SOME)
- val lhs_constraint = (case opt_var of SOME (_, SOME T, _) => T | _ => dummyT)
+ | SOME var => prep_var var lthy |>> SOME)
+ val lhs_constraints = (case opt_var of SOME (_, SOME T, _) => [T] | _ => [])
- fun prep_term T = parse_term ctxt #> Type.constraint T #> Syntax.check_term ctxt;
- val lhs = prep_term lhs_constraint raw_lhs
- val rhs = prep_term dummyT raw_rhs
+ fun prep_term Ts = parse_term ctxt #> fold Type.constraint Ts #> Syntax.check_term ctxt;
+ val lhs = prep_term lhs_constraints raw_lhs
+ val rhs = prep_term [] raw_rhs
- val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
+ val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined"
val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
val _ = if is_Const rhs then () else warning "The definiens is not a constant"
--- a/src/HOL/Tools/Transfer/transfer.ML Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Tue Apr 12 15:01:06 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/code_evaluation.ML Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Tools/code_evaluation.ML Tue Apr 12 15:01:06 2016 +0200
@@ -165,9 +165,9 @@
| NONE => NONE)
| subst_termify t = subst_termify_app (strip_comb t)
-fun check_termify _ ts = the_default ts (map_default subst_termify ts);
+fun check_termify ts = the_default ts (map_default subst_termify ts);
-val _ = Context.>> (Syntax_Phases.term_check 0 "termify" check_termify);
+val _ = Context.>> (Syntax_Phases.term_check 0 "termify" (K check_termify));
(** evaluation **)
--- a/src/HOL/Tools/record.ML Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Tools/record.ML Tue Apr 12 15:01:06 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/HOL/Transitive_Closure.thy Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Transitive_Closure.thy Tue Apr 12 15:01:06 2016 +0200
@@ -534,7 +534,7 @@
lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+"
by (blast elim: tranclE dest: trancl_into_rtrancl)
-lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y"
+lemma irrefl_trancl_rD: "\<forall>x. (x, x) \<notin> r^+ \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> x \<noteq> y"
by (blast dest: r_into_trancl)
lemma trancl_subset_Sigma_aux:
--- a/src/HOL/Word/Bool_List_Representation.thy Tue Apr 12 11:18:29 2016 +0200
+++ b/src/HOL/Word/Bool_List_Representation.thy Tue Apr 12 15:01:06 2016 +0200
@@ -993,7 +993,7 @@
lemma bin_rsplit_size_sign' [rule_format] :
"\<lbrakk>n > 0; rev sw = bin_rsplit n (nw, w)\<rbrakk> \<Longrightarrow>
(ALL v: set sw. bintrunc n v = v)"
- apply (induct sw arbitrary: nw w v)
+ apply (induct sw arbitrary: nw w)
apply clarsimp
apply clarsimp
apply (drule bthrs)
--- a/src/Pure/Isar/class_declaration.ML Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/Isar/class_declaration.ML Tue Apr 12 15:01:06 2016 +0200
@@ -107,7 +107,6 @@
fun prep_class_elems prep_decl thy sups raw_elems =
let
-
(* user space type system: only permits 'a type variable, improves towards 'a *)
val algebra = Sign.classes_of thy;
val inter_sort = curry (Sorts.inter_sort algebra);
@@ -118,7 +117,7 @@
val base_constraints = (map o apsnd)
(map_type_tfree (K (TVar ((Name.aT, 0), proto_base_sort))) o fst o fst o snd)
(Class.these_operations thy sups);
- fun singleton_fixateT Ts =
+ val singleton_fixate = burrow_types (fn Ts =>
let
val tfrees = fold Term.add_tfreesT Ts [];
val inferred_sort =
@@ -140,9 +139,8 @@
in
(map o map_atyps)
(fn T as TVar (xi, _) => if Type_Infer.is_param xi then fixateT else T | T => T) Ts
- end;
- fun singleton_fixate _ ts = burrow_types singleton_fixateT ts;
- fun unify_params ctxt ts =
+ end);
+ fun unify_params ts =
let
val param_Ts = (fold o fold_aterms)
(fn Free (v, T) => if is_param v then fold_atyps (insert (op =)) T else I | _ => I) ts [];
@@ -162,10 +160,10 @@
val init_class_body =
fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints
#> Class.redeclare_operations thy sups
- #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" singleton_fixate);
+ #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" (K singleton_fixate));
val ((raw_supparams, _, raw_inferred_elems, _), _) =
Proof_Context.init_global thy
- |> Context.proof_map (Syntax_Phases.term_check 0 "unify_params" unify_params)
+ |> Context.proof_map (Syntax_Phases.term_check 0 "unify_params" (K unify_params))
|> prep_decl raw_supexpr init_class_body raw_elems;
fun filter_element (Element.Fixes []) = NONE
| filter_element (e as Element.Fixes _) = SOME e
--- a/src/Pure/Isar/expression.ML Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/Isar/expression.ML Tue Apr 12 15:01:06 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.ML Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/Isar/proof.ML Tue Apr 12 15:01:06 2016 +0200
@@ -600,7 +600,7 @@
let
val ctxt' =
ctxt |> is_none (Variable.default_type ctxt x) ?
- Variable.declare_constraints (Free (x, Proof_Context.default_constraint ctxt mx));
+ Variable.declare_constraints (Free (x, Mixfix.default_constraint mx));
val t = Free (#1 (Proof_Context.inferred_param x ctxt'));
in ((t, mx), ctxt') end
| t => ((t, mx), ctxt));
--- a/src/Pure/Isar/proof_context.ML Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Apr 12 15:01:06 2016 +0200
@@ -130,9 +130,6 @@
val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
- val set_object_logic_constraint: Proof.context -> Proof.context
- val restore_object_logic_constraint: Proof.context -> Proof.context -> Proof.context
- val default_constraint: Proof.context -> mixfix -> typ
val read_var: binding * string option * mixfix -> Proof.context ->
(binding * typ option * mixfix) * Proof.context
val cert_var: binding * typ option * mixfix -> Proof.context ->
@@ -666,7 +663,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))
@@ -1059,33 +1056,10 @@
(** basic logical entities **)
-(* default type constraint *)
-
-val object_logic_constraint =
- Config.bool
- (Config.declare ("Proof_Context.object_logic_constraint", @{here}) (K (Config.Bool false)));
-
-val set_object_logic_constraint = Config.put object_logic_constraint true;
-fun restore_object_logic_constraint ctxt =
- Config.put object_logic_constraint (Config.get ctxt object_logic_constraint);
-
-fun default_constraint ctxt mx =
- let
- val A =
- (case (Object_Logic.get_base_sort ctxt, Config.get ctxt object_logic_constraint) of
- (SOME S, true) => Type_Infer.anyT S
- | _ => dummyT);
- in
- (case mx of
- Binder _ => (A --> A) --> A
- | _ => replicate (Mixfix.mixfix_args mx) A ---> A)
- end;
-
-
(* variables *)
fun declare_var (x, opt_T, mx) ctxt =
- let val T = (case opt_T of SOME T => T | NONE => default_constraint ctxt mx)
+ let val T = (case opt_T of SOME T => T | NONE => Mixfix.default_constraint mx)
in (T, ctxt |> Variable.declare_constraints (Free (x, T))) end;
fun add_syntax vars ctxt =
--- a/src/Pure/Proof/extraction.ML Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/Proof/extraction.ML Tue Apr 12 15:01:06 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 11:18:29 2016 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Tue Apr 12 15:01:06 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/Syntax/mixfix.ML Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/Syntax/mixfix.ML Tue Apr 12 15:01:06 2016 +0200
@@ -27,6 +27,7 @@
val reset_pos: mixfix -> mixfix
val pretty_mixfix: mixfix -> Pretty.T
val mixfix_args: mixfix -> int
+ val default_constraint: mixfix -> typ
val make_type: int -> typ
val binder_name: string -> string
val syn_ext_types: (string * typ * mixfix) list -> Syntax_Ext.syn_ext
@@ -118,6 +119,12 @@
| mixfix_args (Structure _) = 0;
+(* default type constraint *)
+
+fun default_constraint (Binder _) = (dummyT --> dummyT) --> dummyT
+ | default_constraint mx = replicate (mixfix_args mx) dummyT ---> dummyT;
+
+
(* syn_ext_types *)
val typeT = Type ("type", []);
--- a/src/Pure/Syntax/syntax_phases.ML Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Tue Apr 12 15:01:06 2016 +0200
@@ -970,18 +970,7 @@
end;
-(* standard phases *)
-
-val _ = Context.>>
- (typ_check 0 "standard" Proof_Context.standard_typ_check #>
- term_check 0 "standard"
- (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #>
- term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #>
- term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);
-
-
-
-(** install operations **)
+(* install operations *)
val _ =
Theory.setup
@@ -1000,3 +989,13 @@
uncheck_terms = uncheck_terms});
end;
+
+
+(* standard phases *)
+
+val _ = Context.>>
+ (Syntax_Phases.typ_check 0 "standard" Proof_Context.standard_typ_check #>
+ Syntax_Phases.term_check 0 "standard"
+ (fn ctxt => Type_Infer_Context.infer_types ctxt #> map (Proof_Context.expand_abbrevs ctxt)) #>
+ Syntax_Phases.term_check 100 "standard_finish" Proof_Context.standard_term_check_finish #>
+ Syntax_Phases.term_uncheck 0 "standard" Proof_Context.standard_term_uncheck);
--- a/src/Pure/System/isabelle_tool.scala Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/System/isabelle_tool.scala Tue Apr 12 15:01:06 2016 +0200
@@ -50,34 +50,27 @@
/* internal tools */
- private var internal_tools = Map.empty[String, (String, List[String] => Nothing)]
+ private val internal_tools: List[Isabelle_Tool] =
+ List(
+ Build.isabelle_tool,
+ Build_Doc.isabelle_tool,
+ Check_Sources.isabelle_tool,
+ Doc.isabelle_tool,
+ ML_Process.isabelle_tool,
+ Options.isabelle_tool,
+ Update_Cartouches.isabelle_tool,
+ Update_Header.isabelle_tool,
+ Update_Then.isabelle_tool,
+ Update_Theorems.isabelle_tool)
private def list_internal(): List[(String, String)] =
- synchronized {
- for ((name, (description, _)) <- internal_tools.toList) yield (name, description)
- }
+ for (tool <- internal_tools.toList) yield (tool.name, tool.description)
private def find_internal(name: String): Option[List[String] => Unit] =
- synchronized { internal_tools.get(name).map(_._2) }
-
- private def register(isabelle_tool: Isabelle_Tool): Unit =
- synchronized {
- internal_tools +=
- (isabelle_tool.name ->
- (isabelle_tool.description,
- args => Command_Line.tool0 { isabelle_tool.body(args) }))
- }
-
- register(Build.isabelle_tool)
- register(Build_Doc.isabelle_tool)
- register(Check_Sources.isabelle_tool)
- register(Doc.isabelle_tool)
- register(ML_Process.isabelle_tool)
- register(Options.isabelle_tool)
- register(Update_Cartouches.isabelle_tool)
- register(Update_Header.isabelle_tool)
- register(Update_Then.isabelle_tool)
- register(Update_Theorems.isabelle_tool)
+ internal_tools.collectFirst({
+ case tool if tool.name == name =>
+ args => Command_Line.tool0 { tool.body(args) }
+ })
/* command line entry point */
--- a/src/Pure/type_infer.ML Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/type_infer.ML Tue Apr 12 15:01:06 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/Pure/variable.ML Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Pure/variable.ML Tue Apr 12 15:01:06 2016 +0200
@@ -230,9 +230,6 @@
(* constraints *)
-fun constrain_var (xi, T) =
- if T = dummyT then Vartab.delete_safe xi else Vartab.update (xi, T);
-
fun constrain_tvar (xi, raw_S) =
let val S = #2 (Term_Position.decode_positionS raw_S)
in if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S) end;
@@ -240,8 +237,8 @@
fun declare_constraints t = map_constraints (fn (types, sorts) =>
let
val types' = fold_aterms
- (fn Free (x, T) => constrain_var ((x, ~1), T)
- | Var v => constrain_var v
+ (fn Free (x, T) => Vartab.update ((x, ~1), T)
+ | Var v => Vartab.update v
| _ => I) t types;
val sorts' = (fold_types o fold_atyps)
(fn TFree (x, S) => constrain_tvar ((x, ~1), S)
--- a/src/Tools/induct.ML Tue Apr 12 11:18:29 2016 +0200
+++ b/src/Tools/induct.ML Tue Apr 12 15:01:06 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 11:18:29 2016 +0200
+++ b/src/Tools/nbe.ML Tue Apr 12 15:01:06 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'