equal
deleted
inserted
replaced
3 Author: Steven Obua, TU Munich |
3 Author: Steven Obua, TU Munich |
4 |
4 |
5 Steven Obua's evaluator. |
5 Steven Obua's evaluator. |
6 *) |
6 *) |
7 |
7 |
8 theory Compute_Oracle |
8 theory Compute_Oracle imports CPure |
9 imports CPure |
9 uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "compute.ML" "linker.ML" |
10 uses |
|
11 "am_interpreter.ML" |
|
12 "am_compiler.ML" |
|
13 "am_util.ML" |
|
14 "compute.ML" |
|
15 begin |
10 begin |
16 |
11 |
17 oracle compute_oracle ("Compute.computer * (int -> string) * cterm") = |
12 setup {* Compute.setup; *} |
18 {* Compute.oracle_fn *} |
|
19 |
|
20 ML {* |
|
21 structure Compute = |
|
22 struct |
|
23 open Compute |
|
24 |
|
25 fun rewrite_param r n ct = |
|
26 compute_oracle (Thm.theory_of_cterm ct) (r, n, ct) |
|
27 |
|
28 fun rewrite r ct = rewrite_param r default_naming ct |
|
29 end |
|
30 *} |
|
31 |
13 |
32 end |
14 end |