(* tests on tools for scripts

    author: Walther Neuper

    060605,

    (c) due to copyright terms

 use"../smltest/Scripts/scrtools.sml";

 use"scrtools.sml";

 *)

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

 "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 -------------";

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

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

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

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

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

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

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

 writeln(term2str auto_script);

 atomty auto_script;

 store_met

  (prep_met Test.thy "met_testinter" [] e_metID

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

   [("#Given" ,["term t_"]),

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

    ],

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

    crls=tval_rls, nrls=e_rls},

 "Script Stepwise 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_"

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

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

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

  ));

 show_mets(); 

 val {scr = Script 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.thy",["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 raise 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 = Script auto_script,...} = assoc_rls "norm_Poly";

 writeln(term2str auto_script);

 atomty auto_script;

 states:=[];

 CalcTree

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

   ("Poly.thy",["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 raise 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 = Script auto_script,...} = assoc_rls "norm_Rational";

 writeln(term2str auto_script);

 atomty auto_script;

 (***

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

 *** . Free (t_, 'z)

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

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

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

 *** . . . . Free (discard_minus_, Script.ID)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 *** . . . . . . . . Free (discard_parentheses_, Script.ID)

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

 *** . . Free (t_, 'a)

 ***)

 states:=[];

 CalcTree

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

   ("Poly.thy",["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"], []) => ()

   | _ => raise 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 = Script auto_script,...} = rls;

 writeln(term2str auto_script);

 if contain_bdv (get_rules rls) then ()

 else raise 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");