Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/ProgLang/scrtools.sml
author Walther Neuper <neuper@ist.tugraz.at>
Mon, 16 Sep 2013 12:20:00 +0200
changeset 52105 2786cc9704c8
parent 48790 98df8f6dc3f9
child 55380 7be2ad0e4acb
permissions -rw-r--r--
Test_Isac works again, perfectly ..

# the same tests works as in 8df4b6196660 (the *child* of "Test_Isac works...")
# ..EXCEPT those marked with "exception Div raised"
# for general state of tests see Test_Isac section {* history of tests *}. 
     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 "-----------------------------------------------------------------";

    16 

    17 

    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;

    24 

    25 store_met

    26  (prep_met @{theory "Test"} "met_testinter" [] e_metID

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

    28   [("#Given" ,["Term t_t"]),

    29    ("#Find"  ,["normalform n_n"])

    30    ],

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

    32    crls=tval_rls, errpats = [], nrls=e_rls},

    33 "Script Stepwise t_t   =                        \

    34  \(Try (Rewrite_Set discard_minus False) @@     \

    35  \ Try (Rewrite_Set expand_poly False) @@       \

    36  \ Try (Repeat (Calculate TIMES)) @@            \

    37  \ Try (Rewrite_Set order_mult_rls False) @@    \

    38  \ Try (Rewrite_Set simplify_power False) @@    \

    39  \ Try (Rewrite_Set calc_add_mult_pow False) @@ \

    40  \ Try (Rewrite_Set reduce_012_mult False) @@   \

    41  \ Try (Rewrite_Set order_add_rls False) @@     \

    42  \ Try (Rewrite_Set collect_numerals False) @@  \

    43  \ Try (Rewrite_Set reduce_012 False) @@        \

    44  \ Try (Rewrite_Set discard_parentheses False)) \

    45  \ t_t"

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

    47   this t_t must be either 'real' or 'bool'  #1#, 

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

    49  ));

    50 show_mets();  

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

    52 writeln(term2str parsed_script);

    53 atomty parsed_script;

    54 

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

    56 states:=[];

    57 CalcTree

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

    59 	   "normalform N"], 

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

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

    62 Iterator 1;

    63 moveActiveRoot 1;

    64 autoCalculate 1 CompleteCalcHead;

    65 

    66 fetchProposedTactic 1  (*..Apply_Method*);

    67 autoCalculate 1 (Step 1);

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

    69 

    70 fetchProposedTactic 1  (*discard_minus_*);

    71 autoCalculate 1 (Step 1);

    72 

    73 fetchProposedTactic 1  (*order_add_rls_*);

    74 autoCalculate 1 (Step 1);

    75 

    76 fetchProposedTactic 1  (*collect_numerals_*);

    77 autoCalculate 1 (Step 1);

    78 

    79 autoCalculate 1 CompleteCalc;

    80 

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

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

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

    84 

    85 

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

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

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

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

    90 writeln(term2str auto_script);

    91 atomty auto_script;

    92 

    93 states:=[];

    94 CalcTree

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

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

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

    98 Iterator 1;

    99 moveActiveRoot 1;

   100 autoCalculate 1 CompleteCalc;

   101 

   102 interSteps 1 ([], Res);

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

   104 

   105 interSteps 1 ([1], Res);

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

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

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

   109 

   110 

   111 

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

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

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

   115 

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

   117 writeln(term2str auto_script);

   118 atomty auto_script;

   119 (*** 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   152 ***)

   153 states:=[];

   154 CalcTree

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

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

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

   158 Iterator 1;

   159 moveActiveRoot 1;

   160 autoCalculate 1 CompleteCalc;

   161 

   162 interSteps 1 ([], Res);

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

   164 

   165 interSteps 1 ([1], Res);

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

   167 

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

   169        \  ((Rewrite_Set norm_Rational False) t_)"

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

   171 *)

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

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

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

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

   176 

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

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

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

   180 val rls = assoc_rls "integration";

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

   182 writeln(term2str auto_script);

   183 

   184 if contain_bdv (get_rules rls) then ()

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

   186 

   187 two_scr_arg auto_script;

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

   189 			      (str2term "someTermWithBdv");

   190 

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

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

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

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

   195 (*no trailing _*)

   196 val p1 = parse thy (

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

   198 "  (Rewrite_Set discard_minus False                   " ^

   199 "   t_t)");

   200 

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

   202 val p2 = parse thy (

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

   204 "  (Rewrite_Set discard_minus False                   " ^

   205 "   t_t)");

   206 

   207 val p3 = parse thy (

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

   209 "  ((Rewrite_Set discard_minus False)                   " ^

   210 "   t_t)");

   211 

   212 val p4 = parse thy (

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

   214 "  ((Rewrite_Set discard_minus False)                   " ^

   215 "   t_t)");

   216 

   217 val p5 = parse thy (

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

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

   220 "    Try (Rewrite_Set discard_parentheses False))               " ^

   221 "   t_t)");

   222 

   223 val p6 = parse thy (

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

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

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

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

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

   229 "    (Repeat                                                     " ^

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

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

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

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

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

   235 "    Try (Rewrite_Set discard_parentheses False))               " ^

   236 "   t_t)"

   237 );
wneuper/isa