1 (* Title: Pure/Tools/compute.ML |
|
2 ID: $Id$ |
|
3 Author: Steven Obua |
|
4 *) |
|
5 |
|
6 signature COMPUTE = sig |
|
7 |
|
8 type computer |
|
9 |
|
10 exception Make of string |
|
11 |
|
12 val basic_make : theory -> thm list -> computer |
|
13 val make : theory -> thm list -> computer |
|
14 |
|
15 val compute : computer -> (int -> string) -> cterm -> term |
|
16 val theory_of : computer -> theory |
|
17 |
|
18 val rewrite_param : computer -> (int -> string) -> cterm -> thm |
|
19 val rewrite : computer -> cterm -> thm |
|
20 |
|
21 end |
|
22 |
|
23 structure Compute : COMPUTE = struct |
|
24 |
|
25 exception Make of string; |
|
26 |
|
27 fun is_mono_typ (Type (_, list)) = forall is_mono_typ list |
|
28 | is_mono_typ _ = false |
|
29 |
|
30 fun is_mono_term (Const (_, t)) = is_mono_typ t |
|
31 | is_mono_term (Var (_, t)) = is_mono_typ t |
|
32 | is_mono_term (Free (_, t)) = is_mono_typ t |
|
33 | is_mono_term (Bound _) = true |
|
34 | is_mono_term (a $ b) = is_mono_term a andalso is_mono_term b |
|
35 | is_mono_term (Abs (_, ty, t)) = is_mono_typ ty andalso is_mono_term t |
|
36 |
|
37 structure AMTermTab = TableFun (type key = AbstractMachine.term val ord = AM_Util.term_ord) |
|
38 |
|
39 fun add x y = x + y : int; |
|
40 fun inc x = x + 1; |
|
41 |
|
42 exception Mono of term; |
|
43 |
|
44 val remove_types = |
|
45 let |
|
46 fun remove_types_var table invtable ccount vcount ldepth t = |
|
47 (case Termtab.lookup table t of |
|
48 NONE => |
|
49 let |
|
50 val a = AbstractMachine.Var vcount |
|
51 in |
|
52 (Termtab.update (t, a) table, |
|
53 AMTermTab.update (a, t) invtable, |
|
54 ccount, |
|
55 inc vcount, |
|
56 AbstractMachine.Var (add vcount ldepth)) |
|
57 end |
|
58 | SOME (AbstractMachine.Var v) => |
|
59 (table, invtable, ccount, vcount, AbstractMachine.Var (add v ldepth)) |
|
60 | SOME _ => sys_error "remove_types_var: lookup should be a var") |
|
61 |
|
62 fun remove_types_const table invtable ccount vcount ldepth t = |
|
63 (case Termtab.lookup table t of |
|
64 NONE => |
|
65 let |
|
66 val a = AbstractMachine.Const ccount |
|
67 in |
|
68 (Termtab.update (t, a) table, |
|
69 AMTermTab.update (a, t) invtable, |
|
70 inc ccount, |
|
71 vcount, |
|
72 a) |
|
73 end |
|
74 | SOME (c as AbstractMachine.Const _) => |
|
75 (table, invtable, ccount, vcount, c) |
|
76 | SOME _ => sys_error "remove_types_const: lookup should be a const") |
|
77 |
|
78 fun remove_types table invtable ccount vcount ldepth t = |
|
79 case t of |
|
80 Var (_, ty) => |
|
81 if is_mono_typ ty then remove_types_var table invtable ccount vcount ldepth t |
|
82 else raise (Mono t) |
|
83 | Free (_, ty) => |
|
84 if is_mono_typ ty then remove_types_var table invtable ccount vcount ldepth t |
|
85 else raise (Mono t) |
|
86 | Const (_, ty) => |
|
87 if is_mono_typ ty then remove_types_const table invtable ccount vcount ldepth t |
|
88 else raise (Mono t) |
|
89 | Abs (_, ty, t') => |
|
90 if is_mono_typ ty then |
|
91 let |
|
92 val (table, invtable, ccount, vcount, t') = |
|
93 remove_types table invtable ccount vcount (inc ldepth) t' |
|
94 in |
|
95 (table, invtable, ccount, vcount, AbstractMachine.Abs t') |
|
96 end |
|
97 else |
|
98 raise (Mono t) |
|
99 | a $ b => |
|
100 let |
|
101 val (table, invtable, ccount, vcount, a) = |
|
102 remove_types table invtable ccount vcount ldepth a |
|
103 val (table, invtable, ccount, vcount, b) = |
|
104 remove_types table invtable ccount vcount ldepth b |
|
105 in |
|
106 (table, invtable, ccount, vcount, AbstractMachine.App (a,b)) |
|
107 end |
|
108 | Bound b => (table, invtable, ccount, vcount, AbstractMachine.Var b) |
|
109 in |
|
110 fn (table, invtable, ccount, vcount) => remove_types table invtable ccount vcount 0 |
|
111 end |
|
112 |
|
113 fun infer_types naming = |
|
114 let |
|
115 fun infer_types invtable ldepth bounds ty (AbstractMachine.Var v) = |
|
116 if v < ldepth then (Bound v, List.nth (bounds, v)) else |
|
117 (case AMTermTab.lookup invtable (AbstractMachine.Var (v-ldepth)) of |
|
118 SOME (t as Var (_, ty)) => (t, ty) |
|
119 | SOME (t as Free (_, ty)) => (t, ty) |
|
120 | _ => sys_error "infer_types: lookup should deliver Var or Free") |
|
121 | infer_types invtable ldepth _ ty (c as AbstractMachine.Const _) = |
|
122 (case AMTermTab.lookup invtable c of |
|
123 SOME (c as Const (_, ty)) => (c, ty) |
|
124 | _ => sys_error "infer_types: lookup should deliver Const") |
|
125 | infer_types invtable ldepth bounds (n,ty) (AbstractMachine.App (a, b)) = |
|
126 let |
|
127 val (a, aty) = infer_types invtable ldepth bounds (n+1, ty) a |
|
128 val (adom, arange) = |
|
129 case aty of |
|
130 Type ("fun", [dom, range]) => (dom, range) |
|
131 | _ => sys_error "infer_types: function type expected" |
|
132 val (b, bty) = infer_types invtable ldepth bounds (0, adom) b |
|
133 in |
|
134 (a $ b, arange) |
|
135 end |
|
136 | infer_types invtable ldepth bounds (0, ty as Type ("fun", [dom, range])) |
|
137 (AbstractMachine.Abs m) = |
|
138 let |
|
139 val (m, _) = infer_types invtable (ldepth+1) (dom::bounds) (0, range) m |
|
140 in |
|
141 (Abs (naming ldepth, dom, m), ty) |
|
142 end |
|
143 | infer_types invtable ldepth bounds ty (AbstractMachine.Abs m) = |
|
144 sys_error "infer_types: cannot infer type of abstraction" |
|
145 |
|
146 fun infer invtable ty term = |
|
147 let |
|
148 val (term', _) = infer_types invtable 0 [] (0, ty) term |
|
149 in |
|
150 term' |
|
151 end |
|
152 in |
|
153 infer |
|
154 end |
|
155 |
|
156 datatype computer = |
|
157 Computer of theory_ref * |
|
158 (AbstractMachine.term Termtab.table * term AMTermTab.table * int * AbstractMachine.program) |
|
159 |
|
160 fun basic_make thy raw_ths = |
|
161 let |
|
162 val ths = map (Thm.transfer thy) raw_ths; |
|
163 |
|
164 fun thm2rule table invtable ccount th = |
|
165 let |
|
166 val prop = Thm.plain_prop_of th |
|
167 handle THM _ => raise (Make "theorems must be plain propositions") |
|
168 val (a, b) = Logic.dest_equals prop |
|
169 handle TERM _ => raise (Make "theorems must be meta-level equations") |
|
170 |
|
171 val (table, invtable, ccount, vcount, prop) = |
|
172 remove_types (table, invtable, ccount, 0) (a$b) |
|
173 handle Mono _ => raise (Make "no type variables allowed") |
|
174 val (left, right) = |
|
175 (case prop of AbstractMachine.App x => x | _ => |
|
176 sys_error "make: remove_types should deliver application") |
|
177 |
|
178 fun make_pattern table invtable n vars (var as AbstractMachine.Var v) = |
|
179 let |
|
180 val var' = the (AMTermTab.lookup invtable var) |
|
181 val table = Termtab.delete var' table |
|
182 val invtable = AMTermTab.delete var invtable |
|
183 val vars = Inttab.update_new (v, n) vars handle Inttab.DUP _ => |
|
184 raise (Make "no duplicate variable in pattern allowed") |
|
185 in |
|
186 (table, invtable, n+1, vars, AbstractMachine.PVar) |
|
187 end |
|
188 | make_pattern table invtable n vars (AbstractMachine.Abs _) = |
|
189 raise (Make "no lambda abstractions allowed in pattern") |
|
190 | make_pattern table invtable n vars (AbstractMachine.Const c) = |
|
191 (table, invtable, n, vars, AbstractMachine.PConst (c, [])) |
|
192 | make_pattern table invtable n vars (AbstractMachine.App (a, b)) = |
|
193 let |
|
194 val (table, invtable, n, vars, pa) = |
|
195 make_pattern table invtable n vars a |
|
196 val (table, invtable, n, vars, pb) = |
|
197 make_pattern table invtable n vars b |
|
198 in |
|
199 case pa of |
|
200 AbstractMachine.PVar => |
|
201 raise (Make "patterns may not start with a variable") |
|
202 | AbstractMachine.PConst (c, args) => |
|
203 (table, invtable, n, vars, AbstractMachine.PConst (c, args@[pb])) |
|
204 end |
|
205 |
|
206 val (table, invtable, vcount, vars, pattern) = |
|
207 make_pattern table invtable 0 Inttab.empty left |
|
208 val _ = (case pattern of |
|
209 AbstractMachine.PVar => |
|
210 raise (Make "patterns may not start with a variable") |
|
211 | _ => ()) |
|
212 |
|
213 (* at this point, there shouldn't be any variables |
|
214 left in table or invtable, only constants *) |
|
215 |
|
216 (* finally, provide a function for renaming the |
|
217 pattern bound variables on the right hand side *) |
|
218 |
|
219 fun rename ldepth vars (var as AbstractMachine.Var v) = |
|
220 if v < ldepth then var |
|
221 else (case Inttab.lookup vars (v - ldepth) of |
|
222 NONE => raise (Make "new variable on right hand side") |
|
223 | SOME n => AbstractMachine.Var ((vcount-n-1)+ldepth)) |
|
224 | rename ldepth vars (c as AbstractMachine.Const _) = c |
|
225 | rename ldepth vars (AbstractMachine.App (a, b)) = |
|
226 AbstractMachine.App (rename ldepth vars a, rename ldepth vars b) |
|
227 | rename ldepth vars (AbstractMachine.Abs m) = |
|
228 AbstractMachine.Abs (rename (ldepth+1) vars m) |
|
229 |
|
230 in |
|
231 (table, invtable, ccount, (pattern, rename 0 vars right)) |
|
232 end |
|
233 |
|
234 val (table, invtable, ccount, rules) = |
|
235 fold_rev (fn th => fn (table, invtable, ccount, rules) => |
|
236 let |
|
237 val (table, invtable, ccount, rule) = |
|
238 thm2rule table invtable ccount th |
|
239 in (table, invtable, ccount, rule::rules) end) |
|
240 ths (Termtab.empty, AMTermTab.empty, 0, []) |
|
241 |
|
242 val prog = AbstractMachine.compile rules |
|
243 |
|
244 in Computer (Theory.self_ref thy, (table, invtable, ccount, prog)) end |
|
245 |
|
246 fun make thy ths = |
|
247 let |
|
248 val (_, {mk_rews={mk=mk,mk_eq_True=emk, ...},...}) = rep_ss (simpset_of thy) |
|
249 fun mk_eq_True th = (case emk th of NONE => [th] | SOME th' => [th, th']) |
|
250 in |
|
251 basic_make thy (maps mk (maps mk_eq_True ths)) |
|
252 end |
|
253 |
|
254 fun compute (Computer r) naming ct = |
|
255 let |
|
256 val {t=t, T=ty, thy=ctthy, ...} = rep_cterm ct |
|
257 val (rthy, (table, invtable, ccount, prog)) = r |
|
258 val thy = Theory.merge (Theory.deref rthy, ctthy) |
|
259 val (table, invtable, ccount, vcount, t) = remove_types (table, invtable, ccount, 0) t |
|
260 val t = AbstractMachine.run prog t |
|
261 val t = infer_types naming invtable ty t |
|
262 in |
|
263 t |
|
264 end |
|
265 |
|
266 fun theory_of (Computer (rthy, _)) = Theory.deref rthy |
|
267 |
|
268 fun default_naming i = "v_" ^ Int.toString i |
|
269 |
|
270 exception Param of computer * (int -> string) * cterm; |
|
271 |
|
272 fun rewrite_param r n ct = |
|
273 let val thy = theory_of_cterm ct in |
|
274 invoke_oracle_i thy "Pure.compute" (thy, Param (r, n, ct)) |
|
275 end |
|
276 |
|
277 fun rewrite r ct = rewrite_param r default_naming ct |
|
278 |
|
279 |
|
280 (* theory setup *) |
|
281 |
|
282 fun compute_oracle (thy, Param (r, naming, ct)) = |
|
283 let |
|
284 val _ = Theory.assert_super (theory_of r) thy |
|
285 val t' = compute r naming ct |
|
286 in |
|
287 Logic.mk_equals (term_of ct, t') |
|
288 end |
|
289 |
|
290 val _ = Context.add_setup (Theory.add_oracle ("compute", compute_oracle)) |
|
291 |
|
292 end |
|