author | wenzelm |
Sat, 16 Apr 2011 15:47:52 +0200 | |
changeset 42360 | da8817d01e7c |
parent 42359 | 6ca5407863ed |
child 42375 | 774df7c59508 |
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 |
38342
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
14 |
|
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
15 |
val overloading: (string * (string * typ) * bool) list -> theory -> local_theory |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
16 |
val overloading_cmd: (string * string * bool) list -> theory -> local_theory |
25519 | 17 |
end; |
18 |
||
19 |
structure Overloading: OVERLOADING = |
|
20 |
struct |
|
21 |
||
26259 | 22 |
(** generic check/uncheck combinators for improvable constants **) |
26238 | 23 |
|
26249 | 24 |
type improvable_syntax = ((((string * typ) list * (string * typ) list) * |
26730 | 25 |
((((string * typ -> (typ * typ) option) * (string * typ -> (typ * term) option)) * bool) * |
26249 | 26 |
(term * term) list)) * bool); |
25519 | 27 |
|
33519 | 28 |
structure ImprovableSyntax = Proof_Data |
29 |
( |
|
26249 | 30 |
type T = { |
26520 | 31 |
primary_constraints: (string * typ) list, |
32 |
secondary_constraints: (string * typ) list, |
|
26249 | 33 |
improve: string * typ -> (typ * typ) option, |
34 |
subst: string * typ -> (typ * term) option, |
|
26730 | 35 |
consider_abbrevs: bool, |
26249 | 36 |
unchecks: (term * term) list, |
37 |
passed: bool |
|
38 |
}; |
|
26238 | 39 |
fun init _ = { |
26520 | 40 |
primary_constraints = [], |
41 |
secondary_constraints = [], |
|
26238 | 42 |
improve = K NONE, |
43 |
subst = K NONE, |
|
26730 | 44 |
consider_abbrevs = false, |
26238 | 45 |
unchecks = [], |
46 |
passed = true |
|
47 |
}; |
|
48 |
); |
|
25536 | 49 |
|
26520 | 50 |
fun map_improvable_syntax f = ImprovableSyntax.map (fn { primary_constraints, |
40782 | 51 |
secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed } => |
52 |
let |
|
26730 | 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) |
|
26520 | 57 |
in { primary_constraints = primary_constraints', secondary_constraints = secondary_constraints', |
26730 | 58 |
improve = improve', subst = subst', consider_abbrevs = consider_abbrevs', |
40782 | 59 |
unchecks = unchecks', passed = passed' } |
60 |
end); |
|
26238 | 61 |
|
26249 | 62 |
val mark_passed = (map_improvable_syntax o apsnd) (K true); |
26238 | 63 |
|
64 |
fun improve_term_check ts ctxt = |
|
25519 | 65 |
let |
36354 | 66 |
val { secondary_constraints, improve, subst, consider_abbrevs, passed, ... } = |
67 |
ImprovableSyntax.get ctxt; |
|
42360 | 68 |
val tsig = (Sign.tsig_of o Proof_Context.theory_of) ctxt; |
69 |
val is_abbrev = consider_abbrevs andalso Proof_Context.abbrev_mode ctxt; |
|
26730 | 70 |
val passed_or_abbrev = passed orelse is_abbrev; |
26238 | 71 |
fun accumulate_improvements (Const (c, ty)) = (case improve (c, ty) |
26597 | 72 |
of SOME ty_ty' => Type.typ_match tsig ty_ty' |
26238 | 73 |
| _ => I) |
74 |
| accumulate_improvements _ = I; |
|
75 |
val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty; |
|
32035 | 76 |
val ts' = (map o map_types) (Envir.subst_type improvements) ts; |
26238 | 77 |
fun apply_subst t = Envir.expand_term (fn Const (c, ty) => (case subst (c, ty) |
26259 | 78 |
of SOME (ty', t') => |
26238 | 79 |
if Type.typ_instance tsig (ty, ty') |
80 |
then SOME (ty', apply_subst t') else NONE |
|
81 |
| NONE => NONE) |
|
26259 | 82 |
| _ => NONE) t; |
26730 | 83 |
val ts'' = if is_abbrev then ts' else map apply_subst ts'; |
40782 | 84 |
in |
85 |
if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE else |
|
26730 | 86 |
if passed_or_abbrev then SOME (ts'', ctxt) |
26238 | 87 |
else SOME (ts'', ctxt |
42360 | 88 |
|> fold (Proof_Context.add_const_constraint o apsnd SOME) secondary_constraints |
26238 | 89 |
|> mark_passed) |
90 |
end; |
|
25519 | 91 |
|
31698 | 92 |
fun rewrite_liberal thy unchecks t = |
93 |
case try (Pattern.rewrite_term thy unchecks []) t |
|
94 |
of NONE => NONE |
|
95 |
| SOME t' => if t aconv t' then NONE else SOME t'; |
|
96 |
||
26238 | 97 |
fun improve_term_uncheck ts ctxt = |
25519 | 98 |
let |
42360 | 99 |
val thy = Proof_Context.theory_of ctxt; |
26238 | 100 |
val unchecks = (#unchecks o ImprovableSyntax.get) ctxt; |
31698 | 101 |
val ts' = map (rewrite_liberal thy unchecks) ts; |
102 |
in if exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end; |
|
26238 | 103 |
|
26520 | 104 |
fun set_primary_constraints ctxt = |
26259 | 105 |
let |
26520 | 106 |
val { primary_constraints, ... } = ImprovableSyntax.get ctxt; |
42360 | 107 |
in fold (Proof_Context.add_const_constraint o apsnd SOME) primary_constraints ctxt end; |
26259 | 108 |
|
39378
df86b1b4ce10
more precise name for activation of improveable syntax
haftmann
parents:
38757
diff
changeset
|
109 |
val activate_improvable_syntax = |
26259 | 110 |
Context.proof_map |
26238 | 111 |
(Syntax.add_term_check 0 "improvement" improve_term_check |
112 |
#> Syntax.add_term_uncheck 0 "improvement" improve_term_uncheck) |
|
26520 | 113 |
#> set_primary_constraints; |
26259 | 114 |
|
115 |
||
116 |
(** overloading target **) |
|
117 |
||
38382 | 118 |
structure Data = Proof_Data |
26259 | 119 |
( |
120 |
type T = ((string * typ) * (string * bool)) list; |
|
121 |
fun init _ = []; |
|
122 |
); |
|
123 |
||
38382 | 124 |
val get_overloading = Data.get o Local_Theory.target_of; |
125 |
val map_overloading = Local_Theory.target o Data.map; |
|
26259 | 126 |
|
30519
c05c0199826f
coherent binding policy with primitive target operations
haftmann
parents:
29606
diff
changeset
|
127 |
fun operation lthy b = get_overloading lthy |
c05c0199826f
coherent binding policy with primitive target operations
haftmann
parents:
29606
diff
changeset
|
128 |
|> get_first (fn ((c, _), (v, checked)) => |
38382 | 129 |
if Binding.name_of b = v then SOME (c, (v, checked)) else NONE); |
26259 | 130 |
|
32343 | 131 |
fun synchronize_syntax ctxt = |
132 |
let |
|
38382 | 133 |
val overloading = Data.get ctxt; |
32343 | 134 |
fun subst (c, ty) = case AList.lookup (op =) overloading (c, ty) |
135 |
of SOME (v, _) => SOME (ty, Free (v, ty)) |
|
136 |
| NONE => NONE; |
|
137 |
val unchecks = |
|
138 |
map (fn (c_ty as (_, ty), (v, _)) => (Free (v, ty), Const c_ty)) overloading; |
|
139 |
in |
|
140 |
ctxt |
|
141 |
|> map_improvable_syntax (K ((([], []), (((K NONE, subst), false), unchecks)), false)) |
|
142 |
end |
|
26259 | 143 |
|
38382 | 144 |
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
|
145 |
Local_Theory.background_theory_result |
38382 | 146 |
(Thm.add_def (not checked) true (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs))) |
147 |
##> map_overloading (filter_out (fn (_, (v', _)) => v' = v)) |
|
148 |
##> Local_Theory.target synchronize_syntax |
|
149 |
#-> (fn (_, def) => pair (Const (c, U), def)) |
|
26259 | 150 |
|
38382 | 151 |
fun foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = |
152 |
case operation lthy b |
|
153 |
of SOME (c, (v, checked)) => if mx <> NoSyn |
|
154 |
then error ("Illegal mixfix syntax for overloaded constant " ^ quote c) |
|
155 |
else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs) |
|
156 |
| NONE => lthy |> |
|
157 |
Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params); |
|
25519 | 158 |
|
25606 | 159 |
fun pretty lthy = |
160 |
let |
|
161 |
val overloading = get_overloading lthy; |
|
162 |
fun pr_operation ((c, ty), (v, _)) = |
|
42359 | 163 |
Pretty.block (Pretty.breaks |
42360 | 164 |
[Pretty.str v, Pretty.str "==", Pretty.str (Proof_Context.extern_const lthy c), |
42359 | 165 |
Pretty.str "::", Syntax.pretty_typ lthy ty]); |
38382 | 166 |
in Pretty.str "overloading" :: map pr_operation overloading end; |
38342
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
167 |
|
38382 | 168 |
fun conclude lthy = |
169 |
let |
|
170 |
val overloading = get_overloading lthy; |
|
40782 | 171 |
val _ = |
172 |
if null overloading then () |
|
173 |
else |
|
174 |
error ("Missing definition(s) for parameter(s) " ^ commas (map (quote |
|
175 |
o Syntax.string_of_term lthy o Const o fst) overloading)); |
|
38382 | 176 |
in lthy end; |
38342
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
177 |
|
38382 | 178 |
fun gen_overloading prep_const raw_overloading thy = |
38342
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
179 |
let |
42360 | 180 |
val ctxt = Proof_Context.init_global thy; |
38382 | 181 |
val _ = if null raw_overloading then error "At least one parameter must be given" else (); |
182 |
val overloading = raw_overloading |> map (fn (v, const, checked) => |
|
183 |
(Term.dest_Const (prep_const ctxt const), (v, checked))); |
|
38342
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
184 |
in |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
185 |
thy |
38382 | 186 |
|> Theory.checkpoint |
42360 | 187 |
|> Proof_Context.init_global |
38382 | 188 |
|> Data.put overloading |
189 |
|> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading |
|
39378
df86b1b4ce10
more precise name for activation of improveable syntax
haftmann
parents:
38757
diff
changeset
|
190 |
|> activate_improvable_syntax |
38382 | 191 |
|> synchronize_syntax |
38342
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
192 |
|> Local_Theory.init NONE "" |
38382 | 193 |
{define = Generic_Target.define foundation, |
38342
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
194 |
notes = Generic_Target.notes |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
195 |
(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
|
196 |
abbrev = Generic_Target.abbrev |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
197 |
(fn prmode => fn (b, mx) => fn (t, _) => fn _ => |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
198 |
Generic_Target.theory_abbrev prmode ((b, mx), t)), |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
199 |
declaration = K Generic_Target.theory_declaration, |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
200 |
syntax_declaration = K Generic_Target.theory_declaration, |
38382 | 201 |
pretty = pretty, |
38342
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
202 |
exit = Local_Theory.target_of o conclude} |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
203 |
end; |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
204 |
|
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
205 |
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
|
206 |
val overloading_cmd = gen_overloading Syntax.read_term; |
09d4a04d5c2e
moved overloading target formally to overloading.ML
haftmann
parents:
36610
diff
changeset
|
207 |
|
25519 | 208 |
end; |