walther@59763
|
1 |
(* Title: "Specify/specify.sml"
|
walther@59763
|
2 |
Author: Walther Neuper
|
walther@59763
|
3 |
(c) due to copyright terms
|
walther@59763
|
4 |
*)
|
walther@59763
|
5 |
|
walther@59763
|
6 |
"-----------------------------------------------------------------------------------------------";
|
walther@59763
|
7 |
"table of contents -----------------------------------------------------------------------------";
|
walther@59763
|
8 |
"-----------------------------------------------------------------------------------------------";
|
walther@59763
|
9 |
"-----------------------------------------------------------------------------------------------";
|
walther@59996
|
10 |
"----------- maximum-example: Specify.finish_phase ---------------------------------------------";
|
walther@59988
|
11 |
"----------- maximum-example: I_Model.complete -------------------------------------------------";
|
Walther@60654
|
12 |
"----------- revise Specify.do_all -------------------------------------------------------------";
|
walther@60014
|
13 |
"----------- specify-phase: low level functions ------------------------------------------------";
|
walther@59763
|
14 |
"-----------------------------------------------------------------------------------------------";
|
walther@59763
|
15 |
"-----------------------------------------------------------------------------------------------";
|
walther@59763
|
16 |
"-----------------------------------------------------------------------------------------------";
|
Walther@60736
|
17 |
open Pos;
|
Walther@60736
|
18 |
open Ctree;
|
Walther@60736
|
19 |
open Test_Code;
|
Walther@60736
|
20 |
open Tactic;
|
Walther@60736
|
21 |
open Specify;
|
Walther@60736
|
22 |
open Step;
|
Walther@60736
|
23 |
|
Walther@60736
|
24 |
open O_Model;
|
Walther@60736
|
25 |
open I_Model;
|
Walther@60736
|
26 |
open P_Model;
|
Walther@60736
|
27 |
open Specify_Step;
|
Walther@60736
|
28 |
open Test_Code;
|
walther@59763
|
29 |
|
Walther@60459
|
30 |
(**** maximum-example: Specify.finish_phase ############################################# ****)
|
walther@59996
|
31 |
"----------- maximum-example: Specify.finish_phase ---------------------------------------------";
|
walther@59996
|
32 |
"----------- maximum-example: Specify.finish_phase ---------------------------------------------";
|
walther@59800
|
33 |
(*//-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --\\* )
|
walther@59800
|
34 |
val (p,_,f,nxt,_,pt) =
|
Walther@60571
|
35 |
Test_Code.init_calc @{context}
|
walther@59997
|
36 |
[(["fixedValues [r=Arbfix]", "maximum A",
|
walther@59800
|
37 |
"valuesFor [a,b]",
|
walther@60242
|
38 |
"relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
|
walther@60242
|
39 |
"relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
|
walther@59800
|
40 |
"relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
|
walther@59800
|
41 |
|
walther@59997
|
42 |
"boundVariable a", "boundVariable b", "boundVariable alpha",
|
walther@59800
|
43 |
"interval {x::real. 0 <= x & x <= 2*r}",
|
walther@59800
|
44 |
"interval {x::real. 0 <= x & x <= 2*r}",
|
walther@59800
|
45 |
"interval {x::real. 0 <= x & x <= pi}",
|
walther@59800
|
46 |
"errorBound (eps=(0::real))"],
|
Walther@60458
|
47 |
("Diff_App",["maximum_of", "function"],["Diff_App", "max_by_calculus"])
|
walther@59800
|
48 |
)];
|
walther@59800
|
49 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@59800
|
50 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@59800
|
51 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
walther@59800
|
52 |
(*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)
|
walther@59800
|
53 |
val pits = get_obj g_pbl pt (fst p);
|
walther@59942
|
54 |
writeln (I_Model.to_string ctxt pits);
|
walther@59800
|
55 |
(*[
|
walther@59800
|
56 |
(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
|
walther@59800
|
57 |
(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),
|
walther@59800
|
58 |
(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
|
walther@59800
|
59 |
(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)
|
walther@59990
|
60 |
val (pt,p) = Specify.finish_phase (pt,p);
|
walther@59800
|
61 |
val pits = get_obj g_pbl pt (fst p);
|
walther@60242
|
62 |
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]]))]"
|
walther@59990
|
63 |
then () else error "completetest.sml: new behav. in Specify.finish_phase 3";
|
walther@59942
|
64 |
writeln (I_Model.to_string ctxt pits);
|
walther@59800
|
65 |
(*[
|
walther@59800
|
66 |
(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
|
walther@59800
|
67 |
(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
|
walther@59800
|
68 |
(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
|
walther@60242
|
69 |
(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up>
|
walther@60242
|
70 |
2 = r \<up> 2] ,(relations, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]*)
|
walther@59800
|
71 |
val mits = get_obj g_met pt (fst p);
|
walther@60242
|
72 |
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]))]"
|
walther@59990
|
73 |
then () else error "completetest.sml: new behav. in Specify.finish_phase 3";
|
walther@59942
|
74 |
writeln (I_Model.to_string ctxt mits);
|
walther@59800
|
75 |
(*[
|
walther@59800
|
76 |
(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
|
walther@59800
|
77 |
(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
|
walther@59800
|
78 |
(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
|
walther@60242
|
79 |
(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up>
|
walther@60242
|
80 |
2 = r \<up> 2] ,(relations, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])),
|
walther@59800
|
81 |
(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
|
walther@59800
|
82 |
(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
|
walther@59800
|
83 |
0 <= x & x <= 2 * r}])),
|
walther@59800
|
84 |
(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
|
walther@59800
|
85 |
( *\\-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --//*)
|
walther@59800
|
86 |
|
Walther@60459
|
87 |
(**** maximum-example: I_Model.complete ################################################## ****)
|
walther@59988
|
88 |
"----------- maximum-example: I_Model.complete -------------------------------------------------";
|
walther@59988
|
89 |
"----------- maximum-example: I_Model.complete -------------------------------------------------";
|
Walther@60459
|
90 |
val c = [];
|
Walther@60571
|
91 |
val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context}
|
Walther@60459
|
92 |
[(["fixedValues [r=Arbfix]", "maximum A",
|
walther@59800
|
93 |
"valuesFor [a,b]",
|
walther@60242
|
94 |
"relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
|
walther@60242
|
95 |
"relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
|
walther@59800
|
96 |
"relations [A=a*b, a/2=r*sin alpha, b/2=r*cos (alpha::real)]",
|
walther@59997
|
97 |
"boundVariable a", "boundVariable b", "boundVariable alpha",
|
walther@59800
|
98 |
"interval {x::real. 0 <= x & x <= 2*r}",
|
walther@59800
|
99 |
"interval {x::real. 0 <= x & x <= 2*r}",
|
walther@59800
|
100 |
"interval {x::real. 0 <= x & x <= pi}",
|
walther@59800
|
101 |
"errorBound (eps=(0::real))"],
|
Walther@60459
|
102 |
("Diff_App", ["maximum_of", "function"], ["Diff_App", "max_by_calculus"]))];
|
Walther@60459
|
103 |
(*** stepwise Specification: Problem model================================================= ***)
|
Walther@60729
|
104 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "fixedValues [r = Arbfix]" = nxt
|
Walther@60729
|
105 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "maximum A" = nxt
|
Walther@60729
|
106 |
(*/---broken elementwise input to lists---\* )
|
Walther@60729
|
107 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "valuesFor [a]" = nxt
|
Walther@60729
|
108 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "valuesFor [b]" = nxt
|
Walther@60729
|
109 |
( *\---broken elementwise input to lists---/*)
|
Walther@60729
|
110 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "valuesFor [a, b]" = nxt
|
Walther@60729
|
111 |
(*/---broken elementwise input to lists---\* )
|
Walther@60729
|
112 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "relations [A = a * b]" = nxt
|
Walther@60729
|
113 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "relations [(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]" = nxt
|
Walther@60729
|
114 |
( *\---broken elementwise input to lists---/*)
|
Walther@60729
|
115 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]" = nxt
|
Walther@60729
|
116 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Diff_App" = nxt
|
Walther@60459
|
117 |
|
Walther@60729
|
118 |
(*/------------------- directly to Problem model is complete --------------------------------\*)
|
Walther@60676
|
119 |
val thy = @{theory "Diff_App"};
|
Walther@60676
|
120 |
val ctxt = Proof_Context.init_global thy;
|
Walther@60459
|
121 |
val (o_model, _, _) = get_obj g_origin pt (fst p);
|
Walther@60655
|
122 |
writeln (O_Model.to_string @{context} o_model);
|
Walther@60655
|
123 |
if O_Model.to_string @{context} o_model = "[\n" ^
|
Walther@60459
|
124 |
"(1, [\"1\", \"2\", \"3\"], #Given, fixedValues, [\"[r = Arbfix]\"]), \n" ^
|
Walther@60459
|
125 |
"(2, [\"1\", \"2\", \"3\"], #Find, maximum, [\"A\"]), \n" ^
|
Walther@60459
|
126 |
"(3, [\"1\", \"2\", \"3\"], #Find, valuesFor, [\"[a]\", \"[b]\"]), \n" ^
|
Walther@60459
|
127 |
"(4, [\"1\", \"2\"], #Relate, relations, [\"[A = a * b]\", \"[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]\"]), \n" ^
|
Walther@60459
|
128 |
"(5, [\"3\"], #Relate, relations, [\"[A = a * b]\", \"[a / 2 = r * sin alpha]\", \"[b / 2 = r * cos alpha]\"]), \n" ^
|
Walther@60459
|
129 |
"(6, [\"1\"], #undef, boundVariable, [\"a\"]), \n" ^
|
Walther@60459
|
130 |
"(7, [\"2\"], #undef, boundVariable, [\"b\"]), \n" ^
|
Walther@60459
|
131 |
"(8, [\"3\"], #undef, boundVariable, [\"alpha\"]), \n" ^
|
Walther@60459
|
132 |
"(9, [\"1\", \"2\"], #undef, interval, [\"{x. 0 \<le> x \<and> x \<le> 2 * r}\"]), \n" ^
|
Walther@60459
|
133 |
"(10, [\"3\"], #undef, interval, [\"{x. 0 \<le> x \<and> x \<le> pi}\"]), \n" ^
|
Walther@60459
|
134 |
"(11, [\"1\", \"2\", \"3\"], #undef, errorBound, [\"eps = 0\"])]"
|
Walther@60459
|
135 |
then () else error "maximum-example: O_Model.to_string o_model CHANGED";
|
Walther@60459
|
136 |
|
Walther@60459
|
137 |
val problem_i_model = get_obj g_pbl pt (fst p); (* is already filled *)
|
Walther@60459
|
138 |
writeln (I_Model.to_string ctxt problem_i_model);
|
Walther@60459
|
139 |
if I_Model.to_string ctxt problem_i_model = "[\n" ^
|
Walther@60739
|
140 |
"(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] , pen2str), \n" ^
|
Walther@60739
|
141 |
"(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A , pen2str), \n" ^
|
Walther@60739
|
142 |
"(3 ,[1, 2, 3] ,true ,#Find ,Cor valuesFor [a, b] , pen2str), \n" ^
|
Walther@60739
|
143 |
"(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str)]"
|
Walther@60459
|
144 |
then () else error "maximum-example: I_Model.to_string problem_i_model CHANGED";
|
Walther@60459
|
145 |
|
Walther@60459
|
146 |
val method_i_model= get_obj g_met pt (fst p); (* is still empty *)
|
Walther@60459
|
147 |
if method_i_model = []then () else error "is still empty CHANGED";
|
Walther@60459
|
148 |
val method_i_model = I_Model.complete o_model problem_i_model
|
Walther@60586
|
149 |
[] ((#model o MethodC.from_store ctxt) ["Diff_App", "max_by_calculus"]);
|
Walther@60459
|
150 |
if I_Model.to_string ctxt method_i_model = "[\n" ^
|
Walther@60739
|
151 |
"(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] , pen2str), \n" ^
|
Walther@60739
|
152 |
"(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A , pen2str), \n" ^
|
Walther@60739
|
153 |
"(3 ,[1, 2, 3] ,true ,#Find ,Cor valuesFor [a, b] , pen2str), \n" ^
|
Walther@60739
|
154 |
"(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str), \n" ^
|
Walther@60739
|
155 |
"(6 ,[1] ,true ,#undef ,Cor boundVariable a , pen2str), \n" ^
|
Walther@60739
|
156 |
"(9 ,[1, 2] ,true ,#undef ,Cor interval {x. 0 \<le> x \<and> x \<le> 2 * r} , pen2str), \n" ^
|
Walther@60739
|
157 |
"(11 ,[1, 2, 3] ,true ,#undef ,Cor errorBound (eps = 0) , pen2str)]"
|
walther@59988
|
158 |
then () else error "completetest.sml: new behav. in I_Model.complete 1";
|
Walther@60729
|
159 |
(*\------------------- directly to Problem model is complete --------------------------------/*)
|
walther@59800
|
160 |
|
Walther@60729
|
161 |
(*/------------------- MethodC model has a copy of Problem ----------------------------------\*)
|
Walther@60729
|
162 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["maximum_of", "function"] = nxt
|
Walther@60729
|
163 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["Diff_App", "max_by_calculus"] = nxt
|
Walther@60729
|
164 |
(*\------------------- MethodC model has a copy of Problem ----------------------------------/*)
|
Walther@60459
|
165 |
|
Walther@60729
|
166 |
(*/------------------- stepwise Specification: MethodC model --------------------------------\*)
|
Walther@60729
|
167 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "boundVariable a" = nxt
|
Walther@60729
|
168 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "interval {x. 0 \<le> x \<and> x \<le> 2 * r}" = nxt
|
Walther@60729
|
169 |
val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "errorBound (eps = 0)" = nxt;
|
Walther@60459
|
170 |
(*** MethodC model is complete ============================================================ ***)
|
Walther@60729
|
171 |
(** )val (p,_,f,nxt,_,pt) = me nxt p c pt; (*exception TERM raised (line 359 of "term.ML"):
|
Walther@60459
|
172 |
fastype_of: Bound
|
Walther@60729
|
173 |
B.0 *)( **)
|
Walther@60729
|
174 |
(*\------------------ Specification of Problem and MethodC model is complete, Solution starts/*)
|
Walther@60459
|
175 |
|
Walther@60459
|
176 |
|
Walther@60654
|
177 |
"----------- revise Specify.do_all -------------------------------------------------------------";
|
Walther@60654
|
178 |
"----------- revise Specify.do_all -------------------------------------------------------------";
|
Walther@60654
|
179 |
"----------- revise Specify.do_all -------------------------------------------------------------";
|
Walther@60654
|
180 |
(* from Minisubplb/100-init-rootpbl.sml:
|
Walther@60654
|
181 |
val (_(*example text*),
|
Walther@60654
|
182 |
(model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
|
Walther@60654
|
183 |
"Extremum (A = 2 * u * v - u \<up> 2)" ::
|
Walther@60654
|
184 |
"SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
|
Walther@60654
|
185 |
"SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
|
Walther@60654
|
186 |
"SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
|
Walther@60654
|
187 |
"FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
|
Walther@60654
|
188 |
"Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
|
Walther@60654
|
189 |
"ErrorBound (\<epsilon> = (0::real))" :: []),
|
Walther@60654
|
190 |
refs as ("Diff_App",
|
Walther@60654
|
191 |
["univariate_calculus", "Optimisation"],
|
Walther@60654
|
192 |
["Optimisation", "by_univariate_calculus"])))
|
Walther@60654
|
193 |
= Store.get (Know_Store.get_expls @ {theory Know_Store}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
|
Walther@60654
|
194 |
*)
|
Walther@60654
|
195 |
val model = ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
|
Walther@60654
|
196 |
"Extremum (A = 2 * u * v - u \<up> 2)" ::
|
Walther@60654
|
197 |
"SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
|
Walther@60654
|
198 |
"SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
|
Walther@60654
|
199 |
"SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
|
Walther@60654
|
200 |
"FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
|
Walther@60654
|
201 |
"Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
|
Walther@60654
|
202 |
"ErrorBound (\<epsilon> = (0::real))" :: [])
|
Walther@60654
|
203 |
val refs = ("Diff_App",
|
Walther@60654
|
204 |
["univariate_calculus", "Optimisation"],
|
Walther@60654
|
205 |
["Optimisation", "by_univariate_calculus"])
|
Walther@60654
|
206 |
|
Walther@60654
|
207 |
val (p,_,f,nxt,_,pt) =
|
Walther@60654
|
208 |
Test_Code.init_calc @{context} [(model, refs)];
|
Walther@60654
|
209 |
"~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))])
|
Walther@60654
|
210 |
= (@{context}, [(model, refs)]);
|
Walther@60654
|
211 |
|
Walther@60654
|
212 |
Specify.do_all (pt, p);
|
Walther@60654
|
213 |
(*//------------------ step into do_all ----------------------------------------------------\\*)
|
Walther@60654
|
214 |
"~~~~~ fun do_all , args:"; val (pt, (*old* )pos as( *old*) (p, _)) = (pt, p);
|
Walther@60654
|
215 |
(*new*)val (f_model, dI, pI, mI, ctxt) = case Ctree.get_obj I pt p of
|
Walther@60654
|
216 |
(*new*) Ctree.PblObj {origin = (f_model, (dI, pI, mI), _), ctxt, ...}
|
Walther@60654
|
217 |
(*new*) => (f_model, dI, pI, mI, ctxt)
|
Walther@60654
|
218 |
(*new*)| _ => raise ERROR "do_all: uncovered case get_obj"
|
Walther@60654
|
219 |
(*new*)val mod_pat = MethodC.from_store ctxt mI |> #model : Model_Pattern.T
|
Walther@60654
|
220 |
|
Walther@60654
|
221 |
(*new*)val i_model = map
|
Walther@60654
|
222 |
(I_Model.complete' mod_pat) f_model (*no parse, take terms*);
|
Walther@60654
|
223 |
"~~~~~ fun complete' , args:"; val (mod_pat, (i, v, f, d, ts)) = (mod_pat, nth 1 f_model);
|
Walther@60654
|
224 |
val SOME xxx =
|
Walther@60654
|
225 |
\<^try>\<open> (i, v, true, f, I_Model.Cor ((d, ts),
|
Walther@60654
|
226 |
((find_first ((fn descriptor => (fn (_, (d, _)) => descriptor = d)) d)) mod_pat |> the |> snd |> snd, ts)
|
Walther@60654
|
227 |
))\<close>
|
Walther@60739
|
228 |
val "(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str)" =
|
Walther@60654
|
229 |
I_Model.single_to_string @{context} xxx;
|
Walther@60654
|
230 |
|
Walther@60654
|
231 |
"~~~~~ fun complete' , args:"; val (mod_pat, (i, v, f, d, ts)) = (mod_pat, nth 7 f_model);
|
Walther@60654
|
232 |
val SOME xxx =
|
Walther@60654
|
233 |
\<^try>\<open> (i, v, true, f, I_Model.Cor ((d, ts),
|
Walther@60654
|
234 |
((find_first ((fn descriptor => (fn (_, (d, _)) => descriptor = d)) d)) mod_pat |> the |> snd |> snd, ts)
|
Walther@60654
|
235 |
))\<close>
|
Walther@60739
|
236 |
val "(7 ,[1] ,true ,#undef ,Cor FunctionVariable a , pen2str)"
|
Walther@60739
|
237 |
= I_Model.single_to_string @{context} xxx;
|
Walther@60654
|
238 |
(*-------------------- stop step into do_all -------------------------------------------------*)
|
Walther@60654
|
239 |
(*/------------------- check result of I_Model.complete' ------------------------------------\*)
|
Walther@60655
|
240 |
if Model_Pattern.to_string @{context} mod_pat = "[\"" ^
|
Walther@60654
|
241 |
"(#Given, (Constants, fixes))\", \"" ^
|
Walther@60654
|
242 |
"(#Given, (Maximum, maxx))\", \"" ^
|
Walther@60654
|
243 |
"(#Given, (Extremum, extr))\", \"" ^
|
Walther@60654
|
244 |
"(#Given, (SideConditions, sideconds))\", \"" ^
|
Walther@60654
|
245 |
"(#Given, (FunctionVariable, funvar))\", \"" ^
|
Walther@60654
|
246 |
"(#Given, (Input_Descript.Domain, doma))\", \"" ^
|
Walther@60654
|
247 |
"(#Given, (ErrorBound, err))\", \"" ^
|
Walther@60654
|
248 |
"(#Find, (AdditionalValues, vals))\"]" then () else error "mod_pat CHANGED";
|
Walther@60654
|
249 |
if I_Model.to_string @{context} i_model = "[\n" ^
|
Walther@60739
|
250 |
"(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n" ^
|
Walther@60739
|
251 |
"(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n" ^
|
Walther@60739
|
252 |
"(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n" ^
|
Walther@60739
|
253 |
"(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n" ^
|
Walther@60739
|
254 |
"(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n" ^
|
Walther@60739
|
255 |
"(6 ,[3] ,true ,#Relate ,Cor SideConditions [u / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>] , pen2str), \n" ^
|
Walther@60739
|
256 |
"(7 ,[1] ,true ,#undef ,Cor FunctionVariable a , pen2str), \n" ^
|
Walther@60739
|
257 |
"(8 ,[2] ,true ,#undef ,Cor FunctionVariable b , pen2str), \n" ^
|
Walther@60739
|
258 |
"(9 ,[3] ,true ,#undef ,Cor FunctionVariable \<alpha> , pen2str), \n" ^
|
Walther@60739
|
259 |
"(10 ,[1, 2] ,true ,#undef ,Cor Input_Descript.Domain {0<..<r} , pen2str), \n" ^
|
Walther@60739
|
260 |
"(11 ,[3] ,true ,#undef ,Cor Input_Descript.Domain {0<..<\<pi> / 2} , pen2str), \n" ^
|
Walther@60739
|
261 |
"(12 ,[1, 2, 3] ,true ,#undef ,Cor ErrorBound (\<epsilon> = 0) , pen2str)]"
|
Walther@60654
|
262 |
then () else error "i_model CHANGED";
|
Walther@60654
|
263 |
(*\------------------- check result of I_Model.complete' ------------------------------------/*)
|
Walther@60654
|
264 |
(*\\------------------ step into do_all ----------------------------------------------------//*)
|
Walther@60654
|
265 |
|
Walther@60654
|
266 |
(*-------------------- continuing do_all -----------------------------------------------------*)
|
Walther@60654
|
267 |
(*new*)
|
Walther@60654
|
268 |
O_Model.values' ctxt f_model;
|
Walther@60654
|
269 |
"~~~~~ fun values' , args:"; val (ctxt, oris) = (ctxt, f_model);
|
Walther@60654
|
270 |
(*//------------------ inserted hidden code ------------------------------------------------\\*)
|
Walther@60654
|
271 |
fun ori2fmz_vals (_, _, _, dsc, ts) =
|
Walther@60675
|
272 |
case \<^try>\<open>(((UnparseC.term ctxt) o Input_Descript.join') (dsc, ts), last_elem ts)\<close> of
|
Walther@60654
|
273 |
SOME x => x
|
Walther@60675
|
274 |
| NONE => raise ERROR ("O_Model.values' called with " ^ UnparseC.terms ctxt ts);
|
Walther@60654
|
275 |
(*\\------------------ inserted hidden code ------------------------------------------------//*)
|
Walther@60654
|
276 |
(split_list o (map
|
Walther@60654
|
277 |
ori2fmz_vals)) oris;
|
Walther@60654
|
278 |
"~~~~~ fun ori2fmz_vals , args:"; val (_, _, _, dsc, ts) = (nth 1 oris);
|
Walther@60654
|
279 |
val xxx = Input_Descript.join' (dsc, ts)
|
Walther@60654
|
280 |
|
Walther@60654
|
281 |
(*-------------------- continuing do_all -----------------------------------------------------*)
|
Walther@60654
|
282 |
(*new*)val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI), i_model, i_model, ctxt);
|
Walther@60654
|
283 |
|
Walther@60654
|
284 |
|
Walther@60654
|
285 |
|
Walther@60459
|
286 |
(**** specify-phase: low level functions ################################################# ****)
|
Walther@60459
|
287 |
"----------- specify-phase: low level functions -----------------------------------------";
|
Walther@60459
|
288 |
"----------- specify-phase: low level functions -----------------------------------------";
|
Walther@60736
|
289 |
open Pos;
|
Walther@60736
|
290 |
open Ctree;
|
Walther@60736
|
291 |
open Test_Code;
|
Walther@60736
|
292 |
open Tactic;
|
Walther@60736
|
293 |
open Specify;
|
Walther@60736
|
294 |
open Step;
|
Walther@60736
|
295 |
|
walther@60010
|
296 |
open O_Model;
|
walther@60010
|
297 |
open I_Model;
|
Walther@60736
|
298 |
open P_Model;
|
walther@60010
|
299 |
open Specify_Step;
|
Walther@60736
|
300 |
|
walther@60010
|
301 |
val formalise = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
|
Walther@60736
|
302 |
"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
|
Walther@60736
|
303 |
(*
|
Walther@60736
|
304 |
Now follow items for ALL SubProblems,
|
Walther@60736
|
305 |
since ROOT MethodC must provide values for "actuals" of ALL SubProblems.
|
Walther@60736
|
306 |
See Biegelinie.thy subsection \<open>Survey on Methods\<close>.
|
Walther@60736
|
307 |
*)
|
Walther@60736
|
308 |
(*
|
Walther@60736
|
309 |
Items for MethodC "IntegrierenUndKonstanteBestimmen2"
|
Walther@60736
|
310 |
*)
|
Walther@60736
|
311 |
"FunktionsVariable x",
|
Walther@60736
|
312 |
(*"Biegelinie y", ..already input for Problem above*)
|
Walther@60736
|
313 |
"AbleitungBiegelinie dy",
|
Walther@60736
|
314 |
"Biegemoment M_b",
|
Walther@60736
|
315 |
"Querkraft Q",
|
Walther@60736
|
316 |
(*
|
Walther@60736
|
317 |
Item for Problem "LINEAR/system", which by [''no_met''] involves refinement
|
Walther@60736
|
318 |
*)
|
Walther@60736
|
319 |
"GleichungsVariablen [c, c_2, c_3, c_4]"
|
Walther@60736
|
320 |
];
|
Walther@60736
|
321 |
(*
|
Walther@60736
|
322 |
Note: the above sequence of items follows the sequence of formal arguments (and of model items)
|
Walther@60736
|
323 |
of MethodC "IntegrierenUndKonstanteBestimmen2"
|
Walther@60736
|
324 |
*)
|
walther@60010
|
325 |
val references = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
|
walther@60010
|
326 |
val p = e_pos'; val c = [];
|
Walther@60571
|
327 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(formalise, references)]; (*nxt = Model_Problem*)
|
walther@59800
|
328 |
|
Walther@60571
|
329 |
(*/------------------- check result of Test_Code.init_calc @{context} ----------------------------------------\*)
|
walther@60010
|
330 |
(*+*)val (o_model, ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]), _) =
|
walther@60010
|
331 |
get_obj g_origin pt (fst p);
|
Walther@60655
|
332 |
(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
|
walther@60010
|
333 |
"(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
|
walther@60010
|
334 |
"(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
|
walther@60010
|
335 |
"(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
|
walther@60010
|
336 |
"(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
|
walther@60010
|
337 |
"(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
|
Walther@60736
|
338 |
"(6, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"]), \n" ^
|
Walther@60736
|
339 |
"(7, [\"1\"], #undef, Biegemoment, [\"M_b\"]), \n" ^
|
Walther@60736
|
340 |
"(8, [\"1\"], #undef, Querkraft, [\"Q\"]), \n" ^
|
Walther@60736
|
341 |
"(9, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"
|
walther@60010
|
342 |
then () else error "[IntegrierenUndKonstanteBestimmen2] O_Model CHANGED";
|
Walther@60571
|
343 |
(*\------------------- check result of Test_Code.init_calc @{context} ----------------------------------------/*)
|
walther@60010
|
344 |
|
Walther@60736
|
345 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Traegerlaenge L" = nxt
|
Walther@60736
|
346 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Streckenlast q_0" = nxt
|
Walther@60736
|
347 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Biegelinie y" = nxt
|
Walther@60736
|
348 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" = nxt
|
Walther@60729
|
349 |
(*/---broken elementwise input to lists---\* )
|
walther@60010
|
350 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
|
Walther@60729
|
351 |
( *\---broken elementwise input to lists---/*)
|
walther@60010
|
352 |
|
Walther@60736
|
353 |
val return_me_Add_Relation_Randbedingungen = me nxt p c pt; (*\<rightarrow>Specify_Problem ["Biegelinien"]*)
|
Walther@60736
|
354 |
(*/------------------- step into me_Add_Relation_Randbedingungen ---------------------------\\*)
|
Walther@60736
|
355 |
"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
|
Walther@60736
|
356 |
val ctxt = Ctree.get_ctxt pt p
|
Walther@60736
|
357 |
val (pt, p) =
|
Walther@60736
|
358 |
(*Step.by_tactic is here for testing by me; do_next would suffice in me*)
|
Walther@60736
|
359 |
case Step.by_tactic tac (pt, p) of
|
Walther@60736
|
360 |
("ok", (_, _, ptp)) => ptp
|
Walther@60736
|
361 |
|
Walther@60736
|
362 |
val ("ok", ([(Specify_Theory "Biegelinie", _, _)], _, _)) =
|
Walther@60736
|
363 |
(*case*)
|
Walther@60736
|
364 |
Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
|
Walther@60736
|
365 |
"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
|
Walther@60736
|
366 |
(p, ((pt, Pos.e_pos'), []));
|
Walther@60736
|
367 |
(*if*) Pos.on_calc_end ip (*else*);
|
Walther@60736
|
368 |
val (_, probl_id, _) = Calc.references (pt, p);
|
Walther@60736
|
369 |
val _ =
|
Walther@60736
|
370 |
(*case*) tacis (*of*);
|
Walther@60736
|
371 |
(*if*) probl_id = Problem.id_empty (*else*);
|
Walther@60736
|
372 |
|
Walther@60736
|
373 |
switch_specify_solve p_ (pt, ip);
|
Walther@60736
|
374 |
"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
|
Walther@60736
|
375 |
(*if*) Pos.on_specification ([], state_pos) (*then*);
|
Walther@60736
|
376 |
|
Walther@60736
|
377 |
specify_do_next (pt, input_pos);
|
Walther@60736
|
378 |
"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
|
Walther@60736
|
379 |
val (_, (p_', tac)) = Specify.find_next_step ptp
|
Walther@60736
|
380 |
val ist_ctxt = Ctree.get_loc pt (p, p_)
|
Walther@60736
|
381 |
val Specify_Theory "Biegelinie" =
|
Walther@60736
|
382 |
(*case*) tac (*of*);
|
Walther@60736
|
383 |
|
Walther@60736
|
384 |
Step_Specify.by_tactic_input tac (pt, (p, p_'));
|
Walther@60736
|
385 |
|
Walther@60736
|
386 |
(*|------------------- contine me_Add_Relation_Randbedingungen -------------------------------*)
|
Walther@60736
|
387 |
(*\------------------- step into me_Add_Relation_Randbedingungen ---------------------------//*)
|
Walther@60736
|
388 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = return_me_Add_Relation_Randbedingungen;
|
Walther@60736
|
389 |
val Specify_Theory "Biegelinie" = nxt
|
Walther@60736
|
390 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["Biegelinien"] = nxt
|
Walther@60736
|
391 |
(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
|
Walther@60736
|
392 |
|
Walther@60736
|
393 |
(*[], Met*)val return_me_Specify_Method_IntegrierenUndKonstanteBestimmen2
|
Walther@60736
|
394 |
= me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)
|
Walther@60736
|
395 |
(*/------------------- step into me_Specify_Method_IntegrierenUndKonstanteBestimmen2--------\*)
|
walther@60010
|
396 |
|
walther@60010
|
397 |
(*/------------------- initial check for whole me ------------------------------------------\*)
|
walther@60010
|
398 |
(*+*)val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt;
|
walther@60010
|
399 |
|
walther@60010
|
400 |
(*+*)val {origin = (o_model, o_refs, _), probl = i_pbl, meth = i_met, spec, ...} =
|
walther@60010
|
401 |
Calc.specify_data (pt, p);
|
walther@60010
|
402 |
(*+*)if o_refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])
|
walther@60010
|
403 |
(*+*)then () else error "initial o_refs CHANGED";
|
Walther@60655
|
404 |
(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
|
walther@60010
|
405 |
"(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
|
walther@60010
|
406 |
"(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
|
walther@60010
|
407 |
"(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
|
walther@60010
|
408 |
"(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
|
walther@60010
|
409 |
"(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
|
Walther@60736
|
410 |
"(6, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"]), \n" ^
|
Walther@60736
|
411 |
"(7, [\"1\"], #undef, Biegemoment, [\"M_b\"]), \n" ^
|
Walther@60736
|
412 |
"(8, [\"1\"], #undef, Querkraft, [\"Q\"]), \n" ^
|
Walther@60736
|
413 |
"(9, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"
|
walther@60010
|
414 |
(*+*)then () else error "initial o_model CHANGED";
|
walther@60010
|
415 |
(*+*)if I_Model.to_string @{context} i_pbl = "[\n" ^
|
Walther@60739
|
416 |
"(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
|
Walther@60739
|
417 |
"(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
|
Walther@60739
|
418 |
"(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n" ^
|
Walther@60739
|
419 |
"(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str)]"
|
walther@60010
|
420 |
(*+*)then () else error "initial i_pbl CHANGED";
|
walther@60010
|
421 |
(*+*)if I_Model.to_string @{context} i_met = "[]"
|
walther@60010
|
422 |
(*+*)then () else error "initial i_met CHANGED";
|
walther@60010
|
423 |
(*+*)val (_, ["Biegelinien"], _) = spec;
|
walther@60010
|
424 |
(*\------------------- initial check for whole me ------------------------------------------/*)
|
walther@60010
|
425 |
|
walther@60010
|
426 |
"~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
|
walther@60010
|
427 |
(*/------------------- step into Step.by_tactic \\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\*)
|
walther@60010
|
428 |
val (pt'''''_', p'''''_') = case
|
walther@60010
|
429 |
|
walther@60010
|
430 |
Step.by_tactic tac (pt, p) of ("ok", (_, _, ptp)) => ptp;
|
walther@60010
|
431 |
(*/------------------- check for entry to Step.by_tactic -----------------------------------\*)
|
walther@60010
|
432 |
(*+*)val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = tac;
|
walther@60010
|
433 |
(*+*)val {origin = (o_model, _, _), ...} = Calc.specify_data (pt, p);
|
Walther@60655
|
434 |
(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
|
walther@60010
|
435 |
"(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
|
walther@60010
|
436 |
"(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
|
walther@60010
|
437 |
"(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
|
walther@60010
|
438 |
"(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
|
walther@60010
|
439 |
"(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
|
Walther@60736
|
440 |
"(6, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"]), \n" ^
|
Walther@60736
|
441 |
"(7, [\"1\"], #undef, Biegemoment, [\"M_b\"]), \n" ^
|
Walther@60736
|
442 |
"(8, [\"1\"], #undef, Querkraft, [\"Q\"]), \n" ^
|
Walther@60736
|
443 |
"(9, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"
|
walther@60010
|
444 |
(*+*)then () else error "o_model AFTER Specify_Method NOTok CHANGED";
|
walther@60010
|
445 |
(*\------------------- check for Step.by_tactic --------------------------------------------/*)
|
walther@60010
|
446 |
"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
|
walther@60010
|
447 |
val Applicable.Yes tac' = (*case*)
|
walther@60010
|
448 |
|
walther@60010
|
449 |
Step.check tac (pt, p) (*of*);
|
walther@60010
|
450 |
"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
|
walther@60010
|
451 |
(*if*) Tactic.for_specify tac (*then*);
|
walther@60010
|
452 |
|
walther@60010
|
453 |
Specify_Step.check tac (ctree, pos);
|
walther@60010
|
454 |
"~~~~~ fun check , args:"; val ((Tactic.Specify_Method mID), (ctree, pos)) = (tac, (ctree, pos));
|
walther@60010
|
455 |
|
walther@60010
|
456 |
val (o_model''''', _, i_model''''') =
|
walther@60014
|
457 |
Specify_Step.complete_for mID (ctree, pos);
|
walther@60014
|
458 |
"~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (mID, (ctree, pos));
|
walther@60010
|
459 |
val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
|
walther@60010
|
460 |
...} = Calc.specify_data (ctree, pos);
|
Walther@60494
|
461 |
val (dI, _, _) = References.select_input o_refs refs;
|
Walther@60586
|
462 |
val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
|
walther@60010
|
463 |
val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
|
walther@60010
|
464 |
val (o_model', ctxt') =
|
walther@60010
|
465 |
|
walther@60010
|
466 |
O_Model.complete_for m_patt root_model (o_model, ctxt);
|
walther@60014
|
467 |
(*/------------------- check entry to O_Model.complete_for -----------------------------------------\*)
|
Walther@60655
|
468 |
(*+*)Model_Pattern.to_string @{context} m_patt = "[\"" ^
|
walther@60010
|
469 |
"(#Given, (Traegerlaenge, l))\", \"" ^
|
walther@60010
|
470 |
"(#Given, (Streckenlast, q))\", \"" ^
|
walther@60010
|
471 |
"(#Given, (FunktionsVariable, v))\", \"" ^
|
walther@60010
|
472 |
"(#Given, (GleichungsVariablen, vs))\", \"" ^
|
walther@60010
|
473 |
"(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^
|
walther@60010
|
474 |
"(#Find, (Biegelinie, b))\", \"" ^
|
walther@60010
|
475 |
"(#Relate, (Randbedingungen, s))\"]";
|
Walther@60736
|
476 |
(*+*) O_Model.to_string @{context} root_model;
|
walther@60014
|
477 |
(*\------------------- check entry to O_Model.complete_for -----------------------------------------/*)
|
walther@60010
|
478 |
"~~~~~ fun complete_for , args:"; val (m_patt, root_model, (o_model, ctxt)) = (m_patt, root_model, (o_model, ctxt));
|
walther@60010
|
479 |
val missing = m_patt |> filter_out
|
walther@60017
|
480 |
(fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor));
|
walther@60010
|
481 |
val add = (root_model
|
walther@60010
|
482 |
|> filter
|
walther@60017
|
483 |
(fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor))
|
walther@60010
|
484 |
;
|
walther@60010
|
485 |
((o_model @ add)
|
walther@60010
|
486 |
|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
|
walther@60010
|
487 |
|> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
|
Walther@60472
|
488 |
|> add_enumerate (* for correct enumeration *)
|
walther@60010
|
489 |
|> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
|
walther@60014
|
490 |
ctxt |> ContextC.add_constraints (add |> values |> TermC.vars')) (*return from O_Model.complete_for*);
|
walther@60014
|
491 |
"~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.complete_for , return:"; val (o_model', ctxt') =
|
walther@60010
|
492 |
((o_model @ add)
|
walther@60010
|
493 |
|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
|
walther@60010
|
494 |
|> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
|
Walther@60472
|
495 |
|> add_enumerate (* for correct enumeration *)
|
walther@60010
|
496 |
|> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
|
walther@60010
|
497 |
ctxt |> ContextC.add_constraints (add |> values |> TermC.vars'));
|
walther@60010
|
498 |
|
walther@60014
|
499 |
(*/------------------- check of result from O_Model.complete_for -----------------------------------\*)
|
Walther@60736
|
500 |
(*+*) O_Model.to_string @{context} o_model'; "O_Model.complete_for: result o_model CHANGED";
|
walther@60014
|
501 |
(*\------------------- check of result from O_Model.complete_for -----------------------------------/*)
|
walther@60010
|
502 |
|
Walther@60676
|
503 |
val thy = ThyC.get_theory @{context} dI
|
Walther@60590
|
504 |
val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
|
walther@60010
|
505 |
|
walther@60014
|
506 |
(o_model', ctxt', i_model) (*return from Specify_Step.complete_for*);
|
walther@60010
|
507 |
|
walther@60014
|
508 |
"~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.check , return:"; val (o_model, _, i_model) =
|
walther@60010
|
509 |
(o_model', ctxt', i_model);
|
walther@60010
|
510 |
|
walther@60010
|
511 |
Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model)) (*return from Specify_Step.check*);
|
walther@60010
|
512 |
"~~~~~ fun Specify_Step.check \<longrightarrow>fun Step.check \<longrightarrow>fun Step.by_tactic , return:"; val (Applicable.Yes tac') =
|
walther@60010
|
513 |
(Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model)));
|
walther@60010
|
514 |
(*if*) Tactic.for_specify' tac' (*then*);
|
walther@60010
|
515 |
val ("ok", ([], [], (_, _))) =
|
walther@60010
|
516 |
|
walther@60010
|
517 |
Step_Specify.by_tactic tac' ptp;
|
walther@60010
|
518 |
"~~~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt,pos as (p, _))) =
|
walther@60010
|
519 |
(tac', ptp);
|
walther@60010
|
520 |
(*NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
|
walther@60010
|
521 |
(*NEW*) ...} = Calc.specify_data (pt, pos);
|
Walther@60494
|
522 |
(*NEW*) val (dI, _, mID) = References.select_input o_refs refs;
|
Walther@60586
|
523 |
(*NEW*) val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
|
walther@60010
|
524 |
(*NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
|
walther@60010
|
525 |
(*NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
|
Walther@60676
|
526 |
(*NEW*) val thy = ThyC.get_theory @{context} dI
|
Walther@60590
|
527 |
(*NEW*) val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
|
walther@60010
|
528 |
(*NEW*) val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', i_model))
|
walther@60010
|
529 |
(*NEW*) (Istate_Def.Uistate, ctxt') (pt, pos)
|
walther@60010
|
530 |
|
walther@60010
|
531 |
(*/------------------- check result of Step_Specify.by_tactic ------------------------------\*)
|
walther@60010
|
532 |
(*+*)val {origin = (o_model, _, _), meth, ...} = Calc.specify_data (pt, pos);
|
Walther@60736
|
533 |
(*+*)O_Model.to_string @{context} o_model;
|
walther@60010
|
534 |
(*+*)if I_Model.to_string @{context} meth = "[\n" ^
|
Walther@60739
|
535 |
"(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
|
Walther@60739
|
536 |
"(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
|
Walther@60739
|
537 |
"(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n" ^
|
Walther@60739
|
538 |
"(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str), \n" ^
|
walther@60023
|
539 |
"(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^
|
Walther@60736
|
540 |
"(6 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der), \n" ^
|
Walther@60736
|
541 |
"(7 ,[1] ,false ,#Given ,Mis Biegemoment id_momentum), \n" ^
|
Walther@60736
|
542 |
"(8 ,[1] ,false ,#Given ,Mis Querkraft id_lat_force), \n" ^
|
Walther@60736
|
543 |
"(9 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs)]"
|
walther@60010
|
544 |
(*+*)then () else error "result of Step_Specify.by_tactic o_model CHANGED";
|
walther@60010
|
545 |
(*\------------------- check result of Step_Specify.by_tactic ------------------------------/*)
|
walther@60010
|
546 |
(*\------------------- step into Step.by_tactic /////////////////////////////////////////////*)
|
walther@60010
|
547 |
|
walther@60010
|
548 |
|
walther@60020
|
549 |
val (_, ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
|
walther@60010
|
550 |
Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []) (*of*);
|
walther@60010
|
551 |
(*/------------------- step into Step.do_next \\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\*)
|
walther@60010
|
552 |
"~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
|
walther@60010
|
553 |
(p'''''_', ((pt'''''_', Pos.e_pos'), []));
|
walther@60010
|
554 |
(*if*) Pos.on_calc_end ip (*else*);
|
walther@60010
|
555 |
val (_, probl_id, _) = Calc.references (pt, p);
|
walther@60010
|
556 |
val _ = (*case*) tacis (*of*);
|
walther@60010
|
557 |
(*if*) probl_id = Problem.id_empty (*else*);
|
walther@60010
|
558 |
|
walther@60020
|
559 |
val (_, ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
|
walther@60010
|
560 |
switch_specify_solve p_ (pt, ip);
|
walther@60010
|
561 |
"~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
|
walther@60010
|
562 |
(*if*) Pos.on_specification ([], state_pos) (*then*);
|
walther@60010
|
563 |
|
walther@60020
|
564 |
val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], [], (pt'''''_'', p'''''_''))) =
|
Walther@60556
|
565 |
Step.specify_do_next (pt, input_pos);
|
walther@60010
|
566 |
(*/------------------- check result of specify_do_next -------------------------------------\*)
|
walther@60010
|
567 |
(*+*)val {origin = (ooo_mod, _, _), meth, ...} = Calc.specify_data (pt'''''_'', p'''''_'');
|
Walther@60736
|
568 |
(*+*) O_Model.to_string @{context} ooo_mod; "result of Step_Specify.by_tactic o_model CHANGED";
|
walther@60010
|
569 |
(*+*)if I_Model.to_string @{context} meth = "[\n" ^
|
Walther@60739
|
570 |
"(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
|
Walther@60739
|
571 |
"(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
|
Walther@60739
|
572 |
"(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n" ^
|
Walther@60739
|
573 |
"(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str), \n" ^
|
Walther@60739
|
574 |
"(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x , pen2str), \n" ^
|
Walther@60736
|
575 |
"(6 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der), \n" ^
|
Walther@60736
|
576 |
"(7 ,[1] ,false ,#Given ,Mis Biegemoment id_momentum), \n" ^
|
Walther@60736
|
577 |
"(8 ,[1] ,false ,#Given ,Mis Querkraft id_lat_force), \n" ^
|
Walther@60736
|
578 |
"(9 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs)]"
|
walther@60010
|
579 |
(*+*)then () else error "result of Step_Specify.by_tactic i_model CHANGED";
|
walther@60010
|
580 |
(*\------------------- check result of specify_do_next -------------------------------------/*)
|
walther@60010
|
581 |
"~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
|
walther@60010
|
582 |
|
walther@60010
|
583 |
(**)val (_, (p_', Add_Given "FunktionsVariable x")) =(**)
|
walther@60010
|
584 |
Specify.find_next_step ptp;
|
Walther@60556
|
585 |
"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
|
Walther@60556
|
586 |
val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
|
Walther@60556
|
587 |
spec = refs, ...} = Calc.specify_data (pt, pos);
|
Walther@60556
|
588 |
val ctxt = Ctree.get_ctxt pt pos;
|
Walther@60556
|
589 |
(*if*) Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin (*else*);
|
Walther@60556
|
590 |
(*if*) p_ = Pos.Pbl (*else*);
|
Walther@60736
|
591 |
|
Walther@60575
|
592 |
val return = for_problem ctxt oris (o_refs, refs) (pbl, met);
|
Walther@60556
|
593 |
"~~~~~ fun for_method , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
|
Walther@60556
|
594 |
(oris, (o_refs, refs), (pbl, met));
|
Walther@60556
|
595 |
val cmI = if mI = MethodC.id_empty then mI' else mI;
|
Walther@60730
|
596 |
val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI;
|
Walther@60741
|
597 |
val (preok, _) = Pre_Conds.check ctxt where_rls where_ (mpc, I_Model.OLD_to_TEST met);
|
Walther@60556
|
598 |
"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return);
|
walther@60010
|
599 |
(*/------------------- check within find_next_step -----------------------------------------\*)
|
Walther@60655
|
600 |
(*+*)Model_Pattern.to_string @{context} (MethodC.from_store ctxt mI' |> #model) = "[\"" ^
|
walther@60010
|
601 |
"(#Given, (Traegerlaenge, l))\", \"" ^
|
walther@60010
|
602 |
"(#Given, (Streckenlast, q))\", \"" ^
|
walther@60010
|
603 |
"(#Given, (FunktionsVariable, v))\", \"" ^ (* <---------- take m_field from here !!!*)
|
walther@60010
|
604 |
"(#Given, (GleichungsVariablen, vs))\", \"" ^
|
walther@60010
|
605 |
"(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^
|
walther@60010
|
606 |
"(#Find, (Biegelinie, b))\", \"" ^
|
walther@60010
|
607 |
"(#Relate, (Randbedingungen, s))\"]";
|
walther@60010
|
608 |
(*\------------------- check within find_next_step -----------------------------------------/*)
|
walther@60010
|
609 |
|
Walther@60676
|
610 |
(*case*) item_to_add (ThyC.get_theory @{context} (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
|
walther@60010
|
611 |
"~~~~~ ~ fun item_to_add , args:"; val (thy, oris, _, itms) =
|
Walther@60676
|
612 |
((ThyC.get_theory @{context} (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
|
walther@60017
|
613 |
(*OLD*)fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v (**)andalso (#3 ori) <> "#undef"(**)
|
walther@60017
|
614 |
fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
|
walther@60017
|
615 |
fun test_id ids r = member op= ids (#1 (r : O_Model.single))
|
walther@60010
|
616 |
fun test_subset itm (_, _, _, d, ts) =
|
Walther@60477
|
617 |
(I_Model.descriptor (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.o_model_values (#5 itm), ts)
|
walther@60010
|
618 |
fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
|
walther@60010
|
619 |
| false_and_not_Sup (_, _, false, _, _) = true
|
walther@60010
|
620 |
| false_and_not_Sup _ = false
|
Walther@60705
|
621 |
val v = if itms = [] then 1 else Pre_Conds.max_variant itms
|
walther@60010
|
622 |
val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
|
walther@60010
|
623 |
val vits =
|
walther@60010
|
624 |
if v = 0
|
walther@60010
|
625 |
then itms (* because of dsc without dat *)
|
walther@60010
|
626 |
else filter (testi_vt v) itms; (* itms..vat *)
|
walther@60010
|
627 |
val icl = filter false_and_not_Sup vits; (* incomplete *)
|
walther@60010
|
628 |
|
walther@60010
|
629 |
(*/------------------- check within item_to_add --------------------------------------------\*)
|
Walther@60736
|
630 |
(*+*)if I_Model.to_string @{context} icl = "[\n" ^ (*.. values, not formals*)
|
Walther@60736
|
631 |
"(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^ (*.. values, not formals*)
|
Walther@60736
|
632 |
"(6 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der), \n" ^ (*.. values, not formals*)
|
Walther@60736
|
633 |
"(7 ,[1] ,false ,#Given ,Mis Biegemoment id_momentum), \n" ^ (*.. values, not formals*)
|
Walther@60736
|
634 |
"(8 ,[1] ,false ,#Given ,Mis Querkraft id_lat_force), \n" ^ (*.. values, not formals*)
|
Walther@60736
|
635 |
"(9 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs)]"
|
walther@60010
|
636 |
(*+*)then () else error "icl within item_to_add CHANGED";
|
Walther@60736
|
637 |
(*+*) O_Model.to_string @{context} vors; "vors within item_to_add CHANGED";
|
walther@60010
|
638 |
(*+*)if I_Model.to_string @{context} itms = "[\n" ^
|
Walther@60739
|
639 |
"(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
|
Walther@60739
|
640 |
"(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
|
Walther@60739
|
641 |
"(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n" ^
|
Walther@60739
|
642 |
"(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str), \n" ^
|
Walther@60736
|
643 |
"(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^
|
Walther@60736
|
644 |
"(6 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der), \n" ^
|
Walther@60736
|
645 |
"(7 ,[1] ,false ,#Given ,Mis Biegemoment id_momentum), \n" ^
|
Walther@60736
|
646 |
"(8 ,[1] ,false ,#Given ,Mis Querkraft id_lat_force), \n" ^
|
Walther@60736
|
647 |
"(9 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs)]"
|
walther@60010
|
648 |
(*+*)then () else error "i_model within item_to_add CHANGED";
|
walther@60010
|
649 |
(*\------------------- check within item_to_add --------------------------------------------/*)
|
walther@60010
|
650 |
|
walther@60010
|
651 |
(*if*) icl = [] (*else*);
|
walther@60010
|
652 |
val SOME ori =(*case*) find_first (test_subset (hd icl)) vors (*of*);
|
walther@60010
|
653 |
|
walther@60336
|
654 |
(*+*)val (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]) = ori
|
walther@60010
|
655 |
(*+*)val SOME ("#Given", "FunktionsVariable x") =
|
walther@60010
|
656 |
|
walther@60010
|
657 |
SOME
|
Walther@60477
|
658 |
(I_Model.get_field_term thy ori (hd icl)) (*return from item_to_add*);
|
Walther@60477
|
659 |
"~~~~~ ~~ fun get_field_term , args:"; val (thy, (_, _, _, d, ts), (_, _, _, fd, itm_)) = (thy, ori, (hd icl));
|
walther@60010
|
660 |
|
walther@60010
|
661 |
val rrrrr =
|
walther@60010
|
662 |
(fd, ((UnparseC.term_in_thy thy) o Input_Descript.join)
|
Walther@60477
|
663 |
(d, subtract op = (o_model_values itm_) ts)) (*return from get_field_term*);
|
Walther@60477
|
664 |
"~~~~~ ~~ from fun get_field_term \<longrightarrow>fun item_to_add \<longrightarrow>fun find_next_step , return:"; val (SOME (fd, ct')) =
|
walther@60010
|
665 |
(SOME rrrrr);
|
walther@60010
|
666 |
("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*return from find_next_step*);
|
walther@60010
|
667 |
|
walther@60010
|
668 |
(*+*)val Add_Given "FunktionsVariable x" = P_Model.mk_additem fd ct';
|
walther@60010
|
669 |
|
walther@60010
|
670 |
"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) =
|
walther@60010
|
671 |
("dummy", (Pos.Met, P_Model.mk_additem fd ct'));
|
walther@60010
|
672 |
val ist_ctxt = Ctree.get_loc pt (p, p_)
|
walther@60010
|
673 |
val _ = (*case*) tac (*of*);
|
walther@60010
|
674 |
|
walther@60010
|
675 |
("dummy",
|
walther@60010
|
676 |
Step_Specify.by_tactic_input tac (pt, (p, p_'))) (*return from specify_do_next*);
|
walther@60010
|
677 |
"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =
|
walther@60010
|
678 |
(tac, (pt, (p, p_')));
|
walther@60010
|
679 |
|
walther@60021
|
680 |
val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
|
walther@60021
|
681 |
Specify.by_Add_ "#Given" ct ptp (*return from by_tactic_input*);
|
walther@60021
|
682 |
"~~~~~ ~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);
|
walther@60097
|
683 |
val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
|
walther@60021
|
684 |
(*if*) p_ = Pos.Met (*then*);
|
walther@60021
|
685 |
val (i_model, m_patt) = (met,
|
Walther@60586
|
686 |
(if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
|
walther@60010
|
687 |
|
walther@60336
|
688 |
val Add (5, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), (Free ("fun_var", _), [Free ("x", _)]))) =
|
walther@60010
|
689 |
(*case*)
|
walther@60021
|
690 |
I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
|
walther@60010
|
691 |
"~~~~~ ~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
|
walther@60021
|
692 |
(ctxt, m_field, oris, i_model, m_patt, ct);
|
Walther@60663
|
693 |
(*.NEW*) val SOME (t as (descriptor $ _)) = (*case*) ParseC.term_opt ctxt str (*of*);
|
walther@60010
|
694 |
(*.NEW*) val SOME m_field = (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
|
walther@60010
|
695 |
|
walther@60336
|
696 |
val ("", (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), [Free ("x", _)]) =
|
walther@60010
|
697 |
(*case*)
|
Walther@60471
|
698 |
O_Model.contains ctxt m_field o_model t (*of*);
|
Walther@60471
|
699 |
"~~~~~ ~~~ fun contains , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
|
walther@60017
|
700 |
val ots = ((distinct op =) o flat o (map #5)) ori
|
walther@60017
|
701 |
val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots
|
walther@60010
|
702 |
val (d, ts) = Input_Descript.split t
|
walther@60017
|
703 |
val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts);
|
walther@60010
|
704 |
(*if*) (subtract op = oids ids) <> [] (*else*);
|
walther@60010
|
705 |
(*if*) d = TermC.empty (*else*);
|
walther@60017
|
706 |
(*if*) member op = (map #4 ori) d (*then*);
|
walther@60010
|
707 |
|
Walther@60471
|
708 |
associate_input ctxt sel (d, ts) ori;
|
Walther@60471
|
709 |
"~~~~~ ~~~~ fun associate_input , args:"; val (ctxt, m_field, (descript, vals), ((id, vat, m_field', descript', vals') :: oris)) =
|
walther@60010
|
710 |
(ctxt, sel, (d, ts), ori);
|
walther@60010
|
711 |
|
Walther@60469
|
712 |
(*/------------------- check within associate_input ------------------------------------------\*)
|
walther@60010
|
713 |
(*+*)val Add_Given "FunktionsVariable x" = tac;
|
walther@60010
|
714 |
(*+*)m_field = "#Given";
|
walther@60336
|
715 |
(*+*)val Const (\<^const_name>\<open>FunktionsVariable\<close>, _) = descript;
|
walther@60010
|
716 |
(*+*)val [Free ("x", _)] = vals;
|
Walther@60655
|
717 |
(*+*)O_Model.to_string @{context} ori = "[\n" ^
|
walther@60010
|
718 |
"(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
|
walther@60010
|
719 |
"(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
|
walther@60010
|
720 |
"(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
|
walther@60010
|
721 |
"(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
|
walther@60010
|
722 |
"(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
|
walther@60010
|
723 |
"(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
|
walther@60010
|
724 |
"(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]";
|
walther@60010
|
725 |
(*+*)val (id, vat, m_field', descript', vals') = nth 5 ori
|
walther@60336
|
726 |
(*+*)val (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]) =
|
walther@60010
|
727 |
(id, vat, m_field', descript', vals')
|
Walther@60469
|
728 |
(*\------------------- check within associate_input ----------------------------------------/*)
|
Walther@60736
|
729 |
(*\------------------- step into me_Specify_Method_IntegrierenUndKonstanteBestimmen2--------*)
|
Walther@60736
|
730 |
(*[], Met*)val (p,_,f,nxt,_,pt) = return_me_Specify_Method_IntegrierenUndKonstanteBestimmen2
|
Walther@60736
|
731 |
val Add_Given "FunktionsVariable x" = nxt;
|
walther@60010
|
732 |
|
Walther@60736
|
733 |
(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy" = nxt
|
Walther@60736
|
734 |
(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Biegemoment M_b" = nxt
|
Walther@60736
|
735 |
(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Querkraft Q" = nxt
|
Walther@60736
|
736 |
(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]" = nxt
|
Walther@60736
|
737 |
(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
|
walther@60010
|
738 |
|
Walther@60736
|
739 |
(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
|
walther@60010
|
740 |
(*/------------------- check entry to me Model_Problem -------------------------------------\*)
|
walther@60010
|
741 |
(*+*)val ([1], Pbl) = p;
|
walther@60010
|
742 |
(*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =
|
walther@60010
|
743 |
get_obj g_origin pt (fst p);
|
Walther@60655
|
744 |
(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
|
walther@60010
|
745 |
"(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
|
walther@60010
|
746 |
"(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
|
walther@60010
|
747 |
"(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
|
walther@60010
|
748 |
(*
|
walther@60154
|
749 |
.. here the O_Model does NOT know, which MethodC will be chosen,
|
Walther@60710
|
750 |
so "belastung_zu_biegelinie q__q v_v b_b id_abl" is NOT known,
|
Walther@60710
|
751 |
"b_b" and "id_abl" are NOT missing.
|
walther@60010
|
752 |
*)
|
walther@60010
|
753 |
then () else error "[Biegelinien, ausBelastung] initial O_Model CHANGED";
|
walther@60010
|
754 |
(*\------------------- check entry to me Model_Problem -------------------------------------/*)
|
walther@60010
|
755 |
|
walther@60010
|
756 |
(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "Streckenlast q_0"*)
|
walther@60010
|
757 |
(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)
|
walther@60010
|
758 |
(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "Funktionen funs'''":*)
|
walther@60010
|
759 |
(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Theory "Biegelinie"*)
|
walther@60010
|
760 |
(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Problem ["vonBelastungZu", "Biegelinien"]*)
|
walther@60010
|
761 |
(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Method ["Biegelinien", "ausBelastung"]*)
|
walther@60010
|
762 |
|
Walther@60736
|
763 |
(*[1], Met*)val return_me_Specify_Method_ausBelastung = me nxt p c pt; (*\<rightarrow>Add_Given "Biegelinie y"*)
|
Walther@60736
|
764 |
(*//------------------ step into me_Specify_Method_ausBelastung ----------------------------\\*)
|
walther@60010
|
765 |
(*+*)val Specify_Method ["Biegelinien", "ausBelastung"] = nxt;
|
Walther@60710
|
766 |
(*+*)(* by \<up> \<up> \<up> \<up> "b_b" and "id_abl" must be requested: PUT THEM INTO O_Model*)
|
walther@60010
|
767 |
|
walther@60010
|
768 |
"~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
|
walther@60010
|
769 |
|
walther@60010
|
770 |
val ("ok", ([], [], (_, _))) = (*case*)
|
walther@60010
|
771 |
Step.by_tactic tac (pt, p) (*of*);
|
walther@60010
|
772 |
"~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
|
walther@60010
|
773 |
val Applicable.Yes tac' = (*case*) check tac (pt, p) (*of*);
|
walther@60010
|
774 |
(*if*) Tactic.for_specify' tac' (*then*);
|
walther@60010
|
775 |
|
walther@60010
|
776 |
val ("ok", ([], [], (_, _))) =
|
walther@60010
|
777 |
Step_Specify.by_tactic tac' ptp;
|
walther@60010
|
778 |
(*/------------------- initial check for Step_Specify.by_tactic ----------------------------\*)
|
walther@60010
|
779 |
(*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =
|
walther@60010
|
780 |
get_obj g_origin pt (fst p);
|
Walther@60655
|
781 |
(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
|
walther@60010
|
782 |
"(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
|
walther@60010
|
783 |
"(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
|
walther@60010
|
784 |
"(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
|
walther@60010
|
785 |
(*
|
walther@60154
|
786 |
.. here the MethodC has been determined by the user,
|
Walther@60710
|
787 |
so "belastung_zu_biegelinie q__q v_v b_b id_abl" IS KNOWN and,
|
Walther@60710
|
788 |
"b_b" and "id_abl" WOULD BE missing (added by O_Model.).
|
walther@60010
|
789 |
*)
|
walther@60154
|
790 |
then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY MethodC";
|
walther@60010
|
791 |
(*\------------------- initial check for Step_Specify.by_tactic ----------------------------/*)
|
walther@60010
|
792 |
"~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt, pos as (p, _))) =
|
walther@60010
|
793 |
(tac', ptp);
|
walther@60010
|
794 |
(*.NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,
|
walther@60010
|
795 |
(*.NEW*) ...} =Calc.specify_data (pt, pos);
|
Walther@60494
|
796 |
(*.NEW*) val (dI, _, mID) = References.select_input o_refs refs;
|
Walther@60586
|
797 |
(*.NEW*) val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
|
walther@60010
|
798 |
(*.NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
|
walther@60010
|
799 |
(*.NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt);
|
walther@60010
|
800 |
|
walther@60010
|
801 |
(*/------------------- check for entry to O_Model.complete_for -----------------------------\*)
|
walther@60010
|
802 |
(*+*)if mID = ["Biegelinien", "ausBelastung"]
|
walther@60154
|
803 |
(*+*)then () else error "MethodC [Biegelinien, ausBelastung] CHANGED";
|
Walther@60655
|
804 |
(*+*)if Model_Pattern.to_string @{context} m_patt = "[\"" ^
|
walther@60010
|
805 |
"(#Given, (Streckenlast, q__q))\", \"" ^
|
walther@60010
|
806 |
"(#Given, (FunktionsVariable, v_v))\", \"" ^
|
Walther@60736
|
807 |
"(#Given, (Biegelinie, b_b))\", \"" ^
|
Walther@60736
|
808 |
"(#Given, (AbleitungBiegelinie, id_der))\", \"" ^
|
Walther@60736
|
809 |
"(#Given, (Biegemoment, id_momentum))\", \"" ^
|
Walther@60736
|
810 |
"(#Given, (Querkraft, id_lat_force))\", \"" ^
|
walther@60010
|
811 |
"(#Find, (Funktionen, fun_s))\"]"
|
walther@60010
|
812 |
(*+*)then () else error "[Biegelinien, ausBelastung] Model_Pattern CHANGED";
|
Walther@60655
|
813 |
(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
|
walther@60010
|
814 |
"(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
|
walther@60010
|
815 |
"(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
|
walther@60010
|
816 |
"(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
|
walther@60154
|
817 |
(*+*)then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY MethodC CHANGED";
|
Walther@60736
|
818 |
(*+*) O_Model.to_string @{context} root_model;
|
Walther@60736
|
819 |
(*+*) O_Model.to_string @{context} o_model';
|
Walther@60736
|
820 |
"[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";
|
walther@60010
|
821 |
(*\------------------- check for entry to O_Model.complete_for -----------------------------/*)
|
walther@60010
|
822 |
|
walther@60010
|
823 |
O_Model.complete_for m_patt root_model (o_model, ctxt);
|
walther@60010
|
824 |
"~~~~ fun complete_for , args:"; val (m_patt, root_model, (o_model, ctxt)) =
|
walther@60010
|
825 |
(m_patt, root_model, (o_model, ctxt));
|
walther@60010
|
826 |
val missing = m_patt |> filter_out
|
walther@60017
|
827 |
(fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor))
|
walther@60010
|
828 |
;
|
walther@60010
|
829 |
val add = root_model
|
walther@60010
|
830 |
|> filter
|
walther@60017
|
831 |
(fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor)
|
walther@60010
|
832 |
;
|
walther@60010
|
833 |
(o_model @ add
|
walther@60010
|
834 |
(*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
|
walther@60010
|
835 |
(*NEW*)
|
walther@60010
|
836 |
|> map (fn (_, b, c, d, e) => (b, c, d, e))
|
Walther@60472
|
837 |
|> add_enumerate
|
walther@60010
|
838 |
|> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
|
walther@60014
|
839 |
ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars')) (*return from O_Model.complete_for*);
|
walther@60014
|
840 |
"~~~~ from fun O_Model.complete_for \<longrightarrow>Step_Specify.by_tactic , return:"; val (o_model', ctxt') =
|
walther@60010
|
841 |
((o_model @ add)
|
walther@60010
|
842 |
(*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
|
walther@60010
|
843 |
(*NEW*)
|
walther@60010
|
844 |
|> map (fn (_, b, c, d, e) => (b, c, d, e))
|
Walther@60472
|
845 |
|> add_enumerate
|
walther@60010
|
846 |
|> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
|
walther@60010
|
847 |
ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars'));
|
walther@60010
|
848 |
|
walther@60014
|
849 |
(*/------------------- check within O_Model.complete_for -------------------------------------------\*)
|
Walther@60736
|
850 |
(*+*) O_Model.to_string @{context} o_model';
|
Walther@60736
|
851 |
"[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";
|
walther@60014
|
852 |
(*\------------------- check within O_Model.complete_for -------------------------------------------/*)
|
walther@60010
|
853 |
|
Walther@60676
|
854 |
(*.NEW*) val thy = ThyC.get_theory @{context} dI
|
Walther@60590
|
855 |
(*.NEW*) val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
|
walther@60010
|
856 |
(*.NEW*) val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', i_model))
|
walther@60010
|
857 |
(*.NEW*) (Istate_Def.Uistate, ctxt') (pt, pos)
|
walther@60010
|
858 |
;
|
Walther@60736
|
859 |
(*+*) I_Model.to_string @{context} i_model; "[Biegelinien, ausBelastung] I_Model CHANGED 1";
|
walther@60010
|
860 |
(*+*)val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt, ...} =
|
walther@60010
|
861 |
(*+*) Calc.specify_data (pt, pos);
|
walther@60010
|
862 |
(*+*)pos = ([1], Met);
|
walther@60010
|
863 |
|
walther@60010
|
864 |
("ok", ([], [], (pt, pos))) (*return from Step_Specify.by_tactic*);
|
walther@60010
|
865 |
"~~~ from Step_Specify.by_tactic \<longrightarrow>Step.by_tactic \<longrightarrow>fun me , return:"; val ("ok", (_, _, (pt, p))) =
|
walther@60010
|
866 |
("ok", ([], [], (pt, pos)));
|
walther@60010
|
867 |
(* val ("helpless", ([(xxxxx, _, _)], _, _)) = (*case*)*)
|
walther@60242
|
868 |
(* SHOULD BE \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> Add_Given "Biegelinie y" | Add_Given "AbleitungBiegelinie dy"*)
|
walther@60010
|
869 |
|
walther@60020
|
870 |
val ("ok", ([( Add_Given "Biegelinie y", _, _)], [], _)) =
|
walther@60010
|
871 |
Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
|
walther@60010
|
872 |
"~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
|
walther@60010
|
873 |
(*.NEW*)(*if*) on_calc_end ip (*else*);
|
walther@60010
|
874 |
(*.NEW*) val (_, probl_id, _) = Calc.references (pt, p);
|
walther@60010
|
875 |
(*-"-*) val _ = (*case*) tacis (*of*);
|
walther@60010
|
876 |
(*.NEW*) (*if*) probl_id = Problem.id_empty (*else*);
|
walther@60010
|
877 |
|
walther@60020
|
878 |
(*.NEW*)val ("ok", ([(Add_Given "Biegelinie y", _, _)], _, _)) =
|
walther@60010
|
879 |
switch_specify_solve p_ (pt, ip);
|
walther@60010
|
880 |
"~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
|
walther@60010
|
881 |
(*if*) Pos.on_specification ([], state_pos) (*then*);
|
walther@60010
|
882 |
|
walther@60020
|
883 |
val ("ok", ([(Add_Given "Biegelinie y", _, _)], _, _)) =
|
Walther@60556
|
884 |
specify_do_next (pt, input_pos);
|
walther@60010
|
885 |
"~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
|
walther@60010
|
886 |
|
walther@60010
|
887 |
val (_, (p_', tac)) =
|
walther@60010
|
888 |
Specify.find_next_step ptp;
|
Walther@60556
|
889 |
"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
|
Walther@60556
|
890 |
val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
|
Walther@60556
|
891 |
spec = refs, ...} = Calc.specify_data (pt, pos);
|
Walther@60556
|
892 |
val ctxt = Ctree.get_ctxt pt pos
|
walther@60010
|
893 |
;
|
Walther@60655
|
894 |
(*+*)O_Model.to_string @{context} oris = "[\n" ^
|
walther@60010
|
895 |
"(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
|
walther@60010
|
896 |
"(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
|
walther@60010
|
897 |
"(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
|
walther@60010
|
898 |
"(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
|
walther@60010
|
899 |
"(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]";
|
walther@60010
|
900 |
(*+*)I_Model.is_complete pbl = true;
|
walther@60010
|
901 |
(*+*)I_Model.to_string @{context} met = "[\n" ^
|
walther@60010
|
902 |
"(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
|
walther@60010
|
903 |
"(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
|
walther@60010
|
904 |
"(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
|
Walther@60710
|
905 |
"(4 ,[1] ,false ,#Given ,Mis Biegelinie b_b), \n" ^
|
walther@60010
|
906 |
"(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";
|
walther@60010
|
907 |
|
Walther@60556
|
908 |
(*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
|
Walther@60556
|
909 |
(*if*) p_ = Pos.Pbl (*else*);
|
Walther@60575
|
910 |
val return = for_method ctxt oris (o_refs, refs) (pbl, met);
|
Walther@60556
|
911 |
"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return);
|
walther@60010
|
912 |
|
Walther@60556
|
913 |
val ist_ctxt = Ctree.get_loc pt (p, p_)
|
Walther@60556
|
914 |
val Add_Given "Biegelinie y" = (*case*) tac (*of*);
|
Walther@60556
|
915 |
val return = Step_Specify.by_tactic_input tac (pt, (p, p_'));
|
walther@60010
|
916 |
(*+*)val Add_Given "Biegelinie y" = tac;
|
walther@60010
|
917 |
val ist_ctxt = Ctree.get_loc pt (p, p_)
|
walther@60010
|
918 |
val _ = (*case*) tac (*of*);
|
walther@60010
|
919 |
|
walther@60020
|
920 |
val (_, ([(Add_Given "Biegelinie y", _, _)], _, (p'''''_'', ([1], Met)))) =
|
walther@60010
|
921 |
Step_Specify.by_tactic_input tac (pt, (p, p_'))
|
walther@60010
|
922 |
(*/------------------- check result of Step_Specify.by_tactic_input ------------------------\*)
|
walther@60010
|
923 |
(*+*)val {meth, ...} = Calc.specify_data (p'''''_'', ([1], Met));
|
walther@60010
|
924 |
(*+*)I_Model.to_string @{context} meth = "[\n" ^ (* result does NOT show Add_Given "Biegelinie y" *)
|
walther@60010
|
925 |
"(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
|
walther@60010
|
926 |
"(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
|
walther@60010
|
927 |
"(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
|
Walther@60710
|
928 |
"(4 ,[1] ,false ,#Given ,Mis Biegelinie b_b), \n" ^
|
walther@60010
|
929 |
"(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";
|
walther@60010
|
930 |
(*\------------------- check result of Step_Specify.by_tactic_input ------------------------/*)
|
walther@60010
|
931 |
"~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) = (tac, (pt, (p, p_')));
|
walther@60010
|
932 |
|
walther@60021
|
933 |
Specify.by_Add_ "#Given" ct ptp;
|
walther@60021
|
934 |
"~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);
|
walther@60097
|
935 |
val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
|
walther@60021
|
936 |
(*if*) p_ = Pos.Met (*then*);
|
walther@60021
|
937 |
val (i_model, m_patt) = (met,
|
Walther@60586
|
938 |
(if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
|
walther@60010
|
939 |
|
Walther@60710
|
940 |
val Add (4, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Biegelinie\<close>, _), [Free ("y", _)]), (Free ("b_b", _), [Free ("y", _)]))) =
|
walther@60010
|
941 |
(*case*)
|
walther@60021
|
942 |
check_single ctxt m_field oris i_model m_patt ct (*of*);
|
walther@60010
|
943 |
|
walther@60010
|
944 |
(*/------------------- check for entry to check_single -------------------------------------\*)
|
Walther@60736
|
945 |
(*+*) O_Model.to_string @{context} oris; "[Biegelinien, ausBelastung] O_Model CHANGED for entry";
|
Walther@60736
|
946 |
(*+*) I_Model.to_string ctxt met; "[Biegelinien, ausBelastung] I_Model CHANGED for entry";
|
walther@60010
|
947 |
(*\------------------- check for entry to check_single -------------------------------------/*)
|
walther@60010
|
948 |
|
walther@60010
|
949 |
"~~~~~ ~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
|
Walther@60586
|
950 |
(ctxt, sel, oris, met, ((#model o MethodC.from_store ctxt) cmI), ct);
|
Walther@60663
|
951 |
val SOME t = (*case*) ParseC.term_opt ctxt str (*of*);
|
walther@60010
|
952 |
|
walther@60336
|
953 |
(*+*)val Const (\<^const_name>\<open>Biegelinie\<close>, _) $ Free ("y", _) = t;
|
walther@60010
|
954 |
|
Walther@60471
|
955 |
(*("associate_input: input ('Biegelinie y') not found in oris (typed)", (0, [], "#Given", Const (\<^const_name>\<open>Biegelinie\<close>, "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]), [])*)
|
walther@60010
|
956 |
(*case*)
|
Walther@60471
|
957 |
contains ctxt m_field o_model t (*of*);
|
Walther@60471
|
958 |
"~~~~~ ~~ fun contains , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
|
walther@60017
|
959 |
val ots = ((distinct op =) o flat o (map #5)) ori
|
walther@60017
|
960 |
val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots
|
walther@60010
|
961 |
val (d, ts) = Input_Descript.split t
|
walther@60017
|
962 |
val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts);
|
walther@60010
|
963 |
(*if*) (subtract op = oids ids) <> [] (*else*);
|
walther@60010
|
964 |
(*if*) d = TermC.empty (*else*);
|
Walther@60471
|
965 |
(*if*) not (subset op = (map make_typeless ts, map make_typeless ots)) (*else*);
|
walther@60010
|
966 |
|
Walther@60471
|
967 |
(*case*) O_Model.associate_input' ctxt sel ts ori (*of*);
|
Walther@60471
|
968 |
"~~~~~ ~~~ fun associate_input' , args:"; val (ctxt, sel, ts, ((id, vat, sel', d, ts') :: oris)) = (ctxt, sel, ts, ori);
|
walther@60010
|
969 |
|
Walther@60471
|
970 |
(*+/---------------- bypass recursion of associate_input' ----------------\*)
|
Walther@60655
|
971 |
(*+*)O_Model.to_string @{context} oris = "[\n" ^
|
walther@60010
|
972 |
"(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
|
walther@60010
|
973 |
"(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
|
walther@60010
|
974 |
"(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
|
walther@60010
|
975 |
"(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]";
|
walther@60010
|
976 |
(*+*)val (id, vat, sel', d, ts') = nth 3 oris; (* 3rd iteration *)
|
Walther@60471
|
977 |
(*+\---------------- bypass recursion of associate_input' ----------------/*)
|
walther@60010
|
978 |
|
walther@60010
|
979 |
(*if*) sel = sel' andalso (inter op = ts ts') <> [] (*else*);
|
walther@60010
|
980 |
|
Walther@60471
|
981 |
(*/------------------- check within associate_input' -------------------------------\*)
|
walther@60010
|
982 |
(*+*)if sel = "#Given" andalso sel' = "#Given"
|
Walther@60471
|
983 |
(*+*)then () else error "associate_input' Model_Pattern CHANGED";
|
walther@60154
|
984 |
(*BUT: m_field can change from root-Problem to sub-MethodC --------------------vvv*)
|
walther@60010
|
985 |
(* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
|
Walther@60655
|
986 |
(*+*)if (Problem.from_store ctxt ["vonBelastungZu", "Biegelinien"] |> #model |> Model_Pattern.to_string @{context}) = "[\"" ^
|
walther@60010
|
987 |
"(#Given, (Streckenlast, q_q))\", \"" ^
|
walther@60010
|
988 |
"(#Given, (FunktionsVariable, v_v))\", \"" ^
|
walther@60010
|
989 |
"(#Find, (Funktionen, funs'''))\"]"
|
Walther@60471
|
990 |
(*+*)then () else error "associate_input' Model_Pattern of Subproblem CHANGED";
|
walther@60242
|
991 |
(* root-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv ------------------------------------- \<up> *)
|
Walther@60655
|
992 |
(*+*)if (Problem.from_store ctxt ["Biegelinien"] |> #model |> Model_Pattern.to_string @{context}) = "[\"" ^
|
walther@60010
|
993 |
"(#Given, (Traegerlaenge, l_l))\", \"" ^
|
walther@60010
|
994 |
"(#Given, (Streckenlast, q_q))\", \"" ^
|
walther@60242
|
995 |
"(#Find, (Biegelinie, b_b))\", \"" ^ (*------------------------------------- \<up> *)
|
walther@60010
|
996 |
"(#Relate, (Randbedingungen, r_b))\"]"
|
Walther@60471
|
997 |
(*+*)then () else error "associate_input' Model_Pattern root-problem CHANGED";
|
walther@60010
|
998 |
(* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
|
Walther@60655
|
999 |
(*+*)if (MethodC.from_store ctxt ["Biegelinien", "ausBelastung"] |> #model |> Model_Pattern.to_string @{context}) = "[\"" ^
|
walther@60010
|
1000 |
"(#Given, (Streckenlast, q__q))\", \"" ^
|
walther@60010
|
1001 |
"(#Given, (FunktionsVariable, v_v))\", \"" ^
|
Walther@60736
|
1002 |
"(#Given, (Biegelinie, b_b))\", \"" ^
|
walther@60023
|
1003 |
"(#Given, (AbleitungBiegelinie, id_der))\", \"" ^
|
Walther@60736
|
1004 |
"(#Given, (Biegemoment, id_momentum))\", \"" ^
|
Walther@60736
|
1005 |
"(#Given, (Querkraft, id_lat_force))\", \"" ^
|
walther@60010
|
1006 |
"(#Find, (Funktionen, fun_s))\"]"
|
Walther@60471
|
1007 |
(*+*)then () else error "associate_input' Model_Pattern CHANGED";
|
Walther@60675
|
1008 |
(*+*)if UnparseC.term @{context} d = "Biegelinie" andalso UnparseC.terms @{context} ts = "[y]"
|
Walther@60675
|
1009 |
(*+*) andalso UnparseC.terms @{context} ts' = "[y]"
|
walther@60010
|
1010 |
(*+*)then
|
walther@60010
|
1011 |
(*+*) (case (inter op = ts ts') of [Free ("y", _(*"real \<Rightarrow> real"*))] => ()
|
Walther@60471
|
1012 |
(*+*) | _ => error "check within associate_input' CHANGED 1")
|
Walther@60471
|
1013 |
(*+*)else error "check within associate_input' CHANGED 2";
|
Walther@60471
|
1014 |
(*\------------------- check within associate_input' -------------------------------/*)
|
walther@60010
|
1015 |
|
Walther@60736
|
1016 |
(*|------------------- contine me_Specify_Method_ausBelastung --------------------------------*)
|
Walther@60736
|
1017 |
(*\------------------- step into me_Specify_Method_ausBelastung ----------------------------//*)
|
Walther@60736
|
1018 |
(*[1], Met*)val (p,_,f,nxt,_,pt) = return_me_Specify_Method_ausBelastung;
|
Walther@60736
|
1019 |
val Add_Given "Biegelinie y" = nxt
|
Walther@60736
|
1020 |
|
Walther@60736
|
1021 |
(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy"= nxt
|
Walther@60736
|
1022 |
(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Biegemoment M_b" = nxt
|
Walther@60736
|
1023 |
(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Querkraft Q" = nxt
|
Walther@60736
|
1024 |
(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Biegelinien", "ausBelastung"] = nxt
|
Walther@60736
|
1025 |
|
Walther@60729
|
1026 |
(*[1, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("sym_neg_equal_iff_equal", _)= nxt
|
Walther@60729
|
1027 |
(*[1, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("Belastung_Querkraft", _)= nxt
|
Walther@60729
|
1028 |
(*[1, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["named", "integrate", "function"])= nxt
|
Walther@60729
|
1029 |
(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Model_Problem= nxt
|
Walther@60729
|
1030 |
(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "functionTerm (- q_0)"= nxt
|
Walther@60729
|
1031 |
(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "integrateBy x"= nxt
|
Walther@60729
|
1032 |
;
|
walther@60010
|
1033 |
(*/------------------- check result of Add_Given "functionTerm (- q_0)" --------------------\*)
|
walther@60010
|
1034 |
if p = ([1, 3], Pbl) andalso
|
walther@60010
|
1035 |
f = Test_Out.PpcKF (Test_Out.Problem [], {Find = [Incompl "antiDerivativeName"],
|
Walther@60729
|
1036 |
Given = [Correct "functionTerm (- q_0)", Incompl "integrateBy"],
|
walther@60010
|
1037 |
Relate = [], Where = [], With = []})
|
walther@60010
|
1038 |
then
|
walther@60010
|
1039 |
(case nxt of Add_Given "integrateBy x" => () | _ => error "specify-phase: low level CHANGED 1")
|
walther@60010
|
1040 |
else error "specify-phase: low level CHANGED 2";
|
walther@60010
|
1041 |
(*\------------------- check result of Add_Given "functionTerm (- q_0)" --------------------/*)
|
walther@60010
|
1042 |
|