5 tools for rewriting, reverse rewriting, context to thy concerning rewriting |
5 tools for rewriting, reverse rewriting, context to thy concerning rewriting |
6 *) |
6 *) |
7 |
7 |
8 signature THEORY_DATA_PRESENTATION = |
8 signature THEORY_DATA_PRESENTATION = |
9 sig |
9 sig |
10 |
|
11 eqtype filename |
10 eqtype filename |
12 |
11 |
13 datatype contthy |
|
14 = ContNOrew of {applto: term, thm_rls: Check_Unique.id, thyID: ThyC.id} |
|
15 | ContNOrewInst of {applto: term, bdvs: subst, thm_rls: Check_Unique.id, thminst: term, thyID: ThyC.id} |
|
16 | ContRls of {applto: term, asms: term list, result: term, rls: Check_Unique.id, thyID: ThyC.id} |
|
17 | ContRlsInst of {applto: term, asms: term list, bdvs: subst, result: term, rls: Check_Unique.id, thyID: ThyC.id} |
|
18 | ContThm of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list, |
|
19 lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord', rhs: term * term, |
|
20 thm: Check_Unique.id, thyID: ThyC.id} |
|
21 | ContThmInst of {applat: term, applto: term, asmrls: Rule_Set.id, asms: (term * term) list, |
|
22 bdvs: subst, lhs: term * term, resasms: term list, result: term, reword: Rewrite_Ord.rew_ord', |
|
23 rhs: term * term, thm: Check_Unique.id, thminst: term, thyID: ThyC.id} |
|
24 | EContThy |
|
25 val guh2filename : Check_Unique.id -> filename |
12 val guh2filename : Check_Unique.id -> filename |
26 val thms_of_rls : Rule_Set.T -> Rule.rule list |
13 val thms_of_rls : Rule_Set.T -> Rule.rule list |
27 val theID2filename : Thy_Write.theID -> filename |
|
28 val no_thycontext : Check_Unique.id -> bool |
|
29 val subs_from : Istate.T -> 'a -> Check_Unique.id -> Subst.input |
|
30 val guh2rewtac : Check_Unique.id -> Subst.input -> Tactic.input |
|
31 val get_tac_checked : Ctree.ctree -> Pos.pos' -> Tactic.input |
|
32 val context_thy : Calc.T -> Tactic.input -> contthy |
|
33 val guh2theID : Check_Unique.id -> Thy_Write.theID |
|
34 end |
14 end |
35 (**) |
15 (**) |
36 structure Thy_Present(**): THEORY_DATA_PRESENTATION(**) = |
16 structure Thy_Present(**): THEORY_DATA_PRESENTATION(**) = |
37 struct |
17 struct |
38 (**) |
18 (**) |
39 |
19 |
40 type filename = string; |
20 type filename = string; |
41 |
|
42 (* packing return-values to matchTheory, contextToThy for xml-generation *) |
|
43 datatype contthy = (*also an item from Know_Store on Browser ...........#*) |
|
44 EContThy (* not from Know_Store ..............................*) |
|
45 | ContThm of (* a theorem in contex ===========================*) |
|
46 {thyID : ThyC.id, (* for *2guh in sub-elems here .*) |
|
47 thm : Check_Unique.id, (* theorem in the context .*) |
|
48 applto : term, (* applied to formula ... .*) |
|
49 applat : term, (* ... with lhs inserted .*) |
|
50 reword : Rewrite_Ord.rew_ord', (* order used for rewrite .*) |
|
51 asms : (term (* asumption instantiated .*) |
|
52 * term) list, (* asumption evaluated .*) |
|
53 lhs : term (* lhs of the theorem ... #*) |
|
54 * term, (* ... instantiated .*) |
|
55 rhs : term (* rhs of the theorem ... #*) |
|
56 * term, (* ... instantiated .*) |
|
57 result : term, (* resulting from the rewrite .*) |
|
58 resasms : term list, (* ... with asms stored .*) |
|
59 asmrls : Rule_Set.id (* ruleset for evaluating asms .*) |
|
60 } |
|
61 | ContThmInst of (* a theorem with bdvs in contex ============ *) |
|
62 {thyID : ThyC.id, (*for *2guh in sub-elems here .*) |
|
63 thm : Check_Unique.id, (*theorem in the context .*) |
|
64 bdvs : subst, (*bound variables to modify... .*) |
|
65 thminst : term, (*... theorem instantiated .*) |
|
66 applto : term, (*applied to formula ... .*) |
|
67 applat : term, (*... with lhs inserted .*) |
|
68 reword : Rewrite_Ord.rew_ord', (*order used for rewrite .*) |
|
69 asms : (term (*asumption instantiated .*) |
|
70 * term) list, (*asumption evaluated .*) |
|
71 lhs : term (*lhs of the theorem ... #*) |
|
72 * term, (*... instantiated .*) |
|
73 rhs : term (*rhs of the theorem ... #*) |
|
74 * term, (*... instantiated .*) |
|
75 result : term, (*resulting from the rewrite .*) |
|
76 resasms : term list, (*... with asms stored .*) |
|
77 asmrls : Rule_Set.id (*ruleset for evaluating asms .*) |
|
78 } |
|
79 | ContRls of (* a rule set in contex ========================= *) |
|
80 {thyID : ThyC.id, (*for *2guh in sub-elems here .*) |
|
81 rls : Check_Unique.id, (*rule set in the context .*) |
|
82 applto : term, (*rewrite this formula .*) |
|
83 result : term, (*resulting from the rewrite .*) |
|
84 asms : term list (*... with asms stored .*) |
|
85 } |
|
86 | ContRlsInst of (* a rule set with bdvs in contex =========== *) |
|
87 {thyID : ThyC.id, (*for *2guh in sub-elems here .*) |
|
88 rls : Check_Unique.id, (*rule set in the context .*) |
|
89 bdvs : subst, (*for bound variables in thms .*) |
|
90 applto : term, (*rewrite this formula .*) |
|
91 result : term, (*resulting from the rewrite .*) |
|
92 asms : term list (*... with asms stored .*) |
|
93 } |
|
94 | ContNOrew of (* no rewrite for thm or rls ================== *) |
|
95 {thyID : ThyC.id, (*for *2guh in sub-elems here .*) |
|
96 thm_rls : Check_Unique.id, (*thm or rls in the context .*) |
|
97 applto : term (*rewrite this formula .*) |
|
98 } |
|
99 | ContNOrewInst of (* no rewrite for some instantiation ====== *) |
|
100 {thyID : ThyC.id, (*for *2guh in sub-elems here .*) |
|
101 thm_rls : Check_Unique.id, (*thm or rls in the context .*) |
|
102 bdvs : subst, (*for bound variables in thms .*) |
|
103 thminst : term, (*... theorem instantiated .*) |
|
104 applto : term (*rewrite this formula .*) |
|
105 } |
|
106 |
|
107 (*.check a rewrite-tac for bdv (RL always used *_Inst !) TODO.WN060718 |
|
108 pass other tacs unchanged.*) |
|
109 fun get_tac_checked pt ((p, _) : Pos.pos') = Ctree.get_obj Ctree.g_tac pt p; |
|
110 |
|
111 (* get the formula f at ptp rewritten by the Rewrite_* already applied to f *) |
|
112 fun context_thy (pt, pos as (p, p_)) (tac as Tactic.Rewrite thm'') = |
|
113 let |
|
114 val thm_deriv = ThmC.long_id thm'' |
|
115 in |
|
116 (case Step.check tac (pt, pos) of |
|
117 Applicable.Yes (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res, asm))) => |
|
118 ContThm |
|
119 {thyID = thy', |
|
120 thm = Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv), |
|
121 applto = f, applat = TermC.empty, reword = ord', |
|
122 asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*), |
|
123 result = res, resasms = asm, asmrls = Rule_Set.id erls} |
|
124 | Applicable.No _ => |
|
125 let |
|
126 val pp = Ctree.par_pblobj pt p |
|
127 val thy' = Ctree.get_obj Ctree.g_domID pt pp |
|
128 val f = case p_ of |
|
129 Pos.Frm => Ctree.get_obj Ctree.g_form pt p |
|
130 | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p |
|
131 | _ => raise ERROR "context_thy: uncovered position" |
|
132 in |
|
133 ContNOrew |
|
134 {thyID = thy', |
|
135 thm_rls = |
|
136 Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv), |
|
137 applto = f} |
|
138 end |
|
139 | _ => raise ERROR "context_thy..Rewrite: uncovered case 2") |
|
140 end |
|
141 | context_thy (pt, pos as (p, p_)) (tac as Tactic.Rewrite_Inst (subs, (thmID, _))) = |
|
142 let val thm = Global_Theory.get_thm (ThyC.Isac ()) thmID |
|
143 in |
|
144 (case Step.check tac (pt, pos) of |
|
145 Applicable.Yes (Tactic.Rewrite_Inst' (thy', ord', erls, _, subst, _, f, (res, asm))) => |
|
146 let |
|
147 val thm_deriv = Thm.get_name_hint thm |
|
148 val thminst = TermC.inst_bdv subst (Eval.norm (Thm.prop_of thm)) |
|
149 in |
|
150 ContThmInst |
|
151 {thyID = thy', |
|
152 thm = |
|
153 Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv), |
|
154 bdvs = subst, thminst = thminst, applto = f, applat = TermC.empty, reword = ord', |
|
155 asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*), |
|
156 result = res, resasms = asm, asmrls = Rule_Set.id erls} |
|
157 end |
|
158 | Applicable.No _ => |
|
159 let |
|
160 val thm = Global_Theory.get_thm (ThyC.Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID |
|
161 val thm_deriv = Thm.get_name_hint thm |
|
162 val pp = Ctree.par_pblobj pt p |
|
163 val thy' = Ctree.get_obj Ctree.g_domID pt pp |
|
164 val subst = Subst.T_from_input (ThyC.get_theory thy') subs |
|
165 val thminst = TermC.inst_bdv subst (Eval.norm (Thm.prop_of thm)) |
|
166 val f = case p_ of |
|
167 Pos.Frm => Ctree.get_obj Ctree.g_form pt p |
|
168 | Pos.Res => (fst o (Ctree.get_obj Ctree.g_result pt)) p |
|
169 | _ => raise ERROR "context_thy: uncovered case 3" |
|
170 in |
|
171 ContNOrewInst |
|
172 {thyID = thy', |
|
173 thm_rls = Thy_Write.thm2guh (Thy_Read.thy_containing_thm thm_deriv) (ThmC.cut_id thm_deriv), |
|
174 bdvs = subst, thminst = thminst, applto = f} |
|
175 end |
|
176 | _ => raise ERROR "context_thy..Rewrite_Inst: uncovered case 4") |
|
177 end |
|
178 | context_thy (pt, p) (tac as Tactic.Rewrite_Set rls') = |
|
179 (case Step.check tac (pt, p) of |
|
180 Applicable.Yes (Tactic.Rewrite_Set' (thy', _, _(*rls*), f, (res,asm))) => |
|
181 ContRls |
|
182 {thyID = thy', |
|
183 rls = Thy_Write.rls2guh (Thy_Read.thy_containing_rls thy' rls') rls', |
|
184 applto = f, result = res, asms = asm} |
|
185 | _ => raise ERROR ("context_thy Rewrite_Set: not for Applicable.No")) |
|
186 | context_thy (pt,p) (tac as Tactic.Rewrite_Set_Inst (_(*subs*), rls')) = |
|
187 (case Step.check tac (pt, p) of |
|
188 Applicable.Yes (Tactic.Rewrite_Set_Inst' (thy', _, subst, _, f, (res,asm))) => |
|
189 ContRlsInst |
|
190 {thyID = thy', |
|
191 rls = Thy_Write.rls2guh (Thy_Read.thy_containing_rls thy' rls') rls', |
|
192 bdvs = subst, applto = f, result = res, asms = asm} |
|
193 | _ => raise ERROR ("context_thy Rewrite_Set_Inst: not for Applicable.No")) |
|
194 | context_thy (_, p) tac = |
|
195 raise ERROR ("context_thy: not for tac " ^ Tactic.input_to_string tac ^ " at " ^ Pos.pos'2str p) |
|
196 |
21 |
197 (* get all theorems in a rule set (recursivley containing rule sets) *) |
22 (* get all theorems in a rule set (recursivley containing rule sets) *) |
198 fun thm_of_rule Rule.Erule = [] |
23 fun thm_of_rule Rule.Erule = [] |
199 | thm_of_rule (thm as Rule.Thm _) = [thm] |
24 | thm_of_rule (thm as Rule.Thm _) = [thm] |
200 | thm_of_rule (Rule.Eval _) = [] |
25 | thm_of_rule (Rule.Eval _) = [] |
203 and thms_of_rls Rule_Set.Empty = [] |
28 and thms_of_rls Rule_Set.Empty = [] |
204 | thms_of_rls (Rule_Def.Repeat {rules,...}) = (flat o (map thm_of_rule)) rules |
29 | thms_of_rls (Rule_Def.Repeat {rules,...}) = (flat o (map thm_of_rule)) rules |
205 | thms_of_rls (Rule_Set.Sequence {rules,...}) = (flat o (map thm_of_rule)) rules |
30 | thms_of_rls (Rule_Set.Sequence {rules,...}) = (flat o (map thm_of_rule)) rules |
206 | thms_of_rls (Rule_Set.Rrls _) = [] |
31 | thms_of_rls (Rule_Set.Rrls _) = [] |
207 |
32 |
208 |
|
209 (* filenames not only for thydata, but also for thy's etc *) |
|
210 fun theID2filename theID = Thy_Write.theID2guh theID ^ ".xml" |
|
211 |
|
212 fun guh2theID guh = |
|
213 let |
|
214 val guh' = Symbol.explode guh |
|
215 val part = implode (take_fromto 1 4 guh') |
|
216 val isa = implode (take_fromto 5 9 guh') |
|
217 in |
|
218 if not (member op = ["exp_", "thy_", "pbl_", "met_"] part) |
|
219 then raise ERROR ("guh '" ^ guh ^ "' does not begin with exp_ | thy_ | pbl_ | met_") |
|
220 else |
|
221 let |
|
222 val chap = case isa of |
|
223 "isab_" => "Isabelle" |
|
224 | "scri_" => "IsacScripts" |
|
225 | "isac_" => "IsacKnowledge" |
|
226 | _ => |
|
227 raise ERROR ("guh2theID: '" ^ guh ^ "' does not have isab_ | scri_ | isac_ at position 5..9") |
|
228 val rest = takerest (9, guh') |
|
229 val thyID = takewhile [] (not o (curry op= "-")) rest |
|
230 val rest' = dropuntil (curry op = "-") rest |
|
231 in case implode rest' of |
|
232 "-part" => [chap] : Thy_Write.theID |
|
233 | "" => [chap, implode thyID] |
|
234 | "-Theorems" => [chap, implode thyID, "Theorems"] |
|
235 | "-Rulesets" => [chap, implode thyID, "Rulesets"] |
|
236 | "-Operations" => [chap, implode thyID, "Operations"] |
|
237 | "-Orders" => [chap, implode thyID, "Orders"] |
|
238 | _ => |
|
239 let val sect = implode (take_fromto 1 5 rest') |
|
240 val sect' = case sect of |
|
241 "-thm-" => "Theorems" |
|
242 | "-rls-" => "Rulesets" |
|
243 | "-cal-" => "Operations" |
|
244 | "-ord-" => "Orders" |
|
245 | _ => |
|
246 raise ERROR ("guh2theID: '" ^ guh ^ "' has '" ^ sect ^ "' instead -thm- | -rls- | -cal- | -ord-") |
|
247 in |
|
248 [chap, implode thyID, sect', implode (takerest (5, rest'))] |
|
249 end |
|
250 end |
|
251 end |
|
252 |
|
253 fun guh2filename guh = guh ^ ".xml"; |
33 fun guh2filename guh = guh ^ ".xml"; |
254 |
34 |
255 fun guh2rewtac guh [] = |
|
256 let |
|
257 val (_, thy, sect, xstr) = case guh2theID guh of |
|
258 [isa, thy, sect, xstr] => (isa, thy, sect, xstr) |
|
259 | _ => raise ERROR "guh2rewtac: uncovered case" |
|
260 in case sect of |
|
261 "Theorems" => Tactic.Rewrite (xstr, ThmC.thm_from_thy (ThyC.get_theory thy) xstr) |
|
262 | "Rulesets" => Tactic.Rewrite_Set xstr |
|
263 | _ => raise ERROR ("guh2rewtac: not impl. for '"^xstr^"'") |
|
264 end |
|
265 | guh2rewtac guh subs = |
|
266 let |
|
267 val (_, thy, sect, xstr) = case guh2theID guh of |
|
268 [isa, thy, sect, xstr] => (isa, thy, sect, xstr) |
|
269 | _ => raise ERROR "guh2rewtac: uncovered case" |
|
270 in case sect of |
|
271 "Theorems" => |
|
272 Tactic.Rewrite_Inst (subs, (xstr, ThmC.thm_from_thy (ThyC.get_theory thy) xstr)) |
|
273 | "Rulesets" => Tactic.Rewrite_Set_Inst (subs, xstr) |
|
274 | str => raise ERROR ("guh2rewtac: not impl. for '" ^ str ^ "'") |
|
275 end |
|
276 |
|
277 (* the front-end may request a context for any element of the hierarchy *) |
|
278 fun no_thycontext guh = (guh2theID guh; false) |
|
279 handle ERROR _ => true; |
|
280 |
|
281 (* get the substitution of bound variables for matchTheory: |
|
282 # lookup the thm|rls' in the script |
|
283 # take the [(bdv, v_),..] from the respective Rewrite_(Set_)Inst |
|
284 # instantiate this subs with the istates env to [(bdv, x),..] |
|
285 # otherwise [] |
|
286 WN060617 hack assuming that all scripts use only one bound variable |
|
287 and use 'v_' as the formal argument for this bound variable*) |
|
288 fun subs_from (Istate.Pstate ({env, ...})) _ guh = |
|
289 let |
|
290 val (_, _, thyID, sect, xstr) = case guh2theID guh of |
|
291 theID as [isa, thyID, sect, xstr] => (theID, isa, thyID, sect, xstr) |
|
292 | _ => raise ERROR "subs_from: uncovered case" |
|
293 in |
|
294 case sect of |
|
295 "Theorems" => |
|
296 let val thm = Global_Theory.get_thm (ThyC.get_theory thyID) xstr |
|
297 in |
|
298 if Auto_Prog.contains_bdv thm |
|
299 then |
|
300 let |
|
301 val formal_arg = TermC.str2term "v_" |
|
302 val value = subst_atomic env formal_arg |
|
303 in ["(''bdv''," ^ UnparseC.term value ^ ")"] : Subst.input end |
|
304 else [] |
|
305 end |
|
306 | "Rulesets" => |
|
307 let |
|
308 val rules = (Rule_Set.get_rules o assoc_rls) xstr |
|
309 in |
|
310 if Auto_Prog.contain_bdv rules |
|
311 then |
|
312 let |
|
313 val formal_arg = TermC.str2term "v_" |
|
314 val value = subst_atomic env formal_arg |
|
315 in ["(''bdv''," ^ UnparseC.term value ^ ")"] : Subst.input end |
|
316 else [] |
|
317 end |
|
318 | str => raise ERROR ("subs_from: uncovered case with " ^ str) |
|
319 end |
|
320 | subs_from _ _ guh = raise ERROR ("subs_from: uncovered case with " ^ guh) |
|
321 |
|
322 (**)end(**) |
35 (**)end(**) |