conditional compilation via system option "isac_test" and antiquotation \<^isac_test>CARTOUCHE:
option is provided in session ROOT, or interactively via $ISABELLE_HOME_USER/etc/preferences (i.e. Isabelle/jEdit plugin preferences);
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.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
20 (*val rule2rls': Rule.rule -> string*)
21 val id_from_rule: Rule.rule -> string
22 val contains: Rule.rule -> T -> bool
25 val equal: (''a * ('b * 'c)) * (''a * ('d * 'e)) -> bool
26 val to_kestore: for_kestore list * for_kestore list -> for_kestore list
28 (*/------- this will disappear eventually ----------------------------------------------------\*)
30 type rrlsstate = term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list
31 val e_rrlsstate: rrlsstate
33 (*\------- this will disappear eventually ----------------------------------------------------/*)
35 val insert_merge: for_kestore -> for_kestore list -> for_kestore list
40 structure Rule_Set(**): RULE_SET(**) =
43 datatype T = datatype Rule_Def.rule_set;
46 (*/------- this will disappear eventually ----------------------------------------------------\*)
47 fun dummy_ord (_: (term * term) list) (_: term, _: term) = true;
49 Rule_Def.Repeat {id = "empty", preconds = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty,
50 srls = Rule_Def.Empty, calc = [], rules = [], errpatts = [], scr = Rule_Def.Empty_Prog}
51 (*\------- this will disappear eventually ----------------------------------------------------/*)
54 fun rep Rule_Def.Empty = rep empty
55 | rep (Rule_Def.Repeat {id, preconds, rew_ord, erls, srls, calc, errpatts, rules, scr}) =
56 {id = id, preconds = preconds, rew_ord = rew_ord, erls = erls, srls = srls, errpats = errpatts,
57 calc = calc, rules = rules, scr = scr}
58 | rep (Rule_Def.Sequence {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.Rrls _) = rep empty
63 fun append_rules id Rule_Def.Empty _ = raise ERROR ("append_rules: with \"" ^ id ^ "\" not for Rule_Def.Empty")
64 | append_rules id (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
65 rules = rs, errpatts = errpatts, scr = sc}) r =
66 Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
67 rules = rs @ r, errpatts = errpatts, scr = sc}
68 | append_rules id (Rule_Def.Sequence {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
69 rules = rs, errpatts = errpatts, scr = sc}) r =
70 Rule_Def.Sequence {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
71 rules = rs @ r, errpatts = errpatts, scr = sc}
72 | append_rules id (Rule_Def.Rrls _) _ = raise ERROR ("append_rules: not for reverse-rewrite-rule-set " ^ id);
74 fun merge_ids rls1 rls2 =
76 val id1 = (#id o rep) rls1
77 val id2 = (#id o rep) rls2
79 if id1 = id2 then id1 else "merged_" ^ id1 ^ "_" ^ id2
82 fun merge _ Rule_Def.Empty rls = rls
83 | merge _ rls Rule_Def.Empty = rls
84 | merge _ (Rrls x) _ = Rrls x (* required for merging Theory_Data *)
85 | merge _ _ (Rrls x) = Rrls x
87 (Rule_Def.Repeat {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
88 rules = rs1, errpatts = eps1, scr = sc1, ...})
89 (Rule_Def.Repeat {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
90 rules = rs2, errpatts = eps2, ...})
92 Rule_Def.Repeat {id = id, rew_ord = ro1, scr = sc1,
93 preconds = union (op =) pc1 pc2,
94 erls = merge (merge_ids er1 er2) er1 er2,
95 srls = merge (merge_ids sr1 sr2) sr1 sr2,
96 calc = union Eval_Def.calc_eq ca1 ca2,
97 rules = union Rule.equal rs1 rs2,
98 errpatts = union (op =) eps1 eps2}
100 (Rule_Def.Sequence {preconds = pc1, rew_ord = ro1, erls = er1, srls = sr1, calc = ca1,
101 rules = rs1, errpatts = eps1, scr = sc1, ...})
102 (Rule_Def.Sequence {preconds = pc2, erls = er2, srls = sr2, calc = ca2,
103 rules = rs2, errpatts = eps2, ...})
105 Rule_Def.Sequence {id = id, rew_ord = ro1, scr = sc1,
106 preconds = union (op =) pc1 pc2,
107 erls = merge (merge_ids er1 er2) er1 er2,
108 srls = merge (merge_ids sr1 sr2) sr1 sr2,
109 calc = union Eval_Def.calc_eq ca1 ca2,
110 rules = union Rule.equal rs1 rs2,
111 errpatts = union (op =) eps1 eps2}
112 | merge id _ _ = raise ERROR ("merge: \"" ^ id ^
113 "\"; not for reverse-rewrite-rule-sets and not for mixed Rls -- Rule_Def.Sequence");
115 (* datastructure for KEStore_Elems, intermediate for thehier *)
117 (id * (* id unique within Isac *)
118 (ThyC.id * (* just for assignment in thehier, not appropriate for parsing etc *)
119 T)) (* ((#id o rep) T) = id by coding discipline *)
120 fun equal ((id1, (_, _)), (id2, (_, _))) = id1 = id2
122 fun insert_merge (re as (id, (thyID, r1))) ys =
123 case get_index (fn y => if curry equal re y then SOME y else NONE) ys of
125 | SOME (i, (_, (_, r2))) =>
127 val r12 = merge id r1 r2
128 in list_update ys i (id, (thyID, r12)) end
129 fun to_kestore (s1, s2) = fold insert_merge s1 s2;
131 (* used only for one hack *)
132 fun keep_unique_rules id
133 (Rule_Def.Repeat {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
134 rules = rs, errpatts = eps, scr = sc}) r =
135 Rule_Def.Repeat {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
136 rules = gen_rems Rule.equal (rs, r),
139 | keep_unique_rules id
140 (Rule_Def.Sequence {id = _, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
141 rules = rs, errpatts = eps, scr = sc}) r =
142 Rule_Def.Sequence {id = id, preconds = pc, rew_ord = ro, erls = er, srls = sr, calc = ca,
143 rules = gen_rems Rule.equal (rs, r),
146 | keep_unique_rules id (Rule_Def.Rrls _) _ = raise ERROR ("keep_unique_rules: not for reverse-rewrite-rule-set "^id)
147 | keep_unique_rules _ rls _ = raise ERROR ("remove_rls called with " ^ id rls);
149 fun get_rules Rule_Def.Empty = []
150 | get_rules (Rule_Def.Repeat {rules, ...}) = rules
151 | get_rules (Rule_Def.Sequence {rules, ...}) = rules
152 | get_rules (Rule_Def.Rrls _) = [];
154 fun id_from_rule (Rule.Rls_ rls) = id rls
155 | id_from_rule r = raise ERROR ("id_from_rule: not defined for " ^ Rule.to_string r);
157 (* check if a rule is contained in a rule-set (recursivley down in Rls_);
158 this rule can even be a rule-set itself *)
161 fun (*find (_, Rls_ rls) = finds (get_rules rls)
162 | find r12 = equal r12
163 and*) finds [] = false
164 | finds (r1 :: rs) = if Rule.equal (r, r1) then true else finds rs
166 finds (get_rules rls)
169 (*/------- this will disappear eventually -----------\*)
170 type rrlsstate = (* state for reverse rewriting, comments see type rule and scr | Rfuns *)
171 (term * term * Rule_Def.rule list list * (Rule_Def.rule * (term * term list)) list);
172 val e_rrlsstate = (UnparseC.term_empty, UnparseC.term_empty, [[Rule_Def.Erule]], [(Rule_Def.Erule, (UnparseC.term_empty, []))]) : rrlsstate;
174 fun ii (_: term) = e_rrlsstate;
175 fun no (_: term) = SOME (UnparseC.term_empty, [UnparseC.term_empty]);
176 fun lo (_: Rule_Def.rule list list) (_: term) (_: Rule_Def.rule) = [(Rule_Def.Erule, (UnparseC.term_empty, [UnparseC.term_empty]))];
177 fun ne (_: Rule_Def.rule list list) (_: term) = SOME Rule_Def.Erule;
178 fun fo (_: Rule_Def.rule list list) (_: term) (_: term) = [(Rule_Def.Erule, (UnparseC.term_empty, [UnparseC.term_empty]))];
180 val e_rfuns = Rule_Def.Rfuns {init_state = ii, normal_form = no, locate_rule = lo,
181 next_rule = ne, attach_form = fo};
184 Rule_Def.Rrls {id = "e_rrls", prepat = [], rew_ord = ("dummy_ord", dummy_ord), erls = Rule_Def.Empty,
185 calc = [], errpatts = [], scr = e_rfuns}
186 (*\------- this will disappear eventually -----------/*)