author | haftmann |
Fri, 23 Mar 2007 09:40:53 +0100 | |
changeset 22508 | 6ee2edbce31c |
parent 22400 | cb0b1bbf7e91 |
child 22554 | d1499fff65d8 |
permissions | -rw-r--r-- |
20387 | 1 |
(* Title: Pure/Tools/codegen_consts.ML |
2 |
ID: $Id$ |
|
3 |
Author: Florian Haftmann, TU Muenchen |
|
4 |
||
20855 | 5 |
Identifying constants by name plus normalized type instantantiation schemes. |
22197 | 6 |
Convenient data structures for constants. Auxiliary. |
20387 | 7 |
*) |
8 |
||
9 |
signature CODEGEN_CONSTS = |
|
10 |
sig |
|
11 |
type const = string * typ list (*type instantiations*) |
|
12 |
val const_ord: const * const -> order |
|
13 |
val eq_const: const * const -> bool |
|
14 |
structure Consttab: TABLE |
|
20600 | 15 |
val inst_of_typ: theory -> string * typ -> const |
16 |
val typ_of_inst: theory -> const -> string * typ |
|
17 |
val norm: theory -> const -> const |
|
18 |
val norm_of_typ: theory -> string * typ -> const |
|
22508 | 19 |
val typ_sort_inst: Sorts.algebra -> typ * sort |
20 |
-> sort Vartab.table -> sort Vartab.table |
|
22197 | 21 |
val typargs: theory -> string * typ -> typ list |
22508 | 22 |
val co_of_const: theory -> const |
23 |
-> string * ((string * sort) list * (string * typ list)) |
|
24 |
val co_of_const': theory -> const |
|
25 |
-> (string * ((string * sort) list * (string * typ list))) option |
|
26 |
val cos_of_consts: theory -> const list |
|
27 |
-> string * ((string * sort) list * (string * typ list) list) |
|
28 |
val const_of_co: theory -> string -> (string * sort) list |
|
29 |
-> string * typ list -> const |
|
30 |
val consts_of_cos: theory -> string -> (string * sort) list |
|
31 |
-> (string * typ list) list -> const list |
|
22183 | 32 |
val find_def: theory -> const -> (string (*theory name*) * thm) option |
21118 | 33 |
val consts_of: theory -> term -> const list |
20387 | 34 |
val read_const: theory -> string -> const |
35 |
val string_of_const: theory -> const -> string |
|
20600 | 36 |
val raw_string_of_const: const -> string |
20387 | 37 |
val string_of_const_typ: theory -> string * typ -> string |
22197 | 38 |
val string_of_typ: theory -> typ -> string |
20387 | 39 |
end; |
40 |
||
41 |
structure CodegenConsts: CODEGEN_CONSTS = |
|
42 |
struct |
|
43 |
||
44 |
||
45 |
(* basic data structures *) |
|
46 |
||
47 |
type const = string * typ list (*type instantiations*); |
|
48 |
val const_ord = prod_ord fast_string_ord (list_ord Term.typ_ord); |
|
49 |
val eq_const = is_equal o const_ord; |
|
50 |
||
51 |
structure Consttab = |
|
52 |
TableFun( |
|
53 |
type key = string * typ list; |
|
54 |
val ord = const_ord; |
|
55 |
); |
|
56 |
||
57 |
||
21463
42dd50268c8b
completed class parameter handling in axclass.ML
haftmann
parents:
21118
diff
changeset
|
58 |
(* type instantiations, overloading, dictionary values *) |
20387 | 59 |
|
22197 | 60 |
fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy); |
61 |
||
20600 | 62 |
fun inst_of_typ thy (c_ty as (c, ty)) = |
22197 | 63 |
(c, Sign.const_typargs thy c_ty); |
20387 | 64 |
|
20600 | 65 |
fun typ_of_inst thy (c_tys as (c, tys)) = |
22197 | 66 |
(c, Sign.const_instance thy c_tys); |
20387 | 67 |
|
20389 | 68 |
fun find_def thy (c, tys) = |
20387 | 69 |
let |
70 |
val specs = Defs.specifications_of (Theory.defs_of thy) c; |
|
20389 | 71 |
val typ_instance = case AxClass.class_of_param thy c |
72 |
of SOME _ => let |
|
73 |
fun instance_tycos (Type (tyco1, _), Type (tyco2, _)) = tyco1 = tyco2 |
|
74 |
| instance_tycos (_ , TVar _) = true |
|
75 |
| instance_tycos ty_ty = Sign.typ_instance thy ty_ty; |
|
76 |
in instance_tycos end |
|
20600 | 77 |
| NONE => Sign.typ_instance thy; |
78 |
fun get_def (_, { is_def, thyname, name, lhs, rhs }) = |
|
79 |
if is_def andalso forall typ_instance (tys ~~ lhs) then |
|
80 |
case try (Thm.get_axiom_i thy) name |
|
22183 | 81 |
of SOME thm => SOME (thyname, thm) |
20600 | 82 |
| NONE => NONE |
83 |
else NONE |
|
20387 | 84 |
in |
20600 | 85 |
get_first get_def specs |
20387 | 86 |
end; |
87 |
||
20600 | 88 |
fun norm thy (c, insts) = |
20387 | 89 |
let |
22183 | 90 |
fun disciplined class [ty as Type (tyco, _)] = |
22197 | 91 |
let |
22400 | 92 |
val sorts = Sorts.mg_domain (Sign.classes_of thy) tyco [class] |
93 |
handle CLASS_ERROR => error ("No such instance: " ^ tyco ^ " :: " ^ class |
|
94 |
^ ",\nrequired for overloaded constant " ^ c); |
|
22197 | 95 |
val vs = Name.invents Name.context "'a" (length sorts); |
96 |
in |
|
97 |
(c, [Type (tyco, map (fn v => TVar ((v, 0), [])) vs)]) |
|
98 |
end |
|
22183 | 99 |
| disciplined class _ = |
100 |
(c, [TVar (("'a", 0), [class])]); |
|
20600 | 101 |
in case AxClass.class_of_param thy c |
22183 | 102 |
of SOME class => disciplined class insts |
22197 | 103 |
| NONE => inst_of_typ thy (c, Sign.the_const_type thy c) |
20387 | 104 |
end; |
105 |
||
20600 | 106 |
fun norm_of_typ thy (c, ty) = |
22197 | 107 |
norm thy (c, Sign.const_typargs thy (c, ty)); |
20600 | 108 |
|
20704 | 109 |
fun consts_of thy t = |
21118 | 110 |
fold_aterms (fn Const c => cons (norm_of_typ thy c) | _ => I) t [] |
20704 | 111 |
|
22197 | 112 |
fun typ_sort_inst algebra = |
113 |
let |
|
114 |
val inters = Sorts.inter_sort algebra; |
|
115 |
fun match _ [] = I |
|
116 |
| match (TVar (v, S)) S' = Vartab.map_default (v, []) (fn S'' => inters (S, inters (S', S''))) |
|
117 |
| match (Type (a, Ts)) S = |
|
118 |
fold2 match Ts (Sorts.mg_domain algebra a S) |
|
119 |
in uncurry match end; |
|
120 |
||
121 |
fun typargs thy (c_ty as (c, ty)) = |
|
122 |
let |
|
123 |
val opt_class = AxClass.class_of_param thy c; |
|
124 |
val tys = Sign.const_typargs thy (c, ty); |
|
125 |
in case (opt_class, tys) |
|
126 |
of (SOME _, [Type (_, tys')]) => tys' |
|
127 |
| _ => tys |
|
128 |
end; |
|
129 |
||
20387 | 130 |
|
22508 | 131 |
(* printing *) |
132 |
||
133 |
fun string_of_const thy (c, tys) = |
|
134 |
space_implode " " (Sign.extern_const thy c |
|
135 |
:: map (enclose "[" "]" o Sign.string_of_typ thy) tys); |
|
136 |
||
137 |
fun raw_string_of_const (c, tys) = |
|
138 |
space_implode " " (c |
|
139 |
:: map (enclose "[" "]" o Display.raw_string_of_typ) tys); |
|
140 |
||
141 |
fun string_of_const_typ thy (c, ty) = |
|
142 |
string_of_const thy (c, Consts.typargs (Sign.consts_of thy) (c, ty)); |
|
143 |
||
144 |
||
145 |
(* conversion between constants and datatype constructors *) |
|
146 |
||
147 |
fun const_of_co thy tyco vs (co, tys) = |
|
148 |
norm_of_typ thy (co, tys ---> Type (tyco, map TFree vs)); |
|
149 |
||
150 |
fun consts_of_cos thy tyco vs cos = |
|
151 |
let |
|
152 |
val dty = Type (tyco, map TFree vs); |
|
153 |
fun mk_co (co, tys) = norm_of_typ thy (co, tys ---> dty); |
|
154 |
in map mk_co cos end; |
|
155 |
||
156 |
local |
|
157 |
||
158 |
exception BAD of string; |
|
159 |
||
160 |
fun gen_co_of_const thy const = |
|
161 |
let |
|
162 |
val (c, ty) = (apsnd Logic.unvarifyT o typ_of_inst thy) const; |
|
163 |
fun err () = raise BAD |
|
164 |
("Illegal type for datatype constructor: " ^ Sign.string_of_typ thy ty); |
|
165 |
val (tys, ty') = strip_type ty; |
|
166 |
val (tyco, vs) = ((apsnd o map) dest_TFree o dest_Type) ty' |
|
167 |
handle TYPE _ => err (); |
|
168 |
val sorts = if has_duplicates (eq_fst op =) vs then err () |
|
169 |
else map snd vs; |
|
170 |
val vs_names = Name.invent_list [] "'a" (length vs); |
|
171 |
val vs_map = map fst vs ~~ vs_names; |
|
172 |
val vs' = vs_names ~~ sorts; |
|
173 |
val tys' = (map o map_type_tfree) (fn (v, sort) => |
|
174 |
(TFree ((the o AList.lookup (op =) vs_map) v, sort))) tys |
|
175 |
handle Option => err (); |
|
176 |
in (tyco, (vs', (c, tys'))) end; |
|
177 |
||
178 |
in |
|
179 |
||
180 |
fun co_of_const thy const = gen_co_of_const thy const handle BAD msg => error msg; |
|
181 |
fun co_of_const' thy const = SOME (gen_co_of_const thy const) handle BAD msg => NONE; |
|
182 |
||
183 |
end; |
|
184 |
||
185 |
fun cos_of_consts thy consts = |
|
186 |
let |
|
187 |
val raw_cos = map (co_of_const thy) consts; |
|
188 |
val (tyco, (vs_names, sorts_cos)) = if (length o distinct (eq_fst op =)) raw_cos = 1 |
|
189 |
then ((fst o hd) raw_cos, ((map fst o fst o snd o hd) raw_cos, |
|
190 |
map ((apfst o map) snd o snd) raw_cos)) |
|
191 |
else error ("Term constructors not referring to the same type: " |
|
192 |
^ commas (map (string_of_const thy) consts)); |
|
193 |
val sorts = foldr1 ((uncurry o map2 o curry o Sorts.inter_sort) (Sign.classes_of thy)) |
|
194 |
(map fst sorts_cos); |
|
195 |
val cos = map snd sorts_cos; |
|
196 |
val vs = vs_names ~~ sorts; |
|
197 |
in (tyco, (vs, cos)) end; |
|
198 |
||
199 |
||
20387 | 200 |
(* reading constants as terms *) |
201 |
||
202 |
fun read_const_typ thy raw_t = |
|
203 |
let |
|
204 |
val t = Sign.read_term thy raw_t |
|
205 |
in case try dest_Const t |
|
20600 | 206 |
of SOME c_ty => (typ_of_inst thy o norm_of_typ thy) c_ty |
20389 | 207 |
| NONE => error ("Not a constant: " ^ Sign.string_of_term thy t) |
20387 | 208 |
end; |
209 |
||
210 |
fun read_const thy = |
|
20600 | 211 |
norm_of_typ thy o read_const_typ thy; |
20387 | 212 |
|
213 |
||
214 |
end; |