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

 "-------- how to stepwise construct Scripts -------";(*TODO remove -- partial_function is easier*)

 "-------- compare Scripts: xxx :: ID --> ''xxx'' :: char list ----------------";

 "-------- Handle Var from parsing by partial_function ------------------------";

 "-------- Compare program terms: from old parsing | from partial_function ----";

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

 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*)

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

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

 );

 "-------- compare Scripts: xxx :: ID --> ''xxx'' :: char list ----------------";

 "-------- compare Scripts: xxx :: ID --> ''xxx'' :: char list ----------------";

 "-------- compare Scripts: xxx :: ID --> ''xxx'' :: char list ----------------";

 (* meth for Minisubpbl ["Test", "squ-equ-test-subpbl1"] *)

 val prog_str_'''' = (* string constants: the intermediate version before partial_function *)

   "Script Solve_root_equation (e_e::bool) (v_v::real) =                  " ^

   " (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@           " ^

   "             (Try (Rewrite_Set ''Test_simplify'' False))) e_e;        " ^

   "     (L_L::bool list) =                                               " ^

   "            (SubProblem (''TestX'',                                   " ^

   "                [''LINEAR'', ''univariate'', ''equation'', ''test''], " ^

   "                [''Test'', ''solve_linear''])                         " ^

   "              [BOOL e_e, REAL v_v])                                   " ^

   "  in Check_elementwise L_L {(v_v::real). Assumptions})                ";

 val prog_str_Free = (* Free varibles: the version up to now *)

   "Script Solve_root_equation (e_e::bool) (v_v::real) =                  " ^

   " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@               " ^

   "             (Try (Rewrite_Set Test_simplify False))) e_e;            " ^

   "     (L_L::bool list) =                                               " ^

   "            (SubProblem (TestX,                                       " ^

   "                [LINEAR, univariate, equation, test],                 " ^

   "                [Test, solve_linear])                                 " ^

   "              [BOOL e_e, REAL v_v])                                   " ^

   "  in Check_elementwise L_L {(v_v::real). Assumptions})                "

 (* term with string constants *)

 val prog_'''' = (TermC.inst_abs o Thm.term_of o the o (TermC.parse @{theory})) prog_str_''''

 val Const ("Test.Solve'_root'_equation", _) $

      Free ("e_e", _) $ Free ("v_v", _) $

      (Const ("HOL.Let", _) $

        (Const ("Script.Seq", _) $

          (Const ("Script.Try", _) $

            (Const ("Script.Rewrite'_Set", _) $

              norm_equation_'''' $ Const ("HOL.False", _))) $

          (Const ("Script.Try", _) $

            (Const ("Script.Rewrite'_Set", _) $

              Test_simplify_'''' $ Const ("HOL.False", _))) $

          Free ("e_e", _)) $

        Abs ("e_e", _,

          Const ("HOL.Let", _) $

            (Const ("Script.SubProblem", _) $

              (Const ("Product_Type.Pair", _) $ TestX_'''' $

                (Const ("Product_Type.Pair", _) $

                  pblkey_'''' $ metkey_'''')) $

              args) $

            Abs ("L_L", _,

              Const ("Script.Check'_elementwise", _) $ Free _ $ (_ $ _)))) = prog_''''

 ;

 (* term with Free varibles *)

 val prog_Free = (TermC.inst_abs o Thm.term_of o the o (TermC.parse @{theory})) prog_str_Free

 val Const ("Test.Solve'_root'_equation", _) $

      Free ("e_e", _) $ Free ("v_v", _) $

      (Const ("HOL.Let", _) $

        (Const ("Script.Seq", _) $

          (Const ("Script.Try", _) $

            (Const ("Script.Rewrite'_Set", _) $

              norm_equation_Free $ Const ("HOL.False", _))) $

          (Const ("Script.Try", _) $

            (Const ("Script.Rewrite'_Set", _) $

              Test_simplify_Free $ Const ("HOL.False", _))) $

          Free ("e_e", _)) $

        Abs ("e_e", _,

          Const ("HOL.Let", _) $

            (Const ("Script.SubProblem", _) $

              (Const ("Product_Type.Pair", _) $ TestX_Free $

                (Const ("Product_Type.Pair", _) $

                  pblkey_Free $ metkey_Free)) $ 

              args) $

            Abs ("L_L", _,

              Const ("Script.Check'_elementwise", _) $ Free _ $ (_ $ _)))) = prog_Free

 ;

 (* compare term with string constants and term with Free varibles *)

 if HOLogic.dest_string norm_equation_'''' = "norm_equation" then () else error "dest_string 1";

 (* --------------------- string constants = Free varibles *)

 if HOLogic.dest_string norm_equation_'''' =  Term.term_name norm_equation_Free then () else error "";

 if HOLogic.dest_string Test_simplify_'''' =  Term.term_name Test_simplify_Free then () else error "";

 if HOLogic.dest_string TestX_'''' =  Term.term_name TestX_Free then () else error "dest_string 2";

 if (pblkey_'''' |> HOLogic.dest_list |> map HOLogic.dest_string) =

   ["LINEAR", "univariate", "equation", "test"] then () else error "dest_string 3";

 (* --------------------- string constants = Free varibles *)

 if (pblkey_'''' |> HOLogic.dest_list |> map HOLogic.dest_string) =

    (pblkey_Free |> HOLogic.dest_list |> map Term.term_name) then () else error "dest_string 4";

 if (metkey_'''' |> HOLogic.dest_list |> map HOLogic.dest_string) =

    (metkey_Free |> HOLogic.dest_list |> map Term.term_name) then () else error "dest_string 5";

 "-------- Handle Var from parsing by partial_function ------------------------";

 "-------- Handle Var from parsing by partial_function ------------------------";

 "-------- Handle Var from parsing by partial_function ------------------------";

 (* (1) parsing proprietary as used up to now *)

 val prog_str_'''' =

   "xxx e_e = (let e_e = (Rewrite_Set ''yyy'' False) e_e in [e_e])"

 val prog_'''' = ((*TermC.inst_abs o*) Thm.term_of o the o (TermC.parse @{theory})) prog_str_''''

 (*Output: val prog_'''' = ... $ (Const ("HOL.Let", "bool... )... $ Free ("e_e", "bool")) $ ...*)

 (* (2) parsing by funpack: take the definition from test/../ProgLang/scrtools.thy *)

 val prog_part = (HOLogic.dest_Trueprop o Thm.prop_of) @{thm simplify.simps}

 (*Output: val prog_part = ... $ (Const ("HOL.Let", "bool... )... $ Var (("e_e", 0), "bool")) $ ...*)

 ;

 Logic.unvarify_global: term -> term

 ;

 val prog_part = (Logic.unvarify_global o HOLogic.dest_Trueprop o Thm.prop_of) @{thm simplify.simps};

 (*val prog_part = ... $ (Const ("HOL.Let", "bool... )... $ Var (("e_e", 0), "bool")) $ ...*)

 (* (3) compare (1)..(2) *)

 if prog_'''' = prog_part then () else error "appl of Logic.unvarify_global changed"

 "-------- Compare program terms: from old parsing | from partial_function ----";

 "-------- Compare program terms: from old parsing | from partial_function ----";

 "-------- Compare program terms: from old parsing | from partial_function ----";

 (* meth for Minisubpbl ["Test", "squ-equ-test-subpbl1"] *)

 (* (1) parsing proprietary as used up to now *)

 val prog_str_'''' = (* string constants: the intermediate version before partial_function *)

   "Script Solve_root_equation (e_e::bool) (v_v::real) =                  " ^

   " (let e_e = ((Try (Rewrite_Set ''norm_equation'' False)) @@           " ^

   "             (Try (Rewrite_Set ''Test_simplify'' False))) e_e;        " ^

   "     (L_L::bool list) =                                               " ^

   "            (SubProblem (''TestX'',                                   " ^

   "                [''LINEAR'', ''univariate'', ''equation'', ''test''], " ^

   "                [''Test'', ''solve_linear''])                         " ^

   "              [BOOL e_e, REAL v_v])                                   " ^

   "  in Check_elementwise L_L {(v_v::real). Assumptions})                ";

 val prog_'''' = (TermC.inst_abs o Thm.term_of o the o (TermC.parse @{theory})) prog_str_''''

 (* body_of ---> src/../scrtools.sml for test with old parsing *)

 fun body_of_'''' (_ $ body) = body

   | body_of_'''' t = raise TERM ("body_of", [t])

 val body_'''' = body_of_'''' prog_'''';

 term2str body_''''; (* with TermC.inst_abs:

      "let e_ea =\n      (Try (Rewrite_Set ''norm_equation'' False) @@\n       Try (Rewrite_Set ''Test_simplify'' False))\n       e_e;\n    L_La =\n      SubProblem\n       (''TestX'', [''LINEAR'', ''univariate'', ''equation'', ''test''],\n        [''Test'', ''solve_linear''])\n       [BOOL e_e, REAL v_v]\nin Check_elementwise L_L {v_v. Assumptions}":

 ------------------------> e_e;  Free ("e_e", "bool"))

 *)

 (* formal_args in src/../scrtools.sml*)

 fun formal_args_'''' scr = (fst o split_last o snd o strip_comb) scr;

 val args_'''' = formal_args_'''' prog_'''';

 case args_'''' of [Free ("e_e", _), Free ("v_v", _)] => ()

 | _ => error "formal_args";

 (* (2) parsing by funpack: take the definition from test/../ProgLang/scrtools.thy *)

 val prog_part = Thm.prop_of @{thm minisubpbl.simps}

 (* body_of ---> src/../scrtools.sml BEFORE above, new body_of *)

 fun body_of_part t = (t

   |> HOLogic.dest_Trueprop

   |> HOLogic.dest_eq

   |> snd

   |> Logic.unvarify_global

   |> TermC.inst_abs)

 handle TERM _ => raise TERM ("body_of", [t])

 val body_part = body_of_part prog_part;

 term2str body_part; (* with TermC.inst_abs, without:

      "let e_ea =\n      (Try (Rewrite_Set ''norm_equation'' False) @@\n       Try (Rewrite_Set ''Test_simplify'' False))\n       ?e_e;\n    L_La =\n      SubProblem\n       (''TestX'', [''LINEAR'', ''univariate'', ''equation'', ''test''],\n        [''Test'', ''solve_linear''])\n       [BOOL e_e, REAL ?v_v]\nin Check_elementwise L_L {v_v. Assumptions}":

 ------------------------> ?e_e;  Var (("e_e", 0), "bool"))

 *)

 (* formal_args ---> src/../scrtools.sml BEFORE old formal_args *)

 fun formal_args_part prog = (prog

   |> HOLogic.dest_Trueprop

   |> HOLogic.dest_eq

   |> fst

   |> Logic.unvarify_global

   |> strip_comb

   |> snd

 )

 handle TERM _ => raise TERM ("formal_args", [t])

 val args_part = formal_args_part prog_part;

 (* (3) compare (1)..(2) *)

 if body_'''' = body_part then () else error "body_of changed";

 if args_'''' = args_part then () else error "formal_args changed"