1 (* Title: Tools/Compute_Oracle/compute.ML |
|
2 Author: Steven Obua |
|
3 *) |
|
4 |
|
5 signature COMPUTE = sig |
|
6 |
|
7 type computer |
|
8 type theorem |
|
9 type naming = int -> string |
|
10 |
|
11 datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML |
|
12 |
|
13 (* Functions designated with a ! in front of them actually update the computer parameter *) |
|
14 |
|
15 exception Make of string |
|
16 val make : machine -> theory -> thm list -> computer |
|
17 val make_with_cache : machine -> theory -> term list -> thm list -> computer |
|
18 val theory_of : computer -> theory |
|
19 val hyps_of : computer -> term list |
|
20 val shyps_of : computer -> sort list |
|
21 (* ! *) val update : computer -> thm list -> unit |
|
22 (* ! *) val update_with_cache : computer -> term list -> thm list -> unit |
|
23 (* ! *) val discard : computer -> unit |
|
24 |
|
25 (* ! *) val set_naming : computer -> naming -> unit |
|
26 val naming_of : computer -> naming |
|
27 |
|
28 exception Compute of string |
|
29 val simplify : computer -> theorem -> thm |
|
30 val rewrite : computer -> cterm -> thm |
|
31 |
|
32 val make_theorem : computer -> thm -> string list -> theorem |
|
33 (* ! *) val instantiate : computer -> (string * cterm) list -> theorem -> theorem |
|
34 (* ! *) val evaluate_prem : computer -> int -> theorem -> theorem |
|
35 (* ! *) val modus_ponens : computer -> int -> thm -> theorem -> theorem |
|
36 |
|
37 end |
|
38 |
|
39 structure Compute :> COMPUTE = struct |
|
40 |
|
41 open Report; |
|
42 |
|
43 datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML |
|
44 |
|
45 (* Terms are mapped to integer codes *) |
|
46 structure Encode :> |
|
47 sig |
|
48 type encoding |
|
49 val empty : encoding |
|
50 val insert : term -> encoding -> int * encoding |
|
51 val lookup_code : term -> encoding -> int option |
|
52 val lookup_term : int -> encoding -> term option |
|
53 val remove_code : int -> encoding -> encoding |
|
54 val remove_term : term -> encoding -> encoding |
|
55 val fold : ((term * int) -> 'a -> 'a) -> encoding -> 'a -> 'a |
|
56 end |
|
57 = |
|
58 struct |
|
59 |
|
60 type encoding = int * (int Termtab.table) * (term Inttab.table) |
|
61 |
|
62 val empty = (0, Termtab.empty, Inttab.empty) |
|
63 |
|
64 fun insert t (e as (count, term2int, int2term)) = |
|
65 (case Termtab.lookup term2int t of |
|
66 NONE => (count, (count+1, Termtab.update_new (t, count) term2int, Inttab.update_new (count, t) int2term)) |
|
67 | SOME code => (code, e)) |
|
68 |
|
69 fun lookup_code t (_, term2int, _) = Termtab.lookup term2int t |
|
70 |
|
71 fun lookup_term c (_, _, int2term) = Inttab.lookup int2term c |
|
72 |
|
73 fun remove_code c (e as (count, term2int, int2term)) = |
|
74 (case lookup_term c e of NONE => e | SOME t => (count, Termtab.delete t term2int, Inttab.delete c int2term)) |
|
75 |
|
76 fun remove_term t (e as (count, term2int, int2term)) = |
|
77 (case lookup_code t e of NONE => e | SOME c => (count, Termtab.delete t term2int, Inttab.delete c int2term)) |
|
78 |
|
79 fun fold f (_, term2int, _) = Termtab.fold f term2int |
|
80 |
|
81 end |
|
82 |
|
83 exception Make of string; |
|
84 exception Compute of string; |
|
85 |
|
86 local |
|
87 fun make_constant t ty encoding = |
|
88 let |
|
89 val (code, encoding) = Encode.insert t encoding |
|
90 in |
|
91 (encoding, AbstractMachine.Const code) |
|
92 end |
|
93 in |
|
94 |
|
95 fun remove_types encoding t = |
|
96 case t of |
|
97 Var (_, ty) => make_constant t ty encoding |
|
98 | Free (_, ty) => make_constant t ty encoding |
|
99 | Const (_, ty) => make_constant t ty encoding |
|
100 | Abs (_, ty, t') => |
|
101 let val (encoding, t'') = remove_types encoding t' in |
|
102 (encoding, AbstractMachine.Abs t'') |
|
103 end |
|
104 | a $ b => |
|
105 let |
|
106 val (encoding, a) = remove_types encoding a |
|
107 val (encoding, b) = remove_types encoding b |
|
108 in |
|
109 (encoding, AbstractMachine.App (a,b)) |
|
110 end |
|
111 | Bound b => (encoding, AbstractMachine.Var b) |
|
112 end |
|
113 |
|
114 local |
|
115 fun type_of (Free (_, ty)) = ty |
|
116 | type_of (Const (_, ty)) = ty |
|
117 | type_of (Var (_, ty)) = ty |
|
118 | type_of _ = sys_error "infer_types: type_of error" |
|
119 in |
|
120 fun infer_types naming encoding = |
|
121 let |
|
122 fun infer_types _ bounds _ (AbstractMachine.Var v) = (Bound v, List.nth (bounds, v)) |
|
123 | infer_types _ bounds _ (AbstractMachine.Const code) = |
|
124 let |
|
125 val c = the (Encode.lookup_term code encoding) |
|
126 in |
|
127 (c, type_of c) |
|
128 end |
|
129 | infer_types level bounds _ (AbstractMachine.App (a, b)) = |
|
130 let |
|
131 val (a, aty) = infer_types level bounds NONE a |
|
132 val (adom, arange) = |
|
133 case aty of |
|
134 Type ("fun", [dom, range]) => (dom, range) |
|
135 | _ => sys_error "infer_types: function type expected" |
|
136 val (b, bty) = infer_types level bounds (SOME adom) b |
|
137 in |
|
138 (a $ b, arange) |
|
139 end |
|
140 | infer_types level bounds (SOME (ty as Type ("fun", [dom, range]))) (AbstractMachine.Abs m) = |
|
141 let |
|
142 val (m, _) = infer_types (level+1) (dom::bounds) (SOME range) m |
|
143 in |
|
144 (Abs (naming level, dom, m), ty) |
|
145 end |
|
146 | infer_types _ _ NONE (AbstractMachine.Abs m) = sys_error "infer_types: cannot infer type of abstraction" |
|
147 |
|
148 fun infer ty term = |
|
149 let |
|
150 val (term', _) = infer_types 0 [] (SOME ty) term |
|
151 in |
|
152 term' |
|
153 end |
|
154 in |
|
155 infer |
|
156 end |
|
157 end |
|
158 |
|
159 datatype prog = |
|
160 ProgBarras of AM_Interpreter.program |
|
161 | ProgBarrasC of AM_Compiler.program |
|
162 | ProgHaskell of AM_GHC.program |
|
163 | ProgSML of AM_SML.program |
|
164 |
|
165 fun machine_of_prog (ProgBarras _) = BARRAS |
|
166 | machine_of_prog (ProgBarrasC _) = BARRAS_COMPILED |
|
167 | machine_of_prog (ProgHaskell _) = HASKELL |
|
168 | machine_of_prog (ProgSML _) = SML |
|
169 |
|
170 type naming = int -> string |
|
171 |
|
172 fun default_naming i = "v_" ^ Int.toString i |
|
173 |
|
174 datatype computer = Computer of |
|
175 (theory_ref * Encode.encoding * term list * unit Sorttab.table * prog * unit Unsynchronized.ref * naming) |
|
176 option Unsynchronized.ref |
|
177 |
|
178 fun theory_of (Computer (Unsynchronized.ref (SOME (rthy,_,_,_,_,_,_)))) = Theory.deref rthy |
|
179 fun hyps_of (Computer (Unsynchronized.ref (SOME (_,_,hyps,_,_,_,_)))) = hyps |
|
180 fun shyps_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = Sorttab.keys (shyptable) |
|
181 fun shyptab_of (Computer (Unsynchronized.ref (SOME (_,_,_,shyptable,_,_,_)))) = shyptable |
|
182 fun stamp_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,stamp,_)))) = stamp |
|
183 fun prog_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,prog,_,_)))) = prog |
|
184 fun encoding_of (Computer (Unsynchronized.ref (SOME (_,encoding,_,_,_,_,_)))) = encoding |
|
185 fun set_encoding (Computer (r as Unsynchronized.ref (SOME (p1,encoding,p2,p3,p4,p5,p6)))) encoding' = |
|
186 (r := SOME (p1,encoding',p2,p3,p4,p5,p6)) |
|
187 fun naming_of (Computer (Unsynchronized.ref (SOME (_,_,_,_,_,_,n)))) = n |
|
188 fun set_naming (Computer (r as Unsynchronized.ref (SOME (p1,p2,p3,p4,p5,p6,naming)))) naming'= |
|
189 (r := SOME (p1,p2,p3,p4,p5,p6,naming')) |
|
190 |
|
191 fun ref_of (Computer r) = r |
|
192 |
|
193 datatype cthm = ComputeThm of term list * sort list * term |
|
194 |
|
195 fun thm2cthm th = |
|
196 let |
|
197 val {hyps, prop, tpairs, shyps, ...} = Thm.rep_thm th |
|
198 val _ = if not (null tpairs) then raise Make "theorems may not contain tpairs" else () |
|
199 in |
|
200 ComputeThm (hyps, shyps, prop) |
|
201 end |
|
202 |
|
203 fun make_internal machine thy stamp encoding cache_pattern_terms raw_ths = |
|
204 let |
|
205 fun transfer (x:thm) = Thm.transfer thy x |
|
206 val ths = map (thm2cthm o Thm.strip_shyps o transfer) raw_ths |
|
207 |
|
208 fun make_pattern encoding n vars (var as AbstractMachine.Abs _) = |
|
209 raise (Make "no lambda abstractions allowed in pattern") |
|
210 | make_pattern encoding n vars (var as AbstractMachine.Var _) = |
|
211 raise (Make "no bound variables allowed in pattern") |
|
212 | make_pattern encoding n vars (AbstractMachine.Const code) = |
|
213 (case the (Encode.lookup_term code encoding) of |
|
214 Var _ => ((n+1, Inttab.update_new (code, n) vars, AbstractMachine.PVar) |
|
215 handle Inttab.DUP _ => raise (Make "no duplicate variable in pattern allowed")) |
|
216 | _ => (n, vars, AbstractMachine.PConst (code, []))) |
|
217 | make_pattern encoding n vars (AbstractMachine.App (a, b)) = |
|
218 let |
|
219 val (n, vars, pa) = make_pattern encoding n vars a |
|
220 val (n, vars, pb) = make_pattern encoding n vars b |
|
221 in |
|
222 case pa of |
|
223 AbstractMachine.PVar => |
|
224 raise (Make "patterns may not start with a variable") |
|
225 | AbstractMachine.PConst (c, args) => |
|
226 (n, vars, AbstractMachine.PConst (c, args@[pb])) |
|
227 end |
|
228 |
|
229 fun thm2rule (encoding, hyptable, shyptable) th = |
|
230 let |
|
231 val (ComputeThm (hyps, shyps, prop)) = th |
|
232 val hyptable = fold (fn h => Termtab.update (h, ())) hyps hyptable |
|
233 val shyptable = fold (fn sh => Sorttab.update (sh, ())) shyps shyptable |
|
234 val (prems, prop) = (Logic.strip_imp_prems prop, Logic.strip_imp_concl prop) |
|
235 val (a, b) = Logic.dest_equals prop |
|
236 handle TERM _ => raise (Make "theorems must be meta-level equations (with optional guards)") |
|
237 val a = Envir.eta_contract a |
|
238 val b = Envir.eta_contract b |
|
239 val prems = map Envir.eta_contract prems |
|
240 |
|
241 val (encoding, left) = remove_types encoding a |
|
242 val (encoding, right) = remove_types encoding b |
|
243 fun remove_types_of_guard encoding g = |
|
244 (let |
|
245 val (t1, t2) = Logic.dest_equals g |
|
246 val (encoding, t1) = remove_types encoding t1 |
|
247 val (encoding, t2) = remove_types encoding t2 |
|
248 in |
|
249 (encoding, AbstractMachine.Guard (t1, t2)) |
|
250 end handle TERM _ => raise (Make "guards must be meta-level equations")) |
|
251 val (encoding, prems) = fold_rev (fn p => fn (encoding, ps) => let val (e, p) = remove_types_of_guard encoding p in (e, p::ps) end) prems (encoding, []) |
|
252 |
|
253 (* Principally, a check should be made here to see if the (meta-) hyps contain any of the variables of the rule. |
|
254 As it is, all variables of the rule are schematic, and there are no schematic variables in meta-hyps, therefore |
|
255 this check can be left out. *) |
|
256 |
|
257 val (vcount, vars, pattern) = make_pattern encoding 0 Inttab.empty left |
|
258 val _ = (case pattern of |
|
259 AbstractMachine.PVar => |
|
260 raise (Make "patterns may not start with a variable") |
|
261 (* | AbstractMachine.PConst (_, []) => |
|
262 (print th; raise (Make "no parameter rewrite found"))*) |
|
263 | _ => ()) |
|
264 |
|
265 (* finally, provide a function for renaming the |
|
266 pattern bound variables on the right hand side *) |
|
267 |
|
268 fun rename level vars (var as AbstractMachine.Var _) = var |
|
269 | rename level vars (c as AbstractMachine.Const code) = |
|
270 (case Inttab.lookup vars code of |
|
271 NONE => c |
|
272 | SOME n => AbstractMachine.Var (vcount-n-1+level)) |
|
273 | rename level vars (AbstractMachine.App (a, b)) = |
|
274 AbstractMachine.App (rename level vars a, rename level vars b) |
|
275 | rename level vars (AbstractMachine.Abs m) = |
|
276 AbstractMachine.Abs (rename (level+1) vars m) |
|
277 |
|
278 fun rename_guard (AbstractMachine.Guard (a,b)) = |
|
279 AbstractMachine.Guard (rename 0 vars a, rename 0 vars b) |
|
280 in |
|
281 ((encoding, hyptable, shyptable), (map rename_guard prems, pattern, rename 0 vars right)) |
|
282 end |
|
283 |
|
284 val ((encoding, hyptable, shyptable), rules) = |
|
285 fold_rev (fn th => fn (encoding_hyptable, rules) => |
|
286 let |
|
287 val (encoding_hyptable, rule) = thm2rule encoding_hyptable th |
|
288 in (encoding_hyptable, rule::rules) end) |
|
289 ths ((encoding, Termtab.empty, Sorttab.empty), []) |
|
290 |
|
291 fun make_cache_pattern t (encoding, cache_patterns) = |
|
292 let |
|
293 val (encoding, a) = remove_types encoding t |
|
294 val (_,_,p) = make_pattern encoding 0 Inttab.empty a |
|
295 in |
|
296 (encoding, p::cache_patterns) |
|
297 end |
|
298 |
|
299 val (encoding, cache_patterns) = fold_rev make_cache_pattern cache_pattern_terms (encoding, []) |
|
300 |
|
301 fun arity (Type ("fun", [a,b])) = 1 + arity b |
|
302 | arity _ = 0 |
|
303 |
|
304 fun make_arity (Const (s, _), i) tab = |
|
305 (Inttab.update (i, arity (Sign.the_const_type thy s)) tab handle TYPE _ => tab) |
|
306 | make_arity _ tab = tab |
|
307 |
|
308 val const_arity_tab = Encode.fold make_arity encoding Inttab.empty |
|
309 fun const_arity x = Inttab.lookup const_arity_tab x |
|
310 |
|
311 val prog = |
|
312 case machine of |
|
313 BARRAS => ProgBarras (AM_Interpreter.compile cache_patterns const_arity rules) |
|
314 | BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile cache_patterns const_arity rules) |
|
315 | HASKELL => ProgHaskell (AM_GHC.compile cache_patterns const_arity rules) |
|
316 | SML => ProgSML (AM_SML.compile cache_patterns const_arity rules) |
|
317 |
|
318 fun has_witness s = not (null (Sign.witness_sorts thy [] [s])) |
|
319 |
|
320 val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable |
|
321 |
|
322 in (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog, stamp, default_naming) end |
|
323 |
|
324 fun make_with_cache machine thy cache_patterns raw_thms = |
|
325 Computer (Unsynchronized.ref (SOME (make_internal machine thy (Unsynchronized.ref ()) Encode.empty cache_patterns raw_thms))) |
|
326 |
|
327 fun make machine thy raw_thms = make_with_cache machine thy [] raw_thms |
|
328 |
|
329 fun update_with_cache computer cache_patterns raw_thms = |
|
330 let |
|
331 val c = make_internal (machine_of_prog (prog_of computer)) (theory_of computer) (stamp_of computer) |
|
332 (encoding_of computer) cache_patterns raw_thms |
|
333 val _ = (ref_of computer) := SOME c |
|
334 in |
|
335 () |
|
336 end |
|
337 |
|
338 fun update computer raw_thms = update_with_cache computer [] raw_thms |
|
339 |
|
340 fun discard computer = |
|
341 let |
|
342 val _ = |
|
343 case prog_of computer of |
|
344 ProgBarras p => AM_Interpreter.discard p |
|
345 | ProgBarrasC p => AM_Compiler.discard p |
|
346 | ProgHaskell p => AM_GHC.discard p |
|
347 | ProgSML p => AM_SML.discard p |
|
348 val _ = (ref_of computer) := NONE |
|
349 in |
|
350 () |
|
351 end |
|
352 |
|
353 fun runprog (ProgBarras p) = AM_Interpreter.run p |
|
354 | runprog (ProgBarrasC p) = AM_Compiler.run p |
|
355 | runprog (ProgHaskell p) = AM_GHC.run p |
|
356 | runprog (ProgSML p) = AM_SML.run p |
|
357 |
|
358 (* ------------------------------------------------------------------------------------- *) |
|
359 (* An oracle for exporting theorems; must only be accessible from inside this structure! *) |
|
360 (* ------------------------------------------------------------------------------------- *) |
|
361 |
|
362 fun merge_hyps hyps1 hyps2 = |
|
363 let |
|
364 fun add hyps tab = fold (fn h => fn tab => Termtab.update (h, ()) tab) hyps tab |
|
365 in |
|
366 Termtab.keys (add hyps2 (add hyps1 Termtab.empty)) |
|
367 end |
|
368 |
|
369 fun add_shyps shyps tab = fold (fn h => fn tab => Sorttab.update (h, ()) tab) shyps tab |
|
370 |
|
371 fun merge_shyps shyps1 shyps2 = Sorttab.keys (add_shyps shyps2 (add_shyps shyps1 Sorttab.empty)) |
|
372 |
|
373 val (_, export_oracle) = Context.>>> (Context.map_theory_result |
|
374 (Thm.add_oracle (Binding.name "compute", fn (thy, hyps, shyps, prop) => |
|
375 let |
|
376 val shyptab = add_shyps shyps Sorttab.empty |
|
377 fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab |
|
378 fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab |
|
379 fun has_witness s = not (null (Sign.witness_sorts thy [] [s])) |
|
380 val shyptab = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptab))) shyptab |
|
381 val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab) |
|
382 val _ = |
|
383 if not (null shyps) then |
|
384 raise Compute ("dangling sort hypotheses: " ^ |
|
385 commas (map (Syntax.string_of_sort_global thy) shyps)) |
|
386 else () |
|
387 in |
|
388 Thm.cterm_of thy (fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop) |
|
389 end))); |
|
390 |
|
391 fun export_thm thy hyps shyps prop = |
|
392 let |
|
393 val th = export_oracle (thy, hyps, shyps, prop) |
|
394 val hyps = map (fn h => Thm.assume (cterm_of thy h)) hyps |
|
395 in |
|
396 fold (fn h => fn p => Thm.implies_elim p h) hyps th |
|
397 end |
|
398 |
|
399 (* --------- Rewrite ----------- *) |
|
400 |
|
401 fun rewrite computer ct = |
|
402 let |
|
403 val thy = Thm.theory_of_cterm ct |
|
404 val {t=t',T=ty,...} = rep_cterm ct |
|
405 val _ = Theory.assert_super (theory_of computer) thy |
|
406 val naming = naming_of computer |
|
407 val (encoding, t) = remove_types (encoding_of computer) t' |
|
408 (*val _ = if (!print_encoding) then writeln (makestring ("encoding: ",Encode.fold (fn x => fn s => x::s) encoding [])) else ()*) |
|
409 val t = runprog (prog_of computer) t |
|
410 val t = infer_types naming encoding ty t |
|
411 val eq = Logic.mk_equals (t', t) |
|
412 in |
|
413 export_thm thy (hyps_of computer) (Sorttab.keys (shyptab_of computer)) eq |
|
414 end |
|
415 |
|
416 (* --------- Simplify ------------ *) |
|
417 |
|
418 datatype prem = EqPrem of AbstractMachine.term * AbstractMachine.term * Term.typ * int |
|
419 | Prem of AbstractMachine.term |
|
420 datatype theorem = Theorem of theory_ref * unit Unsynchronized.ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table |
|
421 * prem list * AbstractMachine.term * term list * sort list |
|
422 |
|
423 |
|
424 exception ParamSimplify of computer * theorem |
|
425 |
|
426 fun make_theorem computer th vars = |
|
427 let |
|
428 val _ = Theory.assert_super (theory_of computer) (theory_of_thm th) |
|
429 |
|
430 val (ComputeThm (hyps, shyps, prop)) = thm2cthm th |
|
431 |
|
432 val encoding = encoding_of computer |
|
433 |
|
434 (* variables in the theorem are identified upfront *) |
|
435 fun collect_vars (Abs (_, _, t)) tab = collect_vars t tab |
|
436 | collect_vars (a $ b) tab = collect_vars b (collect_vars a tab) |
|
437 | collect_vars (Const _) tab = tab |
|
438 | collect_vars (Free _) tab = tab |
|
439 | collect_vars (Var ((s, i), ty)) tab = |
|
440 if List.find (fn x => x=s) vars = NONE then |
|
441 tab |
|
442 else |
|
443 (case Symtab.lookup tab s of |
|
444 SOME ((s',i'),ty') => |
|
445 if s' <> s orelse i' <> i orelse ty <> ty' then |
|
446 raise Compute ("make_theorem: variable name '"^s^"' is not unique") |
|
447 else |
|
448 tab |
|
449 | NONE => Symtab.update (s, ((s, i), ty)) tab) |
|
450 val vartab = collect_vars prop Symtab.empty |
|
451 fun encodevar (s, t as (_, ty)) (encoding, tab) = |
|
452 let |
|
453 val (x, encoding) = Encode.insert (Var t) encoding |
|
454 in |
|
455 (encoding, Symtab.update (s, (x, ty)) tab) |
|
456 end |
|
457 val (encoding, vartab) = Symtab.fold encodevar vartab (encoding, Symtab.empty) |
|
458 val varsubst = Inttab.make (map (fn (s, (x, _)) => (x, NONE)) (Symtab.dest vartab)) |
|
459 |
|
460 (* make the premises and the conclusion *) |
|
461 fun mk_prem encoding t = |
|
462 (let |
|
463 val (a, b) = Logic.dest_equals t |
|
464 val ty = type_of a |
|
465 val (encoding, a) = remove_types encoding a |
|
466 val (encoding, b) = remove_types encoding b |
|
467 val (eq, encoding) = Encode.insert (Const ("==", ty --> ty --> @{typ "prop"})) encoding |
|
468 in |
|
469 (encoding, EqPrem (a, b, ty, eq)) |
|
470 end handle TERM _ => let val (encoding, t) = remove_types encoding t in (encoding, Prem t) end) |
|
471 val (encoding, prems) = |
|
472 (fold_rev (fn t => fn (encoding, l) => |
|
473 case mk_prem encoding t of |
|
474 (encoding, t) => (encoding, t::l)) (Logic.strip_imp_prems prop) (encoding, [])) |
|
475 val (encoding, concl) = remove_types encoding (Logic.strip_imp_concl prop) |
|
476 val _ = set_encoding computer encoding |
|
477 in |
|
478 Theorem (Theory.check_thy (theory_of_thm th), stamp_of computer, vartab, varsubst, |
|
479 prems, concl, hyps, shyps) |
|
480 end |
|
481 |
|
482 fun theory_of_theorem (Theorem (rthy,_,_,_,_,_,_,_)) = Theory.deref rthy |
|
483 fun update_theory thy (Theorem (_,p0,p1,p2,p3,p4,p5,p6)) = |
|
484 Theorem (Theory.check_thy thy,p0,p1,p2,p3,p4,p5,p6) |
|
485 fun stamp_of_theorem (Theorem (_,s, _, _, _, _, _, _)) = s |
|
486 fun vartab_of_theorem (Theorem (_,_,vt,_,_,_,_,_)) = vt |
|
487 fun varsubst_of_theorem (Theorem (_,_,_,vs,_,_,_,_)) = vs |
|
488 fun update_varsubst vs (Theorem (p0,p1,p2,_,p3,p4,p5,p6)) = Theorem (p0,p1,p2,vs,p3,p4,p5,p6) |
|
489 fun prems_of_theorem (Theorem (_,_,_,_,prems,_,_,_)) = prems |
|
490 fun update_prems prems (Theorem (p0,p1,p2,p3,_,p4,p5,p6)) = Theorem (p0,p1,p2,p3,prems,p4,p5,p6) |
|
491 fun concl_of_theorem (Theorem (_,_,_,_,_,concl,_,_)) = concl |
|
492 fun hyps_of_theorem (Theorem (_,_,_,_,_,_,hyps,_)) = hyps |
|
493 fun update_hyps hyps (Theorem (p0,p1,p2,p3,p4,p5,_,p6)) = Theorem (p0,p1,p2,p3,p4,p5,hyps,p6) |
|
494 fun shyps_of_theorem (Theorem (_,_,_,_,_,_,_,shyps)) = shyps |
|
495 fun update_shyps shyps (Theorem (p0,p1,p2,p3,p4,p5,p6,_)) = Theorem (p0,p1,p2,p3,p4,p5,p6,shyps) |
|
496 |
|
497 fun check_compatible computer th s = |
|
498 if stamp_of computer <> stamp_of_theorem th then |
|
499 raise Compute (s^": computer and theorem are incompatible") |
|
500 else () |
|
501 |
|
502 fun instantiate computer insts th = |
|
503 let |
|
504 val _ = check_compatible computer th |
|
505 |
|
506 val thy = theory_of computer |
|
507 |
|
508 val vartab = vartab_of_theorem th |
|
509 |
|
510 fun rewrite computer t = |
|
511 let |
|
512 val naming = naming_of computer |
|
513 val (encoding, t) = remove_types (encoding_of computer) t |
|
514 val t = runprog (prog_of computer) t |
|
515 val _ = set_encoding computer encoding |
|
516 in |
|
517 t |
|
518 end |
|
519 |
|
520 fun assert_varfree vs t = |
|
521 if AbstractMachine.forall_consts (fn x => Inttab.lookup vs x = NONE) t then |
|
522 () |
|
523 else |
|
524 raise Compute "instantiate: assert_varfree failed" |
|
525 |
|
526 fun assert_closed t = |
|
527 if AbstractMachine.closed t then |
|
528 () |
|
529 else |
|
530 raise Compute "instantiate: not a closed term" |
|
531 |
|
532 fun compute_inst (s, ct) vs = |
|
533 let |
|
534 val _ = Theory.assert_super (theory_of_cterm ct) thy |
|
535 val ty = typ_of (ctyp_of_term ct) |
|
536 in |
|
537 (case Symtab.lookup vartab s of |
|
538 NONE => raise Compute ("instantiate: variable '"^s^"' not found in theorem") |
|
539 | SOME (x, ty') => |
|
540 (case Inttab.lookup vs x of |
|
541 SOME (SOME _) => raise Compute ("instantiate: variable '"^s^"' has already been instantiated") |
|
542 | SOME NONE => |
|
543 if ty <> ty' then |
|
544 raise Compute ("instantiate: wrong type for variable '"^s^"'") |
|
545 else |
|
546 let |
|
547 val t = rewrite computer (term_of ct) |
|
548 val _ = assert_varfree vs t |
|
549 val _ = assert_closed t |
|
550 in |
|
551 Inttab.update (x, SOME t) vs |
|
552 end |
|
553 | NONE => raise Compute "instantiate: internal error")) |
|
554 end |
|
555 |
|
556 val vs = fold compute_inst insts (varsubst_of_theorem th) |
|
557 in |
|
558 update_varsubst vs th |
|
559 end |
|
560 |
|
561 fun match_aterms subst = |
|
562 let |
|
563 exception no_match |
|
564 open AbstractMachine |
|
565 fun match subst (b as (Const c)) a = |
|
566 if a = b then subst |
|
567 else |
|
568 (case Inttab.lookup subst c of |
|
569 SOME (SOME a') => if a=a' then subst else raise no_match |
|
570 | SOME NONE => if AbstractMachine.closed a then |
|
571 Inttab.update (c, SOME a) subst |
|
572 else raise no_match |
|
573 | NONE => raise no_match) |
|
574 | match subst (b as (Var _)) a = if a=b then subst else raise no_match |
|
575 | match subst (App (u, v)) (App (u', v')) = match (match subst u u') v v' |
|
576 | match subst (Abs u) (Abs u') = match subst u u' |
|
577 | match subst _ _ = raise no_match |
|
578 in |
|
579 fn b => fn a => (SOME (match subst b a) handle no_match => NONE) |
|
580 end |
|
581 |
|
582 fun apply_subst vars_allowed subst = |
|
583 let |
|
584 open AbstractMachine |
|
585 fun app (t as (Const c)) = |
|
586 (case Inttab.lookup subst c of |
|
587 NONE => t |
|
588 | SOME (SOME t) => Computed t |
|
589 | SOME NONE => if vars_allowed then t else raise Compute "apply_subst: no vars allowed") |
|
590 | app (t as (Var _)) = t |
|
591 | app (App (u, v)) = App (app u, app v) |
|
592 | app (Abs m) = Abs (app m) |
|
593 in |
|
594 app |
|
595 end |
|
596 |
|
597 fun splicein n l L = List.take (L, n) @ l @ List.drop (L, n+1) |
|
598 |
|
599 fun evaluate_prem computer prem_no th = |
|
600 let |
|
601 val _ = check_compatible computer th |
|
602 val prems = prems_of_theorem th |
|
603 val varsubst = varsubst_of_theorem th |
|
604 fun run vars_allowed t = |
|
605 runprog (prog_of computer) (apply_subst vars_allowed varsubst t) |
|
606 in |
|
607 case List.nth (prems, prem_no) of |
|
608 Prem _ => raise Compute "evaluate_prem: no equality premise" |
|
609 | EqPrem (a, b, ty, _) => |
|
610 let |
|
611 val a' = run false a |
|
612 val b' = run true b |
|
613 in |
|
614 case match_aterms varsubst b' a' of |
|
615 NONE => |
|
616 let |
|
617 fun mk s = Syntax.string_of_term_global Pure.thy |
|
618 (infer_types (naming_of computer) (encoding_of computer) ty s) |
|
619 val left = "computed left side: "^(mk a') |
|
620 val right = "computed right side: "^(mk b') |
|
621 in |
|
622 raise Compute ("evaluate_prem: cannot assign computed left to right hand side\n"^left^"\n"^right^"\n") |
|
623 end |
|
624 | SOME varsubst => |
|
625 update_prems (splicein prem_no [] prems) (update_varsubst varsubst th) |
|
626 end |
|
627 end |
|
628 |
|
629 fun prem2term (Prem t) = t |
|
630 | prem2term (EqPrem (a,b,_,eq)) = |
|
631 AbstractMachine.App (AbstractMachine.App (AbstractMachine.Const eq, a), b) |
|
632 |
|
633 fun modus_ponens computer prem_no th' th = |
|
634 let |
|
635 val _ = check_compatible computer th |
|
636 val thy = |
|
637 let |
|
638 val thy1 = theory_of_theorem th |
|
639 val thy2 = theory_of_thm th' |
|
640 in |
|
641 if Theory.subthy (thy1, thy2) then thy2 |
|
642 else if Theory.subthy (thy2, thy1) then thy1 else |
|
643 raise Compute "modus_ponens: theorems are not compatible with each other" |
|
644 end |
|
645 val th' = make_theorem computer th' [] |
|
646 val varsubst = varsubst_of_theorem th |
|
647 fun run vars_allowed t = |
|
648 runprog (prog_of computer) (apply_subst vars_allowed varsubst t) |
|
649 val prems = prems_of_theorem th |
|
650 val prem = run true (prem2term (List.nth (prems, prem_no))) |
|
651 val concl = run false (concl_of_theorem th') |
|
652 in |
|
653 case match_aterms varsubst prem concl of |
|
654 NONE => raise Compute "modus_ponens: conclusion does not match premise" |
|
655 | SOME varsubst => |
|
656 let |
|
657 val th = update_varsubst varsubst th |
|
658 val th = update_prems (splicein prem_no (prems_of_theorem th') prems) th |
|
659 val th = update_hyps (merge_hyps (hyps_of_theorem th) (hyps_of_theorem th')) th |
|
660 val th = update_shyps (merge_shyps (shyps_of_theorem th) (shyps_of_theorem th')) th |
|
661 in |
|
662 update_theory thy th |
|
663 end |
|
664 end |
|
665 |
|
666 fun simplify computer th = |
|
667 let |
|
668 val _ = check_compatible computer th |
|
669 val varsubst = varsubst_of_theorem th |
|
670 val encoding = encoding_of computer |
|
671 val naming = naming_of computer |
|
672 fun infer t = infer_types naming encoding @{typ "prop"} t |
|
673 fun run t = infer (runprog (prog_of computer) (apply_subst true varsubst t)) |
|
674 fun runprem p = run (prem2term p) |
|
675 val prop = Logic.list_implies (map runprem (prems_of_theorem th), run (concl_of_theorem th)) |
|
676 val hyps = merge_hyps (hyps_of computer) (hyps_of_theorem th) |
|
677 val shyps = merge_shyps (shyps_of_theorem th) (Sorttab.keys (shyptab_of computer)) |
|
678 in |
|
679 export_thm (theory_of_theorem th) hyps shyps prop |
|
680 end |
|
681 |
|
682 end |
|
683 |
|