author | haftmann |
Wed, 11 Aug 2010 12:30:48 +0200 | |
changeset 38342 | 09d4a04d5c2e |
parent 36610 | bafd82950e24 |
child 38377 | 2dfd8b7b8274 |
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 |
|
35126 | 9 |
val init: (string * (string * typ) * bool) list -> theory -> Proof.context |
25519 | 10 |
val conclude: local_theory -> local_theory |
11 |
val declare: string * typ -> theory -> term * theory |
|
30519
c05c0199826f
coherent binding policy with primitive target operations
haftmann
parents:
29606
diff
changeset
|
12 |
val confirm: binding -> local_theory -> local_theory |
c05c0199826f
coherent binding policy with primitive target operations
haftmann
parents:
29606
diff
changeset
|
13 |
val define: bool -> binding -> string * term -> theory -> thm * theory |
c05c0199826f
coherent binding policy with primitive target operations
haftmann
parents:
29606
diff
changeset
|
14 |
val operation: Proof.context -> binding -> (string * bool) option |
25606 | 15 |
val pretty: Proof.context -> Pretty.T |
35859 | 16 |
|
26238 | 17 |
type improvable_syntax |
18 |
val add_improvable_syntax: Proof.context -> Proof.context |
|
19 |
val map_improvable_syntax: (improvable_syntax -> improvable_syntax) |
|
20 |
-> Proof.context -> Proof.context |
|
26520 | 21 |
val set_primary_constraints: Proof.context -> Proof.context |
38342
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
22 |
|
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
23 |
val overloading: (string * (string * typ) * bool) list -> theory -> local_theory |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
24 |
val overloading_cmd: (string * string * bool) list -> theory -> local_theory |
25519 | 25 |
end; |
26 |
||
27 |
structure Overloading: OVERLOADING = |
|
28 |
struct |
|
29 |
||
26259 | 30 |
(** generic check/uncheck combinators for improvable constants **) |
26238 | 31 |
|
26249 | 32 |
type improvable_syntax = ((((string * typ) list * (string * typ) list) * |
26730 | 33 |
((((string * typ -> (typ * typ) option) * (string * typ -> (typ * term) option)) * bool) * |
26249 | 34 |
(term * term) list)) * bool); |
25519 | 35 |
|
33519 | 36 |
structure ImprovableSyntax = Proof_Data |
37 |
( |
|
26249 | 38 |
type T = { |
26520 | 39 |
primary_constraints: (string * typ) list, |
40 |
secondary_constraints: (string * typ) list, |
|
26249 | 41 |
improve: string * typ -> (typ * typ) option, |
42 |
subst: string * typ -> (typ * term) option, |
|
26730 | 43 |
consider_abbrevs: bool, |
26249 | 44 |
unchecks: (term * term) list, |
45 |
passed: bool |
|
46 |
}; |
|
26238 | 47 |
fun init _ = { |
26520 | 48 |
primary_constraints = [], |
49 |
secondary_constraints = [], |
|
26238 | 50 |
improve = K NONE, |
51 |
subst = K NONE, |
|
26730 | 52 |
consider_abbrevs = false, |
26238 | 53 |
unchecks = [], |
54 |
passed = true |
|
55 |
}; |
|
56 |
); |
|
25536 | 57 |
|
26520 | 58 |
fun map_improvable_syntax f = ImprovableSyntax.map (fn { primary_constraints, |
26730 | 59 |
secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed } => let |
60 |
val (((primary_constraints', secondary_constraints'), |
|
61 |
(((improve', subst'), consider_abbrevs'), unchecks')), passed') |
|
62 |
= f (((primary_constraints, secondary_constraints), |
|
63 |
(((improve, subst), consider_abbrevs), unchecks)), passed) |
|
26520 | 64 |
in { primary_constraints = primary_constraints', secondary_constraints = secondary_constraints', |
26730 | 65 |
improve = improve', subst = subst', consider_abbrevs = consider_abbrevs', |
66 |
unchecks = unchecks', passed = passed' |
|
26249 | 67 |
} end); |
26238 | 68 |
|
26249 | 69 |
val mark_passed = (map_improvable_syntax o apsnd) (K true); |
26238 | 70 |
|
71 |
fun improve_term_check ts ctxt = |
|
25519 | 72 |
let |
36354 | 73 |
val { secondary_constraints, improve, subst, consider_abbrevs, passed, ... } = |
74 |
ImprovableSyntax.get ctxt; |
|
26238 | 75 |
val tsig = (Sign.tsig_of o ProofContext.theory_of) ctxt; |
27285 | 76 |
val is_abbrev = consider_abbrevs andalso ProofContext.abbrev_mode ctxt; |
26730 | 77 |
val passed_or_abbrev = passed orelse is_abbrev; |
26238 | 78 |
fun accumulate_improvements (Const (c, ty)) = (case improve (c, ty) |
26597 | 79 |
of SOME ty_ty' => Type.typ_match tsig ty_ty' |
26238 | 80 |
| _ => I) |
81 |
| accumulate_improvements _ = I; |
|
82 |
val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty; |
|
32035 | 83 |
val ts' = (map o map_types) (Envir.subst_type improvements) ts; |
26238 | 84 |
fun apply_subst t = Envir.expand_term (fn Const (c, ty) => (case subst (c, ty) |
26259 | 85 |
of SOME (ty', t') => |
26238 | 86 |
if Type.typ_instance tsig (ty, ty') |
87 |
then SOME (ty', apply_subst t') else NONE |
|
88 |
| NONE => NONE) |
|
26259 | 89 |
| _ => NONE) t; |
26730 | 90 |
val ts'' = if is_abbrev then ts' else map apply_subst ts'; |
91 |
in if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE else |
|
92 |
if passed_or_abbrev then SOME (ts'', ctxt) |
|
26238 | 93 |
else SOME (ts'', ctxt |
26520 | 94 |
|> fold (ProofContext.add_const_constraint o apsnd SOME) secondary_constraints |
26238 | 95 |
|> mark_passed) |
96 |
end; |
|
25519 | 97 |
|
31698 | 98 |
fun rewrite_liberal thy unchecks t = |
99 |
case try (Pattern.rewrite_term thy unchecks []) t |
|
100 |
of NONE => NONE |
|
101 |
| SOME t' => if t aconv t' then NONE else SOME t'; |
|
102 |
||
26238 | 103 |
fun improve_term_uncheck ts ctxt = |
25519 | 104 |
let |
26238 | 105 |
val thy = ProofContext.theory_of ctxt; |
106 |
val unchecks = (#unchecks o ImprovableSyntax.get) ctxt; |
|
31698 | 107 |
val ts' = map (rewrite_liberal thy unchecks) ts; |
108 |
in if exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end; |
|
26238 | 109 |
|
26520 | 110 |
fun set_primary_constraints ctxt = |
26259 | 111 |
let |
26520 | 112 |
val { primary_constraints, ... } = ImprovableSyntax.get ctxt; |
113 |
in fold (ProofContext.add_const_constraint o apsnd SOME) primary_constraints ctxt end; |
|
26259 | 114 |
|
115 |
val add_improvable_syntax = |
|
116 |
Context.proof_map |
|
26238 | 117 |
(Syntax.add_term_check 0 "improvement" improve_term_check |
118 |
#> Syntax.add_term_uncheck 0 "improvement" improve_term_uncheck) |
|
26520 | 119 |
#> set_primary_constraints; |
26259 | 120 |
|
121 |
||
122 |
(** overloading target **) |
|
123 |
||
124 |
(* bookkeeping *) |
|
125 |
||
33519 | 126 |
structure OverloadingData = Proof_Data |
26259 | 127 |
( |
128 |
type T = ((string * typ) * (string * bool)) list; |
|
129 |
fun init _ = []; |
|
130 |
); |
|
131 |
||
33671 | 132 |
val get_overloading = OverloadingData.get o Local_Theory.target_of; |
133 |
val map_overloading = Local_Theory.target o OverloadingData.map; |
|
26259 | 134 |
|
30519
c05c0199826f
coherent binding policy with primitive target operations
haftmann
parents:
29606
diff
changeset
|
135 |
fun operation lthy b = get_overloading lthy |
c05c0199826f
coherent binding policy with primitive target operations
haftmann
parents:
29606
diff
changeset
|
136 |
|> get_first (fn ((c, _), (v, checked)) => |
c05c0199826f
coherent binding policy with primitive target operations
haftmann
parents:
29606
diff
changeset
|
137 |
if Binding.name_of b = v then SOME (c, checked) else NONE); |
26259 | 138 |
|
32343 | 139 |
|
140 |
(* target *) |
|
26259 | 141 |
|
32343 | 142 |
fun synchronize_syntax ctxt = |
143 |
let |
|
144 |
val overloading = OverloadingData.get ctxt; |
|
145 |
fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty) |
|
146 |
of SOME (v, _) => SOME (ty, Free (v, ty)) |
|
147 |
| NONE => NONE; |
|
148 |
val unchecks = |
|
149 |
map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading; |
|
150 |
in |
|
151 |
ctxt |
|
152 |
|> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false)) |
|
153 |
end |
|
26259 | 154 |
|
32343 | 155 |
fun init raw_overloading thy = |
156 |
let |
|
157 |
val _ = if null raw_overloading then error "At least one parameter must be given" else (); |
|
158 |
val overloading = map (fn (v, c_ty, checked) => (c_ty, (v, checked))) raw_overloading; |
|
159 |
in |
|
160 |
thy |
|
32379
a97e9caebd60
additional checkpoints avoid problems in error situations
haftmann
parents:
32343
diff
changeset
|
161 |
|> Theory.checkpoint |
36610
bafd82950e24
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents:
36354
diff
changeset
|
162 |
|> ProofContext.init_global |
32343 | 163 |
|> OverloadingData.put overloading |
164 |
|> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading |
|
165 |
|> add_improvable_syntax |
|
166 |
|> synchronize_syntax |
|
167 |
end; |
|
26259 | 168 |
|
169 |
fun declare c_ty = pair (Const c_ty); |
|
170 |
||
36106
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35859
diff
changeset
|
171 |
fun define checked b (c, t) = |
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35859
diff
changeset
|
172 |
Thm.add_def (not checked) true (b, Logic.mk_equals (Const (c, Term.fastype_of t), t)) |
19deea200358
Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents:
35859
diff
changeset
|
173 |
#>> snd; |
25519 | 174 |
|
32343 | 175 |
fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b)) |
33671 | 176 |
#> Local_Theory.target synchronize_syntax |
25519 | 177 |
|
178 |
fun conclude lthy = |
|
179 |
let |
|
180 |
val overloading = get_overloading lthy; |
|
181 |
val _ = if null overloading then () else |
|
26259 | 182 |
error ("Missing definition(s) for parameter(s) " ^ commas (map (quote |
25519 | 183 |
o Syntax.string_of_term lthy o Const o fst) overloading)); |
184 |
in |
|
185 |
lthy |
|
186 |
end; |
|
187 |
||
25606 | 188 |
fun pretty lthy = |
189 |
let |
|
190 |
val thy = ProofContext.theory_of lthy; |
|
191 |
val overloading = get_overloading lthy; |
|
192 |
fun pr_operation ((c, ty), (v, _)) = |
|
25861 | 193 |
(Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==", |
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26730
diff
changeset
|
194 |
Pretty.str (Sign.extern_const thy c), Pretty.str "::", Syntax.pretty_typ lthy ty]; |
25606 | 195 |
in |
196 |
(Pretty.block o Pretty.fbreaks) |
|
197 |
(Pretty.str "overloading" :: map pr_operation overloading) |
|
198 |
end; |
|
199 |
||
38342
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
200 |
fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c); |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
201 |
|
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
202 |
fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
203 |
case operation lthy b |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
204 |
of SOME (c, checked) => if mx <> NoSyn then syntax_error c |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
205 |
else lthy |> Local_Theory.theory_result (declare (c, U) |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
206 |
##>> define checked b_def (c, rhs)) |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
207 |
||> confirm b |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
208 |
| NONE => lthy |> |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
209 |
Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params); |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
210 |
|
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
211 |
fun gen_overloading prep_const raw_ops thy = |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
212 |
let |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
213 |
val ctxt = ProofContext.init_global thy; |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
214 |
val ops = raw_ops |> map (fn (name, const, checked) => |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
215 |
(name, Term.dest_Const (prep_const ctxt const), checked)); |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
216 |
in |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
217 |
thy |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
218 |
|> init ops |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
219 |
|> Local_Theory.init NONE "" |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
220 |
{define = Generic_Target.define overloading_foundation, |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
221 |
notes = Generic_Target.notes |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
222 |
(fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts), |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
223 |
abbrev = Generic_Target.abbrev |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
224 |
(fn prmode => fn (b, mx) => fn (t, _) => fn _ => |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
225 |
Generic_Target.theory_abbrev prmode ((b, mx), t)), |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
226 |
declaration = K Generic_Target.theory_declaration, |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
227 |
syntax_declaration = K Generic_Target.theory_declaration, |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
228 |
pretty = single o pretty, |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
229 |
reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of, |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
230 |
exit = Local_Theory.target_of o conclude} |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
231 |
end; |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
232 |
|
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
233 |
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
|
234 |
val overloading_cmd = gen_overloading Syntax.read_term; |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
235 |
|
25519 | 236 |
end; |