author | Christian Sternagel |
Fri, 09 Aug 2013 19:34:23 +0900 | |
changeset 53007 | 54e290da6da8 |
parent 53006 | 83d9984ee639 |
child 53008 | 128bec4e3fca |
permissions | -rw-r--r-- |
37789 | 1 |
(* Author: Alexander Krauss, TU Muenchen |
2 |
Author: Christian Sternagel, University of Innsbruck |
|
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 |
||
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; |
53005
47db379a6cf9
move treatment of polymorphism to adhoc overloading command;
Christian Sternagel
parents:
53004
diff
changeset
|
105 |
val T = t |> fastype_of; |
52622
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 |
||
53004 | 138 |
fun unifiable_with thy T1 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; |
53004 | 143 |
in can (Sign.typ_unify thy (T1, T2')) (Vartab.empty, maxidx2) end; |
37789 | 144 |
|
53006
83d9984ee639
avoid misleading "instances" in function name;
Christian Sternagel
parents:
53005
diff
changeset
|
145 |
fun get_candidates ctxt (c, T) = |
53007 | 146 |
get_variants ctxt c |
147 |
|> Option.map (map_filter (fn (t, T') => |
|
148 |
if unifiable_with (Proof_Context.theory_of ctxt) T T' then SOME t |
|
149 |
else NONE)); |
|
52687 | 150 |
|
53007 | 151 |
fun insert_variants ctxt t (oconst as Const (c, T)) = |
53006
83d9984ee639
avoid misleading "instances" in function name;
Christian Sternagel
parents:
53005
diff
changeset
|
152 |
(case get_candidates ctxt (c, T) of |
53007 | 153 |
SOME [] => unresolved_overloading_error ctxt (c, T) t [] |
154 |
| SOME [variant] => variant |
|
155 |
| _ => oconst) |
|
156 |
| insert_variants _ _ oconst = oconst; |
|
37789 | 157 |
|
53007 | 158 |
fun insert_overloaded ctxt variant = |
159 |
(case try Term.type_of variant of |
|
160 |
NONE => variant |
|
161 |
| SOME T => |
|
162 |
Pattern.rewrite_term (Proof_Context.theory_of ctxt) [] |
|
163 |
[Option.map (Const o rpair T) o get_overloaded ctxt o Term.map_types (K dummyT)] variant); |
|
164 |
||
165 |
fun check ctxt = |
|
166 |
map (fn t => Term.map_aterms (insert_variants ctxt t) t); |
|
167 |
||
168 |
fun uncheck ctxt = |
|
169 |
if Config.get ctxt show_variants then I |
|
170 |
else map (insert_overloaded ctxt); |
|
171 |
||
172 |
fun reject_unresolved ctxt = |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
173 |
let |
53007 | 174 |
val the_candidates = the o get_candidates ctxt; |
37789 | 175 |
fun check_unresolved t = |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
176 |
(case filter (is_overloaded ctxt o fst) (Term.add_consts t []) of |
53007 | 177 |
[] => t |
178 |
| (cT :: _) => unresolved_overloading_error ctxt cT t (the_candidates cT)); |
|
179 |
in map check_unresolved end; |
|
37789 | 180 |
|
181 |
(* setup *) |
|
182 |
||
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
183 |
val _ = Context.>> |
53007 | 184 |
(Syntax_Phases.term_check 0 "adhoc_overloading" check |
185 |
#> Syntax_Phases.term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved |
|
186 |
#> Syntax_Phases.term_uncheck 0 "adhoc_overloading" uncheck); |
|
37789 | 187 |
|
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
188 |
(* commands *) |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
189 |
|
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
190 |
fun generic_adhoc_overloading_cmd add = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
191 |
if add then |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
192 |
fold (fn (oconst, ts) => |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
193 |
generic_add_overloaded oconst |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
194 |
#> fold (generic_add_variant oconst) ts) |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
195 |
else |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
196 |
fold (fn (oconst, ts) => |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
197 |
fold (generic_remove_variant oconst) ts); |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
198 |
|
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
199 |
fun adhoc_overloading_cmd' add args phi = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
200 |
let val args' = args |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
201 |
|> map (apsnd (map_filter (fn t => |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
202 |
let val t' = Morphism.term phi t; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
203 |
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
|
204 |
in generic_adhoc_overloading_cmd add args' end; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
205 |
|
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
206 |
fun adhoc_overloading_cmd add raw_args lthy = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
207 |
let |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
208 |
fun const_name ctxt = fst o dest_Const o Proof_Context.read_const ctxt false dummyT; |
53005
47db379a6cf9
move treatment of polymorphism to adhoc overloading command;
Christian Sternagel
parents:
53004
diff
changeset
|
209 |
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
|
210 |
val args = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
211 |
raw_args |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
212 |
|> map (apfst (const_name lthy)) |
53005
47db379a6cf9
move treatment of polymorphism to adhoc overloading command;
Christian Sternagel
parents:
53004
diff
changeset
|
213 |
|> map (apsnd (map (read_term lthy))); |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
214 |
in |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
215 |
Local_Theory.declaration {syntax = true, pervasive = false} |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
216 |
(adhoc_overloading_cmd' add args) lthy |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
217 |
end; |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
218 |
|
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
219 |
val _ = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
220 |
Outer_Syntax.local_theory @{command_spec "adhoc_overloading"} |
52893 | 221 |
"add adhoc overloading for constants / fixed variables" |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
222 |
(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
|
223 |
|
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
224 |
val _ = |
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
225 |
Outer_Syntax.local_theory @{command_spec "no_adhoc_overloading"} |
52893 | 226 |
"add adhoc overloading for constants / fixed variables" |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
227 |
(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
|
228 |
|
45422 | 229 |
end; |
52622
e0ff1625e96d
localized and modernized adhoc-overloading (patch by Christian Sternagel);
wenzelm
parents:
50768
diff
changeset
|
230 |