author | Christian Sternagel |
Fri, 02 Aug 2013 12:11:02 +0900 | |
changeset 52892 | 9ce4d52c9176 |
parent 52707 | e2d08b9c9047 |
child 52893 | aa2afbafd983 |
permissions | -rw-r--r-- |
37789 | 1 |
(* Author: Alexander Krauss, TU Muenchen |
2 |
Author: Christian Sternagel, University of Innsbruck |
|
3 |
||
4 |
Ad-hoc overloading of constants based on their types. |
|
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 |
||
45422 | 22 |
val show_variants = Attrib.setup_config_bool @{binding show_variants} (K false); |
37789 | 23 |
|
24 |
(* errors *) |
|
25 |
||
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
26 |
fun duplicate_variant_error oconst = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
27 |
error ("Duplicate variant of " ^ quote oconst); |
37789 | 28 |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
29 |
fun not_a_variant_error oconst = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
30 |
error ("Not a variant of " ^ quote oconst); |
37789 | 31 |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
32 |
fun not_overloaded_error oconst = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
33 |
error ("Constant " ^ quote oconst ^ " is not declared as overloaded"); |
37789 | 34 |
|
52688
1e13b2515e2b
show variants in error messages; more precise error messages (give witnesses for multiple instances)
Christian Sternagel
parents:
52687
diff
changeset
|
35 |
fun unresolved_overloading_error ctxt (c, T) t instances = |
1e13b2515e2b
show variants in error messages; more precise error messages (give witnesses for multiple instances)
Christian Sternagel
parents:
52687
diff
changeset
|
36 |
let val ctxt' = Config.put show_variants true ctxt |
1e13b2515e2b
show variants in error messages; more precise error messages (give witnesses for multiple instances)
Christian Sternagel
parents:
52687
diff
changeset
|
37 |
in |
1e13b2515e2b
show variants in error messages; more precise error messages (give witnesses for multiple instances)
Christian Sternagel
parents:
52687
diff
changeset
|
38 |
cat_lines ( |
1e13b2515e2b
show variants in error messages; more precise error messages (give witnesses for multiple instances)
Christian Sternagel
parents:
52687
diff
changeset
|
39 |
"Unresolved overloading of constant" :: |
1e13b2515e2b
show variants in error messages; more precise error messages (give witnesses for multiple instances)
Christian Sternagel
parents:
52687
diff
changeset
|
40 |
quote c ^ " :: " ^ quote (Syntax.string_of_typ ctxt' T) :: |
1e13b2515e2b
show variants in error messages; more precise error messages (give witnesses for multiple instances)
Christian Sternagel
parents:
52687
diff
changeset
|
41 |
"in term " :: |
1e13b2515e2b
show variants in error messages; more precise error messages (give witnesses for multiple instances)
Christian Sternagel
parents:
52687
diff
changeset
|
42 |
quote (Syntax.string_of_term ctxt' t) :: |
1e13b2515e2b
show variants in error messages; more precise error messages (give witnesses for multiple instances)
Christian Sternagel
parents:
52687
diff
changeset
|
43 |
(if null instances then "no instances" else "multiple instances:") :: |
52892 | 44 |
map (Markup.markup Markup.item o Syntax.string_of_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
|
45 |
|> error |
1e13b2515e2b
show variants in error messages; more precise error messages (give witnesses for multiple instances)
Christian Sternagel
parents:
52687
diff
changeset
|
46 |
end; |
37789 | 47 |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
48 |
(* generic data *) |
37789 | 49 |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
50 |
fun variants_eq ((v1, T1), (v2, T2)) = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
51 |
Term.aconv_untyped (v1, v2) andalso T1 = T2; |
37789 | 52 |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
53 |
structure Overload_Data = Generic_Data |
37789 | 54 |
( |
55 |
type T = |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
56 |
{variants : (term * typ) list Symtab.table, |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
57 |
oconsts : string Termtab.table}; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
58 |
val empty = {variants = Symtab.empty, oconsts = Termtab.empty}; |
37789 | 59 |
val extend = I; |
60 |
||
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
37818
diff
changeset
|
61 |
fun merge |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
62 |
({variants = vtab1, oconsts = otab1}, |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
63 |
{variants = vtab2, oconsts = otab2}) : T = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
64 |
let |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
65 |
fun merge_oconsts _ (oconst1, oconst2) = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
66 |
if oconst1 = oconst2 then oconst1 |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
67 |
else duplicate_variant_error oconst1; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
68 |
in |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
69 |
{variants = Symtab.merge_list variants_eq (vtab1, vtab2), |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
70 |
oconsts = Termtab.join merge_oconsts (otab1, otab2)} |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
71 |
end; |
37789 | 72 |
); |
73 |
||
74 |
fun map_tables f g = |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
75 |
Overload_Data.map (fn {variants = vtab, oconsts = otab} => |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
76 |
{variants = f vtab, oconsts = g otab}); |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
77 |
|
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
78 |
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
|
79 |
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
|
80 |
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
|
81 |
|
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
82 |
fun generic_add_overloaded oconst context = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
83 |
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
|
84 |
else map_tables (Symtab.update (oconst, [])) I context; |
37789 | 85 |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
86 |
fun generic_remove_overloaded oconst context = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
87 |
let |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
88 |
fun remove_oconst_and_variants context oconst = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
89 |
let |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
90 |
val remove_variants = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
91 |
(case get_variants (Context.proof_of context) oconst of |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
92 |
NONE => I |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
93 |
| 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
|
94 |
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
|
95 |
in |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
96 |
if is_overloaded (Context.proof_of context) oconst then remove_oconst_and_variants context oconst |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
97 |
else not_overloaded_error oconst |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
98 |
end; |
37789 | 99 |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
100 |
local |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
101 |
fun generic_variant add oconst t context = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
102 |
let |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
103 |
val ctxt = Context.proof_of context; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
104 |
val _ = if is_overloaded ctxt oconst then () else not_overloaded_error oconst; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
105 |
val T = t |> singleton (Variable.polymorphic ctxt) |> fastype_of; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
106 |
val t' = Term.map_types (K dummyT) t; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
107 |
in |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
108 |
if add then |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
109 |
let |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
110 |
val _ = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
111 |
(case get_overloaded ctxt t' of |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
112 |
NONE => () |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
113 |
| SOME oconst' => duplicate_variant_error oconst'); |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
114 |
in |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
115 |
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
|
116 |
end |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
117 |
else |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
118 |
let |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
119 |
val _ = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
120 |
if member variants_eq (the (get_variants ctxt oconst)) (t', T) then () |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
121 |
else not_a_variant_error oconst; |
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.map_entry oconst (remove1 variants_eq (t', T))) |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
124 |
(Termtab.delete_safe t') context |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
125 |
|> (fn context => |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
126 |
(case get_variants (Context.proof_of context) oconst of |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
127 |
SOME [] => generic_remove_overloaded oconst context |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
128 |
| _ => context)) |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
129 |
end |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
130 |
end; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
131 |
in |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
132 |
val generic_add_variant = generic_variant true; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
133 |
val generic_remove_variant = generic_variant false; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
134 |
end; |
37789 | 135 |
|
136 |
(* check / uncheck *) |
|
137 |
||
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
138 |
fun unifiable_with thy T1 (t, T2) = |
37789 | 139 |
let |
140 |
val maxidx1 = Term.maxidx_of_typ T1; |
|
141 |
val T2' = Logic.incr_tvar (maxidx1 + 1) T2; |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
142 |
val maxidx2 = Term.maxidx_typ T2' maxidx1; |
37789 | 143 |
in |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
144 |
(Sign.typ_unify thy (T1, T2') (Vartab.empty, maxidx2); SOME t) |
37789 | 145 |
handle Type.TUNIFY => NONE |
146 |
end; |
|
147 |
||
52687 | 148 |
fun get_instances ctxt (c, T) = |
149 |
Same.function (get_variants ctxt) c |
|
150 |
|> map_filter (unifiable_with (Proof_Context.theory_of ctxt) T); |
|
151 |
||
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
152 |
fun insert_variants_same ctxt t (Const (c, T)) = |
52687 | 153 |
(case get_instances ctxt (c, T) of |
52688
1e13b2515e2b
show variants in error messages; more precise error messages (give witnesses for multiple instances)
Christian Sternagel
parents:
52687
diff
changeset
|
154 |
[] => unresolved_overloading_error ctxt (c, T) t [] |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
155 |
| [variant] => variant |
45422 | 156 |
| _ => raise Same.SAME) |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
157 |
| insert_variants_same _ _ _ = raise Same.SAME; |
37789 | 158 |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
159 |
fun insert_overloaded_same ctxt variant = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
160 |
let |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
161 |
val thy = Proof_Context.theory_of ctxt; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
162 |
val t = Pattern.rewrite_term thy [] [fn t => |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
163 |
Term.map_types (K dummyT) t |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
164 |
|> get_overloaded ctxt |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
165 |
|> Option.map (Const o rpair (fastype_of variant))] variant; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
166 |
in |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
167 |
if Term.aconv_untyped (variant, t) then raise Same.SAME |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
168 |
else t |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
169 |
end; |
37789 | 170 |
|
171 |
fun gen_check_uncheck replace ts ctxt = |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
172 |
Same.capture (Same.map replace) ts |
37789 | 173 |
|> Option.map (rpair ctxt); |
174 |
||
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
175 |
fun check ts ctxt = gen_check_uncheck (fn t => |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
176 |
Term_Subst.map_aterms_same (insert_variants_same ctxt t) t) ts ctxt; |
45422 | 177 |
|
178 |
fun uncheck ts ctxt = |
|
52707
e2d08b9c9047
permissive uncheck -- allow printing of malformed terms (e.g. in error messages);
traytel
parents:
52688
diff
changeset
|
179 |
if Config.get ctxt show_variants orelse exists (is_none o try Term.type_of) ts then NONE |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
180 |
else gen_check_uncheck (insert_overloaded_same ctxt) ts ctxt; |
37789 | 181 |
|
182 |
fun reject_unresolved ts ctxt = |
|
183 |
let |
|
184 |
fun check_unresolved t = |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
185 |
(case filter (is_overloaded ctxt o fst) (Term.add_consts t []) of |
45422 | 186 |
[] => () |
52688
1e13b2515e2b
show variants in error messages; more precise error messages (give witnesses for multiple instances)
Christian Sternagel
parents:
52687
diff
changeset
|
187 |
| ((c, T) :: _) => unresolved_overloading_error ctxt (c, T) t (get_instances ctxt (c, T))); |
37789 | 188 |
val _ = map check_unresolved ts; |
189 |
in NONE end; |
|
190 |
||
191 |
(* setup *) |
|
192 |
||
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
193 |
val _ = Context.>> |
45444 | 194 |
(Syntax_Phases.term_check' 0 "adhoc_overloading" check |
195 |
#> Syntax_Phases.term_check' 1 "adhoc_overloading_unresolved_check" reject_unresolved |
|
196 |
#> Syntax_Phases.term_uncheck' 0 "adhoc_overloading" uncheck); |
|
37789 | 197 |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
198 |
(* commands *) |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
199 |
|
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
200 |
fun generic_adhoc_overloading_cmd add = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
201 |
if add then |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
202 |
fold (fn (oconst, ts) => |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
203 |
generic_add_overloaded oconst |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
204 |
#> fold (generic_add_variant oconst) ts) |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
205 |
else |
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 |
fold (generic_remove_variant oconst) ts); |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
208 |
|
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
209 |
fun adhoc_overloading_cmd' add args phi = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
210 |
let val args' = args |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
211 |
|> map (apsnd (map_filter (fn t => |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
212 |
let val t' = Morphism.term phi t; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
213 |
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
|
214 |
in generic_adhoc_overloading_cmd add args' end; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
215 |
|
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
216 |
fun adhoc_overloading_cmd add raw_args lthy = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
217 |
let |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
218 |
fun const_name ctxt = fst o dest_Const o Proof_Context.read_const ctxt false dummyT; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
219 |
val args = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
220 |
raw_args |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
221 |
|> map (apfst (const_name lthy)) |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
222 |
|> map (apsnd (map (Syntax.read_term lthy))); |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
223 |
in |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
224 |
Local_Theory.declaration {syntax = true, pervasive = false} |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
225 |
(adhoc_overloading_cmd' add args) lthy |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
226 |
end; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
227 |
|
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
228 |
val _ = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
229 |
Outer_Syntax.local_theory @{command_spec "adhoc_overloading"} |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
230 |
"add ad-hoc overloading for constants / fixed variables" |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
231 |
(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
|
232 |
|
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
233 |
val _ = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
234 |
Outer_Syntax.local_theory @{command_spec "no_adhoc_overloading"} |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
235 |
"add ad-hoc overloading for constants / fixed variables" |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
236 |
(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
|
237 |
|
45422 | 238 |
end; |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
239 |