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