1 (* Title: Pure/Tools/codegen_func.ML |
|
2 ID: $Id$ |
|
3 Author: Florian Haftmann, TU Muenchen |
|
4 |
|
5 Basic handling of defining equations ("func"s) for code generator framework. |
|
6 *) |
|
7 |
|
8 signature CODEGEN_FUNC = |
|
9 sig |
|
10 val assert_rew: thm -> thm |
|
11 val mk_rew: thm -> thm |
|
12 val mk_func: thm -> thm |
|
13 val head_func: thm -> CodegenConsts.const * typ |
|
14 val bad_thm: string -> 'a |
|
15 val error_thm: (thm -> thm) -> thm -> thm |
|
16 val warning_thm: (thm -> thm) -> thm -> thm option |
|
17 |
|
18 val inst_thm: sort Vartab.table -> thm -> thm |
|
19 val expand_eta: int -> thm -> thm |
|
20 val rewrite_func: thm list -> thm -> thm |
|
21 val norm_args: thm list -> thm list |
|
22 val norm_varnames: (string -> string) -> (string -> string) -> thm list -> thm list |
|
23 end; |
|
24 |
|
25 structure CodegenFunc : CODEGEN_FUNC = |
|
26 struct |
|
27 |
|
28 |
|
29 (* auxiliary *) |
|
30 |
|
31 exception BAD_THM of string; |
|
32 fun bad_thm msg = raise BAD_THM msg; |
|
33 fun error_thm f thm = f thm handle BAD_THM msg => error msg; |
|
34 fun warning_thm f thm = SOME (f thm) handle BAD_THM msg |
|
35 => (warning ("code generator: " ^ msg); NONE); |
|
36 |
|
37 |
|
38 (* making rewrite theorems *) |
|
39 |
|
40 fun assert_rew thm = |
|
41 let |
|
42 val thy = Thm.theory_of_thm thm; |
|
43 val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm |
|
44 handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm) |
|
45 | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm); |
|
46 fun vars_of t = fold_aterms |
|
47 (fn Var (v, _) => insert (op =) v |
|
48 | Free _ => bad_thm ("Illegal free variable in rewrite theorem\n" |
|
49 ^ Display.string_of_thm thm) |
|
50 | _ => I) t []; |
|
51 fun tvars_of t = fold_term_types |
|
52 (fn _ => fold_atyps (fn TVar (v, _) => insert (op =) v |
|
53 | TFree _ => bad_thm |
|
54 ("Illegal free type variable in rewrite theorem\n" ^ Display.string_of_thm thm))) t []; |
|
55 val lhs_vs = vars_of lhs; |
|
56 val rhs_vs = vars_of rhs; |
|
57 val lhs_tvs = tvars_of lhs; |
|
58 val rhs_tvs = tvars_of lhs; |
|
59 val _ = if null (subtract (op =) lhs_vs rhs_vs) |
|
60 then () |
|
61 else bad_thm ("Free variables on right hand side of rewrite theorem\n" |
|
62 ^ Display.string_of_thm thm); |
|
63 val _ = if null (subtract (op =) lhs_tvs rhs_tvs) |
|
64 then () |
|
65 else bad_thm ("Free type variables on right hand side of rewrite theorem\n" |
|
66 ^ Display.string_of_thm thm) |
|
67 in thm end; |
|
68 |
|
69 fun mk_rew thm = |
|
70 let |
|
71 val thy = Thm.theory_of_thm thm; |
|
72 val ctxt = ProofContext.init thy; |
|
73 in |
|
74 thm |
|
75 |> LocalDefs.meta_rewrite_rule ctxt |
|
76 |> assert_rew |
|
77 end; |
|
78 |
|
79 |
|
80 (* making defining equations *) |
|
81 |
|
82 fun assert_func thm = |
|
83 let |
|
84 val thy = Thm.theory_of_thm thm; |
|
85 val (head, args) = (strip_comb o fst o Logic.dest_equals |
|
86 o ObjectLogic.drop_judgment thy o Thm.plain_prop_of) thm; |
|
87 val _ = case head of Const _ => () | _ => |
|
88 bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm); |
|
89 val _ = |
|
90 if has_duplicates (op =) |
|
91 ((fold o fold_aterms) (fn Var (v, _) => cons v |
|
92 | _ => I |
|
93 ) args []) |
|
94 then bad_thm ("Duplicated variables on left hand side of equation\n" |
|
95 ^ Display.string_of_thm thm) |
|
96 else () |
|
97 fun check _ (Abs _) = bad_thm |
|
98 ("Abstraction on left hand side of equation\n" |
|
99 ^ Display.string_of_thm thm) |
|
100 | check 0 (Var _) = () |
|
101 | check _ (Var _) = bad_thm |
|
102 ("Variable with application on left hand side of defining equation\n" |
|
103 ^ Display.string_of_thm thm) |
|
104 | check n (t1 $ t2) = (check (n+1) t1; check 0 t2) |
|
105 | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty |
|
106 then bad_thm |
|
107 ("Partially applied constant on left hand side of equation\n" |
|
108 ^ Display.string_of_thm thm) |
|
109 else (); |
|
110 val _ = map (check 0) args; |
|
111 in thm end; |
|
112 |
|
113 val mk_func = assert_func o mk_rew; |
|
114 |
|
115 fun head_func thm = |
|
116 let |
|
117 val thy = Thm.theory_of_thm thm; |
|
118 val (Const (c_ty as (_, ty))) = (fst o strip_comb o fst o Logic.dest_equals |
|
119 o ObjectLogic.drop_judgment thy o Thm.plain_prop_of) thm; |
|
120 val const = CodegenConsts.const_of_cexpr thy c_ty; |
|
121 in (const, ty) end; |
|
122 |
|
123 |
|
124 (* utilities *) |
|
125 |
|
126 fun inst_thm tvars' thm = |
|
127 let |
|
128 val thy = Thm.theory_of_thm thm; |
|
129 val tvars = (Term.add_tvars o Thm.prop_of) thm []; |
|
130 fun mk_inst (tvar as (v, _)) = case Vartab.lookup tvars' v |
|
131 of SOME sort => SOME (pairself (Thm.ctyp_of thy o TVar) (tvar, (v, sort))) |
|
132 | NONE => NONE; |
|
133 val insts = map_filter mk_inst tvars; |
|
134 in Thm.instantiate (insts, []) thm end; |
|
135 |
|
136 fun expand_eta k thm = |
|
137 let |
|
138 val thy = Thm.theory_of_thm thm; |
|
139 val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm; |
|
140 val (head, args) = strip_comb lhs; |
|
141 val l = if k = ~1 |
|
142 then (length o fst o strip_abs) rhs |
|
143 else Int.max (0, k - length args); |
|
144 val used = Name.make_context (map (fst o fst) (Term.add_vars lhs [])); |
|
145 fun get_name _ 0 used = ([], used) |
|
146 | get_name (Abs (v, ty, t)) k used = |
|
147 used |
|
148 |> Name.variants [v] |
|
149 ||>> get_name t (k - 1) |
|
150 |>> (fn ([v'], vs') => (v', ty) :: vs') |
|
151 | get_name t k used = |
|
152 let |
|
153 val (tys, _) = (strip_type o fastype_of) t |
|
154 in case tys |
|
155 of [] => raise TERM ("expand_eta", [t]) |
|
156 | ty :: _ => |
|
157 used |
|
158 |> Name.variants [""] |
|
159 |-> (fn [v] => get_name (t $ Var ((v, 0), ty)) (k - 1) |
|
160 #>> (fn vs' => (v, ty) :: vs')) |
|
161 end; |
|
162 val (vs, _) = get_name rhs l used; |
|
163 val vs_refl = map (fn (v, ty) => Thm.reflexive (Thm.cterm_of thy (Var ((v, 0), ty)))) vs; |
|
164 in |
|
165 thm |
|
166 |> fold (fn refl => fn thm => Thm.combination thm refl) vs_refl |
|
167 |> Conv.fconv_rule Drule.beta_eta_conversion |
|
168 end; |
|
169 |
|
170 fun rewrite_func rewrites thm = |
|
171 let |
|
172 val rewrite = MetaSimplifier.rewrite false rewrites; |
|
173 val (ct_eq, [ct_lhs, ct_rhs]) = (Drule.strip_comb o Thm.cprop_of) thm; |
|
174 val Const ("==", _) = Thm.term_of ct_eq; |
|
175 val (ct_f, ct_args) = Drule.strip_comb ct_lhs; |
|
176 val rhs' = rewrite ct_rhs; |
|
177 val args' = map rewrite ct_args; |
|
178 val lhs' = Thm.symmetric (fold (fn th1 => fn th2 => Thm.combination th2 th1) |
|
179 args' (Thm.reflexive ct_f)); |
|
180 in Thm.transitive (Thm.transitive lhs' thm) rhs' end; |
|
181 |
|
182 fun norm_args thms = |
|
183 let |
|
184 val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals; |
|
185 val k = fold (curry Int.max o num_args_of o Thm.plain_prop_of) thms 0; |
|
186 in |
|
187 thms |
|
188 |> map (expand_eta k) |
|
189 |> map (Conv.fconv_rule Drule.beta_eta_conversion) |
|
190 end; |
|
191 |
|
192 fun canonical_tvars purify_tvar thm = |
|
193 let |
|
194 val ctyp = Thm.ctyp_of (Thm.theory_of_thm thm); |
|
195 fun tvars_subst_for thm = (fold_types o fold_atyps) |
|
196 (fn TVar (v_i as (v, _), sort) => let |
|
197 val v' = purify_tvar v |
|
198 in if v = v' then I |
|
199 else insert (op =) (v_i, (v', sort)) end |
|
200 | _ => I) (prop_of thm) []; |
|
201 fun mk_inst (v_i, (v', sort)) (maxidx, acc) = |
|
202 let |
|
203 val ty = TVar (v_i, sort) |
|
204 in |
|
205 (maxidx + 1, (ctyp ty, ctyp (TVar ((v', maxidx), sort))) :: acc) |
|
206 end; |
|
207 val maxidx = Thm.maxidx_of thm + 1; |
|
208 val (_, inst) = fold mk_inst (tvars_subst_for thm) (maxidx + 1, []); |
|
209 in Thm.instantiate (inst, []) thm end; |
|
210 |
|
211 fun canonical_vars purify_var thm = |
|
212 let |
|
213 val cterm = Thm.cterm_of (Thm.theory_of_thm thm); |
|
214 fun vars_subst_for thm = fold_aterms |
|
215 (fn Var (v_i as (v, _), ty) => let |
|
216 val v' = purify_var v |
|
217 in if v = v' then I |
|
218 else insert (op =) (v_i, (v', ty)) end |
|
219 | _ => I) (prop_of thm) []; |
|
220 fun mk_inst (v_i as (v, i), (v', ty)) (maxidx, acc) = |
|
221 let |
|
222 val t = Var (v_i, ty) |
|
223 in |
|
224 (maxidx + 1, (cterm t, cterm (Var ((v', maxidx), ty))) :: acc) |
|
225 end; |
|
226 val maxidx = Thm.maxidx_of thm + 1; |
|
227 val (_, inst) = fold mk_inst (vars_subst_for thm) (maxidx + 1, []); |
|
228 in Thm.instantiate ([], inst) thm end; |
|
229 |
|
230 fun canonical_absvars purify_var thm = |
|
231 let |
|
232 val t = Thm.plain_prop_of thm; |
|
233 val t' = Term.map_abs_vars purify_var t; |
|
234 in Thm.rename_boundvars t t' thm end; |
|
235 |
|
236 fun norm_varnames purify_tvar purify_var thms = |
|
237 let |
|
238 fun burrow_thms f [] = [] |
|
239 | burrow_thms f thms = |
|
240 thms |
|
241 |> Conjunction.intr_balanced |
|
242 |> f |
|
243 |> Conjunction.elim_balanced (length thms) |
|
244 in |
|
245 thms |
|
246 |> burrow_thms (canonical_tvars purify_tvar) |
|
247 |> map (canonical_vars purify_var) |
|
248 |> map (canonical_absvars purify_var) |
|
249 |> map Drule.zero_var_indexes |
|
250 end; |
|
251 |
|
252 end; |
|