1.1 --- a/test/Tools/isac/Test_Isac.thy Wed Sep 27 12:17:44 2023 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Oct 02 12:02:59 2023 +0200
1.3 @@ -277,939 +277,6 @@
1.4 ML_file "Specify/cas-command.sml"
1.5 ML_file "Specify/p-spec.sml"
1.6 ML_file "Specify/specify.sml"
1.7 -ML \<open>
1.8 -\<close> ML \<open>
1.9 -(* Title: "Specify/specify.sml"
1.10 - Author: Walther Neuper
1.11 - (c) due to copyright terms
1.12 -*)
1.13 -
1.14 -"-----------------------------------------------------------------------------------------------";
1.15 -"table of contents -----------------------------------------------------------------------------";
1.16 -"-----------------------------------------------------------------------------------------------";
1.17 -"-----------------------------------------------------------------------------------------------";
1.18 -"----------- maximum-example: Specify.finish_phase ---------------------------------------------";
1.19 -"----------- revise Specify.do_all -------------------------------------------------------------";
1.20 -"----------- specify-phase: low level functions ------------------------------------------------";
1.21 -"-----------------------------------------------------------------------------------------------";
1.22 -"-----------------------------------------------------------------------------------------------";
1.23 -"-----------------------------------------------------------------------------------------------";
1.24 -open Pos;
1.25 -open Ctree;
1.26 -open Test_Code;
1.27 -open Tactic;
1.28 -open Specify;
1.29 -open Step;
1.30 -
1.31 -open O_Model;
1.32 -open I_Model;
1.33 -open P_Model;
1.34 -open Specify_Step;
1.35 -open Test_Code;
1.36 -
1.37 -(**** maximum-example: Specify.finish_phase ############################################# ****)
1.38 -"----------- maximum-example: Specify.finish_phase ---------------------------------------------";
1.39 -"----------- maximum-example: Specify.finish_phase ---------------------------------------------";
1.40 -(*//-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --\\* )
1.41 - val (p,_,f,nxt,_,pt) =
1.42 - Test_Code.init_calc @{context}
1.43 - [(["fixedValues [r=Arbfix]", "maximum A",
1.44 - "valuesFor [a,b]",
1.45 - "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
1.46 - "relations [A=a*b, (a/2) \<up> 2 + (b/2) \<up> 2 = r \<up> 2]",
1.47 - "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
1.48 -
1.49 - "boundVariable a", "boundVariable b", "boundVariable alpha",
1.50 - "interval {x::real. 0 <= x & x <= 2*r}",
1.51 - "interval {x::real. 0 <= x & x <= 2*r}",
1.52 - "interval {x::real. 0 <= x & x <= pi}",
1.53 - "errorBound (eps=(0::real))"],
1.54 - ("Diff_App",["maximum_of", "function"],["Diff_App", "max_by_calculus"])
1.55 - )];
1.56 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.57 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.58 - val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.59 - (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)
1.60 - val pits = get_obj g_pbl pt (fst p);
1.61 - writeln (I_Model.to_string ctxt pits);
1.62 -(*[
1.63 -(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
1.64 -(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),
1.65 -(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
1.66 -(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)
1.67 - val (pt,p) = Specify.finish_phase (pt,p);
1.68 - val pits = get_obj g_pbl pt (fst p);
1.69 - if I_Model.to_string ctxt pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(rs_, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]"
1.70 - then () else error "completetest.sml: new behav. in Specify.finish_phase 3";
1.71 - writeln (I_Model.to_string ctxt pits);
1.72 -(*[
1.73 -(1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
1.74 -(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
1.75 -(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
1.76 -(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up>
1.77 -2 = r \<up> 2] ,(relations, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]]))]*)
1.78 - val mits = get_obj g_met pt (fst p);
1.79 - if I_Model.to_string ctxt mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] ,(rs_, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]"
1.80 - then () else error "completetest.sml: new behav. in Specify.finish_phase 3";
1.81 - writeln (I_Model.to_string ctxt mits);
1.82 -(*[
1.83 -(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
1.84 -(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
1.85 -(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
1.86 -(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up>
1.87 -2 = r \<up> 2] ,(relations, [[A = a * b],[(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]])),
1.88 -(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
1.89 -(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
1.90 -0 <= x & x <= 2 * r}])),
1.91 -(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
1.92 -( *\\-------- WAS OUT OF Test UNTIL 200209, ERROR PROBABLY FROM INTRO. OF Isabelle's funpack --//*)
1.93 -
1.94 -
1.95 -(**** revise Specify.do_all ############################################################## ****);
1.96 -"----------- revise Specify.do_all -------------------------------------------------------------";
1.97 -"----------- revise Specify.do_all -------------------------------------------------------------";
1.98 -(* from Minisubplb/100-init-rootpbl.sml:
1.99 -val (_(*example text*),
1.100 - (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
1.101 - "Extremum (A = 2 * u * v - u \<up> 2)" ::
1.102 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
1.103 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
1.104 - "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
1.105 - "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
1.106 - "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
1.107 - "ErrorBound (\<epsilon> = (0::real))" :: []),
1.108 - refs as ("Diff_App",
1.109 - ["univariate_calculus", "Optimisation"],
1.110 - ["Optimisation", "by_univariate_calculus"])))
1.111 - = Store.get (Know_Store.get_expls @ {theory Know_Store}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
1.112 -*)
1.113 -val model = ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
1.114 - "Extremum (A = 2 * u * v - u \<up> 2)" ::
1.115 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
1.116 - "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
1.117 - "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
1.118 - "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
1.119 - "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
1.120 - "ErrorBound (\<epsilon> = (0::real))" :: [])
1.121 -val refs = ("Diff_App",
1.122 - ["univariate_calculus", "Optimisation"],
1.123 - ["Optimisation", "by_univariate_calculus"])
1.124 -
1.125 -val (p,_,f,nxt,_,pt) =
1.126 - Test_Code.init_calc @{context} [(model, refs)];
1.127 -"~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))])
1.128 - = (@{context}, [(model, refs)]);
1.129 -
1.130 - Specify.do_all (pt, p);
1.131 -(*//------------------ step into do_all ----------------------------------------------------\\*)
1.132 -"~~~~~ fun do_all , args:"; val (pt, (*old* )pos as( *old*) (p, _)) = (pt, p);
1.133 - val (itms, oris, probl, o_refs, spec, ctxt) = case Ctree.get_obj I pt p of
1.134 - Ctree.PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ctxt, ...}
1.135 - => (itms, oris, probl, o_spec, spec, ctxt)
1.136 - | _ => raise ERROR "LI.by_tactic: no PblObj"
1.137 - val (_, pbl_id', met_id') = References.select_input o_refs spec
1.138 - val {model = pbl_patt, ...} = Problem.from_store ctxt pbl_id';
1.139 - val {model = met_patt, ...} = MethodC.from_store ctxt met_id';
1.140 - val (pbl_imod, met_imod) = I_Model.s_make_complete oris
1.141 - (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
1.142 -;
1.143 -(*-------------------- stop step into do_all -------------------------------------------------*)
1.144 -(*/------------------- check result of I_Model.complete' ------------------------------------\*)
1.145 -\<close> ML \<open>
1.146 -(*+*)if Model_Pattern.to_string @{context} met_patt = "[\"" ^
1.147 - "(#Given, (Constants, fixes))\", \"" ^
1.148 - "(#Given, (Maximum, maxx))\", \"" ^
1.149 - "(#Given, (Extremum, extr))\", \"" ^
1.150 - "(#Given, (SideConditions, sideconds))\", \"" ^
1.151 - "(#Given, (FunctionVariable, funvar))\", \"" ^
1.152 - "(#Given, (Input_Descript.Domain, doma))\", \"" ^
1.153 - "(#Given, (ErrorBound, err))\", \"" ^
1.154 - "(#Find, (AdditionalValues, vals))\"]"
1.155 -(*+*)then () else error "mod_pat CHANGED";
1.156 -\<close> ML \<open>
1.157 -(*+*)if I_Model.to_string_TEST @{context} met_imod = "[\n" ^
1.158 - "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
1.159 - "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
1.160 - "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
1.161 - "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
1.162 - "(7, [1], true ,#undef, (Cor_TEST FunctionVariable a , pen2str, Position.T)), \n" ^
1.163 - "(10, [1, 2], true ,#undef, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
1.164 - "(12, [1, 2, 3], true ,#undef, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
1.165 - "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
1.166 -(*+*)then () else error "met_imod CHANGED";
1.167 -(*\------------------- check result of I_Model.complete' ------------------------------------/*)
1.168 -(*\\------------------ step into do_all ----------------------------------------------------//*)
1.169 -
1.170 -\<close> ML \<open>
1.171 -(*-------------------- continuing do_all -----------------------------------------------------*)
1.172 - val (pt, _) = Ctree.cupdate_problem pt p
1.173 - (o_refs, I_Model.TEST_to_OLD pbl_imod, I_Model.TEST_to_OLD met_imod, ctxt)
1.174 -;
1.175 -
1.176 -
1.177 -
1.178 -\<close> ML \<open>
1.179 -(**** specify-phase: low level functions ################################################# ****)
1.180 -"----------- specify-phase: low level functions -----------------------------------------";
1.181 -"----------- specify-phase: low level functions -----------------------------------------";
1.182 -open Pos;
1.183 -open Ctree;
1.184 -open Test_Code;
1.185 -open Tactic;
1.186 -open Specify;
1.187 -open Step;
1.188 -
1.189 -open O_Model;
1.190 -open I_Model;
1.191 -open P_Model;
1.192 -open Specify_Step;
1.193 -
1.194 -val formalise = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
1.195 - "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
1.196 -(*
1.197 - Now follow items for ALL SubProblems,
1.198 - since ROOT MethodC must provide values for "actuals" of ALL SubProblems.
1.199 - See Biegelinie.thy subsection \<open>Survey on Methods\<close>.
1.200 -*)
1.201 -(*
1.202 - Items for MethodC "IntegrierenUndKonstanteBestimmen2"
1.203 -*)
1.204 - "FunktionsVariable x",
1.205 - (*"Biegelinie y", ..already input for Problem above*)
1.206 - "AbleitungBiegelinie dy",
1.207 - "Biegemoment M_b",
1.208 - "Querkraft Q",
1.209 -(*
1.210 - Item for Problem "LINEAR/system", which by [''no_met''] involves refinement
1.211 -*)
1.212 - "GleichungsVariablen [c, c_2, c_3, c_4]"
1.213 -];
1.214 -(*
1.215 - Note: the above sequence of items follows the sequence of formal arguments (and of model items)
1.216 - of MethodC "IntegrierenUndKonstanteBestimmen2"
1.217 -*)
1.218 -val references = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
1.219 -val p = e_pos'; val c = [];
1.220 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(formalise, references)]; (*nxt = Model_Problem*)
1.221 -
1.222 -(*/------------------- check result of Test_Code.init_calc @{context} ----------------------------------------\*)
1.223 -(*+*)val (o_model, ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]), _) =
1.224 - get_obj g_origin pt (fst p);
1.225 -(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
1.226 - "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
1.227 - "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
1.228 - "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
1.229 - "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
1.230 - "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
1.231 - "(6, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"]), \n" ^
1.232 - "(7, [\"1\"], #undef, Biegemoment, [\"M_b\"]), \n" ^
1.233 - "(8, [\"1\"], #undef, Querkraft, [\"Q\"]), \n" ^
1.234 - "(9, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"
1.235 -then () else error "[IntegrierenUndKonstanteBestimmen2] O_Model CHANGED";
1.236 -(*\------------------- check result of Test_Code.init_calc @{context} ----------------------------------------/*)
1.237 -
1.238 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Traegerlaenge L" = nxt
1.239 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Streckenlast q_0" = nxt
1.240 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Biegelinie y" = nxt
1.241 -(*[], 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
1.242 -(*/---broken elementwise input to lists---\* )
1.243 -(*[], 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]"*)
1.244 -( *\---broken elementwise input to lists---/*)
1.245 -
1.246 -val return_me_Add_Relation_Randbedingungen = me nxt p c pt; (*\<rightarrow>Specify_Problem ["Biegelinien"]*)
1.247 -(*/------------------- step into me_Add_Relation_Randbedingungen ---------------------------\\*)
1.248 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
1.249 - val ctxt = Ctree.get_ctxt pt p
1.250 - val (pt, p) =
1.251 - (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
1.252 - case Step.by_tactic tac (pt, p) of
1.253 - ("ok", (_, _, ptp)) => ptp
1.254 -
1.255 -val ("ok", ([(Specify_Theory "Biegelinie", _, _)], _, _)) =
1.256 - (*case*)
1.257 - Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
1.258 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
1.259 - (p, ((pt, Pos.e_pos'), []));
1.260 - (*if*) Pos.on_calc_end ip (*else*);
1.261 - val (_, probl_id, _) = Calc.references (pt, p);
1.262 -val _ =
1.263 - (*case*) tacis (*of*);
1.264 - (*if*) probl_id = Problem.id_empty (*else*);
1.265 -
1.266 -\<close> ML \<open>
1.267 - switch_specify_solve p_ (pt, ip);
1.268 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
1.269 - (*if*) Pos.on_specification ([], state_pos) (*then*);
1.270 -
1.271 - specify_do_next (pt, input_pos);
1.272 -"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
1.273 - val (_, (p_', tac)) = Specify.find_next_step ptp
1.274 - val ist_ctxt = Ctree.get_loc pt (p, p_)
1.275 -val Specify_Theory "Biegelinie" =
1.276 - (*case*) tac (*of*);
1.277 -
1.278 -Step_Specify.by_tactic_input tac (pt, (p, p_'));
1.279 -
1.280 -(*|------------------- contine me_Add_Relation_Randbedingungen -------------------------------*)
1.281 -(*\------------------- step into me_Add_Relation_Randbedingungen ---------------------------//*)
1.282 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = return_me_Add_Relation_Randbedingungen;
1.283 - val Specify_Theory "Biegelinie" = nxt
1.284 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Problem ["Biegelinien"] = nxt
1.285 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
1.286 -
1.287 -(*[], Met*)val return_me_Specify_Method_IntegrierenUndKonstanteBestimmen2
1.288 - = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)
1.289 -(*/------------------- step into me_Specify_Method_IntegrierenUndKonstanteBestimmen2--------\*)
1.290 -
1.291 -(*/------------------- initial check for whole me ------------------------------------------\*)
1.292 -(*+*)val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt;
1.293 -
1.294 -(*+*)val {origin = (o_model, o_refs, _), probl = i_pbl, meth = i_met, spec, ...} =
1.295 - Calc.specify_data (pt, p);
1.296 -(*+*)if o_refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])
1.297 -(*+*)then () else error "initial o_refs CHANGED";
1.298 -(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
1.299 - "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
1.300 - "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
1.301 - "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
1.302 - "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
1.303 - "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
1.304 - "(6, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"]), \n" ^
1.305 - "(7, [\"1\"], #undef, Biegemoment, [\"M_b\"]), \n" ^
1.306 - "(8, [\"1\"], #undef, Querkraft, [\"Q\"]), \n" ^
1.307 - "(9, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"
1.308 -(*+*)then () else error "initial o_model CHANGED";
1.309 -(*+*)if I_Model.to_string @{context} i_pbl = "[\n" ^
1.310 - "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
1.311 - "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
1.312 - "(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n" ^
1.313 - "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str)]"
1.314 -(*+*)then () else error "initial i_pbl CHANGED";
1.315 -(*+*)if I_Model.to_string @{context} i_met = "[]"
1.316 -(*+*)then () else error "initial i_met CHANGED";
1.317 -(*+*)val (_, ["Biegelinien"], _) = spec;
1.318 -(*\------------------- initial check for whole me ------------------------------------------/*)
1.319 -
1.320 -"~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
1.321 -(*/------------------- step into Step.by_tactic \\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\*)
1.322 - val (pt'''''_', p'''''_') = case
1.323 -
1.324 - Step.by_tactic tac (pt, p) of ("ok", (_, _, ptp)) => ptp;
1.325 -(*/------------------- check for entry to Step.by_tactic -----------------------------------\*)
1.326 -(*+*)val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = tac;
1.327 -(*+*)val {origin = (o_model, _, _), ...} = Calc.specify_data (pt, p);
1.328 -(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
1.329 - "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
1.330 - "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
1.331 - "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
1.332 - "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
1.333 - "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
1.334 - "(6, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"]), \n" ^
1.335 - "(7, [\"1\"], #undef, Biegemoment, [\"M_b\"]), \n" ^
1.336 - "(8, [\"1\"], #undef, Querkraft, [\"Q\"]), \n" ^
1.337 - "(9, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"])]"
1.338 -(*+*)then () else error "o_model AFTER Specify_Method NOTok CHANGED";
1.339 -(*\------------------- check for Step.by_tactic --------------------------------------------/*)
1.340 -"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
1.341 - val Applicable.Yes tac' = (*case*)
1.342 -
1.343 - Step.check tac (pt, p) (*of*);
1.344 -"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
1.345 - (*if*) Tactic.for_specify tac (*then*);
1.346 -
1.347 -Specify_Step.check tac (ctree, pos);
1.348 -"~~~~~ fun check , args:"; val ((Tactic.Specify_Method mID), (ctree, pos)) = (tac, (ctree, pos));
1.349 -
1.350 - val (o_model''''', _, i_model''''') =
1.351 - Specify_Step.complete_for mID (ctree, pos);
1.352 -"~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (mID, (ctree, pos));
1.353 - val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
1.354 - ...} = Calc.specify_data (ctree, pos);
1.355 - val (dI, _, _) = References.select_input o_refs refs;
1.356 - val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
1.357 - val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
1.358 - val (o_model', ctxt') =
1.359 -
1.360 - O_Model.complete_for m_patt root_model (o_model, ctxt);
1.361 -(*/------------------- check entry to O_Model.complete_for -----------------------------------------\*)
1.362 -(*+*)Model_Pattern.to_string @{context} m_patt = "[\"" ^
1.363 - "(#Given, (Traegerlaenge, l))\", \"" ^
1.364 - "(#Given, (Streckenlast, q))\", \"" ^
1.365 - "(#Given, (FunktionsVariable, v))\", \"" ^
1.366 - "(#Given, (GleichungsVariablen, vs))\", \"" ^
1.367 - "(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^
1.368 - "(#Find, (Biegelinie, b))\", \"" ^
1.369 - "(#Relate, (Randbedingungen, s))\"]";
1.370 -(*+*) O_Model.to_string @{context} root_model;
1.371 -(*\------------------- check entry to O_Model.complete_for -----------------------------------------/*)
1.372 -"~~~~~ fun complete_for , args:"; val (m_patt, root_model, (o_model, ctxt)) = (m_patt, root_model, (o_model, ctxt));
1.373 - val missing = m_patt |> filter_out
1.374 - (fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor));
1.375 - val add = (root_model
1.376 - |> filter
1.377 - (fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor))
1.378 -;
1.379 - ((o_model @ add)
1.380 - |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
1.381 - |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
1.382 - |> add_enumerate (* for correct enumeration *)
1.383 - |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
1.384 - ctxt |> ContextC.add_constraints (add |> values |> TermC.vars')) (*return from O_Model.complete_for*);
1.385 -"~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.complete_for , return:"; val (o_model', ctxt') =
1.386 - ((o_model @ add)
1.387 - |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
1.388 - |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
1.389 - |> add_enumerate (* for correct enumeration *)
1.390 - |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
1.391 - ctxt |> ContextC.add_constraints (add |> values |> TermC.vars'));
1.392 -
1.393 -(*/------------------- check of result from O_Model.complete_for -----------------------------------\*)
1.394 -(*+*) O_Model.to_string @{context} o_model'; "O_Model.complete_for: result o_model CHANGED";
1.395 -(*\------------------- check of result from O_Model.complete_for -----------------------------------/*)
1.396 -
1.397 - val thy = ThyC.get_theory @{context} dI
1.398 - val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
1.399 -
1.400 - (o_model', ctxt', i_model) (*return from Specify_Step.complete_for*);
1.401 -
1.402 -"~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.check , return:"; val (o_model, _, i_model) =
1.403 - (o_model', ctxt', i_model);
1.404 -
1.405 - Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model)) (*return from Specify_Step.check*);
1.406 -"~~~~~ fun Specify_Step.check \<longrightarrow>fun Step.check \<longrightarrow>fun Step.by_tactic , return:"; val (Applicable.Yes tac') =
1.407 - (Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model)));
1.408 - (*if*) Tactic.for_specify' tac' (*then*);
1.409 - val ("ok", ([], [], (_, _))) =
1.410 -
1.411 -Step_Specify.by_tactic tac' ptp;
1.412 -"~~~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt,pos as (p, _))) =
1.413 - (tac', ptp);
1.414 -(*NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
1.415 -(*NEW*) ...} = Calc.specify_data (pt, pos);
1.416 -(*NEW*) val (dI, _, mID) = References.select_input o_refs refs;
1.417 -(*NEW*) val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
1.418 -(*NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
1.419 -(*NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
1.420 -(*NEW*) val thy = ThyC.get_theory @{context} dI
1.421 -(*NEW*) val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
1.422 -(*NEW*) val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', i_model))
1.423 -(*NEW*) (Istate_Def.Uistate, ctxt') (pt, pos)
1.424 -
1.425 -(*/------------------- check result of Step_Specify.by_tactic ------------------------------\*)
1.426 -(*+*)val {origin = (o_model, _, _), meth, ...} = Calc.specify_data (pt, pos);
1.427 -(*+*)O_Model.to_string @{context} o_model;
1.428 -(*+*)if I_Model.to_string @{context} meth = "[\n" ^
1.429 - "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
1.430 - "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
1.431 - "(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n" ^
1.432 - "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str), \n" ^
1.433 - "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^
1.434 - "(6 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der), \n" ^
1.435 - "(7 ,[1] ,false ,#Given ,Mis Biegemoment id_momentum), \n" ^
1.436 - "(8 ,[1] ,false ,#Given ,Mis Querkraft id_lat_force), \n" ^
1.437 - "(9 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs)]"
1.438 -(*+*)then () else error "result of Step_Specify.by_tactic o_model CHANGED";
1.439 -(*\------------------- check result of Step_Specify.by_tactic ------------------------------/*)
1.440 -(*\------------------- step into Step.by_tactic /////////////////////////////////////////////*)
1.441 -
1.442 -
1.443 -\<close> ML \<open>
1.444 -val (_, ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
1.445 - Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []) (*of*);
1.446 -(*/------------------- step into Step.do_next \\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\*)
1.447 -"~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
1.448 - (p'''''_', ((pt'''''_', Pos.e_pos'), []));
1.449 - (*if*) Pos.on_calc_end ip (*else*);
1.450 - val (_, probl_id, _) = Calc.references (pt, p);
1.451 - val _ = (*case*) tacis (*of*);
1.452 - (*if*) probl_id = Problem.id_empty (*else*);
1.453 -
1.454 -val (_, ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
1.455 - switch_specify_solve p_ (pt, ip);
1.456 -"~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
1.457 - (*if*) Pos.on_specification ([], state_pos) (*then*);
1.458 -
1.459 -val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], [], (pt'''''_'', p'''''_''))) =
1.460 - Step.specify_do_next (pt, input_pos);
1.461 -(*/------------------- check result of specify_do_next -------------------------------------\*)
1.462 -(*+*)val {origin = (ooo_mod, _, _), meth, ...} = Calc.specify_data (pt'''''_'', p'''''_'');
1.463 -(*+*) O_Model.to_string @{context} ooo_mod; "result of Step_Specify.by_tactic o_model CHANGED";
1.464 -(*+*)if I_Model.to_string @{context} meth = "[\n" ^
1.465 - "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
1.466 - "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
1.467 - "(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n" ^
1.468 - "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str), \n" ^
1.469 - "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x , pen2str), \n" ^
1.470 - "(6 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der), \n" ^
1.471 - "(7 ,[1] ,false ,#Given ,Mis Biegemoment id_momentum), \n" ^
1.472 - "(8 ,[1] ,false ,#Given ,Mis Querkraft id_lat_force), \n" ^
1.473 - "(9 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs)]"
1.474 -(*+*)then () else error "result of Step_Specify.by_tactic i_model CHANGED";
1.475 -(*\------------------- check result of specify_do_next -------------------------------------/*)
1.476 -"~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
1.477 -
1.478 -(**)val (_, (p_', Add_Given "FunktionsVariable x")) =(**)
1.479 - Specify.find_next_step ptp;
1.480 -"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
1.481 - val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
1.482 - spec = refs, ...} = Calc.specify_data (pt, pos);
1.483 - val ctxt = Ctree.get_ctxt pt pos;
1.484 - (*if*) Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin (*else*);
1.485 - (*if*) p_ = Pos.Pbl (*else*);
1.486 -
1.487 -val return = for_problem ctxt oris (o_refs, refs) (pbl, met);
1.488 -"~~~~~ fun for_method , args:"; val (oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
1.489 - (oris, (o_refs, refs), (pbl, met));
1.490 - val cmI = if mI = MethodC.id_empty then mI' else mI;
1.491 - val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI;
1.492 - val (preok, _) = Pre_Conds.check ctxt where_rls where_ (mpc, I_Model.OLD_to_TEST met);
1.493 -"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return);
1.494 -(*/------------------- check within find_next_step -----------------------------------------\*)
1.495 -(*+*)Model_Pattern.to_string @{context} (MethodC.from_store ctxt mI' |> #model) = "[\"" ^
1.496 - "(#Given, (Traegerlaenge, l))\", \"" ^
1.497 - "(#Given, (Streckenlast, q))\", \"" ^
1.498 - "(#Given, (FunktionsVariable, v))\", \"" ^ (* <---------- take m_field from here !!!*)
1.499 - "(#Given, (GleichungsVariablen, vs))\", \"" ^
1.500 - "(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^
1.501 - "(#Find, (Biegelinie, b))\", \"" ^
1.502 - "(#Relate, (Randbedingungen, s))\"]";
1.503 -(*\------------------- check within find_next_step -----------------------------------------/*)
1.504 -
1.505 - (*case*) item_to_add (ThyC.get_theory @{context} (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
1.506 -"~~~~~ ~ fun item_to_add , args:"; val (thy, oris, _, itms) =
1.507 - ((ThyC.get_theory @{context} (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
1.508 -(*OLD*)fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v (**)andalso (#3 ori) <> "#undef"(**)
1.509 - fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
1.510 - fun test_id ids r = member op= ids (#1 (r : O_Model.single))
1.511 - fun test_subset itm (_, _, _, d, ts) =
1.512 - (I_Model.descriptor (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.o_model_values (#5 itm), ts)
1.513 - fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
1.514 - | false_and_not_Sup (_, _, false, _, _) = true
1.515 - | false_and_not_Sup _ = false
1.516 - val v = if itms = [] then 1 else Pre_Conds.max_variant itms
1.517 - val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
1.518 - val vits =
1.519 - if v = 0
1.520 - then itms (* because of dsc without dat *)
1.521 - else filter (testi_vt v) itms; (* itms..vat *)
1.522 - val icl = filter false_and_not_Sup vits; (* incomplete *)
1.523 -
1.524 -(*/------------------- check within item_to_add --------------------------------------------\*)
1.525 -(*+*)if I_Model.to_string @{context} icl = "[\n" ^ (*.. values, not formals*)
1.526 - "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^ (*.. values, not formals*)
1.527 - "(6 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der), \n" ^ (*.. values, not formals*)
1.528 - "(7 ,[1] ,false ,#Given ,Mis Biegemoment id_momentum), \n" ^ (*.. values, not formals*)
1.529 - "(8 ,[1] ,false ,#Given ,Mis Querkraft id_lat_force), \n" ^ (*.. values, not formals*)
1.530 - "(9 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs)]"
1.531 -(*+*)then () else error "icl within item_to_add CHANGED";
1.532 -(*+*) O_Model.to_string @{context} vors; "vors within item_to_add CHANGED";
1.533 -(*+*)if I_Model.to_string @{context} itms = "[\n" ^
1.534 - "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L , pen2str), \n" ^
1.535 - "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 , pen2str), \n" ^
1.536 - "(3 ,[1] ,true ,#Find ,Cor Biegelinie y , pen2str), \n" ^
1.537 - "(4 ,[1] ,true ,#Relate ,Cor Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str), \n" ^
1.538 - "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^
1.539 - "(6 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der), \n" ^
1.540 - "(7 ,[1] ,false ,#Given ,Mis Biegemoment id_momentum), \n" ^
1.541 - "(8 ,[1] ,false ,#Given ,Mis Querkraft id_lat_force), \n" ^
1.542 - "(9 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs)]"
1.543 -(*+*)then () else error "i_model within item_to_add CHANGED";
1.544 -(*\------------------- check within item_to_add --------------------------------------------/*)
1.545 -
1.546 - (*if*) icl = [] (*else*);
1.547 - val SOME ori =(*case*) find_first (test_subset (hd icl)) vors (*of*);
1.548 -
1.549 -(*+*)val (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]) = ori
1.550 -(*+*)val SOME ("#Given", "FunktionsVariable x") =
1.551 -
1.552 - SOME
1.553 - (I_Model.get_field_term thy ori (hd icl)) (*return from item_to_add*);
1.554 -"~~~~~ ~~ fun get_field_term , args:"; val (thy, (_, _, _, d, ts), (_, _, _, fd, itm_)) = (thy, ori, (hd icl));
1.555 -
1.556 -val rrrrr =
1.557 - (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join)
1.558 - (d, subtract op = (o_model_values itm_) ts)) (*return from get_field_term*);
1.559 -"~~~~~ ~~ from fun get_field_term \<longrightarrow>fun item_to_add \<longrightarrow>fun find_next_step , return:"; val (SOME (fd, ct')) =
1.560 - (SOME rrrrr);
1.561 - ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*return from find_next_step*);
1.562 -
1.563 -(*+*)val Add_Given "FunktionsVariable x" = P_Model.mk_additem fd ct';
1.564 -
1.565 -"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) =
1.566 - ("dummy", (Pos.Met, P_Model.mk_additem fd ct'));
1.567 - val ist_ctxt = Ctree.get_loc pt (p, p_)
1.568 - val _ = (*case*) tac (*of*);
1.569 -
1.570 - ("dummy",
1.571 -Step_Specify.by_tactic_input tac (pt, (p, p_'))) (*return from specify_do_next*);
1.572 -"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =
1.573 - (tac, (pt, (p, p_')));
1.574 -
1.575 - val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
1.576 - Specify.by_Add_ "#Given" ct ptp (*return from by_tactic_input*);
1.577 -"~~~~~ ~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);
1.578 - val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
1.579 - (*if*) p_ = Pos.Met (*then*);
1.580 - val (i_model, m_patt) = (met,
1.581 - (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
1.582 -
1.583 -val Add (5, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), (Free ("fun_var", _), [Free ("x", _)]))) =
1.584 - (*case*)
1.585 - I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
1.586 -"~~~~~ ~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
1.587 - (ctxt, m_field, oris, i_model, m_patt, ct);
1.588 -(*.NEW*) val SOME (t as (descriptor $ _)) = (*case*) ParseC.term_opt ctxt str (*of*);
1.589 -(*.NEW*) val SOME m_field = (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
1.590 -
1.591 -val ("", (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), [Free ("x", _)]) =
1.592 - (*case*)
1.593 - O_Model.contains ctxt m_field o_model t (*of*);
1.594 -"~~~~~ ~~~ fun contains , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
1.595 - val ots = ((distinct op =) o flat o (map #5)) ori
1.596 - val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots
1.597 - val (d, ts) = Input_Descript.split t
1.598 - val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts);
1.599 - (*if*) (subtract op = oids ids) <> [] (*else*);
1.600 - (*if*) d = TermC.empty (*else*);
1.601 - (*if*) member op = (map #4 ori) d (*then*);
1.602 -
1.603 - associate_input ctxt sel (d, ts) ori;
1.604 -"~~~~~ ~~~~ fun associate_input , args:"; val (ctxt, m_field, (descript, vals), ((id, vat, m_field', descript', vals') :: oris)) =
1.605 - (ctxt, sel, (d, ts), ori);
1.606 -
1.607 -(*/------------------- check within associate_input ------------------------------------------\*)
1.608 -(*+*)val Add_Given "FunktionsVariable x" = tac;
1.609 -(*+*)m_field = "#Given";
1.610 -(*+*)val Const (\<^const_name>\<open>FunktionsVariable\<close>, _) = descript;
1.611 -(*+*)val [Free ("x", _)] = vals;
1.612 -(*+*)O_Model.to_string @{context} ori = "[\n" ^
1.613 - "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
1.614 - "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
1.615 - "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
1.616 - "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
1.617 - "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
1.618 - "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
1.619 - "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]";
1.620 -(*+*)val (id, vat, m_field', descript', vals') = nth 5 ori
1.621 -(*+*)val (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]) =
1.622 - (id, vat, m_field', descript', vals')
1.623 -(*\------------------- check within associate_input ----------------------------------------/*)
1.624 -(*\------------------- step into me_Specify_Method_IntegrierenUndKonstanteBestimmen2--------*)
1.625 -(*[], Met*)val (p,_,f,nxt,_,pt) = return_me_Specify_Method_IntegrierenUndKonstanteBestimmen2
1.626 - val Add_Given "FunktionsVariable x" = nxt;
1.627 -
1.628 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy" = nxt
1.629 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Biegemoment M_b" = nxt
1.630 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Querkraft Q" = nxt
1.631 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]" = nxt
1.632 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
1.633 -
1.634 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Model_Problem = nxt
1.635 -(*/------------------- check entry to me Model_Problem -------------------------------------\*)
1.636 -(*+*)val ([1], Pbl) = p;
1.637 -(*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =
1.638 - get_obj g_origin pt (fst p);
1.639 -(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
1.640 - "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
1.641 - "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
1.642 - "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
1.643 -(*
1.644 -.. here the O_Model does NOT know, which MethodC will be chosen,
1.645 -so "belastung_zu_biegelinie q__q v_v b_b id_abl" is NOT known,
1.646 -"b_b" and "id_abl" are NOT missing.
1.647 -*)
1.648 -then () else error "[Biegelinien, ausBelastung] initial O_Model CHANGED";
1.649 -(*\------------------- check entry to me Model_Problem -------------------------------------/*)
1.650 -
1.651 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "Streckenlast q_0"*)
1.652 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)
1.653 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "Funktionen funs'''":*)
1.654 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Theory "Biegelinie"*)
1.655 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Problem ["vonBelastungZu", "Biegelinien"]*)
1.656 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Method ["Biegelinien", "ausBelastung"]*)
1.657 -
1.658 -(*[1], Met*)val return_me_Specify_Method_ausBelastung = me nxt p c pt; (*\<rightarrow>Add_Given "Biegelinie y"*)
1.659 -(*//------------------ step into me_Specify_Method_ausBelastung ----------------------------\\*)
1.660 -(*+*)val Specify_Method ["Biegelinien", "ausBelastung"] = nxt;
1.661 -(*+*)(* by \<up> \<up> \<up> \<up> "b_b" and "id_abl" must be requested: PUT THEM INTO O_Model*)
1.662 -
1.663 -"~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
1.664 -
1.665 - val ("ok", ([], [], (_, _))) = (*case*)
1.666 - Step.by_tactic tac (pt, p) (*of*);
1.667 -"~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
1.668 - val Applicable.Yes tac' = (*case*) check tac (pt, p) (*of*);
1.669 - (*if*) Tactic.for_specify' tac' (*then*);
1.670 -
1.671 - val ("ok", ([], [], (_, _))) =
1.672 -Step_Specify.by_tactic tac' ptp;
1.673 -(*/------------------- initial check for Step_Specify.by_tactic ----------------------------\*)
1.674 -(*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =
1.675 - get_obj g_origin pt (fst p);
1.676 -(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
1.677 - "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
1.678 - "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
1.679 - "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
1.680 -(*
1.681 -.. here the MethodC has been determined by the user,
1.682 -so "belastung_zu_biegelinie q__q v_v b_b id_abl" IS KNOWN and,
1.683 -"b_b" and "id_abl" WOULD BE missing (added by O_Model.).
1.684 -*)
1.685 -then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY MethodC";
1.686 -(*\------------------- initial check for Step_Specify.by_tactic ----------------------------/*)
1.687 -"~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt, pos as (p, _))) =
1.688 - (tac', ptp);
1.689 -(*.NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,
1.690 -(*.NEW*) ...} =Calc.specify_data (pt, pos);
1.691 -(*.NEW*) val (dI, _, mID) = References.select_input o_refs refs;
1.692 -(*.NEW*) val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
1.693 -(*.NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
1.694 -(*.NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt);
1.695 -
1.696 -(*/------------------- check for entry to O_Model.complete_for -----------------------------\*)
1.697 -(*+*)if mID = ["Biegelinien", "ausBelastung"]
1.698 -(*+*)then () else error "MethodC [Biegelinien, ausBelastung] CHANGED";
1.699 -(*+*)if Model_Pattern.to_string @{context} m_patt = "[\"" ^
1.700 - "(#Given, (Streckenlast, q__q))\", \"" ^
1.701 - "(#Given, (FunktionsVariable, v_v))\", \"" ^
1.702 - "(#Given, (Biegelinie, b_b))\", \"" ^
1.703 - "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^
1.704 - "(#Given, (Biegemoment, id_momentum))\", \"" ^
1.705 - "(#Given, (Querkraft, id_lat_force))\", \"" ^
1.706 - "(#Find, (Funktionen, fun_s))\"]"
1.707 -(*+*)then () else error "[Biegelinien, ausBelastung] Model_Pattern CHANGED";
1.708 -(*+*)if O_Model.to_string @{context} o_model = "[\n" ^
1.709 - "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
1.710 - "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
1.711 - "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
1.712 -(*+*)then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY MethodC CHANGED";
1.713 -(*+*) O_Model.to_string @{context} root_model;
1.714 -(*+*) O_Model.to_string @{context} o_model';
1.715 - "[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";
1.716 -(*\------------------- check for entry to O_Model.complete_for -----------------------------/*)
1.717 -
1.718 - O_Model.complete_for m_patt root_model (o_model, ctxt);
1.719 -"~~~~ fun complete_for , args:"; val (m_patt, root_model, (o_model, ctxt)) =
1.720 - (m_patt, root_model, (o_model, ctxt));
1.721 - val missing = m_patt |> filter_out
1.722 - (fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor))
1.723 -;
1.724 - val add = root_model
1.725 - |> filter
1.726 - (fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor)
1.727 -;
1.728 - (o_model @ add
1.729 -(*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
1.730 -(*NEW*)
1.731 - |> map (fn (_, b, c, d, e) => (b, c, d, e))
1.732 - |> add_enumerate
1.733 - |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
1.734 - ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars')) (*return from O_Model.complete_for*);
1.735 -"~~~~ from fun O_Model.complete_for \<longrightarrow>Step_Specify.by_tactic , return:"; val (o_model', ctxt') =
1.736 - ((o_model @ add)
1.737 -(*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
1.738 -(*NEW*)
1.739 - |> map (fn (_, b, c, d, e) => (b, c, d, e))
1.740 - |> add_enumerate
1.741 - |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
1.742 - ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars'));
1.743 -
1.744 -(*/------------------- check within O_Model.complete_for -------------------------------------------\*)
1.745 -(*+*) O_Model.to_string @{context} o_model';
1.746 - "[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";
1.747 -(*\------------------- check within O_Model.complete_for -------------------------------------------/*)
1.748 -
1.749 -(*.NEW*) val thy = ThyC.get_theory @{context} dI
1.750 -(*.NEW*) val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
1.751 -(*.NEW*) val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', i_model))
1.752 -(*.NEW*) (Istate_Def.Uistate, ctxt') (pt, pos)
1.753 -;
1.754 -(*+*) I_Model.to_string @{context} i_model; "[Biegelinien, ausBelastung] I_Model CHANGED 1";
1.755 -(*+*)val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt, ...} =
1.756 -(*+*) Calc.specify_data (pt, pos);
1.757 -(*+*)pos = ([1], Met);
1.758 -
1.759 - ("ok", ([], [], (pt, pos))) (*return from Step_Specify.by_tactic*);
1.760 -"~~~ from Step_Specify.by_tactic \<longrightarrow>Step.by_tactic \<longrightarrow>fun me , return:"; val ("ok", (_, _, (pt, p))) =
1.761 - ("ok", ([], [], (pt, pos)));
1.762 -(* val ("helpless", ([(xxxxx, _, _)], _, _)) = (*case*)*)
1.763 - (* SHOULD BE \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> Add_Given "Biegelinie y" | Add_Given "AbleitungBiegelinie dy"*)
1.764 -
1.765 -val ("ok", ([( Add_Given "Biegelinie y", _, _)], [], _)) =
1.766 - Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
1.767 -"~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
1.768 -(*.NEW*)(*if*) on_calc_end ip (*else*);
1.769 -(*.NEW*) val (_, probl_id, _) = Calc.references (pt, p);
1.770 -(*-"-*) val _ = (*case*) tacis (*of*);
1.771 -(*.NEW*) (*if*) probl_id = Problem.id_empty (*else*);
1.772 -
1.773 -(*.NEW*)val ("ok", ([(Add_Given "Biegelinie y", _, _)], _, _)) =
1.774 - switch_specify_solve p_ (pt, ip);
1.775 -"~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
1.776 - (*if*) Pos.on_specification ([], state_pos) (*then*);
1.777 -
1.778 - val ("ok", ([(Add_Given "Biegelinie y", _, _)], _, _)) =
1.779 - specify_do_next (pt, input_pos);
1.780 -"~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
1.781 -
1.782 - val (_, (p_', tac)) =
1.783 - Specify.find_next_step ptp;
1.784 -"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
1.785 - val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
1.786 - spec = refs, ...} = Calc.specify_data (pt, pos);
1.787 - val ctxt = Ctree.get_ctxt pt pos
1.788 -;
1.789 -(*+*)O_Model.to_string @{context} oris = "[\n" ^
1.790 - "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
1.791 - "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
1.792 - "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
1.793 - "(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
1.794 - "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]";
1.795 -(*+*)I_Model.is_complete pbl = true;
1.796 -(*+*)I_Model.to_string @{context} met = "[\n" ^
1.797 - "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
1.798 - "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
1.799 - "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
1.800 - "(4 ,[1] ,false ,#Given ,Mis Biegelinie b_b), \n" ^
1.801 - "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";
1.802 -
1.803 - (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
1.804 - (*if*) p_ = Pos.Pbl (*else*);
1.805 -val return = for_method ctxt oris (o_refs, refs) (pbl, met);
1.806 -"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) = (return);
1.807 -
1.808 - val ist_ctxt = Ctree.get_loc pt (p, p_)
1.809 - val Add_Given "Biegelinie y" = (*case*) tac (*of*);
1.810 -val return = Step_Specify.by_tactic_input tac (pt, (p, p_'));
1.811 -(*+*)val Add_Given "Biegelinie y" = tac;
1.812 - val ist_ctxt = Ctree.get_loc pt (p, p_)
1.813 - val _ = (*case*) tac (*of*);
1.814 -
1.815 - val (_, ([(Add_Given "Biegelinie y", _, _)], _, (p'''''_'', ([1], Met)))) =
1.816 -Step_Specify.by_tactic_input tac (pt, (p, p_'))
1.817 -(*/------------------- check result of Step_Specify.by_tactic_input ------------------------\*)
1.818 -(*+*)val {meth, ...} = Calc.specify_data (p'''''_'', ([1], Met));
1.819 -(*+*)I_Model.to_string @{context} meth = "[\n" ^ (* result does NOT show Add_Given "Biegelinie y" *)
1.820 - "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
1.821 - "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
1.822 - "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
1.823 - "(4 ,[1] ,false ,#Given ,Mis Biegelinie b_b), \n" ^
1.824 - "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";
1.825 -(*\------------------- check result of Step_Specify.by_tactic_input ------------------------/*)
1.826 -"~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) = (tac, (pt, (p, p_')));
1.827 -
1.828 - Specify.by_Add_ "#Given" ct ptp;
1.829 -"~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);
1.830 - val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
1.831 - (*if*) p_ = Pos.Met (*then*);
1.832 - val (i_model, m_patt) = (met,
1.833 - (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
1.834 -
1.835 -val Add (4, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Biegelinie\<close>, _), [Free ("y", _)]), (Free ("b_b", _), [Free ("y", _)]))) =
1.836 - (*case*)
1.837 - check_single ctxt m_field oris i_model m_patt ct (*of*);
1.838 -
1.839 -(*/------------------- check for entry to check_single -------------------------------------\*)
1.840 -(*+*) O_Model.to_string @{context} oris; "[Biegelinien, ausBelastung] O_Model CHANGED for entry";
1.841 -(*+*) I_Model.to_string ctxt met; "[Biegelinien, ausBelastung] I_Model CHANGED for entry";
1.842 -(*\------------------- check for entry to check_single -------------------------------------/*)
1.843 -
1.844 -"~~~~~ ~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
1.845 - (ctxt, sel, oris, met, ((#model o MethodC.from_store ctxt) cmI), ct);
1.846 - val SOME t = (*case*) ParseC.term_opt ctxt str (*of*);
1.847 -
1.848 -(*+*)val Const (\<^const_name>\<open>Biegelinie\<close>, _) $ Free ("y", _) = t;
1.849 -
1.850 -(*("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")]), [])*)
1.851 - (*case*)
1.852 - contains ctxt m_field o_model t (*of*);
1.853 -"~~~~~ ~~ fun contains , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
1.854 - val ots = ((distinct op =) o flat o (map #5)) ori
1.855 - val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots
1.856 - val (d, ts) = Input_Descript.split t
1.857 - val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts);
1.858 - (*if*) (subtract op = oids ids) <> [] (*else*);
1.859 - (*if*) d = TermC.empty (*else*);
1.860 - (*if*) not (subset op = (map make_typeless ts, map make_typeless ots)) (*else*);
1.861 -
1.862 - (*case*) O_Model.associate_input' ctxt sel ts ori (*of*);
1.863 -"~~~~~ ~~~ fun associate_input' , args:"; val (ctxt, sel, ts, ((id, vat, sel', d, ts') :: oris)) = (ctxt, sel, ts, ori);
1.864 -
1.865 -(*+/---------------- bypass recursion of associate_input' ----------------\*)
1.866 -(*+*)O_Model.to_string @{context} oris = "[\n" ^
1.867 - "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
1.868 - "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
1.869 - "(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
1.870 - "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]";
1.871 -(*+*)val (id, vat, sel', d, ts') = nth 3 oris; (* 3rd iteration *)
1.872 -(*+\---------------- bypass recursion of associate_input' ----------------/*)
1.873 -
1.874 - (*if*) sel = sel' andalso (inter op = ts ts') <> [] (*else*);
1.875 -
1.876 -(*/------------------- check within associate_input' -------------------------------\*)
1.877 -(*+*)if sel = "#Given" andalso sel' = "#Given"
1.878 -(*+*)then () else error "associate_input' Model_Pattern CHANGED";
1.879 -(*BUT: m_field can change from root-Problem to sub-MethodC --------------------vvv*)
1.880 -(* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
1.881 -(*+*)if (Problem.from_store ctxt ["vonBelastungZu", "Biegelinien"] |> #model |> Model_Pattern.to_string @{context}) = "[\"" ^
1.882 - "(#Given, (Streckenlast, q_q))\", \"" ^
1.883 - "(#Given, (FunktionsVariable, v_v))\", \"" ^
1.884 - "(#Find, (Funktionen, funs'''))\"]"
1.885 -(*+*)then () else error "associate_input' Model_Pattern of Subproblem CHANGED";
1.886 -(* root-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv ------------------------------------- \<up>*)
1.887 -(*+*)if (Problem.from_store ctxt ["Biegelinien"] |> #model |> Model_Pattern.to_string @{context}) = "[\"" ^
1.888 - "(#Given, (Traegerlaenge, l_l))\", \"" ^
1.889 - "(#Given, (Streckenlast, q_q))\", \"" ^
1.890 - "(#Find, (Biegelinie, b_b))\", \"" ^ (*------------------------------------- \<up> *)
1.891 - "(#Relate, (Randbedingungen, r_b))\"]"
1.892 -(*+*)then () else error "associate_input' Model_Pattern root-problem CHANGED";
1.893 -(* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
1.894 -(*+*)if (MethodC.from_store ctxt ["Biegelinien", "ausBelastung"] |> #model |> Model_Pattern.to_string @{context}) = "[\"" ^
1.895 - "(#Given, (Streckenlast, q__q))\", \"" ^
1.896 - "(#Given, (FunktionsVariable, v_v))\", \"" ^
1.897 - "(#Given, (Biegelinie, b_b))\", \"" ^
1.898 - "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^
1.899 - "(#Given, (Biegemoment, id_momentum))\", \"" ^
1.900 - "(#Given, (Querkraft, id_lat_force))\", \"" ^
1.901 - "(#Find, (Funktionen, fun_s))\"]"
1.902 -(*+*)then () else error "associate_input' Model_Pattern CHANGED";
1.903 -(*+*)if UnparseC.term @{context} d = "Biegelinie" andalso UnparseC.terms @{context} ts = "[y]"
1.904 -(*+*) andalso UnparseC.terms @{context} ts' = "[y]"
1.905 -(*+*)then
1.906 -(*+*) (case (inter op = ts ts') of [Free ("y", _(*"real \<Rightarrow> real"*))] => ()
1.907 -(*+*) | _ => error "check within associate_input' CHANGED 1")
1.908 -(*+*)else error "check within associate_input' CHANGED 2";
1.909 -(*\------------------- check within associate_input' -------------------------------/*)
1.910 -
1.911 -(*|------------------- contine me_Specify_Method_ausBelastung --------------------------------*)
1.912 -(*\------------------- step into me_Specify_Method_ausBelastung ----------------------------//*)
1.913 -(*[1], Met*)val (p,_,f,nxt,_,pt) = return_me_Specify_Method_ausBelastung;
1.914 - val Add_Given "Biegelinie y" = nxt
1.915 -
1.916 -(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie dy"= nxt
1.917 -(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Biegemoment M_b" = nxt
1.918 -(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Querkraft Q" = nxt
1.919 -(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["Biegelinien", "ausBelastung"] = nxt
1.920 -
1.921 -(*[1, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("sym_neg_equal_iff_equal", _)= nxt
1.922 -(*[1, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Rewrite ("Belastung_Querkraft", _)= nxt
1.923 -(*[1, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Subproblem ("Biegelinie", ["named", "integrate", "function"])= nxt
1.924 -(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Model_Problem= nxt
1.925 -(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "functionTerm (- q_0)"= nxt
1.926 -(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "integrateBy x"= nxt
1.927 -;
1.928 -(*/------------------- check result of Add_Given "functionTerm (- q_0)" --------------------\*)
1.929 -if p = ([1, 3], Pbl) andalso
1.930 - f = Test_Out.PpcKF (Test_Out.Problem [], {Find = [Incompl "antiDerivativeName"],
1.931 - Given = [Correct "functionTerm (- q_0)", Incompl "integrateBy"],
1.932 - Relate = [], Where = [], With = []})
1.933 -then
1.934 - (case nxt of Add_Given "integrateBy x" => () | _ => error "specify-phase: low level CHANGED 1")
1.935 -else error "specify-phase: low level CHANGED 2";
1.936 -(*\------------------- check result of Add_Given "functionTerm (- q_0)" --------------------/*)
1.937 -
1.938 -
1.939 -\<close>
1.940 ML_file "Specify/sub-problem.sml"
1.941 ML_file "Specify/step-specify.sml"
1.942