author | wenzelm |
Fri, 11 May 2007 17:54:36 +0200 | |
changeset 22936 | 284b56463da8 |
parent 22921 | 475ff421a6a3 |
child 23691 | cedf9610b71d |
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 |
|
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22737
diff
changeset
|
11 |
type const = string * string option (*constant name, possibly instance*) |
20387 | 12 |
val const_ord: const * const -> order |
13 |
val eq_const: const * const -> bool |
|
14 |
structure Consttab: TABLE |
|
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
15 |
val const_of_cexpr: theory -> string * typ -> const |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
16 |
val string_of_typ: theory -> typ -> string |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
17 |
val string_of_const: theory -> const -> string |
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22737
diff
changeset
|
18 |
val read_bare_const: theory -> string -> string * typ |
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
19 |
val read_const: theory -> string -> const |
22737 | 20 |
val read_const_exprs: theory -> (const list -> const list) |
21 |
-> string list -> const list |
|
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
22 |
|
22508 | 23 |
val co_of_const: theory -> const |
24 |
-> string * ((string * sort) list * (string * typ list)) |
|
25 |
val co_of_const': theory -> const |
|
26 |
-> (string * ((string * sort) list * (string * typ list))) option |
|
27 |
val cos_of_consts: theory -> const list |
|
28 |
-> string * ((string * sort) list * (string * typ list) list) |
|
29 |
val const_of_co: theory -> string -> (string * sort) list |
|
30 |
-> string * typ list -> const |
|
31 |
val consts_of_cos: theory -> string -> (string * sort) list |
|
32 |
-> (string * typ list) list -> const list |
|
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
33 |
|
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
34 |
val typargs: theory -> string * typ -> typ list |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
35 |
val typ_sort_inst: Sorts.algebra -> typ * sort |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
36 |
-> sort Vartab.table -> sort Vartab.table |
20387 | 37 |
end; |
38 |
||
39 |
structure CodegenConsts: CODEGEN_CONSTS = |
|
40 |
struct |
|
41 |
||
42 |
||
43 |
(* basic data structures *) |
|
44 |
||
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
45 |
type const = string * string option; |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
46 |
val const_ord = prod_ord fast_string_ord (option_ord string_ord); |
20387 | 47 |
val eq_const = is_equal o const_ord; |
48 |
||
49 |
structure Consttab = |
|
50 |
TableFun( |
|
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
51 |
type key = const; |
20387 | 52 |
val ord = const_ord; |
53 |
); |
|
54 |
||
22197 | 55 |
fun string_of_typ thy = setmp show_sorts true (Sign.string_of_typ thy); |
56 |
||
20387 | 57 |
|
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
58 |
(* conversion between constant expressions and constants *) |
20387 | 59 |
|
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
60 |
fun const_of_cexpr thy (c_ty as (c, _)) = |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
61 |
case AxClass.class_of_param thy c |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
62 |
of SOME class => (case Sign.const_typargs thy c_ty |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
63 |
of [Type (tyco, _)] => if can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class] |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
64 |
then (c, SOME tyco) |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
65 |
else (c, NONE) |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
66 |
| [_] => (c, NONE)) |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
67 |
| NONE => (c, NONE); |
20387 | 68 |
|
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
69 |
fun string_of_const thy (c, NONE) = Sign.extern_const thy c |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
70 |
| string_of_const thy (c, SOME tyco) = Sign.extern_const thy c |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
71 |
^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco); |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
72 |
|
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
73 |
|
22737 | 74 |
(* reading constants as terms and wildcards pattern *) |
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
75 |
|
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22737
diff
changeset
|
76 |
fun read_bare_const thy raw_t = |
20387 | 77 |
let |
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
78 |
val t = Sign.read_term thy raw_t; |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
79 |
in case try dest_Const t |
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22737
diff
changeset
|
80 |
of SOME c_ty => c_ty |
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
81 |
| NONE => error ("Not a constant: " ^ Sign.string_of_term thy t) |
22197 | 82 |
end; |
83 |
||
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22737
diff
changeset
|
84 |
fun read_const thy = const_of_cexpr thy o read_bare_const thy; |
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
22737
diff
changeset
|
85 |
|
22737 | 86 |
local |
87 |
||
88 |
fun consts_of thy some_thyname = |
|
89 |
let |
|
90 |
val this_thy = Option.map theory some_thyname |> the_default thy; |
|
91 |
val cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I) |
|
92 |
((snd o #constants o Consts.dest o #consts o Sign.rep_sg) this_thy) []; |
|
93 |
fun classop c = case AxClass.class_of_param thy c |
|
94 |
of NONE => [(c, NONE)] |
|
95 |
| SOME class => Symtab.fold |
|
96 |
(fn (tyco, classes) => if AList.defined (op =) classes class |
|
97 |
then cons (c, SOME tyco) else I) |
|
98 |
((#arities o Sorts.rep_algebra o Sign.classes_of) this_thy) |
|
99 |
[(c, NONE)]; |
|
100 |
val consts = maps classop cs; |
|
101 |
fun test_instance thy (class, tyco) = |
|
102 |
can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class] |
|
103 |
fun belongs_here thyname (c, NONE) = |
|
104 |
not (exists (fn thy' => Sign.declared_const thy' c) (Theory.parents_of this_thy)) |
|
105 |
| belongs_here thyname (c, SOME tyco) = |
|
106 |
let |
|
107 |
val SOME class = AxClass.class_of_param thy c |
|
108 |
in not (exists (fn thy' => test_instance thy' (class, tyco)) |
|
109 |
(Theory.parents_of this_thy)) |
|
110 |
end; |
|
111 |
in case some_thyname |
|
112 |
of NONE => consts |
|
113 |
| SOME thyname => filter (belongs_here thyname) consts |
|
114 |
end; |
|
115 |
||
116 |
fun read_const_expr thy "*" = ([], consts_of thy NONE) |
|
117 |
| read_const_expr thy s = if String.isSuffix ".*" s |
|
118 |
then ([], consts_of thy (SOME (unsuffix ".*" s))) |
|
119 |
else ([read_const thy s], []); |
|
120 |
||
121 |
in |
|
122 |
||
123 |
fun read_const_exprs thy select = |
|
124 |
(op @) o apsnd select o pairself flat o split_list o map (read_const_expr thy); |
|
125 |
||
126 |
end; (*local*) |
|
20387 | 127 |
|
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
128 |
(* conversion between constants, constant expressions and datatype constructors *) |
22508 | 129 |
|
130 |
fun const_of_co thy tyco vs (co, tys) = |
|
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
131 |
const_of_cexpr thy (co, tys ---> Type (tyco, map TFree vs)); |
22508 | 132 |
|
133 |
fun consts_of_cos thy tyco vs cos = |
|
134 |
let |
|
135 |
val dty = Type (tyco, map TFree vs); |
|
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
136 |
fun mk_co (co, tys) = const_of_cexpr thy (co, tys ---> dty); |
22508 | 137 |
in map mk_co cos end; |
138 |
||
139 |
local |
|
140 |
||
141 |
exception BAD of string; |
|
142 |
||
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
143 |
fun mg_typ_of_const thy (c, NONE) = Sign.the_const_type thy c |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
144 |
| mg_typ_of_const thy (c, SOME tyco) = |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
145 |
let |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
146 |
val SOME class = AxClass.class_of_param thy c; |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
147 |
val ty = Sign.the_const_type thy c; |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
148 |
(*an approximation*) |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
149 |
val sorts = Sorts.mg_domain (Sign.classes_of thy) tyco [class] |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
150 |
handle CLASS_ERROR => raise BAD ("No such instance: " ^ tyco ^ " :: " ^ class |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
151 |
^ ",\nrequired for overloaded constant " ^ c); |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
152 |
val vs = Name.invents Name.context "'a" (length sorts); |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
153 |
in map_atyps (K (Type (tyco, map (fn v => TVar ((v, 0), [])) vs))) ty end; |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
154 |
|
22508 | 155 |
fun gen_co_of_const thy const = |
156 |
let |
|
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
157 |
val (c, _) = const; |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
158 |
val ty = (Logic.unvarifyT o mg_typ_of_const thy) const; |
22508 | 159 |
fun err () = raise BAD |
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
160 |
("Illegal type for datatype constructor: " ^ string_of_typ thy ty); |
22508 | 161 |
val (tys, ty') = strip_type ty; |
162 |
val (tyco, vs) = ((apsnd o map) dest_TFree o dest_Type) ty' |
|
163 |
handle TYPE _ => err (); |
|
164 |
val sorts = if has_duplicates (eq_fst op =) vs then err () |
|
165 |
else map snd vs; |
|
166 |
val vs_names = Name.invent_list [] "'a" (length vs); |
|
167 |
val vs_map = map fst vs ~~ vs_names; |
|
168 |
val vs' = vs_names ~~ sorts; |
|
169 |
val tys' = (map o map_type_tfree) (fn (v, sort) => |
|
170 |
(TFree ((the o AList.lookup (op =) vs_map) v, sort))) tys |
|
171 |
handle Option => err (); |
|
172 |
in (tyco, (vs', (c, tys'))) end; |
|
173 |
||
174 |
in |
|
175 |
||
176 |
fun co_of_const thy const = gen_co_of_const thy const handle BAD msg => error msg; |
|
177 |
fun co_of_const' thy const = SOME (gen_co_of_const thy const) handle BAD msg => NONE; |
|
178 |
||
179 |
end; |
|
180 |
||
181 |
fun cos_of_consts thy consts = |
|
182 |
let |
|
183 |
val raw_cos = map (co_of_const thy) consts; |
|
184 |
val (tyco, (vs_names, sorts_cos)) = if (length o distinct (eq_fst op =)) raw_cos = 1 |
|
185 |
then ((fst o hd) raw_cos, ((map fst o fst o snd o hd) raw_cos, |
|
186 |
map ((apfst o map) snd o snd) raw_cos)) |
|
187 |
else error ("Term constructors not referring to the same type: " |
|
188 |
^ commas (map (string_of_const thy) consts)); |
|
189 |
val sorts = foldr1 ((uncurry o map2 o curry o Sorts.inter_sort) (Sign.classes_of thy)) |
|
190 |
(map fst sorts_cos); |
|
191 |
val cos = map snd sorts_cos; |
|
192 |
val vs = vs_names ~~ sorts; |
|
193 |
in (tyco, (vs, cos)) end; |
|
194 |
||
195 |
||
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
196 |
(* dictionary values *) |
20387 | 197 |
|
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
198 |
fun typargs thy (c_ty as (c, ty)) = |
20387 | 199 |
let |
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
200 |
val opt_class = AxClass.class_of_param thy c; |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
201 |
val tys = Sign.const_typargs thy (c, ty); |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
202 |
in case (opt_class, tys) |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
203 |
of (SOME class, ty as [Type (tyco, tys')]) => |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
204 |
if can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class] |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
205 |
then tys' else ty |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
206 |
| _ => tys |
20387 | 207 |
end; |
208 |
||
22554
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
209 |
fun typ_sort_inst algebra = |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
210 |
let |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
211 |
val inters = Sorts.inter_sort algebra; |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
212 |
fun match _ [] = I |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
213 |
| match (TVar (v, S)) S' = Vartab.map_default (v, []) (fn S'' => inters (S, inters (S', S''))) |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
214 |
| match (Type (a, Ts)) S = |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
215 |
fold2 match Ts (Sorts.mg_domain algebra a S) |
d1499fff65d8
simplified constant representation in code generator
haftmann
parents:
22508
diff
changeset
|
216 |
in uncurry match end; |
20387 | 217 |
|
218 |
end; |