339 val t2 = (term_of o hd o tl) chkmodel; |
339 val t2 = (term_of o hd o tl) chkmodel; |
340 val t3 = (term_of o hd o tl o tl) chkmodel; |
340 val t3 = (term_of o hd o tl o tl) chkmodel; |
341 case t3 of Const ("Integrate.antiDerivative", _) $ _ => () |
341 case t3 of Const ("Integrate.antiDerivative", _) $ _ => () |
342 | _ => error "integrate.sml: Integrate.antiDerivative ???"; |
342 | _ => error "integrate.sml: Integrate.antiDerivative ???"; |
343 |
343 |
344 (*=== inhibit exn ?============================================================= |
|
345 val model = {Given =["functionTerm f_f", "integrateBy v_v"], |
344 val model = {Given =["functionTerm f_f", "integrateBy v_v"], |
346 Where =[], |
345 Where =[], |
347 Find =["antiDerivativeName F_"], |
346 Find =["antiDerivativeName F_F"], |
348 With =[], |
347 With =[], |
349 Relate=[]}:string ppc; |
348 Relate=[]}:string ppc; |
350 val chkmodel = ((map (the o (parse thy))) o ppc2list) model; |
349 val chkmodel = ((map (the o (parse thy))) o ppc2list) model; |
351 val t1 = (term_of o hd) chkmodel; |
350 val t1 = (term_of o hd) chkmodel; |
352 val t2 = (term_of o hd o tl) chkmodel; |
351 val t2 = (term_of o hd o tl) chkmodel; |
355 | _ => error "integrate.sml: Integrate.antiDerivativeName"; |
354 | _ => error "integrate.sml: Integrate.antiDerivativeName"; |
356 |
355 |
357 "----- compare 'Find's from problem, script, formalization -------"; |
356 "----- compare 'Find's from problem, script, formalization -------"; |
358 val {ppc,...} = get_pbt ["named","integrate","function"]; |
357 val {ppc,...} = get_pbt ["named","integrate","function"]; |
359 val ("#Find", (Const ("Integrate.antiDerivativeName", _), |
358 val ("#Find", (Const ("Integrate.antiDerivativeName", _), |
360 F1_ as Free ("F_", F1_type))) = last_elem ppc; |
359 F1_ as Free ("F_F", F1_type))) = last_elem ppc; |
361 val {scr = Script sc,... } = get_met ["diff","integration","named"]; |
360 val {scr = Script sc,... } = get_met ["diff","integration","named"]; |
362 val [_,_, F2_] = formal_args sc; |
361 val [_,_, F2_] = formal_args sc; |
363 if F1_ = F2_ then () else error "integrate.sml: unequal find's"; |
362 if F1_ = F2_ then () else error "integrate.sml: unequal find's"; |
364 |
363 |
365 val ((dsc as Const ("Integrate.antiDerivativeName", _)) |
364 val ((dsc as Const ("Integrate.antiDerivativeName", _)) |
377 "----------- check Scripts ------------------------------"; |
376 "----------- check Scripts ------------------------------"; |
378 "----------- check Scripts ------------------------------"; |
377 "----------- check Scripts ------------------------------"; |
379 "----------- check Scripts ------------------------------"; |
378 "----------- check Scripts ------------------------------"; |
380 val str = |
379 val str = |
381 "Script IntegrationScript (f_f::real) (v_v::real) = \ |
380 "Script IntegrationScript (f_f::real) (v_v::real) = \ |
382 \ (let t_ = Take (Integral f_ D v_v) \ |
381 \ (let t_t = Take (Integral f_f D v_v) \ |
383 \ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))"; |
382 \ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_t::real))"; |
384 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
383 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
385 atomty sc; |
384 atomty sc; |
386 |
385 |
387 val str = |
386 val str = |
388 "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_::real=>real) = \ |
387 "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = \ |
389 \ (let t_ = Take (F_ v_v = Integral f_ D v_v) \ |
388 \ (let t_t = Take (F_F v_v = Integral f_f D v_v) \ |
390 \ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_)"; |
389 \ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_t)"; |
391 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
390 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
392 atomty sc; |
391 atomty sc; |
393 show_mets(); |
392 show_mets(); |
394 |
393 |
395 |
394 |
416 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
415 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f; |
417 if f2str f = "c + x + 1 / 3 * x ^^^ 3" then () |
416 if f2str f = "c + x + 1 / 3 * x ^^^ 3" then () |
418 else error "integrate.sml: method [diff,integration]"; |
417 else error "integrate.sml: method [diff,integration]"; |
419 |
418 |
420 |
419 |
|
420 (*=== inhibit exn ?============================================================= |
421 "----------- me method [diff,integration,named] ---------"; |
421 "----------- me method [diff,integration,named] ---------"; |
422 "----------- me method [diff,integration,named] ---------"; |
422 "----------- me method [diff,integration,named] ---------"; |
423 "----------- me method [diff,integration,named] ---------"; |
423 "----------- me method [diff,integration,named] ---------"; |
424 (*exp_CalcInt_No-2.xml*) |
424 (*exp_CalcInt_No-2.xml*) |
425 val fmz = ["functionTerm (x^^^2 + 1)", |
425 val fmz = ["functionTerm (x^^^2 + 1)", |
494 "----------- method analog to rls 'integration' ---------"; |
494 "----------- method analog to rls 'integration' ---------"; |
495 store_met |
495 store_met |
496 (prep_met thy "met_testint" [] e_metID |
496 (prep_met thy "met_testint" [] e_metID |
497 (["diff","integration","test"], |
497 (["diff","integration","test"], |
498 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
498 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
499 ("#Find" ,["antiDerivative F_"]) |
499 ("#Find" ,["antiDerivative F_F"]) |
500 ], |
500 ], |
501 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], |
501 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], |
502 srls = e_rls, |
502 srls = e_rls, |
503 prls=e_rls, |
503 prls=e_rls, |
504 crls = Atools_erls, nrls = e_rls}, |
504 crls = Atools_erls, nrls = e_rls}, |