diff -r 5100a9c3abf8 -r 875b6efa7ced src/Pure/isac/smltest/Scripts/scrtools.sml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/isac/smltest/Scripts/scrtools.sml	Wed Jul 21 13:53:39 2010 +0200
@@ -0,0 +1,193 @@
+(* 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");