1.1 --- a/test/Tools/isac/Interpret/script.sml Wed Mar 14 17:12:43 2012 +0100
1.2 +++ b/test/Tools/isac/Interpret/script.sml Sat Mar 17 11:06:46 2012 +0100
1.3 @@ -11,6 +11,7 @@
1.4 "----------- fun init_form, fun get_stac -------------------------";
1.5 "----------- x+1=2 start SubProblem 'stac2tac_ TODO: no match for ";
1.6 "----------- Take as 1st stac in script --------------------------";
1.7 +"----------- 'trace_script' from outside 'fun me '----------------";
1.8 "-----------------------------------------------------------------";
1.9 "-----------------------------------------------------------------";
1.10 "-----------------------------------------------------------------";
1.11 @@ -399,3 +400,98 @@
1.12 (line 908 of "/usr/local/isabisac/src/Tools/isac/Interpret/ctree.sml")*)
1.13
1.14
1.15 +"----------- 'trace_script' from outside 'fun me '----------------";
1.16 +"----------- 'trace_script' from outside 'fun me '----------------";
1.17 +"----------- 'trace_script' from outside 'fun me '----------------";
1.18 +val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
1.19 +val (dI',pI',mI') =
1.20 + ("Test", ["sqroot-test","univariate","equation","test"],
1.21 + ["Test","squ-equ-test-subpbl1"]);
1.22 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.23 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.24 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.25 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.26 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.27 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.28 +val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.29 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
1.30 +(*from_pblobj_or_detail': no istate = from_pblobj_or_detail' "Isac" p pt;*)
1.31 +
1.32 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*---------------------------------------------------*)
1.33 +val (p'''', pt'''') = (p, pt);
1.34 +f2str f = "x + 1 = 2"; snd nxt = Rewrite_Set "norm_equation";
1.35 +val (p, p_) = p(* = ([1], Frm)*);
1.36 +val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.37 +val (env, loc_, curry_arg, res, Safe, true) = scrstate;
1.38 + env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
1.39 + loc_ = [];
1.40 + curry_arg = NONE;
1.41 + term2str res = "??.empty"; (* scrstate before starting interpretation *)
1.42 +(*term2str (go loc_ sc) = "Script Solve_root_equation e_e v_v = ...*)
1.43 +
1.44 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
1.45 +val (p'''', pt'''') = (p, pt);
1.46 +f2str f = "x + 1 + -1 * 2 = 0"; snd nxt = Rewrite_Set "Test_simplify";
1.47 +val (p, p_) = p(* = ([1], Res)*);
1.48 +val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.49 +val (env, loc_, curry_arg, res, Safe, true) = scrstate;
1.50 + env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
1.51 + loc_ = [R, L, R, L, L, R, R];
1.52 + curry_arg = SOME (str2term "e_e::bool");
1.53 + term2str res = "x + 1 + -1 * 2 = 0";(* scrstate after norm_equation, before Test_simplify *)
1.54 +term2str (go loc_ sc) = "Rewrite_Set norm_equation False";
1.55 +
1.56 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
1.57 +val (p'''', pt'''') = (p, pt);
1.58 +f2str f = "-1 + x = 0"; snd nxt = Subproblem ("Test", ["linear", "univariate", "equation", "test"]);
1.59 +val (p, p_) = p(* = ([2], Res)*);
1.60 +val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.61 +val (env, loc_, curry_arg, res, Safe, false) = scrstate;
1.62 + env2str env = "[\"\n(e_e, x + 1 = 2)\",\"\n(v_v, x)\"]";
1.63 + loc_ = [R, L, R, L, R, R];
1.64 + curry_arg = SOME (str2term "e_e::bool");
1.65 + term2str res = "-1 + x = 0"; (* scrstate after Test_simplify, before Subproblem *)
1.66 +term2str (go loc_ sc) = "Rewrite_Set Test_simplify False";
1.67 +
1.68 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
1.69 +val (p'''', pt'''') = (p, pt); (*f2str f = exception Match; ...is a model, not a formula*)
1.70 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
1.71 +val (p'''', pt'''') = (p, pt);
1.72 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
1.73 +val (p'''', pt'''') = (p, pt);
1.74 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
1.75 +val (p'''', pt'''') = (p, pt);
1.76 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
1.77 +val (p'''', pt'''') = (p, pt);
1.78 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
1.79 +val (p'''', pt'''') = (p, pt);
1.80 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
1.81 +val (p'''', pt'''') = (p, pt);
1.82 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = Apply_Method ["Test", "solve_linear"]*)
1.83 +(*from_pblobj_or_detail': no istate = from_pblobj_or_detail' "Isac" p pt;*)
1.84 +
1.85 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*---------------------------------------------------*)
1.86 +val (p'''', pt'''') = (p, pt);
1.87 +f2str f = "-1 + x = 0"; snd nxt = Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv");
1.88 +val (p, p_) = p(* = ([3, 1], Frm)*);
1.89 +val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.90 +val (env, loc_, curry_arg, res, Safe, true) = scrstate;
1.91 + env2str env = "[\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"]";
1.92 + loc_ = [];
1.93 + curry_arg = NONE;
1.94 + term2str res = "??.empty"; (* scrstate before starting interpretation *)
1.95 +(*term2str (go loc_ sc) = "Script Solve_linear e_e v_v = ...*)
1.96 +
1.97 +val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*-------------------------------------------*)
1.98 +val (p'''', pt'''') = (p, pt);
1.99 +f2str f = "x = 0 + -1 * -1"; snd nxt = Rewrite_Set "Test_simplify";
1.100 +val (p, p_) = p(* = ([3, 1], Res)*);
1.101 +val (srls, (ScrState scrstate, ctxt), Script sc) = from_pblobj_or_detail' "Isac" (p, p_) pt;
1.102 +val (env, loc_, curry_arg, res, Safe, true) = scrstate;
1.103 + env2str env = "[\"\n(e_e, -1 + x = 0)\",\"\n(v_v, x)\"]";
1.104 + loc_ = [R, L, R, L, R, L, R];
1.105 + curry_arg = SOME (str2term "e_e::bool");
1.106 + term2str res = "x = 0 + -1 * -1";(* scrstate after isolate_bdv, before Test_simplify *)
1.107 +term2str (go loc_ sc) = "Rewrite_Set_Inst [(bdv, v_v)] isolate_bdv False";
1.108 +
1.109 +