1.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Wed Sep 08 17:17:29 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Wed Sep 08 17:20:03 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_v","equalities eqs_",
1.8 + ["functionOf f_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 @@ -89,7 +89,7 @@
1.13 map (the o (parseold thy)) fmz3;
1.14 " --------- [derivative_of,function] --------- ";
1.15 val pbt =
1.16 - ["functionTerm f_","boundVariable v_v","derivative f_'_"];
1.17 + ["functionTerm f_f","boundVariable v_v","derivative f_f'"];
1.18 map (the o (parseold thy)) pbt;
1.19 val fmz =
1.20 [(*28.11.00: "functionTerm (A_0=a*#2*sqrt r^^^#2 - (a//#2)^^^#2)",*)
1.21 @@ -99,7 +99,7 @@
1.22 map (the o (parseold thy)) fmz;
1.23 " --------- [find_values,tool] --------- ";
1.24 val pbt =
1.25 - ["maxArgument ma_","functionTerm f_","boundVariable v_v",
1.26 + ["maxArgument ma_","functionTerm f_f","boundVariable v_v",
1.27 "valuesFor vls_","additionalRels rs_"];
1.28 map (the o (parseold thy)) pbt;
1.29 val fmz1 =
1.30 @@ -519,25 +519,25 @@
1.31 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
1.32 "---------------------- 1.5.03: Make_fun_by_explicit ---------------------";
1.33 str2term
1.34 - "Script Make_fun_by_explicit (f_::real) (v_v::real) \
1.35 - \ (eqs_::bool list) = \
1.36 - \ (let h_ = (hd o (filterVar f_)) eqs_; \
1.37 - \ e_1 = hd (dropWhile (ident h_) eqs_); \
1.38 + "Script Make_fun_by_explicit (f_f::real) (v_v::real) \
1.39 + \ (eqs::bool list) = \
1.40 + \ (let h_ = (hd o (filterVar f_)) eqs; \
1.41 + \ e_1 = hd (dropWhile (ident h_) eqs); \
1.42 \ vs_ = dropWhile (ident f_) (Vars h_); \
1.43 \ v_1 = hd (dropWhile (ident v_v) vs_); \
1.44 \ (s_1::bool list)=(SubProblem(Reals_,[univar,equation],[no_met])\
1.45 \ [BOOL e_1, REAL v_1])\
1.46 \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
1.47 -val f_ = (str2term "f_::real",
1.48 +val f_ = (str2term "f_f::real",
1.49 str2term "A");
1.50 val v_v = (str2term "v_v::real",
1.51 str2term "b");
1.52 -val eqs_=(str2term "eqs_::bool list",
1.53 +val eqs=(str2term "eqs::bool list",
1.54 str2term "[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]");
1.55 -val env = [f_, v_v, eqs_];
1.56 +val env = [f_f, v_v, eqs];
1.57
1.58 (*--- 1.line in script ---*)
1.59 -val t = str2term "(hd o (filterVar v_v)) (eqs_::bool list)";
1.60 +val t = str2term "(hd o (filterVar v_v)) (eqs::bool list)";
1.61 val s = subst_atomic env t;
1.62 term2str s;
1.63 val t = str2term
1.64 @@ -548,7 +548,7 @@
1.65 val env = env @ [(str2term "h_::bool", str2term s')];
1.66
1.67 (*--- 2.line in script ---*)
1.68 -val t = str2term "hd (dropWhile (ident h_) (eqs_::bool list))";
1.69 +val t = str2term "hd (dropWhile (ident h_) (eqs::bool list))";
1.70 val s = subst_atomic env t;
1.71 term2str s;
1.72 val t = str2term
1.73 @@ -610,10 +610,10 @@
1.74 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
1.75 "---------------------- 2.5.03: Make_fun_by_new_variable -----------------";
1.76 str2term
1.77 - "Script Make_fun_by_new_variable (f_::real) (v_v::real) \
1.78 - \ (eqs_::bool list) = \
1.79 - \(let h_ = (hd o (filterVar f_)) eqs_; \
1.80 - \ es_ = dropWhile (ident h_) eqs_; \
1.81 + "Script Make_fun_by_new_variable (f_f::real) (v_v::real) \
1.82 + \ (eqs::bool list) = \
1.83 + \(let h_ = (hd o (filterVar f_)) eqs; \
1.84 + \ es_ = dropWhile (ident h_) eqs; \
1.85 \ vs_ = dropWhile (ident f_) (Vars h_); \
1.86 \ v_1 = nth_ 1 vs_; \
1.87 \ v_2 = nth_ 2 vs_; \
1.88 @@ -624,16 +624,16 @@
1.89 \ (s_2::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\
1.90 \ [BOOL e_2, REAL v_2])\
1.91 \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)";
1.92 -val f_ = (str2term "f_::real",
1.93 +val f_ = (str2term "f_f::real",
1.94 str2term "A");
1.95 val v_v = (str2term "v_v::real",
1.96 str2term "alpha");
1.97 -val eqs_=(str2term "eqs_::bool list",
1.98 +val eqs=(str2term "eqs::bool list",
1.99 str2term "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]");
1.100 -val env = [f_, v_v, eqs_];
1.101 +val env = [f_f, v_v, eqs];
1.102
1.103 (*--- 1.line in script ---*)
1.104 -val t = str2term "(hd o (filterVar (f_::real))) (eqs_::bool list)";
1.105 +val t = str2term "(hd o (filterVar (f_f::real))) (eqs::bool list)";
1.106 val s = subst_atomic env t;
1.107 term2str s;
1.108 val t = str2term
1.109 @@ -646,7 +646,7 @@
1.110 val env = env @ [(str2term "h_::bool", str2term s')];
1.111
1.112 (*--- 2.line in script ---*)
1.113 -val t = str2term "dropWhile (ident (h_::bool)) (eqs_::bool list)";
1.114 +val t = str2term "dropWhile (ident (h_::bool)) (eqs::bool list)";
1.115 val s = subst_atomic env t;
1.116 term2str s;
1.117 val t = str2term
1.118 @@ -659,7 +659,7 @@
1.119 val env = env @ [(str2term "es_::bool list", str2term s')];
1.120
1.121 (*--- 3.line in script ---*)
1.122 -val t = str2term "dropWhile (ident (f_::real)) (Vars (h_::bool))";
1.123 +val t = str2term "dropWhile (ident (f_f::real)) (Vars (h_::bool))";
1.124 val s = subst_atomic env t;
1.125 term2str s;
1.126 val t = str2term "dropWhile (ident A) (Vars (A = a * b))";