1 (* Title: BaseDefinitions/rule-set.sml
3 (c) due to copyright terms
5 In ISAC a Rule_Set serves rewriting. Know_Store holds all rule-sets for ubiquitous access.
9 datatype T = datatype Rule_Def.rule_set
13 val rep: T -> {calc: Rule_Def.eval_ml_from_prog list, asm_rls: T, errpats: Rule_Def.errpatID list, id: string,
14 preconds: term list, rew_ord: Rewrite_Ord.T, rules: Rule_Def.rule list, program: Rule_Def.program, prog_rls: T}
16 val append_rules: string -> T -> Rule_Def.rule list -> T
17 val append_erls_rules: string -> T -> Rule_Def.rule list -> T
18 val keep_unique_rules: string -> T -> Rule_Def.rule list -> T
19 val merge: string -> T -> T -> T
20 val get_rules: T -> Rule_Def.rule list
21 val id_from_rule: Proof.context -> Rule.rule -> string
22 val contains: Rule.rule -> T -> bool
24 (*type for_know_store*)
26 val equal: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool
27 val to_kestore: for_kestore list * for_kestore list -> for_kestore list
29 (*/------- this will disappear eventually ----------------------------------------------------\*)
31 type rrlsstate = term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list
32 val e_rrlsstate: rrlsstate
34 (*\------- this will disappear eventually ----------------------------------------------------/*)
35 (*from isac_test for Minisubpbl*)
36 val to_string_test: Proof.context -> T -> string
39 val insert_merge: for_kestore -> for_kestore list -> for_kestore list
44 structure Rule_Set(**): RULE_SET(**) =
47 datatype T = datatype Rule_Def.rule_set;
50 (*/------- this will disappear eventually ----------------------------------------------------\*)
51 val dummy_ord = Rewrite_Ord.function_empty;
53 Rule_Def.Repeat {id = "empty", preconds = [], rew_ord = ("dummy_ord", dummy_ord), asm_rls = Rule_Def.Empty,
54 prog_rls = Rule_Def.Empty, calc = [], rules = [], errpatts = [], program = Rule_Def.Empty_Prog}
55 (*\------- this will disappear eventually ----------------------------------------------------/*)
58 fun rep Rule_Def.Empty = rep empty
59 | rep (Rule_Def.Repeat {id, preconds, rew_ord, asm_rls, prog_rls, calc, errpatts, rules, program}) =
60 {id = id, preconds = preconds, rew_ord = rew_ord, asm_rls = asm_rls, prog_rls = prog_rls, errpats = errpatts,
61 calc = calc, rules = rules, program = program}
62 | rep (Rule_Def.Sequence {id, preconds, rew_ord, asm_rls, prog_rls, calc, errpatts, rules, program}) =
63 {id = id, preconds = preconds, rew_ord = rew_ord, asm_rls = asm_rls, prog_rls = prog_rls, errpats = errpatts,
64 calc = calc, rules = rules, program = program}
65 | rep (Rule_Def.Rrls _) = rep empty
66 fun to_string_test _ Rule_Def.Empty = "Rule_Set.Empty"
67 | to_string_test ctxt (Rule_Def.Repeat {id, preconds, rew_ord, asm_rls = _, prog_rls = _, calc = _, errpatts = _, rules, program}) =
68 "(Rule_Def.Repeat {id = " ^ id ^ ", preconds = " ^ UnparseC.terms ctxt preconds ^ ", rew_ord = " ^ Rewrite_Ord.to_string rew_ord
69 ^ ",\n asm_rls = _, prog_rls = _, calc = _, errpatts = _, "
70 ^ ",\n rules = " ^ Rule.s_to_string rules
71 ^ ",\n rules = " ^ Rule_Def.program_to_string ctxt program ^ "})"
72 | to_string_test ctxt (Rule_Def.Sequence {id, preconds, rew_ord, asm_rls = _, prog_rls = _, calc = _, errpatts = _, rules, program}) =
73 "(Rule_Def.Repeat {id = " ^ id ^ ", preconds = " ^ UnparseC.terms ctxt preconds ^ ", rew_ord = " ^ Rewrite_Ord.to_string rew_ord
74 ^ ",\n asm_rls = _, prog_rls = _, calc = _, errpatts = _, "
75 ^ ",\n rules = " ^ Rule.s_to_string rules
76 ^ ",\n rules = " ^ Rule_Def.program_to_string ctxt program ^ "})"
77 | to_string_test _ (Rule_Def.Rrls _) = "Rule_Def.Rrls _"
79 fun append_rules id Rule_Def.Empty r = (*.. required for append_erls_rules *)
80 Rule_Def.Repeat {id = id, preconds = [], rew_ord = ("dummy_ord", dummy_ord), asm_rls = Rule_Def.Empty,
81 prog_rls = Rule_Def.Empty, calc = [], rules = r, errpatts = [], program = Rule_Def.Empty_Prog}
82 | append_rules id (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, asm_rls = er, prog_rls = sr, calc = ca,
83 rules = rs, errpatts = errpatts, program = sc}) r =
84 Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, asm_rls = er, prog_rls = sr, calc = ca,
85 rules = rs @ r, errpatts = errpatts, program = sc}
86 | append_rules id (Rule_Def.Sequence {id = _, preconds = pc, rew_ord = ro, asm_rls = er, prog_rls = sr, calc = ca,
87 rules = rs, errpatts = errpatts, program = sc}) r =
88 Rule_Def.Sequence {id = id, preconds = pc, rew_ord = ro, asm_rls = er, prog_rls = sr, calc = ca,
89 rules = rs @ r, errpatts = errpatts, program = sc}
90 | append_rules id (Rule_Def.Rrls _) _ = raise ERROR ("append_rules: not for reverse-rewrite-rule-set " ^ id);
92 fun append_erls_rules id_erls Rule_Def.Empty _ =
93 raise ERROR ("append_erls_rules: with \"" ^ id_erls ^ "\" not for Rule_Def.Empty")
94 | append_erls_rules id_erls (Rule_Def.Repeat
95 {id = id, preconds = pc, rew_ord = ro, asm_rls = asm_rls, prog_rls = sr, calc = ca,
96 rules = rules, errpatts = errpatts, program = sc}) rs =
97 Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, asm_rls = append_rules id_erls asm_rls rs,
98 prog_rls = sr, calc = ca, rules = rules, errpatts = errpatts, program = sc}
99 | append_erls_rules id_erls (Rule_Def.Sequence
100 {id = id, preconds = pc, rew_ord = ro, asm_rls = asm_rls, prog_rls = sr, calc = ca,
101 rules = rules, errpatts = errpatts, program = sc}) rs =
102 Rule_Def.Sequence {id = id, preconds = pc, rew_ord = ro, asm_rls = append_rules id_erls asm_rls rs,
103 prog_rls = sr, calc = ca, rules = rules, errpatts = errpatts, program = sc}
104 | append_erls_rules id_erls (Rule_Def.Rrls _) _ =
105 raise ERROR ("append_erls_rules: not for reverse-rewrite-rule-set " ^ id_erls);
107 fun merge_ids rls1 rls2 =
109 val id1 = (#id o rep) rls1
110 val id2 = (#id o rep) rls2
112 if id1 = id2 then id1 else "merged_" ^ id1 ^ "_" ^ id2
115 fun merge _ Rule_Def.Empty rls = rls
116 | merge _ rls Rule_Def.Empty = rls
117 | merge _ (Rrls x) _ = Rrls x (* required for merging Theory_Data *)
118 | merge _ _ (Rrls x) = Rrls x
120 (Rule_Def.Repeat {preconds = pc1, rew_ord = ro1, asm_rls = er1, prog_rls = sr1, calc = ca1,
121 rules = rs1, errpatts = eps1, program = sc1, ...})
122 (Rule_Def.Repeat {preconds = pc2, asm_rls = er2, prog_rls = sr2, calc = ca2,
123 rules = rs2, errpatts = eps2, ...})
125 Rule_Def.Repeat {id = id, rew_ord = ro1, program = sc1,
126 preconds = union (op =) pc1 pc2,
127 asm_rls = merge (merge_ids er1 er2) er1 er2,
128 prog_rls = merge (merge_ids sr1 sr2) sr1 sr2,
129 calc = union Eval_Def.equal ca1 ca2,
130 rules = union Rule.equal rs1 rs2,
131 errpatts = union (op =) eps1 eps2}
133 (Rule_Def.Sequence {preconds = pc1, rew_ord = ro1, asm_rls = er1, prog_rls = sr1, calc = ca1,
134 rules = rs1, errpatts = eps1, program = sc1, ...})
135 (Rule_Def.Sequence {preconds = pc2, asm_rls = er2, prog_rls = sr2, calc = ca2,
136 rules = rs2, errpatts = eps2, ...})
138 Rule_Def.Sequence {id = id, rew_ord = ro1, program = sc1,
139 preconds = union (op =) pc1 pc2,
140 asm_rls = merge (merge_ids er1 er2) er1 er2,
141 prog_rls = merge (merge_ids sr1 sr2) sr1 sr2,
142 calc = union Eval_Def.equal ca1 ca2,
143 rules = union Rule.equal rs1 rs2,
144 errpatts = union (op =) eps1 eps2}
145 | merge id _ _ = raise ERROR ("merge: \"" ^ id ^
146 "\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Rule_Def.Sequence");
148 (* datastructure for Know_Store, intermediate for thehier *)
150 (id * (* id unique within Isac *)
151 (ThyC.id * (* just for assignment in thehier, not appropriate for parsing etc *)
152 T)) (* ((#id o rep) T) = id by coding discipline *)
153 fun equal ((id1, (_, _)), (id2, (_, _))) = id1 = id2
155 fun insert_merge (re as (id, (thyID, r1))) ys =
156 case get_index (fn y => if curry equal re y then SOME y else NONE) ys of
158 | SOME (i, (_, (_, r2))) =>
160 val r12 = merge id r1 r2
161 in list_update ys i (id, (thyID, r12)) end
162 fun to_kestore (s1, s2) = fold insert_merge s1 s2;
164 (* used only for one hack *)
165 fun keep_unique_rules id
166 (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, asm_rls = er, prog_rls = sr, calc = ca,
167 rules = rs, errpatts = eps, program = sc}) r =
168 Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, asm_rls = er, prog_rls = sr, calc = ca,
169 rules = gen_rems Rule.equal (rs, r),
172 | keep_unique_rules id
173 (Rule_Def.Sequence {id = _, preconds = pc, rew_ord = ro, asm_rls = er, prog_rls = sr, calc = ca,
174 rules = rs, errpatts = eps, program = sc}) r =
175 Rule_Def.Sequence {id = id, preconds = pc, rew_ord = ro, asm_rls = er, prog_rls = sr, calc = ca,
176 rules = gen_rems Rule.equal (rs, r),
179 | keep_unique_rules id (Rule_Def.Rrls _) _ = raise ERROR ("keep_unique_rules: not for reverse-rewrite-rule-set "^id)
180 | keep_unique_rules _ rls _ = raise ERROR ("remove_rls called with " ^ id rls);
182 fun get_rules Rule_Def.Empty = []
183 | get_rules (Rule_Def.Repeat {rules, ...}) = rules
184 | get_rules (Rule_Def.Sequence {rules, ...}) = rules
185 | get_rules (Rule_Def.Rrls _) = [];
187 fun id_from_rule _ (Rule.Rls_ rls) = id rls
188 | id_from_rule ctxt r =
189 raise ERROR ("id_from_rule: not defined for " ^ Rule.to_string ctxt r);
191 (* check if a rule is contained in a rule-set (recursivley down in Rls_);
192 this rule can even be a rule-set itself *)
195 fun (*find (_, Rls_ rls) = finds (get_rules rls)
196 | find r12 = equal r12
197 and*) finds [] = false
198 | finds (r1 :: rs) = if Rule.equal (r, r1) then true else finds rs
200 finds (get_rules rls)
203 (*/------- this will disappear eventually -----------\*)
204 type rrlsstate = (* state for reverse rewriting, comments see type rule and program | Rfuns *)
205 (term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list);
206 val e_rrlsstate = (UnparseC.term_empty, UnparseC.term_empty, [[Rule_Def.Erule]], [(Rule_Def.Erule, (UnparseC.term_empty, []))]) : rrlsstate;
208 fun ii (_: term) = e_rrlsstate;
209 fun no (_: term) = SOME (UnparseC.term_empty, [UnparseC.term_empty]);
210 fun lo (_: Rule_Def.rule list list) (_: term) (_: Rule_Def.rule) = [(Rule_Def.Erule, (UnparseC.term_empty, [UnparseC.term_empty]))];
211 fun ne (_: Rule_Def.rule list list) (_: term) = SOME Rule_Def.Erule;
212 fun fo (_: Rule_Def.rule list list) (_: term) (_: term) = [(Rule_Def.Erule, (UnparseC.term_empty, [UnparseC.term_empty]))];
214 val e_rfuns = Rule_Def.Rfuns {init_state = ii, normal_form = no, locate_rule = lo,
215 next_rule = ne, attach_form = fo};
218 Rule_Def.Rrls {id = "e_rrls", prepat = [], rew_ord = ("dummy_ord", dummy_ord), asm_rls = Rule_Def.Empty,
219 calc = [], errpatts = [], program = e_rfuns}
220 (*\------- this will disappear eventually -----------/*)