(* 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");