4 Ad-hoc overloading of constants based on their types. |
4 Ad-hoc overloading of constants based on their types. |
5 *) |
5 *) |
6 |
6 |
7 signature ADHOC_OVERLOADING = |
7 signature ADHOC_OVERLOADING = |
8 sig |
8 sig |
9 |
|
10 val add_overloaded: string -> theory -> theory |
9 val add_overloaded: string -> theory -> theory |
11 val add_variant: string -> string -> theory -> theory |
10 val add_variant: string -> string -> theory -> theory |
12 |
11 |
13 val show_variants: bool Unsynchronized.ref |
12 val show_variants: bool Config.T |
14 val setup: theory -> theory |
13 val setup: theory -> theory |
15 |
|
16 end |
14 end |
17 |
|
18 |
15 |
19 structure Adhoc_Overloading: ADHOC_OVERLOADING = |
16 structure Adhoc_Overloading: ADHOC_OVERLOADING = |
20 struct |
17 struct |
21 |
18 |
22 val show_variants = Unsynchronized.ref false; |
19 val show_variants = Attrib.setup_config_bool @{binding show_variants} (K false); |
23 |
20 |
24 |
21 |
25 (* errors *) |
22 (* errors *) |
26 |
23 |
27 fun duplicate_variant_err int_name ext_name = |
24 fun duplicate_variant_err int_name ext_name = |
73 in map_tables (Symtab.update (ext_name, [])) I thy end; |
70 in map_tables (Symtab.update (ext_name, [])) I thy end; |
74 |
71 |
75 fun add_variant ext_name name thy = |
72 fun add_variant ext_name name thy = |
76 let |
73 let |
77 val _ = is_overloaded thy ext_name orelse not_overloaded_err ext_name; |
74 val _ = is_overloaded thy ext_name orelse not_overloaded_err ext_name; |
78 val _ = case get_external thy name of |
75 val _ = |
79 NONE => () |
76 (case get_external thy name of |
80 | SOME gen' => duplicate_variant_err name gen'; |
77 NONE => () |
|
78 | SOME gen' => duplicate_variant_err name gen'); |
81 val T = Sign.the_const_type thy name; |
79 val T = Sign.the_const_type thy name; |
82 in |
80 in |
83 map_tables (Symtab.cons_list (ext_name, (name, T))) |
81 map_tables (Symtab.cons_list (ext_name, (name, T))) |
84 (Symtab.update (name, ext_name)) thy |
82 (Symtab.update (name, ext_name)) thy |
85 end |
83 end |
86 |
84 |
87 |
85 |
88 (* check / uncheck *) |
86 (* check / uncheck *) |
89 |
87 |
97 (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME c) |
95 (Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME c) |
98 handle Type.TUNIFY => NONE |
96 handle Type.TUNIFY => NONE |
99 end; |
97 end; |
100 |
98 |
101 fun insert_internal_same ctxt t (Const (c, T)) = |
99 fun insert_internal_same ctxt t (Const (c, T)) = |
102 (case map_filter (unifiable_with ctxt T) |
100 (case map_filter (unifiable_with ctxt T) |
103 (Same.function (get_variants (Proof_Context.theory_of ctxt)) c) of |
101 (Same.function (get_variants (Proof_Context.theory_of ctxt)) c) of |
104 [] => unresolved_err ctxt (c, T) t "no instances" |
102 [] => unresolved_err ctxt (c, T) t "no instances" |
105 | [c'] => Const (c', dummyT) |
103 | [c'] => Const (c', dummyT) |
106 | _ => raise Same.SAME) |
104 | _ => raise Same.SAME) |
107 | insert_internal_same _ _ _ = raise Same.SAME; |
105 | insert_internal_same _ _ _ = raise Same.SAME; |
108 |
106 |
109 fun insert_external_same ctxt _ (Const (c, T)) = |
107 fun insert_external_same ctxt _ (Const (c, T)) = |
110 Const (Same.function (get_external (Proof_Context.theory_of ctxt)) c, T) |
108 Const (Same.function (get_external (Proof_Context.theory_of ctxt)) c, T) |
111 | insert_external_same _ _ _ = raise Same.SAME; |
109 | insert_external_same _ _ _ = raise Same.SAME; |
112 |
110 |
113 fun gen_check_uncheck replace ts ctxt = |
111 fun gen_check_uncheck replace ts ctxt = |
114 Same.capture (Same.map (fn t => Term_Subst.map_aterms_same (replace ctxt t) t)) ts |
112 Same.capture (Same.map (fn t => Term_Subst.map_aterms_same (replace ctxt t) t)) ts |
115 |> Option.map (rpair ctxt); |
113 |> Option.map (rpair ctxt); |
116 |
114 |
117 val check = gen_check_uncheck insert_internal_same; |
115 val check = gen_check_uncheck insert_internal_same; |
118 fun uncheck ts ctxt = |
116 |
119 if !show_variants then NONE |
117 fun uncheck ts ctxt = |
|
118 if Config.get ctxt show_variants then NONE |
120 else gen_check_uncheck insert_external_same ts ctxt; |
119 else gen_check_uncheck insert_external_same ts ctxt; |
121 |
120 |
122 fun reject_unresolved ts ctxt = |
121 fun reject_unresolved ts ctxt = |
123 let |
122 let |
124 val thy = Proof_Context.theory_of ctxt; |
123 val thy = Proof_Context.theory_of ctxt; |
125 fun check_unresolved t = |
124 fun check_unresolved t = |
126 case filter (is_overloaded thy o fst) (Term.add_consts t []) of |
125 (case filter (is_overloaded thy o fst) (Term.add_consts t []) of |
127 [] => () |
126 [] => () |
128 | ((c, T) :: _) => unresolved_err ctxt (c, T) t "multiple instances"; |
127 | ((c, T) :: _) => unresolved_err ctxt (c, T) t "multiple instances"); |
129 |
|
130 val _ = map check_unresolved ts; |
128 val _ = map check_unresolved ts; |
131 in NONE end; |
129 in NONE end; |
132 |
130 |
133 |
131 |
134 (* setup *) |
132 (* setup *) |
135 |
133 |
136 val setup = Context.theory_map |
134 val setup = Context.theory_map |
137 (Syntax.context_term_check 0 "adhoc_overloading" check |
135 (Syntax.context_term_check 0 "adhoc_overloading" check |
138 #> Syntax.context_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved |
136 #> Syntax.context_term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved |
139 #> Syntax.context_term_uncheck 0 "adhoc_overloading" uncheck); |
137 #> Syntax.context_term_uncheck 0 "adhoc_overloading" uncheck); |
140 |
138 |
141 end |
139 end; |