# HG changeset patch # User Walther Neuper # Date 1285239411 -7200 # Node ID e4f42a63d6656af68505f77d546adf2c01b8206c # Parent f57ddfd09474355e58bb91a224ce69a26bb759e0 interrupted update test/../Knowledge/integrate.sml, repaired term2str term2str by help from Florian and Jasmin; took the former. Found at that point in integrate.sml, that all "op +" etc need to be updated. diff -r f57ddfd09474 -r e4f42a63d665 src/Tools/isac/calcelems.sml --- a/src/Tools/isac/calcelems.sml Thu Sep 23 08:54:26 2010 +0200 +++ b/src/Tools/isac/calcelems.sml Thu Sep 23 12:56:51 2010 +0200 @@ -601,7 +601,12 @@ fun termopt2str (SOME t) = "SOME " ^ (Syntax.string_of_term (thy2ctxt' "Isac") t) | termopt2str NONE = "NONE"; -fun term2str t = Syntax.string_of_term (thy2ctxt' "Isac") t; +(*fun term2str t = Syntax.string_of_term (thy2ctxt' "Isac") t; Isa2002*) +(*Florian1009: 'val' would ensure static lookup, i.e. only at compile time; + however, dynamic lookup is required, since "Isac" is not yet built here.*) +fun term2str t = Print_Mode.setmp [] (Syntax.string_of_term +(ProofContext.init_global (Thy_Info.get_theory "Isac"))) t; + fun terms2str ts= (strs2str o (map (Syntax.string_of_term (thy2ctxt' "Isac")))) ts; fun type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ; diff -r f57ddfd09474 -r e4f42a63d665 test/Tools/isac/Knowledge/integrate.sml --- a/test/Tools/isac/Knowledge/integrate.sml Thu Sep 23 08:54:26 2010 +0200 +++ b/test/Tools/isac/Knowledge/integrate.sml Thu Sep 23 12:56:51 2010 +0200 @@ -8,35 +8,35 @@ *) val thy = theory "Integrate"; -"-----------------------------------------------------------------"; -"table of contents -----------------------------------------------"; -"-----------------------------------------------------------------"; -"----------- parsing ---------------------------------------------"; -"----------- integrate by rewriting ------------------------------"; -"----------- test add_new_c, is_f_x ------------------------------"; -"----------- simplify by ruleset reducing make_ratpoly_in --------"; -"----------- simplify by ruleset extending make_polynomial_in ----"; -"----------- integrate by ruleset --------------------------------"; -"----------- rewrite 3rd integration in 7.27 ---------------------"; -"----------- check probem type -----------------------------------"; -"----------- check Scripts ---------------------------------------"; -"----------- me method [diff,integration] ------------------------"; -"----------- me method [diff,integration,named] ------------------"; -"----------- me method [diff,integration,named] Biegelinie.Q -----"; -"----------- interSteps [diff,integration] -----------------------"; -"----------- method analog to rls 'integration' ------------------"; -"----------- Ambiguous input: Integral ?u + ?v D ?bdv = ..--------"; -"----------- CAS input -------------------------------------------"; -"-----------------------------------------------------------------"; -"-----------------------------------------------------------------"; -"-----------------------------------------------------------------"; +"--------------------------------------------------------"; +"table of contents --------------------------------------"; +"--------------------------------------------------------"; +"----------- parsing ------------------------------------"; +"----------- integrate by rewriting ---------------------"; +"----------- test add_new_c, is_f_x ---------------------"; +"----------- simplify by ruleset reducing make_ratpoly_in"; +"----------- simplify by extending make_polynomial_in ---"; +"----------- integrate by ruleset -----------------------"; +"----------- rewrite 3rd integration in 7.27 ------------"; +"----------- check probem type --------------------------"; +"----------- check Scripts ------------------------------"; +"----------- me method [diff,integration] ---------------"; +"----------- me method [diff,integration,named] ---------"; +"----------- me met [diff,integration,named] Biegelinie.Q"; +"----------- interSteps [diff,integration] --------------"; +"----------- method analog to rls 'integration' ---------"; +"----------- Ambiguous input: Integral ?u + ?v D ?bdv = ."; +"----------- CAS input ----------------------------------"; +"--------------------------------------------------------"; +"--------------------------------------------------------"; +"--------------------------------------------------------"; -"----------- parsing ---------------------------------------------"; -"----------- parsing ---------------------------------------------"; -"----------- parsing ---------------------------------------------"; -fun str2term str = (term_of o the o (parse Integrate.thy)) str; +"----------- parsing ------------------------------------"; +"----------- parsing ------------------------------------"; +"----------- parsing ------------------------------------"; +fun str2term str = (term_of o the o (parse thy)) str; fun term2s t = Syntax.string_of_term (thy2ctxt' "Integrate") t; val t = str2term "Integral x D x"; @@ -48,9 +48,9 @@ | _ => raise error "integrate.sml: parsing: ff x is_f_x"; -"----------- integrate by rewriting ------------------------------"; -"----------- integrate by rewriting ------------------------------"; -"----------- integrate by rewriting ------------------------------"; +"----------- integrate by rewriting ---------------------"; +"----------- integrate by rewriting ---------------------"; +"----------- integrate by rewriting ---------------------"; val conditions_in_integration_rules = Rls {id="conditions_in_integration_rules", preconds = [], @@ -66,38 +66,50 @@ scr = EmptyScr}; val subs = [(str2term "bdv", str2term "x")]; fun rewrit thm str = - fst (the (rewrite_inst_ Integrate.thy tless_true + fst (the (rewrite_inst_ thy tless_true conditions_in_integration_rules true subs thm str)); -val str = rewrit integral_const (str2term "Integral 1 D x"); term2s str; -val str = rewrit integral_const (str2term "Integral M'/EJ D x"); term2s str; -val str = (rewrit integral_const (str2term "Integral x D x")) +val str = rewrit @{thm "integral_const"} (str2term "Integral 1 D x"); +term2s str; +val str = rewrit @{thm "integral_const"} (str2term "Integral M'/EJ D x"); +term2s str; +val str = (rewrit @{thm "integral_const"} (str2term "Integral x D x")) handle OPTION => str2term "no_rewrite"; -val str = rewrit integral_var (str2term "Integral x D x"); term2s str; -val str = (rewrit integral_var (str2term "Integral a D x")) +val str = rewrit @{thm "integral_var"} (str2term "Integral x D x"); +term2s str; +val str = (rewrit @{thm "integral_var"} (str2term "Integral a D x")) handle OPTION => str2term "no_rewrite"; -val str = rewrit integral_add (str2term "Integral x + 1 D x"); term2s str; +val str = rewrit @{thm "integral_add"} (str2term "Integral x + 1 D x"); +term2s str; -val str = rewrit integral_mult (str2term "Integral M'/EJ * x^^^3 D x");term2s str; -val str = (rewrit integral_mult (str2term "Integral x * x D x")) +val str = rewrit @{thm "integral_mult"} (str2term "Integral M'/EJ * x^^^3 D x"); +term2s str; +val str = (rewrit @{thm "integral_mult"} (str2term "Integral x * x D x")) handle OPTION => str2term "no_rewrite"; -val str = rewrit integral_pow (str2term "Integral x^^^3 D x"); term2s str; +val str = rewrit @{thm "integral_pow"} (str2term "Integral x^^^3 D x"); +term2s str; -"----------- test add_new_c, is_f_x ------------------------------"; -"----------- test add_new_c, is_f_x ------------------------------"; -"----------- test add_new_c, is_f_x ------------------------------"; +"----------- test add_new_c, is_f_x ---------------------"; +"----------- test add_new_c, is_f_x ---------------------"; +"----------- test add_new_c, is_f_x ---------------------"; val term = str2term "x^^^2*c + c_2"; val cc = new_c term; if term2str cc = "c_3" then () else raise error "integrate.sml: new_c ???"; val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy; +"####1###################################################"; +term2str t' = "x ^^^ 2 * c + c_2 = op + (x ^^^ 2 * c + c_2) c_3" --REDO "op +"; +"####2###################################################"; + if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then () else raise error "intergrate.sml: diff. eval_add_new_c"; +"####3###################################################"; + val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_"); val SOME (thmstr, thm) = get_calculation1_ thy cc term; @@ -151,7 +163,7 @@ ], scr = EmptyScr}; fun rewrit thm t = - fst (the (rewrite_inst_ Integrate.thy tless_true + fst (the (rewrite_inst_ thy tless_true conditions_in_integration true subs thm t)); val t = rewrit call_for_new_c (str2term "x ^^^ 2 / 2"); term2s t; val t = (rewrit call_for_new_c t) @@ -165,9 +177,9 @@ --------------------------------------------------------------------*) -"----------- simplify by ruleset reducing make_ratpoly_in --------"; -"----------- simplify by ruleset reducing make_ratpoly_in --------"; -"----------- simplify by ruleset reducing make_ratpoly_in --------"; +"----------- simplify by ruleset reducing make_ratpoly_in"; +"----------- simplify by ruleset reducing make_ratpoly_in"; +"----------- simplify by ruleset reducing make_ratpoly_in"; val thy = Isac.thy; val subs = [(str2term"bdv",str2term"x")]; val t = str2term "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)"; @@ -234,17 +246,17 @@ -"----------- simplify by ruleset extending make_polynomial_in ----"; -"----------- simplify by ruleset extending make_polynomial_in ----"; -"----------- simplify by ruleset extending make_polynomial_in ----"; +"----------- simplify by extending make_polynomial_in ---"; +"----------- simplify by extending make_polynomial_in ---"; +"----------- simplify by extending make_polynomial_in ---"; trace_rewrite:=true; trace_rewrite:=false; (*postponed: see *) -"----------- integrate by ruleset --------------------------------"; -"----------- integrate by ruleset --------------------------------"; -"----------- integrate by ruleset --------------------------------"; +"----------- integrate by ruleset -----------------------"; +"----------- integrate by ruleset -----------------------"; +"----------- integrate by ruleset -----------------------"; val rls = "integration_rules"; val subs = [("bdv","x::real")]; fun rewrit_sinst subs rls str = @@ -294,9 +306,9 @@ then () else raise error "integrate.sml: diff.behav. in integration #4"; -"----------- rewrite 3rd integration in 7.27 ---------------------"; -"----------- rewrite 3rd integration in 7.27 ---------------------"; -"----------- rewrite 3rd integration in 7.27 ---------------------"; +"----------- rewrite 3rd integration in 7.27 ------------"; +"----------- rewrite 3rd integration in 7.27 ------------"; +"----------- rewrite 3rd integration in 7.27 ------------"; val thy = Isac.thy (*because of Undeclared constant "Biegelinie.EI*); val bdv = [(str2term"bdv", str2term"x")]; val t = str2term @@ -311,15 +323,15 @@ then () else raise error "integrate.sml 3rd integration in 7.27, integration"; -"----------- check probem type -----------------------------------"; -"----------- check probem type -----------------------------------"; -"----------- check probem type -----------------------------------"; +"----------- check probem type --------------------------"; +"----------- check probem type --------------------------"; +"----------- check probem type --------------------------"; val model = {Given =["functionTerm f_f", "integrateBy v_v"], Where =[], Find =["antiDerivative F_"], With =[], Relate=[]}:string ppc; -val chkmodel = ((map (the o (parse Integrate.thy))) o ppc2list) model; +val chkmodel = ((map (the o (parse thy))) o ppc2list) model; val t1 = (term_of o hd) chkmodel; val t2 = (term_of o hd o tl) chkmodel; val t3 = (term_of o hd o tl o tl) chkmodel; @@ -331,7 +343,7 @@ Find =["antiDerivativeName F_"], With =[], Relate=[]}:string ppc; -val chkmodel = ((map (the o (parse Integrate.thy))) o ppc2list) model; +val chkmodel = ((map (the o (parse thy))) o ppc2list) model; val t1 = (term_of o hd) chkmodel; val t2 = (term_of o hd o tl) chkmodel; val t3 = (term_of o hd o tl o tl) chkmodel; @@ -358,9 +370,9 @@ | _ => raise error "integrate.sml: Integrate.Integrate ???"; -"----------- check Scripts ---------------------------------------"; -"----------- check Scripts ---------------------------------------"; -"----------- check Scripts ---------------------------------------"; +"----------- check Scripts ------------------------------"; +"----------- check Scripts ------------------------------"; +"----------- check Scripts ------------------------------"; val str = "Script IntegrationScript (f_f::real) (v_v::real) = \ \ (let t_ = Take (Integral f_ D v_v) \ @@ -377,9 +389,9 @@ show_mets(); -"----------- me method [diff,integration] ---------------------"; -"----------- me method [diff,integration] ---------------------"; -"----------- me method [diff,integration] ---------------------"; +"----------- me method [diff,integration] ---------------"; +"----------- me method [diff,integration] ---------------"; +"----------- me method [diff,integration] ---------------"; (*exp_CalcInt_No-1.xml*) val fmz = ["functionTerm (x^^^2 + 1)", "integrateBy x","antiDerivative FF"]; @@ -402,9 +414,9 @@ else raise error "integrate.sml: method [diff,integration]"; -"----------- me method [diff,integration,named] ------------------"; -"----------- me method [diff,integration,named] ------------------"; -"----------- me method [diff,integration,named] ------------------"; +"----------- me method [diff,integration,named] ---------"; +"----------- me method [diff,integration,named] ---------"; +"----------- me method [diff,integration,named] ---------"; (*exp_CalcInt_No-2.xml*) val fmz = ["functionTerm (x^^^2 + 1)", "integrateBy x","antiDerivativeName F"]; @@ -427,9 +439,9 @@ else raise error "integrate.sml: method [diff,integration,named]"; -"----------- me method [diff,integration,named] Biegelinie.Q -----"; -"----------- me method [diff,integration,named] Biegelinie.Q -----"; -"----------- me method [diff,integration,named] Biegelinie.Q -----"; +"----------- me met [diff,integration,named] Biegelinie.Q"; +"----------- me met [diff,integration,named] Biegelinie.Q"; +"----------- me met [diff,integration,named] Biegelinie.Q"; (*exp_CalcInt_No-3.xml*) val fmz = ["functionTerm (- q_0)", "integrateBy x","antiDerivativeName Q"]; @@ -454,9 +466,9 @@ else raise error "integrate.sml: method [diff,integration,named] .Q"; -"----------- interSteps [diff,integration] -----------------------"; -"----------- interSteps [diff,integration] -----------------------"; -"----------- interSteps [diff,integration] -----------------------"; +"----------- interSteps [diff,integration] --------------"; +"----------- interSteps [diff,integration] --------------"; +"----------- interSteps [diff,integration] --------------"; states:=[]; CalcTree [(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"], @@ -473,11 +485,11 @@ else raise error "integrate.sml: interSteps on Rewrite_Set_Inst 1"; -"----------- method analog to rls 'integration' ------------------"; -"----------- method analog to rls 'integration' ------------------"; -"----------- method analog to rls 'integration' ------------------"; +"----------- method analog to rls 'integration' ---------"; +"----------- method analog to rls 'integration' ---------"; +"----------- method analog to rls 'integration' ---------"; store_met - (prep_met Integrate.thy "met_testint" [] e_metID + (prep_met thy "met_testint" [] e_metID (["diff","integration","test"], [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_"]) @@ -521,9 +533,9 @@ else raise error "integrate.sml: test-script doesnt work"; -"----------- Ambiguous input: Integral ?u + ?v D ?bdv = ..--------"; -"----------- Ambiguous input: Integral ?u + ?v D ?bdv = ..--------"; -"----------- Ambiguous input: Integral ?u + ?v D ?bdv = ..--------"; +"----------- Ambiguous input: Integral ?u + ?v D ?bdv = ."; +"----------- Ambiguous input: Integral ?u + ?v D ?bdv = ."; +"----------- Ambiguous input: Integral ?u + ?v D ?bdv = ."; states:=[]; CalcTree [(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"], @@ -556,9 +568,10 @@ if existpt' ([1,1,5], Res) pt then () else raise error "integrate.sml: interSteps on Rewrite_Set_Inst 2"; -"----------- CAS input -------------------------------------------"; -"----------- CAS input -------------------------------------------"; -"----------- CAS input -------------------------------------------"; + +"----------- CAS input ----------------------------------"; +"----------- CAS input ----------------------------------"; +"----------- CAS input ----------------------------------"; val t = str2term "Integrate (x^^^2 + x + 1, x)"; case t of Const ("Integrate.Integrate", _) $ _ => () | _ => raise error "diff.sml behav.changed for Integrate (..., x)"; diff -r f57ddfd09474 -r e4f42a63d665 test/Tools/isac/Test_Isac.thy --- a/test/Tools/isac/Test_Isac.thy Thu Sep 23 08:54:26 2010 +0200 +++ b/test/Tools/isac/Test_Isac.thy Thu Sep 23 12:56:51 2010 +0200 @@ -77,9 +77,20 @@ use"complex.sml"; use"diff.sml"; use"diffapp.sml"; -(**) -use"Knowledge/integrate.sml"; -(**) +*) +ML {*print_depth 99*} + +ML {* +fun term2str trm = Print_Mode.setmp (Print_Mode.input :: + filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) + (Syntax.string_of_term @{context}) trm; +val trm = str2term "a+b"; term2str trm; +val trm = str2term "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3"; term2str trm; +"========================================================="; +*} + +use "Knowledge/integrate.sml"; +(* use"equation.sml"; (*use"inssort.sml"; problems with recdef in Isabelle2002*) use"logexp.sml"; @@ -104,6 +115,9 @@ use"algein.sml"; cd "../.."; *) +use_thy "../../Pure/Isar/Test_Parse_Term" +use_thy "../../Pure/Isar/Test_Parsers" + ML{* writeln "**** run tests on IsacKnowledge complete ****************" *}; (* val path = "/home/neuper/proto2/testsml2xml/";