author  wenzelm 
Sun, 08 Jul 2007 19:51:58 +0200  
changeset 23655  d2d1138e0ddc 
parent 23173  51179ca0c429 
child 23663  84b5c89b8b49 
permissions  rwrr 
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 