1.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Mon Sep 06 14:48:38 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Mon Sep 06 15:09:37 2010 +0200
1.3 @@ -45,7 +45,7 @@
1.4 map (the o (parseold thy)) fmz;
1.5 " -------------- [make,function] -------------- ";
1.6 val pbt =
1.7 - ["functionOf f_","boundVariable v_","equalities eqs_",
1.8 + ["functionOf f_","boundVariable v_v","equalities eqs_",
1.9 "functionTerm f_0_"];
1.10 map (the o (parseold thy)) pbt;
1.11 val fmz12 =
1.12 @@ -60,7 +60,7 @@
1.13 map (the o (parseold thy)) fmz3;
1.14 " --------- [univar,equation] --------- ";
1.15 val pbt =
1.16 - ["equality e_","solveFor v_","solutions v_i_"];
1.17 + ["equality e_e","solveFor v_v","solutions v_i_"];
1.18 map (the o (parseold thy)) pbt;
1.19 val fmz =
1.20 ["equality ((a/2)^^^2 + (b/2)^^^2 = r^^^2)",
1.21 @@ -68,7 +68,7 @@
1.22 map (the o (parseold thy)) fmz;
1.23 " ---- [on_interval,maximum_of,function] ---- ";
1.24 val pbt =
1.25 - ["functionTerm t_","boundVariable v_","interval itv_",
1.26 + ["functionTerm t_","boundVariable v_v","interval itv_",
1.27 "errorBound err_","maxArgument v_0_"];
1.28 map (the o (parseold thy)) pbt;
1.29 val fmz12 =
1.30 @@ -89,7 +89,7 @@
1.31 map (the o (parseold thy)) fmz3;
1.32 " --------- [derivative_of,function] --------- ";
1.33 val pbt =
1.34 - ["functionTerm f_","boundVariable v_","derivative f_'_"];
1.35 + ["functionTerm f_","boundVariable v_v","derivative f_'_"];
1.36 map (the o (parseold thy)) pbt;
1.37 val fmz =
1.38 [(*28.11.00: "functionTerm (A_0=a*#2*sqrt r^^^#2 - (a//#2)^^^#2)",*)
1.39 @@ -99,7 +99,7 @@
1.40 map (the o (parseold thy)) fmz;
1.41 " --------- [find_values,tool] --------- ";
1.42 val pbt =
1.43 - ["maxArgument ma_","functionTerm f_","boundVariable v_",
1.44 + ["maxArgument ma_","functionTerm f_","boundVariable v_v",
1.45 "valuesFor vls_","additionalRels rs_"];
1.46 map (the o (parseold thy)) pbt;
1.47 val fmz1 =
1.48 @@ -428,7 +428,7 @@
1.49 val mits = get_obj g_met pt (fst p);
1.50 writeln (itms2str_ ctxt mits);
1.51 (*
1.52 - if itms2str_ ctxt mits = "[\n(1 ,[1] ,true ,#Given ,Cor functionEq (hd rs_) ,(t_, [hd rs_])),\n(2 ,[1] ,true ,#Given ,Cor boundVariable v_ ,(v_, [v_])),\n(3 ,[1] ,true ,#Given ,Cor interval itv_ ,(itv_, [itv_])),\n(4 ,[1] ,true ,#Find ,Cor maxArgument v__0 ,(v_0_, [v__0]))]" then ()
1.53 + if itms2str_ ctxt mits = "[\n(1 ,[1] ,true ,#Given ,Cor functionEq (hd rs_) ,(t_, [hd rs_])),\n(2 ,[1] ,true ,#Given ,Cor boundVariable v_v ,(v_, [v_])),\n(3 ,[1] ,true ,#Given ,Cor interval itv_ ,(itv_, [itv_])),\n(4 ,[1] ,true ,#Find ,Cor maxArgument v__0 ,(v_0_, [v__0]))]" then ()
1.54 else raise error "diffapp.sml: diff.behav. in autoCalc .. scripts for max 1";
1.55 *)
1.56 (*FIXME: the environments contain identifers, and NOT values ?!?!?*)
1.57 @@ -445,17 +445,17 @@
1.58 str2term
1.59 "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\
1.60 \ (v_::real) (itv_::real set) (err_::bool) = \
1.61 - \ (let e_ = (hd o (filterVar m_)) rs_; \
1.62 + \ (let e_e = (hd o (filterVar m_)) rs_; \
1.63 \ t_ = (if 1 < length_ rs_ \
1.64 \ then (SubProblem (Reals_,[make,function],[no_met])\
1.65 - \ [real_ m_, real_ v_, bool_list_ rs_])\
1.66 + \ [real_ m_, real_ v_v, bool_list_ rs_])\
1.67 \ else (hd rs_)); \
1.68 \ (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \
1.69 \ [Isac,maximum_on_interval])\
1.70 - \ [bool_ t_, real_ v_, real_set_ itv_]\
1.71 + \ [bool_ t_, real_ v_v, real_set_ itv_]\
1.72 \ in ((SubProblem (Reals_,[find_values,tool],[Isac,find_values]) \
1.73 - \ [real_ mx_, real_ (Rhs t_), real_ v_, real_ m_, \
1.74 - \ bool_list_ (dropWhile (ident e_) rs_)])::bool list))";
1.75 + \ [real_ mx_, real_ (Rhs t_), real_ v_v, real_ m_, \
1.76 + \ bool_list_ (dropWhile (ident e_e) rs_)])::bool list))";
1.77
1.78 val fix_ = (str2term "fix_::bool list",
1.79 str2term "[r=Arbfix]");
1.80 @@ -463,7 +463,7 @@
1.81 str2term "A");
1.82 val rs_ = (str2term "rs_::bool list",
1.83 str2term "[A = a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]");
1.84 -val v_ = (str2term "v_::real",
1.85 +val v_v = (str2term "v_::real",
1.86 str2term "b");
1.87 val itv_ = (str2term "itv_::real set",
1.88 str2term "{x::real. 0 <= x & x <= 2*r}");
1.89 @@ -494,7 +494,7 @@
1.90 val t = str2term
1.91 "(if 1 < length_ rs_ \
1.92 \ then (SubProblem (Reals_,[make,function],[no_met])\
1.93 - \ [real_ m_, real_ v_, bool_list_ rs_])\
1.94 + \ [real_ m_, real_ v_v, bool_list_ rs_])\
1.95 \ else (hd rs_))";
1.96 val s = subst_atomic env t;
1.97 term2str s;
1.98 @@ -524,20 +524,20 @@
1.99 \ (let h_ = (hd o (filterVar f_)) eqs_; \
1.100 \ e_1 = hd (dropWhile (ident h_) eqs_); \
1.101 \ vs_ = dropWhile (ident f_) (Vars h_); \
1.102 - \ v_1 = hd (dropWhile (ident v_) vs_); \
1.103 + \ v_1 = hd (dropWhile (ident v_v) vs_); \
1.104 \ (s_1::bool list)=(SubProblem(Reals_,[univar,equation],[no_met])\
1.105 \ [bool_ e_1, real_ v_1])\
1.106 \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
1.107 val f_ = (str2term "f_::real",
1.108 str2term "A");
1.109 -val v_ = (str2term "v_::real",
1.110 +val v_v = (str2term "v_::real",
1.111 str2term "b");
1.112 val eqs_=(str2term "eqs_::bool list",
1.113 str2term "[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]");
1.114 -val env = [f_, v_, eqs_];
1.115 +val env = [f_, v_v, eqs_];
1.116
1.117 (*--- 1.line in script ---*)
1.118 -val t = str2term "(hd o (filterVar v_)) (eqs_::bool list)";
1.119 +val t = str2term "(hd o (filterVar v_v)) (eqs_::bool list)";
1.120 val s = subst_atomic env t;
1.121 term2str s;
1.122 val t = str2term
1.123 @@ -573,7 +573,7 @@
1.124 val env = env @ [(str2term "vs_::real list", str2term s')];
1.125
1.126 (*--- 4.line in script ---*)
1.127 -val t = str2term "hd (dropWhile (ident v_) vs_)";
1.128 +val t = str2term "hd (dropWhile (ident v_v) vs_)";
1.129 val s = subst_atomic env t;
1.130 term2str s;
1.131 val t = str2term "hd (dropWhile (ident b) [a, b])";
1.132 @@ -626,11 +626,11 @@
1.133 \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)";
1.134 val f_ = (str2term "f_::real",
1.135 str2term "A");
1.136 -val v_ = (str2term "v_::real",
1.137 +val v_v = (str2term "v_::real",
1.138 str2term "alpha");
1.139 val eqs_=(str2term "eqs_::bool list",
1.140 str2term "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]");
1.141 -val env = [f_, v_, eqs_];
1.142 +val env = [f_, v_v, eqs_];
1.143
1.144 (*--- 1.line in script ---*)
1.145 val t = str2term "(hd o (filterVar (f_::real))) (eqs_::bool list)";