src/Tools/isac/Knowledge/DiffApp-oldscr.sml
branchisac-update-Isa09-2
changeset 37995 fac82f29f143
parent 37994 eb4c556a525b
child 59585 0bb418c3855a
     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_)]]