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