Type_Infer.object_logic controls improvement of type inference result;
authorwenzelm
Tue Apr 12 14:38:57 2016 +0200 (2016-04-12)
changeset 62958b41c1cb5e251
parent 62957 a9c40cf517d1
child 62959 19c2a58623ed
Type_Infer.object_logic controls improvement of type inference result;
NEWS
src/HOL/Code_Evaluation.thy
src/HOL/HOL.thy
src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/HOL/Tools/Transfer/transfer.ML
src/HOL/Tools/record.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/proof_context.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/type_infer.ML
src/Tools/induct.ML
src/Tools/nbe.ML
     1.1 --- a/NEWS	Tue Apr 12 13:49:37 2016 +0200
     1.2 +++ b/NEWS	Tue Apr 12 14:38:57 2016 +0200
     1.3 @@ -9,6 +9,13 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Type-inference improves sorts of newly introduced type variables for
     1.8 +the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL).
     1.9 +Thus terms like "f x" or "\<And>x. P x" without any further syntactic context
    1.10 +produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare
    1.11 +INCOMPATIBILITY, need to provide explicit type constraints for Pure
    1.12 +types where this is really intended.
    1.13 +
    1.14  * Mixfix annotations support general block properties, with syntax
    1.15  "(\<open>x=a y=b z \<dots>\<close>". Notable property names are "indent", "consistent",
    1.16  "unbreakable", "markup". The existing notation "(DIGITS" is equivalent
     2.1 --- a/src/HOL/Code_Evaluation.thy	Tue Apr 12 13:49:37 2016 +0200
     2.2 +++ b/src/HOL/Code_Evaluation.thy	Tue Apr 12 14:38:57 2016 +0200
     2.3 @@ -69,6 +69,7 @@
     2.4  subsection \<open>Tools setup and evaluation\<close>
     2.5  
     2.6  lemma eq_eq_TrueD:
     2.7 +  fixes x y :: "'a::{}"
     2.8    assumes "(x \<equiv> y) \<equiv> Trueprop True"
     2.9    shows "x \<equiv> y"
    2.10    using assms by simp
     3.1 --- a/src/HOL/HOL.thy	Tue Apr 12 13:49:37 2016 +0200
     3.2 +++ b/src/HOL/HOL.thy	Tue Apr 12 14:38:57 2016 +0200
     3.3 @@ -747,7 +747,7 @@
     3.4  lemma swap: "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"
     3.5    by (rule classical) iprover
     3.6  
     3.7 -lemma thin_refl: "\<And>X. \<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W" .
     3.8 +lemma thin_refl: "\<lbrakk>x = x; PROP W\<rbrakk> \<Longrightarrow> PROP W" .
     3.9  
    3.10  ML \<open>
    3.11  structure Hypsubst = Hypsubst
    3.12 @@ -1506,7 +1506,7 @@
    3.13    unfolding induct_true_def
    3.14    by (iprover intro: equal_intr_rule)
    3.15  
    3.16 -lemma [induct_simp]: "(\<And>x. induct_true) \<equiv> Trueprop induct_true"
    3.17 +lemma [induct_simp]: "(\<And>x::'a::{}. induct_true) \<equiv> Trueprop induct_true"
    3.18    unfolding induct_true_def
    3.19    by (iprover intro: equal_intr_rule)
    3.20  
     4.1 --- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Apr 12 13:49:37 2016 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue Apr 12 14:38:57 2016 +0200
     4.3 @@ -1052,7 +1052,7 @@
     4.4          val deadfixed_T =
     4.5            build_map lthy [] (mk_undefined o op -->) (apply2 tupleT_of_funT (param1_T, param2_T))
     4.6            |> singleton (Type_Infer_Context.infer_types lthy)
     4.7 -          |> singleton (Type_Infer.fixate lthy)
     4.8 +          |> singleton (Type_Infer.fixate lthy false)
     4.9            |> type_of
    4.10            |> dest_funT
    4.11            |-> generalize_types 1
     5.1 --- a/src/HOL/Tools/Function/function.ML	Tue Apr 12 13:49:37 2016 +0200
     5.2 +++ b/src/HOL/Tools/Function/function.ML	Tue Apr 12 14:38:57 2016 +0200
     5.3 @@ -80,11 +80,7 @@
     5.4  
     5.5  fun prepare_function do_print prep fixspec eqns config lthy =
     5.6    let
     5.7 -    val ((fixes0, spec0), ctxt') =
     5.8 -      lthy
     5.9 -      |> Proof_Context.set_object_logic_constraint
    5.10 -      |> prep fixspec eqns
    5.11 -      ||> Proof_Context.restore_object_logic_constraint lthy;
    5.12 +    val ((fixes0, spec0), ctxt') = prep fixspec eqns lthy;
    5.13      val fixes = map (apfst (apfst Binding.name_of)) fixes0;
    5.14      val spec = map (fn (bnd, prop) => (bnd, [prop])) spec0;
    5.15      val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Tue Apr 12 13:49:37 2016 +0200
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Tue Apr 12 14:38:57 2016 +0200
     6.3 @@ -120,7 +120,7 @@
     6.4        th RS @{thm eq_reflection}
     6.5    | _ => th)
     6.6  
     6.7 -val meta_fun_cong = @{lemma "f == g ==> f x == g x" by simp}
     6.8 +val meta_fun_cong = @{lemma "\<And>f :: 'a::{} \<Rightarrow> 'b::{}.f == g ==> f x == g x" by simp}
     6.9  
    6.10  fun full_fun_cong_expand th =
    6.11    let
     7.1 --- a/src/HOL/Tools/Transfer/transfer.ML	Tue Apr 12 13:49:37 2016 +0200
     7.2 +++ b/src/HOL/Tools/Transfer/transfer.ML	Tue Apr 12 14:38:57 2016 +0200
     7.3 @@ -518,8 +518,7 @@
     7.4          end
     7.5        | go _ ctxt = dummy ctxt
     7.6    in
     7.7 -    go t ctxt |> fst |> Syntax.check_term ctxt |>
     7.8 -      map_types (map_type_tfree (fn (a, _) => TFree (a, @{sort type})))
     7.9 +    go t ctxt |> fst |> Syntax.check_term ctxt
    7.10    end
    7.11  
    7.12  (** Monotonicity analysis **)
     8.1 --- a/src/HOL/Tools/record.ML	Tue Apr 12 13:49:37 2016 +0200
     8.2 +++ b/src/HOL/Tools/record.ML	Tue Apr 12 14:38:57 2016 +0200
     8.3 @@ -1063,7 +1063,7 @@
     8.4  *)
     8.5  val simproc =
     8.6    Simplifier.make_simproc @{context} "record"
     8.7 -   {lhss = [@{term "x"}],
     8.8 +   {lhss = [@{term "x::'a::{}"}],
     8.9      proc = fn _ => fn ctxt => fn ct =>
    8.10        let
    8.11          val thy = Proof_Context.theory_of ctxt;
    8.12 @@ -1147,7 +1147,7 @@
    8.13    both a more update and an update to a field within it.*)
    8.14  val upd_simproc =
    8.15    Simplifier.make_simproc @{context} "record_upd"
    8.16 -   {lhss = [@{term "x"}],
    8.17 +   {lhss = [@{term "x::'a::{}"}],
    8.18      proc = fn _ => fn ctxt => fn ct =>
    8.19        let
    8.20          val thy = Proof_Context.theory_of ctxt;
    8.21 @@ -1292,7 +1292,7 @@
    8.22      P t > 0: split up to given bound of record extensions.*)
    8.23  fun split_simproc P =
    8.24    Simplifier.make_simproc @{context} "record_split"
    8.25 -   {lhss = [@{term x}],
    8.26 +   {lhss = [@{term "x::'a::{}"}],
    8.27      proc = fn _ => fn ctxt => fn ct =>
    8.28        (case Thm.term_of ct of
    8.29          Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ =>
     9.1 --- a/src/Pure/Isar/expression.ML	Tue Apr 12 13:49:37 2016 +0200
     9.2 +++ b/src/Pure/Isar/expression.ML	Tue Apr 12 14:38:57 2016 +0200
     9.3 @@ -175,7 +175,7 @@
     9.4      val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types;
     9.5      val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
     9.6      val arg = type_parms @ map2 Type.constraint parm_types' insts';
     9.7 -    val res = Syntax.check_terms ctxt arg;
     9.8 +    val res = Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt) arg;
     9.9      val ctxt' = ctxt |> fold Variable.auto_fixes res;
    9.10  
    9.11      (* instantiation *)
    10.1 --- a/src/Pure/Isar/proof_context.ML	Tue Apr 12 13:49:37 2016 +0200
    10.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Apr 12 14:38:57 2016 +0200
    10.3 @@ -666,7 +666,7 @@
    10.4  
    10.5  fun prepare_patterns ctxt =
    10.6    let val Mode {pattern, ...} = get_mode ctxt in
    10.7 -    Type_Infer.fixate ctxt #>
    10.8 +    Type_Infer.fixate ctxt pattern #>
    10.9      pattern ? Variable.polymorphic ctxt #>
   10.10      (map o Term.map_types) (prepare_patternT ctxt) #>
   10.11      (if pattern then prepare_dummies else map (check_dummies ctxt))
    11.1 --- a/src/Pure/Proof/extraction.ML	Tue Apr 12 13:49:37 2016 +0200
    11.2 +++ b/src/Pure/Proof/extraction.ML	Tue Apr 12 14:38:57 2016 +0200
    11.3 @@ -167,8 +167,9 @@
    11.4  fun read_term ctxt T s =
    11.5    let
    11.6      val ctxt' = ctxt
    11.7 -      |> Config.put Type_Infer_Context.const_sorts false
    11.8 -      |> Proof_Context.set_defsort [];
    11.9 +      |> Proof_Context.set_defsort []
   11.10 +      |> Config.put Type_Infer.object_logic false
   11.11 +      |> Config.put Type_Infer_Context.const_sorts false;
   11.12      val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term;
   11.13    in parse ctxt' s |> Type.constraint T |> Syntax.check_term ctxt' end;
   11.14  
    12.1 --- a/src/Pure/Proof/proof_syntax.ML	Tue Apr 12 13:49:37 2016 +0200
    12.2 +++ b/src/Pure/Proof/proof_syntax.ML	Tue Apr 12 14:38:57 2016 +0200
    12.3 @@ -215,7 +215,10 @@
    12.4        |> Proof_Context.init_global
    12.5        |> Proof_Context.allow_dummies
    12.6        |> Proof_Context.set_mode Proof_Context.mode_schematic
    12.7 -      |> topsort ? (Config.put Type_Infer_Context.const_sorts false #> Proof_Context.set_defsort []);
    12.8 +      |> topsort ?
    12.9 +        (Proof_Context.set_defsort [] #>
   12.10 +         Config.put Type_Infer.object_logic false #>
   12.11 +         Config.put Type_Infer_Context.const_sorts false);
   12.12    in
   12.13      fn ty => fn s =>
   12.14        (if ty = propT then Syntax.parse_prop else Syntax.parse_term) ctxt s
    13.1 --- a/src/Pure/type_infer.ML	Tue Apr 12 13:49:37 2016 +0200
    13.2 +++ b/src/Pure/type_infer.ML	Tue Apr 12 14:38:57 2016 +0200
    13.3 @@ -16,7 +16,8 @@
    13.4    val paramify_vars: typ -> typ
    13.5    val deref: typ Vartab.table -> typ -> typ
    13.6    val finish: Proof.context -> typ Vartab.table -> typ list * term list -> typ list * term list
    13.7 -  val fixate: Proof.context -> term list -> term list
    13.8 +  val object_logic: bool Config.T
    13.9 +  val fixate: Proof.context -> bool -> term list -> term list
   13.10  end;
   13.11  
   13.12  structure Type_Infer: TYPE_INFER =
   13.13 @@ -99,14 +100,22 @@
   13.14  
   13.15  (* fixate -- introduce fresh type variables *)
   13.16  
   13.17 -fun fixate ctxt ts =
   13.18 +val object_logic =
   13.19 +  Config.bool (Config.declare ("Type_Infer.object_logic", @{here}) (K (Config.Bool true)));
   13.20 +
   13.21 +fun fixate ctxt pattern ts =
   13.22    let
   13.23 +    val base_sort = Object_Logic.get_base_sort ctxt;
   13.24 +    val improve_sort =
   13.25 +      if is_some base_sort andalso not pattern andalso Config.get ctxt object_logic
   13.26 +      then fn [] => the base_sort | S => S else I;
   13.27 +
   13.28      fun subst_param (xi, S) (inst, used) =
   13.29        if is_param xi then
   13.30          let
   13.31            val [a] = Name.invent used Name.aT 1;
   13.32            val used' = Name.declare a used;
   13.33 -        in (((xi, S), TFree (a, S)) :: inst, used') end
   13.34 +        in (((xi, S), TFree (a, improve_sort S)) :: inst, used') end
   13.35        else (inst, used);
   13.36      val used = (fold o fold_types) Term.declare_typ_names ts (Variable.names_of ctxt);
   13.37      val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], used);
    14.1 --- a/src/Tools/induct.ML	Tue Apr 12 13:49:37 2016 +0200
    14.2 +++ b/src/Tools/induct.ML	Tue Apr 12 14:38:57 2016 +0200
    14.3 @@ -172,7 +172,7 @@
    14.4  
    14.5  val rearrange_eqs_simproc =
    14.6    Simplifier.make_simproc @{context} "rearrange_eqs"
    14.7 -   {lhss = [@{term "Pure.all(t)"}],
    14.8 +   {lhss = [@{term "Pure.all (t :: 'a::{} \<Rightarrow> prop)"}],
    14.9      proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct};
   14.10  
   14.11  
    15.1 --- a/src/Tools/nbe.ML	Tue Apr 12 13:49:37 2016 +0200
    15.2 +++ b/src/Tools/nbe.ML	Tue Apr 12 14:38:57 2016 +0200
    15.3 @@ -544,7 +544,10 @@
    15.4      val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt);
    15.5      val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
    15.6      fun type_infer t' =
    15.7 -      Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt)
    15.8 +      Syntax.check_term
    15.9 +        (ctxt
   15.10 +          |> Config.put Type_Infer.object_logic false
   15.11 +          |> Config.put Type_Infer_Context.const_sorts false)
   15.12          (Type.constraint (fastype_of t_original) t');
   15.13      fun check_tvars t' =
   15.14        if null (Term.add_tvars t' []) then t'