1 (* Handle user-input during the specify- and the solve-phase.
4 (c) due to copyright terms
20 | Given of cterm' list
21 | Relate of cterm' list
23 val imodel2fstr : iitem list -> (string * cterm') list
26 val Isac : 'a -> theory
29 SpecifyTools.ori list ->
30 SpecifyTools.itm list ->
31 ('a * (Term.term * Term.term)) list ->
32 string * cterm' -> SpecifyTools.itm
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 *)
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 Unsynchronized.ref
47 calcstate' -> Term.term -> string * calcstate'
49 'a * ((Term.term * Term.term) list -> Term.term * Term.term -> bool)
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
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
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 *)
71 (''a * (Term.term * Term.term)) list ->
72 ''a * string -> int list * bool * ''a * SpecifyTools.itm_ *)
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 *)
83 Term.term * rule * (Term.term * Term.term list) ->
84 tac * tac_ * (pos' * istate) *)
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)
92 (string * (Term.term * Term.term)) list ->
93 (string * string) list -> SpecifyTools.itm list *)
101 (***. handle an input calc-head .***)
103 (*------------------------------------------------------------------(**)
104 structure inform :INFORM =
106 (**)------------------------------------------------------------------*)
110 (*Where is never input*)
111 | Find of cterm' list
112 | Relate of cterm' list;
114 type imodel = iitem list;
116 (*calc-head as input*)
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;
126 fun is_casinput (hdf: cterm') ((fmz_, spec): fmz) =
127 hdf <> "" andalso fmz_ = [] andalso spec = e_spec;
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;
136 fun flattup2 (a,(b,c,d,e)) = (a,b,c,d,e);
140 (*.association list with cas-commands, for generating a complete calc-head.*)
142 (term * (*cas-command, eg. 'solve'*)
143 (spec * (*theory, problem, method*)
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*)
152 val castab = Unsynchronized.ref ([]: castab);
156 (* val (dI,pI,mI) = spec;
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;*)
174 (* val (dI,pI,mI) = spec;
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;
194 (*.check if the input term is a CAScmd and return a ptree with
195 a _complete_ calchead.*)
199 let val (h,argl) = strip_comb hdt
200 in case assoc (!castab, h) of
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);
210 let val dtss = argl2dtss argl
211 val (pI, pits, mI, mits, pre) = cas_input_ spec dtss
212 val spec = (dI, pI, mI)
214 cappend_problem e_ptree [] e_istate ([], e_spec)
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
222 (*lazy evaluation for Isac.thy*)
223 fun Isac _ = assoc_thy "Isac.thy";
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;
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'))) =
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 error ("parsitm (" ^ itm2str_ (thy2ctxt dI) itm^
256 "): Par should be internal");
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
269 fun is_e_ts [] = true
270 | is_e_ts [Const ("List.list.Nil", _)] = true
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));
280 fun appl_add' dI oris ppc pbt (sel, ct) =
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;
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);
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;
295 (* val (msg,xx) = is_notyet_input thy ppc all ori' pbt;
297 | (msg,_) => error ("appl_add': "^msg))
298 (* val (msg,(_,_,_,d,ts),all) = is_known thy sel oris (term_of ct);
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)))
305 (*.generate preliminary itm_ from a strin (with field "#Given" etc.).*)
306 (* val (f, str) = hd selcts;
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
312 NONE => ([], false, f, Syn str)
314 (* val SOME ct = parse thy str;
316 let val (d,ts) = ((split_dts thy) o term_of) ct
317 val popt = find_first (eq7 (f,d)) pbt
319 NONE => ([1](*??*), true(*??*), f, Sup (d,ts))
320 | SOME (f, (d, id)) => ([1], true, f, Cor ((d,ts), (id, ts)))
325 (*.input into empty PblObj, i.e. empty fmz+origin (unknown example).*)
326 fun unknown_expl dI pbt selcts =
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;
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));
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);
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);
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 tracing(itms2str_ thy iii);
363 val itm = appl_add' dI oris ppc pbt selct;
364 val ppc = insert_ppc' itm ppc;
366 val _::selct::ss = (selct::ss);
367 val itm = appl_add' dI oris ppc pbt selct;
368 val ppc = insert_ppc' itm ppc;
370 val _::selct::ss = (selct::ss);
371 val itm = appl_add' dI oris ppc pbt selct;
372 val ppc = insert_ppc' itm ppc;
373 tracing(itms2str_ thy ppc);
375 val _::selct::ss = (selct::ss);
376 val itm = appl_add' dI oris ppc pbt selct;
377 val ppc = insert_ppc' itm ppc;
381 fun oris2itms _ _ ([]:ori list) = ([]:itm list)
382 | oris2itms pbt vat ((i,v,f,d,ts)::(os: ori list)) =
384 then (i,v,true,f,Cor ((d,ts),(e_term,[])))::(oris2itms pbt vat os)
385 else oris2itms pbt vat os;
387 fun filter_dsc oris itm =
388 filter_out ((curry op= ((d_in o #5) (itm:itm))) o
389 (#4:ori -> term)) oris;
394 fun par2fstr ((_,_,_,f, Par s):itm) = (f, s)
395 | par2fstr itm = 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 error ("parsitm ("^itm2str_ (thy2ctxt' "Isac") itm ^
405 "): Par should be internal");
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;
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;
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,...} =
442 in if is_casinput hdf fmz then the (cas_input (str2term hdf))
443 else (*hacked WN0602 ~~~ ~~~~~~~~~, ..dropped !*)
444 let val (pos_, pits, mits) =
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
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)
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;
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
481 | input_icalhd pt ((p,_), hdf, imodel, _(*Met*), spec as (dI,pI,mI)) =
482 error "input_icalhd Met not impl.";
485 (***. handle an input formula .***)
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 ?
492 Beispiele zum Equationsolver von Richard Lang aus /src/sml/kbtest/rlang.sml
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"
499 4. "12 * x + 4 * x ^^^ 2 = 4 * (-4 + x ^^^ 2)",Subproblem["normalize", "poly"..
501 4.3. "16 + 12 * x = 0", Subproblem["degree_1", "polynomial", "univariate"..
503 4.3.3. "[x = -4 / 3]")), Check_elementwise "Assumptions"
506 ------------------------------------------------------------------------------
507 (1)..(6): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite verschiebt [Ableitung ware in 4.3.n]
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 ------------------------------------------------------------------------------
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"
518 4. "(3 + (-1 * x + x ^^^ 2)) * x = 1 * (9 * x + (x ^^^ 3 + -6 * x ^^^ 2))"
519 Subproblem["normalize", "polynomial", "univariate"..
521 4.4. "-6 * x + 5 * x ^^^ 2 = 0", Subproblem["bdv_only", "degree_2", "poly"..
523 4.4.4. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
524 4.4.5. "[x = 0, x = 6 / 5]"
526 5. "[x = 0, x = 6 / 5]", Check_elementwise "Assumptions"
528 ------------------------------------------------------------------------------
529 (1)..(4): keine 'richtige' Eingabe kann abgeleitet werden, die einen Summanden auf die andere Seite schiebt [Ableitung waere in 4.4.x]
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 ------------------------------------------------------------------------------
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)"
540 6. "13 + 13 * x + -2 * sqrt ((4 + 4 * x) * (9 + 9 * x)) = 1 + x"
541 Subproblem["sq", "root'", "univariate", "equation"]
543 6.6. "144 + 288 * x + 144 * x ^^^ 2 = 144 + x ^^^ 2 + 288 * x + 143 * x ^^^ 2"
544 Subproblem["normalize", "polynomial", "univariate", "equation"]
546 6.6.3 "0 = 0" Subproblem["degree_0", "polynomial", "univariate", "equation"]
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]
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 ------------------------------------------------------------------------------
555 (*sh. comments auf 498*)
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) =
563 if equal f2 i2 then dropwhile' equal (f2::fs) (i2::is)
564 else (rev (f1::f2::fs), i1::i2::is)
565 else 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 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 error "dropwhile': did not start with equal elements";
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
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
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
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*)
594 (*040214: version for concat_deriv*)
595 fun rev_deriv' (t, r, (t', a)) = (t', sym_Thm r, (t, a));
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));
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, [])
617 | (fod, []) => if derivat fod = ifo
618 then (true, fod) (*ifo is normal form*)
620 | ([], ifod) => if fo = derivat ifod
621 then (true, ((map rev_deriv') o rev) 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
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 (tracing o trtas2str) fod';
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, []))"]
640 (tracing o trtas2str) (map rev_deriv' rifod');
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, []))"]
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';
658 val (tacis, c, ptp as (pt, pos as (p,p_))) = ([],[],(pt, lev_back pos));
660 val (tacis, c, ptp as (pt, pos as (p,p_))) = cs';
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;
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
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) =
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))
685 in compare_step (tacis, c @ c' @ c'', ptp) ifo end
687 (* tracing (trtas2str der);
690 (*.handle a user-input formula, which may be a CAS-command, too.
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;
701 val ((cs as (_, _, ptp as (pt, pos as (p, p_))): calcstate'), istr) =
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));
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;
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)
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;
722 SOME (pt, _) => ("ok",([],[],(pt, (p, Met))))
724 compare_step ([],[],(pt,
725 (*last step re-calc in compare_step TODO*)
728 | NONE => ("syntax error in '"^istr^"'", e_calcstate');
731 (*------------------------------------------------------------------(**)
734 (**)------------------------------------------------------------------*)