author | haftmann |
Sat, 24 Oct 2020 15:16:54 +0000 | |
changeset 72505 | 974071d873ba |
parent 69829 | 3bfa28b3a5b2 |
child 72516 | 17dc99589a91 |
permissions | -rw-r--r-- |
25519 | 1 |
(* Title: Pure/Isar/overloading.ML |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
||
4 |
Overloaded definitions without any discipline. |
|
5 |
*) |
|
6 |
||
7 |
signature OVERLOADING = |
|
8 |
sig |
|
26238 | 9 |
type improvable_syntax |
39378
df86b1b4ce10
more precise name for activation of improveable syntax
haftmann
parents:
38757
diff
changeset
|
10 |
val activate_improvable_syntax: Proof.context -> Proof.context |
26238 | 11 |
val map_improvable_syntax: (improvable_syntax -> improvable_syntax) |
12 |
-> Proof.context -> Proof.context |
|
26520 | 13 |
val set_primary_constraints: Proof.context -> Proof.context |
60339
0e6742f89c03
dedicated config options to deactivate uncheck phase for improvable syntax
haftmann
parents:
60338
diff
changeset
|
14 |
val show_reverted_improvements: bool Config.T; |
38342
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
15 |
|
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
16 |
val overloading: (string * (string * typ) * bool) list -> theory -> local_theory |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
17 |
val overloading_cmd: (string * string * bool) list -> theory -> local_theory |
69829 | 18 |
val theory_map: (string * (string * typ) * bool) list |
19 |
-> (local_theory -> local_theory) -> theory -> theory |
|
20 |
val theory_map_result: (string * (string * typ) * bool) list |
|
21 |
-> (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) |
|
22 |
-> theory -> 'b * theory |
|
25519 | 23 |
end; |
24 |
||
25 |
structure Overloading: OVERLOADING = |
|
26 |
struct |
|
27 |
||
42404 | 28 |
(* generic check/uncheck combinators for improvable constants *) |
26238 | 29 |
|
60338 | 30 |
type improvable_syntax = { |
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 |
no_subst_in_abbrev_mode: bool, |
|
36 |
unchecks: (term * term) list |
|
37 |
} |
|
25519 | 38 |
|
42404 | 39 |
structure Improvable_Syntax = Proof_Data |
33519 | 40 |
( |
60338 | 41 |
type T = {syntax: improvable_syntax, secondary_pass: bool} |
42 |
fun init _ = {syntax = { |
|
43 |
primary_constraints = [], |
|
44 |
secondary_constraints = [], |
|
45 |
improve = K NONE, |
|
46 |
subst = K NONE, |
|
47 |
no_subst_in_abbrev_mode = false, |
|
48 |
unchecks = [] |
|
49 |
}, secondary_pass = false}: T; |
|
26238 | 50 |
); |
25536 | 51 |
|
60338 | 52 |
fun map_improvable_syntax f = |
53 |
Improvable_Syntax.map (fn {syntax, secondary_pass} => {syntax = f syntax, secondary_pass = secondary_pass}); |
|
26238 | 54 |
|
60338 | 55 |
val mark_passed = |
56 |
Improvable_Syntax.map (fn {syntax, secondary_pass} => {syntax = syntax, secondary_pass = true}); |
|
26238 | 57 |
|
58 |
fun improve_term_check ts ctxt = |
|
25519 | 59 |
let |
42388 | 60 |
val thy = Proof_Context.theory_of ctxt; |
61 |
||
60338 | 62 |
val {syntax = {secondary_constraints, improve, subst, no_subst_in_abbrev_mode, ...}, secondary_pass} = |
42404 | 63 |
Improvable_Syntax.get ctxt; |
60338 | 64 |
val no_subst = Proof_Context.abbrev_mode ctxt andalso no_subst_in_abbrev_mode; |
42388 | 65 |
fun accumulate_improvements (Const (c, ty)) = |
66 |
(case improve (c, ty) of |
|
67 |
SOME ty_ty' => Sign.typ_match thy ty_ty' |
|
26238 | 68 |
| _ => I) |
69 |
| accumulate_improvements _ = I; |
|
42388 | 70 |
fun apply_subst t = |
71 |
Envir.expand_term |
|
72 |
(fn Const (c, ty) => |
|
73 |
(case subst (c, ty) of |
|
74 |
SOME (ty', t') => |
|
75 |
if Sign.typ_instance thy (ty, ty') |
|
26238 | 76 |
then SOME (ty', apply_subst t') else NONE |
77 |
| NONE => NONE) |
|
26259 | 78 |
| _ => NONE) t; |
60338 | 79 |
val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty; |
80 |
val ts' = |
|
81 |
ts |
|
82 |
|> (map o map_types) (Envir.subst_type improvements) |
|
83 |
|> not no_subst ? map apply_subst; |
|
40782 | 84 |
in |
60338 | 85 |
if secondary_pass orelse no_subst then |
86 |
if eq_list (op aconv) (ts, ts') then NONE |
|
87 |
else SOME (ts', ctxt) |
|
42404 | 88 |
else |
60338 | 89 |
SOME (ts', ctxt |
42404 | 90 |
|> fold (Proof_Context.add_const_constraint o apsnd SOME) secondary_constraints |
91 |
|> mark_passed) |
|
26238 | 92 |
end; |
25519 | 93 |
|
31698 | 94 |
fun rewrite_liberal thy unchecks t = |
60347 | 95 |
(case try (Pattern.rewrite_term_top thy unchecks []) t of |
42404 | 96 |
NONE => NONE |
97 |
| SOME t' => if t aconv t' then NONE else SOME t'); |
|
31698 | 98 |
|
60339
0e6742f89c03
dedicated config options to deactivate uncheck phase for improvable syntax
haftmann
parents:
60338
diff
changeset
|
99 |
val show_reverted_improvements = |
67147 | 100 |
Attrib.setup_config_bool \<^binding>\<open>show_reverted_improvements\<close> (K true); |
60339
0e6742f89c03
dedicated config options to deactivate uncheck phase for improvable syntax
haftmann
parents:
60338
diff
changeset
|
101 |
|
26238 | 102 |
fun improve_term_uncheck ts ctxt = |
25519 | 103 |
let |
42360 | 104 |
val thy = Proof_Context.theory_of ctxt; |
60338 | 105 |
val {syntax = {unchecks, ...}, ...} = Improvable_Syntax.get ctxt; |
60339
0e6742f89c03
dedicated config options to deactivate uncheck phase for improvable syntax
haftmann
parents:
60338
diff
changeset
|
106 |
val revert = Config.get ctxt show_reverted_improvements; |
31698 | 107 |
val ts' = map (rewrite_liberal thy unchecks) ts; |
60339
0e6742f89c03
dedicated config options to deactivate uncheck phase for improvable syntax
haftmann
parents:
60338
diff
changeset
|
108 |
in if revert andalso exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end; |
26238 | 109 |
|
26520 | 110 |
fun set_primary_constraints ctxt = |
60338 | 111 |
let |
112 |
val {syntax = {primary_constraints, ...}, ...} = Improvable_Syntax.get ctxt; |
|
42360 | 113 |
in fold (Proof_Context.add_const_constraint o apsnd SOME) primary_constraints ctxt end; |
26259 | 114 |
|
39378
df86b1b4ce10
more precise name for activation of improveable syntax
haftmann
parents:
38757
diff
changeset
|
115 |
val activate_improvable_syntax = |
26259 | 116 |
Context.proof_map |
45444 | 117 |
(Syntax_Phases.term_check' 0 "improvement" improve_term_check |
118 |
#> Syntax_Phases.term_uncheck' 0 "improvement" improve_term_uncheck) |
|
26520 | 119 |
#> set_primary_constraints; |
26259 | 120 |
|
121 |
||
42404 | 122 |
(* overloading target *) |
26259 | 123 |
|
38382 | 124 |
structure Data = Proof_Data |
26259 | 125 |
( |
126 |
type T = ((string * typ) * (string * bool)) list; |
|
127 |
fun init _ = []; |
|
128 |
); |
|
129 |
||
38382 | 130 |
val get_overloading = Data.get o Local_Theory.target_of; |
131 |
val map_overloading = Local_Theory.target o Data.map; |
|
26259 | 132 |
|
42404 | 133 |
fun operation lthy b = |
134 |
get_overloading lthy |
|
30519
c05c0199826f
coherent binding policy with primitive target operations
haftmann
parents:
29606
diff
changeset
|
135 |
|> get_first (fn ((c, _), (v, checked)) => |
38382 | 136 |
if Binding.name_of b = v then SOME (c, (v, checked)) else NONE); |
26259 | 137 |
|
32343 | 138 |
fun synchronize_syntax ctxt = |
139 |
let |
|
38382 | 140 |
val overloading = Data.get ctxt; |
42404 | 141 |
fun subst (c, ty) = |
142 |
(case AList.lookup (op =) overloading (c, ty) of |
|
143 |
SOME (v, _) => SOME (ty, Free (v, ty)) |
|
144 |
| NONE => NONE); |
|
32343 | 145 |
val unchecks = |
146 |
map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading; |
|
64596 | 147 |
in |
32343 | 148 |
ctxt |
60338 | 149 |
|> map_improvable_syntax (K {primary_constraints = [], |
150 |
secondary_constraints = [], improve = K NONE, subst = subst, |
|
151 |
no_subst_in_abbrev_mode = false, unchecks = unchecks}) |
|
46916
e7ea35b41e2d
Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
wenzelm
parents:
45444
diff
changeset
|
152 |
end; |
26259 | 153 |
|
38382 | 154 |
fun define_overloaded (c, U) (v, checked) (b_def, rhs) = |
38757
2b3e054ae6fc
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
wenzelm
parents:
38382
diff
changeset
|
155 |
Local_Theory.background_theory_result |
42375
774df7c59508
report Name_Space.declare/define, relatively to context;
wenzelm
parents:
42360
diff
changeset
|
156 |
(Thm.add_def_global (not checked) true |
46916
e7ea35b41e2d
Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
wenzelm
parents:
45444
diff
changeset
|
157 |
(Thm.def_binding_optional (Binding.name v) b_def, |
e7ea35b41e2d
Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
wenzelm
parents:
45444
diff
changeset
|
158 |
Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs))) |
38382 | 159 |
##> map_overloading (filter_out (fn (_, (v', _)) => v' = v)) |
47245
ff1770df59b8
Local_Theory.map_contexts with explicit level indication: 0 = main target at bottom;
wenzelm
parents:
47081
diff
changeset
|
160 |
##> Local_Theory.map_contexts (K synchronize_syntax) |
46916
e7ea35b41e2d
Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
wenzelm
parents:
45444
diff
changeset
|
161 |
#-> (fn (_, def) => pair (Const (c, U), def)); |
26259 | 162 |
|
47289 | 163 |
fun foundation (((b, U), mx), (b_def, rhs)) params lthy = |
42404 | 164 |
(case operation lthy b of |
165 |
SOME (c, (v, checked)) => |
|
62752 | 166 |
if Mixfix.is_empty mx then |
167 |
lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs) |
|
62765
5b95a12b7b19
tuned messages -- position is usually missing here;
wenzelm
parents:
62752
diff
changeset
|
168 |
else error ("Illegal mixfix syntax for overloaded constant " ^ quote c) |
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60339
diff
changeset
|
169 |
| NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params); |
25519 | 170 |
|
25606 | 171 |
fun pretty lthy = |
172 |
let |
|
173 |
val overloading = get_overloading lthy; |
|
174 |
fun pr_operation ((c, ty), (v, _)) = |
|
42359 | 175 |
Pretty.block (Pretty.breaks |
64596 | 176 |
[Pretty.str v, Pretty.str "\<equiv>", Proof_Context.pretty_const lthy c, |
42359 | 177 |
Pretty.str "::", Syntax.pretty_typ lthy ty]); |
60246 | 178 |
in |
179 |
[Pretty.block |
|
180 |
(Pretty.fbreaks (Pretty.keyword1 "overloading" :: map pr_operation overloading))] |
|
181 |
end; |
|
38342
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
182 |
|
38382 | 183 |
fun conclude lthy = |
184 |
let |
|
185 |
val overloading = get_overloading lthy; |
|
40782 | 186 |
val _ = |
187 |
if null overloading then () |
|
188 |
else |
|
42404 | 189 |
error ("Missing definition(s) for parameter(s) " ^ |
190 |
commas_quote (map (Syntax.string_of_term lthy o Const o fst) overloading)); |
|
38382 | 191 |
in lthy end; |
38342
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
192 |
|
69829 | 193 |
fun gen_overloading prep_const raw_overloading_spec thy = |
38342
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
194 |
let |
42360 | 195 |
val ctxt = Proof_Context.init_global thy; |
69829 | 196 |
val _ = if null raw_overloading_spec then error "At least one parameter must be given" else (); |
197 |
val overloading_spec = raw_overloading_spec |> map (fn (v, const, checked) => |
|
38382 | 198 |
(Term.dest_Const (prep_const ctxt const), (v, checked))); |
38342
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
199 |
in |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
200 |
thy |
66337
5caea089dd17
more structural sharing between common target Generic_Target.init
haftmann
parents:
66335
diff
changeset
|
201 |
|> Generic_Target.init |
66335
a849ce33923d
treat exit separate from regular local theory operations
haftmann
parents:
64596
diff
changeset
|
202 |
{background_naming = Sign.naming_of thy, |
66337
5caea089dd17
more structural sharing between common target Generic_Target.init
haftmann
parents:
66335
diff
changeset
|
203 |
setup = Proof_Context.init_global |
69829 | 204 |
#> Data.put overloading_spec |
205 |
#> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading_spec |
|
66337
5caea089dd17
more structural sharing between common target Generic_Target.init
haftmann
parents:
66335
diff
changeset
|
206 |
#> activate_improvable_syntax |
5caea089dd17
more structural sharing between common target Generic_Target.init
haftmann
parents:
66335
diff
changeset
|
207 |
#> synchronize_syntax, |
5caea089dd17
more structural sharing between common target Generic_Target.init
haftmann
parents:
66335
diff
changeset
|
208 |
conclude = conclude} |
38382 | 209 |
{define = Generic_Target.define foundation, |
60341
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60339
diff
changeset
|
210 |
notes = Generic_Target.notes Generic_Target.theory_target_notes, |
fcbd7f0c52c3
clearly separated target primitives (target_foo) from self-contained target operations (foo)
haftmann
parents:
60339
diff
changeset
|
211 |
abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev, |
47279
4bab649dedf0
clarified standard_declaration vs. theory_declaration;
wenzelm
parents:
47250
diff
changeset
|
212 |
declaration = K Generic_Target.theory_declaration, |
72505 | 213 |
theory_registration = Locale.add_registration_theory, |
61890
f6ded81f5690
abandoned attempt to unify sublocale and interpretation into global theories
haftmann
parents:
60347
diff
changeset
|
214 |
locale_dependency = fn _ => error "Not possible in overloading target", |
66335
a849ce33923d
treat exit separate from regular local theory operations
haftmann
parents:
64596
diff
changeset
|
215 |
pretty = pretty} |
38342
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
216 |
end; |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
217 |
|
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
218 |
val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const); |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
219 |
val overloading_cmd = gen_overloading Syntax.read_term; |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
220 |
|
69829 | 221 |
fun theory_map overloading_spec g = |
222 |
overloading overloading_spec #> g #> Local_Theory.exit_global; |
|
223 |
fun theory_map_result overloading_spec f g = |
|
224 |
overloading overloading_spec #> g #> Local_Theory.exit_result_global f; |
|
225 |
||
25519 | 226 |
end; |