151 fun the_reserved (Target { reserved, ... }) = reserved; |
151 fun the_reserved (Target { reserved, ... }) = reserved; |
152 fun the_includes (Target { includes, ... }) = includes; |
152 fun the_includes (Target { includes, ... }) = includes; |
153 fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x; |
153 fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x; |
154 fun the_module_alias (Target { module_alias , ... }) = module_alias; |
154 fun the_module_alias (Target { module_alias , ... }) = module_alias; |
155 |
155 |
156 structure CodeTargetData = Theory_Data |
156 structure Targets = Theory_Data |
157 ( |
157 ( |
158 type T = (target Symtab.table * string list) * int; |
158 type T = (target Symtab.table * string list) * int; |
159 val empty = ((Symtab.empty, []), 80); |
159 val empty = ((Symtab.empty, []), 80); |
160 val extend = I; |
160 val extend = I; |
161 fun merge (((target1, exc1), width1), ((target2, exc2), width2)) : T = |
161 fun merge (((target1, exc1), width1), ((target2, exc2), width2)) : T = |
162 ((Symtab.join (merge_target true) (target1, target2), |
162 ((Symtab.join (merge_target true) (target1, target2), |
163 Library.merge (op =) (exc1, exc2)), Int.max (width1, width2)); |
163 Library.merge (op =) (exc1, exc2)), Int.max (width1, width2)); |
164 ); |
164 ); |
165 |
165 |
166 val abort_allowed = snd o fst o CodeTargetData.get; |
166 val abort_allowed = snd o fst o Targets.get; |
167 |
167 |
168 val the_default_width = snd o CodeTargetData.get; |
168 val the_default_width = snd o Targets.get; |
169 |
169 |
170 fun assert_target thy target = if Symtab.defined ((fst o fst) (CodeTargetData.get thy)) target |
170 fun assert_target thy target = if Symtab.defined ((fst o fst) (Targets.get thy)) target |
171 then target |
171 then target |
172 else error ("Unknown code target language: " ^ quote target); |
172 else error ("Unknown code target language: " ^ quote target); |
173 |
173 |
174 fun put_target (target, seri) thy = |
174 fun put_target (target, seri) thy = |
175 let |
175 let |
176 val lookup_target = Symtab.lookup ((fst o fst) (CodeTargetData.get thy)); |
176 val lookup_target = Symtab.lookup ((fst o fst) (Targets.get thy)); |
177 val _ = case seri |
177 val _ = case seri |
178 of Extends (super, _) => if is_some (lookup_target super) then () |
178 of Extends (super, _) => if is_some (lookup_target super) then () |
179 else error ("Unknown code target language: " ^ quote super) |
179 else error ("Unknown code target language: " ^ quote super) |
180 | _ => (); |
180 | _ => (); |
181 val overwriting = case (Option.map the_serializer o lookup_target) target |
181 val overwriting = case (Option.map the_serializer o lookup_target) target |
187 val _ = if overwriting |
187 val _ = if overwriting |
188 then warning ("Overwriting existing target " ^ quote target) |
188 then warning ("Overwriting existing target " ^ quote target) |
189 else (); |
189 else (); |
190 in |
190 in |
191 thy |
191 thy |
192 |> (CodeTargetData.map o apfst o apfst oo Symtab.map_default) |
192 |> (Targets.map o apfst o apfst o Symtab.update) |
193 (target, make_target ((serial (), seri), (([], Symtab.empty), |
193 (target, make_target ((serial (), seri), (([], Symtab.empty), |
194 (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)), |
194 (mk_name_syntax_table ((Symtab.empty, Symreltab.empty), (Symtab.empty, Symtab.empty)), |
195 Symtab.empty)))) |
195 Symtab.empty)))) |
196 ((map_target o apfst o apsnd o K) seri) |
|
197 end; |
196 end; |
198 |
197 |
199 fun add_target (target, seri) = put_target (target, Serializer seri); |
198 fun add_target (target, seri) = put_target (target, Serializer seri); |
200 fun extend_target (target, (super, modify)) = |
199 fun extend_target (target, (super, modify)) = |
201 put_target (target, Extends (super, modify)); |
200 put_target (target, Extends (super, modify)); |
203 fun map_target_data target f thy = |
202 fun map_target_data target f thy = |
204 let |
203 let |
205 val _ = assert_target thy target; |
204 val _ = assert_target thy target; |
206 in |
205 in |
207 thy |
206 thy |
208 |> (CodeTargetData.map o apfst o apfst o Symtab.map_entry target o map_target) f |
207 |> (Targets.map o apfst o apfst o Symtab.map_entry target o map_target) f |
209 end; |
208 end; |
210 |
209 |
211 fun map_reserved target = |
210 fun map_reserved target = |
212 map_target_data target o apsnd o apfst o apfst; |
211 map_target_data target o apsnd o apfst o apfst; |
213 fun map_includes target = |
212 fun map_includes target = |
215 fun map_name_syntax target = |
214 fun map_name_syntax target = |
216 map_target_data target o apsnd o apsnd o apfst o map_name_syntax_table; |
215 map_target_data target o apsnd o apsnd o apfst o map_name_syntax_table; |
217 fun map_module_alias target = |
216 fun map_module_alias target = |
218 map_target_data target o apsnd o apsnd o apsnd; |
217 map_target_data target o apsnd o apsnd o apsnd; |
219 |
218 |
220 fun set_default_code_width k = (CodeTargetData.map o apsnd) (K k); |
219 fun set_default_code_width k = (Targets.map o apsnd) (K k); |
221 |
220 |
222 |
221 |
223 (** serializer usage **) |
222 (** serializer usage **) |
224 |
223 |
225 (* montage *) |
224 (* montage *) |
226 |
225 |
227 fun the_literals thy = |
226 fun the_literals thy = |
228 let |
227 let |
229 val ((targets, _), _) = CodeTargetData.get thy; |
228 val ((targets, _), _) = Targets.get thy; |
230 fun literals target = case Symtab.lookup targets target |
229 fun literals target = case Symtab.lookup targets target |
231 of SOME data => (case the_serializer data |
230 of SOME data => (case the_serializer data |
232 of Serializer (_, literals) => literals |
231 of Serializer (_, literals) => literals |
233 | Extends (super, _) => literals super) |
232 | Extends (super, _) => literals super) |
234 | NONE => error ("Unknown code target language: " ^ quote target); |
233 | NONE => error ("Unknown code target language: " ^ quote target); |
282 program4 names2 |
281 program4 names2 |
283 end; |
282 end; |
284 |
283 |
285 fun mount_serializer thy alt_serializer target some_width module args naming program names = |
284 fun mount_serializer thy alt_serializer target some_width module args naming program names = |
286 let |
285 let |
287 val ((targets, abortable), default_width) = CodeTargetData.get thy; |
286 val ((targets, abortable), default_width) = Targets.get thy; |
288 fun collapse_hierarchy target = |
287 fun collapse_hierarchy target = |
289 let |
288 let |
290 val data = case Symtab.lookup targets target |
289 val data = case Symtab.lookup targets target |
291 of SOME data => data |
290 of SOME data => data |
292 | NONE => error ("Unknown code target language: " ^ quote target); |
291 | NONE => error ("Unknown code target language: " ^ quote target); |