author | haftmann |
Thu, 06 Apr 2006 16:08:22 +0200 | |
changeset 19340 | a4fe025ecd90 |
parent 19280 | 5091dc43817b |
child 19341 | 3414c04fbc39 |
permissions | -rw-r--r-- |
19280
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
1 |
(* Title: Pure/Tools/CODEGEN_THEOREMS.ML |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
2 |
ID: $Id$ |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
3 |
Author: Florian Haftmann, TU Muenchen |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
4 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
5 |
Theorems used for code generation. |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
6 |
*) |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
7 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
8 |
signature CODEGEN_THEOREMS = |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
9 |
sig |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
10 |
val add_notify: (string option -> theory -> theory) -> theory -> theory; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
11 |
val add_preproc: (theory -> thm list -> thm list) -> theory -> theory; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
12 |
val add_funn: thm -> theory -> theory; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
13 |
val add_pred: thm -> theory -> theory; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
14 |
val add_unfold: thm -> theory -> theory; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
15 |
val preprocess: theory -> thm list -> thm list; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
16 |
val preprocess_term: theory -> term -> term; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
17 |
end; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
18 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
19 |
structure CodegenTheorems: CODEGEN_THEOREMS = |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
20 |
struct |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
21 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
22 |
(** auxiliary **) |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
23 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
24 |
fun dest_funn thm = |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
25 |
case try (fst o dest_Const o fst o strip_comb o fst o Logic.dest_equals o prop_of) thm |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
26 |
of SOME c => SOME (c, thm) |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
27 |
| NONE => NONE; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
28 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
29 |
fun dest_pred thm = |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
30 |
case try (fst o dest_Const o fst o strip_comb o snd o Logic.dest_implies o prop_of) thm |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
31 |
of SOME c => SOME (c, thm) |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
32 |
| NONE => NONE; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
33 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
34 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
35 |
(** theory data **) |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
36 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
37 |
datatype procs = Procs of { |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
38 |
preprocs: (serial * (theory -> thm list -> thm list)) list, |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
39 |
notify: (serial * (string option -> theory -> theory)) list |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
40 |
}; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
41 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
42 |
fun mk_procs (preprocs, notify) = Procs { preprocs = preprocs, notify = notify }; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
43 |
fun map_procs f (Procs { preprocs, notify }) = mk_procs (f (preprocs, notify)); |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
44 |
fun merge_procs _ (Procs { preprocs = preprocs1, notify = notify1 }, |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
45 |
Procs { preprocs = preprocs2, notify = notify2 }) = |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
46 |
mk_procs (AList.merge (op =) (K true) (preprocs1, preprocs2), |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
47 |
AList.merge (op =) (K true) (notify1, notify2)); |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
48 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
49 |
datatype codethms = Codethms of { |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
50 |
funns: thm list Symtab.table, |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
51 |
preds: thm list Symtab.table, |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
52 |
unfolds: thm list |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
53 |
}; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
54 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
55 |
fun mk_codethms ((funns, preds), unfolds) = |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
56 |
Codethms { funns = funns, preds = preds, unfolds = unfolds }; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
57 |
fun map_codethms f (Codethms { funns, preds, unfolds }) = |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
58 |
mk_codethms (f ((funns, preds), unfolds)); |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
59 |
fun merge_codethms _ (Codethms { funns = funns1, preds = preds1, unfolds = unfolds1 }, |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
60 |
Codethms { funns = funns2, preds = preds2, unfolds = unfolds2 }) = |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
61 |
mk_codethms ((Symtab.join (K (uncurry (fold (insert eq_thm)))) (funns1, funns2), |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
62 |
Symtab.join (K (uncurry (fold (insert eq_thm)))) (preds1, preds2)), |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
63 |
fold (insert eq_thm) unfolds1 unfolds2); |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
64 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
65 |
datatype T = T of { |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
66 |
procs: procs, |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
67 |
codethms: codethms |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
68 |
}; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
69 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
70 |
fun mk_T (procs, codethms) = T { procs = procs, codethms = codethms }; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
71 |
fun map_T f (T { procs, codethms }) = mk_T (f (procs, codethms)); |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
72 |
fun merge_T pp (T { procs = procs1, codethms = codethms1 }, |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
73 |
T { procs = procs2, codethms = codethms2 }) = |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
74 |
mk_T (merge_procs pp (procs1, procs2), merge_codethms pp (codethms1, codethms2)); |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
75 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
76 |
structure CodegenTheorems = TheoryDataFun |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
77 |
(struct |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
78 |
val name = "Pure/CodegenTheorems"; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
79 |
type T = T; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
80 |
val empty = mk_T (mk_procs ([], []), |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
81 |
mk_codethms ((Symtab.empty, Symtab.empty), [])); |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
82 |
val copy = I; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
83 |
val extend = I; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
84 |
val merge = merge_T; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
85 |
fun print _ _ = (); |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
86 |
end); |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
87 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
88 |
val _ = Context.add_setup CodegenTheorems.init; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
89 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
90 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
91 |
(** notifiers and preprocessors **) |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
92 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
93 |
fun add_notify f = |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
94 |
CodegenTheorems.map (map_T (fn (procs, codethms) => |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
95 |
(procs |> map_procs (fn (preprocs, notify) => |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
96 |
(preprocs, (serial (), f) :: notify)), codethms))); |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
97 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
98 |
fun notify_all c thy = |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
99 |
fold (fn f => f c) (((fn Procs { notify, ... } => map snd notify) |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
100 |
o (fn T { procs, ... } => procs) o CodegenTheorems.get) thy) thy; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
101 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
102 |
fun add_preproc f = |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
103 |
CodegenTheorems.map (map_T (fn (procs, codethms) => |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
104 |
(procs |> map_procs (fn (preprocs, notify) => |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
105 |
((serial (), f) :: preprocs, notify)), codethms))) |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
106 |
#> notify_all NONE; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
107 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
108 |
fun preprocess thy = |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
109 |
fold (fn f => f thy) (((fn Procs { preprocs, ... } => map snd preprocs) |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
110 |
o (fn T { procs, ... } => procs) o CodegenTheorems.get) thy); |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
111 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
112 |
fun preprocess_term thy t = |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
113 |
let |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
114 |
val x = Free (variant (add_term_names (t, [])) "x", fastype_of t); |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
115 |
(* fake definition *) |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
116 |
val eq = setmp quick_and_dirty true (SkipProof.make_thm thy) |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
117 |
(Logic.mk_equals (x, t)); |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
118 |
fun err () = error "preprocess_term: bad preprocessor" |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
119 |
in case map prop_of (preprocess thy [eq]) of |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
120 |
[Const ("==", _) $ x' $ t'] => if x = x' then t' else err () |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
121 |
| _ => err () |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
122 |
end; |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
123 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
124 |
fun add_unfold thm = |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
125 |
CodegenTheorems.map (map_T (fn (procs, codethms) => |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
126 |
(procs, codethms |> map_codethms (fn (defs, unfolds) => |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
127 |
(defs, thm :: unfolds))))) |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
128 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
129 |
fun add_funn thm = |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
130 |
case dest_funn thm |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
131 |
of SOME (c, thm) => |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
132 |
CodegenTheorems.map (map_T (fn (procs, codethms) => |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
133 |
(procs, codethms |> map_codethms (fn ((funns, preds), unfolds) => |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
134 |
((funns |> Symtab.default (c, []) |> Symtab.map (fn thms => thms @ [thm]), preds), unfolds))))) |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
135 |
| NONE => error ("not a function equation: " ^ string_of_thm thm); |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
136 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
137 |
fun add_pred thm = |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
138 |
case dest_pred thm |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
139 |
of SOME (c, thm) => |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
140 |
CodegenTheorems.map (map_T (fn (procs, codethms) => |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
141 |
(procs, codethms |> map_codethms (fn ((funns, preds), unfolds) => |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
142 |
((funns, preds |> Symtab.default (c, []) |> Symtab.map (fn thms => thms @ [thm])), unfolds))))) |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
143 |
| NONE => error ("not a predicate clause: " ^ string_of_thm thm); |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
144 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
145 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
146 |
(** isar **) |
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
147 |
|
5091dc43817b
slight improvement in serializer, stub for code generator theorems added
haftmann
parents:
diff
changeset
|
148 |
end; (* struct *) |