|
1 (* data-definitions, which should not occur in code-files to be re-evaluated |
|
2 use"definitions.sml"; |
|
3 *) |
|
4 |
|
5 type cterm' = string; |
|
6 val empty_cterm' = "empty_cterm'"; |
|
7 type thmID = string; |
|
8 type thm' = thmID * cterm'; |
|
9 type rls' = string; |
|
10 |
|
11 (*.fun calculate_ fetches the evaluation-function via this list.*) |
|
12 (*ie. there is NO rewriting involved in contrary to eval_rls*) |
|
13 type calc = |
|
14 (string * (*op in calculate_ from scripts*) |
|
15 (string * (*op in isa-term 'Const(op,_)' *) |
|
16 (string -> term -> theory -> (string * term) option))); (*eval_fun*) |
|
17 fun e_evalfn (_:'a) (_:term) (_:theory) = None:(string * term) option; |
|
18 |
|
19 type subs' = (cterm' * cterm') list; (*16.11.00 for FE-KE*) |
|
20 type subst = (term * term) list; (*here for ets2str*) |
|
21 fun subst2str (s:subst) = |
|
22 (strs2str o |
|
23 (map (pair2str o |
|
24 (apsnd (Sign.string_of_term (sign_of thy))) o |
|
25 (apfst (Sign.string_of_term (sign_of thy)))))) s; |
|
26 |
|
27 |
|
28 |
|
29 datatype rule = |
|
30 Thm of (string * thm) |
|
31 | Calc of string * (*check for equality*) |
|
32 (string -> term -> theory -> (string * term) option) |
|
33 | Rls_ of rls (*.ie. rule sets may be nested.*) |
|
34 and scr = |
|
35 EmptyScr |
|
36 | Script of term (*for meth'*) |
|
37 | Rfuns of {init_state : term -> |
|
38 (term * (*the current formula: |
|
39 goes locate_gen -> next_tac via istate*) |
|
40 term * (*the final formula*) |
|
41 rule list (*of reverse rewrite set (#1#)*) |
|
42 list * (*may be serveral, eg. in norm_rational*) |
|
43 (rule * (*Thm (+ Thm generated from Calc) resulting in ...*) |
|
44 (term * (*... rewrite with ...*) |
|
45 term list)) (*... assumptions*) |
|
46 list), (*derivation from given term to normalform |
|
47 in reverse order with sym_thm; |
|
48 (#1#) could be extracted from here #1*) |
|
49 |
|
50 normal_form: term -> (term * term list) option, |
|
51 locate_rule: rule list list -> term -> rule |
|
52 -> (rule * (term * term list)) list, |
|
53 next_rule : rule list list -> term -> rule option, |
|
54 attach_form: rule list list -> term -> term |
|
55 -> (rule * (term * term list)) list} |
|
56 and rls = |
|
57 Erls (*for init e_rls*) |
|
58 | Rls of {id : string, (*for trace_rewrite:=true*) |
|
59 preconds : term list, (*unused 20.8.02*) |
|
60 rew_ord : string * (subst -> (term * term) -> bool),(*for rules*) |
|
61 erls : rls, (*for the conditions in rules*) |
|
62 (* '^ because of rewrite in applicable_in; |
|
63 compare type meth'; FIXXME take name as string into Rls !*) |
|
64 srls : rls, (*for evaluation of list_fns in script*) |
|
65 calc : calc list, (*for Calculate in scr*) |
|
66 asm_thm : thm' list, (*FIXXME remove with put_asm*) |
|
67 rules : rule list, |
|
68 scr : scr} (*Script term (how to restrict type ???)*) |
|
69 | Seq of {id : string, (*for trace_rewrite:=true*) |
|
70 preconds : term list, (*unused 20.8.02*) |
|
71 rew_ord : string * (subst -> (term * term) -> bool),(*for rules*) |
|
72 erls : rls, (*for the conditions in rules*) |
|
73 (* '^ because of rewrite in applicable_in; |
|
74 compare type meth'; FIXXME take name as string into Rls !*) |
|
75 srls : rls, (*for evaluation of list_fns in script*) |
|
76 calc : calc list, (*for Calculate in scr*) |
|
77 asm_thm : thm' list, (*FIXXME remove with put_asm*) |
|
78 rules : rule list, |
|
79 scr : scr} (*Script term (how to restrict type ???)*) |
|
80 | Rrls of {id : string, (*for trace_rewrite:=true*) |
|
81 prepat : (term list * |
|
82 (*preconds, eval with subst from pattern*) |
|
83 term ) (*pattern matched in subterms*) |
|
84 list, (*meta-conjunction is or*) |
|
85 rew_ord : string * (subst -> (term * term) -> bool),(*for rules*) |
|
86 erls : rls, (*for the conditions in rules and pat*) |
|
87 (* '^ because of rewrite in applicable_in |
|
88 compare type meth'*) |
|
89 calc : calc list, (*for Calculate in scr*) |
|
90 asm_thm : thm' list, (*FIXXME remove with put_asm*) |
|
91 scr : scr}; (*Rfuns {...} (how to restrict type ???)*) |
|
92 (*1.8.02 ad (how to restrict type ???): scr should be usable indepentently |
|
93 from rls, and then contain both Script _AND_ Rfuns !!!*) |
|
94 |
|
95 |
|
96 |
|
97 val e_rule = Thm ("refl",refl) : rule; |
|
98 fun id_of_thm (Thm (id, _)) = id |
|
99 | id_of_thm _ = raise error "id_of_thm"; |
|
100 fun thm_of_thm (Thm (_, thm)) = thm |
|
101 | thm_of_thm _ = raise error "thm_of_thm"; |
|
102 fun rep_thm_G' (Thm (thmid, thm)) = (thmid, thm); |
|
103 fun rule2str (Thm (str, thm)) = "Thm (\""^str^"\","^(string_of_thm thm)^")" |
|
104 | rule2str (Calc (str,f)) = "Calc (\""^str^"\",fn)" |
|
105 | rule2str (Rls_ _) = "Rls_ rls";(*FIXXME*) |
|
106 fun eqrule (Thm (id1,_), Thm (id2,_)) = id1 = id2 |
|
107 | eqrule (Calc (id1,_), Calc (id2,_)) = id1 = id2 |
|
108 | eqrule (Rls_ _, Rls_ _) = false (*{id=id1}{id=id2} = id1 = id2 FIXXME*) |
|
109 | eqrule _ = false; |
|
110 fun memrls r (Rls {rules,...}) = gen_mem eqrule (r, rules) |
|
111 | memrls r (Seq {rules,...}) = gen_mem eqrule (r, rules) |
|
112 | memrls r _ = raise error ("memrls: incomplete impl. r= "^(rule2str r)); |
|
113 |
|
114 |
|
115 type rrlsstate = (*state for reverse rewriting*) |
|
116 (term * (*the current formula: |
|
117 goes locate_gen -> next_tac via istate*) |
|
118 term * (*the final formula*) |
|
119 rule list (*of reverse rewrite set (#1#)*) |
|
120 list * (*may be serveral, eg. in norm_rational*) |
|
121 (rule * (*Thm (+ Thm generated from Calc) resulting in ...*) |
|
122 (term * (*... rewrite with ...*) |
|
123 term list)) (*... assumptions*) |
|
124 list); (*derivation from given term to normalform |
|
125 in reverse order with sym_thm; |
|
126 (#1#) could be extracted from here #1*) |
|
127 val e_type = Type("empty",[]); |
|
128 val a_type = TFree("'a",[]); |
|
129 val e_term = Const("empty",e_type); |
|
130 val a_term = Free("empty",a_type); |
|
131 val e_rrlsstate = (e_term,e_term,[[e_rule]],[(e_rule,(e_term,[]))]):rrlsstate; |
|
132 |
|
133 |
|
134 |
|
135 |
|
136 (*22.2.02: ging auf Linux nicht (Stefan) |
|
137 val e_scr = Script ((term_of o the o (parse thy)) "e_script");*) |
|
138 val e_term = Const("empty", Type("'a", [])); |
|
139 val e_scr = Script e_term; |
|
140 |
|
141 |
|
142 (*ad thm': |
|
143 there are two kinds of theorems ... |
|
144 (1) known by isabelle |
|
145 (2) not known, eg. calc_thm, instantiated rls |
|
146 the latter have a thmid "#..." |
|
147 and thus outside isa we ALWAYS transport both(thmid,string_of_thm) |
|
148 and have a special assoc_thm / assoc_rls in this interface *) |
|
149 type theory' = string; (* = domID ^".thy" *) |
|
150 fun string_of_thy thy = |
|
151 ((last_elem (Sign.stamp_names_of (sign_of thy)))^".thy"):theory'; |
|
152 val theory2domID = string_of_thy; |
|
153 val theory2theory' = string_of_thy; |
|
154 |
|
155 type rew_ord' = string; |
|
156 |
|
157 val theory' = ref ([]:(theory' * theory) list); |
|
158 val rew_ord' = ref ([]:(rew_ord' * (subst -> (term * term) -> bool)) list); |
|
159 val ruleset' = ref ([]:(string * rls) list); |
|
160 val theorem' = ref ([]:(string * thm) list); |
|
161 (*val xxx = fn: a b => (a,b); ??? fun-definition ???*) |
|
162 local |
|
163 fun ii (_:term) = e_rrlsstate; |
|
164 fun no (_:term) = Some (e_term,[e_term]); |
|
165 fun lo (_:rule list list) (_:term) (_:rule) = [(e_rule,(e_term,[e_term]))]; |
|
166 fun ne (_:rule list list) (_:term) = Some e_rule; |
|
167 fun fo (_:rule list list) (_:term) (_:term) = [(e_rule,(e_term,[e_term]))]; |
|
168 in |
|
169 val e_rfuns = Rfuns {init_state=ii,normal_form=no,locate_rule=lo, |
|
170 next_rule=ne,attach_form=fo}; |
|
171 end; |
|
172 |
|
173 |
|
174 |
|
175 fun dummy_ord (_:subst) (_:term,_:term) = true; |
|
176 val e_rls = |
|
177 Rls{id = "e_rls", |
|
178 preconds = [], |
|
179 rew_ord = ("dummy_ord", dummy_ord), |
|
180 erls = Erls,srls = Erls, |
|
181 calc = [], |
|
182 asm_thm = [], |
|
183 rules = [], scr = EmptyScr}:rls; |
|
184 val e_rrls = Rrls {id = "e_rrls", |
|
185 prepat = [], |
|
186 rew_ord = ("dummy_ord", dummy_ord), |
|
187 erls = Erls, |
|
188 calc = [], |
|
189 asm_thm=[], |
|
190 scr=e_rfuns}:rls; |
|
191 ruleset' := overwritel (!ruleset', [("e_rls",e_rls), |
|
192 ("e_rrls",e_rrls) |
|
193 ]); |
|
194 |
|
195 fun rep_rls (Rls {id,preconds,rew_ord,erls,srls,calc,asm_thm,rules,scr}) = |
|
196 {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc, |
|
197 asm_thm=asm_thm,rules=rules,scr=scr} |
|
198 | rep_rls (Seq {id,preconds,rew_ord,erls,srls,calc,asm_thm,rules,scr}) = |
|
199 {id=id,preconds=preconds,rew_ord=rew_ord,erls=erls,srls=srls,calc=calc, |
|
200 asm_thm=asm_thm,rules=rules,scr=scr} |
|
201 | rep_rls (Rls {id,...}) = |
|
202 raise error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id) |
|
203 | rep_rls (Seq {id,...}) = |
|
204 raise error("rep_rls doesn't take apart reverse-rewrite-rule-sets: "^id); |
|
205 fun rep_rrls |
|
206 (Rrls {id,asm_thm, calc, erls, prepat, rew_ord, |
|
207 scr=Rfuns |
|
208 {attach_form,init_state,locate_rule, |
|
209 next_rule,normal_form}}) = |
|
210 {id=id,asm_thm=asm_thm, calc=calc, erls=erls, prepat=prepat, |
|
211 rew_ord=rew_ord, attach_form=attach_form, init_state=init_state, |
|
212 locate_rule=locate_rule, next_rule=next_rule, normal_form=normal_form} |
|
213 | rep_rrls (Rls {id,...}) = |
|
214 raise error ("rep_rrls doesn't take apart (normal) rule-sets: "^id) |
|
215 | rep_rrls (Seq {id,...}) = |
|
216 raise error ("rep_rrls doesn't take apart (normal) rule-sets: "^id); |
|
217 (*.id requested for all, Rls,Seq,Rrls.*) |
|
218 fun id_rls (Rls {id,...}) = id |
|
219 | id_rls (Seq {id,...}) = id |
|
220 | id_rls (Rrls {id,...}) = id; |
|
221 |
|
222 fun append_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
223 asm_thm=at,rules =rs,scr=sc}) r = |
|
224 (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
225 asm_thm=at,rules = rs @ r,scr=sc}:rls) |
|
226 | append_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
227 asm_thm=at,rules =rs,scr=sc}) r = |
|
228 (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
229 asm_thm=at,rules = rs @ r,scr=sc}:rls) |
|
230 | append_rls id (Rrls _) _ = raise error |
|
231 ("append_rls: not for reverse-rewrite-rule-set "^id); |
|
232 |
|
233 fun eq_rule (Thm thm1, Thm thm2) = thm1 = thm2 |
|
234 | eq_rule (Calc (id1,_), Calc (id2,_)) = id1 = id2 |
|
235 | eq_rule _ = false; |
|
236 |
|
237 fun merge_rls _ Erls rls = rls |
|
238 | merge_rls _ rls Erls = rls |
|
239 | merge_rls id |
|
240 (Rls {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1, |
|
241 asm_thm=at1,rules =rs1,scr=sc1}) |
|
242 r2 = |
|
243 (Rls {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2), |
|
244 rew_ord=ro1,erls=(*merge_rls er1 er2*)er1, |
|
245 srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1 |
|
246 ((#srls o rep_rls) r2), |
|
247 calc=ca1 @ ((#calc o rep_rls) r2), |
|
248 asm_thm=at1 @ ((#asm_thm o rep_rls) r2), |
|
249 rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2), |
|
250 scr=sc1}:rls) |
|
251 | merge_rls id |
|
252 (Seq {id=id1,preconds=pc1,rew_ord=ro1,erls=er1,srls=sr1,calc=ca1, |
|
253 asm_thm=at1,rules =rs1,scr=sc1}) |
|
254 r2 = |
|
255 (Seq {id=id,preconds=pc1 @ ((#preconds o rep_rls) r2), |
|
256 rew_ord=ro1,erls=(*merge_rls er1 er2*)er1, |
|
257 srls=merge_rls ("merged_"^id1^"_"^((#id o rep_rls) r2)) sr1 |
|
258 ((#srls o rep_rls) r2), |
|
259 calc=ca1 @ ((#calc o rep_rls) r2), |
|
260 asm_thm=at1 @ ((#asm_thm o rep_rls) r2), |
|
261 rules = gen_union eq_rule rule2str (rs1, (#rules o rep_rls) r2), |
|
262 scr=sc1}:rls) |
|
263 | merge_rls _ _ _ = raise error |
|
264 "merge_rls: not for reverse-rewrite-rule-sets"; |
|
265 fun remove_rls id (Rls {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
266 asm_thm=at,rules =rs,scr=sc}) r = |
|
267 (Rls{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
268 asm_thm=at,rules = gen_rems eq_rule (rs, r), |
|
269 scr=sc}:rls) |
|
270 | remove_rls id (Seq {id=_,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
271 asm_thm=at,rules =rs,scr=sc}) r = |
|
272 (Seq{id=id,preconds=pc,rew_ord=ro,erls=er,srls=sr,calc=ca, |
|
273 asm_thm=at,rules = gen_rems eq_rule (rs, r), |
|
274 scr=sc}:rls) |
|
275 | remove_rls id (Rrls _) _ = raise error |
|
276 ("remove_rls: not for reverse-rewrite-rule-set "^id); |
|
277 |
|
278 gen_rems (op=) ([1,2,3], [3,4,5]); |
|
279 |
|
280 |
|
281 |
|
282 fun assoc' ([], key) = raise error ("ME_Isa: '"^key^"' not known") |
|
283 | assoc' ((keyi, xi) :: pairs, key) = |
|
284 if key = keyi then Some xi else assoc' (pairs, key); |
|
285 |
|
286 fun assoc_thy (thy:theory') = ((the o assoc')(!theory',thy)) |
|
287 handle _ => raise error ("ME_Isa: '"^thy^"' not in system"); |
|
288 fun assoc_rls (rls:rls') = ((the o assoc')(!ruleset',rls)) |
|
289 handle _ => raise error ("ME_Isa: '"^rls^"' not in system"); |
|
290 |
|
291 fun termopt2str (Some t) = |
|
292 "Some " ^ (Sign.string_of_term (sign_of(assoc_thy "Isac.thy")) t) |
|
293 | termopt2str None = "None"; |
|
294 fun term2str t = Sign.string_of_term (sign_of(assoc_thy "Isac.thy")) t; |
|
295 (*for tests only*) |
|
296 fun terms2str ts= (strs2str o (map (Sign.string_of_term |
|
297 (sign_of (assoc_thy "Isac.thy"))))) ts; |
|
298 |
|
299 (*recursive defs:*) |
|
300 fun scr2str (Script s) = "Script "^(term2str s) |
|
301 | scr2str (Rfuns _) = "Rfuns"; |
|
302 |
|
303 |
|
304 type domID = string; (* domID ^"thy" = theory' ??check 3.00!!*) |
|
305 val e_domID = "e_domID":domID; |
|
306 type pblID = string list; (* domID::...*) |
|
307 val e_pblID = ["e_pblID"]:pblID; |
|
308 type metID = (domID * string); |
|
309 val e_metID = (e_domID,"e_metID"):metID; |
|
310 |
|
311 fun metID2str ((domID,mI):metID) = pair2str (domID,mI); |
|
312 |