1 (* Title: CalcElements/rule.sml
2 Author: Walther Neuper 2018
3 (c) copyright due to lincense terms
5 TODO: use "Rule" for renaming identifiers.
6 Some stuff waits for later rounds of restructuring, e.g. TermC.empty
11 datatype rule = datatype Rule_Def.rule
12 datatype program = datatype Rule_Def.program
14 val id_rls: Rule_Def.rule_set -> string
15 val id_rule: Rule_Def.rule -> string
16 val eq_rule: Rule_Def.rule * Rule_Def.rule -> bool
17 val rule2str: Rule_Def.rule -> string
18 val rule2str': Rule_Def.rule -> string
20 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
22 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
23 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
27 structure Rule(**): RULE(**) =
31 datatype rule = datatype Rule_Def.rule
32 datatype program = datatype Rule_Def.program
34 type calc = Rule_Def.calc (*..from Rule_Def*)
35 type calID = Rule_Def.calID; (*..from Rule_Def*)
36 (* eval function calling sml code during rewriting.
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
41 Num_Calc: prog_calcID * (calID * eval_fn)) -> rule*)
42 type eval_fn = Rule_Def.eval_fn (*..from Rule_Def*)
44 fun id_rls Rule_Def.Empty = "empty" (*WN060714 quick and dirty: recursive defs! TODO "Rule_Def.Empty"*)
45 | id_rls (Rule_Def.Repeat {id, ...}) = id
46 | id_rls (Rule_Def.Seqence {id, ...}) = id
47 | id_rls (Rule_Def.Rrls {id, ...}) = id;
49 fun id_rule (Rule_Def.Thm (id, _)) = id
50 | id_rule (Rule_Def.Num_Calc (id, _)) = id
51 | id_rule (Rule_Def.Cal1 (id, _)) = id
52 | id_rule (Rule_Def.Rls_ rls) = id_rls rls
53 | id_rule Rule_Def.Erule = "Erule";
54 fun eq_rule (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
56 | eq_rule (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = id_rls rls1 = id_rls rls2
59 fun rule2str Rule_Def.Erule = "Erule"
60 | rule2str (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ ThmC_Def.string_of_thmI thm ^ ")"
61 | rule2str (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
62 | rule2str (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
63 | rule2str (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ id_rls rls ^ "\")";
64 fun rule2str' Rule_Def.Erule = "Erule"
65 | rule2str' (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")"
66 | rule2str' (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
67 | rule2str' (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
68 | rule2str' (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ id_rls rls ^ "\")";