(* tests for ME/script.sml

   WN.13.3.00

   WN050908 OLD FILE, MERGE WITH smltest/ME/script.sml

use"systest/script.sml";

use"script.sml";

*)

"         scripts: Variante 'funktional'               ";

"############## Make_fun_by_new_variable ##############";

"############## Make_fun_by_explicit ##############";

"################ Solve_root_equation #################";

"------- Notlocatable: Free_Solve -------";

"  --- test100:  nxt_tac order------------------------------------ ";

"  --- test100:  order 1 3 1 2 ----------------------------------- ";

" --- test200: nxt_tac order ------------------------------------- ";

" --- test200: order 3 1 1 2 --------------------------------- ";

"  --- root-equation:  nxt_tac order------------------------------ ";

"  --- root-equation:  1.norm_equation ------------------------------ ";

(* --- test200: calculate -----------------------------------------*)

"  --- check_elementwise ------------------------------ ";

"  --- test 30.4.02 Testterm:  Repeat Repeat Or ------------------ ";

"  --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";

"--------- sel_rules ---------------------------------------------";

"-----------------------------------------------------------------";

" ################################################# 6.5.03";

"         scripts: Variante 'funktional'            6.5.03";

" ################################################# 6.5.03 ";

val c = (the o (parse DiffApp.thy)) 

  "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\

   \      (v_::real) (itv_::real set) (err_::bool) =          \ 

   \ (let e_ = (hd o (filterVar m_)) rs_;              \

   \      t_ = (if 1 < length_ rs_                            \

   \           then (SubProblem (Reals_,[make,function],[no_met])\

   \                     [real_ m_, real_ v_, bool_list_ rs_])\

   \           else (hd rs_));                                \

   \      (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \

   \                                [Isac,maximum_on_interval])\

   \                               [bool_ t_, real_ v_, real_set_ itv_]\

   \ in ((SubProblem (Reals_,[find_values,tool],[Isac,find_values])   \

   \      [real_ mx_, real_ (Rhs t_), real_ v_, real_ m_,     \

   \       bool_list_ (dropWhile (ident e_) rs_)])::bool list))";

"################################################### 6.5.03";

"############## Make_fun_by_new_variable ########### 6.5.03";

"################################################### 6.5.03";

