refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
1 (* Title: Pure/Isar/overloading.ML
2 Author: Florian Haftmann, TU Muenchen
4 Overloaded definitions without any discipline.
7 signature OVERLOADING =
10 val activate_improvable_syntax: Proof.context -> Proof.context
11 val map_improvable_syntax: (improvable_syntax -> improvable_syntax)
12 -> Proof.context -> Proof.context
13 val set_primary_constraints: Proof.context -> Proof.context
15 val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
16 val overloading_cmd: (string * string * bool) list -> theory -> local_theory
19 structure Overloading: OVERLOADING =
22 (* generic check/uncheck combinators for improvable constants *)
24 type improvable_syntax = ((((string * typ) list * (string * typ) list) *
25 ((((string * typ -> (typ * typ) option) * (string * typ -> (typ * term) option)) * bool) *
26 (term * term) list)) * bool);
28 structure Improvable_Syntax = Proof_Data
31 primary_constraints: (string * typ) list,
32 secondary_constraints: (string * typ) list,
33 improve: string * typ -> (typ * typ) option,
34 subst: string * typ -> (typ * term) option,
35 consider_abbrevs: bool,
36 unchecks: (term * term) list,
40 primary_constraints = [],
41 secondary_constraints = [],
44 consider_abbrevs = false,
50 fun map_improvable_syntax f = Improvable_Syntax.map (fn {primary_constraints,
51 secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed} =>
53 val (((primary_constraints', secondary_constraints'),
54 (((improve', subst'), consider_abbrevs'), unchecks')), passed')
55 = f (((primary_constraints, secondary_constraints),
56 (((improve, subst), consider_abbrevs), unchecks)), passed)
58 {primary_constraints = primary_constraints', secondary_constraints = secondary_constraints',
59 improve = improve', subst = subst', consider_abbrevs = consider_abbrevs',
60 unchecks = unchecks', passed = passed'}
63 val mark_passed = (map_improvable_syntax o apsnd) (K true);
65 fun improve_term_check ts ctxt =
67 val thy = Proof_Context.theory_of ctxt;
69 val {secondary_constraints, improve, subst, consider_abbrevs, passed, ...} =
70 Improvable_Syntax.get ctxt;
71 val is_abbrev = consider_abbrevs andalso Proof_Context.abbrev_mode ctxt;
72 val passed_or_abbrev = passed orelse is_abbrev;
73 fun accumulate_improvements (Const (c, ty)) =
74 (case improve (c, ty) of
75 SOME ty_ty' => Sign.typ_match thy ty_ty'
77 | accumulate_improvements _ = I;
78 val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty;
79 val ts' = (map o map_types) (Envir.subst_type improvements) ts;
83 (case subst (c, ty) of
85 if Sign.typ_instance thy (ty, ty')
86 then SOME (ty', apply_subst t') else NONE
89 val ts'' = if is_abbrev then ts' else map apply_subst ts';
91 if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE
92 else if passed_or_abbrev then SOME (ts'', ctxt)
95 |> fold (Proof_Context.add_const_constraint o apsnd SOME) secondary_constraints
99 fun rewrite_liberal thy unchecks t =
100 (case try (Pattern.rewrite_term thy unchecks []) t of
102 | SOME t' => if t aconv t' then NONE else SOME t');
104 fun improve_term_uncheck ts ctxt =
106 val thy = Proof_Context.theory_of ctxt;
107 val {unchecks, ...} = Improvable_Syntax.get ctxt;
108 val ts' = map (rewrite_liberal thy unchecks) ts;
109 in if exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end;
111 fun set_primary_constraints ctxt =
112 let val {primary_constraints, ...} = Improvable_Syntax.get ctxt;
113 in fold (Proof_Context.add_const_constraint o apsnd SOME) primary_constraints ctxt end;
115 val activate_improvable_syntax =
117 (Syntax.context_term_check 0 "improvement" improve_term_check
118 #> Syntax.context_term_uncheck 0 "improvement" improve_term_uncheck)
119 #> set_primary_constraints;
122 (* overloading target *)
124 structure Data = Proof_Data
126 type T = ((string * typ) * (string * bool)) list;
130 val get_overloading = Data.get o Local_Theory.target_of;
131 val map_overloading = Local_Theory.target o Data.map;
133 fun operation lthy b =
135 |> get_first (fn ((c, _), (v, checked)) =>
136 if Binding.name_of b = v then SOME (c, (v, checked)) else NONE);
138 fun synchronize_syntax ctxt =
140 val overloading = Data.get ctxt;
142 (case AList.lookup (op =) overloading (c, ty) of
143 SOME (v, _) => SOME (ty, Free (v, ty))
146 map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading;
149 |> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false))
152 fun define_overloaded (c, U) (v, checked) (b_def, rhs) =
153 Local_Theory.background_theory_result
154 (Thm.add_def_global (not checked) true
155 (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
156 ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v))
157 ##> Local_Theory.target synchronize_syntax
158 #-> (fn (_, def) => pair (Const (c, U), def))
160 fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
161 (case operation lthy b of
162 SOME (c, (v, checked)) =>
164 then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
165 else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
167 |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params));
171 val overloading = get_overloading lthy;
172 fun pr_operation ((c, ty), (v, _)) =
173 Pretty.block (Pretty.breaks
174 [Pretty.str v, Pretty.str "==", Pretty.str (Proof_Context.extern_const lthy c),
175 Pretty.str "::", Syntax.pretty_typ lthy ty]);
176 in Pretty.str "overloading" :: map pr_operation overloading end;
180 val overloading = get_overloading lthy;
182 if null overloading then ()
184 error ("Missing definition(s) for parameter(s) " ^
185 commas_quote (map (Syntax.string_of_term lthy o Const o fst) overloading));
188 fun gen_overloading prep_const raw_overloading thy =
190 val ctxt = Proof_Context.init_global thy;
191 val _ = if null raw_overloading then error "At least one parameter must be given" else ();
192 val overloading = raw_overloading |> map (fn (v, const, checked) =>
193 (Term.dest_Const (prep_const ctxt const), (v, checked)));
197 |> Proof_Context.init_global
198 |> Data.put overloading
199 |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
200 |> activate_improvable_syntax
201 |> synchronize_syntax
202 |> Local_Theory.init NONE ""
203 {define = Generic_Target.define foundation,
204 notes = Generic_Target.notes
205 (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
206 abbrev = Generic_Target.abbrev
207 (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
208 Generic_Target.theory_abbrev prmode ((b, mx), t)),
209 declaration = Generic_Target.theory_declaration o #syntax,
211 exit = Local_Theory.target_of o conclude}
214 val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
215 val overloading_cmd = gen_overloading Syntax.read_term;