author  wenzelm 
Sun, 01 Mar 2009 23:36:12 +0100  
changeset 30190  479806475f3c 
parent 28537  1e84256d1a8a 
child 31597  9a59cf39ee78 
permissions  rwrr 
19459  1 
(* Title: HOL/Tools/typedef_codegen.ML 
2 
ID: $Id$ 

3 
Author: Stefan Berghofer and Florian Haftmann, TU Muenchen 

4 

5 
Code generators for trivial typedefs. 

6 
*) 

7 

8 
signature TYPEDEF_CODEGEN = 

9 
sig 

20428  10 
val setup: theory > theory 
19459  11 
end; 
12 

13 
structure TypedefCodegen: TYPEDEF_CODEGEN = 

14 
struct 

15 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset

16 
fun typedef_codegen thy defs dep module brack t gr = 
19459  17 
let 
18 
fun get_name (Type (tname, _)) = tname 

19 
 get_name _ = ""; 

20 
fun mk_fun s T ts = 

21 
let 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset

22 
val (_, gr') = Codegen.invoke_tycodegen thy defs dep module false T gr; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset

23 
val (ps, gr'') = 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset

24 
fold_map (Codegen.invoke_codegen thy defs dep module true) ts gr'; 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset

25 
val id = Codegen.mk_qual_id module (Codegen.get_const_id gr'' s) 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset

26 
in SOME (Codegen.mk_app brack (Codegen.str id) ps, gr'') end; 
19459  27 
fun lookup f T = 
19704  28 
(case TypedefPackage.get_info thy (get_name T) of 
19459  29 
NONE => "" 
19704  30 
 SOME info => f info); 
19459  31 
in 
32 
(case strip_comb t of 

33 
(Const (s, Type ("fun", [T, U])), ts) => 

19704  34 
if lookup #Rep_name T = s andalso 
19459  35 
is_none (Codegen.get_assoc_type thy (get_name T)) 
36 
then mk_fun s T ts 

19704  37 
else if lookup #Abs_name U = s andalso 
19459  38 
is_none (Codegen.get_assoc_type thy (get_name U)) 
39 
then mk_fun s U ts 

40 
else NONE 

41 
 _ => NONE) 

42 
end; 

43 

26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset

44 
fun mk_tyexpr [] s = Codegen.str s 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset

45 
 mk_tyexpr [p] s = Pretty.block [p, Codegen.str (" " ^ s)] 
19459  46 
 mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps; 
47 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset

48 
fun typedef_tycodegen thy defs dep module brack (Type (s, Ts)) gr = 
19704  49 
(case TypedefPackage.get_info thy s of 
19459  50 
NONE => NONE 
19704  51 
 SOME {abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...} => 
19459  52 
if is_some (Codegen.get_assoc_type thy tname) then NONE else 
53 
let 

54 
val module' = Codegen.if_library 

27398
768da1da59d6
simplified retrieval of theory names of consts and types
haftmann
parents:
26975
diff
changeset

55 
(Codegen.thyname_of_type thy tname) module; 
19459  56 
val node_id = tname ^ " (type)"; 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset

57 
val ((((qs, (_, Abs_id)), (_, Rep_id)), ty_id), gr') = gr > fold_map 
19459  58 
(Codegen.invoke_tycodegen thy defs dep module (length Ts = 1)) 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset

59 
Ts >> 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset

60 
Codegen.mk_const_id module' Abs_name >> 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset

61 
Codegen.mk_const_id module' Rep_name >> 
19459  62 
Codegen.mk_type_id module' s; 
63 
val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id) 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset

64 
in SOME (tyexpr, case try (Codegen.get_node gr') node_id of 
19459  65 
NONE => 
66 
let 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset

67 
val (p :: ps, gr'') = fold_map 
19459  68 
(Codegen.invoke_tycodegen thy defs node_id module' false) 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset

69 
(oldT :: Us) (Codegen.add_edge (node_id, dep) 
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset

70 
(Codegen.new_node (node_id, (NONE, "", "")) gr')); 
19459  71 
val s = 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset

72 
Codegen.string_of (Pretty.block [Codegen.str "datatype ", 
19459  73 
mk_tyexpr ps (snd ty_id), 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset

74 
Codegen.str " =", Pretty.brk 1, Codegen.str (Abs_id ^ " of"), 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset

75 
Pretty.brk 1, p, Codegen.str ";"]) ^ "\n\n" ^ 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset

76 
Codegen.string_of (Pretty.block [Codegen.str ("fun " ^ Rep_id), 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset

77 
Pretty.brk 1, Codegen.str ("(" ^ Abs_id), Pretty.brk 1, 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset

78 
Codegen.str "x) = x;"]) ^ "\n\n" ^ 
19459  79 
(if "term_of" mem !Codegen.mode then 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset

80 
Codegen.string_of (Pretty.block [Codegen.str "fun ", 
19459  81 
Codegen.mk_term_of gr'' module' false newT, Pretty.brk 1, 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset

82 
Codegen.str ("(" ^ Abs_id), Pretty.brk 1, 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset

83 
Codegen.str "x) =", Pretty.brk 1, 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset

84 
Pretty.block [Codegen.str ("Const (\"" ^ Abs_name ^ "\","), 
19459  85 
Pretty.brk 1, Codegen.mk_type false (oldT > newT), 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset

86 
Codegen.str ")"], Codegen.str " $", Pretty.brk 1, 
19459  87 
Codegen.mk_term_of gr'' module' false oldT, Pretty.brk 1, 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset

88 
Codegen.str "x;"]) ^ "\n\n" 
19459  89 
else "") ^ 
90 
(if "test" mem !Codegen.mode then 

26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset

91 
Codegen.string_of (Pretty.block [Codegen.str "fun ", 
19459  92 
Codegen.mk_gen gr'' module' false [] "" newT, Pretty.brk 1, 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset

93 
Codegen.str "i =", Pretty.brk 1, 
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset

94 
Pretty.block [Codegen.str (Abs_id ^ " ("), 
19459  95 
Codegen.mk_gen gr'' module' false [] "" oldT, Pretty.brk 1, 
26975
103dca19ef2e
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
berghofe
parents:
20597
diff
changeset

96 
Codegen.str "i);"]]) ^ "\n\n" 
19459  97 
else "") 
98 
in Codegen.map_node node_id (K (NONE, module', s)) gr'' end 

28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset

99 
 SOME _ => Codegen.add_edge (node_id, dep) gr') 
19459  100 
end) 
28537
1e84256d1a8a
established canonical argument order in SML code generators
haftmann
parents:
27398
diff
changeset

101 
 typedef_tycodegen thy defs dep module brack _ gr = NONE; 
19459  102 

103 
val setup = 

104 
Codegen.add_codegen "typedef" typedef_codegen 

105 
#> Codegen.add_tycodegen "typedef" typedef_tycodegen 

106 

107 
end; 