7 signature OVERLOADING = |
7 signature OVERLOADING = |
8 sig |
8 sig |
9 val init: (string * (string * typ) * bool) list -> theory -> local_theory |
9 val init: (string * (string * typ) * bool) list -> theory -> local_theory |
10 val conclude: local_theory -> local_theory |
10 val conclude: local_theory -> local_theory |
11 val declare: string * typ -> theory -> term * theory |
11 val declare: string * typ -> theory -> term * theory |
12 val confirm: string -> local_theory -> local_theory |
12 val confirm: binding -> local_theory -> local_theory |
13 val define: bool -> string -> string * term -> theory -> thm * theory |
13 val define: bool -> binding -> string * term -> theory -> thm * theory |
14 val operation: Proof.context -> string -> (string * bool) option |
14 val operation: Proof.context -> binding -> (string * bool) option |
15 val pretty: Proof.context -> Pretty.T |
15 val pretty: Proof.context -> Pretty.T |
16 |
16 |
17 type improvable_syntax |
17 type improvable_syntax |
18 val add_improvable_syntax: Proof.context -> Proof.context |
18 val add_improvable_syntax: Proof.context -> Proof.context |
19 val map_improvable_syntax: (improvable_syntax -> improvable_syntax) |
19 val map_improvable_syntax: (improvable_syntax -> improvable_syntax) |
121 ); |
121 ); |
122 |
122 |
123 val get_overloading = OverloadingData.get o LocalTheory.target_of; |
123 val get_overloading = OverloadingData.get o LocalTheory.target_of; |
124 val map_overloading = LocalTheory.target o OverloadingData.map; |
124 val map_overloading = LocalTheory.target o OverloadingData.map; |
125 |
125 |
126 fun operation lthy v = get_overloading lthy |
126 fun operation lthy b = get_overloading lthy |
127 |> get_first (fn ((c, _), (v', checked)) => if v = v' then SOME (c, checked) else NONE); |
127 |> get_first (fn ((c, _), (v, checked)) => |
|
128 if Binding.name_of b = v then SOME (c, checked) else NONE); |
128 |
129 |
129 fun confirm c = map_overloading (filter_out (fn (_, (c', _)) => c' = c)); |
130 fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b)); |
130 |
131 |
131 |
132 |
132 (* overloaded declarations and definitions *) |
133 (* overloaded declarations and definitions *) |
133 |
134 |
134 fun declare c_ty = pair (Const c_ty); |
135 fun declare c_ty = pair (Const c_ty); |
135 |
136 |
136 fun define checked name (c, t) = Thm.add_def (not checked) true (Binding.name name, |
137 fun define checked b (c, t) = Thm.add_def (not checked) true |
137 Logic.mk_equals (Const (c, Term.fastype_of t), t)); |
138 (b, Logic.mk_equals (Const (c, Term.fastype_of t), t)); |
138 |
139 |
139 |
140 |
140 (* target *) |
141 (* target *) |
141 |
142 |
142 fun init raw_overloading thy = |
143 fun init raw_overloading thy = |