1 (* Title: CalcElements/rule-set.sml
3 (c) due to copyright terms
5 In ISAC a Rule_Set serves rewriting. KEStore holds all rule-sets for ubiquitous access.
9 datatype T = datatype Rule_Def.rule_set
12 val rls2str: T -> string
13 val rep: T -> {calc: Rule_Def.calc list, erls: T, errpats: Rule_Def.errpatID list, id: string,
14 preconds: term list, rew_ord: Rewrite_Ord.rew_ord, rules: Rule_Def.rule list, scr: Rule_Def.program, srls: T}
16 val append_rules: string -> T -> Rule_Def.rule list -> T
17 val keep_unique_rules: string -> T -> Rule_Def.rule list -> T
18 val merge: string -> T -> T -> T
19 val get_rules: T -> Rule_Def.rule list
22 val equal: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool
23 val to_kestore: for_kestore list * for_kestore list -> for_kestore list
25 (*/------- this will disappear eventually -----------\*)
27 type rrlsstate = term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list
28 val e_rrlsstate: rrlsstate
30 (*\------- this will disappear eventually -----------/*)
32 val rule2str: Rule_Def.rule -> string
33 val rule2str': Rule_Def.rule -> string
35 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
37 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
38 val insert_merge: for_kestore -> for_kestore list -> for_kestore list
39 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
43 structure Rule_Set(**): RULE_SET(**) =
46 datatype T = datatype Rule_Def.rule_set
47 type identifier = string
49 (*/------- this will disappear eventually ----------------------------------------------------\*)
50 fun dummy_ord (_: (term * term) list) (_: term, _: term) = true;
52 Rule_Def.Repeat {id = "empty", preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty,
53 srls = Rule_Def.Empty, calc = [], rules = [], errpatts = [], scr = Rule_Def.EmptyScr}
54 (*\------- this will disappear eventually ----------------------------------------------------/*)
56 fun rls2str xxx = Rule.id_rls xxx;
57 fun rep Rule_Def.Empty = rep empty
58 | rep (Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
59 {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
60 calc = calc, rules = rules, scr = scr}
61 | rep (Rule_Def.Seqence {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
62 {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
63 calc = calc, rules = rules, scr = scr}
64 | rep (Rule_Def.Rrls _) = rep empty
66 fun append_rules id Rule_Def.Empty _ = raise ERROR ("append_rules: with \"" ^ id ^ "\" not for Rule_Def.Empty")
67 | append_rules id (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
68 rules = rs, errpatts = errpatts, scr = sc}) r =
69 Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
70 rules = rs @ r, errpatts = errpatts, scr = sc}
71 | append_rules id (Rule_Def.Seqence {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
72 rules = rs, errpatts = errpatts, scr = sc}) r =
73 Rule_Def.Seqence {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
74 rules = rs @ r, errpatts = errpatts, scr = sc}
75 | append_rules id (Rule_Def.Rrls _) _ = raise ERROR ("append_rules: not for reverse-rewrite-rule-set " ^ id);
77 fun merge_ids rls1 rls2 =
79 val id1 = (#id o rep) rls1
80 val id2 = (#id o rep) rls2
82 if id1 = id2 then id1 else "merged_" ^ id1 ^ "_" ^ id2
85 fun merge _ Rule_Def.Empty rls = rls
86 | merge _ rls Rule_Def.Empty = rls
87 | merge _ (Rrls x) _ = Rrls x (* required for merging Theory_Data *)
88 | merge _ _ (Rrls x) = Rrls x
90 (Rule_Def.Repeat {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
91 rules = rs1, errpatts = eps1, scr = sc1, ...})
92 (Rule_Def.Repeat {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
93 rules = rs2, errpatts = eps2, ...})
95 Rule_Def.Repeat {id = id, rew_ord = ro1, scr = sc1,
96 preconds = union (op =) pc1 pc2,
97 erls = merge (merge_ids er1 er2) er1 er2,
98 srls = merge (merge_ids sr1 sr2) sr1 sr2,
99 calc = union Exec_Def.calc_eq ca1 ca2,
100 rules = union Rule.eq_rule rs1 rs2,
101 errpatts = union (op =) eps1 eps2}
103 (Rule_Def.Seqence {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
104 rules = rs1, errpatts = eps1, scr = sc1, ...})
105 (Rule_Def.Seqence {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
106 rules = rs2, errpatts = eps2, ...})
108 Rule_Def.Seqence {id = id, rew_ord = ro1, scr = sc1,
109 preconds = union (op =) pc1 pc2,
110 erls = merge (merge_ids er1 er2) er1 er2,
111 srls = merge (merge_ids sr1 sr2) sr1 sr2,
112 calc = union Exec_Def.calc_eq ca1 ca2,
113 rules = union Rule.eq_rule rs1 rs2,
114 errpatts = union (op =) eps1 eps2}
115 | merge id _ _ = error ("merge: \"" ^ id ^
116 "\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Rule_Def.Seqence");
118 fun rule2str Rule_Def.Erule = "Erule"
119 | rule2str (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ ThmC.string_of_thmI thm ^ ")"
120 | rule2str (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
121 | rule2str (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
122 | rule2str (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ rls2str rls ^ "\")";
123 fun rule2str' Rule_Def.Erule = "Erule"
124 | rule2str' (Rule_Def.Thm (str, _)) = "Thm (\"" ^ str ^ "\",\"\")"
125 | rule2str' (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
126 | rule2str' (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
127 | rule2str' (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ rls2str rls ^ "\")";
129 (* datastructure for KEStore_Elems, intermediate for thehier *)
131 (identifier * (* identifier unique within Isac *)
132 (ThyC.theory' * (* just for assignment in thehier, not appropriate for parsing etc *)
133 T)) (* ((#id o rep) T) = identifier by coding discipline *)
134 fun equal ((id1, (_, _)), (id2, (_, _))) = id1 = id2
136 fun insert_merge (re as (id, (thyID, r1))) ys =
137 case get_index (fn y => if curry equal re y then SOME y else NONE) ys of
139 | SOME (i, (_, (_, r2))) =>
141 val r12 = merge id r1 r2
142 in list_update ys i (id, (thyID, r12)) end
143 fun to_kestore (s1, s2) = fold insert_merge s1 s2;
145 (* used only for one hack *)
146 fun keep_unique_rules id
147 (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
148 rules = rs, errpatts = eps, scr = sc}) r =
149 Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
150 rules = gen_rems Rule.eq_rule (rs, r),
153 | keep_unique_rules id
154 (Rule_Def.Seqence {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
155 rules = rs, errpatts = eps, scr = sc}) r =
156 Rule_Def.Seqence {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
157 rules = gen_rems Rule.eq_rule (rs, r),
160 | keep_unique_rules id (Rule_Def.Rrls _) _ = raise ERROR ("keep_unique_rules: not for reverse-rewrite-rule-set "^id)
161 | keep_unique_rules _ rls _ = raise ERROR ("remove_rls called with " ^ rls2str rls);
163 fun get_rules Rule_Def.Empty = []
164 | get_rules (Rule_Def.Repeat {rules, ...}) = rules
165 | get_rules (Rule_Def.Seqence {rules, ...}) = rules
166 | get_rules (Rule_Def.Rrls _) = [];
168 (*/------- this will disappear eventually -----------\*)
169 type rrlsstate = (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
170 (term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list);
171 val e_rrlsstate = (UnparseC.e_term, UnparseC.e_term, [[Rule_Def.Erule]], [(Rule_Def.Erule, (UnparseC.e_term, []))]) : rrlsstate;
173 fun ii (_: term) = e_rrlsstate;
174 fun no (_: term) = SOME (UnparseC.e_term, [UnparseC.e_term]);
175 fun lo (_: Rule_Def.rule list list) (_: term) (_: Rule_Def.rule) = [(Rule_Def.Erule, (UnparseC.e_term, [UnparseC.e_term]))];
176 fun ne (_: Rule_Def.rule list list) (_: term) = SOME Rule_Def.Erule;
177 fun fo (_: Rule_Def.rule list list) (_: term) (_: term) = [(Rule_Def.Erule, (UnparseC.e_term, [UnparseC.e_term]))];
179 val e_rfuns = Rule_Def.Rfuns {init_state = ii, normal_form = no, locate_rule = lo,
180 next_rule = ne, attach_form = fo};
183 Rule_Def.Rrls {id = "e_rrls", prepat = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty,
184 calc = [], errpatts = [], scr = e_rfuns}
185 (*\------- this will disappear eventually -----------/*)