|
1 (* Handle user-input during the specify- and the solve-phase. |
|
2 author: Walther Neuper |
|
3 0603 |
|
4 (c) due to copyright terms |
|
5 |
|
6 use"ME/inform.sml"; |
|
7 use"inform.sml"; |
|
8 *) |
|
9 |
|
10 signature INFORM = |
|
11 sig |
|
12 |
|
13 type castab |
|
14 type icalhd |
|
15 |
|
16 (* type iitem *) |
|
17 datatype |
|
18 iitem = |
|
19 Find of cterm' list |
|
20 | Given of cterm' list |
|
21 | Relate of cterm' list |
|
22 type imodel |
|
23 val imodel2fstr : iitem list -> (string * cterm') list |
|
24 |
|
25 |
|
26 val Isac : 'a -> theory |
|
27 val appl_add' : |
|
28 theory' -> |
|
29 SpecifyTools.ori list -> |
|
30 SpecifyTools.itm list -> |
|
31 ('a * (Term.term * Term.term)) list -> |
|
32 string * cterm' -> SpecifyTools.itm |
|
33 (* val appl_adds : |
|
34 theory' -> |
|
35 SpecifyTools.ori list -> |
|
36 SpecifyTools.itm list -> |
|
37 (string * (Term.term * Term.term)) list -> |
|
38 (string * string) list -> SpecifyTools.itm list *) |
|
39 (* val cas_input : string -> ptree * ocalhd *) |
|
40 (* val cas_input_ : |
|
41 spec -> |
|
42 (Term.term * Term.term list) list -> |
|
43 pblID * SpecifyTools.itm list * metID * SpecifyTools.itm list * |
|
44 (bool * Term.term) list *) |
|
45 val castab : castab ref |
|
46 val compare_step : |
|
47 calcstate' -> Term.term -> string * calcstate' |
|
48 (* val concat_deriv : |
|
49 'a * ((Term.term * Term.term) list -> Term.term * Term.term -> bool) |
|
50 -> |
|
51 rls -> |
|
52 rule list -> |
|
53 Term.term -> |
|
54 Term.term -> |
|
55 bool * (Term.term * rule * (Term.term * Term.term list)) list *) |
|
56 val dropwhile' : (* systest/auto-inform.sml *) |
|
57 ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list |
|
58 (* val dtss2itm_ : |
|
59 pbt_ list -> |
|
60 Term.term * Term.term list -> |
|
61 int list * bool * string * SpecifyTools.itm_ *) |
|
62 (* val e_icalhd : icalhd *) |
|
63 val eq7 : ''a * ''b -> ''a * (''b * 'c) -> bool |
|
64 val equal : ''a -> ''a -> bool |
|
65 (* val filter_dsc : |
|
66 SpecifyTools.ori list -> SpecifyTools.itm -> SpecifyTools.ori list *) |
|
67 (* val filter_sep : ('a -> bool) -> 'a list -> 'a list * 'a list *) |
|
68 (* val flattup2 : 'a * ('b * 'c * 'd * 'e) -> 'a * 'b * 'c * 'd * 'e *) |
|
69 (* val fstr2itm_ : |
|
70 theory -> |
|
71 (''a * (Term.term * Term.term)) list -> |
|
72 ''a * string -> int list * bool * ''a * SpecifyTools.itm_ *) |
|
73 val inform : |
|
74 calcstate' -> cterm' -> string * calcstate' |
|
75 val input_icalhd : ptree -> icalhd -> ptree * ocalhd |
|
76 (* val is_Par : SpecifyTools.itm -> bool *) |
|
77 (* val is_casinput : cterm' -> fmz -> bool *) |
|
78 (* val is_e_ts : Term.term list -> bool *) |
|
79 (* val itms2fstr : SpecifyTools.itm -> string * string *) |
|
80 (* val mk_tacis : |
|
81 rew_ord' * 'a -> |
|
82 rls -> |
|
83 Term.term * rule * (Term.term * Term.term list) -> |
|
84 tac * tac_ * (pos' * istate) *) |
|
85 val oris2itms : |
|
86 'a -> int -> SpecifyTools.ori list -> SpecifyTools.itm list |
|
87 (* val par2fstr : SpecifyTools.itm -> string * cterm' *) |
|
88 (* val parsitm : theory -> SpecifyTools.itm -> SpecifyTools.itm *) |
|
89 val rev_deriv' : 'a * rule * ('b * 'c) -> 'b * rule * ('a * 'c) |
|
90 (* val unknown_expl : |
|
91 theory' -> |
|
92 (string * (Term.term * Term.term)) list -> |
|
93 (string * string) list -> SpecifyTools.itm list *) |
|
94 end |
|
95 |
|
96 |
|
97 |
|
98 |
|
99 |
|
100 |
|
101 (***. handle an input calc-head .***) |
|
102 |
|
103 (*------------------------------------------------------------------(**) |
|
104 structure inform :INFORM = |
|
105 struct |
|
106 (**)------------------------------------------------------------------*) |
|
107 |
|
108 datatype iitem = |
|
109 Given of cterm' list |
|
110 (*Where is never input*) |
|
111 | Find of cterm' list |
|
112 | Relate of cterm' list; |
|
113 |
|
114 type imodel = iitem list; |
|
115 |
|
116 (*calc-head as input*) |
|
117 type icalhd = |
|
118 pos' * (*the position of the calc-head in the calc-tree |
|
119 pos' as (p,p_) where p_ is neglected due to pos_ below*) |
|
120 cterm' * (*the headline*) |
|
121 imodel * (*the model (without Find) of the calc-head*) |
|
122 pos_ * (*model belongs to Pbl or Met*) |
|
123 spec; (*specification: domID, pblID, metID*) |
|
124 val e_icalhd = (e_pos', "", [Given [""]], Pbl, e_spec): icalhd; |
|
125 |
|
126 fun is_casinput (hdf: cterm') ((fmz_, spec): fmz) = |
|
127 hdf <> "" andalso fmz_ = [] andalso spec = e_spec; |
|
128 |
|
129 (*.handle an input as into an algebra system.*) |
|
130 fun dtss2itm_ ppc (d, ts) = |
|
131 let val (f, (d, id)) = the (find_first ((curry op= d) o |
|
132 (#1: (term * term) -> term) o |
|
133 (#2: pbt_ -> (term * term))) ppc) |
|
134 in ([1], true, f, Cor ((d, ts), (id, ts))) end; |
|
135 |
|
136 fun flattup2 (a,(b,c,d,e)) = (a,b,c,d,e); |
|
137 |
|
138 |
|
139 |
|
140 (*.association list with cas-commands, for generating a complete calc-head.*) |
|
141 type castab = |
|
142 (term * (*cas-command, eg. 'solve'*) |
|
143 (spec * (*theory, problem, method*) |
|
144 |
|
145 (*the function generating a kind of formalization*) |
|
146 (term list -> (*the arguments of the cas-command, eg. (x+1=2, x)*) |
|
147 (term * (*description of an element*) |
|
148 term list) (*value of the element (always put into a list)*) |
|
149 list))) (*of elements in the formalization*) |
|
150 list; (*of cas-entries in the association list*) |
|
151 |
|
152 val castab = ref ([]: castab); |
|
153 |
|
154 |
|
155 (*..*) |
|
156 (* val (dI,pI,mI) = spec; |
|
157 *) |
|
158 (*fun cas_input_ ((dI,pI,mI): spec) dtss = |
|
159 let val thy = assoc_thy dI |
|
160 val {ppc,...} = get_pbt pI |
|
161 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*) |
|
162 val its = add_id its_ |
|
163 val pits = map flattup2 its |
|
164 val (pI, mI) = if mI <> ["no_met"] then (pI, mI) |
|
165 else let val SOME (pI,_) = refine_pbl thy pI pits |
|
166 in (pI, (hd o #met o get_pbt) pI) end |
|
167 val {ppc,pre,prls,...} = get_met mI |
|
168 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*) |
|
169 val its = add_id its_ |
|
170 val mits = map flattup2 its |
|
171 val pre = check_preconds thy prls pre mits |
|
172 in (pI, pits: itm list, mI, mits: itm list, pre) end;*) |
|
173 |
|
174 (* val (dI,pI,mI) = spec; |
|
175 *) |
|
176 fun cas_input_ ((dI,pI,mI): spec) dtss = |
|
177 let val thy = assoc_thy dI |
|
178 val {ppc,...} = get_pbt pI |
|
179 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*) |
|
180 val its = add_id its_ |
|
181 val pits = map flattup2 its |
|
182 val (pI, mI) = if mI <> ["no_met"] then (pI, mI) |
|
183 else case refine_pbl thy pI pits of |
|
184 SOME (pI,_) => (pI, (hd o #met o get_pbt) pI) |
|
185 | NONE => (pI, (hd o #met o get_pbt) pI) |
|
186 val {ppc,pre,prls,...} = get_met mI |
|
187 val its_ = map (dtss2itm_ ppc) dtss (*([1],true,"#Given",Cor (...))*) |
|
188 val its = add_id its_ |
|
189 val mits = map flattup2 its |
|
190 val pre = check_preconds thy prls pre mits |
|
191 in (pI, pits: itm list, mI, mits: itm list, pre) end; |
|
192 |
|
193 |
|
194 (*.check if the input term is a CAScmd and return a ptree with |
|
195 a _complete_ calchead.*) |
|
196 (* val hdt = ifo; |
|
197 *) |
|
198 fun cas_input hdt = |
|
199 let val (h,argl) = strip_comb hdt |
|
200 in case assoc (!castab, h) of |
|
201 NONE => NONE |
|
202 (*let val (pt,_) = |
|
203 cappend_problem e_ptree [] e_istate |
|
204 ([], e_spec) ([], e_spec, e_term) |
|
205 in (pt, (false, Pbl, e_term(*FIXXME031:'not found'*), |
|
206 [], [], e_spec)) end*) |
|
207 | SOME (spec as (dI,_,_), argl2dtss) => |
|
208 (* val SOME (spec as (dI,_,_), argl2dtss ) = assoc (!castab, h); |
|
209 *) |
|
210 let val dtss = argl2dtss argl |
|
211 val (pI, pits, mI, mits, pre) = cas_input_ spec dtss |
|
212 val spec = (dI, pI, mI) |
|
213 val (pt,_) = |
|
214 cappend_problem e_ptree [] e_istate ([], e_spec) |
|
215 ([], e_spec, hdt) |
|
216 val pt = update_spec pt [] spec |
|
217 val pt = update_pbl pt [] pits |
|
218 val pt = update_met pt [] mits |
|
219 in SOME (pt, (true, Met, hdt, mits, pre, spec):ocalhd) end |
|
220 end; |
|
221 |
|
222 (*lazy evaluation for Isac.thy*) |
|
223 fun Isac _ = assoc_thy "Isac.thy"; |
|
224 |
|
225 (*re-parse itms with a new thy and prepare for checking with ori list*) |
|
226 fun parsitm dI (itm as (i,v,b,f, Cor ((d,ts),_)):itm) = |
|
227 (* val itm as (i,v,b,f, Cor ((d,ts),_)) = hd probl; |
|
228 *) |
|
229 (let val t = (comp_dts (Isac "delay")) (d,ts); |
|
230 val s = Syntax.string_of_term (thy2ctxt dI) t; |
|
231 (*this ^ should raise the exn on unability of re-parsing dts*) |
|
232 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm)) |
|
233 | parsitm dI (itm as (i,v,b,f, Syn str)) = |
|
234 (let val t = (term_of o the o (parse dI)) str |
|
235 in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str)) |
|
236 | parsitm dI (itm as (i,v,b,f, Typ str)) = |
|
237 (let val t = (term_of o the o (parse dI)) str |
|
238 in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str)) |
|
239 | parsitm dI (itm as (i,v,_,f, Inc ((d,ts),_))) = |
|
240 (let val t = (comp_dts (Isac "delay")) (d,ts); |
|
241 val s = Syntax.string_of_term (thy2ctxt dI) t; |
|
242 (*this ^ should raise the exn on unability of re-parsing dts*) |
|
243 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm)) |
|
244 | parsitm dI (itm as (i,v,_,f, Sup (d,ts))) = |
|
245 (let val t = (comp_dts (Isac"delay" )) (d,ts); |
|
246 val s = Syntax.string_of_term (thy2ctxt dI) t; |
|
247 (*this ^ should raise the exn on unability of re-parsing dts*) |
|
248 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm)) |
|
249 | parsitm dI (itm as (i,v,_,f, Mis (d,t'))) = |
|
250 (let val t = d $ t'; |
|
251 val s = Syntax.string_of_term (thy2ctxt dI) t; |
|
252 (*this ^ should raise the exn on unability of re-parsing dts*) |
|
253 in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm)) |
|
254 | parsitm dI (itm as (i,v,_,f, Par _)) = |
|
255 raise error ("parsitm (" ^ itm2str_ (thy2ctxt dI) itm^ |
|
256 "): Par should be internal"); |
|
257 |
|
258 (*separate a list to a pair of elements that do NOT satisfy the predicate, |
|
259 and of elements that satisfy the predicate, i.e. (false, true)*) |
|
260 fun filter_sep pred xs = |
|
261 let fun filt ab [] = ab |
|
262 | filt (a,b) (x :: xs) = if pred x |
|
263 then filt (a,b@[x]) xs |
|
264 else filt (a@[x],b) xs |
|
265 in filt ([],[]) xs end; |
|
266 fun is_Par ((_,_,_,_,Par _):itm) = true |
|
267 | is_Par _ = false; |
|
268 |
|
269 fun is_e_ts [] = true |
|
270 | is_e_ts [Const ("List.list.Nil", _)] = true |
|
271 | is_e_ts _ = false; |
|
272 |
|
273 (*WN.9.11.03 copied from fun appl_add (in modspec.sml)*) |
|
274 (* val (sel,ct) = selct; |
|
275 val (dI, oris, ppc, pbt, (sel, ct))= |
|
276 (#1 (some_spec ospec spec), oris, []:itm list, |
|
277 ((#ppc o get_pbt) (#2 (some_spec ospec spec))), |
|
278 hd (imodel2fstr imodel)); |
|
279 *) |
|
280 fun appl_add' dI oris ppc pbt (sel, ct) = |
|
281 let |
|
282 val thy = assoc_thy dI; |
|
283 in case parse thy ct of |
|
284 NONE => (0,[],false,sel, Syn ct):itm |
|
285 | SOME ct => (* val SOME ct = parse thy ct; |
|
286 *) |
|
287 (case is_known thy sel oris (term_of ct) of |
|
288 (* val ("",ori'(*ts='ct'*), all) = is_known thy sel oris (term_of ct); |
|
289 *) |
|
290 ("",ori'(*ts='ct'*), all) => |
|
291 (case is_notyet_input thy ppc all ori' pbt of |
|
292 (* val ("",itm) = is_notyet_input thy ppc all ori' pbt; |
|
293 *) |
|
294 ("",itm) => itm |
|
295 (* val (msg,xx) = is_notyet_input thy ppc all ori' pbt; |
|
296 *) |
|
297 | (msg,_) => raise error ("appl_add': "^msg)) |
|
298 (* val (msg,(_,_,_,d,ts),all) = is_known thy sel oris (term_of ct); |
|
299 *) |
|
300 | (msg,(i,v,_,d,ts),_) => |
|
301 if is_e_ts ts then (i,v,false, sel, Inc ((d,ts),(e_term,[]))) |
|
302 else (i,v,false,sel, Sup (d,ts))) |
|
303 end; |
|
304 |
|
305 (*.generate preliminary itm_ from a strin (with field "#Given" etc.).*) |
|
306 (* val (f, str) = hd selcts; |
|
307 *) |
|
308 fun eq7 (f, d) (f', (d', _)) = f=f' andalso d=d'; |
|
309 fun fstr2itm_ thy pbt (f, str) = |
|
310 let val topt = parse thy str |
|
311 in case topt of |
|
312 NONE => ([], false, f, Syn str) |
|
313 | SOME ct => |
|
314 (* val SOME ct = parse thy str; |
|
315 *) |
|
316 let val (d,ts) = ((split_dts thy) o term_of) ct |
|
317 val popt = find_first (eq7 (f,d)) pbt |
|
318 in case popt of |
|
319 NONE => ([1](*??*), true(*??*), f, Sup (d,ts)) |
|
320 | SOME (f, (d, id)) => ([1], true, f, Cor ((d,ts), (id, ts))) |
|
321 end |
|
322 end; |
|
323 |
|
324 |
|
325 (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*) |
|
326 fun unknown_expl dI pbt selcts = |
|
327 let |
|
328 val thy = assoc_thy dI |
|
329 val its_ = map (fstr2itm_ thy pbt) selcts (*([1],true,"#Given",Cor (...))*) |
|
330 val its = add_id its_ |
|
331 in (map flattup2 its): itm list end; |
|
332 |
|
333 |
|
334 |
|
335 |
|
336 (*WN.11.03 for input_icalhd, ~ specify_additem for Add_Given/_Find/_Relation |
|
337 appl_add': generate 1 item |
|
338 appl_add' . is_known: parse, get data from oris (vats, all (elems if list)..) |
|
339 appl_add' . is_notyet_input: compare with items in model already input |
|
340 insert_ppc': insert this 1 item*) |
|
341 (* val (dI,oris,ppc,pbt,selcts) =((#1 (some_spec ospec spec)),oris,[(*!!*)], |
|
342 ((#ppc o get_pbt) (#2 (some_spec ospec spec))), |
|
343 (imodel2fstr imodel)); |
|
344 *) |
|
345 fun appl_adds dI [] _ pbt selcts = unknown_expl dI pbt selcts |
|
346 (*already present itms in model are being overwritten*) |
|
347 | appl_adds dI oris ppc pbt [] = ppc |
|
348 | appl_adds dI oris ppc pbt (selct::ss) = |
|
349 (* val selct = (sel, string_of_cterm ct); |
|
350 *) |
|
351 let val itm = appl_add' dI oris ppc pbt selct; |
|
352 in appl_adds dI oris (insert_ppc' itm ppc) pbt ss end; |
|
353 (* val (dI, oris, ppc, pbt, selct::ss) = |
|
354 (dI, pors, probl, ppc, map itms2fstr probl); |
|
355 ...vvv |
|
356 *) |
|
357 (* val (dI, oris, ppc, pbt, (selct::ss))= |
|
358 (#1 (some_spec ospec spec), oris, []:itm list, |
|
359 ((#ppc o get_pbt) (#2 (some_spec ospec spec))),(imodel2fstr imodel)); |
|
360 val iii = appl_adds dI oris ppc pbt (selct::ss); |
|
361 writeln(itms2str_ thy iii); |
|
362 |
|
363 val itm = appl_add' dI oris ppc pbt selct; |
|
364 val ppc = insert_ppc' itm ppc; |
|
365 |
|
366 val _::selct::ss = (selct::ss); |
|
367 val itm = appl_add' dI oris ppc pbt selct; |
|
368 val ppc = insert_ppc' itm ppc; |
|
369 |
|
370 val _::selct::ss = (selct::ss); |
|
371 val itm = appl_add' dI oris ppc pbt selct; |
|
372 val ppc = insert_ppc' itm ppc; |
|
373 writeln(itms2str_ thy ppc); |
|
374 |
|
375 val _::selct::ss = (selct::ss); |
|
376 val itm = appl_add' dI oris ppc pbt selct; |
|
377 val ppc = insert_ppc' itm ppc; |
|
378 *) |
|
379 |
|
380 |
|
381 fun oris2itms _ _ ([]:ori list) = ([]:itm list) |
|
382 | oris2itms pbt vat ((i,v,f,d,ts)::(os: ori list)) = |
|
383 if member op = vat v |
|
384 then (i,v,true,f,Cor ((d,ts),(e_term,[])))::(oris2itms pbt vat os) |
|
385 else oris2itms pbt vat os; |
|
386 |
|
387 fun filter_dsc oris itm = |
|
388 filter_out ((curry op= ((d_in o #5) (itm:itm))) o |
|
389 (#4:ori -> term)) oris; |
|
390 |
|
391 |
|
392 |
|
393 |
|
394 fun par2fstr ((_,_,_,f, Par s):itm) = (f, s) |
|
395 | par2fstr itm = raise error ("par2fstr: called with " ^ |
|
396 itm2str_ (thy2ctxt' "Isac") itm); |
|
397 fun itms2fstr ((_,_,_,f, Cor ((d,ts),_)):itm) = (f, comp_dts'' (d,ts)) |
|
398 | itms2fstr (_,_,_,f, Syn str) = (f, str) |
|
399 | itms2fstr (_,_,_,f, Typ str) = (f, str) |
|
400 | itms2fstr (_,_,_,f, Inc ((d,ts),_)) = (f, comp_dts'' (d,ts)) |
|
401 | itms2fstr (_,_,_,f, Sup (d,ts)) = (f, comp_dts'' (d,ts)) |
|
402 | itms2fstr (_,_,_,f, Mis (d,t)) = (f, term2str (d $ t)) |
|
403 | itms2fstr (itm as (_,_,_,f, Par _)) = |
|
404 raise error ("parsitm ("^itm2str_ (thy2ctxt' "Isac") itm ^ |
|
405 "): Par should be internal"); |
|
406 |
|
407 fun imodel2fstr iitems = |
|
408 let fun xxx is [] = is |
|
409 | xxx is ((Given strs)::iis) = |
|
410 xxx (is @ (map (pair "#Given") strs)) iis |
|
411 | xxx is ((Find strs)::iis) = |
|
412 xxx (is @ (map (pair "#Find") strs)) iis |
|
413 | xxx is ((Relate strs)::iis) = |
|
414 xxx (is @ (map (pair "#Relate") strs)) iis |
|
415 in xxx [] iitems end; |
|
416 |
|
417 (*.input a CAS-command via a whole calchead; |
|
418 dWN0602 ropped due to change of design in the front-end.*) |
|
419 (*since previous calc-head _only_ has changed: |
|
420 EITHER _1_ part of the specification OR some items in the model; |
|
421 the hdform is left as is except in cas_input .*) |
|
422 (*FIXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX___Met___XXXXXXXXXXXME.TODO.WN:11.03*) |
|
423 (* val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) = |
|
424 (p, "xxx", empty_model, Pbl, e_spec); |
|
425 val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) = |
|
426 (p,"", [Given ["fixedValues [r=Arbfix]"], |
|
427 Find ["maximum A", "valuesFor [a,b]"], |
|
428 Relate ["relations [A=a*b, a/2=r*sin alpha, \ |
|
429 \b/2=r*cos alpha]"]], Pbl, e_spec); |
|
430 val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) = |
|
431 (([],Pbl), "not used here", |
|
432 [Given ["fixedValues [r=Arbfix]"], |
|
433 Find ["maximum A", "valuesFor [a,b]"(*new input*)], |
|
434 Relate ["relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]"]], Pbl, |
|
435 ("DiffApp.thy", ["e_pblID"], ["e_metID"])); |
|
436 val ((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)) = ichd; |
|
437 *) |
|
438 fun input_icalhd pt (((p,_), hdf, imodel, Pbl, spec as (dI,pI,mI)):icalhd) = |
|
439 let val PblObj {fmz = fmz as (fmz_,_), origin = (oris, ospec, hdf'), |
|
440 spec = sspec as (sdI,spI,smI), probl, meth,...} = |
|
441 get_obj I pt p; |
|
442 in if is_casinput hdf fmz then the (cas_input (str2term hdf)) |
|
443 else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*) |
|
444 let val (pos_, pits, mits) = |
|
445 if dI <> sdI |
|
446 then let val its = map (parsitm (assoc_thy dI)) probl; |
|
447 val (its, trms) = filter_sep is_Par its; |
|
448 val pbt = (#ppc o get_pbt) (#2(some_spec ospec sspec)); |
|
449 in (Pbl, appl_adds dI oris its pbt |
|
450 (map par2fstr trms), meth) end else |
|
451 if pI <> spI |
|
452 then if pI = snd3 ospec then (Pbl, probl, meth) else |
|
453 let val pbt = (#ppc o get_pbt) pI |
|
454 val dI' = #1 (some_spec ospec spec) |
|
455 val oris = if pI = #2 ospec then oris |
|
456 else prep_ori fmz_(assoc_thy"Isac.thy") pbt; |
|
457 in (Pbl, appl_adds dI' oris probl pbt |
|
458 (map itms2fstr probl), meth) end else |
|
459 if mI <> smI (*FIXME.WN0311: what if probl is incomplete?!*) |
|
460 then let val met = (#ppc o get_met) mI |
|
461 val mits = complete_metitms oris probl meth met |
|
462 in if foldl and_ (true, map #3 mits) |
|
463 then (Pbl, probl, mits) else (Met, probl, mits) |
|
464 end else |
|
465 (Pbl, appl_adds (#1 (some_spec ospec spec)) oris [(*!!!*)] |
|
466 ((#ppc o get_pbt) (#2 (some_spec ospec spec))) |
|
467 (imodel2fstr imodel), meth); |
|
468 val pt = update_spec pt p spec; |
|
469 in if pos_ = Pbl |
|
470 then let val {prls,where_,...} = get_pbt (#2 (some_spec ospec spec)) |
|
471 val pre =check_preconds(assoc_thy"Isac.thy")prls where_ pits |
|
472 in (update_pbl pt p pits, |
|
473 (ocalhd_complete pits pre spec, |
|
474 Pbl, hdf', pits, pre, spec):ocalhd) end |
|
475 else let val {prls,pre,...} = get_met (#3 (some_spec ospec spec)) |
|
476 val pre = check_preconds (assoc_thy"Isac.thy") prls pre mits |
|
477 in (update_met pt p mits, |
|
478 (ocalhd_complete mits pre spec, |
|
479 Met, hdf', mits, pre, spec):ocalhd) end |
|
480 end end |
|
481 | input_icalhd pt ((p,_), hdf, imodel, _(*Met*), spec as (dI,pI,mI)) = |
|
482 raise error "input_icalhd Met not impl."; |
|
483 |
|
484 |
|
485 (***. handle an input formula .***) |
|
486 (* |
|
487 Untersuchung zur Formeleingabe (appendFormula, replaceFormla) zu einer Anregung von Alan Krempler: |
|
488 Welche RICHTIGEN Formeln koennen NICHT abgeleitet werden, |
|
489 wenn Abteilungen nur auf gleichem Level gesucht werden ? |
|
490 WN.040216 |
|
491 |
|
492 Beispiele zum Equationsolver von Richard Lang aus /src/sml/kbtest/rlang.sml |
|
493 |
|
494 ------------------------------------------------------------------------------ |
|
495 "Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)"; |
|
496 ------------------------------------------------------------------------------ |
|
497 1. "5 * x / (x - 2) - x / (x + 2) = 4" |
|
498 ... |
|
499 4. "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)",Subproblem["normalize", "poly".. |
|
500 ... |
|
501 4.3. "16 + 12 * x = 0", Subproblem["degree_1", "polynomial", "univariate".. |
|
502 ... |
|
503 4.3.3. "[x = -4 / 3]")), Check_elementwise "Assumptions" |
|
504 ... |
|
505 "[x = -4 / 3]" |
|
506 ------------------------------------------------------------------------------ |
|
507 (1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n] |
|
508 |
|
509 (4.1)..(4.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n] |
|
510 ------------------------------------------------------------------------------ |
|
511 |
|
512 |
|
513 ------------------------------------------------------------------------------ |
|
514 "Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)"; |
|
515 ------------------------------------------------------------------------------ |
|
516 1. "x / (x ^^^ 2 - 6 * x + 9) - 1 / (x ^^^ 2 - 3 * x) = 1 / x" |
|
517 ... |
|
518 4. "(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))" |
|
519 Subproblem["normalize", "polynomial", "univariate".. |
|
520 ... |
|
521 4.4. "-6 * x + 5 * x ^^^ 2 = 0", Subproblem["bdv_only", "degree_2", "poly".. |
|
522 ... |
|
523 4.4.4. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions" |
|
524 4.4.5. "[x = 0, x = 6 / 5]" |
|
525 ... |
|
526 5. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions" |
|
527 "[x = 6 / 5]" |
|
528 ------------------------------------------------------------------------------ |
|
529 (1)..(4): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite schiebt [Ableitung waere in 4.4.x] |
|
530 |
|
531 (4.1)..(4.4.5): keine 'richtige' Eingabe kann abgeleitet werden, die dem Ergebnis "[x = 6 / 5]" aequivalent ist [Ableitung waere in 5.] |
|
532 ------------------------------------------------------------------------------ |
|
533 |
|
534 |
|
535 ------------------------------------------------------------------------------ |
|
536 "Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))"; |
|
537 ------------------------------------------------------------------------------ |
|
538 1. "sqrt (x + 1) + sqrt (4 * x + 4) = sqrt (9 * x + 9)" |
|
539 ... |
|
540 6. "13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x" |
|
541 Subproblem["sq", "root", "univariate", "equation"] |
|
542 ... |
|
543 6.6. "144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2" |
|
544 Subproblem["normalize", "polynomial", "univariate", "equation"] |
|
545 ... |
|
546 6.6.3 "0 = 0" Subproblem["degree_0", "polynomial", "univariate", "equation"] |
|
547 ... Or_to_List |
|
548 6.6.3.2 "UniversalList" |
|
549 ------------------------------------------------------------------------------ |
|
550 (1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die eine der Wurzeln auf die andere Seite verschieb [Ableitung ware in 6.6.n] |
|
551 |
|
552 (6.1)..(6.3): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 6.6.n] |
|
553 ------------------------------------------------------------------------------ |
|
554 *) |
|
555 (*sh. comments auf 498*) |
|
556 |
|
557 fun equal a b = a=b; |
|
558 |
|
559 (*the lists contain eq-al elem-pairs at the beginning; |
|
560 return first list reverted (again) - ie. in order as required subsequently*) |
|
561 fun dropwhile' equal (f1::f2::fs) (i1::i2::is) = |
|
562 if equal f1 i1 then |
|
563 if equal f2 i2 then dropwhile' equal (f2::fs) (i2::is) |
|
564 else (rev (f1::f2::fs), i1::i2::is) |
|
565 else raise error "dropwhile': did not start with equal elements" |
|
566 | dropwhile' equal (f::fs) [i] = |
|
567 if equal f i then (rev (f::fs), [i]) |
|
568 else raise error "dropwhile': did not start with equal elements" |
|
569 | dropwhile' equal [f] (i::is) = |
|
570 if equal f i then ([f], i::is) |
|
571 else raise error "dropwhile': did not start with equal elements"; |
|
572 (* |
|
573 fun equal a b = a=b; |
|
574 val foder = [0,1,2,3,4,5]; val ifoder = [11,12,3,4,5]; |
|
575 val r_foder = rev foder; val r_ifoder = rev ifoder; |
|
576 dropwhile' equal r_foder r_ifoder; |
|
577 > vval it = ([0, 1, 2, 3], [3, 12, 11]) : int list * int list |
|
578 |
|
579 val foder = [3,4,5]; val ifoder = [11,12,3,4,5]; |
|
580 val r_foder = rev foder; val r_ifoder = rev ifoder; |
|
581 dropwhile' equal r_foder r_ifoder; |
|
582 > val it = ([3], [3, 12, 11]) : int list * int list |
|
583 |
|
584 val foder = [5]; val ifoder = [11,12,3,4,5]; |
|
585 val r_foder = rev foder; val r_ifoder = rev ifoder; |
|
586 dropwhile' equal r_foder r_ifoder; |
|
587 > val it = ([5], [5, 4, 3, 12, 11]) : int list * int list |
|
588 |
|
589 val foder = [10,11,12,13,14,15]; val ifoder = [11,12,3,4,5]; |
|
590 val r_foder = rev foder; val r_ifoder = rev ifoder; |
|
591 dropwhile' equal r_foder r_ifoder; |
|
592 > *** dropwhile': did not start with equal elements*) |
|
593 |
|
594 (*040214: version for concat_deriv*) |
|
595 fun rev_deriv' (t, r, (t', a)) = (t', sym_Thm r, (t, a)); |
|
596 |
|
597 fun mk_tacis ro erls (t, r as Thm _, (t', a)) = |
|
598 (Rewrite (rule2thm' r), |
|
599 Rewrite' ("Isac.thy", fst ro, erls, false, |
|
600 rule2thm' r, t, (t', a)), |
|
601 (e_pos'(*to be updated before generate tacis!!!*), Uistate)) |
|
602 | mk_tacis ro erls (t, r as Rls_ rls, (t', a)) = |
|
603 (Rewrite_Set (rule2rls' r), |
|
604 Rewrite_Set' ("Isac.thy", false, rls, t, (t', a)), |
|
605 (e_pos'(*to be updated before generate tacis!!!*), Uistate)); |
|
606 |
|
607 (*fo = ifo excluded already in inform*) |
|
608 fun concat_deriv rew_ord erls rules fo ifo = |
|
609 let fun derivat ([]:(term * rule * (term * term list)) list) = e_term |
|
610 | derivat dt = (#1 o #3 o last_elem) dt |
|
611 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2 |
|
612 val fod = make_deriv (Isac"") erls rules (snd rew_ord) NONE fo |
|
613 val ifod = make_deriv (Isac"") erls rules (snd rew_ord) NONE ifo |
|
614 in case (fod, ifod) of |
|
615 ([], []) => if fo = ifo then (true, []) |
|
616 else (false, []) |
|
617 | (fod, []) => if derivat fod = ifo |
|
618 then (true, fod) (*ifo is normal form*) |
|
619 else (false, []) |
|
620 | ([], ifod) => if fo = derivat ifod |
|
621 then (true, ((map rev_deriv') o rev) ifod) |
|
622 else (false, []) |
|
623 | (fod, ifod) => |
|
624 if derivat fod = derivat ifod (*common normal form found*) |
|
625 then let val (fod', rifod') = |
|
626 dropwhile' equal (rev fod) (rev ifod) |
|
627 in (true, fod' @ (map rev_deriv' rifod')) end |
|
628 else (false, []) |
|
629 end; |
|
630 (* |
|
631 val ({rew_ord, erls, rules,...}, fo, ifo) = |
|
632 (rep_rls Test_simplify, str2term "x+1+ -1*2=0", str2term "-2*1+(x+1)=0"); |
|
633 (writeln o trtas2str) fod'; |
|
634 > [" |
|
635 (x + 1 + -1 * 2 = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (x + 1) = 0, []))"," |
|
636 (-1 * 2 + (x + 1) = 0, Thm ("radd_commute","?m + ?n = ?n + ?m"), (-1 * 2 + (1 + x) = 0, []))"," |
|
637 (-1 * 2 + (1 + x) = 0, Thm ("radd_left_commute","?x + (?y + ?z) = ?y + (?x + ?z)"), (1 + (-1 * 2 + x) = 0, []))"," |
|
638 (1 + (-1 * 2 + x) = 0, Thm ("#mult_Float ((~1,0), (0,0)) __ ((2,0), (0,0))","-1 * 2 = -2"), (1 + (-2 + x) = 0, []))"] |
|
639 val it = () : unit |
|
640 (writeln o trtas2str) (map rev_deriv' rifod'); |
|
641 > [" |
|
642 (1 + (-2 + x) = 0, Thm ("sym_#mult_Float ((~2,0), (0,0)) __ ((1,0), (0,0))","-2 = -2 * 1"), (1 + (-2 * 1 + x) = 0, []))"," |
|
643 (1 + (-2 * 1 + x) = 0, Thm ("sym_radd_left_commute","?y + (?x + ?z) = ?x + (?y + ?z)"), (-2 * 1 + (1 + x) = 0, []))"," |
|
644 (-2 * 1 + (1 + x) = 0, Thm ("sym_radd_commute","?n + ?m = ?m + ?n"), (-2 * 1 + (x + 1) = 0, []))"] |
|
645 val it = () : unit |
|
646 *) |
|
647 |
|
648 |
|
649 (*.compare inform with ctree.form at current pos by nrls; |
|
650 if found, embed the derivation generated during comparison |
|
651 if not, let the mat-engine compute the next ctree.form.*) |
|
652 (*structure copied from complete_solve |
|
653 CAUTION: tacis in returned calcstate' do NOT construct resulting ptp -- |
|
654 all_modspec etc. has to be inserted at Subproblem'*) |
|
655 (* val (tacis, c, ptp as (pt, pos as (p,p_))) = (tacis, ptp); |
|
656 val (tacis, c, ptp as (pt, pos as (p,p_))) = cs'; |
|
657 |
|
658 val (tacis, c, ptp as (pt, pos as (p,p_))) = ([],[],(pt, lev_back pos)); |
|
659 -----rec.call: |
|
660 val (tacis, c, ptp as (pt, pos as (p,p_))) = cs'; |
|
661 *) |
|
662 fun compare_step ((tacis, c, ptp as (pt, pos as (p,p_))): calcstate') ifo = |
|
663 let val fo = case p_ of Frm => get_obj g_form pt p |
|
664 | Res => (fst o (get_obj g_result pt)) p |
|
665 | _ => e_term (*on PblObj is fo <> ifo*); |
|
666 val {nrls,...} = get_met (get_obj g_metID pt (par_pblobj pt p)) |
|
667 val {rew_ord, erls, rules,...} = rep_rls nrls |
|
668 val (found, der) = concat_deriv rew_ord erls rules fo ifo; |
|
669 in if found |
|
670 then let val tacis' = map (mk_tacis rew_ord erls) der; |
|
671 val (c', ptp) = embed_deriv tacis' ptp; |
|
672 in ("ok", (tacis (*@ tacis'?WN050408*), c @ c', ptp)) end |
|
673 else |
|
674 if pos = ([], Res) |
|
675 then ("no derivation found", (tacis, c, ptp): calcstate') |
|
676 else let val cs' as (tacis, c', ptp) = nxt_solve_ ptp; |
|
677 val cs' as (tacis, c'', ptp) = |
|
678 case tacis of |
|
679 ((Subproblem _, _, _)::_) => |
|
680 let val ptp as (pt, (p,_)) = all_modspec ptp |
|
681 val mI = get_obj g_metID pt p |
|
682 in nxt_solv (Apply_Method' (mI, NONE, e_istate)) |
|
683 e_istate ptp end |
|
684 | _ => cs'; |
|
685 in compare_step (tacis, c @ c' @ c'', ptp) ifo end |
|
686 end; |
|
687 (* writeln (trtas2str der); |
|
688 *) |
|
689 |
|
690 (*.handle a user-input formula, which may be a CAS-command, too. |
|
691 CAS-command: |
|
692 create a calchead, and do 1 step |
|
693 TOOODO.WN0602 works only for the root-problem !!! |
|
694 formula, which is no CAS-command: |
|
695 compare iform with calc-tree.form at pos by equ_nrls and all subsequent pos; |
|
696 collect all the tacs applied by the way.*) |
|
697 (*structure copied from autocalc*) |
|
698 (* val (cs as (_, _, (pt, pos as (p, p_))): calcstate') = cs'; |
|
699 val ifo = str2term ifo; |
|
700 |
|
701 val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) = |
|
702 (cs', encode ifo); |
|
703 val ((cs as (_, _, ptp as (pt, pos as (p, p_)))), istr)=(cs', (encode ifo)); |
|
704 val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) = |
|
705 (([],[],(pt,p)), (encode ifo)); |
|
706 *) |
|
707 fun inform (cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate') istr = |
|
708 case parse (assoc_thy "Isac.thy") istr of |
|
709 (* val SOME ifo = parse (assoc_thy "Isac.thy") istr; |
|
710 *) |
|
711 SOME ifo => |
|
712 let val ifo = term_of ifo |
|
713 val fo = case p_ of Frm => get_obj g_form pt p |
|
714 | Res => (fst o (get_obj g_result pt)) p |
|
715 | _ => #3 (get_obj g_origin pt p) |
|
716 in if fo = ifo |
|
717 then ("same-formula", cs) |
|
718 (*thus ctree not cut with replaceFormula!*) |
|
719 else case cas_input ifo of |
|
720 (* val SOME (pt, _) = cas_input ifo; |
|
721 *) |
|
722 SOME (pt, _) => ("ok",([],[],(pt, (p, Met)))) |
|
723 | NONE => |
|
724 compare_step ([],[],(pt, |
|
725 (*last step re-calc in compare_step TODO*) |
|
726 lev_back pos)) ifo |
|
727 end |
|
728 | NONE => ("syntax error in '"^istr^"'", e_calcstate'); |
|
729 |
|
730 |
|
731 (*------------------------------------------------------------------(**) |
|
732 end |
|
733 open inform; |
|
734 (**)------------------------------------------------------------------*) |