1.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Mon Apr 19 20:44:18 2021 +0200
1.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Tue Apr 20 16:58:44 2021 +0200
1.3 @@ -22,7 +22,7 @@
1.4 val p = e_pos'; val c = [];
1.5 val (p,_,f,nxt,_,pt) =
1.6 CalcTreeTEST
1.7 - [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
1.8 + [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
1.9 ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
1.10 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
1.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.12 @@ -53,14 +53,14 @@
1.13 val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
1.14 (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
1.15 | _ => error "solve Apply_Method: uncovered case init_pstate";
1.16 -(*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)";
1.17 +(*+*)pstate2str (the_pstate is) = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [], empty, NONE, \n??.empty, ORundef, false, true)";
1.18 val ini = LItool.implicit_take sc env;
1.19 val p = lev_dn p;
1.20
1.21 val NONE = (*case*) ini (*of*);
1.22 val Next_Step (is', ctxt', m') =
1.23 LI.find_next_step sc (pt, (p, Res)) is ctxt;
1.24 -(*+*)pstate2str (the_pstate is') = "([\"\n(f_f, x ^^^ 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], empty, NONE, \nIntegral x ^^^ 2 + 1 D x, ORundef, false, false)";
1.25 +(*+*)pstate2str (the_pstate is') = "([\"\n(f_f, x \<up> 2 + 1)\",\"\n(v_v, x)\"], [R,L,R], empty, NONE, \nIntegral x \<up> 2 + 1 D x, ORundef, false, false)";
1.26 val Safe_Step (_, _, Take' _) = (*case*)
1.27 locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' (*of*);
1.28 "~~~~~ fun locate_input_tactic , args:"; val ((Prog prog), cstate, istate, ctxt, tac)