(* Title: tests on tools for scripts

   Author: Walther Neuper 060605

   (c) due to copyright terms

*)

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

"table of contents -----------------------------------------------";

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

"-------- test auto-generated script '(Repeat (Calculate times))'-";

"-------- test the same called by interSteps norm_Poly -----------";

"-------- test the same called by interSteps norm_Rational -------";

"-------- check auto-gen.script for Rewrite_Set_Inst -------------";

"-------- how to stepwise construct Scripts ----------------------";

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

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

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

"-------- test auto-generated script '(Repeat (Calculate times))'-";

"-------- test auto-generated script '(Repeat (Calculate times))'-";

"-------- test auto-generated script '(Repeat (Calculate times))'-";

val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";

writeln(term2str auto_script);

atomty auto_script;

store_met

 (prep_met @{theory "Test"} "met_testinter" [] e_metID

 (["Test","test_interSteps_1"]:metID,

  [("#Given" ,["Term t_t"]),

   ("#Find"  ,["normalform n_n"])

   ],

  {rew_ord' = "dummy_ord", rls' = tval_rls, calc = [], srls = e_rls, prls = e_rls,

   crls=tval_rls, errpats = [], nrls=e_rls},

"Script Stepwise t_t   =                        \

 \(Try (Rewrite_Set discard_minus False) @@     \

 \ Try (Rewrite_Set expand_poly False) @@       \

 \ Try (Repeat (Calculate TIMES)) @@            \

 \ Try (Rewrite_Set order_mult_rls False) @@    \

 \ Try (Rewrite_Set simplify_power False) @@    \

 \ Try (Rewrite_Set calc_add_mult_pow False) @@ \

 \ Try (Rewrite_Set reduce_012_mult False) @@   \

 \ Try (Rewrite_Set order_add_rls False) @@     \

 \ Try (Rewrite_Set collect_numerals False) @@  \

 \ Try (Rewrite_Set reduce_012 False) @@        \

 \ Try (Rewrite_Set discard_parentheses False)) \

 \ t_t"

(*presently this script cannot become equal in types to auto_script, because:

  this t_t must be either 'real' or 'bool'  #1#, 

  while the auto_script must be 'z and type-instantiated before usage*)

 ));

show_mets();  

val {scr = Prog parsed_script,...} = get_met ["Test","test_interSteps_1"];

writeln(term2str parsed_script);

atomty parsed_script;

(*the structure of the auto-gen. script is interpreted correctly*)

states:=[];

CalcTree

[(["Term (b + a - b)",(*this is Schalk 299b*)

	   "normalform N"], 

  ("Poly",["polynomial","simplification"],

  ["Test","test_interSteps_1"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalcHead;

fetchProposedTactic 1  (*..Apply_Method*);

autoCalculate 1 (Step 1);

getTactic 1 ([1], Frm)  (*still empty*);

fetchProposedTactic 1  (*discard_minus_*);

autoCalculate 1 (Step 1);

fetchProposedTactic 1  (*order_add_rls_*);

autoCalculate 1 (Step 1);

fetchProposedTactic 1  (*collect_numerals_*);

autoCalculate 1 (Step 1);

autoCalculate 1 CompleteCalc;

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

if existpt' ([1], Frm) pt then ()

else error "scrtools.sml: test-script test_interSteps_1 doesnt work";

"-------- test the same called by interSteps norm_Poly -----------";

"-------- test the same called by interSteps norm_Poly -----------";

"-------- test the same called by interSteps norm_Poly -----------";

val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";

writeln(term2str auto_script);

atomty auto_script;

states:=[];

CalcTree

[(["Term (b + a - b)", "normalform N"], 

  ("Poly",["polynomial","simplification"],

  ["simplification","for_polynomials"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

interSteps 1 ([], Res);

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

interSteps 1 ([1], Res);

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

if existpt' ([1,4], Res) pt then ()

else error  "scrtools.sml: auto-generated norm_Poly doesnt work";

"-------- test the same called by interSteps norm_Rational -------";

"-------- test the same called by interSteps norm_Rational -------";

"-------- test the same called by interSteps norm_Rational -------";

val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Rational";

writeln(term2str auto_script);

atomty auto_script;

(*** 

*** Const (Script.Stepwise, 'z => 'z => 'z)

*** . Free (t_t, 'z)

*** . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)

*** . . Const (Script.Try, ('a => 'a) => 'a => 'a)

*** . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)

*** . . . . Free (discard_minus, ID)

*** . . . . Const (HOL.False, bool)

*** . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)

*** . . . Const (Script.Try, ('a => 'a) => 'a => 'a)

*** . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)

*** . . . . . Free (rat_mult_poly, ID)

*** . . . . . Const (HOL.False, bool)

*** . . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)

*** . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)

*** . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)

*** . . . . . . Free (make_rat_poly_with_parentheses, ID)

*** . . . . . . Const (HOL.False, bool)

*** . . . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)

*** . . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)

*** . . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)

*** . . . . . . . Free (cancel_p_rls, ID)

*** . . . . . . . Const (HOL.False, bool)

*** . . . . . Const (Script.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)

*** . . . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)

*** . . . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)

