9 signature RULE = |
9 signature RULE = |
10 sig |
10 sig |
11 datatype rule = datatype Rule_Def.rule |
11 datatype rule = datatype Rule_Def.rule |
12 datatype program = datatype Rule_Def.program |
12 datatype program = datatype Rule_Def.program |
13 |
13 |
14 val id_rls: Rule_Def.rule_set -> string |
14 val set_id: Rule_Def.rule_set -> string |
15 val id_rule: Rule_Def.rule -> string |
15 val id: Rule_Def.rule -> string |
16 val eq_rule: Rule_Def.rule * Rule_Def.rule -> bool |
16 val equal: Rule_Def.rule * Rule_Def.rule -> bool |
17 val rule2str: Rule_Def.rule -> string |
17 val to_string: Rule_Def.rule -> string |
18 val rule2str': Rule_Def.rule -> string |
18 val to_string_short: Rule_Def.rule -> string |
19 |
19 |
20 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
20 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
21 (*NONE*) |
21 (*NONE*) |
22 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
22 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
23 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
23 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
26 (**) |
26 (**) |
27 structure Rule(**): RULE(**) = |
27 structure Rule(**): RULE(**) = |
28 struct |
28 struct |
29 (**) |
29 (**) |
30 |
30 |
31 datatype rule = datatype Rule_Def.rule |
31 datatype rule = datatype Rule_Def.rule; |
32 datatype program = datatype Rule_Def.program |
32 datatype program = datatype Rule_Def.program; |
33 |
33 |
34 type calc = Rule_Def.calc (*..from Rule_Def*) |
34 type calc = Rule_Def.calc |
35 type calID = Rule_Def.calID; (*..from Rule_Def*) |
35 type calID = Rule_Def.calID; |
36 (* eval function calling sml code during rewriting. |
36 type eval_fn = Rule_Def.eval_fn; |
37 Unifying "type cal" and "type calc" would make Lucas-Interpretation more efficient, |
|
38 see "fun rule2stac": instead of |
|
39 Num_Calc: calID * eval_fn -> rule |
|
40 would be better |
|
41 Num_Calc: prog_calcID * (calID * eval_fn)) -> rule*) |
|
42 type eval_fn = Rule_Def.eval_fn (*..from Rule_Def*) |
|
43 |
37 |
44 fun id_rls Rule_Def.Empty = "empty" (*WN060714 quick and dirty: recursive defs! TODO "Rule_Def.Empty"*) |
38 fun set_id Rule_Def.Empty = "empty" (*WN060714 quick and dirty: recursive defs! TODO "Rule_Def.Empty"*) |
45 | id_rls (Rule_Def.Repeat {id, ...}) = id |
39 | set_id (Rule_Def.Repeat {id, ...}) = id |
46 | id_rls (Rule_Def.Seqence {id, ...}) = id |
40 | set_id (Rule_Def.Seqence {id, ...}) = id |
47 | id_rls (Rule_Def.Rrls {id, ...}) = id; |
41 | set_id (Rule_Def.Rrls {id, ...}) = id; |
48 |
42 |
49 fun id_rule (Rule_Def.Thm (id, _)) = id |
43 fun id (Rule_Def.Thm (id, _)) = id |
50 | id_rule (Rule_Def.Num_Calc (id, _)) = id |
44 | id (Rule_Def.Num_Calc (id, _)) = id |
51 | id_rule (Rule_Def.Cal1 (id, _)) = id |
45 | id (Rule_Def.Cal1 (id, _)) = id |
52 | id_rule (Rule_Def.Rls_ rls) = id_rls rls |
46 | id (Rule_Def.Rls_ rls) = set_id rls |
53 | id_rule Rule_Def.Erule = "Erule"; |
47 | id Rule_Def.Erule = "Erule"; |
54 fun eq_rule (Rule_Def.Thm (thm1, _), Rule_Def.Thm (thm2, _)) = thm1 = thm2 |
48 fun equal (Rule_Def.Thm (thm1, _), Rule_Def.Thm (thm2, _)) = thm1 = thm2 |
55 | eq_rule (Rule_Def.Num_Calc (id1, _), Rule_Def.Num_Calc (id2, _)) = id1 = id2 |
49 | equal (Rule_Def.Num_Calc (id1, _), Rule_Def.Num_Calc (id2, _)) = id1 = id2 |
56 | eq_rule (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = id_rls rls1 = id_rls rls2 |
50 | equal (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = set_id rls1 = set_id rls2 |
57 | eq_rule _ = false; |
51 | equal _ = false; |
58 |
52 |
59 fun rule2str Rule_Def.Erule = "Erule" |
53 fun to_string Rule_Def.Erule = "Erule" |
60 | rule2str (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ ThmC_Def.string_of_thmI thm ^ ")" |
54 | to_string (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ ThmC_Def.string_of_thmI thm ^ ")" |
61 | rule2str (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)" |
55 | to_string (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)" |
62 | rule2str (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)" |
56 | to_string (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)" |
63 | rule2str (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ id_rls rls ^ "\")"; |
57 | to_string (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")"; |
64 fun rule2str' Rule_Def.Erule = "Erule" |
58 fun to_string_short Rule_Def.Erule = "Erule" |
65 | rule2str' (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")" |
59 | to_string_short (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")" |
66 | rule2str' (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)" |
60 | to_string_short (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)" |
67 | rule2str' (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)" |
61 | to_string_short (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)" |
68 | rule2str' (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ id_rls rls ^ "\")"; |
62 | to_string_short (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")"; |
69 |
63 |
70 (**)end(**) |
64 (**)end(**) |