|
1 structure codegen_prep = |
|
2 struct |
|
3 |
|
4 exception Prepare_thms of string; |
|
5 |
|
6 fun is_meta_eq th = |
|
7 let |
|
8 fun check ((Const ("==", _)) $ _ $ _) = true |
|
9 | check _ = false |
|
10 in |
|
11 check (concl_of th) |
|
12 end |
|
13 |
|
14 fun printty ty = |
|
15 let |
|
16 fun immerse s [] = [] |
|
17 | immerse s [x] = [x] |
|
18 | immerse s (x::xs) = x::s::(immerse s xs) |
|
19 |
|
20 fun py t = |
|
21 let |
|
22 val (name, args) = dest_Type t |
|
23 val args' = map printty args |
|
24 in |
|
25 concat (immerse "_" (name::args')) |
|
26 end |
|
27 |
|
28 val (args, res) = strip_type ty |
|
29 val tystrs = map py (args@[res]) |
|
30 |
|
31 val s = "'"^(concat (immerse "_" tystrs))^"'" |
|
32 in |
|
33 s |
|
34 end |
|
35 |
|
36 fun head_name th = |
|
37 let val s = |
|
38 let |
|
39 val h = fst (strip_comb (hd (snd (strip_comb (concl_of th))))) |
|
40 val n = fst (dest_Const h) |
|
41 val ty = snd (dest_Const h) |
|
42 val hn = fst (dest_Const h) |
|
43 in |
|
44 hn^"_"^(printty ty) handle _ => (writeln ("warning: polymorphic "^hn); hn) |
|
45 end |
|
46 in |
|
47 s |
|
48 end |
|
49 |
|
50 val mangle_id = |
|
51 let |
|
52 fun tr #"=" = "_eq_" |
|
53 | tr #"." = "_" |
|
54 | tr #" " = "_" |
|
55 | tr #"<" = "_le_" |
|
56 | tr #">" = "_ge_" |
|
57 | tr #"(" = "_bro_" |
|
58 | tr #")" = "_brc_" |
|
59 | tr #"+" = "_plus_" |
|
60 | tr #"*" = "_mult_" |
|
61 | tr #"-" = "_minus_" |
|
62 | tr #"|" = "_or_" |
|
63 | tr #"&" = "_and_" |
|
64 | tr x = Char.toString x |
|
65 fun m s = "simp_"^(String.translate tr s) |
|
66 in |
|
67 m |
|
68 end |
|
69 |
|
70 fun group f [] = [] |
|
71 | group f (x::xs) = |
|
72 let |
|
73 val g = group f xs |
|
74 val key = f x |
|
75 in |
|
76 case assoc (g, key) of |
|
77 None => (key, [x])::g |
|
78 | Some l => overwrite (g, (key, x::l)) |
|
79 end |
|
80 |
|
81 fun prepare_thms ths = |
|
82 let |
|
83 val ths = (filter is_meta_eq ths) @ (map (standard o mk_meta_eq) (filter (not o is_meta_eq) ths)) |
|
84 val _ = if forall Thm.no_prems ths then () else raise (Prepare_thms "premisse found") |
|
85 val thmgroups = group head_name ths |
|
86 val test_clashgroups = group (fn (a,b) => mangle_id a) thmgroups |
|
87 val _ = if (length thmgroups <> length test_clashgroups) then raise (Prepare_thms "clash after name mangling") else () |
|
88 |
|
89 fun prep (name, ths) = |
|
90 let |
|
91 val m = mangle_id name |
|
92 |
|
93 in |
|
94 (m, true, ths) |
|
95 end |
|
96 |
|
97 val thmgroups = map prep thmgroups |
|
98 in |
|
99 (thmgroups) |
|
100 end |
|
101 |
|
102 fun writestr filename s = |
|
103 let |
|
104 val f = TextIO.openOut filename |
|
105 val _ = TextIO.output(f, s) |
|
106 val _ = TextIO.closeOut f |
|
107 in |
|
108 () |
|
109 end |
|
110 end |