270 |
270 |
271 |
271 |
272 |
272 |
273 (** trivial code generator **) |
273 (** trivial code generator **) |
274 |
274 |
275 fun typedef_codegen thy gr dep brack t = |
275 fun typedef_codegen thy defs gr dep thyname brack t = |
276 let |
276 let |
|
277 fun get_name (Type (tname, _)) = tname |
|
278 | get_name _ = ""; |
277 fun mk_fun s T ts = |
279 fun mk_fun s T ts = |
278 let |
280 let |
279 val (gr', _) = Codegen.invoke_tycodegen thy dep false (gr, T); |
281 val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr, T); |
280 val (gr'', ps) = |
282 val (gr'', ps) = |
281 foldl_map (Codegen.invoke_codegen thy dep true) (gr', ts); |
283 foldl_map (Codegen.invoke_codegen thy defs dep thyname true) (gr', ts); |
282 val id = Codegen.mk_const_id thy s |
284 val id = Codegen.mk_const_id thy |
|
285 thyname (Codegen.thyname_of_type (get_name T) thy) s |
283 in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end; |
286 in SOME (gr'', Codegen.mk_app brack (Pretty.str id) ps) end; |
284 fun get_name (Type (tname, _)) = tname |
|
285 | get_name _ = ""; |
|
286 fun lookup f T = getOpt (Option.map f (Symtab.lookup |
287 fun lookup f T = getOpt (Option.map f (Symtab.lookup |
287 (TypedefData.get thy, get_name T)), "") |
288 (TypedefData.get thy, get_name T)), "") |
288 in |
289 in |
289 (case strip_comb t of |
290 (case strip_comb t of |
290 (Const (s, Type ("fun", [T, U])), ts) => |
291 (Const (s, Type ("fun", [T, U])), ts) => |
300 |
301 |
301 fun mk_tyexpr [] s = Pretty.str s |
302 fun mk_tyexpr [] s = Pretty.str s |
302 | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)] |
303 | mk_tyexpr [p] s = Pretty.block [p, Pretty.str (" " ^ s)] |
303 | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps; |
304 | mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps; |
304 |
305 |
305 fun typedef_tycodegen thy gr dep brack (Type (s, Ts)) = |
306 fun typedef_tycodegen thy defs gr dep thyname brack (Type (s, Ts)) = |
306 (case Symtab.lookup (TypedefData.get thy, s) of |
307 (case Symtab.lookup (TypedefData.get thy, s) of |
307 NONE => NONE |
308 NONE => NONE |
308 | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) => |
309 | SOME (newT as Type (tname, Us), oldT, Abs_name, Rep_name) => |
309 if isSome (Codegen.get_assoc_type thy tname) then NONE else |
310 if isSome (Codegen.get_assoc_type thy tname) then NONE else |
310 let |
311 let |
311 val Abs_id = Codegen.mk_const_id thy Abs_name; |
312 val thyname' = Codegen.thyname_of_type tname thy; |
312 val Rep_id = Codegen.mk_const_id thy Rep_name; |
313 val Abs_id = Codegen.mk_const_id thy thyname' thyname' Abs_name; |
313 val ty_id = Codegen.mk_type_id thy s; |
314 val Rep_id = Codegen.mk_const_id thy thyname' thyname' Rep_name; |
|
315 val ty_id = Codegen.mk_type_id thy thyname' thyname' s; |
|
316 val ty_call_id = Codegen.mk_type_id thy thyname thyname' s; |
314 val (gr', qs) = foldl_map |
317 val (gr', qs) = foldl_map |
315 (Codegen.invoke_tycodegen thy dep (length Ts = 1)) (gr, Ts); |
318 (Codegen.invoke_tycodegen thy defs dep thyname (length Ts = 1)) (gr, Ts); |
316 val gr'' = Graph.add_edge (Abs_id, dep) gr' handle Graph.UNDEF _ => |
319 val gr'' = Graph.add_edge (Abs_name, dep) gr' handle Graph.UNDEF _ => |
317 let |
320 let |
318 val (gr'', p :: ps) = foldl_map |
321 val (gr'', p :: ps) = foldl_map |
319 (Codegen.invoke_tycodegen thy Abs_id false) |
322 (Codegen.invoke_tycodegen thy defs Abs_name thyname' false) |
320 (Graph.add_edge (Abs_id, dep) |
323 (Graph.add_edge (Abs_name, dep) |
321 (Graph.new_node (Abs_id, (NONE, "")) gr'), oldT :: Us); |
324 (Graph.new_node (Abs_name, (NONE, "", "")) gr'), oldT :: Us); |
322 val s = |
325 val s = |
323 Pretty.string_of (Pretty.block [Pretty.str "datatype ", |
326 Pretty.string_of (Pretty.block [Pretty.str "datatype ", |
324 mk_tyexpr ps ty_id, |
327 mk_tyexpr ps ty_id, |
325 Pretty.str " =", Pretty.brk 1, Pretty.str (Abs_id ^ " of"), |
328 Pretty.str " =", Pretty.brk 1, Pretty.str (Abs_id ^ " of"), |
326 Pretty.brk 1, p, Pretty.str ";"]) ^ "\n\n" ^ |
329 Pretty.brk 1, p, Pretty.str ";"]) ^ "\n\n" ^ |
327 Pretty.string_of (Pretty.block [Pretty.str ("fun " ^ Rep_id), |
330 Pretty.string_of (Pretty.block [Pretty.str ("fun " ^ Rep_id), |
328 Pretty.brk 1, Pretty.str ("(" ^ Abs_id), Pretty.brk 1, |
331 Pretty.brk 1, Pretty.str ("(" ^ Abs_id), Pretty.brk 1, |
329 Pretty.str "x) = x;"]) ^ "\n\n" ^ |
332 Pretty.str "x) = x;"]) ^ "\n\n" ^ |
330 (if "term_of" mem !Codegen.mode then |
333 (if "term_of" mem !Codegen.mode then |
331 Pretty.string_of (Pretty.block [Pretty.str "fun ", |
334 Pretty.string_of (Pretty.block [Pretty.str "fun ", |
332 Codegen.mk_term_of thy false newT, Pretty.brk 1, |
335 Codegen.mk_term_of thy thyname' false newT, Pretty.brk 1, |
333 Pretty.str ("(" ^ Abs_id), Pretty.brk 1, |
336 Pretty.str ("(" ^ Abs_id), Pretty.brk 1, |
334 Pretty.str "x) =", Pretty.brk 1, |
337 Pretty.str "x) =", Pretty.brk 1, |
335 Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","), |
338 Pretty.block [Pretty.str ("Const (\"" ^ Abs_name ^ "\","), |
336 Pretty.brk 1, Codegen.mk_type false (oldT --> newT), |
339 Pretty.brk 1, Codegen.mk_type false (oldT --> newT), |
337 Pretty.str ")"], Pretty.str " $", Pretty.brk 1, |
340 Pretty.str ")"], Pretty.str " $", Pretty.brk 1, |
338 Codegen.mk_term_of thy false oldT, Pretty.brk 1, |
341 Codegen.mk_term_of thy thyname' false oldT, Pretty.brk 1, |
339 Pretty.str "x;"]) ^ "\n\n" |
342 Pretty.str "x;"]) ^ "\n\n" |
340 else "") ^ |
343 else "") ^ |
341 (if "test" mem !Codegen.mode then |
344 (if "test" mem !Codegen.mode then |
342 Pretty.string_of (Pretty.block [Pretty.str "fun ", |
345 Pretty.string_of (Pretty.block [Pretty.str "fun ", |
343 Codegen.mk_gen thy false [] "" newT, Pretty.brk 1, |
346 Codegen.mk_gen thy thyname' false [] "" newT, Pretty.brk 1, |
344 Pretty.str "i =", Pretty.brk 1, |
347 Pretty.str "i =", Pretty.brk 1, |
345 Pretty.block [Pretty.str (Abs_id ^ " ("), |
348 Pretty.block [Pretty.str (Abs_id ^ " ("), |
346 Codegen.mk_gen thy false [] "" oldT, Pretty.brk 1, |
349 Codegen.mk_gen thy thyname' false [] "" oldT, Pretty.brk 1, |
347 Pretty.str "i);"]]) ^ "\n\n" |
350 Pretty.str "i);"]]) ^ "\n\n" |
348 else "") |
351 else "") |
349 in Graph.map_node Abs_id (K (NONE, s)) gr'' end |
352 in Graph.map_node Abs_name (K (NONE, thyname', s)) gr'' end |
350 in |
353 in |
351 SOME (gr'', mk_tyexpr qs ty_id) |
354 SOME (gr'', mk_tyexpr qs ty_call_id) |
352 end) |
355 end) |
353 | typedef_tycodegen thy gr dep brack _ = NONE; |
356 | typedef_tycodegen thy defs gr dep thyname brack _ = NONE; |
354 |
357 |
355 val setup = |
358 val setup = |
356 [TypedefData.init, |
359 [TypedefData.init, |
357 Codegen.add_codegen "typedef" typedef_codegen, |
360 Codegen.add_codegen "typedef" typedef_codegen, |
358 Codegen.add_tycodegen "typedef" typedef_tycodegen]; |
361 Codegen.add_tycodegen "typedef" typedef_tycodegen]; |