author | wenzelm |
Tue, 29 Sep 2009 16:24:36 +0200 | |
changeset 32740 | 9dd0a2f83429 |
parent 31976 | 17414e2736f4 |
child 36945 | 9bec62c10714 |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: Tools/Compute_Oracle/compute.ML |
23174 | 2 |
Author: Steven Obua |
3 |
*) |
|
4 |
||
5 |
signature COMPUTE = sig |
|
6 |
||
7 |
type computer |
|
25217 | 8 |
type theorem |
9 |
type naming = int -> string |
|
23174 | 10 |
|
23663 | 11 |
datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML |
23174 | 12 |
|
25217 | 13 |
(* Functions designated with a ! in front of them actually update the computer parameter *) |
14 |
||
23663 | 15 |
exception Make of string |
16 |
val make : machine -> theory -> thm list -> computer |
|
25520 | 17 |
val make_with_cache : machine -> theory -> term list -> 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 |
25520 | 22 |
(* ! *) val update_with_cache : computer -> term list -> thm list -> unit |
25217 | 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 |
|
23663 | 31 |
|
25217 | 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 |
|
23663 | 36 |
|
23174 | 37 |
end |
38 |
||
23663 | 39 |
structure Compute :> COMPUTE = struct |
40 |
||
25217 | 41 |
open Report; |
24654 | 42 |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
43 |
datatype machine = BARRAS | BARRAS_COMPILED | HASKELL | SML |
23663 | 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 |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
52 |
val lookup_term : int -> encoding -> term option |
23663 | 53 |
val remove_code : int -> encoding -> encoding |
54 |
val remove_term : term -> encoding -> encoding |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
55 |
val fold : ((term * int) -> 'a -> 'a) -> encoding -> 'a -> 'a |
23663 | 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 |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
66 |
NONE => (count, (count+1, Termtab.update_new (t, count) term2int, Inttab.update_new (count, t) int2term)) |
23663 | 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 |
||
25520 | 79 |
fun fold f (_, term2int, _) = Termtab.fold f term2int |
23663 | 80 |
|
81 |
end |
|
82 |
||
23174 | 83 |
exception Make of string; |
23663 | 84 |
exception Compute of string; |
23174 | 85 |
|
23663 | 86 |
local |
87 |
fun make_constant t ty encoding = |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
88 |
let |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
89 |
val (code, encoding) = Encode.insert t encoding |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
90 |
in |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
91 |
(encoding, AbstractMachine.Const code) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
92 |
end |
23663 | 93 |
in |
23174 | 94 |
|
23663 | 95 |
fun remove_types encoding t = |
96 |
case t of |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
97 |
Var (_, ty) => make_constant t ty encoding |
23663 | 98 |
| Free (_, ty) => make_constant t ty encoding |
99 |
| Const (_, ty) => make_constant t ty encoding |
|
100 |
| Abs (_, ty, t') => |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
101 |
let val (encoding, t'') = remove_types encoding t' in |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
102 |
(encoding, AbstractMachine.Abs t'') |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
103 |
end |
23663 | 104 |
| a $ b => |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
105 |
let |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
106 |
val (encoding, a) = remove_types encoding a |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
107 |
val (encoding, b) = remove_types encoding b |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
108 |
in |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
109 |
(encoding, AbstractMachine.App (a,b)) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
110 |
end |
23663 | 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 = |
|
23174 | 121 |
let |
23663 | 122 |
fun infer_types _ bounds _ (AbstractMachine.Var v) = (Bound v, List.nth (bounds, v)) |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
123 |
| infer_types _ bounds _ (AbstractMachine.Const code) = |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
124 |
let |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
125 |
val c = the (Encode.lookup_term code encoding) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
126 |
in |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
127 |
(c, type_of c) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
128 |
end |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
129 |
| infer_types level bounds _ (AbstractMachine.App (a, b)) = |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
130 |
let |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
131 |
val (a, aty) = infer_types level bounds NONE a |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
132 |
val (adom, arange) = |
23174 | 133 |
case aty of |
134 |
Type ("fun", [dom, range]) => (dom, range) |
|
135 |
| _ => sys_error "infer_types: function type expected" |
|
23663 | 136 |
val (b, bty) = infer_types level bounds (SOME adom) b |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
137 |
in |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
138 |
(a $ b, arange) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
139 |
end |
23663 | 140 |
| infer_types level bounds (SOME (ty as Type ("fun", [dom, range]))) (AbstractMachine.Abs m) = |
23174 | 141 |
let |
23663 | 142 |
val (m, _) = infer_types (level+1) (dom::bounds) (SOME range) m |
23174 | 143 |
in |
23663 | 144 |
(Abs (naming level, dom, m), ty) |
23174 | 145 |
end |
23663 | 146 |
| infer_types _ _ NONE (AbstractMachine.Abs m) = sys_error "infer_types: cannot infer type of abstraction" |
23174 | 147 |
|
23663 | 148 |
fun infer ty term = |
23174 | 149 |
let |
23663 | 150 |
val (term', _) = infer_types 0 [] (SOME ty) term |
23174 | 151 |
in |
152 |
term' |
|
153 |
end |
|
154 |
in |
|
155 |
infer |
|
156 |
end |
|
23663 | 157 |
end |
23174 | 158 |
|
23663 | 159 |
datatype prog = |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
160 |
ProgBarras of AM_Interpreter.program |
23663 | 161 |
| ProgBarrasC of AM_Compiler.program |
162 |
| ProgHaskell of AM_GHC.program |
|
163 |
| ProgSML of AM_SML.program |
|
23174 | 164 |
|
25217 | 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 |
||
32740 | 174 |
datatype computer = Computer of |
175 |
(theory_ref * Encode.encoding * term list * unit Sorttab.table * prog * unit Unsynchronized.ref * naming) |
|
176 |
option Unsynchronized.ref |
|
25217 | 177 |
|
32740 | 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' = |
|
25217 | 186 |
(r := SOME (p1,encoding',p2,p3,p4,p5,p6)) |
32740 | 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'= |
|
25217 | 189 |
(r := SOME (p1,p2,p3,p4,p5,p6,naming')) |
190 |
||
191 |
fun ref_of (Computer r) = r |
|
23663 | 192 |
|
193 |
datatype cthm = ComputeThm of term list * sort list * term |
|
194 |
||
195 |
fun thm2cthm th = |
|
23174 | 196 |
let |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
197 |
val {hyps, prop, tpairs, shyps, ...} = Thm.rep_thm th |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
198 |
val _ = if not (null tpairs) then raise Make "theorems may not contain tpairs" else () |
23663 | 199 |
in |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
200 |
ComputeThm (hyps, shyps, prop) |
23663 | 201 |
end |
23174 | 202 |
|
25520 | 203 |
fun make_internal machine thy stamp encoding cache_pattern_terms raw_ths = |
23663 | 204 |
let |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
205 |
fun transfer (x:thm) = Thm.transfer thy x |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
206 |
val ths = map (thm2cthm o Thm.strip_shyps o transfer) raw_ths |
23174 | 207 |
|
25520 | 208 |
fun make_pattern encoding n vars (var as AbstractMachine.Abs _) = |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
209 |
raise (Make "no lambda abstractions allowed in pattern") |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
210 |
| make_pattern encoding n vars (var as AbstractMachine.Var _) = |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
211 |
raise (Make "no bound variables allowed in pattern") |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
212 |
| make_pattern encoding n vars (AbstractMachine.Const code) = |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
213 |
(case the (Encode.lookup_term code encoding) of |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
214 |
Var _ => ((n+1, Inttab.update_new (code, n) vars, AbstractMachine.PVar) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
215 |
handle Inttab.DUP _ => raise (Make "no duplicate variable in pattern allowed")) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
216 |
| _ => (n, vars, AbstractMachine.PConst (code, []))) |
25520 | 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 |
||
23663 | 229 |
fun thm2rule (encoding, hyptable, shyptable) th = |
230 |
let |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
231 |
val (ComputeThm (hyps, shyps, prop)) = th |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
232 |
val hyptable = fold (fn h => Termtab.update (h, ())) hyps hyptable |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
233 |
val shyptable = fold (fn sh => Sorttab.update (sh, ())) shyps shyptable |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
234 |
val (prems, prop) = (Logic.strip_imp_prems prop, Logic.strip_imp_concl prop) |
23663 | 235 |
val (a, b) = Logic.dest_equals prop |
236 |
handle TERM _ => raise (Make "theorems must be meta-level equations (with optional guards)") |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
237 |
val a = Envir.eta_contract a |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
238 |
val b = Envir.eta_contract b |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
239 |
val prems = map Envir.eta_contract prems |
23174 | 240 |
|
23663 | 241 |
val (encoding, left) = remove_types encoding a |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
242 |
val (encoding, right) = remove_types encoding b |
23663 | 243 |
fun remove_types_of_guard encoding g = |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
244 |
(let |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
245 |
val (t1, t2) = Logic.dest_equals g |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
246 |
val (encoding, t1) = remove_types encoding t1 |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
247 |
val (encoding, t2) = remove_types encoding t2 |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
248 |
in |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
249 |
(encoding, AbstractMachine.Guard (t1, t2)) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
250 |
end handle TERM _ => raise (Make "guards must be meta-level equations")) |
23663 | 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, []) |
23174 | 252 |
|
23663 | 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 |
|
23174 | 258 |
val _ = (case pattern of |
23663 | 259 |
AbstractMachine.PVar => |
23174 | 260 |
raise (Make "patterns may not start with a variable") |
23663 | 261 |
(* | AbstractMachine.PConst (_, []) => |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
262 |
(print th; raise (Make "no parameter rewrite found"))*) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
263 |
| _ => ()) |
23174 | 264 |
|
265 |
(* finally, provide a function for renaming the |
|
23663 | 266 |
pattern bound variables on the right hand side *) |
23174 | 267 |
|
23663 | 268 |
fun rename level vars (var as AbstractMachine.Var _) = var |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
269 |
| rename level vars (c as AbstractMachine.Const code) = |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
270 |
(case Inttab.lookup vars code of |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
271 |
NONE => c |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
272 |
| SOME n => AbstractMachine.Var (vcount-n-1+level)) |
23663 | 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) |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
277 |
|
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
278 |
fun rename_guard (AbstractMachine.Guard (a,b)) = |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
279 |
AbstractMachine.Guard (rename 0 vars a, rename 0 vars b) |
23174 | 280 |
in |
23663 | 281 |
((encoding, hyptable, shyptable), (map rename_guard prems, pattern, rename 0 vars right)) |
23174 | 282 |
end |
283 |
||
23663 | 284 |
val ((encoding, hyptable, shyptable), rules) = |
285 |
fold_rev (fn th => fn (encoding_hyptable, rules) => |
|
23174 | 286 |
let |
23663 | 287 |
val (encoding_hyptable, rule) = thm2rule encoding_hyptable th |
288 |
in (encoding_hyptable, rule::rules) end) |
|
25217 | 289 |
ths ((encoding, Termtab.empty, Sorttab.empty), []) |
23174 | 290 |
|
25520 | 291 |
fun make_cache_pattern t (encoding, cache_patterns) = |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
292 |
let |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
293 |
val (encoding, a) = remove_types encoding t |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
294 |
val (_,_,p) = make_pattern encoding 0 Inttab.empty a |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
295 |
in |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
296 |
(encoding, p::cache_patterns) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
297 |
end |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
298 |
|
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
299 |
val (encoding, cache_patterns) = fold_rev make_cache_pattern cache_pattern_terms (encoding, []) |
25520 | 300 |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
301 |
fun arity (Type ("fun", [a,b])) = 1 + arity b |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
302 |
| arity _ = 0 |
25520 | 303 |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
304 |
fun make_arity (Const (s, _), i) tab = |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
305 |
(Inttab.update (i, arity (Sign.the_const_type thy s)) tab handle TYPE _ => tab) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
306 |
| make_arity _ tab = tab |
25520 | 307 |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
308 |
val const_arity_tab = Encode.fold make_arity encoding Inttab.empty |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
309 |
fun const_arity x = Inttab.lookup const_arity_tab x |
25520 | 310 |
|
23663 | 311 |
val prog = |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
312 |
case machine of |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
313 |
BARRAS => ProgBarras (AM_Interpreter.compile cache_patterns const_arity rules) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
314 |
| BARRAS_COMPILED => ProgBarrasC (AM_Compiler.compile cache_patterns const_arity rules) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
315 |
| HASKELL => ProgHaskell (AM_GHC.compile cache_patterns const_arity rules) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
316 |
| SML => ProgSML (AM_SML.compile cache_patterns const_arity rules) |
23174 | 317 |
|
23663 | 318 |
fun has_witness s = not (null (Sign.witness_sorts thy [] [s])) |
23174 | 319 |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
320 |
val shyptable = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptable))) shyptable |
23663 | 321 |
|
25217 | 322 |
in (Theory.check_thy thy, encoding, Termtab.keys hyptable, shyptable, prog, stamp, default_naming) end |
323 |
||
32740 | 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))) |
|
23663 | 326 |
|
25520 | 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 = |
|
25217 | 330 |
let |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
331 |
val c = make_internal (machine_of_prog (prog_of computer)) (theory_of computer) (stamp_of computer) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
332 |
(encoding_of computer) cache_patterns raw_thms |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
333 |
val _ = (ref_of computer) := SOME c |
25217 | 334 |
in |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
335 |
() |
25217 | 336 |
end |
337 |
||
25520 | 338 |
fun update computer raw_thms = update_with_cache computer [] raw_thms |
339 |
||
25217 | 340 |
fun discard computer = |
23174 | 341 |
let |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
342 |
val _ = |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
343 |
case prog_of computer of |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
344 |
ProgBarras p => AM_Interpreter.discard p |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
345 |
| ProgBarrasC p => AM_Compiler.discard p |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
346 |
| ProgHaskell p => AM_GHC.discard p |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
347 |
| ProgSML p => AM_SML.discard p |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
348 |
val _ = (ref_of computer) := NONE |
23174 | 349 |
in |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
350 |
() |
25217 | 351 |
end |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
352 |
|
25217 | 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 |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
356 |
| runprog (ProgSML p) = AM_SML.run p |
25217 | 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 |
||
28290 | 373 |
val (_, export_oracle) = Context.>>> (Context.map_theory_result |
30288
a32700e45ab3
Thm.add_oracle interface: replaced old bstring by binding;
wenzelm
parents:
29269
diff
changeset
|
374 |
(Thm.add_oracle (Binding.name "compute", fn (thy, hyps, shyps, prop) => |
25217 | 375 |
let |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
376 |
val shyptab = add_shyps shyps Sorttab.empty |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
377 |
fun delete s shyptab = Sorttab.delete s shyptab handle Sorttab.UNDEF _ => shyptab |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
378 |
fun delete_term t shyptab = fold delete (Sorts.insert_term t []) shyptab |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
379 |
fun has_witness s = not (null (Sign.witness_sorts thy [] [s])) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
380 |
val shyptab = fold Sorttab.delete (filter has_witness (Sorttab.keys (shyptab))) shyptab |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
381 |
val shyps = if Sorttab.is_empty shyptab then [] else Sorttab.keys (fold delete_term (prop::hyps) shyptab) |
31322
526e149999cc
attempt to eliminate adhoc makestring at runtime (which is not well-defined);
wenzelm
parents:
30288
diff
changeset
|
382 |
val _ = |
526e149999cc
attempt to eliminate adhoc makestring at runtime (which is not well-defined);
wenzelm
parents:
30288
diff
changeset
|
383 |
if not (null shyps) then |
526e149999cc
attempt to eliminate adhoc makestring at runtime (which is not well-defined);
wenzelm
parents:
30288
diff
changeset
|
384 |
raise Compute ("dangling sort hypotheses: " ^ |
526e149999cc
attempt to eliminate adhoc makestring at runtime (which is not well-defined);
wenzelm
parents:
30288
diff
changeset
|
385 |
commas (map (Syntax.string_of_sort_global thy) shyps)) |
526e149999cc
attempt to eliminate adhoc makestring at runtime (which is not well-defined);
wenzelm
parents:
30288
diff
changeset
|
386 |
else () |
25217 | 387 |
in |
28290 | 388 |
Thm.cterm_of thy (fold_rev (fn hyp => fn p => Logic.mk_implies (hyp, p)) hyps prop) |
389 |
end))); |
|
25217 | 390 |
|
391 |
fun export_thm thy hyps shyps prop = |
|
392 |
let |
|
28290 | 393 |
val th = export_oracle (thy, hyps, shyps, prop) |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
394 |
val hyps = map (fn h => assume (cterm_of thy h)) hyps |
25217 | 395 |
in |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
396 |
fold (fn h => fn p => implies_elim p h) hyps th |
25217 | 397 |
end |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
398 |
|
25217 | 399 |
(* --------- Rewrite ----------- *) |
400 |
||
401 |
fun rewrite computer ct = |
|
402 |
let |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
403 |
val thy = Thm.theory_of_cterm ct |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
404 |
val {t=t',T=ty,...} = rep_cterm ct |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
405 |
val _ = Theory.assert_super (theory_of computer) thy |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
406 |
val naming = naming_of computer |
25217 | 407 |
val (encoding, t) = remove_types (encoding_of computer) t' |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
408 |
(*val _ = if (!print_encoding) then writeln (makestring ("encoding: ",Encode.fold (fn x => fn s => x::s) encoding [])) else ()*) |
25217 | 409 |
val t = runprog (prog_of computer) t |
410 |
val t = infer_types naming encoding ty t |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
411 |
val eq = Logic.mk_equals (t', t) |
25217 | 412 |
in |
413 |
export_thm thy (hyps_of computer) (Sorttab.keys (shyptab_of computer)) eq |
|
414 |
end |
|
415 |
||
416 |
(* --------- Simplify ------------ *) |
|
23663 | 417 |
|
25217 | 418 |
datatype prem = EqPrem of AbstractMachine.term * AbstractMachine.term * Term.typ * int |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
419 |
| Prem of AbstractMachine.term |
32740 | 420 |
datatype theorem = Theorem of theory_ref * unit Unsynchronized.ref * (int * typ) Symtab.table * (AbstractMachine.term option) Inttab.table |
25217 | 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 = |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
440 |
if List.find (fn x => x=s) vars = NONE then |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
441 |
tab |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
442 |
else |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
443 |
(case Symtab.lookup tab s of |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
444 |
SOME ((s',i'),ty') => |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
445 |
if s' <> s orelse i' <> i orelse ty <> ty' then |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
446 |
raise Compute ("make_theorem: variable name '"^s^"' is not unique") |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
447 |
else |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
448 |
tab |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
449 |
| NONE => Symtab.update (s, ((s, i), ty)) tab) |
25217 | 450 |
val vartab = collect_vars prop Symtab.empty |
451 |
fun encodevar (s, t as (_, ty)) (encoding, tab) = |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
452 |
let |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
453 |
val (x, encoding) = Encode.insert (Var t) encoding |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
454 |
in |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
455 |
(encoding, Symtab.update (s, (x, ty)) tab) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
456 |
end |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
457 |
val (encoding, vartab) = Symtab.fold encodevar vartab (encoding, Symtab.empty) |
25217 | 458 |
val varsubst = Inttab.make (map (fn (s, (x, _)) => (x, NONE)) (Symtab.dest vartab)) |
23174 | 459 |
|
25217 | 460 |
(* make the premises and the conclusion *) |
461 |
fun mk_prem encoding t = |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
462 |
(let |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
463 |
val (a, b) = Logic.dest_equals t |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
464 |
val ty = type_of a |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
465 |
val (encoding, a) = remove_types encoding a |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
466 |
val (encoding, b) = remove_types encoding b |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
467 |
val (eq, encoding) = Encode.insert (Const ("==", ty --> ty --> @{typ "prop"})) encoding |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
468 |
in |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
469 |
(encoding, EqPrem (a, b, ty, eq)) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
470 |
end handle TERM _ => let val (encoding, t) = remove_types encoding t in (encoding, Prem t) end) |
25217 | 471 |
val (encoding, prems) = |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
472 |
(fold_rev (fn t => fn (encoding, l) => |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
473 |
case mk_prem encoding t of |
25217 | 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, |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
479 |
prems, concl, hyps, shyps) |
25217 | 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 |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
499 |
raise Compute (s^": computer and theorem are incompatible") |
25217 | 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 |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
512 |
val naming = naming_of computer |
25217 | 513 |
val (encoding, t) = remove_types (encoding_of computer) t |
514 |
val t = runprog (prog_of computer) t |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
515 |
val _ = set_encoding computer encoding |
23174 | 516 |
in |
517 |
t |
|
518 |
end |
|
519 |
||
25217 | 520 |
fun assert_varfree vs t = |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
521 |
if AbstractMachine.forall_consts (fn x => Inttab.lookup vs x = NONE) t then |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
522 |
() |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
523 |
else |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
524 |
raise Compute "instantiate: assert_varfree failed" |
25217 | 525 |
|
526 |
fun assert_closed t = |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
527 |
if AbstractMachine.closed t then |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
528 |
() |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
529 |
else |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
530 |
raise Compute "instantiate: not a closed term" |
23663 | 531 |
|
25217 | 532 |
fun compute_inst (s, ct) vs = |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
533 |
let |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
534 |
val _ = Theory.assert_super (theory_of_cterm ct) thy |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
535 |
val ty = typ_of (ctyp_of_term ct) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
536 |
in |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
537 |
(case Symtab.lookup vartab s of |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
538 |
NONE => raise Compute ("instantiate: variable '"^s^"' not found in theorem") |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
539 |
| SOME (x, ty') => |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
540 |
(case Inttab.lookup vs x of |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
541 |
SOME (SOME _) => raise Compute ("instantiate: variable '"^s^"' has already been instantiated") |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
542 |
| SOME NONE => |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
543 |
if ty <> ty' then |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
544 |
raise Compute ("instantiate: wrong type for variable '"^s^"'") |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
545 |
else |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
546 |
let |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
547 |
val t = rewrite computer (term_of ct) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
548 |
val _ = assert_varfree vs t |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
549 |
val _ = assert_closed t |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
550 |
in |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
551 |
Inttab.update (x, SOME t) vs |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
552 |
end |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
553 |
| NONE => raise Compute "instantiate: internal error")) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
554 |
end |
23174 | 555 |
|
25217 | 556 |
val vs = fold compute_inst insts (varsubst_of_theorem th) |
557 |
in |
|
558 |
update_varsubst vs th |
|
559 |
end |
|
23174 | 560 |
|
25217 | 561 |
fun match_aterms subst = |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
562 |
let |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
563 |
exception no_match |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
564 |
open AbstractMachine |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
565 |
fun match subst (b as (Const c)) a = |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
566 |
if a = b then subst |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
567 |
else |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
568 |
(case Inttab.lookup subst c of |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
569 |
SOME (SOME a') => if a=a' then subst else raise no_match |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
570 |
| SOME NONE => if AbstractMachine.closed a then |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
571 |
Inttab.update (c, SOME a) subst |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
572 |
else raise no_match |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
573 |
| NONE => raise no_match) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
574 |
| match subst (b as (Var _)) a = if a=b then subst else raise no_match |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
575 |
| match subst (App (u, v)) (App (u', v')) = match (match subst u u') v v' |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
576 |
| match subst (Abs u) (Abs u') = match subst u u' |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
577 |
| match subst _ _ = raise no_match |
23663 | 578 |
in |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
579 |
fn b => fn a => (SOME (match subst b a) handle no_match => NONE) |
25217 | 580 |
end |
581 |
||
582 |
fun apply_subst vars_allowed subst = |
|
583 |
let |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
584 |
open AbstractMachine |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
585 |
fun app (t as (Const c)) = |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
586 |
(case Inttab.lookup subst c of |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
587 |
NONE => t |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
588 |
| SOME (SOME t) => Computed t |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
589 |
| SOME NONE => if vars_allowed then t else raise Compute "apply_subst: no vars allowed") |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
590 |
| app (t as (Var _)) = t |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
591 |
| app (App (u, v)) = App (app u, app v) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
592 |
| app (Abs m) = Abs (app m) |
25217 | 593 |
in |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
594 |
app |
23663 | 595 |
end |
596 |
||
25217 | 597 |
fun splicein n l L = List.take (L, n) @ l @ List.drop (L, n+1) |
23663 | 598 |
|
25217 | 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 = |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
605 |
runprog (prog_of computer) (apply_subst vars_allowed varsubst t) |
25217 | 606 |
in |
607 |
case List.nth (prems, prem_no) of |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
608 |
Prem _ => raise Compute "evaluate_prem: no equality premise" |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
609 |
| EqPrem (a, b, ty, _) => |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
610 |
let |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
611 |
val a' = run false a |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
612 |
val b' = run true b |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
613 |
in |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
614 |
case match_aterms varsubst b' a' of |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
615 |
NONE => |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
616 |
let |
31322
526e149999cc
attempt to eliminate adhoc makestring at runtime (which is not well-defined);
wenzelm
parents:
30288
diff
changeset
|
617 |
fun mk s = Syntax.string_of_term_global Pure.thy |
526e149999cc
attempt to eliminate adhoc makestring at runtime (which is not well-defined);
wenzelm
parents:
30288
diff
changeset
|
618 |
(infer_types (naming_of computer) (encoding_of computer) ty s) |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
619 |
val left = "computed left side: "^(mk a') |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
620 |
val right = "computed right side: "^(mk b') |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
621 |
in |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
622 |
raise Compute ("evaluate_prem: cannot assign computed left to right hand side\n"^left^"\n"^right^"\n") |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
623 |
end |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
624 |
| SOME varsubst => |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
625 |
update_prems (splicein prem_no [] prems) (update_varsubst varsubst th) |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
626 |
end |
25217 | 627 |
end |
23663 | 628 |
|
25217 | 629 |
fun prem2term (Prem t) = t |
630 |
| prem2term (EqPrem (a,b,_,eq)) = |
|
631 |
AbstractMachine.App (AbstractMachine.App (AbstractMachine.Const eq, a), b) |
|
23663 | 632 |
|
25217 | 633 |
fun modus_ponens computer prem_no th' th = |
634 |
let |
|
635 |
val _ = check_compatible computer th |
|
636 |
val thy = |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
637 |
let |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
638 |
val thy1 = theory_of_theorem th |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
639 |
val thy2 = theory_of_thm th' |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
640 |
in |
26674 | 641 |
if Theory.subthy (thy1, thy2) then thy2 |
642 |
else if Theory.subthy (thy2, thy1) then thy1 else |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
643 |
raise Compute "modus_ponens: theorems are not compatible with each other" |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
644 |
end |
25217 | 645 |
val th' = make_theorem computer th' [] |
646 |
val varsubst = varsubst_of_theorem th |
|
647 |
fun run vars_allowed t = |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
648 |
runprog (prog_of computer) (apply_subst vars_allowed varsubst t) |
25217 | 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 |
|
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
654 |
NONE => raise Compute "modus_ponens: conclusion does not match premise" |
25217 | 655 |
| SOME varsubst => |
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
656 |
let |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
657 |
val th = update_varsubst varsubst th |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
658 |
val th = update_prems (splicein prem_no (prems_of_theorem th') prems) th |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
659 |
val th = update_hyps (merge_hyps (hyps_of_theorem th) (hyps_of_theorem th')) th |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
660 |
val th = update_shyps (merge_shyps (shyps_of_theorem th) (shyps_of_theorem th')) th |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
661 |
in |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
662 |
update_theory thy th |
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
25520
diff
changeset
|
663 |
end |
25217 | 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 |
|
23174 | 681 |
|
682 |
end |
|
23663 | 683 |