1.1 --- a/test/Tools/isac/Test_Isac.thy Thu Mar 15 15:48:52 2018 +0100
1.2 +++ b/test/Tools/isac/Test_Isac.thy Fri Mar 23 10:14:39 2018 +0100
1.3 @@ -146,6 +146,114 @@
1.4 ML_file "ProgLang/rewrite.sml"
1.5 ML_file "ProgLang/listC.sml"
1.6 ML_file "ProgLang/scrtools.sml"
1.7 +
1.8 +ML {*
1.9 +"~~~~~ fun xxx, args:"; val () = ();
1.10 +*} ML {*
1.11 +"-------- test the same called by interSteps norm_Poly -----------";
1.12 +"-------- test the same called by interSteps norm_Poly -----------";
1.13 +"-------- test the same called by interSteps norm_Poly -----------";
1.14 +val Seq {scr = Prog auto_script,...} = assoc_rls "norm_Poly";
1.15 +writeln(term2str auto_script);
1.16 +(*Script Stepwise t_t =
1.17 + (Try (Rewrite_Set discard_minus False) @@
1.18 + Try (Rewrite_Set expand_poly_ False) @@
1.19 + Try (Repeat (Calculate TIMES)) @@
1.20 + Try (Rewrite_Set order_mult_rls_ False) @@
1.21 + Try (Rewrite_Set simplify_power_ False) @@
1.22 + Try (Rewrite_Set calc_add_mult_pow_ False) @@
1.23 + Try (Rewrite_Set reduce_012_mult_ False) @@
1.24 + Try (Rewrite_Set order_add_rls_ False) @@
1.25 + Try (Rewrite_Set collect_numerals_ False) @@
1.26 + Try (Rewrite_Set reduce_012_ False) @@
1.27 + Try (Rewrite_Set discard_parentheses1 False))
1.28 + ??.empty ..WORKS, NEVERTHELESS *)
1.29 +atomty auto_script;
1.30 +
1.31 +reset_states ();
1.32 +CalcTree
1.33 +[(["Term (b + a - b)", "normalform N"],
1.34 + ("Poly",["polynomial","simplification"],
1.35 + ["simplification","for_polynomials"]))];
1.36 +Iterator 1;
1.37 +moveActiveRoot 1;
1.38 +autoCalculate 1 CompleteCalc;
1.39 +
1.40 +val ((pt,p),_) = get_calc 1;
1.41 +show_pt pt;
1.42 +(* isabisac17 = 15 [
1.43 +(([], Frm), Simplify (b + a - b)),
1.44 +(([1], Frm), b + a - b),
1.45 +(([1], Res), a),
1.46 +(([], Res), a)] *)
1.47 +
1.48 +interSteps 1 ([], Res);
1.49 +val ((pt,p),_) = get_calc 1;
1.50 +show_pt pt;
1.51 +(* isabisac17 = 15 [
1.52 +(([], Frm), Simplify (b + a - b)),
1.53 +(([1], Frm), b + a - b),
1.54 +(([1], Res), a),
1.55 +(([], Res), a)] *)
1.56 +
1.57 +interSteps 1 ([1], Res);
1.58 +(*interSteps 1 ([1], Res)<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 8</ERROR></SYSERROR>*)
1.59 +"~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1], Res));
1.60 + val ((pt, p), tacis) = get_calc cI;
1.61 +(*if*) (not o is_interpos) ip = false;
1.62 +val ip' = lev_pred' pt ip;
1.63 +
1.64 +(*Math_Engine.detailstep pt ip ..ERROR interSteps>..>init_istate: "norm_Poly" has EmptyScr*)
1.65 +"~~~~~ fun detailstep, args:"; val (pt, (pos as (p, _))) = (pt, ip);
1.66 + val nd = Ctree.get_nd pt p
1.67 + val cn = Ctree.children nd;
1.68 +(*if*) null cn = true;
1.69 +(*if*) (Tac.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)] = true;
1.70 +
1.71 +(*Solve.detailrls pt pos ..ERROR interSteps>..>init_istate: "norm_Poly" has EmptyScr*)
1.72 +"~~~~~ fun detailrls, args:"; val (pt, (pos as (p, _))) = (pt, pos);
1.73 + val t = get_obj g_form pt p
1.74 + val tac = get_obj g_tac pt p
1.75 + val rls = (assoc_rls o Tac.rls_of) tac
1.76 + val ctxt = get_ctxt pt pos
1.77 +val Seq _ = (*case*) rls (*of*);
1.78 +
1.79 +(* val is = Generate.init_istate tac t ..ERROR ,,>..>init_istate: "norm_Poly" has EmptyScr*)
1.80 +"~~~~~ fun init_istate, args:"; val ((Tac.Rewrite_Set rls), t) = (tac, t);
1.81 +val Celem.Seq {scr = Celem.Prog s,...} = (*case*) assoc_rls rls (*of*);
1.82 +
1.83 +"~~~~~ to detailrls return val:"; val is = (Selem.ScrState ([(LTool.one_scr_arg s, t)], [], NONE, Celem.e_term, Selem.Sundef, true))
1.84 + val tac_ = Tac.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
1.85 + val pos' = ((lev_on o lev_dn) p, Ctree.Frm)
1.86 + val thy = Celem.assoc_thy "Isac"
1.87 + val (_, _, _, pt') = Generate.generate1 thy tac_ (is, ctxt) pos' pt (* implicit Take *)
1.88 + val (_,_, (pt'', _)) = complete_solve CompleteSubpbl [] (pt', pos')
1.89 + val newnds = children (get_nd pt'' p)
1.90 + val pt''' = ins_chn newnds pt p (*complete_solve cuts branches after*);
1.91 +
1.92 +"~~~~~ to detailstep return val:"; val xxx = ("detailrls", pt''', (p @ [length newnds], Res));
1.93 +"~~~~~ to interSteps return val:"; val ("detailrls", pt, lastpos) = xxx;
1.94 +show_pt pt;
1.95 +(*[
1.96 +(([], Frm), Simplify (b + a - b)),
1.97 +(([1], Frm), b + a - b),
1.98 +(([1,1], Frm), b + a - b),
1.99 +(([1,1], Res), b + a + -1 * b),
1.100 +(([1,2], Res), a + b + -1 * b),
1.101 +(([1,3], Res), a + 0 * b),
1.102 +(([1,4], Res), a),
1.103 +(([1], Res), a),
1.104 +(([], Res), a)]*)
1.105 +if existpt' ([1,4], Res) pt then ()
1.106 +else error "scrtools.sml: auto-generated norm_Poly doesnt work";
1.107 +*} ML {*
1.108 +*} ML {*
1.109 +*} ML {*
1.110 +*} ML {*
1.111 +*} ML {*
1.112 +"~~~~~ fun xxx, args:"; val () = ();
1.113 +*}
1.114 +
1.115 ML_file "ProgLang/tools.sml"
1.116 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
1.117 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
1.118 @@ -155,6 +263,7 @@
1.119 ML_file "Minisubpbl/100-init-rootpbl.sml"
1.120 ML_file "Minisubpbl/150-add-given.sml"
1.121 ML_file "Minisubpbl/200-start-method.sml"
1.122 + ML_file "Minisubpbl/250-Rewrite_Set-from-method.sml"
1.123 ML_file "Minisubpbl/300-init-subpbl.sml"
1.124 ML_file "Minisubpbl/400-start-meth-subpbl.sml"
1.125 ML_file "Minisubpbl/490-nxt-Check_Postcond.sml"