*** . . . . . . . . Free (norm_Rational_rls, ID)

*** . . . . . . . . Const (HOL.False, bool)

*** . . . . . . Const (Script.Try, ('a => 'a) => 'a => 'a)

*** . . . . . . . Const (Script.Rewrite'_Set, ID => bool => 'a => 'a)

*** . . . . . . . . Free (discard_parentheses1, ID)

*** . . . . . . . . Const (HOL.False, bool)

*** . . Const (empty, 'a)

***)

states:=[];

CalcTree

[(["Term (b + a - b)", "normalform N"], 

  ("Poly",["polynomial","simplification"],

  ["simplification","of_rationals"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

interSteps 1 ([], Res);

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

interSteps 1 ([1], Res);

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

(*with "Script SimplifyScript (t_::real) =                \

       \  ((Rewrite_Set norm_Rational False) t_)"

val (Form form, SOME tac, asm) = pt_extract (pt, ([1], Res));

*)

val (Form form, SOME tac, asm) = pt_extract (pt, ([2], Res));

case (term2str form, tac, terms2strs asm) of

    ("a", Check_Postcond ["polynomial", "simplification"], []) => ()

  | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work";

"-------- check auto-gen.script for Rewrite_Set_Inst -------------";

"-------- check auto-gen.script for Rewrite_Set_Inst -------------";

"-------- check auto-gen.script for Rewrite_Set_Inst -------------";

val rls = assoc_rls "integration";

val Seq {scr = Prog auto_script,...} = rls;

writeln(term2str auto_script);

if contain_bdv (get_rules rls) then ()

else error "scrtools.sml: contain_bdv doesnt work for 'integration'";

two_scr_arg auto_script;

init_istate (Rewrite_Set_Inst (["(bdv, x)"], "integration_rules")) 

			      (str2term "someTermWithBdv");

"-------- how to stepwise construct Scripts ----------------------";

"-------- how to stepwise construct Scripts ----------------------";

"-------- how to stepwise construct Scripts ----------------------";

val thy = @{theory "Rational"};

(*no trailing _*)

val p1 = parse thy (

"Script SimplifyScript (t_t::real) =                             " ^

"  (Rewrite_Set discard_minus False                   " ^

"   t_t)");

(*required (): (Rewrite_Set discard_minus False)*)

val p2 = parse thy (

"Script SimplifyScript (t_t::real) =                             " ^

"  (Rewrite_Set discard_minus False                   " ^

"   t_t)");

val p3 = parse thy (

"Script SimplifyScript (t_t::real) =                             " ^

"  ((Rewrite_Set discard_minus False)                   " ^

"   t_t)");

val p4 = parse thy (

"Script SimplifyScript (t_t::real) =                             " ^

"  ((Rewrite_Set discard_minus False)                   " ^

"   t_t)");

val p5 = parse thy (

"Script SimplifyScript (t_t::real) =                             " ^

"  ((Try (Rewrite_Set discard_minus False)                   " ^

"    Try (Rewrite_Set discard_parentheses False))               " ^

"   t_t)");

val p6 = parse thy (

"Script SimplifyScript (t_t::real) =                             " ^

"  ((Try (Rewrite_Set discard_minus False) @@                   " ^

"    Try (Rewrite_Set rat_mult_poly False) @@                    " ^

"    Try (Rewrite_Set make_rat_poly_with_parentheses False) @@   " ^

"    Try (Rewrite_Set cancel_p_rls False) @@                     " ^

"    (Repeat                                                     " ^

"     ((Try (Rewrite_Set add_fractions_p_rls False) @@        " ^

"       Try (Rewrite_Set rat_mult_div_pow False) @@              " ^

"       Try (Rewrite_Set make_rat_poly_with_parentheses False) @@" ^

"       Try (Rewrite_Set cancel_p_rls False) @@                  " ^

"       Try (Rewrite_Set rat_reduce_1 False)))) @@               " ^

"    Try (Rewrite_Set discard_parentheses False))               " ^

"   t_t)"

);