1 (* Title: BaseDefinitions/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 set_id: Rule_Def.rule_set -> string
15 val id: Rule_Def.rule -> string
16 val equal: Rule_Def.rule * Rule_Def.rule -> bool
17 val to_string: Rule_Def.rule -> string
18 val to_string_short: Rule_Def.rule -> string
21 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
22 val thm_id: rule -> string
23 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
25 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
29 structure Rule(**): RULE(**) =
33 datatype rule = datatype Rule_Def.rule;
34 datatype program = datatype Rule_Def.program;
35 type is_as_string = string;
37 type calc = Rule_Def.calc
38 type calID = Rule_Def.calID;
39 type eval_fn = Rule_Def.eval_fn;
41 fun set_id Rule_Def.Empty = "empty" (*WN060714 quick and dirty: recursive defs! TODO "Rule_Def.Empty"*)
42 | set_id (Rule_Def.Repeat {id, ...}) = id
43 | set_id (Rule_Def.Seqence {id, ...}) = id
44 | set_id (Rule_Def.Rrls {id, ...}) = id;
46 fun id (Rule_Def.Thm (id, _)) = id
47 | id (Rule_Def.Num_Calc (id, _)) = id
48 | id (Rule_Def.Cal1 (id, _)) = id
49 | id (Rule_Def.Rls_ rls) = set_id rls
50 | id Rule_Def.Erule = "Erule";
51 fun equal (Rule_Def.Thm (thm1, _), Rule_Def.Thm (thm2, _)) = thm1 = thm2
52 | equal (Rule_Def.Num_Calc (id1, _), Rule_Def.Num_Calc (id2, _)) = id1 = id2
53 | equal (Rule_Def.Rls_ rls1, Rule_Def.Rls_ rls2) = set_id rls1 = set_id rls2
56 fun to_string Rule_Def.Erule = "Erule"
57 | to_string (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ ThmC_Def.string_of_thm thm ^ ")"
58 | to_string (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
59 | to_string (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
60 | to_string (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
61 fun to_string_short Rule_Def.Erule = "Erule"
62 | to_string_short (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")"
63 | to_string_short (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
64 | to_string_short (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
65 | to_string_short (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ set_id rls ^ "\")";
67 fun thm_id (Rule_Def.Thm (id, _)) = id
68 | thm_id _ = raise ERROR ("Rule.thm_id: uncovered case " (* ^ to_string r *))
69 fun thm (Rule_Def.Thm (_, thm)) = thm
70 | thm r = raise ERROR ("Rule.thm: uncovered case " ^ to_string r)