1.1 --- a/src/Tools/isac/Knowledge/DiffApp-oldscr.sml Wed Sep 08 17:20:03 2010 +0200
1.2 +++ b/src/Tools/isac/Knowledge/DiffApp-oldscr.sml Wed Sep 08 17:49:36 2010 +0200
1.3 @@ -7,32 +7,32 @@
1.4 ML> ...
1.5 ML> val c = (the o (parse thy)) s;
1.6 val c =
1.7 - "Script1 Maximum_value fix_ m_ rs_ v_v itv_ err_ =
1.8 - let e_e = (hd o filter (Testvar m_)) rs_;
1.9 + "Script1 Maximum_value f_ix m_ r_s v_v itv_ err_ =
1.10 + let e_e = (hd o filter (Testvar m_)) r_s;
1.11 t_ =
1.12 - if #1 < Length rs_
1.13 - then make_fun (R, [make, function], no_met) m_ v_v rs_
1.14 - else (Lhs o hd) rs_;
1.15 + if #1 < Length r_s
1.16 + then make_fun (R, [make, function], no_met) m_ v_v r_s
1.17 + else (Lhs o hd) r_s;
1.18 mx_ =
1.19 max_on_interval (R, [on_interval, max_of, function],
1.20 maximum_on_interval) t_ v_v itv_
1.21 in find_vals (R, [find_values, tool], find_values)
1.22 - mx_ t_ v_v m_ dropWhile (op = e_e) rs_" : cterm
1.23 + mx_ t_ v_v m_ dropWhile (op = e_e) r_s" : cterm
1.24
1.25 ML> set show_types;
1.26 ML> c;
1.27 val c =
1.28 - "Script1 Maximum_value fix_::bool list m_::real rs_::bool list v_v::real itv_v::real set err_::bool =
1.29 - let e_e::bool = (hd o filter (Testvar m_)) rs_;
1.30 + "Script1 Maximum_value f_ix::bool list m_::real r_s::bool list v_v::real itv_v::real set err_::bool =
1.31 + let e_e::bool = (hd o filter (Testvar m_)) r_s;
1.32 t_::real =
1.33 - if (#1::real) < Length rs_
1.34 - then make_fun (R::ID, [make::ID, function::ID], no_met::ID) m_ v_v rs_
1.35 - else (Lhs o hd) rs_;
1.36 + if (#1::real) < Length r_s
1.37 + then make_fun (R::ID, [make::ID, function::ID], no_met::ID) m_ v_v r_s
1.38 + else (Lhs o hd) r_s;
1.39 mx_::real =
1.40 max_on_interval (R, [on_interval::ID, max_of::ID, function],
1.41 maximum_on_interval::ID) t_ v_v itv_
1.42 in find_vals (R, [find_values::ID, tool::ID], find_values)
1.43 - mx_ t_ v_v m_ dropWhile (op = e_e) rs_" : cterm
1.44 + mx_ t_ v_v m_ dropWhile (op = e_e) r_s" : cterm
1.45
1.46
1.47
1.48 @@ -44,20 +44,20 @@
1.49 ML> val c = (the o (parse thy)) s;
1.50 val c =
1.51 "Script maximum =
1.52 - Input [Bool fix_, Real m_, BoolList rs_, Real v_v, RealSet itv_, Bool err_]
1.53 - Local [Bool e_e, Real t_, Real mx_, RealList vs_]
1.54 + Input [Bool f_ix, Real m_, BoolList r_s, Real v_v, RealSet itv_, Bool err_]
1.55 + Local [Bool e_e, Real t_, Real mx_, RealList v_s]
1.56 Tacs [SEQU
1.57 - [let e_e = (hd o filter (Testvar m_)) rs_
1.58 - in if #1 < Length rs_
1.59 + [let e_e = (hd o filter (Testvar m_)) r_s
1.60 + in if #1 < Length r_s
1.61 then Subproblem Spec (R, [make, function], no_met)
1.62 - InOut [In m_, In v_v, In rs_, Out t_]
1.63 - else t_ := (Lhs o hd) rs_ ;
1.64 + InOut [In m_, In v_v, In r_s, Out t_]
1.65 + else t_ := (Lhs o hd) r_s ;
1.66 Subproblem Spec (R, [on_interval, max_of, function],
1.67 maximum_on_interval)
1.68 InOut [In t_, In v_v, In itv_, In err_, Out mx_] ;
1.69 Subproblem Spec (R, [find_values, tool], find_values)
1.70 - InOut [In mx_, In t_, In v_v, In m_, In (dropWhile (op = e_e) rs_),
1.71 - Out vs_]]]
1.72 + InOut [In mx_, In t_, In v_v, In m_, In (dropWhile (op = e_e) r_s),
1.73 + Out v_s]]]
1.74 Return []" : cterm
1.75
1.76 ML> ...
1.77 @@ -65,11 +65,11 @@
1.78 val c =
1.79 "Script make_fun_by_new_variable =
1.80 Input [Real f_f, Real v_v, BoolList eqs]
1.81 - Local [Bool h_, BoolList es_, RealList vs_, Real v1_, Real v2_, Bool e1,
1.82 + Local [Bool h_, BoolList es_, RealList v_s, Real v1_, Real v2_, Bool e1,
1.83 Bool e2_, BoolList s_1, BoolList s_2]
1.84 Tacs [SEQU
1.85 [let h_ = (hd o filter (Testvar m_)) eqs; es_ = eqs -- [h_];
1.86 - vs_ = Var h_ -- [f_]; v1_ = Nth #1 vs_; v2_ = Nth #2 vs_;
1.87 + v_s = Var h_ -- [f_]; v1_ = Nth #1 v_s; v2_ = Nth #2 v_s;
1.88 e1_ = (hd o filter (Testvar v1_)) es_;
1.89 e2_ = (hd o filter (Testvar v2_)) es_
1.90 in Subproblem Spec (R, [univar, equation], no_met)
1.91 @@ -85,10 +85,10 @@
1.92 val c =
1.93 "Script make_fun_explicit =
1.94 Input [Real f_f, Real v_v, BoolList eqs]
1.95 - Local [Bool h_, Bool eq_, RealList vs_, Real v1_, BoolList ss_]
1.96 + Local [Bool h_, Bool eq_, RealList v_s, Real v1_, BoolList ss_]
1.97 Tacs [SEQU
1.98 [let h_ = (hd o filter (Testvar m_)) eqs; eq_ = hd (eqs -- [h_]);
1.99 - vs_ = Var h_ -- [f_]; v1_ = hd (vs_ -- [v_])
1.100 + v_s = Var h_ -- [f_]; v1_ = hd (v_s -- [v_])
1.101 in Subproblem Spec (R, [univar, equation], no_met)
1.102 InOut [In eq_, In v1_, Out ss_]],
1.103 Take (Bool h_) ; Substitute [(v1_, (Rhs o hd) ss_)]]