1.1 --- a/src/Tools/isac/BaseDefinitions/method-def.sml Mon Jun 20 18:37:54 2022 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/method-def.sml Mon Jun 20 18:43:51 2022 +0200
1.3 @@ -47,7 +47,7 @@
1.4 scr : Rule.program, (* filled in MethodC.prep_input *)
1.5 prls : Rule_Set.T, (* for evaluation of preconditions in "#Where" on "#Given" *)
1.6 ppc : Model_Pattern.T, (* contains "#Given", "#Where", "#Find", "#Relate"
1.7 - for constraints on identifiers see "O_Model.copy_name" *)
1.8 +(??) for constraints on identifiers see "O_Model.cpy_nam" *)
1.9 pre : term list (* ? DEL, as soon as they are input interactively ? *)
1.10 };
1.11 val empty = {guh = "met_empty", mathauthors = [], init = id_empty, rew_ord' = Rewrite_Ord.e_rew_ord',
2.1 --- a/src/Tools/isac/Specify/Specify.thy Mon Jun 20 18:37:54 2022 +0200
2.2 +++ b/src/Tools/isac/Specify/Specify.thy Mon Jun 20 18:43:51 2022 +0200
2.3 @@ -26,5 +26,6 @@
2.4 \<close> ML \<open>
2.5 \<close> ML \<open>
2.6 \<close> ML \<open>
2.7 +\<close> ML \<open>
2.8 \<close>
2.9 end
3.1 --- a/src/Tools/isac/Specify/o-model.sml Mon Jun 20 18:37:54 2022 +0200
3.2 +++ b/src/Tools/isac/Specify/o-model.sml Mon Jun 20 18:43:51 2022 +0200
3.3 @@ -347,4 +347,4 @@
3.4 else (UnparseC.term_in_ctxt ctxt d ^ " not in example", (0, [], sel, d, ts), [])
3.5 end
3.6
3.7 -(**)end(**);
3.8 \ No newline at end of file
3.9 +(**)end(**);
4.1 --- a/test/Tools/isac/Specify/m-match.sml Mon Jun 20 18:37:54 2022 +0200
4.2 +++ b/test/Tools/isac/Specify/m-match.sml Mon Jun 20 18:43:51 2022 +0200
4.3 @@ -52,9 +52,9 @@
4.4 then () else error "fun match_oris CHANGED";
4.5
4.6
4.7 -"----------- M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!) ------------=-------";
4.8 -"----------- M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!) ------------=-------";
4.9 -"----------- M_Match.arguments, is_cp, O_Model.copy_name +with EqSystem (!) --------------------";
4.10 +(??)"----------- M_Match.arguments, is_cp, O_Model.cpy_nam +with EqSystem (!) ----------------------";
4.11 +(??)"----------- M_Match.arguments, is_cp, O_Model.cpy_nam +with EqSystem (!) ----------------------";
4.12 +(??)"----------- M_Match.arguments, is_cp, O_Model.cpy_nam +with EqSystem (!) ----------------------";
4.13 val Const (\<^const_name>\<open>SubProblem\<close>,_) $
4.14 (Const (\<^const_name>\<open>Pair\<close>,_) $
4.15 Free (dI',_) $
5.1 --- a/test/Tools/isac/Test_Some.thy Mon Jun 20 18:37:54 2022 +0200
5.2 +++ b/test/Tools/isac/Test_Some.thy Mon Jun 20 18:43:51 2022 +0200
5.3 @@ -111,6 +111,767 @@
5.4 section \<open>===================================================================================\<close>
5.5 ML \<open>
5.6 \<close> ML \<open>
5.7 +(**** specify-phase: low level functions ################################################# ****)
5.8 +"----------- specify-phase: low level functions -----------------------------------------";
5.9 +"----------- specify-phase: low level functions -----------------------------------------";
5.10 +open O_Model;
5.11 +open I_Model;
5.12 +open Specify_Step;
5.13 +val formalise = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
5.14 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
5.15 + "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
5.16 + "AbleitungBiegelinie dy"];
5.17 +val references = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
5.18 +val p = e_pos'; val c = [];
5.19 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(formalise, references)]; (*nxt = Model_Problem*)
5.20 +
5.21 +(*/------------------- check result of CalcTreeTEST ----------------------------------------\*)
5.22 +(*+*)val (o_model, ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]), _) =
5.23 + get_obj g_origin pt (fst p);
5.24 +(*+*)if O_Model.to_string o_model = "[\n" ^
5.25 + "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
5.26 + "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
5.27 + "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
5.28 + "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
5.29 + "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
5.30 + "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
5.31 + "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"
5.32 +then () else error "[IntegrierenUndKonstanteBestimmen2] O_Model CHANGED";
5.33 +(*\------------------- check result of CalcTreeTEST ----------------------------------------/*)
5.34 +
5.35 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "Traegerlaenge L"*)
5.36 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "Streckenlast q_0"*)
5.37 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "Biegelinie y"*)
5.38 +(*[], 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*)
5.39 +(*[], 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]"*)
5.40 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Theory "Biegelinie"*)
5.41 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Problem ["Biegelinien"]*)
5.42 +(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)
5.43 +
5.44 +(*/------------------- step into whole me \<rightarrow>Specify_Method |||||||||||||||||||||||||||||||||\*)
5.45 +(*[], Met*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)
5.46 +
5.47 +(*/------------------- initial check for whole me ------------------------------------------\*)
5.48 +(*+*)val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt;
5.49 +(*+*)val Add_Given "FunktionsVariable x" = nxt''''';
5.50 +
5.51 +(*+*)val {origin = (o_model, o_refs, _), probl = i_pbl, meth = i_met, spec, ...} =
5.52 + Calc.specify_data (pt, p);
5.53 +(*+*)if o_refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])
5.54 +(*+*)then () else error "initial o_refs CHANGED";
5.55 +(*+*)if O_Model.to_string o_model = "[\n" ^
5.56 + "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
5.57 + "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
5.58 + "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
5.59 + "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
5.60 + "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
5.61 + "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
5.62 + "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"
5.63 +(*+*)then () else error "initial o_model CHANGED";
5.64 +(*+*)if I_Model.to_string @{context} i_pbl = "[\n" ^
5.65 + "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
5.66 + "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
5.67 + "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
5.68 + "(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]]))]"
5.69 +(*+*)then () else error "initial i_pbl CHANGED";
5.70 +(*+*)if I_Model.to_string @{context} i_met = "[]"
5.71 +(*+*)then () else error "initial i_met CHANGED";
5.72 +(*+*)val (_, ["Biegelinien"], _) = spec;
5.73 +(*\------------------- initial check for whole me ------------------------------------------/*)
5.74 +
5.75 +"~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
5.76 +(*/------------------- step into Step.by_tactic \\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\*)
5.77 + val (pt'''''_', p'''''_') = case
5.78 +
5.79 + Step.by_tactic tac (pt, p) of ("ok", (_, _, ptp)) => ptp;
5.80 +(*/------------------- check for entry to Step.by_tactic -----------------------------------\*)
5.81 +(*+*)val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = tac;
5.82 +(*+*)val {origin = (o_model, _, _), ...} = Calc.specify_data (pt, p);
5.83 +(*+*)if O_Model.to_string o_model = "[\n" ^
5.84 + "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
5.85 + "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
5.86 + "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
5.87 + "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
5.88 +(* these -------vvvvvv must be read from Model_Pattern in *)
5.89 + "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
5.90 + "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
5.91 + "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"
5.92 +(*+*)then () else error "o_model AFTER Specify_Method NOTok CHANGED";
5.93 +(*\------------------- check for Step.by_tactic --------------------------------------------/*)
5.94 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
5.95 + val Applicable.Yes tac' = (*case*)
5.96 +
5.97 + Step.check tac (pt, p) (*of*);
5.98 +"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
5.99 + (*if*) Tactic.for_specify tac (*then*);
5.100 +
5.101 +Specify_Step.check tac (ctree, pos);
5.102 +"~~~~~ fun check , args:"; val ((Tactic.Specify_Method mID), (ctree, pos)) = (tac, (ctree, pos));
5.103 +
5.104 + val (o_model''''', _, i_model''''') =
5.105 + Specify_Step.complete_for mID (ctree, pos);
5.106 +"~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (mID, (ctree, pos));
5.107 + val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
5.108 + ...} = Calc.specify_data (ctree, pos);
5.109 + val (dI, _, _) = References.select o_refs refs;
5.110 + val {ppc = m_patt, pre, prls, ...} = MethodC.from_store mID
5.111 + val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
5.112 + val (o_model', ctxt') =
5.113 +
5.114 + O_Model.complete_for m_patt root_model (o_model, ctxt);
5.115 +(*/------------------- check entry to O_Model.complete_for -----------------------------------------\*)
5.116 +(*+*)Model_Pattern.to_string m_patt = "[\"" ^
5.117 + "(#Given, (Traegerlaenge, l))\", \"" ^
5.118 + "(#Given, (Streckenlast, q))\", \"" ^
5.119 + "(#Given, (FunktionsVariable, v))\", \"" ^
5.120 + "(#Given, (GleichungsVariablen, vs))\", \"" ^
5.121 + "(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^
5.122 + "(#Find, (Biegelinie, b))\", \"" ^
5.123 + "(#Relate, (Randbedingungen, s))\"]";
5.124 +(*+*) O_Model.to_string root_model = "[\n" ^ (*.. = o_model for Pos.([], _) *)
5.125 + "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
5.126 + "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
5.127 + "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
5.128 + "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
5.129 + "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
5.130 + "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
5.131 + "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]";
5.132 +(*\------------------- check entry to O_Model.complete_for -----------------------------------------/*)
5.133 +"~~~~~ fun complete_for , args:"; val (m_patt, root_model, (o_model, ctxt)) = (m_patt, root_model, (o_model, ctxt));
5.134 + val missing = m_patt |> filter_out
5.135 + (fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor));
5.136 + val add = (root_model
5.137 + |> filter
5.138 + (fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor))
5.139 +;
5.140 + ((o_model @ add)
5.141 + |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
5.142 + |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
5.143 + |> add_enumerate (* for correct enumeration *)
5.144 + |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
5.145 + ctxt |> ContextC.add_constraints (add |> values |> TermC.vars')) (*return from O_Model.complete_for*);
5.146 +"~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.complete_for , return:"; val (o_model', ctxt') =
5.147 + ((o_model @ add)
5.148 + |> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
5.149 + |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
5.150 + |> add_enumerate (* for correct enumeration *)
5.151 + |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
5.152 + ctxt |> ContextC.add_constraints (add |> values |> TermC.vars'));
5.153 +
5.154 +(*/------------------- check of result from O_Model.complete_for -----------------------------------\*)
5.155 +(*+*)if O_Model.to_string o_model' = "[\n" ^
5.156 + "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
5.157 + "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
5.158 + "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
5.159 + "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
5.160 + "(5, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
5.161 + "(6, [\"1\"], #Given, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
5.162 + "(7, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"
5.163 +(*+*)then () else error "O_Model.complete_for: result o_model CHANGED";
5.164 +(*\------------------- check of result from O_Model.complete_for -----------------------------------/*)
5.165 +
5.166 + val thy = ThyC.get_theory dI
5.167 + val (_, (i_model, _)) = M_Match.match_itms_oris thy i_prob (m_patt, pre, prls) o_model';
5.168 +
5.169 + (o_model', ctxt', i_model) (*return from Specify_Step.complete_for*);
5.170 +
5.171 +"~~~~~ fun complete_for \<longrightarrow>fun Specify_Step.check , return:"; val (o_model, _, i_model) =
5.172 + (o_model', ctxt', i_model);
5.173 +
5.174 + Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model)) (*return from Specify_Step.check*);
5.175 +"~~~~~ fun Specify_Step.check \<longrightarrow>fun Step.check \<longrightarrow>fun Step.by_tactic , return:"; val (Applicable.Yes tac') =
5.176 + (Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model)));
5.177 + (*if*) Tactic.for_specify' tac' (*then*);
5.178 + val ("ok", ([], [], (_, _))) =
5.179 +
5.180 +Step_Specify.by_tactic tac' ptp;
5.181 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt,pos as (p, _))) =
5.182 + (tac', ptp);
5.183 +(*NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
5.184 +(*NEW*) ...} = Calc.specify_data (pt, pos);
5.185 +(*NEW*) val (dI, _, mID) = References.select o_refs refs;
5.186 +(*NEW*) val {ppc = m_patt, pre, prls, ...} = MethodC.from_store mID
5.187 +(*NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
5.188 +(*NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
5.189 +(*NEW*) val thy = ThyC.get_theory dI
5.190 +(*NEW*) val (_, (i_model, _)) = M_Match.match_itms_oris thy i_prob (m_patt, pre, prls) o_model';
5.191 +(*NEW*) val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', i_model))
5.192 +(*NEW*) (Istate_Def.Uistate, ctxt') (pt, pos)
5.193 +
5.194 +(*/------------------- check result of Step_Specify.by_tactic ------------------------------\*)
5.195 +(*+*)val {origin = (o_model, _, _), meth, ...} = Calc.specify_data (pt, pos);
5.196 +(*+*)O_Model.to_string o_model = "[\n" ^
5.197 + "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
5.198 + "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
5.199 + "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
5.200 + "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
5.201 + "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
5.202 + "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
5.203 + "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]";
5.204 +(* ERROR ------- \<up> \<up> CORRECTED TO #Given *)
5.205 +(*+*)if I_Model.to_string @{context} meth = "[\n" ^
5.206 + "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
5.207 + "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
5.208 + "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
5.209 + "(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" ^
5.210 + "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^
5.211 + "(6 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs), \n" ^
5.212 + "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"
5.213 +(*+*)then () else error "result of Step_Specify.by_tactic o_model CHANGED";
5.214 +(*\------------------- check result of Step_Specify.by_tactic ------------------------------/*)
5.215 +(*\------------------- step into Step.by_tactic /////////////////////////////////////////////*)
5.216 +
5.217 +
5.218 +val (_, ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
5.219 + Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []) (*of*);
5.220 +(*/------------------- step into Step.do_next \\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\*)
5.221 +"~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
5.222 + (p'''''_', ((pt'''''_', Pos.e_pos'), []));
5.223 + (*if*) Pos.on_calc_end ip (*else*);
5.224 + val (_, probl_id, _) = Calc.references (pt, p);
5.225 + val _ = (*case*) tacis (*of*);
5.226 + (*if*) probl_id = Problem.id_empty (*else*);
5.227 +
5.228 +val (_, ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
5.229 + switch_specify_solve p_ (pt, ip);
5.230 +"~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
5.231 + (*if*) Pos.on_specification ([], state_pos) (*then*);
5.232 +
5.233 +val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], [], (pt'''''_'', p'''''_''))) =
5.234 + specify_do_next (pt, input_pos);
5.235 +(*/------------------- check result of specify_do_next -------------------------------------\*)
5.236 +(*+*)val {origin = (ooo_mod, _, _), meth, ...} = Calc.specify_data (pt'''''_'', p'''''_'');
5.237 +(*+*)if O_Model.to_string ooo_mod = "[\n" ^
5.238 + "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
5.239 + "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
5.240 + "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
5.241 + "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
5.242 + "(5, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
5.243 + "(6, [\"1\"], #Given, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
5.244 + "(7, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"
5.245 +(*+*)then () else error "result of Step_Specify.by_tactic o_model CHANGED";
5.246 +(*+*)if I_Model.to_string @{context} meth = "[\n" ^
5.247 + "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
5.248 + "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
5.249 + "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
5.250 + "(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" ^
5.251 + "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(fun_var, [x])), \n" ^
5.252 + "(6 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs), \n" ^
5.253 + "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"
5.254 +(*+*)then () else error "result of Step_Specify.by_tactic i_model CHANGED";
5.255 +(*\------------------- check result of specify_do_next -------------------------------------/*)
5.256 +"~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
5.257 +
5.258 +(**)val (_, (p_', Add_Given "FunktionsVariable x")) =(**)
5.259 + Specify.find_next_step ptp;
5.260 +"~~~~~ fun find_next_step , args:"; val (pt, (p, p_)) = (ptp);
5.261 +(*.NEW*)val pblobj as {meth = met, origin = origin as (oris, (dI', pI', mI'), _),
5.262 +(*.NEW*) probl = pbl, spec = (dI, pI, mI), ctxt, ...} = Calc.specify_data (pt, (p, p_));
5.263 +(*.NEW*)(*if*) Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin (*else*);
5.264 + val cpI = if pI = Problem.id_empty then pI' else pI;
5.265 + val cmI = if mI = MethodC.id_empty then mI' else mI;
5.266 + val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;
5.267 + val (preok, pre) = Pre_Conds.check prls where_ pbl 0;
5.268 + (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
5.269 + val mpc = (#ppc o MethodC.from_store) cmI
5.270 + val Pos.Met = (*case*) p_ (*of*);
5.271 + val NONE = (*case*) find_first (I_Model.is_error o #5) met (*of*);
5.272 +
5.273 +(*/------------------- check within find_next_step -----------------------------------------\*)
5.274 +(*+*)Model_Pattern.to_string (MethodC.from_store mI' |> #ppc) = "[\"" ^
5.275 + "(#Given, (Traegerlaenge, l))\", \"" ^
5.276 + "(#Given, (Streckenlast, q))\", \"" ^
5.277 + "(#Given, (FunktionsVariable, v))\", \"" ^ (* <---------- take m_field from here !!!*)
5.278 + "(#Given, (GleichungsVariablen, vs))\", \"" ^
5.279 + "(#Given, (AbleitungBiegelinie, id_abl))\", \"" ^
5.280 + "(#Find, (Biegelinie, b))\", \"" ^
5.281 + "(#Relate, (Randbedingungen, s))\"]";
5.282 +(*\------------------- check within find_next_step -----------------------------------------/*)
5.283 +
5.284 + (*case*) item_to_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
5.285 +"~~~~~ ~ fun item_to_add , args:"; val (thy, oris, _, itms) =
5.286 + ((ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
5.287 +(*OLD*)fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v (**)andalso (#3 ori) <> "#undef"(**)
5.288 + fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
5.289 + fun test_id ids r = member op= ids (#1 (r : O_Model.single))
5.290 + fun test_subset itm (_, _, _, d, ts) =
5.291 + (I_Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.ts_in (#5 itm), ts)
5.292 + fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
5.293 + | false_and_not_Sup (_, _, false, _, _) = true
5.294 + | false_and_not_Sup _ = false
5.295 + val v = if itms = [] then 1 else I_Model.max_vt itms
5.296 + val vors = if v = 0 then oris else filter (testr_vt v) oris (* oris..vat *)
5.297 + val vits =
5.298 + if v = 0
5.299 + then itms (* because of dsc without dat *)
5.300 + else filter (testi_vt v) itms; (* itms..vat *)
5.301 + val icl = filter false_and_not_Sup vits; (* incomplete *)
5.302 +
5.303 +(*/------------------- check within item_to_add --------------------------------------------\*)
5.304 +(*+*)if I_Model.to_string @{context} icl = "[\n" ^ (*.. values*)
5.305 + "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^
5.306 + "(6 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs), \n" ^
5.307 + "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"
5.308 +(*+*)then () else error "icl within item_to_add CHANGED";
5.309 +(*+*)if O_Model.to_string vors = "[\n" ^
5.310 + "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
5.311 + "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
5.312 + "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
5.313 + "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
5.314 + "(5, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
5.315 + "(6, [\"1\"], #Given, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
5.316 + "(7, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"
5.317 +(*+*)then () else error "vors within item_to_add CHANGED";
5.318 +(*+*)if I_Model.to_string @{context} itms = "[\n" ^
5.319 + "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^
5.320 + "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
5.321 + "(3 ,[1] ,true ,#Find ,Cor Biegelinie y ,(b_b, [y])), \n" ^
5.322 + "(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" ^
5.323 + "(5 ,[1] ,false ,#Given ,Mis FunktionsVariable fun_var), \n" ^ (*.. still NOT ,true ,#Given , Cor*)
5.324 + "(6 ,[1] ,false ,#Given ,Mis GleichungsVariablen vs), \n" ^
5.325 + "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"
5.326 +(*+*)then () else error "i_model within item_to_add CHANGED";
5.327 +(*\------------------- check within item_to_add --------------------------------------------/*)
5.328 +
5.329 + (*if*) icl = [] (*else*);
5.330 + val SOME ori =(*case*) find_first (test_subset (hd icl)) vors (*of*);
5.331 +
5.332 +(*+*)val (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]) = ori
5.333 +(*+*)val SOME ("#Given", "FunktionsVariable x") =
5.334 +
5.335 + SOME
5.336 + (I_Model.geti_ct thy ori (hd icl)) (*return from item_to_add*);
5.337 +"~~~~~ ~~ fun geti_ct , args:"; val (thy, (_, _, _, d, ts), (_, _, _, fd, itm_)) = (thy, ori, (hd icl));
5.338 +
5.339 +val rrrrr =
5.340 + (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join)
5.341 + (d, subtract op = (ts_in itm_) ts)) (*return from geti_ct*);
5.342 +"~~~~~ ~~ from fun geti_ct \<longrightarrow>fun item_to_add \<longrightarrow>fun find_next_step , return:"; val (SOME (fd, ct')) =
5.343 + (SOME rrrrr);
5.344 + ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*return from find_next_step*);
5.345 +
5.346 +(*+*)val Add_Given "FunktionsVariable x" = P_Model.mk_additem fd ct';
5.347 +
5.348 +"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) =
5.349 + ("dummy", (Pos.Met, P_Model.mk_additem fd ct'));
5.350 + val ist_ctxt = Ctree.get_loc pt (p, p_)
5.351 + val _ = (*case*) tac (*of*);
5.352 +
5.353 + ("dummy",
5.354 +Step_Specify.by_tactic_input tac (pt, (p, p_'))) (*return from specify_do_next*);
5.355 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =
5.356 + (tac, (pt, (p, p_')));
5.357 +
5.358 + val ("ok", ([(Add_Given "FunktionsVariable x", _, _)], _, _)) =
5.359 + Specify.by_Add_ "#Given" ct ptp (*return from by_tactic_input*);
5.360 +"~~~~~ ~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);
5.361 + val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
5.362 + (*if*) p_ = Pos.Met (*then*);
5.363 + val (i_model, m_patt) = (met,
5.364 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store |> #ppc)
5.365 +
5.366 +val Add (5, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), (Free ("fun_var", _), [Free ("x", _)]))) =
5.367 + (*case*)
5.368 + I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
5.369 +"~~~~~ ~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
5.370 + (ctxt, m_field, oris, i_model, m_patt, ct);
5.371 +(*.NEW*) val SOME (t as (descriptor $ _)) = (*case*) TermC.parseNEW ctxt str (*of*);
5.372 +(*.NEW*) val SOME m_field = (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
5.373 +
5.374 +val ("", (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]), [Free ("x", _)]) =
5.375 + (*case*)
5.376 + O_Model.contains ctxt m_field o_model t (*of*);
5.377 +"~~~~~ ~~~ fun contains , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
5.378 + val ots = ((distinct op =) o flat o (map #5)) ori
5.379 + val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots
5.380 + val (d, ts) = Input_Descript.split t
5.381 + val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts);
5.382 + (*if*) (subtract op = oids ids) <> [] (*else*);
5.383 + (*if*) d = TermC.empty (*else*);
5.384 + (*if*) member op = (map #4 ori) d (*then*);
5.385 +\<close> ML \<open>
5.386 +
5.387 + associate_input ctxt sel (d, ts) ori;
5.388 +\<close> text \<open>
5.389 +val it = (
5.390 + "",
5.391 + (5, [1], "#Given", Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), [Free ("x", "real")]),
5.392 + [Free ("x", "real")]
5.393 + ): message * O_Model.single * values
5.394 +\<close> ML \<open>
5.395 +[@{term xxx}] : values
5.396 +\<close> ML \<open>
5.397 +\<close> ML \<open>
5.398 +\<close> ML \<open>
5.399 +\<close> ML \<open>
5.400 +"~~~~~ ~~~~ fun associate_input , args:"; val (ctxt, m_field, (descript, vals), ((id, vat, m_field', descript', vals') :: oris)) =
5.401 + (ctxt, sel, (d, ts), ori);
5.402 +
5.403 +(*/------------------- check within associate_input --------------------------------------------\*)
5.404 +(*+*)val Add_Given "FunktionsVariable x" = tac;
5.405 +(*+*)m_field = "#Given";
5.406 +(*+*)val Const (\<^const_name>\<open>FunktionsVariable\<close>, _) = descript;
5.407 +(*+*)val [Free ("x", _)] = vals;
5.408 +(*+*)O_Model.to_string ori = "[\n" ^
5.409 + "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
5.410 + "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
5.411 + "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
5.412 + "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
5.413 + "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^
5.414 + "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
5.415 + "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]";
5.416 +(*+*)val (id, vat, m_field', descript', vals') = nth 5 ori
5.417 +(*+*)val (5, [1], "#Given", Const (\<^const_name>\<open>FunktionsVariable\<close>, _), [Free ("x", _)]) =
5.418 + (id, vat, m_field', descript', vals')
5.419 +(*\------------------- check within associate_input --------------------------------------------/*)
5.420 +(*-------------------- stop step into whole me ----------------------------------------------*)
5.421 +(*\------------------- step into whole me \<rightarrow>Specify_Method |||||||||||||||||||||||||||||||||/*)
5.422 +
5.423 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*\<rightarrow>Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)
5.424 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "AbleitungBiegelinie dy"*)
5.425 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)
5.426 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Model_Problem*)
5.427 +
5.428 +(*/------------------- check entry to me Model_Problem -------------------------------------\*)
5.429 +(*+*)val ([1], Pbl) = p;
5.430 +(*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =
5.431 + get_obj g_origin pt (fst p);
5.432 +(*+*)if O_Model.to_string o_model = "[\n" ^
5.433 + "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
5.434 + "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
5.435 + "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
5.436 +(*
5.437 +.. here the O_Model does NOT know, which MethodC will be chosen,
5.438 +so "belastung_zu_biegelinie q__q v_v id_fun id_abl" is NOT known,
5.439 +"id_fun" and "id_abl" are NOT missing.
5.440 +*)
5.441 +then () else error "[Biegelinien, ausBelastung] initial O_Model CHANGED";
5.442 +(*\------------------- check entry to me Model_Problem -------------------------------------/*)
5.443 +
5.444 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "Streckenlast q_0"*)
5.445 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Given "FunktionsVariable x"*)
5.446 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Add_Find "Funktionen funs'''":*)
5.447 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Theory "Biegelinie"*)
5.448 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Problem ["vonBelastungZu", "Biegelinien"]*)
5.449 +(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Specify_Method ["Biegelinien", "ausBelastung"]*)
5.450 +
5.451 +(*[1], Met*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*\<rightarrow>Add_Given "Biegelinie y"*)
5.452 +(*/------------------- step into me\<rightarrow>Add_Given "Biegelinie y" ||||||||||||||||||||||||||||||\*)
5.453 +(*+*)val Specify_Method ["Biegelinien", "ausBelastung"] = nxt;
5.454 +(*+*)(* by \<up> \<up> \<up> \<up> "id_fun" and "id_abl" must be requested: PUT THEM INTO O_Model*)
5.455 +
5.456 +"~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
5.457 +
5.458 + val ("ok", ([], [], (_, _))) = (*case*)
5.459 + Step.by_tactic tac (pt, p) (*of*);
5.460 +"~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
5.461 + val Applicable.Yes tac' = (*case*) check tac (pt, p) (*of*);
5.462 + (*if*) Tactic.for_specify' tac' (*then*);
5.463 +
5.464 + val ("ok", ([], [], (_, _))) =
5.465 +Step_Specify.by_tactic tac' ptp;
5.466 +(*/------------------- initial check for Step_Specify.by_tactic ----------------------------\*)
5.467 +(*+*)val (o_model, ("Biegelinie", ["vonBelastungZu", "Biegelinien"], ["Biegelinien", "ausBelastung"]), _) =
5.468 + get_obj g_origin pt (fst p);
5.469 +(*+*)if O_Model.to_string o_model = "[\n" ^
5.470 + "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
5.471 + "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
5.472 + "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
5.473 +(*
5.474 +.. here the MethodC has been determined by the user,
5.475 +so "belastung_zu_biegelinie q__q v_v id_fun id_abl" IS KNOWN and,
5.476 +"id_fun" and "id_abl" WOULD BE missing (added by O_Model.).
5.477 +*)
5.478 +then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY MethodC";
5.479 +(*\------------------- initial check for Step_Specify.by_tactic ----------------------------/*)
5.480 +"~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt, pos as (p, _))) =
5.481 + (tac', ptp);
5.482 +(*.NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,
5.483 +(*.NEW*) ...} =Calc.specify_data (pt, pos);
5.484 +(*.NEW*) val (dI, _, mID) = References.select o_refs refs;
5.485 +(*.NEW*) val {ppc = m_patt, pre, prls, ...} = MethodC.from_store mID
5.486 +(*.NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
5.487 +(*.NEW*) val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt);
5.488 +
5.489 +(*/------------------- check for entry to O_Model.complete_for -----------------------------\*)
5.490 +(*+*)if mID = ["Biegelinien", "ausBelastung"]
5.491 +(*+*)then () else error "MethodC [Biegelinien, ausBelastung] CHANGED";
5.492 +(*+*)if Model_Pattern.to_string m_patt = "[\"" ^
5.493 + "(#Given, (Streckenlast, q__q))\", \"" ^
5.494 + "(#Given, (FunktionsVariable, v_v))\", \"" ^
5.495 + "(#Given, (Biegelinie, id_fun))\", \"" ^ (*.. add value from O_Model of root-problem*)
5.496 + "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^ (*.. add value from O_Model of root-problem*)
5.497 + "(#Find, (Funktionen, fun_s))\"]"
5.498 +(*+*)then () else error "[Biegelinien, ausBelastung] Model_Pattern CHANGED";
5.499 +(*+*)if O_Model.to_string o_model = "[\n" ^
5.500 + "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
5.501 + "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
5.502 + "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"])]"
5.503 +(*+*)then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY MethodC CHANGED";
5.504 +(*+*)if O_Model.to_string root_model = "[\n" ^
5.505 + "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
5.506 + "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
5.507 + "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
5.508 + "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^
5.509 + "(5, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
5.510 + "(6, [\"1\"], #Given, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^
5.511 + "(7, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"
5.512 +(*+*)then () else error "[Biegelinien, ausBelastung] root O_Model CHANGED";
5.513 +(*+*)if O_Model.to_string o_model' = "[\n" ^ (*.. OK: is value of O_Model.complete_for *)
5.514 + "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
5.515 + "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
5.516 + "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
5.517 + "(4, [\"1\"], #Given, Biegelinie, [\"y\"]), \n" ^ (*.. value from O_Model of root-problem*)
5.518 + "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]" (*.. value from O_Model of root-problem*)
5.519 +(* \<up> ----- aim at dropping this field *)
5.520 +(*+*)then () else error "[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";
5.521 +(*\------------------- check for entry to O_Model.complete_for -----------------------------/*)
5.522 +
5.523 + O_Model.complete_for m_patt root_model (o_model, ctxt);
5.524 +"~~~~ fun complete_for , args:"; val (m_patt, root_model, (o_model, ctxt)) =
5.525 + (m_patt, root_model, (o_model, ctxt));
5.526 + val missing = m_patt |> filter_out
5.527 + (fn (_, (descriptor, _)) => (member op = (map #4 o_model) descriptor))
5.528 +;
5.529 + val add = root_model
5.530 + |> filter
5.531 + (fn (_, _, _, descriptor, _) => (member op = (map (fst o snd) missing)) descriptor)
5.532 +;
5.533 + (o_model @ add
5.534 +(*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
5.535 +(*NEW*)
5.536 + |> map (fn (_, b, c, d, e) => (b, c, d, e))
5.537 + |> add_enumerate
5.538 + |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
5.539 + ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars')) (*return from O_Model.complete_for*);
5.540 +"~~~~ from fun O_Model.complete_for \<longrightarrow>Step_Specify.by_tactic , return:"; val (o_model', ctxt') =
5.541 + ((o_model @ add)
5.542 +(*NEW*)|> map (fn (a, b, _, descr, e) => (a, b, the (Model_Pattern.get_field descr m_patt), descr, e))
5.543 +(*NEW*)
5.544 + |> map (fn (_, b, c, d, e) => (b, c, d, e))
5.545 + |> add_enumerate
5.546 + |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
5.547 + ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars'));
5.548 +
5.549 +(*/------------------- check within O_Model.complete_for -------------------------------------------\*)
5.550 +(*+*)if O_Model.to_string o_model' = "[\n" ^ (*.. OK: is return from step into *)
5.551 + "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
5.552 + "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
5.553 + "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
5.554 + "(4, [\"1\"], #Given, Biegelinie, [\"y\"]), \n" ^
5.555 + "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"
5.556 +(* \<up> ----- aim at dropping this field *)
5.557 +(*+*)then () else error "[Biegelinien, ausBelastung] O_Model EXTENDED BY MethodC CHANGED";
5.558 +(*\------------------- check within O_Model.complete_for -------------------------------------------/*)
5.559 +
5.560 +(*.NEW*) val thy = ThyC.get_theory dI
5.561 +(*.NEW*) val (_, (i_model, _)) = M_Match.match_itms_oris thy i_prob (m_patt, pre, prls) o_model';
5.562 +(*.NEW*) val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', i_model))
5.563 +(*.NEW*) (Istate_Def.Uistate, ctxt') (pt, pos)
5.564 +;
5.565 +(*+*)if I_Model.to_string @{context} i_model = "[\n" ^
5.566 + "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
5.567 + "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
5.568 + "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
5.569 + "(4 ,[1] ,false ,#Given ,Mis Biegelinie id_fun), \n" ^
5.570 + "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"
5.571 +(*+*)then () else error "[Biegelinien, ausBelastung] I_Model CHANGED 1";
5.572 +(*+*)val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt, ...} =
5.573 +(*+*) Calc.specify_data (pt, pos);
5.574 +(*+*)pos = ([1], Met);
5.575 +
5.576 + ("ok", ([], [], (pt, pos))) (*return from Step_Specify.by_tactic*);
5.577 +"~~~ from Step_Specify.by_tactic \<longrightarrow>Step.by_tactic \<longrightarrow>fun me , return:"; val ("ok", (_, _, (pt, p))) =
5.578 + ("ok", ([], [], (pt, pos)));
5.579 +(* val ("helpless", ([(xxxxx, _, _)], _, _)) = (*case*)*)
5.580 + (* SHOULD BE \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> \<up> Add_Given "Biegelinie y" | Add_Given "AbleitungBiegelinie dy"*)
5.581 +
5.582 +val ("ok", ([( Add_Given "Biegelinie y", _, _)], [], _)) =
5.583 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
5.584 +"~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
5.585 +(*.NEW*)(*if*) on_calc_end ip (*else*);
5.586 +(*.NEW*) val (_, probl_id, _) = Calc.references (pt, p);
5.587 +(*-"-*) val _ = (*case*) tacis (*of*);
5.588 +(*.NEW*) (*if*) probl_id = Problem.id_empty (*else*);
5.589 +
5.590 +(*.NEW*)val ("ok", ([(Add_Given "Biegelinie y", _, _)], _, _)) =
5.591 + switch_specify_solve p_ (pt, ip);
5.592 +"~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
5.593 + (*if*) Pos.on_specification ([], state_pos) (*then*);
5.594 +
5.595 + val ("ok", ([(Add_Given "Biegelinie y", _, _)], _, _)) =
5.596 + specify_do_next (pt, input_pos);
5.597 +"~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
5.598 +
5.599 + val (_, (p_', tac)) =
5.600 + Specify.find_next_step ptp;
5.601 +"~~~~~ fun find_next_step , args:"; val (pt, (p, p_)) = (ptp);
5.602 + val (pblobj, met, origin, oris, dI', pI', mI', pbl, dI, pI, mI) =
5.603 + case Ctree.get_obj I pt p of
5.604 + pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
5.605 + probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)
5.606 + | Ctree.PrfObj _ => raise ERROR "nxt_specify_: not on PrfObj"
5.607 +;
5.608 +(*+*)O_Model.to_string oris = "[\n" ^
5.609 + "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
5.610 + "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
5.611 + "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
5.612 + "(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
5.613 + "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]";
5.614 +(*+*)I_Model.is_complete pbl = true;
5.615 +(*+*)I_Model.to_string @{context} met = "[\n" ^
5.616 + "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
5.617 + "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
5.618 + "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
5.619 + "(4 ,[1] ,false ,#Given ,Mis Biegelinie id_fun), \n" ^
5.620 + "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";
5.621 +
5.622 + (*if*) Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin (*else*);
5.623 + val cpI = if pI = Problem.id_empty then pI' else pI;
5.624 + val cmI = if mI = MethodC.id_empty then mI' else mI;
5.625 + val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;
5.626 + val (preok, pre) = Pre_Conds.check prls where_ pbl 0;
5.627 + val preok = foldl and_ (true, map fst pre);
5.628 + val mpc = (#ppc o MethodC.from_store) cmI
5.629 + val Pos.Met = (*case*) p_ (*of*);
5.630 + val NONE = (*case*) find_first (is_error o #5) met (*of*);
5.631 + (*val SOME ("#Given", "Biegelinie y") =*)
5.632 + val SOME (fd, ct') = (*case*)
5.633 + item_to_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
5.634 +
5.635 + ("ok", (Pos.Met, P_Model.mk_additem fd ct')) (*return from find_next_step*);
5.636 +"~~~~~ from fun find_next_step \<longrightarrow>fun specify_do_next , return:"; val (_, (p_', tac)) =
5.637 + ("dummy", (Pos.Met, P_Model.mk_additem fd ct'));
5.638 +(*+*)val Add_Given "Biegelinie y" = tac;
5.639 + val ist_ctxt = Ctree.get_loc pt (p, p_)
5.640 + val _ = (*case*) tac (*of*);
5.641 +
5.642 + val (_, ([(Add_Given "Biegelinie y", _, _)], _, (p'''''_'', ([1], Met)))) =
5.643 +Step_Specify.by_tactic_input tac (pt, (p, p_'))
5.644 +(*/------------------- check result of Step_Specify.by_tactic_input ------------------------\*)
5.645 +(*+*)val {meth, ...} = Calc.specify_data (p'''''_'', ([1], Met));
5.646 +(*+*)I_Model.to_string @{context} meth = "[\n" ^ (* result does NOT show Add_Given "Biegelinie y" *)
5.647 + "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
5.648 + "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
5.649 + "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
5.650 + "(4 ,[1] ,false ,#Given ,Mis Biegelinie id_fun), \n" ^
5.651 + "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";
5.652 +(*\------------------- check result of Step_Specify.by_tactic_input ------------------------/*)
5.653 +"~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) = (tac, (pt, (p, p_')));
5.654 +
5.655 + Specify.by_Add_ "#Given" ct ptp;
5.656 +"~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, ptp);
5.657 + val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
5.658 + (*if*) p_ = Pos.Met (*then*);
5.659 + val (i_model, m_patt) = (met,
5.660 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store |> #ppc)
5.661 +
5.662 +val Add (4, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Biegelinie\<close>, _), [Free ("y", _)]), (Free ("id_fun", _), [Free ("y", _)]))) =
5.663 + (*case*)
5.664 + check_single ctxt m_field oris i_model m_patt ct (*of*);
5.665 +
5.666 +(*/------------------- check for entry to check_single -------------------------------------\*)
5.667 +(*+*)if O_Model.to_string oris = "[\n" ^
5.668 + "(1, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^
5.669 + "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
5.670 + "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
5.671 + "(4, [\"1\"], #Given, Biegelinie, [\"y\"]), \n" ^ (*------------------- \<up> \<up> \<up> \<up> ^*)
5.672 + "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]"
5.673 +(*+*)then () else error "[Biegelinien, ausBelastung] O_Model CHANGED for entry";
5.674 +(*+*)if I_Model.to_string ctxt met = "[\n" ^
5.675 + "(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])), \n" ^
5.676 + "(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])), \n" ^
5.677 + "(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs'''])), \n" ^
5.678 + "(4 ,[1] ,false ,#Given ,Mis Biegelinie id_fun), \n" ^
5.679 + "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_der)]"
5.680 +(*+*)then () else error "[Biegelinien, ausBelastung] I_Model CHANGED for entry";
5.681 +(*\------------------- check for entry to check_single -------------------------------------/*)
5.682 +
5.683 +"~~~~~ ~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
5.684 + (ctxt, sel, oris, met, ((#ppc o MethodC.from_store) cmI), ct);
5.685 + val SOME t = (*case*) TermC.parseNEW ctxt str (*of*);
5.686 +
5.687 +(*+*)val Const (\<^const_name>\<open>Biegelinie\<close>, _) $ Free ("y", _) = t;
5.688 +
5.689 +(*("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")]), [])*)
5.690 + (*case*)
5.691 + contains ctxt m_field o_model t (*of*);
5.692 +"~~~~~ ~~ fun contains , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
5.693 + val ots = ((distinct op =) o flat o (map #5)) ori
5.694 + val oids = ((map (fst o dest_Free)) o (distinct op =) o flat o (map TermC.vars)) ots
5.695 + val (d, ts) = Input_Descript.split t
5.696 + val ids = map (fst o dest_Free) (((distinct op =) o (flat o (map TermC.vars))) ts);
5.697 + (*if*) (subtract op = oids ids) <> [] (*else*);
5.698 + (*if*) d = TermC.empty (*else*);
5.699 + (*if*) not (subset op = (map make_typeless ts, map make_typeless ots)) (*else*);
5.700 +
5.701 + (*case*) O_Model.associate_input' ctxt sel ts ori (*of*);
5.702 +"~~~~~ ~~~ fun associate_input' , args:"; val (ctxt, sel, ts, ((id, vat, sel', d, ts') :: oris)) = (ctxt, sel, ts, ori);
5.703 +
5.704 +(*+/---------------- bypass recursion of associate_input' ----------------\*)
5.705 +(*+*)O_Model.to_string oris = "[\n" ^
5.706 + "(2, [\"1\"], #Given, FunktionsVariable, [\"x\"]), \n" ^
5.707 + "(3, [\"1\"], #Find, Funktionen, [\"funs'''\"]), \n" ^
5.708 + "(4, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^
5.709 + "(5, [\"1\"], #Given, AbleitungBiegelinie, [\"dy\"])]";
5.710 +(*+*)val (id, vat, sel', d, ts') = nth 3 oris; (* 3rd iteration *)
5.711 +(*+\---------------- bypass recursion of associate_input' ----------------/*)
5.712 +
5.713 + (*if*) sel = sel' andalso (inter op = ts ts') <> [] (*else*);
5.714 +
5.715 +(*/------------------- check within associate_input' -------------------------------\*)
5.716 +(*+*)if sel = "#Given" andalso sel' = "#Given"
5.717 +(*+*)then () else error "associate_input' Model_Pattern CHANGED";
5.718 +(*BUT: m_field can change from root-Problem to sub-MethodC --------------------vvv*)
5.719 +(* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
5.720 +(*+*)if (Problem.from_store ["vonBelastungZu", "Biegelinien"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^
5.721 + "(#Given, (Streckenlast, q_q))\", \"" ^
5.722 + "(#Given, (FunktionsVariable, v_v))\", \"" ^
5.723 + "(#Find, (Funktionen, funs'''))\"]"
5.724 +(*+*)then () else error "associate_input' Model_Pattern of Subproblem CHANGED";
5.725 +(* root-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv ------------------------------------- \<up> *)
5.726 +(*+*)if (Problem.from_store ["Biegelinien"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^
5.727 + "(#Given, (Traegerlaenge, l_l))\", \"" ^
5.728 + "(#Given, (Streckenlast, q_q))\", \"" ^
5.729 + "(#Find, (Biegelinie, b_b))\", \"" ^ (*------------------------------------- \<up> *)
5.730 + "(#Relate, (Randbedingungen, r_b))\"]"
5.731 +(*+*)then () else error "associate_input' Model_Pattern root-problem CHANGED";
5.732 +(* sub-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv*)
5.733 +(*+*)if (MethodC.from_store ["Biegelinien", "ausBelastung"] |> #ppc |> Model_Pattern.to_string) = "[\"" ^
5.734 + "(#Given, (Streckenlast, q__q))\", \"" ^
5.735 + "(#Given, (FunktionsVariable, v_v))\", \"" ^
5.736 + "(#Given, (Biegelinie, id_fun))\", \"" ^ (*--------------------------------- \<up> *)
5.737 + "(#Given, (AbleitungBiegelinie, id_der))\", \"" ^
5.738 + "(#Find, (Funktionen, fun_s))\"]"
5.739 +(*+*)then () else error "associate_input' Model_Pattern CHANGED";
5.740 +(*+*)if UnparseC.term d = "Biegelinie" andalso UnparseC.terms ts = "[\"y\"]"
5.741 +(*+*) andalso UnparseC.terms ts' = "[\"y\"]"
5.742 +(*+*)then
5.743 +(*+*) (case (inter op = ts ts') of [Free ("y", _(*"real \<Rightarrow> real"*))] => ()
5.744 +(*+*) | _ => error "check within associate_input' CHANGED 1")
5.745 +(*+*)else error "check within associate_input' CHANGED 2";
5.746 +(*\------------------- check within associate_input' -------------------------------/*)
5.747 +(*-------------------- stop step into me\<rightarrow>Add_Given "Biegelinie y" --------------------------*)
5.748 +(*\------------------- step into me\<rightarrow>Add_Given "Biegelinie y" ||||||||||||||||||||||||||||||/*)
5.749 +
5.750 +(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*\<rightarrow>Add_Given "AbleitungBiegelinie dy"*)
5.751 +(*[1], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Apply_Method ["Biegelinien", "ausBelastung"]*)
5.752 +(*[1, 1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Rewrite ("sym_neg_equal_iff_equal", "(?a1 = ?b1) = (- ?a1 = - ?b1)")*)
5.753 +(*[1, 1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Rewrite ("Belastung_Querkraft", "- qq ?x = Q' ?x")*)
5.754 +(*[1, 2], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow>Subproblem ("Biegelinie", ["named", "integrate", "function"])*)
5.755 +(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Model_Problem*)
5.756 +(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "functionTerm (- q_0)"*)
5.757 +(*[1, 3], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "integrateBy x"*)
5.758 +
5.759 +(*/------------------- check result of Add_Given "functionTerm (- q_0)" --------------------\*)
5.760 +if p = ([1, 3], Pbl) andalso
5.761 + f = Test_Out.PpcKF (Test_Out.Problem [], {Find = [Incompl "antiDerivativeName"],
5.762 + Given = [Incompl "integrateBy", Correct "functionTerm (- q_0)"],
5.763 + Relate = [], Where = [], With = []})
5.764 +then
5.765 + (case nxt of Add_Given "integrateBy x" => () | _ => error "specify-phase: low level CHANGED 1")
5.766 +else error "specify-phase: low level CHANGED 2";
5.767 +(*\------------------- check result of Add_Given "functionTerm (- q_0)" --------------------/*)
5.768 \<close> ML \<open>
5.769 \<close> ML \<open>
5.770 \<close>