1 (* Title: Interpret/li-tool.sml
2 Author: Walther Neuper 050908
3 (c) copyright due to lincense terms.
5 "-----------------------------------------------------------------";
6 "table of contents -----------------------------------------------";
7 "-----------------------------------------------------------------";
8 "----------- fun implicit_take, fun get_first_argument -------------------------";
9 "----------- fun from_prog ---------------------------------------";
10 "----------- fun specific_from_prog ----------------------------";
11 "----------- fun de_esc_underscore -------------------------------";
12 "----------- fun go ----------------------------------------------";
13 "----------- fun formal_args -------------------------------------";
14 "----------- fun dsc_valT ----------------------------------------";
15 "----------- fun arguments_from_model ---------------------------------------";
16 "----------- fun init_pstate -----------------------------------------------------------------";
17 "-----------------------------------------------------------------";
18 "-----------------------------------------------------------------";
19 "-----------------------------------------------------------------";
21 val thy = @{theory Isac_Knowledge};
23 "----------- fun implicit_take, fun get_first_argument -------------------------";
24 "----------- fun implicit_take, fun get_first_argument -------------------------";
25 "----------- fun implicit_take, fun get_first_argument -------------------------";
26 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
27 val (dI',pI',mI') = ("Test",["sqroot-test", "univariate", "equation", "test"],
28 ["Test", "squ-equ-test-subpbl1"]);
29 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
30 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
31 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
32 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
33 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
34 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
35 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
36 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
37 "~~~~~ fun me, args:"; val tac = nxt;
38 "~~~~~ fun Step.by_tactic, args:"; val ptp as (pt, p) = (pt, p);
39 val Applicable.Yes m = Step.check tac (pt, p);
40 (*if*) Tactic.for_specify' m; (*false*)
41 "~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = (m, ptp);
42 "~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,ctxt), pos as (p,_))
44 val {prog_rls, ...} = MethodC.from_store ctxt mI;
45 val PblObj {meth=itms, ...} = get_obj I pt p;
46 val thy' = get_obj g_domID pt p;
47 val thy = ThyC.get_theory @{context} thy';
48 val prog_rls = LItool.get_simplifier (pt, pos)
49 val (is as Pstate {env, ...}, ctxt, sc) = init_pstate ctxt (I_Model.OLD_to_TEST itms) mI;
50 val ini = implicit_take @{context} sc env;
51 "----- fun implicit_take, args:"; val (Prog sc) = sc;
52 "----- fun get_first_argument, args:"; val (y, h $ body) = (thy, sc);
53 case get_first_argument sc of SOME (Free ("e_e", _)) => ()
54 | _ => error "script: Const (?, ?) in script (as term) changed";;
56 "----------- fun from_prog ---------------------------------------";
57 "----------- fun from_prog ---------------------------------------";
58 "----------- fun from_prog ---------------------------------------";
59 (* compare test/../interface.sml
60 "--------- getTactic, fetchApplicableTactics ------------";
63 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
64 ("Test", ["sqroot-test", "univariate", "equation", "test"],
65 ["Test", "squ-equ-test-subpbl1"]))];
68 autoCalculate 1 CompleteCalc;
69 val ((pt,_),_) = States.get_calc 1;
72 (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
73 val tacs = from_prog pt ([],Pbl);
74 case tacs of [Apply_Method ["Test", "squ-equ-test-subpbl1"]] => ()
75 | _ => error "script.sml: diff.behav. in from_prog ([],Pbl)";
77 val tacs = from_prog pt ([1],Res);
78 case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
79 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
80 Check_elementwise "Assumptions"] => ()
81 | _ => error "script.sml: diff.behav. in from_prog ([1],Res)";
83 val tacs = from_prog pt ([3],Pbl);
84 case tacs of [Apply_Method ["Test", "solve_linear"]] => ()
85 | _ => error "script.sml: diff.behav. in from_prog ([3],Pbl)";
87 val tacs = from_prog pt ([3,1],Res);
88 case tacs of [Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), Rewrite_Set "Test_simplify"] => ()
89 | _ => error "script.sml: diff.behav. in from_prog ([3,1],Res)";
91 val tacs = from_prog pt ([3],Res);
92 case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
93 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
94 Check_elementwise "Assumptions"] => ()
95 | _ => error "script.sml: diff.behav. in from_prog ([3],Res)";
97 val tacs = (from_prog pt ([],Res)) handle PTREE str => [Tac str];
98 case tacs of [Tac "no tactics applicable at the end of a calculation"] => ()
99 | _ => error "script.sml: diff.behav. in from_prog ([],Res)";
101 "----------- fun specific_from_prog ----------------------------";
102 "----------- fun specific_from_prog ----------------------------";
103 "----------- fun specific_from_prog ----------------------------";
105 CalcTree @{context} [(["equality (x+1=(2::real))", "solveFor x", "solutions L"],
106 ("Test", ["sqroot-test", "univariate", "equation", "test"],
107 ["Test", "squ-equ-test-subpbl1"]))];
110 autoCalculate 1 CompleteCalc;
112 (*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)
113 fetchApplicableTactics 1 99999 ([],Pbl);
115 fetchApplicableTactics 1 99999 ([1],Res);
116 "~~~~~ fun fetchApplicableTactics, args:"; val (cI, (scope:int), (p:pos')) = (1, 99999, ([1],Res));
117 val ((pt, _), _) = States.get_calc cI;
119 case from_prog pt p of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",
120 Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),
121 Check_elementwise "Assumptions"] => ()
122 | _ => error "fetchApplicableTactics ([1],Res) changed";
125 specific_from_prog pt p;
127 ### Tactic.applicable: not impl. for tac='Subproblem(Test,["LINEAR", "univariate", "equation", "test"])'
128 ### Tactic.applicable: not impl. for tac = 'Check_elementwise "Assumptions"'
131 "~~~~~ fun specific_from_prog , args:"; val (pt, pos as (p, p_)) = (pt, p);
132 (*if*) Pos.on_specification (p, p_) (*else*);
133 val pp = par_pblobj pt p
134 val thy' = (get_obj g_domID pt pp):ThyC.id
135 val thy = ThyC.get_theory @{context} thy'
136 val metID = get_obj g_metID pt pp
138 if metID = MethodC.id_empty
139 then (thd3 o snd3) (get_obj g_origin pt pp)
141 val {program=Prog sc,prog_rls,asm_rls,rew_ord=ro,...} = MethodC.from_store ctxt metID'
142 val Pstate ist = get_istate_LI pt (p,p_)
143 val ctxt = get_ctxt pt (p, p_)
144 val alltacs = (*we expect at least 1 stac in a script*)
145 map ((LItool.tac_from_prog (pt, pos)) o rep_stacexpr o #1 o
146 (check_leaf "selrul" ctxt prog_rls (get_subst ist) )) (stacpbls sc)
148 (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
150 (*WN120611 stopped and took version 1 again for fetchApplicableTactics !
151 (distinct op = o flat o (map (Tactic.applicable thy ro asm_rls f))) alltacs
153 ### Tactic.applicable: not impl. for tac='Subproblem(Test,["LINEAR", "univariate", "equation", "test"])'
154 ### Tactic.applicable: not impl. for tac = 'Check_elementwise "Assumptions"'
157 "----------- fun de_esc_underscore -------------------------------";
158 "----------- fun de_esc_underscore -------------------------------";
159 "----------- fun de_esc_underscore -------------------------------";
161 > val str = "Rewrite_Set_Inst";
162 > val esc = esc_underscore str;
163 val it = "Rewrite_Set_Inst" : string
164 > val des = de_esc_underscore esc;
165 val des = de_esc_underscore esc;*)
167 "----------- fun go ----------------------------------------------";
168 "----------- fun go ----------------------------------------------";
169 "----------- fun go ----------------------------------------------";
171 > val t = (Thm.term_of o the o (TermC.parse thy)) "a+b";
172 val it = Const (#,#) $ Free (#,#) $ Free ("b", "RealDef.real") : term
173 > val plus_a = TermC.sub_at [L] t;
174 > val b = TermC.sub_at [R] t;
175 > val plus = TermC.sub_at [L,L] t;
176 > val a = TermC.sub_at [L,R] t;
178 > val t = (Thm.term_of o the o (TermC.parse thy)) "a+b+c";
179 val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c", "RealDef.real") : term
180 > val pl_pl_a_b = TermC.sub_at [L] t;
181 > val c = TermC.sub_at [R] t;
182 > val a = TermC.sub_at [L,R,L,R] t;
183 > val b = TermC.sub_at [L,R,R] t;
186 "----------- fun formal_args -------------------------------------";
187 "----------- fun formal_args -------------------------------------";
188 "----------- fun formal_args -------------------------------------";
190 > formal_args program;
191 [Free ("f_", "RealDef.real"),Free ("v_", "RealDef.real"),
192 Free ("eqs_", "bool List.list")] : term list
194 "----------- fun dsc_valT ----------------------------------------";
195 "----------- fun dsc_valT ----------------------------------------";
196 "----------- fun dsc_valT ----------------------------------------";
197 (*> val t = (Thm.term_of o the o (TermC.parse thy)) "equality";
199 val T = "bool => Tools.una" : typ
200 > val dsc = dsc_valT t;
201 val dsc = "una" : string
203 > val t = (Thm.term_of o the o (TermC.parse thy)) "fixedValues";
205 val T = "bool List.list => Tools.nam" : typ
206 > val dsc = dsc_valT t;
207 val dsc = "nam" : string*)
208 "----------- fun arguments_from_model ---------------------------------------";
209 "----------- fun arguments_from_model ---------------------------------------";
210 "----------- fun arguments_from_model ---------------------------------------";
212 > val sc = ... Solve_root_equation ...
213 > val mI = ("Program", "sqrt-equ-test");
214 > val PblObj{meth={model=itms,...},...} = get_obj I pt [];
215 > val ts = arguments_from_model thy mI itms;
216 > map (UnparseC.term_in_thy thy) ts;
217 ["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)", "x", "#0"] : string list
220 "----------- fun init_pstate -----------------------------------------------------------------";
221 "----------- fun init_pstate -----------------------------------------------------------------";
222 "----------- fun init_pstate -----------------------------------------------------------------";
224 This test is deeply nested (down into details of creating environments).
225 In order to make Sidekick show the structure add to each
226 * (*/...\*) and (*\.../*)
227 * a companion > ML < (*/...\*) and > ML < (*\.../*)
228 Note the wrong ^----^ delimiters.
230 val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
231 "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
232 "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
233 "AbleitungBiegelinie dy"];
234 val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
235 ["IntegrierenUndKonstanteBestimmen2"]);
236 val p = e_pos'; val c = [];
237 (*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; val Model_Problem = nxt
238 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Traegerlaenge L" = nxt
239 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Streckenlast q_0" = nxt
240 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Biegelinie y" = nxt
241 (*/---broken elementwise input to lists---\* )
242 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
243 (*isa* ) val Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" = nxt
244 ( *isa2*) val Add_Relation "Randbedingungen [y 0 = 0]" = nxt
245 (*[], 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]"*)
246 (*isa*) val Specify_Theory "Biegelinie" = nxt
247 (*isa2* ) val Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]" = nxt( **)
248 ( *\---broken elementwise input to lists---/*)
249 (*[], 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
250 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Biegelinie" = nxt
251 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["Biegelinien"] = nxt
252 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
253 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "FunktionsVariable x" = nxt
254 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]" = nxt
255 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy" = nxt
257 (*[], Met*)val return_Add_Given_AbleitungBieg
259 (*/------------------- step into me_Add_Given_AbleitungBieg --------------------------------\\*)
261 "~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
262 val ctxt = Ctree.get_ctxt pt p
263 val ("ok", (_, _, ptp as (pt, p))) =
264 (*case*) Step.by_tactic tac (pt, p) (*of*);
267 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
268 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
269 (p, ((pt, Pos.e_pos'), []) );
270 (*if*) Pos.on_calc_end ip (*else*);
271 val (_, probl_id, _) = Calc.references (pt, p);
273 (*case*) tacis (*of*);
274 (*if*) probl_id = Problem.id_empty (*else*);
276 switch_specify_solve p_ (pt, ip);
277 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
278 (*if*) Pos.on_specification ([], state_pos) (*then*);
280 specify_do_next (pt, input_pos);
281 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
282 val (_, (p_', tac)) = Specify.find_next_step ptp
283 val ist_ctxt = Ctree.get_loc pt (p, p_)
284 val Tactic.Apply_Method mI =
287 LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
288 ist_ctxt (pt, (p, p_'));
289 "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
290 ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));
291 val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
292 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
293 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
294 val {model, ...} = MethodC.from_store ctxt mI;
295 val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
297 (*+*)if (itms |> I_Model.to_string @{context}) = "[\n" ^
298 "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
299 "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
300 "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
301 "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]])), \n" ^
302 "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(fun_var, [x])), \n" ^
303 "(6 ,[1] ,true ,#Given ,Cor GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]])), \n" ^
304 "(7 ,[1] ,true ,#Given ,Cor AbleitungBiegelinie dy ,(id_der, [dy]))]"
305 (*+*)then () else error "init_pstate: initial i_model changed";
306 (*+*)if (itms |> I_Model.penv_to_string @{context}) = "[" ^ (*to be eliminated*)
307 (*1*)"(l_l, [L]), " ^
308 (*2*)"(q_q, [q_0]), " ^
309 (*3*)"(b_b, [y]), " ^
310 (*4*)"(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]), " ^
311 (*5*)"(fun_var, [x]), " ^
312 (*6*)"(vs, [[c, c_2, c_3, c_4]]), " ^
313 (*7*)"(id_der, [dy])]"
314 (*+*)then () else error "init_pstate: initial penv changed";
317 LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI (*of*);
318 (*//------------------ step into init_pstate -----------------------------------------------\\*)
319 "~~~~~ fun init_pstate , args:"; val (ctxt, i_model, met_id) = (ctxt, (I_Model.OLD_to_TEST itms), mI);
320 val (model_patt, program, prog, prog_rls, where_, where_rls) =
321 case MethodC.from_store ctxt met_id of
322 {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...}=>
323 (model_patt, program, prog, prog_rls, where_, where_rls)
325 val return_of_max_variant =
326 of_max_variant model_patt i_model;
327 (*///----------------- step into of_max_variant --------------------------------------------\\*)
328 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
330 map (fn (_, variants, _, _, _) => variants) i_model
333 val variants_separated = map (filter_variants' i_model) all_variants
334 val sums_corr = map (cnt_corrects) variants_separated
335 val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
336 val (_, max_variant) = hd (*..crude decision, up to improvement *)
337 (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
339 filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
340 val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
342 (*+*)if (equal_descr_pairs |> descr_pairs_to_string @{context}) = "[" ^
343 (*defined: in program+model--vvvv--,----------------------------------------- in problem ---vvv*)
344 "((#Given, (Traegerlaenge, l_l)), (1, [1], true ,#Given, " ^ "(Cor_TEST Traegerlaenge L ,(l_l, [L]), Position.T))), " ^
345 (*-------------------------------------------------------------------------------------penv-^^^^^^^^^ DROP!*)
346 "((#Given, (Streckenlast, q_q)), (2, [1], true ,#Given, " ^
347 "(Cor_TEST Streckenlast q_0 ,(q_q, [q_0]), Position.T))), " ^
348 "((#Given, (FunktionsVariable, fun_var)), (5, [1], true ,#Given, " ^
349 "(Cor_TEST FunktionsVariable x ,(fun_var, [x]), Position.T))), " ^
350 "((#Given, (GleichungsVariablen, vs)), (6, [1], true ,#Given, " ^
351 "(Cor_TEST GleichungsVariablen [c, c_2, c_3, c_4] ,(vs, [[c, c_2, c_3, c_4]]), Position.T))), " ^
352 "((#Given, (AbleitungBiegelinie, id_der)), (7, [1], true ,#Given, " ^
353 "(Cor_TEST AbleitungBiegelinie dy ,(id_der, [dy]), Position.T))), " ^
354 "((#Find, (Biegelinie, b_b)), (3, [1], true ,#Find, (Cor_TEST Biegelinie y ,(b_b, [y]), Position.T))), " ^
355 (*-----------------------------------------------------------------------penv-^^^^^^^^^ DROP!*)
356 "((#Relate, (Randbedingungen, r_b)), (4, [1], true ,#Relate, " ^
357 "(Cor_TEST Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] ,(r_b, [[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]), Position.T)))]"
358 (*-----------------------------------------------------------------penv-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ DROP!*)
359 then () else error "of_max_variant: equal_descr_pairs CHANGED";
361 val return_make_env_model = make_env_model equal_descr_pairs;
362 (*////---------------- step into make_env_model --------------------------------------------\\*)
363 "~~~~~ fun make_env_model , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
364 "~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 4 equal_descr_pairs;
365 "~~~~~ fun mk_env_model , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb);
367 handle_lists id (descr, ts);
368 "~~~~~ fun handle_lists , args:"; val (id, (descr, ts)) = (id, (descr, ts));
369 (*+*)val xxx = ts |> UnparseC.terms @{context};
370 (*if*) Model_Pattern.is_list_descr descr (*then*);
371 (*if*) length ts > 1 (*then*);
372 (*if*) TermC.is_list (hd ts) (*then*);
373 val return_handle_lists_step =
374 [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) (map TermC.the_single ts))]
375 (*+*)val "[\"\n(vs, [c, c_2, c_3, c_4])\"]"
376 = return_handle_lists_step |> Subst.to_string @{context}
377 (*\\\\---------------- step into make_env_model --------------------------------------------//*)
378 val env_model = return_make_env_model
379 (*+*)val "[\"\n(l_l, L)\", \"\n(q_q, q_0)\", \"\n(fun_var, x)\", \"\n(vs, [c, c_2, c_3, c_4])\", \"\n(id_der, dy)\", \"\n(b_b, y)\", \"\n(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\"]"
380 = env_model |> Subst.to_string @{context}
382 (*|||----------------- contine of_max_variant ------------------------------------------------*)
383 val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
384 val subst_eval_list = make_envs_preconds equal_givens
385 val (env_subst, env_eval) = split_list subst_eval_list
386 val return_of_max_variant_step = (i_model_max, env_model, (env_subst, env_eval));
388 (*+*)if return_of_max_variant_step = return_of_max_variant then () else error "<>";
389 (*\\\----------------- step into of_max_variant --------------------------------------------//*)
390 val (_, env_model, (env_subst, env_eval)) = return_of_max_variant
392 (*|------------------- contine init_pstate ---------------------------------------------------*)
393 val actuals = map snd env_model
394 (*+*) val "[L, q_0, x, [c, c_2, c_3, c_4], dy, y, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]]"
395 = actuals |> UnparseC.terms @{context}
397 val formals = Program.formal_args prog
398 (*+*)val "[l_l, q_q, fun_var, b_b, r_b, vs, id_der]"
399 = formals |> UnparseC.terms @{context}
400 (*+*)val 7 = length formals
403 Pre_Conds.check_envs_TEST ctxt where_rls where_ (env_model, (env_subst, env_eval))
404 val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));
405 val ist = Istate.e_pstate
406 |> Istate.set_eval prog_rls
407 |> Istate.set_env_true (relate_args [] formals actuals ctxt prog met_id formals actuals)
409 (*+*)(relate_args [] formals actuals ctxt prog met_id formals actuals)
411 val return_init_pstate = (Istate.Pstate ist, ctxt, program)
412 (*\\------------------ step into init_pstate -----------------------------------------------//*)
413 (*\------------------- step into me_Add_Given_AbleitungBieg --------------------------------//*)
414 val (p,_,f,nxt,_,pt) = return_Add_Given_AbleitungBieg;
415 val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
416 (* final test ... ----------------------------------------------------------------------------*)
417 (*+*)val ([], Met) = p
418 (*+*)val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt