proper abbreviations in class
authorhaftmann
Tue Apr 22 08:33:12 2008 +0200 (2008-04-22)
changeset 26730bbb5e6904d78
parent 26729 43a72d892594
child 26731 48df747c8543
proper abbreviations in class
src/Pure/Isar/class.ML
src/Pure/Isar/overloading.ML
     1.1 --- a/src/Pure/Isar/class.ML	Tue Apr 22 08:33:10 2008 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Apr 22 08:33:12 2008 +0200
     1.3 @@ -191,7 +191,6 @@
     1.4  
     1.5  fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy;
     1.6  
     1.7 -fun partial_morphism thy class = #morphism (the_class_data thy class) thy [];
     1.8  fun morphism thy class = #morphism (the_class_data thy class) thy (these_defs thy [class]);
     1.9  
    1.10  fun these_assm_intros thy =
    1.11 @@ -438,7 +437,7 @@
    1.12      ctxt
    1.13      |> fold declare_const primary_constraints
    1.14      |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints),
    1.15 -        ((improve, subst), unchecks)), false))
    1.16 +        (((improve, subst), true), unchecks)), false))
    1.17      |> Overloading.set_primary_constraints
    1.18    end;
    1.19  
    1.20 @@ -581,7 +580,7 @@
    1.21    let
    1.22      val prfx = class_prefix class;
    1.23      val thy' = thy |> Sign.add_path prfx;
    1.24 -    val phi = partial_morphism thy' class;
    1.25 +    val phi = morphism thy' class;
    1.26  
    1.27      val c' = Sign.full_name thy' c;
    1.28      val dict' = Morphism.term phi dict;
    1.29 @@ -608,14 +607,16 @@
    1.30    let
    1.31      val prfx = class_prefix class;
    1.32      val thy' = thy |> Sign.add_path prfx;
    1.33 -    val phi = morphism thy class;
    1.34  
    1.35 +    val unchecks = map (fn (c, (_, (ty, t))) => (t, Const (c, ty)))
    1.36 +      (these_operations thy [class]);
    1.37      val c' = Sign.full_name thy' c;
    1.38 -    val rhs' = Morphism.term phi rhs;
    1.39 -    val ty' = Logic.unvarifyT (Term.fastype_of rhs');
    1.40 +    val rhs' = Pattern.rewrite_term thy unchecks [] rhs;
    1.41 +    val rhs'' = map_types Logic.varifyT rhs';
    1.42 +    val ty' = Term.fastype_of rhs';
    1.43    in
    1.44      thy'
    1.45 -    |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs') |> snd
    1.46 +    |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs'') |> snd
    1.47      |> Sign.add_const_constraint (c', SOME ty')
    1.48      |> Sign.notation true prmode [(Const (c', ty'), mx)]
    1.49      |> register_operation class (c', (rhs', NONE))
    1.50 @@ -673,8 +674,8 @@
    1.51    in
    1.52      ctxt
    1.53      |> Overloading.map_improvable_syntax
    1.54 -         (fn (((primary_constraints, _), ((improve, _), _)), _) =>
    1.55 -            (((primary_constraints, []), ((improve, subst), unchecks)), false))
    1.56 +         (fn (((primary_constraints, _), (((improve, _), _), _)), _) =>
    1.57 +            (((primary_constraints, []), (((improve, subst), false), unchecks)), false))
    1.58    end;
    1.59  
    1.60  
    1.61 @@ -744,7 +745,7 @@
    1.62      |> fold (Variable.declare_names o Free o snd) inst_params
    1.63      |> (Overloading.map_improvable_syntax o apfst)
    1.64           (fn ((_, _), ((_, subst), unchecks)) =>
    1.65 -            ((primary_constraints, []), ((improve, K NONE), [])))
    1.66 +            ((primary_constraints, []), (((improve, K NONE), false), [])))
    1.67      |> Overloading.add_improvable_syntax
    1.68      |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
    1.69      |> synchronize_inst_syntax
     2.1 --- a/src/Pure/Isar/overloading.ML	Tue Apr 22 08:33:10 2008 +0200
     2.2 +++ b/src/Pure/Isar/overloading.ML	Tue Apr 22 08:33:12 2008 +0200
     2.3 @@ -28,7 +28,7 @@
     2.4  (** generic check/uncheck combinators for improvable constants **)
     2.5  
     2.6  type improvable_syntax = ((((string * typ) list * (string * typ) list) *
     2.7 -  (((string * typ -> (typ * typ) option) * (string * typ -> (typ * term) option)) *
     2.8 +  ((((string * typ -> (typ * typ) option) * (string * typ -> (typ * term) option)) * bool) *
     2.9      (term * term) list)) * bool);
    2.10  
    2.11  structure ImprovableSyntax = ProofDataFun(
    2.12 @@ -37,6 +37,7 @@
    2.13      secondary_constraints: (string * typ) list,
    2.14      improve: string * typ -> (typ * typ) option,
    2.15      subst: string * typ -> (typ * term) option,
    2.16 +    consider_abbrevs: bool,
    2.17      unchecks: (term * term) list,
    2.18      passed: bool
    2.19    };
    2.20 @@ -45,26 +46,32 @@
    2.21      secondary_constraints = [],
    2.22      improve = K NONE,
    2.23      subst = K NONE,
    2.24 +    consider_abbrevs = false,
    2.25      unchecks = [],
    2.26      passed = true
    2.27    };
    2.28  );
    2.29  
    2.30  fun map_improvable_syntax f = ImprovableSyntax.map (fn { primary_constraints,
    2.31 -  secondary_constraints, improve, subst, unchecks, passed } => let
    2.32 -    val (((primary_constraints', secondary_constraints'), ((improve', subst'), unchecks')), passed')
    2.33 -      = f (((primary_constraints, secondary_constraints), ((improve, subst), unchecks)), passed)
    2.34 +  secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed } => let
    2.35 +    val (((primary_constraints', secondary_constraints'),
    2.36 +      (((improve', subst'), consider_abbrevs'), unchecks')), passed')
    2.37 +        = f (((primary_constraints, secondary_constraints),
    2.38 +            (((improve, subst), consider_abbrevs), unchecks)), passed)
    2.39    in { primary_constraints = primary_constraints', secondary_constraints = secondary_constraints',
    2.40 -    improve = improve', subst = subst', unchecks = unchecks', passed = passed'
    2.41 +    improve = improve', subst = subst', consider_abbrevs = consider_abbrevs',
    2.42 +    unchecks = unchecks', passed = passed'
    2.43    } end);
    2.44  
    2.45  val mark_passed = (map_improvable_syntax o apsnd) (K true);
    2.46  
    2.47  fun improve_term_check ts ctxt =
    2.48    let
    2.49 -    val { primary_constraints, secondary_constraints, improve, subst, passed, ... } =
    2.50 -      ImprovableSyntax.get ctxt;
    2.51 +    val { primary_constraints, secondary_constraints, improve, subst,
    2.52 +      consider_abbrevs, passed, ... } = ImprovableSyntax.get ctxt;
    2.53      val tsig = (Sign.tsig_of o ProofContext.theory_of) ctxt;
    2.54 +    val is_abbrev = consider_abbrevs andalso ProofContext.is_abbrev_mode ctxt;
    2.55 +    val passed_or_abbrev = passed orelse is_abbrev;
    2.56      fun accumulate_improvements (Const (c, ty)) = (case improve (c, ty)
    2.57           of SOME ty_ty' => Type.typ_match tsig ty_ty'
    2.58            | _ => I)
    2.59 @@ -77,9 +84,9 @@
    2.60                then SOME (ty', apply_subst t') else NONE
    2.61            | NONE => NONE)
    2.62          | _ => NONE) t;
    2.63 -    val ts'' = map apply_subst ts';
    2.64 -  in if eq_list (op aconv) (ts, ts'') andalso passed then NONE else
    2.65 -    if passed then SOME (ts'', ctxt)
    2.66 +    val ts'' = if is_abbrev then ts' else map apply_subst ts';
    2.67 +  in if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE else
    2.68 +    if passed_or_abbrev then SOME (ts'', ctxt)
    2.69      else SOME (ts'', ctxt
    2.70        |> fold (ProofContext.add_const_constraint o apsnd SOME) secondary_constraints
    2.71        |> mark_passed)
    2.72 @@ -147,7 +154,7 @@
    2.73      |> ProofContext.init
    2.74      |> OverloadingData.put overloading
    2.75      |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
    2.76 -    |> map_improvable_syntax (K ((([], []), ((K NONE, subst), unchecks)), false))
    2.77 +    |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
    2.78      |> add_improvable_syntax
    2.79    end;
    2.80