1.1 --- a/test/Tools/isac/Interpret/li-tool.sml Tue May 19 12:33:35 2020 +0200
1.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Wed May 20 12:52:09 2020 +0200
1.3 @@ -24,8 +24,8 @@
1.4 "----------- fun implicit_take, fun get_first_argument -------------------------";
1.5 "----------- fun implicit_take, fun get_first_argument -------------------------";
1.6 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
1.7 -val (dI',pI',mI') = ("Test",["sqroot-test","univariate","equation","test"],
1.8 - ["Test","squ-equ-test-subpbl1"]);
1.9 +val (dI',pI',mI') = ("Test",["sqroot-test", "univariate", "equation", "test"],
1.10 + ["Test", "squ-equ-test-subpbl1"]);
1.11 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.12 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.13 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
1.14 @@ -60,9 +60,9 @@
1.15 "--------- getTactic, fetchApplicableTactics ------------";
1.16 *)
1.17 reset_states ();
1.18 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.19 - ("Test", ["sqroot-test","univariate","equation","test"],
1.20 - ["Test","squ-equ-test-subpbl1"]))];
1.21 + CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.22 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.23 + ["Test", "squ-equ-test-subpbl1"]))];
1.24 Iterator 1;
1.25 moveActiveRoot 1;
1.26 autoCalculate 1 CompleteCalc;
1.27 @@ -102,9 +102,9 @@
1.28 "----------- fun specific_from_prog ----------------------------";
1.29 "----------- fun specific_from_prog ----------------------------";
1.30 reset_states ();
1.31 - CalcTree [(["equality (x+1=(2::real))", "solveFor x","solutions L"],
1.32 - ("Test", ["sqroot-test","univariate","equation","test"],
1.33 - ["Test","squ-equ-test-subpbl1"]))];
1.34 + CalcTree [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
1.35 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
1.36 + ["Test", "squ-equ-test-subpbl1"]))];
1.37 Iterator 1;
1.38 moveActiveRoot 1;
1.39 autoCalculate 1 CompleteCalc;
1.40 @@ -124,7 +124,7 @@
1.41 (*WAS:
1.42 specific_from_prog pt p;
1.43 ...
1.44 -### Tactic.applicable: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'
1.45 +### Tactic.applicable: not impl. for tac='Subproblem(Test,["LINEAR", "univariate", "equation", "test"])'
1.46 ### Tactic.applicable: not impl. for tac = 'Check_elementwise "Assumptions"'
1.47 *)
1.48
1.49 @@ -150,7 +150,7 @@
1.50 (*WN120611 stopped and took version 1 again for fetchApplicableTactics !
1.51 (Library.distinct op = o flat o (map (Tactic.applicable thy ro erls f))) alltacs
1.52 ...
1.53 -### Tactic.applicable: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])'
1.54 +### Tactic.applicable: not impl. for tac='Subproblem(Test,["LINEAR", "univariate", "equation", "test"])'
1.55 ### Tactic.applicable: not impl. for tac = 'Check_elementwise "Assumptions"'
1.56 *)
1.57
1.58 @@ -169,14 +169,14 @@
1.59 "----------- fun go ----------------------------------------------";
1.60 (*
1.61 > val t = (Thm.term_of o the o (parse thy)) "a+b";
1.62 -val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term
1.63 +val it = Const (#,#) $ Free (#,#) $ Free ("b", "RealDef.real") : term
1.64 > val plus_a = at_location [L] t;
1.65 > val b = at_location [R] t;
1.66 > val plus = at_location [L,L] t;
1.67 > val a = at_location [L,R] t;
1.68
1.69 > val t = (Thm.term_of o the o (parse thy)) "a+b+c";
1.70 -val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c","RealDef.real") : term
1.71 +val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c", "RealDef.real") : term
1.72 > val pl_pl_a_b = at_location [L] t;
1.73 > val c = at_location [R] t;
1.74 > val a = at_location [L,R,L,R] t;
1.75 @@ -188,8 +188,8 @@
1.76 "----------- fun formal_args -------------------------------------";
1.77 (*
1.78 > formal_args scr;
1.79 - [Free ("f_","RealDef.real"),Free ("v_","RealDef.real"),
1.80 - Free ("eqs_","bool List.list")] : term list
1.81 + [Free ("f_", "RealDef.real"),Free ("v_", "RealDef.real"),
1.82 + Free ("eqs_", "bool List.list")] : term list
1.83 *)
1.84 "----------- fun dsc_valT ----------------------------------------";
1.85 "----------- fun dsc_valT ----------------------------------------";
1.86 @@ -210,17 +210,17 @@
1.87 "----------- fun arguments_from_model ---------------------------------------";
1.88 (*
1.89 > val sc = ... Solve_root_equation ...
1.90 -> val mI = ("Program","sqrt-equ-test");
1.91 +> val mI = ("Program", "sqrt-equ-test");
1.92 > val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];
1.93 > val ts = arguments_from_model thy mI itms;
1.94 > map (UnparseC.term_in_thy thy) ts;
1.95 -["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list
1.96 +["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)", "x", "#0"] : string list
1.97 *)
1.98
1.99 "----------- fun init_pstate -----------------------------------------------------------------";
1.100 "----------- fun init_pstate -----------------------------------------------------------------";
1.101 "----------- fun init_pstate -----------------------------------------------------------------";
1.102 -val fmz = ["Traegerlaenge L","Streckenlast q_0","Biegelinie y",
1.103 +val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
1.104 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
1.105 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
1.106 "AbleitungBiegelinie dy"];
1.107 @@ -247,7 +247,7 @@
1.108 "~~~~~ fun init_pstate , args:"; val (srls, thy, itms, metID) = (srls, ThyC.get_theory thy, meth, metID);
1.109 val (Pstate st, ctxt, Prog _) = init_pstate srls ctxt itms metID;
1.110 if pstate2str st =
1.111 - "([\"\n(l, L)\",\"\n(q, q_0)\",\"\n(v, x)\",\"\n(b, dy)\",\"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\",\"\n(vs, [c, c_2, c_3, c_4])\",\"\n(id_abl, y)\"], [], erls_IntegrierenUndK.., NONE, \n??.empty, ORundef, false, true)"
1.112 + "([\"\n(l, L)\", \"\n(q, q_0)\", \"\n(v, x)\", \"\n(b, dy)\", \"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\", \"\n(vs, [c, c_2, c_3, c_4])\", \"\n(id_abl, y)\"], [], erls_IntegrierenUndK.., NONE, \n??.empty, ORundef, false, true)"
1.113 then () else error "init_pstate changed for Biegelinie";
1.114
1.115 (*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Model_Problem*)