6 For main code see structure Eval. |
6 For main code see structure Eval. |
7 *) |
7 *) |
8 signature EVALUATE__DEFINITION = |
8 signature EVALUATE__DEFINITION = |
9 sig |
9 sig |
10 eqtype const_id |
10 eqtype const_id |
11 (*eqtype calID*) |
11 type ml_fun = Rule_Def.eval_fn |
|
12 val ml_fun_empty: ml_fun |
12 type ml |
13 type ml |
13 (*type cal*) |
14 |
14 eqtype prog_id |
15 eqtype prog_id |
15 (*eqtype prog_calcID*) |
|
16 type ml_from_prog |
16 type ml_from_prog |
17 (*type calc_elem*) |
17 |
18 val equal: ml_from_prog * ml_from_prog -> bool |
18 val equal: ml_from_prog * ml_from_prog -> bool |
19 (*val calc_eq: ml_from_prog * ml_from_prog -> bool*) |
19 |
20 type ml_fun = Rule_Def.eval_fn |
|
21 (*type eval_fn = Rule_Def.eval_fn*) |
|
22 val ml_fun_empty: ml_fun |
|
23 (*val e_evalfn: ml_fun*) |
|
24 val ml_fun_to_store: ml_fun -> theory -> theory |
20 val ml_fun_to_store: ml_fun -> theory -> theory |
25 (*val set_data: ml_fun -> theory -> theory*) |
|
26 val ml_fun_from_store: theory -> ml_fun |
21 val ml_fun_from_store: theory -> ml_fun |
27 (*val the_data: theory -> ml_fun*) |
22 |
28 (**) |
|
29 end |
23 end |
30 |
24 |
31 (**) |
25 (**) |
32 structure Eval_Def(**): EVALUATE__DEFINITION(**) = |
26 structure Eval_Def(**): EVALUATE__DEFINITION(**) = |
33 struct |
27 struct |
34 (**) |
28 (**) |
35 |
29 |
36 type const_id = Rule_Def.eval_const_id (* op in Isabelle term "Const( op, _)" *) |
30 type const_id = Rule_Def.eval_const_id (* op in Isabelle term "Const( op, _)" *) |
37 type ml_fun = Rule_Def.eval_fn |
31 type ml_fun = Rule_Def.eval_fn |
|
32 fun ml_fun_empty (_ : 'a) (_ : term) (_ : Proof.context) = NONE : (string * term) option; |
38 type ml = const_id * ml_fun; |
33 type ml = const_id * ml_fun; |
39 |
34 |
40 type prog_id = string; (* accepted by partial_function in method*) |
35 type prog_id = string; (* accepted by partial_function in method *) |
41 type ml_from_prog = (* fun calculate_ fetches the evaluation-function via this list *) |
36 type ml_from_prog = (* fetched by fun calculate_ *) |
42 prog_id * (* a simple identifier used in programs *) |
37 prog_id * (* a simple identifier used in programs *) |
43 (const_id * (* a long identifier used in Const *) |
38 (const_id * (* a long identifier used in Const *) |
44 ml_fun) (* an ML function *) |
39 ml_fun) (* ML function for evaluation within rewriting *) |
45 |
40 |
46 fun equal ((pi1, (ci1, _)), (pi2, (ci2, _))) = |
41 fun equal ((pi1, (ci1, _)), (pi2, (ci2, _))) = |
47 if pi1 = pi2 |
42 if pi1 = pi2 |
48 then if ci1 = ci2 then true else raise ERROR ("equal: " ^ ci1 ^ " <> " ^ ci2) |
43 then if ci1 = ci2 then true else raise ERROR ("equal: " ^ ci1 ^ " <> " ^ ci2) |
49 else false |
44 else false |
52 Unifying "type ml" and "type calc" would make Lucas-Interpretation more efficient, |
47 Unifying "type ml" and "type calc" would make Lucas-Interpretation more efficient, |
53 see "fun rule2stac": instead of |
48 see "fun rule2stac": instead of |
54 Eval: const_id * eval_fn -> rule |
49 Eval: const_id * eval_fn -> rule |
55 would be better |
50 would be better |
56 Eval: prog_id * (const_id * eval_fn)) -> rule*) |
51 Eval: prog_id * (const_id * eval_fn)) -> rule*) |
57 type eval_fn = Rule_Def.eval_fn |
|
58 fun ml_fun_empty (_ : 'a) (_ : term) (_ : Proof.context) = NONE : (string * term) option; |
|
59 |
52 |
60 |
53 |
61 (* theory data for Isar command 'calculation' *) |
54 (* theory data for Isar command 'calculation' *) |
62 |
55 |
63 structure Data = Theory_Data |
56 structure Data = Theory_Data |
64 ( |
57 ( |
65 type T = eval_fn option; |
58 type T = ml_fun option; |
66 val empty = NONE; |
59 val empty = NONE; |
67 val extend = I; |
60 val extend = I; |
68 fun merge _ = NONE; |
61 fun merge _ = NONE; |
69 ); |
62 ); |
70 |
63 |