| author | wenzelm |
| Thu, 31 May 2007 20:55:32 +0200 | |
| changeset 23173 | 51179ca0c429 |
| child 23663 | 84b5c89b8b49 |
| permissions | -rw-r--r-- |
|
23173
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Tools/Compute_Oracle/Compute_Oracle.thy |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
3 |
Author: Steven Obua, TU Munich |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
4 |
|
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
5 |
Steven Obua's evaluator. |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
6 |
*) |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
7 |
|
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
8 |
theory Compute_Oracle |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
9 |
imports CPure |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
10 |
uses |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
11 |
"am_interpreter.ML" |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
12 |
"am_compiler.ML" |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
13 |
"am_util.ML" |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
14 |
"compute.ML" |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
15 |
begin |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
16 |
|
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
17 |
oracle compute_oracle ("Compute.computer * (int -> string) * cterm") =
|
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
18 |
{* Compute.oracle_fn *}
|
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
19 |
|
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
20 |
ML {*
|
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
21 |
structure Compute = |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
22 |
struct |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
23 |
open Compute |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
24 |
|
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
25 |
fun rewrite_param r n ct = |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
26 |
compute_oracle (Thm.theory_of_cterm ct) (r, n, ct) |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
27 |
|
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
28 |
fun rewrite r ct = rewrite_param r default_naming ct |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
29 |
end |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
30 |
*} |
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
31 |
|
|
51179ca0c429
proper theory setup for compute oracle (based on CPure);
wenzelm
parents:
diff
changeset
|
32 |
end |