explicit argument expansion of uncheck rules;
authorhaftmann
Mon Jun 01 18:59:20 2015 +0200 (2015-06-01)
changeset 603477d64ad9910e2
parent 60346 90d0103af558
child 60348 e66830e878e3
explicit argument expansion of uncheck rules;
rewriting of user-space type system must behave similarly to abbreviations
NEWS
src/Pure/Isar/class.ML
src/Pure/Isar/overloading.ML
     1.1 --- a/NEWS	Mon Jun 01 18:59:20 2015 +0200
     1.2 +++ b/NEWS	Mon Jun 01 18:59:20 2015 +0200
     1.3 @@ -13,6 +13,17 @@
     1.4  (intermediate legacy feature in Isabelle2015).  INCOMPATIBILITY.
     1.5  
     1.6  
     1.7 +*** Pure ***
     1.8 +
     1.9 +* Abbreviations in type classes now carry proper sort constraint.
    1.10 +Rare INCOMPATIBILITY in situations where the previous misbehaviour
    1.11 +has been exploited previously.
    1.12 +
    1.13 +* Refinement of user-space type system in type classes: pseudo-local
    1.14 +operations behave more similar to abbreviations.  Potential
    1.15 +INCOMPATIBILITY in exotic situations.
    1.16 +
    1.17 +
    1.18  *** HOL ***
    1.19  
    1.20  * Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.
     2.1 --- a/src/Pure/Isar/class.ML	Mon Jun 01 18:59:20 2015 +0200
     2.2 +++ b/src/Pure/Isar/class.ML	Mon Jun 01 18:59:20 2015 +0200
     2.3 @@ -259,9 +259,22 @@
     2.4  
     2.5  (* class context syntax *)
     2.6  
     2.7 +fun make_rewrite t c_ty =
     2.8 +  let
     2.9 +    val (vs, t') = strip_abs t;
    2.10 +    val vts = map snd vs
    2.11 +      |> Name.invent_names Name.context Name.uu
    2.12 +      |> map (fn (v, T) => Var ((v, 0), T));
    2.13 +  in (betapplys (t, vts), betapplys (Const c_ty, vts)) end;
    2.14 +
    2.15  fun these_unchecks thy =
    2.16 -  map_filter (fn (c, (_, ((ty, t), input_only))) => if input_only then NONE else SOME (t, Const (c, ty)))
    2.17 -  o these_operations thy;
    2.18 +  these_operations thy
    2.19 +  #> map_filter (fn (c, (_, ((ty, t), input_only))) =>
    2.20 +    if input_only then NONE else SOME (make_rewrite t (c, ty)));
    2.21 +
    2.22 +fun these_unchecks_reversed thy =
    2.23 +  these_operations thy
    2.24 +  #> map (fn (c, (_, ((ty, t), _))) => (Const (c, ty), t));
    2.25  
    2.26  fun redeclare_const thy c =
    2.27    let val b = Long_Name.base_name c
    2.28 @@ -421,7 +434,7 @@
    2.29  fun canonical_abbrev_target class phi prmode ((b, mx), rhs) lthy =
    2.30    let
    2.31      val thy = Proof_Context.theory_of lthy;
    2.32 -    val preprocess = perhaps (try (Pattern.rewrite_term thy (these_unchecks thy [class]) []));
    2.33 +    val preprocess = perhaps (try (Pattern.rewrite_term_top thy (these_unchecks thy [class]) []));
    2.34      val (global_rhs, (extra_tfrees, (type_params, term_params))) =
    2.35        Generic_Target.export_abbrev lthy preprocess rhs;
    2.36      val mx' = Generic_Target.check_mixfix_global (b, null term_params) mx;
    2.37 @@ -443,7 +456,7 @@
    2.38      val thy = Proof_Context.theory_of lthy;
    2.39      val phi = morphism thy class;
    2.40      val rhs_generic =
    2.41 -      perhaps (try (Pattern.rewrite_term thy (map swap (these_unchecks thy [class])) [])) rhs;
    2.42 +      perhaps (try (Pattern.rewrite_term_top thy (these_unchecks_reversed thy [class]) [])) rhs;
    2.43    in
    2.44      lthy
    2.45      |> canonical_abbrev_target class phi prmode ((b, mx), rhs)
     3.1 --- a/src/Pure/Isar/overloading.ML	Mon Jun 01 18:59:20 2015 +0200
     3.2 +++ b/src/Pure/Isar/overloading.ML	Mon Jun 01 18:59:20 2015 +0200
     3.3 @@ -87,7 +87,7 @@
     3.4    end;
     3.5  
     3.6  fun rewrite_liberal thy unchecks t =
     3.7 -  (case try (Pattern.rewrite_term thy unchecks []) t of
     3.8 +  (case try (Pattern.rewrite_term_top thy unchecks []) t of
     3.9      NONE => NONE
    3.10    | SOME t' => if t aconv t' then NONE else SOME t');
    3.11