# HG changeset patch # User Walther Neuper # Date 1283959203 -7200 # Node ID eb4c556a525b9f832b0bad79db8dd65156328f9e # Parent e4796b1125fb60bff4a0e2ebb0070a6f99ab4994 tuned src/Knowledge + test/Knowledge: find . -type f -exec sed -i s/"f_\""/"f_f\""/g {} \; find . -type f -exec sed -i s/"f_,"/"f_f,"/g {} \; find . -type f -exec sed -i s/"f_:"/"f_f:"/g {} \; find . -type f -exec sed -i s/"f_'_"/"f_f'"/g {} \; find . -type f -exec sed -i s/"eqs_"/"eqs"/g {} \; find . -type f -exec sed -i s/"f'_ "/"f_f' "/g {} \; find . -type f -exec sed -i s/"f'_)"/"f_f')"/g {} \; diff -r e4796b1125fb -r eb4c556a525b src/Tools/isac/Knowledge/DiffApp-oldscr.sml --- a/src/Tools/isac/Knowledge/DiffApp-oldscr.sml Wed Sep 08 17:17:29 2010 +0200 +++ b/src/Tools/isac/Knowledge/DiffApp-oldscr.sml Wed Sep 08 17:20:03 2010 +0200 @@ -64,11 +64,11 @@ ML> val c = (the o (parse thy)) s; val c = "Script make_fun_by_new_variable = - Input [Real f_, Real v_v, BoolList eqs_] + Input [Real f_f, Real v_v, BoolList eqs] Local [Bool h_, BoolList es_, RealList vs_, Real v1_, Real v2_, Bool e1, Bool e2_, BoolList s_1, BoolList s_2] Tacs [SEQU - [let h_ = (hd o filter (Testvar m_)) eqs_; es_ = eqs_ -- [h_]; + [let h_ = (hd o filter (Testvar m_)) eqs; es_ = eqs -- [h_]; vs_ = Var h_ -- [f_]; v1_ = Nth #1 vs_; v2_ = Nth #2 vs_; e1_ = (hd o filter (Testvar v1_)) es_; e2_ = (hd o filter (Testvar v2_)) es_ @@ -84,10 +84,10 @@ ML> val c = (the o (parse thy)) s; val c = "Script make_fun_explicit = - Input [Real f_, Real v_v, BoolList eqs_] + Input [Real f_f, Real v_v, BoolList eqs] Local [Bool h_, Bool eq_, RealList vs_, Real v1_, BoolList ss_] Tacs [SEQU - [let h_ = (hd o filter (Testvar m_)) eqs_; eq_ = hd (eqs_ -- [h_]); + [let h_ = (hd o filter (Testvar m_)) eqs; eq_ = hd (eqs -- [h_]); vs_ = Var h_ -- [f_]; v1_ = hd (vs_ -- [v_]) in Subproblem Spec (R, [univar, equation], no_met) InOut [In eq_, In v1_, Out ss_]], diff -r e4796b1125fb -r eb4c556a525b src/Tools/isac/Knowledge/DiffApp.sml --- a/src/Tools/isac/Knowledge/DiffApp.sml Wed Sep 08 17:17:29 2010 +0200 +++ b/src/Tools/isac/Knowledge/DiffApp.sml Wed Sep 08 17:20:03 2010 +0200 @@ -26,9 +26,9 @@ prep_pbt DiffAppl.thy (["DiffAppl","make","function"]:pblID, - [("#Given" ,"functionOf f_"), + [("#Given" ,"functionOf f_f"), ("#Given" ,"boundVariable v_v"), - ("#Given" ,"equalities eqs_"), + ("#Given" ,"equalities eqs"), ("#Find" ,"functionTerm f_0_") ]), @@ -43,7 +43,7 @@ prep_pbt DiffAppl.thy (["DiffAppl","find_values","tool"]:pblID, [("#Given" ,"maxArgument ma_"), - ("#Given" ,"functionTerm f_"), + ("#Given" ,"functionTerm f_f"), ("#Given" ,"boundVariable v_v"), ("#Find" ,"valuesFor vls_"), ("#Relate","additionalRels rs_") @@ -68,9 +68,9 @@ (("DiffAppl","make_fun_by_new_variable"):metID, {ppc = prep_met DiffAppl.thy - [("#Given" ,"functionOf f_"), + [("#Given" ,"functionOf f_f"), ("#Given" ,"boundVariable v_v"), - ("#Given" ,"equalities eqs_"), + ("#Given" ,"equalities eqs"), ("#Find" ,"functionTerm f_0_") ], rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], @@ -78,9 +78,9 @@ (("DiffAppl","make_fun_by_explicit"):metID, {ppc = prep_met DiffAppl.thy - [("#Given" ,"functionOf f_"), + [("#Given" ,"functionOf f_f"), ("#Given" ,"boundVariable v_v"), - ("#Given" ,"equalities eqs_"), + ("#Given" ,"equalities eqs"), ("#Find" ,"functionTerm f_0_") ], rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], diff -r e4796b1125fb -r eb4c556a525b src/Tools/isac/Knowledge/DiffApp.thy --- a/src/Tools/isac/Knowledge/DiffApp.thy Wed Sep 08 17:17:29 2010 +0200 +++ b/src/Tools/isac/Knowledge/DiffApp.thy Wed Sep 08 17:20:03 2010 +0200 @@ -96,21 +96,21 @@ store_pbt (prep_pbt thy "pbl_fun_make" [] e_pblID (["make","function"]:pblID, - [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]), + [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), ("#Find" ,["functionEq f_1_"]) ], e_rls, NONE, [])); store_pbt (prep_pbt thy "pbl_fun_max_expl" [] e_pblID (["by_explicit","make","function"]:pblID, - [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]), + [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), ("#Find" ,["functionEq f_1_"]) ], e_rls, NONE, [["DiffApp","make_fun_by_explicit"]])); store_pbt (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID (["by_new_variable","make","function"]:pblID, - [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]), + [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), (*WN.12.5.03: precond for distinction still missing*) ("#Find" ,["functionEq f_1_"]) ], @@ -134,7 +134,7 @@ store_pbt (prep_pbt thy "pbl_tool_findvals" [] e_pblID (["find_values","tool"]:pblID, - [("#Given" ,["maxArgument ma_","functionEq f_","boundVariable v_v"]), + [("#Given" ,["maxArgument ma_","functionEq f_f","boundVariable v_v"]), ("#Find" ,["valuesFor vls_"]), ("#Relate",["additionalRels rs_"]) ], @@ -179,15 +179,15 @@ store_met (prep_met thy "met_diffapp_funnew" [] e_metID (["DiffApp","make_fun_by_new_variable"]:metID, - [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]), + [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), ("#Find" ,["functionEq f_1_"]) ], {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls, calc=[], crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)}, - "Script Make_fun_by_new_variable (f_::real) (v_v::real) " ^ - " (eqs_::bool list) = " ^ - "(let h_ = (hd o (filterVar f_)) eqs_; " ^ - " es_ = dropWhile (ident h_) eqs_; " ^ + "Script Make_fun_by_new_variable (f_f::real) (v_v::real) " ^ + " (eqs::bool list) = " ^ + "(let h_ = (hd o (filterVar f_)) eqs; " ^ + " es_ = dropWhile (ident h_) eqs; " ^ " vs_ = dropWhile (ident f_) (Vars h_); " ^ " v_1 = nth_ 1 vs_; " ^ " v_2 = nth_ 2 vs_; " ^ @@ -204,16 +204,16 @@ store_met (prep_met thy "met_diffapp_funexp" [] e_metID (["DiffApp","make_fun_by_explicit"]:metID, - [("#Given" ,["functionOf f_","boundVariable v_v","equalities eqs_"]), + [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), ("#Find" ,["functionEq f_1_"]) ], {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls, crls = eval_rls, nrls=norm_Rational (*, asm_rls=[],asm_thm=[]*)}, - "Script Make_fun_by_explicit (f_::real) (v_v::real) " ^ - " (eqs_::bool list) = " ^ - " (let h_ = (hd o (filterVar f_)) eqs_; " ^ - " e_1 = hd (dropWhile (ident h_) eqs_); " ^ + "Script Make_fun_by_explicit (f_f::real) (v_v::real) " ^ + " (eqs::bool list) = " ^ + " (let h_ = (hd o (filterVar f_)) eqs; " ^ + " e_1 = hd (dropWhile (ident h_) eqs); " ^ " vs_ = dropWhile (ident f_) (Vars h_); " ^ " v_1 = hd (dropWhile (ident v_v) vs_); " ^ " (s_1::bool list)= " ^ diff -r e4796b1125fb -r eb4c556a525b src/Tools/isac/Knowledge/Integrate.thy --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Sep 08 17:17:29 2010 +0200 +++ b/src/Tools/isac/Knowledge/Integrate.thy Wed Sep 08 17:20:03 2010 +0200 @@ -337,22 +337,22 @@ store_pbt (prep_pbt thy "pbl_fun_integ" [] e_pblID (["integrate","function"], - [("#Given" ,["functionTerm f_", "integrateBy v_v"]), + [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_"]) ], append_rls "e_rls" e_rls [(*for preds in where_*)], - SOME "Integrate (f_, v_v)", + SOME "Integrate (f_f, v_v)", [["diff","integration"]])); (*here "named" is used differently from Differentiation"*) store_pbt (prep_pbt thy "pbl_fun_integ_nam" [] e_pblID (["named","integrate","function"], - [("#Given" ,["functionTerm f_", "integrateBy v_v"]), + [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivativeName F_"]) ], append_rls "e_rls" e_rls [(*for preds in where_*)], - SOME "Integrate (f_, v_v)", + SOME "Integrate (f_f, v_v)", [["diff","integration","named"]])); (** methods **) @@ -360,14 +360,14 @@ store_met (prep_met thy "met_diffint" [] e_metID (["diff","integration"], - [("#Given" ,["functionTerm f_", "integrateBy v_v"]), + [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_"]) ], {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls, nrls = e_rls}, -"Script IntegrationScript (f_::real) (v_v::real) = " ^ +"Script IntegrationScript (f_f::real) (v_v::real) = " ^ " (let t_ = Take (Integral f_ D v_v) " ^ " in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))" )); @@ -375,14 +375,14 @@ store_met (prep_met thy "met_diffint_named" [] e_metID (["diff","integration","named"], - [("#Given" ,["functionTerm f_", "integrateBy v_v"]), + [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivativeName F_"]) ], {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls, nrls = e_rls}, -"Script NamedIntegrationScript (f_::real) (v_v::real) (F_::real=>real) = " ^ +"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_::real=>real) = " ^ " (let t_ = Take (F_ v_v = Integral f_ D v_v) " ^ " in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@ " ^ " (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_) " diff -r e4796b1125fb -r eb4c556a525b src/Tools/isac/Knowledge/Test.thy --- a/src/Tools/isac/Knowledge/Test.thy Wed Sep 08 17:17:29 2010 +0200 +++ b/src/Tools/isac/Knowledge/Test.thy Wed Sep 08 17:20:03 2010 +0200 @@ -549,7 +549,7 @@ (prep_pbt thy (["thy"], [("#Given" ,"boolTestGiven g_"), - ("#Find" ,"boolTestFind f_") + ("#Find" ,"boolTestFind f_f") ], [])); @@ -557,7 +557,7 @@ (prep_pbt thy (["testeq","thy"], [("#Given" ,"boolTestGiven g_"), - ("#Find" ,"boolTestFind f_") + ("#Find" ,"boolTestFind f_f") ], [])); @@ -604,7 +604,7 @@ (*, prep_met thy (*test for equations*) (["Test","testeq"]:metID, [("#Given" ,["boolTestGiven g_"]), - ("#Find" ,["boolTestFind f_"]) + ("#Find" ,["boolTestFind f_f"]) ], {rew_ord'="e_rew_ord",rls'="tval_rls",asm_rls=[], asm_thm=[("square_equation_left","")]}, diff -r e4796b1125fb -r eb4c556a525b test/Tools/isac/Knowledge/diff.sml --- a/test/Tools/isac/Knowledge/diff.sml Wed Sep 08 17:17:29 2010 +0200 +++ b/test/Tools/isac/Knowledge/diff.sml Wed Sep 08 17:20:03 2010 +0200 @@ -32,15 +32,15 @@ " _________________ problemtype _________________ "; " _________________ problemtype _________________ "; " _________________ problemtype _________________ "; -val pbt = {Given =["functionTerm f_", "differentiateFor v_v"], +val pbt = {Given =["functionTerm f_f", "differentiateFor v_v"], Where =[], - Find =["derivative f_'_"], + Find =["derivative f_f'"], With =[], Relate=[]}:string ppc; val chkpbt = ((map (the o (parse Diff.thy))) o ppc2list) pbt; val org = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))", - "differentiateFor x","derivative f_'_"]; + "differentiateFor x","derivative f_f'"]; val chkorg = map (the o (parse Diff.thy)) org; get_pbt ["derivative_of","function"]; @@ -195,7 +195,7 @@ " ______________ differentiate: me (*+ tacs input*) ______________ "; " ______________ differentiate: me (*+ tacs input*) ______________ "; val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)", - "differentiateFor x","derivative f_'_"]; + "differentiateFor x","derivative f_f'"]; val (dI',pI',mI') = ("Diff",["derivative_of","function"], ["diff","diff_simpl"]); @@ -211,7 +211,7 @@ (*val nxt = ("Add_Given",Add_Given "differentiateFor x");*) val (p,_,f,nxt,_,pt) = me nxt p c pt; "--- s4 ---"; -(*val nxt = ("Add_Find",Add_Find "derivative f_'_");*) +(*val nxt = ("Add_Find",Add_Find "derivative f_f'");*) val (p,_,f,nxt,_,pt) = me nxt p c pt; "--- s5 ---"; (*val nxt = ("Specify_Theory",Specify_Theory dI');*) @@ -305,7 +305,7 @@ " _________________ script-eval corrected _________________ "; val scr = Script (((inst_abs (assoc_thy "Test")) o term_of o the o (parse Diff.thy)) - "Script Differentiate (f_::real) (v_v::real) = \ + "Script Differentiate (f_f::real) (v_v::real) = \ \(let f_ = Try (Repeat (Rewrite frac_conv False f_)); \ \ f_ = Try (Repeat (Rewrite root_conv False f_)); \ \ f_ = Repeat \ @@ -344,7 +344,7 @@ val parseee = (term_of o the o (parse Diff.thy)); val ct = "d_d x (x ^^^ #2 + #3 * x + #4)"; -val envvv = [(parseee"f_",parseee ct),(parseee"v_",parseee"x")]; +val envvv = [(parseee"f_f",parseee ct),(parseee"v_",parseee"x")]; val ets0=[([],(Tac'(Script.thy,"BS","",""),envvv,envvv,empty,empty,Safe)), ([],(User', [], [], empty, empty,Sundef))]:ets; val l0 = []; @@ -410,7 +410,7 @@ set_dstate 1 test_hide 4 1;(*SelRule,St..PutRuleRes,TskipS..*) StdinSML 1 0 0 0 New_Proof; val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))", - "differentiateFor x","derivative f_'_"]; + "differentiateFor x","derivative f_f'"]; val (dI',pI',mI') = ("Diff",["derivative_of","function"], ["diff","differentiate_on_R"]); @@ -425,7 +425,7 @@ set_dstate 1 test_hide 0 2;(*PutRule,TskipS..PutRuleRes,Tt..*) StdinSML 1 0 0 0 New_Proof; val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))", - "differentiateFor x","derivative f_'_"]; + "differentiateFor x","derivative f_f'"]; val (dI',pI',mI') = ("Diff",["derivative_of","function"], ["diff","differentiate_on_R"]); @@ -437,7 +437,7 @@ "---------------------1.5.02 me from script ---------------------"; (*exp_Diff_No-1.xml*) val fmz = ["functionTerm (x ^^^ 2 + 3 * x + 4)", - "differentiateFor x","derivative f_'_"]; + "differentiateFor x","derivative f_f'"]; val (dI',pI',mI') = ("Diff",["derivative_of","function"], ["diff","diff_simpl"]); @@ -470,14 +470,14 @@ "----------- primed id -------------------------------------------"; "----------- primed id -------------------------------------------"; -val f_ = str2term "f_::bool"; +val f_ = str2term "f_f::bool"; val f = str2term "A = s * (a - s)"; val v_v = str2term "v_"; val v = str2term "s"; val screxp0 = str2term "Take ((primed (lhs f_)) = d_d v_v (rhs f_))"; atomty screxp0; -val screxp1 = subst_atomic [(f_, f), (v_, v)] screxp0; +val screxp1 = subst_atomic [(f_f, f), (v_, v)] screxp0; term2str screxp1; atomty screxp1; @@ -486,8 +486,8 @@ else raise error "diff.sml: diff.behav. in 'primed'"; atomty f'_; -val str = "Script DiffEqScr (f_::bool) (v_v::real) = \ -\ (let f'_ = Take ((primed (lhs f_)) = d_d v_v (rhs f_)) \ +val str = "Script DiffEqScr (f_f::bool) (v_v::real) = \ +\ (let f_f' = Take ((primed (lhs f_)) = d_d v_v (rhs f_)) \ \ in (((Try (Repeat (Rewrite frac_conv False))) @@ \ \ (Try (Repeat (Rewrite root_conv False))) @@ \ \ (Try (Repeat (Rewrite realpow_pow False))) @@ \ @@ -512,7 +512,7 @@ \ (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or \ \ (Repeat (Rewrite_Set make_polynomial False)))) @@ \ \ (Try (Repeat (Rewrite sym_frac_conv False))) @@ \ - \ (Try (Repeat (Rewrite sym_root_conv False))))) f'_)" + \ (Try (Repeat (Rewrite sym_root_conv False))))) f_f')" ; val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; @@ -567,7 +567,7 @@ CalcTree [(["functionTerm (x^2 + x+ 1/x + 2/x^2)", (*"functionTerm ((x^3)^5)",*) - "differentiateFor x", "derivative f_'_"], + "differentiateFor x", "derivative f_f'"], ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))]; Iterator 1; @@ -582,7 +582,7 @@ states:=[]; CalcTree [(["functionTerm (x^3 * x^5)", - "differentiateFor x", "derivative f_'_"], + "differentiateFor x", "derivative f_f'"], ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))]; Iterator 1; @@ -607,7 +607,7 @@ states:=[]; CalcTree [(["functionTerm (x^3 * x^5)", - "differentiateFor x", "derivative f_'_"], + "differentiateFor x", "derivative f_f'"], ("Isac", ["derivative_of","function"], ["diff","after_simplification"]))]; Iterator 1; @@ -627,7 +627,7 @@ states:=[]; CalcTree [(["functionTerm ((x^3)^5)", - "differentiateFor x", "derivative f_'_"], + "differentiateFor x", "derivative f_f'"], ("Isac", ["derivative_of","function"], ["diff","after_simplification"]))]; Iterator 1; @@ -644,7 +644,7 @@ "----------- autoCalculate differentiate_equality ----------------"; states:=[]; CalcTree -[(["functionEq (A = s * (a - s))", "differentiateFor s", "derivativeEq f_'_"], +[(["functionEq (A = s * (a - s))", "differentiateFor s", "derivativeEq f_f'"], ("Isac", ["named","derivative_of","function"], ["diff","differentiate_equality"]))]; Iterator 1; @@ -676,7 +676,7 @@ states:=[]; CalcTree [(["functionTerm (x^2 + x + 1)", - "differentiateFor x", "derivative f_'_"], + "differentiateFor x", "derivative f_f'"], ("Isac", ["derivative_of","function"], ["diff","differentiate_on_R"]))]; Iterator 1; diff -r e4796b1125fb -r eb4c556a525b test/Tools/isac/Knowledge/diffapp.sml --- a/test/Tools/isac/Knowledge/diffapp.sml Wed Sep 08 17:17:29 2010 +0200 +++ b/test/Tools/isac/Knowledge/diffapp.sml Wed Sep 08 17:20:03 2010 +0200 @@ -45,7 +45,7 @@ map (the o (parseold thy)) fmz; " -------------- [make,function] -------------- "; val pbt = - ["functionOf f_","boundVariable v_v","equalities eqs_", + ["functionOf f_f","boundVariable v_v","equalities eqs", "functionTerm f_0_"]; map (the o (parseold thy)) pbt; val fmz12 = @@ -89,7 +89,7 @@ map (the o (parseold thy)) fmz3; " --------- [derivative_of,function] --------- "; val pbt = - ["functionTerm f_","boundVariable v_v","derivative f_'_"]; + ["functionTerm f_f","boundVariable v_v","derivative f_f'"]; map (the o (parseold thy)) pbt; val fmz = [(*28.11.00: "functionTerm (A_0=a*#2*sqrt r^^^#2 - (a//#2)^^^#2)",*) @@ -99,7 +99,7 @@ map (the o (parseold thy)) fmz; " --------- [find_values,tool] --------- "; val pbt = - ["maxArgument ma_","functionTerm f_","boundVariable v_v", + ["maxArgument ma_","functionTerm f_f","boundVariable v_v", "valuesFor vls_","additionalRels rs_"]; map (the o (parseold thy)) pbt; val fmz1 = @@ -519,25 +519,25 @@ "---------------------- 1.5.03: Make_fun_by_explicit ---------------------"; "---------------------- 1.5.03: Make_fun_by_explicit ---------------------"; str2term - "Script Make_fun_by_explicit (f_::real) (v_v::real) \ - \ (eqs_::bool list) = \ - \ (let h_ = (hd o (filterVar f_)) eqs_; \ - \ e_1 = hd (dropWhile (ident h_) eqs_); \ + "Script Make_fun_by_explicit (f_f::real) (v_v::real) \ + \ (eqs::bool list) = \ + \ (let h_ = (hd o (filterVar f_)) eqs; \ + \ e_1 = hd (dropWhile (ident h_) eqs); \ \ vs_ = dropWhile (ident f_) (Vars h_); \ \ v_1 = hd (dropWhile (ident v_v) vs_); \ \ (s_1::bool list)=(SubProblem(Reals_,[univar,equation],[no_met])\ \ [BOOL e_1, REAL v_1])\ \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)"; -val f_ = (str2term "f_::real", +val f_ = (str2term "f_f::real", str2term "A"); val v_v = (str2term "v_v::real", str2term "b"); -val eqs_=(str2term "eqs_::bool list", +val eqs=(str2term "eqs::bool list", str2term "[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"); -val env = [f_, v_v, eqs_]; +val env = [f_f, v_v, eqs]; (*--- 1.line in script ---*) -val t = str2term "(hd o (filterVar v_v)) (eqs_::bool list)"; +val t = str2term "(hd o (filterVar v_v)) (eqs::bool list)"; val s = subst_atomic env t; term2str s; val t = str2term @@ -548,7 +548,7 @@ val env = env @ [(str2term "h_::bool", str2term s')]; (*--- 2.line in script ---*) -val t = str2term "hd (dropWhile (ident h_) (eqs_::bool list))"; +val t = str2term "hd (dropWhile (ident h_) (eqs::bool list))"; val s = subst_atomic env t; term2str s; val t = str2term @@ -610,10 +610,10 @@ "---------------------- 2.5.03: Make_fun_by_new_variable -----------------"; "---------------------- 2.5.03: Make_fun_by_new_variable -----------------"; str2term - "Script Make_fun_by_new_variable (f_::real) (v_v::real) \ - \ (eqs_::bool list) = \ - \(let h_ = (hd o (filterVar f_)) eqs_; \ - \ es_ = dropWhile (ident h_) eqs_; \ + "Script Make_fun_by_new_variable (f_f::real) (v_v::real) \ + \ (eqs::bool list) = \ + \(let h_ = (hd o (filterVar f_)) eqs; \ + \ es_ = dropWhile (ident h_) eqs; \ \ vs_ = dropWhile (ident f_) (Vars h_); \ \ v_1 = nth_ 1 vs_; \ \ v_2 = nth_ 2 vs_; \ @@ -624,16 +624,16 @@ \ (s_2::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\ \ [BOOL e_2, REAL v_2])\ \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)"; -val f_ = (str2term "f_::real", +val f_ = (str2term "f_f::real", str2term "A"); val v_v = (str2term "v_v::real", str2term "alpha"); -val eqs_=(str2term "eqs_::bool list", +val eqs=(str2term "eqs::bool list", str2term "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]"); -val env = [f_, v_v, eqs_]; +val env = [f_f, v_v, eqs]; (*--- 1.line in script ---*) -val t = str2term "(hd o (filterVar (f_::real))) (eqs_::bool list)"; +val t = str2term "(hd o (filterVar (f_f::real))) (eqs::bool list)"; val s = subst_atomic env t; term2str s; val t = str2term @@ -646,7 +646,7 @@ val env = env @ [(str2term "h_::bool", str2term s')]; (*--- 2.line in script ---*) -val t = str2term "dropWhile (ident (h_::bool)) (eqs_::bool list)"; +val t = str2term "dropWhile (ident (h_::bool)) (eqs::bool list)"; val s = subst_atomic env t; term2str s; val t = str2term @@ -659,7 +659,7 @@ val env = env @ [(str2term "es_::bool list", str2term s')]; (*--- 3.line in script ---*) -val t = str2term "dropWhile (ident (f_::real)) (Vars (h_::bool))"; +val t = str2term "dropWhile (ident (f_f::real)) (Vars (h_::bool))"; val s = subst_atomic env t; term2str s; val t = str2term "dropWhile (ident A) (Vars (A = a * b))"; diff -r e4796b1125fb -r eb4c556a525b test/Tools/isac/Knowledge/integrate.sml --- a/test/Tools/isac/Knowledge/integrate.sml Wed Sep 08 17:17:29 2010 +0200 +++ b/test/Tools/isac/Knowledge/integrate.sml Wed Sep 08 17:20:03 2010 +0200 @@ -314,7 +314,7 @@ "----------- check probem type -----------------------------------"; "----------- check probem type -----------------------------------"; "----------- check probem type -----------------------------------"; -val model = {Given =["functionTerm f_", "integrateBy v_v"], +val model = {Given =["functionTerm f_f", "integrateBy v_v"], Where =[], Find =["antiDerivative F_"], With =[], @@ -326,7 +326,7 @@ case t3 of Const ("Integrate.antiDerivative", _) $ _ => () | _ => raise error "integrate.sml: Integrate.antiDerivative ???"; -val model = {Given =["functionTerm f_", "integrateBy v_v"], +val model = {Given =["functionTerm f_f", "integrateBy v_v"], Where =[], Find =["antiDerivativeName F_"], With =[], @@ -362,14 +362,14 @@ "----------- check Scripts ---------------------------------------"; "----------- check Scripts ---------------------------------------"; val str = -"Script IntegrationScript (f_::real) (v_v::real) = \ +"Script IntegrationScript (f_f::real) (v_v::real) = \ \ (let t_ = Take (Integral f_ D v_v) \ \ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))"; val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; atomty sc; val str = -"Script NamedIntegrationScript (f_::real) (v_v::real) (F_::real=>real) = \ +"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_::real=>real) = \ \ (let t_ = Take (F_ v_v = Integral f_ D v_v) \ \ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_)"; val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; @@ -479,17 +479,17 @@ store_met (prep_met Integrate.thy "met_testint" [] e_metID (["diff","integration","test"], - [("#Given" ,["functionTerm f_", "integrateBy v_v"]), + [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_"]) ], {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = e_rls, prls=e_rls, crls = Atools_erls, nrls = e_rls}, -"Script IntegrationScript (f_::real) (v_v::real) = \ +"Script IntegrationScript (f_f::real) (v_v::real) = \ \ (((Rewrite_Set_Inst [(bdv,v_v)] integration_rules False) @@ \ \ (Rewrite_Set_Inst [(bdv,v_v)] add_new_c False) @@ \ -\ (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) (f_::real))" +\ (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) (f_f::real))" )); states:=[];