author | Manuel Eberl <eberlm@in.tum.de> |
Fri, 29 Mar 2024 19:28:59 +0100 | |
changeset 80061 | 4c1347e172b1 |
parent 78095 | bc42c074e58f |
child 80127 | 39f9084a9668 |
permissions | -rw-r--r-- |
53538 | 1 |
(* Author: Alexander Krauss, TU Muenchen |
2 |
Author: Christian Sternagel, University of Innsbruck |
|
37789 | 3 |
|
52893 | 4 |
Adhoc overloading of constants based on their types. |
37789 | 5 |
*) |
6 |
||
7 |
signature ADHOC_OVERLOADING = |
|
8 |
sig |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
9 |
val is_overloaded: Proof.context -> string -> bool |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
10 |
val generic_add_overloaded: string -> Context.generic -> Context.generic |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
11 |
val generic_remove_overloaded: string -> Context.generic -> Context.generic |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
12 |
val generic_add_variant: string -> term -> Context.generic -> Context.generic |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
13 |
(*If the list of variants is empty at the end of "generic_remove_variant", then |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
14 |
"generic_remove_overloaded" is called implicitly.*) |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
15 |
val generic_remove_variant: string -> term -> Context.generic -> Context.generic |
45422 | 16 |
val show_variants: bool Config.T |
37789 | 17 |
end |
18 |
||
19 |
structure Adhoc_Overloading: ADHOC_OVERLOADING = |
|
20 |
struct |
|
21 |
||
69593 | 22 |
val show_variants = Attrib.setup_config_bool \<^binding>\<open>show_variants\<close> (K false); |
37789 | 23 |
|
53538 | 24 |
|
37789 | 25 |
(* errors *) |
26 |
||
53008
128bec4e3fca
indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents:
53007
diff
changeset
|
27 |
fun err_duplicate_variant oconst = |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
28 |
error ("Duplicate variant of " ^ quote oconst); |
37789 | 29 |
|
53008
128bec4e3fca
indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents:
53007
diff
changeset
|
30 |
fun err_not_a_variant oconst = |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
31 |
error ("Not a variant of " ^ quote oconst); |
37789 | 32 |
|
53008
128bec4e3fca
indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents:
53007
diff
changeset
|
33 |
fun err_not_overloaded oconst = |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
34 |
error ("Constant " ^ quote oconst ^ " is not declared as overloaded"); |
37789 | 35 |
|
53540
7903fe2c271b
prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents:
53538
diff
changeset
|
36 |
fun err_unresolved_overloading ctxt0 (c, T) t instances = |
7903fe2c271b
prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents:
53538
diff
changeset
|
37 |
let |
7903fe2c271b
prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents:
53538
diff
changeset
|
38 |
val ctxt = Config.put show_variants true ctxt0 |
7903fe2c271b
prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents:
53538
diff
changeset
|
39 |
val const_space = Proof_Context.const_space ctxt |
7903fe2c271b
prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents:
53538
diff
changeset
|
40 |
val prt_const = |
7903fe2c271b
prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents:
53538
diff
changeset
|
41 |
Pretty.block [Name_Space.pretty ctxt const_space c, Pretty.str " ::", Pretty.brk 1, |
7903fe2c271b
prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents:
53538
diff
changeset
|
42 |
Pretty.quote (Syntax.pretty_typ ctxt T)] |
52688
1e13b2515e2b
show variants in error messages; more precise error messages (give witnesses for multiple instances)
Christian Sternagel
parents:
52687
diff
changeset
|
43 |
in |
53537 | 44 |
error (Pretty.string_of (Pretty.chunks [ |
45 |
Pretty.block [ |
|
46 |
Pretty.str "Unresolved adhoc overloading of constant", Pretty.brk 1, |
|
53540
7903fe2c271b
prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents:
53538
diff
changeset
|
47 |
prt_const, Pretty.brk 1, Pretty.str "in term", Pretty.brk 1, |
7903fe2c271b
prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents:
53538
diff
changeset
|
48 |
Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t)]], |
53537 | 49 |
Pretty.block ( |
50 |
(if null instances then [Pretty.str "no instances"] |
|
51 |
else Pretty.fbreaks ( |
|
52 |
Pretty.str "multiple instances:" :: |
|
53540
7903fe2c271b
prefer explicit type constraint (again, see also Type.appl_error);
wenzelm
parents:
53538
diff
changeset
|
53 |
map (Pretty.mark Markup.item o Syntax.pretty_term ctxt) instances)))])) |
52688
1e13b2515e2b
show variants in error messages; more precise error messages (give witnesses for multiple instances)
Christian Sternagel
parents:
52687
diff
changeset
|
54 |
end; |
37789 | 55 |
|
53538 | 56 |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
57 |
(* generic data *) |
37789 | 58 |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
59 |
fun variants_eq ((v1, T1), (v2, T2)) = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
60 |
Term.aconv_untyped (v1, v2) andalso T1 = T2; |
37789 | 61 |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
62 |
structure Overload_Data = Generic_Data |
37789 | 63 |
( |
64 |
type T = |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
65 |
{variants : (term * typ) list Symtab.table, |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
66 |
oconsts : string Termtab.table}; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
67 |
val empty = {variants = Symtab.empty, oconsts = Termtab.empty}; |
37789 | 68 |
|
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
37818
diff
changeset
|
69 |
fun merge |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
70 |
({variants = vtab1, oconsts = otab1}, |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
71 |
{variants = vtab2, oconsts = otab2}) : T = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
72 |
let |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
73 |
fun merge_oconsts _ (oconst1, oconst2) = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
74 |
if oconst1 = oconst2 then oconst1 |
53008
128bec4e3fca
indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents:
53007
diff
changeset
|
75 |
else err_duplicate_variant oconst1; |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
76 |
in |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
77 |
{variants = Symtab.merge_list variants_eq (vtab1, vtab2), |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
78 |
oconsts = Termtab.join merge_oconsts (otab1, otab2)} |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
79 |
end; |
37789 | 80 |
); |
81 |
||
82 |
fun map_tables f g = |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
83 |
Overload_Data.map (fn {variants = vtab, oconsts = otab} => |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
84 |
{variants = f vtab, oconsts = g otab}); |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
85 |
|
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
86 |
val is_overloaded = Symtab.defined o #variants o Overload_Data.get o Context.Proof; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
87 |
val get_variants = Symtab.lookup o #variants o Overload_Data.get o Context.Proof; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
88 |
val get_overloaded = Termtab.lookup o #oconsts o Overload_Data.get o Context.Proof; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
89 |
|
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
90 |
fun generic_add_overloaded oconst context = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
91 |
if is_overloaded (Context.proof_of context) oconst then context |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
92 |
else map_tables (Symtab.update (oconst, [])) I context; |
37789 | 93 |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
94 |
fun generic_remove_overloaded oconst context = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
95 |
let |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
96 |
fun remove_oconst_and_variants context oconst = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
97 |
let |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
98 |
val remove_variants = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
99 |
(case get_variants (Context.proof_of context) oconst of |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
100 |
NONE => I |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
101 |
| SOME vs => fold (Termtab.remove (op =) o rpair oconst o fst) vs); |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
102 |
in map_tables (Symtab.delete_safe oconst) remove_variants context end; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
103 |
in |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
104 |
if is_overloaded (Context.proof_of context) oconst then remove_oconst_and_variants context oconst |
53008
128bec4e3fca
indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents:
53007
diff
changeset
|
105 |
else err_not_overloaded oconst |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
106 |
end; |
37789 | 107 |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
108 |
local |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
109 |
fun generic_variant add oconst t context = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
110 |
let |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
111 |
val ctxt = Context.proof_of context; |
53008
128bec4e3fca
indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents:
53007
diff
changeset
|
112 |
val _ = if is_overloaded ctxt oconst then () else err_not_overloaded oconst; |
53005
47db379a6cf9
move treatment of polymorphism to adhoc overloading command;
Christian Sternagel
parents:
53004
diff
changeset
|
113 |
val T = t |> fastype_of; |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
114 |
val t' = Term.map_types (K dummyT) t; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
115 |
in |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
116 |
if add then |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
117 |
let |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
118 |
val _ = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
119 |
(case get_overloaded ctxt t' of |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
120 |
NONE => () |
53008
128bec4e3fca
indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents:
53007
diff
changeset
|
121 |
| SOME oconst' => err_duplicate_variant oconst'); |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
122 |
in |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
123 |
map_tables (Symtab.cons_list (oconst, (t', T))) (Termtab.update (t', oconst)) context |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
124 |
end |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
125 |
else |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
126 |
let |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
127 |
val _ = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
128 |
if member variants_eq (the (get_variants ctxt oconst)) (t', T) then () |
53008
128bec4e3fca
indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents:
53007
diff
changeset
|
129 |
else err_not_a_variant oconst; |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
130 |
in |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
131 |
map_tables (Symtab.map_entry oconst (remove1 variants_eq (t', T))) |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
132 |
(Termtab.delete_safe t') context |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
133 |
|> (fn context => |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
134 |
(case get_variants (Context.proof_of context) oconst of |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
135 |
SOME [] => generic_remove_overloaded oconst context |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
136 |
| _ => context)) |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
137 |
end |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
138 |
end; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
139 |
in |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
140 |
val generic_add_variant = generic_variant true; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
141 |
val generic_remove_variant = generic_variant false; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
142 |
end; |
37789 | 143 |
|
53538 | 144 |
|
37789 | 145 |
(* check / uncheck *) |
146 |
||
53004 | 147 |
fun unifiable_with thy T1 T2 = |
37789 | 148 |
let |
149 |
val maxidx1 = Term.maxidx_of_typ T1; |
|
150 |
val T2' = Logic.incr_tvar (maxidx1 + 1) T2; |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
151 |
val maxidx2 = Term.maxidx_typ T2' maxidx1; |
53004 | 152 |
in can (Sign.typ_unify thy (T1, T2')) (Vartab.empty, maxidx2) end; |
37789 | 153 |
|
53006
83d9984ee639
avoid misleading "instances" in function name;
Christian Sternagel
parents:
53005
diff
changeset
|
154 |
fun get_candidates ctxt (c, T) = |
53007 | 155 |
get_variants ctxt c |
156 |
|> Option.map (map_filter (fn (t, T') => |
|
157 |
if unifiable_with (Proof_Context.theory_of ctxt) T T' then SOME t |
|
158 |
else NONE)); |
|
52687 | 159 |
|
53007 | 160 |
fun insert_variants ctxt t (oconst as Const (c, T)) = |
53006
83d9984ee639
avoid misleading "instances" in function name;
Christian Sternagel
parents:
53005
diff
changeset
|
161 |
(case get_candidates ctxt (c, T) of |
53008
128bec4e3fca
indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents:
53007
diff
changeset
|
162 |
SOME [] => err_unresolved_overloading ctxt (c, T) t [] |
53007 | 163 |
| SOME [variant] => variant |
164 |
| _ => oconst) |
|
165 |
| insert_variants _ _ oconst = oconst; |
|
37789 | 166 |
|
54004 | 167 |
fun insert_overloaded ctxt = |
168 |
let |
|
169 |
fun proc t = |
|
170 |
Term.map_types (K dummyT) t |
|
171 |
|> get_overloaded ctxt |
|
172 |
|> Option.map (Const o rpair (Term.type_of t)); |
|
173 |
in |
|
55237
1e341728bae9
prefer top-down rewriting for output (i.e. uncheck), in accordance to term abbreviations (see 5d2fe4e09354) and AST translations;
wenzelm
parents:
54468
diff
changeset
|
174 |
Pattern.rewrite_term_top (Proof_Context.theory_of ctxt) [] [proc] |
54004 | 175 |
end; |
53007 | 176 |
|
177 |
fun check ctxt = |
|
178 |
map (fn t => Term.map_aterms (insert_variants ctxt t) t); |
|
179 |
||
54468
f6ffe53387ef
reintroduced e2d08b9c9047, lost in 54e290da6da8 + e13b0c88c798
traytel
parents:
54004
diff
changeset
|
180 |
fun uncheck ctxt ts = |
f6ffe53387ef
reintroduced e2d08b9c9047, lost in 54e290da6da8 + e13b0c88c798
traytel
parents:
54004
diff
changeset
|
181 |
if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of) ts then ts |
f6ffe53387ef
reintroduced e2d08b9c9047, lost in 54e290da6da8 + e13b0c88c798
traytel
parents:
54004
diff
changeset
|
182 |
else map (insert_overloaded ctxt) ts; |
53007 | 183 |
|
184 |
fun reject_unresolved ctxt = |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
185 |
let |
53007 | 186 |
val the_candidates = the o get_candidates ctxt; |
37789 | 187 |
fun check_unresolved t = |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
188 |
(case filter (is_overloaded ctxt o fst) (Term.add_consts t []) of |
53007 | 189 |
[] => t |
53008
128bec4e3fca
indicate error-functions more prominently (by name prefix instead of suffix);
Christian Sternagel
parents:
53007
diff
changeset
|
190 |
| (cT :: _) => err_unresolved_overloading ctxt cT t (the_candidates cT)); |
53007 | 191 |
in map check_unresolved end; |
37789 | 192 |
|
53538 | 193 |
|
37789 | 194 |
(* setup *) |
195 |
||
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
196 |
val _ = Context.>> |
53007 | 197 |
(Syntax_Phases.term_check 0 "adhoc_overloading" check |
198 |
#> Syntax_Phases.term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved |
|
199 |
#> Syntax_Phases.term_uncheck 0 "adhoc_overloading" uncheck); |
|
37789 | 200 |
|
53538 | 201 |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
202 |
(* commands *) |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
203 |
|
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
204 |
fun generic_adhoc_overloading_cmd add = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
205 |
if add then |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
206 |
fold (fn (oconst, ts) => |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
207 |
generic_add_overloaded oconst |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
208 |
#> fold (generic_add_variant oconst) ts) |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
209 |
else |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
210 |
fold (fn (oconst, ts) => |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
211 |
fold (generic_remove_variant oconst) ts); |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
212 |
|
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
213 |
fun adhoc_overloading_cmd' add args phi = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
214 |
let val args' = args |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
215 |
|> map (apsnd (map_filter (fn t => |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
216 |
let val t' = Morphism.term phi t; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
217 |
in if Term.aconv_untyped (t, t') then SOME t' else NONE end))); |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
218 |
in generic_adhoc_overloading_cmd add args' end; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
219 |
|
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
220 |
fun adhoc_overloading_cmd add raw_args lthy = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
221 |
let |
55954 | 222 |
fun const_name ctxt = |
56002 | 223 |
fst o dest_Const o Proof_Context.read_const {proper = false, strict = false} ctxt; (* FIXME {proper = true, strict = true} (!?) *) |
53005
47db379a6cf9
move treatment of polymorphism to adhoc overloading command;
Christian Sternagel
parents:
53004
diff
changeset
|
224 |
fun read_term ctxt = singleton (Variable.polymorphic ctxt) o Syntax.read_term ctxt; |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
225 |
val args = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
226 |
raw_args |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
227 |
|> map (apfst (const_name lthy)) |
53005
47db379a6cf9
move treatment of polymorphism to adhoc overloading command;
Christian Sternagel
parents:
53004
diff
changeset
|
228 |
|> map (apsnd (map (read_term lthy))); |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
229 |
in |
78095 | 230 |
Local_Theory.declaration {syntax = true, pervasive = false, pos = Position.thread_data ()} |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
231 |
(adhoc_overloading_cmd' add args) lthy |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
232 |
end; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
233 |
|
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
234 |
val _ = |
69593 | 235 |
Outer_Syntax.local_theory \<^command_keyword>\<open>adhoc_overloading\<close> |
52893 | 236 |
"add adhoc overloading for constants / fixed variables" |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
237 |
(Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd true); |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
238 |
|
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
239 |
val _ = |
69593 | 240 |
Outer_Syntax.local_theory \<^command_keyword>\<open>no_adhoc_overloading\<close> |
59414 | 241 |
"delete adhoc overloading for constants / fixed variables" |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
242 |
(Parse.and_list1 (Parse.const -- Scan.repeat Parse.term) >> adhoc_overloading_cmd false); |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
243 |
|
45422 | 244 |
end; |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
245 |