val sc = (the o (parse DiffApp.thy)) (*start interpretieren*)

  "Script Make_fun_by_new_variable (f_::real) (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_;                                   \

   \     e_1 = (hd o (filterVar v_1)) es_;            \

   \     e_2 = (hd o (filterVar v_2)) es_;            \

   \  (s_1::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\

   \                    [bool_ e_1, real_ v_1]);\

   \  (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 ags = map (term_of o the o (parse DiffApp.thy)) 

  ["A::real", "alpha::real", 

   "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]"];

val ll = [](*:loc_*);

(* problem with exn PTREE + eval_to -------------------------

"-------------- subproblem with empty formalizaton -------";

val (mI1,m1) = 

  ("Subproblem", tac2tac_ pt p

   (Subproblem (("Reals",["univar","equation","test"],

		(""(*"ANDERN !!!!!!!*),"no_met")),[])));

val (mI2,m2) = (mI1,m1);

val (mI3,m3) = 

  ("Substitute", tac2tac_ pt p

   (Substitute [("a","#2*r*sin alpha"),("b","#2*r*cos alpha")]));

"------- same_tacpbl + eval_to -------";

val SOME(l1,t1) = same_tacpbl sc ll (mI1,m1);

loc_2str l1;

(*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)

Syntax.string_of_term (thy2ctxt' "DiffApp") t1;

(*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *)

val SOME(l2,t2) = same_tacpbl sc l1 (mI2,m2);

loc_2str l2;

(*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)

Syntax.string_of_term (thy2ctxt' "DiffApp") t2;

(*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *)

val SOME(l3,t3) = same_tacpbl sc l2 (mI3,m3);

loc_2str l3;

(*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*)

Syntax.string_of_term (thy2ctxt' "DiffApp") t3;

(*"Substitute [(v_1, (Rhs o hd) B.1), (v_2, (Rhs o hd) B.0)] B.8"*)

"------- eq_tacIDs + eq_consts + eval_args -------";

val eq_ids = eq_tacIDs (*start-loc_*)[] sc (mI,m) [];

val eq_cons = filter (eq_consts m) eq_ids;

val Ready (l,(_,m)::_,_) = eval_args sc (mI,m) [(1,ags)] eq_cons;

"------- locate -------";

"-------------- subproblem with formalizaton -------";

val (mI,m) = 

  ("Subproblem", tac2tac_ pt []

   (Subproblem (("Reals",["univar","equation","test"],

		(""(*"ANDERN !!!!!!!*),"no_met")),

	       ["a//#2=r*sin alpha","a"])));

"------- same_tacpbl + eval_to -------";

"------- eq_tacIDs + eq_consts + eval_args -------";

val eq_ids = eq_tacIDs [] sc (mI,m) [];

val eq_cons = filter (eq_consts m) eq_ids;

val Ready (l,(_,m)::_,_) = eval_args sc (mI,m) [(1,ags)] eq_cons;

"------- locate -------";

-------------------------------------------------------*)

(* use"ME/script.sml";

   use"test-script.sml";

   *)

"############## Make_fun_by_explicit ############## 6.5.03";

"############## Make_fun_by_explicit ############## 6.5.03";

"############## Make_fun_by_explicit ############## 6.5.03";

val c = (the o (parse DiffApp.thy)) 

   "Script Make_fun_by_explicit (f_::real) (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_) 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_)";

(*#####################################################--------11.5.02

"################ Solve_root_equation #################";

(*#####################################################*)

val sc = (term_of o the o (parse Test.thy))

  "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\

   \ (let e_ = Rewrite square_equation_left True eq_;     \

   \      e_ = Rewrite_Set Test_simplify False e_;          \

   \      e_ = Rewrite_Set rearrange_assoc False e_;          \

   \      e_ = Rewrite_Set isolate_root False e_;             \

   \      e_ = Rewrite_Set Test_simplify False e_;          \

   \      e_ = Rewrite square_equation_left True e_;        \

   \      e_ = Rewrite_Set Test_simplify False e_;          \

   \      e_ = Rewrite_Set norm_equation False e_;        \

   \      e_ = Rewrite_Set Test_simplify False e_;      \

   \      e_ = Rewrite_Set_Inst [(bdv,v_)] isolate_bdv False e_;\

   \      e_ = Rewrite_Set Test_simplify False e_       \

   \ in [e_::bool])";

val ags = map (term_of o the o (parse Test.thy)) 

  ["sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)", "x::real","#0"];

val fmz = 

  ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",

   "solveFor x","errorBound (eps = #0)","solutions v_i_"];

----------------------------------------------------------------11.5.02...*)

(*################################# meNEW raises exception with not-locatable

"--------------------- Notlocatable: Free_Solve ---------------------";

"--------------------- Notlocatable: Free_Solve ---------------------";

"--------------------- Notlocatable: Free_Solve ---------------------";

val fmz = []; 

val (dI',pI',mI') =

  ("Test.thy",["sqroot-test","univariate","equation","test"],

   ["Test","sqrt-equ-test"]);

(*val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

val (p,_,f,nxt,_,pt) = me (mI,m) e_pos'[1] EmptyPtree;*)

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

val nxt = ("Model_Problem",

	   Model_Problem ["sqroot-test","univariate","equation","test"]);

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val nxt =

  ("Add_Given",

   Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))");

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val nxt = ("Add_Given",Add_Given "solveFor x");

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)");

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val nxt = ("Add_Find",Add_Find "solutions v_i_");

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val nxt = ("Specify_Theory",Specify_Theory "Test.thy");

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val nxt =

  ("Specify_Problem",Specify_Problem ["sqroot-test","univariate","equation","test"]);

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]);

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

"--- -1 ---";

val nxt = ("Free_Solve",Free_Solve);  

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

"--- 0 ---";

val nxt = ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)");

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

(*me ("Begin_Trans" ////*)

"--- 1 ---";

val nxt = ("Rewrite_Asm",Rewrite_Asm ("square_equation_left",""));

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

"--- 2 ---";

val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

"--- 3 ---";

val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

if f = Form'

    (FormKF

       (~1,EdUndef,1,Nundef,

        "9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)"))

then () else raise error "behaviour in root-expl. Free_Solve changed";

writeln (pr_ptree pr_short pt);

---------------------------------meNEW raises exception with not-locatable*)

val d = e_rls;

"  --- test100:  nxt_tac order------------------------------------ ";

"  --- test100:  nxt_tac order------------------------------------ ";

val scr as (Script sc) = Script (((inst_abs Test.thy) 

				  o term_of o the o (parse thy))

 "Script Testeq (e_::bool) =                                        \

   \(While (contains_root e_) Do                                     \

   \((Try (Repeat (Rewrite rroot_square_inv False))) @@    \

   \  (Try (Repeat (Rewrite square_equation_left True))) @@ \

   \  (Try (Repeat (Rewrite radd_0 False)))))\

   \ e_            ");

atomty sc;

val (dI',pI',mI') = ("Test.thy",["sqroot-test","univariate","equation","test"],

		     ["Test","sqrt-equ-test"]);

val p = e_pos'; val c = []; 

val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));

val (p,_,_,_,_,pt) = me (mI,m) p c  EmptyPtree;

val nxt = ("Specify_Theory",Specify_Theory "Test.thy");

val (p,_,_,_,_,pt) = me nxt p c pt;

val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]); (*for asm in square_equation_left*)

val (p,_,_,_,_,pt) = me nxt p c pt;

val p = ([1],Res):pos';

val eq_ = (term_of o the o (parse thy))"e_::bool";

val ct =   "0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0";

val ve0_= (term_of o the o (parse thy)) ct;

val ets0=[([],(Tac_(Script.thy,"BS","",""),[(eq_,ve0_)],[(eq_,ve0_)],

	       e_term,e_term,Safe)),

	  ([],(User', [],                [],        e_term, e_term,Sundef))]:ets;

val l0 = [];

" --------------- 1. ---------------------------------------------";

val (pt,_) = cappend_atomic pt[1]e_istate e_term(Rewrite("test",""))(str2term ct,[])Complete;

(*12.10.03:*** Unknown theorem(s) "rroot_square_inv"

val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv",""));

*)

val scr as (Script sc) = 

    Script (((inst_abs Test.thy)  o term_of o the o (parse thy)) 

 "Script Testterm (g_::real) = (Calculate cancel g_)");

(*

val scr as (Script sc) = 

    Script (((inst_abs Test.thy)  o term_of o the o (parse thy)) 

 "Script Testterm (g_::real) = (Calculate power g_)");

val scr as (Script sc) = 

    Script (((inst_abs Test.thy)  o term_of o the o (parse thy)) 

 "Script Testterm (g_::real) = (Calculate pow g_)");

..............................................................*)

writeln

"%%%%%%%%%%TODO 7.9.00---vvvvvv--- conflicts with Isa-types \n\

\     (Repeat (Calculate cancel g_)) Or                     \n\

\     (Repeat (Calculate power g_)) Or                        \n\

\%%%%%%%%%%%%%%%%%%%%%---^^^^^^--- conflicts with Isa-types \n\

\%%%%%%%%%%%%%%%%%%%%%TODO before Detail Rewrite_Set";

"--------- sel_rules ---------------------------------------------";

"--------- sel_rules ---------------------------------------------";

"--------- sel_rules ---------------------------------------------";

 states:=[];

 CalcTree

 [(["equality (x+1=2)", "solveFor x","solutions L"], 

   ("Test.thy", 

    ["sqroot-test","univariate","equation","test"],

    ["Test","squ-equ-test-subpbl1"]))];

 Iterator 1;

 moveActiveRoot 1;

 autoCalculate 1 CompleteCalc;

 val ((pt,_),_) = get_calc 1;

 show_pt pt;

 val tacs = sel_rules pt ([],Pbl);

 if tacs = [Apply_Method ["Test", "squ-equ-test-subpbl1"]] then ()

 else raise error "script.sml: diff.behav. in sel_rules ([],Pbl)";

 val tacs = sel_rules pt ([1],Res);

 if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",

      Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]),

      Check_elementwise "Assumptions"] then ()

 else raise error "script.sml: diff.behav. in sel_rules ([1],Res)";

 val tacs = sel_rules pt ([3],Pbl);

 if tacs = [Apply_Method ["Test", "solve_linear"]] then ()

 else raise error "script.sml: diff.behav. in sel_rules ([3],Pbl)";

 val tacs = sel_rules pt ([3,1],Res);

 if tacs = [Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"),

      Rewrite_Set "Test_simplify"] then ()

 else raise error "script.sml: diff.behav. in sel_rules ([3,1],Res)";

 val tacs = sel_rules pt ([3],Res);

 if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",

      Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]),

      Check_elementwise "Assumptions"] then ()

 else raise error "script.sml: diff.behav. in sel_rules ([3],Res)";

 val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str];

 if tacs = [Tac "no tactics applicable at the end of a calculation"] then ()

 else raise error "script.sml: diff.behav. in sel_rules ([],Res)";