test/Tools/isac/Interpret/lucas-interpreter.sml
changeset 60242 73ee61385493
parent 60154 2ab0d1523731
child 60309 70a1d102660d
child 60324 5c7128feb370
     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)