1.1 --- a/test/Tools/isac/Specify/specify.sml Mon Apr 19 20:44:18 2021 +0200
1.2 +++ b/test/Tools/isac/Specify/specify.sml Tue Apr 20 16:58:44 2021 +0200
1.3 @@ -22,8 +22,8 @@
1.4 CalcTreeTEST
1.5 [(["fixedValues [r=Arbfix]", "maximum A",
1.6 "valuesFor [a,b]",
1.7 - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.8 - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.9 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
1.10 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
1.11 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
1.12
1.13 "boundVariable a", "boundVariable b", "boundVariable alpha",
1.14 @@ -46,25 +46,25 @@
1.15 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)
1.16 val (pt,p) = Specify.finish_phase (pt,p);
1.17 val pits = get_obj g_pbl pt (fst p);
1.18 - if I_Model.to_string ctxt pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]"
1.19 + if I_Model.to_string ctxt pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(rs_, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]"
1.20 then () else error "completetest.sml: new behav. in Specify.finish_phase 3";
1.21 writeln (I_Model.to_string ctxt pits);
1.22 (*[
1.23 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
1.24 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
1.25 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
1.26 -(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
1.27 -2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
1.28 +(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up>
1.29 +2 = r \<up> 2] ,(relations, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]*)
1.30 val mits = get_obj g_met pt (fst p);
1.31 - if I_Model.to_string ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]"
1.32 + if I_Model.to_string ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(rs_, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]"
1.33 then () else error "completetest.sml: new behav. in Specify.finish_phase 3";
1.34 writeln (I_Model.to_string ctxt mits);
1.35 (*[
1.36 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
1.37 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
1.38 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
1.39 -(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
1.40 -2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
1.41 +(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up>
1.42 +2 = r \<up> 2] ,(relations, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])),
1.43 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
1.44 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
1.45 0 <= x & x <= 2 * r}])),
1.46 @@ -79,8 +79,8 @@
1.47 CalcTreeTEST
1.48 [(["fixedValues [r=Arbfix]", "maximum A",
1.49 "valuesFor [a,b]",
1.50 - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.51 - "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
1.52 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
1.53 + "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
1.54 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
1.55
1.56 "boundVariable a", "boundVariable b", "boundVariable alpha",
1.57 @@ -104,7 +104,7 @@
1.58 (1, ["1", "2", "3"], #Given,fixedValues, ["[r = Arbfix]"]),
1.59 (2, ["1", "2", "3"], #Find,maximum, ["A"]),
1.60 (3, ["1", "2", "3"], #Find,valuesFor, ["[a]", "[b]"]),
1.61 -(4, ["1", "2"], #Relate,relations, ["[A = a * b]", "[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"]),
1.62 +(4, ["1", "2"], #Relate,relations, ["[A = a * b]", "[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]"]),
1.63 (5, ["3"], #Relate,relations, ["[A = a * b]", "[a / 2 = r * sin alpha]", "[b / 2 = r * cos alpha]"]),
1.64 (6, ["1"], #undef,boundVariable, ["a"]),
1.65 (7, ["2"], #undef,boundVariable, ["b"]),
1.66 @@ -118,8 +118,8 @@
1.67 (1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])),
1.68 (2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])),
1.69 (3 ,[1,2,3] ,true,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
1.70 -(4 ,[1,2] ,true,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
1.71 -2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
1.72 +(4 ,[1,2] ,true,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up>
1.73 +2 = r \<up> 2] ,(rs_, [[A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]*)
1.74 val mits = get_obj g_met pt (fst p);
1.75 val mits = I_Model.complete oris pits []
1.76 ((#ppc o MethodC.from_store) ["DiffApp", "max_by_calculus"]);
1.77 @@ -128,14 +128,14 @@
1.78 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
1.79 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
1.80 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
1.81 -(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
1.82 -2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
1.83 +(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up>
1.84 +2 = r \<up> 2] ,(rs_, [[A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])),
1.85 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
1.86 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
1.87 0 <= x & x <= 2 * r}])),
1.88 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
1.89 if I_Model.to_string ctxt mits
1.90 - = "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[r = Arbfix]])), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A ,(m_m, [A])), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor valuesFor [a, b] ,(v_s, [[a, b]])), \n(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(r_s, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])), \n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_v, [a])), \n(9 ,[1, 2] ,true ,#undef ,Cor interval {x. 0 \<le> x \<and> x \<le> 2 * r} ,(i_tv, [{x. 0 \<le> x \<and> x \<le> 2 * r}])), \n(11 ,[1, 2, 3] ,true ,#undef ,Cor errorBound (eps = 0) ,(e_rr, [eps = 0]))]"
1.91 + = "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(f_ix, [[r = Arbfix]])), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A ,(m_m, [A])), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor valuesFor [a, b] ,(v_s, [[a, b]])), \n(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(r_s, [[A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])), \n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_v, [a])), \n(9 ,[1, 2] ,true ,#undef ,Cor interval {x. 0 \<le> x \<and> x \<le> 2 * r} ,(i_tv, [{x. 0 \<le> x \<and> x \<le> 2 * r}])), \n(11 ,[1, 2, 3] ,true ,#undef ,Cor errorBound (eps = 0) ,(e_rr, [eps = 0]))]"
1.92 then () else error "completetest.sml: new behav. in I_Model.complete 1";
1.93
1.94 open O_Model;
1.95 @@ -335,7 +335,7 @@
1.96 "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
1.97 "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
1.98 "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]";
1.99 -(* ERROR -------^^^^^^ CORRECTED TO #Given *)
1.100 +(* ERROR ------- \<up> \<up> CORRECTED TO #Given *)
1.101 (*+*)if I_Model.to_string @{context} meth = "[\n" ^
1.102 "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
1.103 "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
1.104 @@ -572,7 +572,7 @@
1.105 (*[1], Met*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*\<rightarrow>Add_Given "Biegelinie y"*)
1.106 (*/------------------- step into me\<rightarrow>Add_Given "Biegelinie y" ||||||||||||||||||||||||||||||\*)
1.107 (*+*)val Specify_Method ["Biegelinien", "ausBelastung"] = nxt;
1.108 -(*+*)(* by ^^^^^^^^^^^^ "id_fun" and "id_abl" must be requested: PUT THEM INTO O_Model*)
1.109 +(*+*)(* by \<up> \<up> \<up> \<up> "id_fun" and "id_abl" must be requested: PUT THEM INTO O_Model*)
1.110
1.111 "~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
1.112
1.113 @@ -637,7 +637,7 @@
1.114 "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
1.115 "(4, [\"1\"], #Given, Biegelinie, [\"y\"]), \n" ^ (*.. value from O_Model of root-problem*)
1.116 "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]" (*.. value from O_Model of root-problem*)
1.117 -(* ^^^----- aim at dropping this field *)
1.118 +(* \<up> ----- aim at dropping this field *)
1.119 (*+*)then () else error "[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";
1.120 (*\------------------- check for entry to O_Model.complete_for -----------------------------/*)
1.121
1.122 @@ -674,7 +674,7 @@
1.123 "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
1.124 "(4, [\"1\"], #Given, Biegelinie, [\"y\"]), \n" ^
1.125 "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"
1.126 -(* ^^^----- aim at dropping this field *)
1.127 +(* \<up> ----- aim at dropping this field *)
1.128 (*+*)then () else error "[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";
1.129 (*\------------------- check within O_Model.complete_for -------------------------------------------/*)
1.130
1.131 @@ -698,7 +698,7 @@
1.132 "~~~ from Step_Specify.by_tactic \<longrightarrow>Step.by_tactic \<longrightarrow>fun me , return:"; val ("ok", (_, _, (pt, p))) =
1.133 ("ok", ([], [], (pt, pos)));
1.134 (* val ("helpless", ([(xxxxx, _, _)], _, _)) = (*case*)*)
1.135 - (* SHOULD BE ^^^^^^^^^^^^^^^^^^^^^^^^^^^ Add_Given "Biegelinie y" | Add_Given "AbleitungBiegelinie dy"*)
1.136 + (* SHOULD BE \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> Add_Given "Biegelinie y" | Add_Given "AbleitungBiegelinie dy"*)
1.137
1.138 val ("ok", ([( Add_Given "Biegelinie y", _, _)], [], _)) =
1.139 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
1.140 @@ -789,7 +789,7 @@
1.141 "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
1.142 "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
1.143 "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
1.144 - "(4, [\"1\"], #Given, Biegelinie, [\"y\"]), \n" ^ (*-------------------^^^^^^^^^^^^^*)
1.145 + "(4, [\"1\"], #Given, Biegelinie, [\"y\"]), \n" ^ (*------------------- \<up> \<up> \<up> \<up> ^*)
1.146 "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"
1.147 (*+*)then () else error "[Biegelinien, ausBelastung] O_Model CHANGED for entry";
1.148 (*+*)if I_Model.to_string ctxt met = "[\n" ^
1.149 @@ -843,18 +843,18 @@
1.150 "(#Given, (FunktionsVariable, v_v))\", \"" ^
1.151 "(#Find, (Funktionen, funs'''))\"]"
1.152 (*+*)then () else error "seek_orits Model_Pattern of Subproblem CHANGED";
1.153 -(* root-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv -------------------------------------^^^*)
1.154 +(* root-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv ------------------------------------- \<up> *)
1.155 (*+*)if (Problem.from_store ["Biegelinien"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^
1.156 "(#Given, (Traegerlaenge, l_l))\", \"" ^
1.157 "(#Given, (Streckenlast, q_q))\", \"" ^
1.158 - "(#Find, (Biegelinie, b_b))\", \"" ^ (*-------------------------------------^^^*)
1.159 + "(#Find, (Biegelinie, b_b))\", \"" ^ (*------------------------------------- \<up> *)
1.160 "(#Relate, (Randbedingungen, r_b))\"]"
1.161 (*+*)then () else error "seek_orits Model_Pattern root-problem CHANGED";
1.162 (* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
1.163 (*+*)if (MethodC.from_store ["Biegelinien", "ausBelastung"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^
1.164 "(#Given, (Streckenlast, q__q))\", \"" ^
1.165 "(#Given, (FunktionsVariable, v_v))\", \"" ^
1.166 - "(#Given, (Biegelinie, id_fun))\", \"" ^ (*---------------------------------^^^*)
1.167 + "(#Given, (Biegelinie, id_fun))\", \"" ^ (*--------------------------------- \<up> *)
1.168 "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^
1.169 "(#Find, (Funktionen, fun_s))\"]"
1.170 (*+*)then () else error "seek_orits Model_Pattern CHANGED";