wneuper/isa: test/Tools/isac/ProgLang/scrtools.sml@7be2ad0e4acb

     1 (* Title: tests on tools for scripts

     2    Author: Walther Neuper 060605

     3    (c) due to copyright terms

     4 *)

     5 "-----------------------------------------------------------------";

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

     7 "-----------------------------------------------------------------";

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

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

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

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

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

    13 "-----------------------------------------------------------------";

    14 "-----------------------------------------------------------------";

    15 "-----------------------------------------------------------------";

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

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

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

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

    22 writeln(term2str auto_script);

    23 atomty auto_script;

    25 show_mets();

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

    27 writeln(term2str parsed_script);

    28 atomty parsed_script;

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

    31 states:=[];

    32 CalcTree

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

    34 	   "normalform N"],

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

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

    37 Iterator 1;

    38 moveActiveRoot 1;

    39 autoCalculate 1 CompleteCalcHead;

    41 fetchProposedTactic 1  (*..Apply_Method*);

    42 autoCalculate 1 (Step 1);

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

    45 fetchProposedTactic 1  (*discard_minus_*);

    46 autoCalculate 1 (Step 1);

    48 fetchProposedTactic 1  (*order_add_rls_*);

    49 autoCalculate 1 (Step 1);

    51 fetchProposedTactic 1  (*collect_numerals_*);

    52 autoCalculate 1 (Step 1);

    54 autoCalculate 1 CompleteCalc;

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

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

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

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

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

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

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

    65 writeln(term2str auto_script);

    66 atomty auto_script;

    68 states:=[];

    69 CalcTree

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

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

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

    73 Iterator 1;

    74 moveActiveRoot 1;

    75 autoCalculate 1 CompleteCalc;

    77 interSteps 1 ([], Res);

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

    80 interSteps 1 ([1], Res);

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

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

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

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

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

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

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

    92 writeln(term2str auto_script);

    93 atomty auto_script;

    94 (***

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

    96 *** . Free (t_t, 'z)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   127 ***)

   128 states:=[];

   129 CalcTree

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

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

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

   133 Iterator 1;

   134 moveActiveRoot 1;

   135 autoCalculate 1 CompleteCalc;

   137 interSteps 1 ([], Res);

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

   140 interSteps 1 ([1], Res);

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

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

   144        \  ((Rewrite_Set norm_Rational False) t_)"

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

   146 *)

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

   148 case (term2str form, tac, terms2strs asm) of

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

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

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

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

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

   155 val rls = assoc_rls "integration";

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

   157 writeln(term2str auto_script);

   159 if contain_bdv (get_rules rls) then ()

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

   162 two_scr_arg auto_script;

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

   164 			      (str2term "someTermWithBdv");

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

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

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

   169 val thy = @{theory "Rational"};

   170 (*no trailing _*)

   171 val p1 = parse thy (

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

   173 "  (Rewrite_Set discard_minus False                   " ^

   174 "   t_t)");

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

   177 val p2 = parse thy (

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

   179 "  (Rewrite_Set discard_minus False                   " ^

   180 "   t_t)");

   182 val p3 = parse thy (

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

   184 "  ((Rewrite_Set discard_minus False)                   " ^

   185 "   t_t)");

   187 val p4 = parse thy (

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

   189 "  ((Rewrite_Set discard_minus False)                   " ^

   190 "   t_t)");

   192 val p5 = parse thy (

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

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

   195 "    Try (Rewrite_Set discard_parentheses False))               " ^

   196 "   t_t)");

   198 val p6 = parse thy (

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

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

   201 "    Try (Rewrite_Set rat_mult_poly False) @@                    " ^

   202 "    Try (Rewrite_Set make_rat_poly_with_parentheses False) @@   " ^

   203 "    Try (Rewrite_Set cancel_p_rls False) @@                     " ^

   204 "    (Repeat                                                     " ^

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

   206 "       Try (Rewrite_Set rat_mult_div_pow False) @@              " ^

   207 "       Try (Rewrite_Set make_rat_poly_with_parentheses False) @@" ^

   208 "       Try (Rewrite_Set cancel_p_rls False) @@                  " ^

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

   210 "    Try (Rewrite_Set discard_parentheses False))               " ^

   211 "   t_t)"

   212 );

author	Mathias Lehnfeld <s1210629013@students.fh-hagenberg.at>
	Sun, 02 Feb 2014 03:09:40 +0100
changeset 55380	7be2ad0e4acb
parent 52105	2786cc9704c8
child 55445	33b0f6db720c
permissions	-rw-r--r--