test/Tools/isac/ProgLang/scrtools.sml
changeset 52105 2786cc9704c8
parent 48790 98df8f6dc3f9
child 55380 7be2ad0e4acb
     1.1 --- a/test/Tools/isac/ProgLang/scrtools.sml	Mon Sep 16 11:28:43 2013 +0200
     1.2 +++ b/test/Tools/isac/ProgLang/scrtools.sml	Mon Sep 16 12:20:00 2013 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  "-------- test the same called by interSteps norm_Poly -----------";
     1.5  "-------- test the same called by interSteps norm_Rational -------";
     1.6  "-------- check auto-gen.script for Rewrite_Set_Inst -------------";
     1.7 +"-------- how to stepwise construct Scripts ----------------------";
     1.8  "-----------------------------------------------------------------";
     1.9  "-----------------------------------------------------------------";
    1.10  "-----------------------------------------------------------------";
    1.11 @@ -187,4 +188,50 @@
    1.12  init_istate (Rewrite_Set_Inst (["(bdv, x)"], "integration_rules")) 
    1.13  			      (str2term "someTermWithBdv");
    1.14  
    1.15 +"-------- how to stepwise construct Scripts ----------------------";
    1.16 +"-------- how to stepwise construct Scripts ----------------------";
    1.17 +"-------- how to stepwise construct Scripts ----------------------";
    1.18 +val thy = @{theory "Rational"};
    1.19 +(*no trailing _*)
    1.20 +val p1 = parse thy (
    1.21 +"Script SimplifyScript (t_t::real) =                             " ^
    1.22 +"  (Rewrite_Set discard_minus False                   " ^
    1.23 +"   t_t)");
    1.24  
    1.25 +(*required (): (Rewrite_Set discard_minus False)*)
    1.26 +val p2 = parse thy (
    1.27 +"Script SimplifyScript (t_t::real) =                             " ^
    1.28 +"  (Rewrite_Set discard_minus False                   " ^
    1.29 +"   t_t)");
    1.30 +
    1.31 +val p3 = parse thy (
    1.32 +"Script SimplifyScript (t_t::real) =                             " ^
    1.33 +"  ((Rewrite_Set discard_minus False)                   " ^
    1.34 +"   t_t)");
    1.35 +
    1.36 +val p4 = parse thy (
    1.37 +"Script SimplifyScript (t_t::real) =                             " ^
    1.38 +"  ((Rewrite_Set discard_minus False)                   " ^
    1.39 +"   t_t)");
    1.40 +
    1.41 +val p5 = parse thy (
    1.42 +"Script SimplifyScript (t_t::real) =                             " ^
    1.43 +"  ((Try (Rewrite_Set discard_minus False)                   " ^
    1.44 +"    Try (Rewrite_Set discard_parentheses False))               " ^
    1.45 +"   t_t)");
    1.46 +
    1.47 +val p6 = parse thy (
    1.48 +"Script SimplifyScript (t_t::real) =                             " ^
    1.49 +"  ((Try (Rewrite_Set discard_minus False) @@                   " ^
    1.50 +"    Try (Rewrite_Set rat_mult_poly False) @@                    " ^
    1.51 +"    Try (Rewrite_Set make_rat_poly_with_parentheses False) @@   " ^
    1.52 +"    Try (Rewrite_Set cancel_p_rls False) @@                     " ^
    1.53 +"    (Repeat                                                     " ^
    1.54 +"     ((Try (Rewrite_Set add_fractions_p_rls False) @@        " ^
    1.55 +"       Try (Rewrite_Set rat_mult_div_pow False) @@              " ^
    1.56 +"       Try (Rewrite_Set make_rat_poly_with_parentheses False) @@" ^
    1.57 +"       Try (Rewrite_Set cancel_p_rls False) @@                  " ^
    1.58 +"       Try (Rewrite_Set rat_reduce_1 False)))) @@               " ^
    1.59 +"    Try (Rewrite_Set discard_parentheses False))               " ^
    1.60 +"   t_t)"
    1.61 +);