1.1 --- a/src/Tools/isac/MathEngBasic/model-def.sml Sun Feb 19 10:29:58 2023 +0100
1.2 +++ b/src/Tools/isac/MathEngBasic/model-def.sml Sun Feb 19 13:03:54 2023 +0100
1.3 @@ -82,6 +82,8 @@
1.4 (values)) * (* set of values for element-wise input *)
1.5 (term * (* penv delayed to future?: variable from Model_Pattern *)
1.6 (term list)) (* set of values for element-wise input *)
1.7 +(*Inp (descriptor * string (*Input gives hints on input format in string*)
1.8 + respective test is saved in Test_Theory.thy *)
1.9 | Syn of TermC.as_string (* PIDE: contains "(__=__)" etc *)
1.10 | Typ of TermC.as_string (* type error: drop with PIDE ? *)
1.11 | Inc of (descriptor * values) * (term * (term list)) (* penv -?- *)
2.1 --- a/src/Tools/isac/Specify/i-model.sml Sun Feb 19 10:29:58 2023 +0100
2.2 +++ b/src/Tools/isac/Specify/i-model.sml Sun Feb 19 13:03:54 2023 +0100
2.3 @@ -25,6 +25,7 @@
2.4 val to_string: Proof.context -> T -> string
2.5
2.6 datatype add_single = Add of single | Err of string
2.7 +(*val init: Proof.context -> Model_Pattern.T -> T*)
2.8 val init: Model_Pattern.T -> T
2.9 val init_TEST: Proof.context -> Model_Pattern.T -> T
2.10 val check_single: Proof.context -> m_field -> O_Model.T -> T -> Model_Pattern.T ->
2.11 @@ -119,7 +120,9 @@
2.12 fun pat_to_item (m_field, (descriptor, _)) =
2.13 (0, [], false, m_field, Syn (UnparseC.term ctxt descriptor ^ " " ^ empty_for (type_of descriptor)))
2.14 in map pat_to_item model_patt end
2.15 -
2.16 +(*########################* )
2.17 +val init = init_TEST
2.18 +( *########################*)
2.19
2.20 (** check input on a model **)
2.21
3.1 --- a/src/Tools/isac/Specify/specify-step.sml Sun Feb 19 10:29:58 2023 +0100
3.2 +++ b/src/Tools/isac/Specify/specify-step.sml Sun Feb 19 13:03:54 2023 +0100
3.3 @@ -44,8 +44,8 @@
3.4 | check (Tactic.Del_Relation ct') _ = Applicable.Yes (Tactic.Del_Relation' ct')
3.5 | check Tactic.Model_Problem (pt, pos as (p, _)) =
3.6 let
3.7 - val pI' = case Ctree.get_obj I pt p of
3.8 - Ctree.PblObj {origin = (_, (_, pI', _),_), ...} => pI'
3.9 + val (pI', ctxt) = case Ctree.get_obj I pt p of
3.10 + Ctree.PblObj {origin = (_, (_, pI', _), _), ctxt, ...} => (pI', ctxt)
3.11 | _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj"
3.12 val {model, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
3.13 val pbl = I_Model.init model
4.1 --- a/src/Tools/isac/Specify/step-specify.sml Sun Feb 19 10:29:58 2023 +0100
4.2 +++ b/src/Tools/isac/Specify/step-specify.sml Sun Feb 19 13:03:54 2023 +0100
4.3 @@ -253,7 +253,7 @@
4.4 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))
4.5 ([], (dI,pI,mI), hdl, ContextC.empty)
4.6 val pt = update_spec pt [] (dI, pI, mI)
4.7 - val pits = I_Model.init model
4.8 + val pits = I_Model.init (*Proof_Context.init_global thy*) model
4.9 val pt = update_pbl pt [] pits
4.10 in ((pt, ([] , Pbl)), []) end
4.11 else
4.12 @@ -265,7 +265,7 @@
4.13 val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)
4.14 ([], (dI, pI, mI)) ([], (dI, pI, mI), TermC.empty, ContextC.empty)
4.15 val pt = update_spec pt [] (dI, pI, mI)
4.16 - val mits = I_Model.init model
4.17 + val mits = I_Model.init (*Proof_Context.init_global thy*) model
4.18 val pt = update_met pt [] mits
4.19 in ((pt, ([], Met)), []) end
4.20 else (* new example, pepare for interactive modeling *)
5.1 --- a/test/Tools/isac/Test_Theory.thy Sun Feb 19 10:29:58 2023 +0100
5.2 +++ b/test/Tools/isac/Test_Theory.thy Sun Feb 19 13:03:54 2023 +0100
5.3 @@ -69,9 +69,440 @@
5.4 \<close> ML \<open>
5.5 \<close>
5.6
5.7 -section \<open>===================================================================================\<close>
5.8 +section \<open>=========="Minisubpbl/150a-add-given-Maximum.sml"==================================\<close>
5.9 ML \<open>
5.10 \<close> ML \<open>
5.11 +(* Title: "Minisubpbl/150a-add-given-Maximum.sml"
5.12 + Author: Walther Neuper 1105
5.13 + (c) copyright due to lincense terms.
5.14 +
5.15 +Note: This test --- steps into me --- more than once, to a somewhat extreme extent;
5.16 + in order not to get lost while working in Test_Some etc,
5.17 + re-introduce ML (*--- step into XXXXX ---*) and Co.
5.18 + and use Sidekick for orientation.
5.19 + Nesting is indicated by /--- //-- ///- at the left margin of the comments.
5.20 +*)
5.21 +
5.22 +open Test_Code
5.23 +open Pos
5.24 +open Ctree
5.25 +open Tactic
5.26 +
5.27 +\<close> ML \<open>
5.28 +val (_(*example text*),
5.29 + (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
5.30 + "Extremum (A = 2 * u * v - u \<up> 2)" ::
5.31 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
5.32 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
5.33 + "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
5.34 + "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
5.35 + "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
5.36 + "ErrorBound (\<epsilon> = (0::real))" :: []),
5.37 + refs as ("Diff_App",
5.38 + ["univariate_calculus", "Optimisation"],
5.39 + ["Optimisation", "by_univariate_calculus"])))
5.40 + = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
5.41 +
5.42 +val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(model, refs)]; val Model_Problem = nxt;
5.43 +val c = [];
5.44 +
5.45 +\<close> ML \<open>
5.46 +(*+*)val PblObj {ctxt, ...} = get_obj I pt [];
5.47 +(*+*)Proof_Context.theory_of ctxt (*= {Pure, .., Diff_App}*);
5.48 +(*val Free ("r", TFree ("'a", [])) = Syntax.read_term ctxt "r" ..ERROR until cs.b7a2ad3b3d45*)
5.49 +(*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term ctxt "r"
5.50 +
5.51 +\<close> text \<open>
5.52 +val return_me_Model_Problem =
5.53 + me nxt p c pt; val Add_Given "Constants [r = 7]" = #4 return_me_Model_Problem;
5.54 +\<close> ML \<open> (*/------------ step into me Model_Problem ------------------------------------------\\*)
5.55 +(*/------------------- step into me Model_Problem ------------------------------------------\\*)
5.56 +"~~~~~ fun me , args:"; val (tac, (p:Pos.pos'), (_:Test_Code.NEW), (pt:Ctree.ctree)) = (nxt, p, c, pt);
5.57 + val (pt, p) =
5.58 + (*ERROR Specify.item_to_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt ... see 100-init-rootpbl.sml*)
5.59 + case Step.by_tactic tac (pt,p) of
5.60 + ("ok", (_, _, ptp)) => ptp;
5.61 +
5.62 +\<close> text \<open>
5.63 +(*val ("ok", (ts as (_, _, _) :: _, _, _)) = (*case*)*)
5.64 +val return_do_next = (*case*)
5.65 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
5.66 +\<close> text \<open>
5.67 +val ts = return_do_next |> #2 |> #1 |> hd (* keep for continuing me Model_Problem *)
5.68 +val continue_Model_Problem = (ts, (pt, p)) (* keep for continuing me Model_Problem *);
5.69 +\<close> ML \<open> (*//----------- step into do_next ---------------------------------------------------\\*)
5.70 +(*//------------------ step into do_next ---------------------------------------------------\\*)
5.71 +"~~~~~ fun do_next , args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) =
5.72 + (p, ((pt, e_pos'),[]));
5.73 + val pIopt = get_pblID (pt,ip);
5.74 + (*if*) ip = ([],Res); (* = false*)
5.75 + val _ = (*case*) tacis (*of*);
5.76 + val SOME _ = (*case*) pIopt (*of*);
5.77 +
5.78 +\<close> text \<open>
5.79 + val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
5.80 + Step.switch_specify_solve p_ (pt, ip);
5.81 +\<close> ML \<open>
5.82 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
5.83 + (*if*) Pos.on_specification ([], state_pos) (*then*);
5.84 +
5.85 +\<close> text \<open>
5.86 + val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
5.87 + Step.specify_do_next (pt, input_pos);
5.88 +\<close> ML \<open> (*///---------- step into specify_do_next -------------------------------------------\\*)
5.89 +(*///----------------- step into specify_do_next -------------------------------------------\\*)
5.90 +"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
5.91 +
5.92 +(* val (_, (p_', tac)) =*)
5.93 +val return_find_next_step = (*keep for continuing specify_do_next*)
5.94 + Specify.find_next_step ptp;
5.95 +\<close> ML \<open> (*////--------- step into find_next_step --------------------------------------------\\*)
5.96 +(*////---------------- step into find_next_step --------------------------------------------\\*)
5.97 +"~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
5.98 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
5.99 + spec = refs, ...} = Calc.specify_data (pt, pos);
5.100 + val ctxt = Ctree.get_ctxt pt pos;
5.101 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
5.102 + (*if*) p_ = Pos.Pbl (*then*);
5.103 +
5.104 + Specify.for_problem ctxt oris (o_refs, refs) (pbl, met);
5.105 +"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
5.106 + = (ctxt, oris, (o_refs, refs), (pbl, met));
5.107 + val cdI = if dI = ThyC.id_empty then dI' else dI;
5.108 + val cpI = if pI = Problem.id_empty then pI' else pI;
5.109 + val cmI = if mI = MethodC.id_empty then mI' else mI;
5.110 + val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
5.111 + val {model = mpc, ...} = MethodC.from_store ctxt cmI
5.112 + val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0;
5.113 + (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
5.114 + (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
5.115 + (*case*) find_first (I_Model.is_error o #5) pbl (*of*);
5.116 +
5.117 +\<close> text \<open>
5.118 + (*case*)
5.119 + Specify.item_to_add (ThyC.get_theory ctxt
5.120 + (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
5.121 +\<close> ML \<open>
5.122 +"~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
5.123 + = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl);
5.124 + fun testr_vt v ori = member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"
5.125 + fun testi_vt v itm = member op= (#2 (itm : I_Model.single)) v
5.126 + fun test_id ids r = member op= ids (#1 (r : O_Model.single))
5.127 + fun test_subset itm (_, _, _, d, ts) =
5.128 + (I_Model.descriptor (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.o_model_values (#5 itm), ts)
5.129 + fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
5.130 + | false_and_not_Sup (_, _, false, _, _) = true
5.131 + | false_and_not_Sup _ = false
5.132 + val v = if itms = [] then 1 else I_Model.max_variant itms
5.133 + val vors = if v = 0 then oris else filter (testr_vt v) oris
5.134 + val vits =
5.135 + if v = 0
5.136 + then itms (* because of dsc without dat *)
5.137 + else filter (testi_vt v) itms; (* itms..vat *)
5.138 +\<close> ML \<open>
5.139 + val icl = filter false_and_not_Sup vits; (* incomplete *)
5.140 + (*if*) icl = [] (*else*);
5.141 +\<close> text \<open>
5.142 +val SOME ori =
5.143 + (*case*) find_first (test_subset (hd icl)) vors (*of*);
5.144 +\<close> ML \<open> (*\\\\--------- step into find_next_step --------------------------------------------//*)
5.145 +(*\\\\---------------- step into find_next_step --------------------------------------------//*)
5.146 +\<close> ML \<open> (*|||---------- continuing specify_do_next --------------------------------------------*)
5.147 +(*|||----------------- continuing specify_do_next --------------------------------------------*)
5.148 +val (_, (p_', tac)) = return_find_next_step (*kept for continuing specify_do_next*)
5.149 +
5.150 + val ist_ctxt = Ctree.get_loc pt (p, p_)
5.151 +\<close> ML \<open>
5.152 +(*NEW for repair*)val Del_Given "Constants [__=__, __=__]" = tac (*<--- #######################*)
5.153 +\<close> ML \<open>
5.154 +(*+*)val Add_Given "Constants [r = 7]" = tac
5.155 +\<close> ML \<open>
5.156 +val _ =
5.157 + (*case*) tac (*of*);
5.158 +
5.159 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
5.160 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =
5.161 + (tac, (pt, (p, p_')));
5.162 +
5.163 + Specify.by_Add_ "#Given" ct ptp;
5.164 +"~~~~~ fun by_Add_ , args:"; val (m_field, ct ,(pt, pos as (_, p_))) =
5.165 + ("#Given", ct, ptp);
5.166 + val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
5.167 + val (i_model, m_patt) =
5.168 + if p_ = Pos.Met then
5.169 + (met,
5.170 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
5.171 + else
5.172 + (pbl,
5.173 + (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model);
5.174 + (*case*)
5.175 + I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
5.176 +"~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, (str(*, pos*))) =
5.177 + (ctxt, m_field, oris, i_model, m_patt, ct);
5.178 +(*new*) val (t as (descriptor $ _)) = Syntax.read_term ctxt str
5.179 +
5.180 +(*+*)val "Constants [r = 7]" = UnparseC.term @{context} t;
5.181 +
5.182 +(*new*)val SOME m_field' =
5.183 +(*new*) (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
5.184 +(*new*) (*if*) m_field <> m_field' (*else*);
5.185 +
5.186 +(*+*)val "#Given" = m_field; val "#Given" = m_field'
5.187 +
5.188 +(*new*)val (msg, _, _) =
5.189 +(*new*) (*case*) O_Model.contains ctxt m_field o_model t (*of*);
5.190 +
5.191 +(*+*)val (_, _, _, _, vals) = hd o_model;
5.192 +(*+*)val "Constants [r = 7]" = UnparseC.term @{context} (@{term Constants} $ (hd vals));
5.193 +(*+*) if "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), " ^
5.194 +(*+*) "\n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), " ^
5.195 +(*+*) "\n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), " ^
5.196 +(*+*) "\n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), " ^
5.197 +(*+*) "\n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), " ^
5.198 +(*+*) "\n(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), " ^
5.199 +(*+*) "\n(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), " ^
5.200 +(*+*) "\n(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), " ^
5.201 +(*+*) "\n(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), " ^
5.202 +(*+*) "\n(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), " ^
5.203 +(*+*) "\n(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
5.204 +(*+*) = O_Model.to_string @{context} o_model then () else error "o_model CHANGED";
5.205 +\<close> ML \<open> (*\\----------- step into into do_next ----------------------------------------------//*)
5.206 +(*\\------------------ step into into do_next ----------------------------------------------//*)
5.207 +
5.208 +\<close> ML \<open> (*|------------ continue with me Model_Problem ----------------------------------------*)
5.209 +(*|------------------- continue with me Model_Problem ----------------------------------------*)
5.210 +val (ts, (pt, p)) = continue_Model_Problem;
5.211 +val ("ok", (ts as (_, _, _) :: _, _, _)) = return_do_next
5.212 +
5.213 +val tacis as (_::_) =
5.214 + (*case*) ts (*of*);
5.215 + val (tac, _, _) = last_elem tacis
5.216 +
5.217 +val return = (p, [] : NEW,
5.218 + TESTg_form ctxt (pt, p), tac, Celem.Sundef, pt);
5.219 +"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt, p));
5.220 + val (form, _, _) = ME_Misc.pt_extract ctxt ptp
5.221 +val Ctree.ModSpec (_, p_, _, gfr, where_, _) =
5.222 + (*case*) form (*of*);
5.223 +
5.224 +(*+*)val Pos.Pbl = p_;
5.225 + Test_Out.PpcKF ( (Test_Out.Problem [],
5.226 + P_Model.from (Proof_Context.theory_of ctxt) gfr where_));
5.227 +
5.228 + P_Model.from (Proof_Context.theory_of ctxt) gfr where_;
5.229 +"~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
5.230 + fun coll model [] = model
5.231 + | coll model ((_, _, _, field, itm_) :: itms) =
5.232 + coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
5.233 +
5.234 + val gfr = coll P_Model.empty itms;
5.235 +"~~~~~ fun coll , args:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: itms))
5.236 + = (P_Model.empty, itms);
5.237 +
5.238 +(*+*)val 4 = length itms;
5.239 +(*+*)val itm = nth 1 itms;
5.240 +
5.241 + coll P_Model.empty [itm];
5.242 +"~~~~~ fun coll , iterate:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: []))
5.243 + = (P_Model.empty, [itm]);
5.244 +
5.245 + (add_sel_ppc thy field model (item_from_feedback thy itm_));
5.246 +"~~~~~ fun add_sel_ppc , args:"; val ((_: theory), sel, {Given = gi, Where = wh, Find = fi, With = wi, Relate = re}, x )
5.247 + = (thy, field, model, (item_from_feedback thy itm_));
5.248 +
5.249 + P_Model.item_from_feedback thy itm_;
5.250 +"~~~~~ fun item_from_feedback , args:"; val (thy, (I_Model.Inc ((d, ts), _))) = (thy, itm_);
5.251 + P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)));
5.252 +\<close> ML \<open> (*\------------ step into into me Model_Problem -------------------------------------//*)
5.253 +(*\------------------- step into into me Model_Problem -------------------------------------//*)
5.254 +val (p, _, f, nxt, _, pt) = return_me_Model_Problem
5.255 +
5.256 +\<close> ML \<open>
5.257 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Maximum A" = nxt;
5.258 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u]" = nxt;
5.259 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [v]" = nxt;
5.260 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)" = nxt;
5.261 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" = nxt;
5.262 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Diff_App" = nxt;
5.263 +val return_me_Specify_Theory
5.264 + = me nxt p c pt; val Specify_Problem ["univariate_calculus", "Optimisation"] = #4 return_me_Specify_Theory;
5.265 +
5.266 +\<close> ML \<open> (*/------------ step into me Specify_Theory -----------------------------------------\\*)
5.267 +(*/------------------- step into me Specify_Theory -----------------------------------------\\*)
5.268 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
5.269 + val ctxt = Ctree.get_ctxt pt p
5.270 + val (pt, p) =
5.271 + case Step.by_tactic tac (pt, p) of
5.272 + ("ok", (_, _, ptp)) => ptp
5.273 +
5.274 +val ("ok", (ts as (_, _, _) :: _, _, _)) =
5.275 + (*case*)
5.276 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
5.277 +\<close> ML \<open> (*//----------- step into do_next ---------------------------------------------------\\*)
5.278 +(*//------------------ step into do_next ---------------------------------------------------\\*)
5.279 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
5.280 + = (p, ((pt, Pos.e_pos'), [])) (*of*);
5.281 + (*if*) Pos.on_calc_end ip (*else*);
5.282 + val (_, probl_id, _) = Calc.references (pt, p);
5.283 +val _ =
5.284 + (*case*) tacis (*of*);
5.285 + (*if*) probl_id = Problem.id_empty (*else*);
5.286 +
5.287 + Step.switch_specify_solve p_ (pt, ip);
5.288 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
5.289 + (*if*) Pos.on_specification ([], state_pos) (*then*);
5.290 +
5.291 + Step.specify_do_next (pt, input_pos);
5.292 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
5.293 + val (_, (p_', tac)) = Specify.find_next_step ptp
5.294 + val ist_ctxt = Ctree.get_loc pt (p, p_);
5.295 + (*case*) tac (*of*);
5.296 +
5.297 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
5.298 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Problem pI), (pt, pos as (p, _)))
5.299 + = (tac, (pt, (p, p_')));
5.300 + val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
5.301 + PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
5.302 + (oris, dI, dI', pI', probl, ctxt)
5.303 + val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
5.304 + val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
5.305 +\<close> ML \<open>(*\\------------ step into do_next ---------------------------------------------------//*)
5.306 +(*\\------------------ step into do_next ---------------------------------------------------//*)
5.307 +\<close> ML \<open> (*\------------ step into me Specify_Theory -----------------------------------------//*)
5.308 +(*\------------------- step into me Specify_Theory -----------------------------------------//*)
5.309 +val (p,_,f,nxt,_,pt) = return_me_Specify_Theory;
5.310 +
5.311 +val return_me_Specify_Problem (* keep for continuing me *)
5.312 + = me nxt p c pt; val Specify_Method ["Optimisation", "by_univariate_calculus"] = #4 return_me_Specify_Problem;
5.313 +\<close> ML \<open> (*/------------ step into me Specify_Problem ----------------------------------------\\*)
5.314 +(*/------------------- step into me Specify_Problem ----------------------------------------\\*)
5.315 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
5.316 + val ctxt = Ctree.get_ctxt pt p
5.317 +
5.318 +(** ) val ("ok", (_, _, ptp as (pt, p))) =( **)
5.319 +(**) val return_by_tactic =(**) (*case*)
5.320 + Step.by_tactic tac (pt, p) (*of*);
5.321 +\<close> ML \<open> (*//----------- step into by_tactic -------------------------------------------------\\*)
5.322 +(*//------------------ step into by_tactic -------------------------------------------------\\*)
5.323 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
5.324 +
5.325 + (*case*)
5.326 + Step.check tac (pt, p) (*of*);
5.327 +"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
5.328 + (*if*) Tactic.for_specify tac (*then*);
5.329 +
5.330 +Specify_Step.check tac (ctree, pos);
5.331 +"~~~~~ fun check , args:"; val ((Tactic.Specify_Problem pID), (pt, pos as (p, _)))
5.332 + = (tac, (ctree, pos));
5.333 + val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
5.334 + Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
5.335 + => (oris, dI, pI, dI', pI', itms)
5.336 + val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
5.337 +\<close> ML \<open> (*\\----------- step into by_tactic -------------------------------------------------//*)
5.338 +(*\\------------------ step into by_tactic -------------------------------------------------//*)
5.339 +val ("ok", (_, _, ptp as (pt, p))) = return_by_tactic (* kept for continuing me *);
5.340 +
5.341 + (*case*)
5.342 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
5.343 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
5.344 + (*if*) Pos.on_calc_end ip (*else*);
5.345 + val (_, probl_id, _) = Calc.references (pt, p);
5.346 +val _ =
5.347 + (*case*) tacis (*of*);
5.348 + (*if*) probl_id = Problem.id_empty (*else*);
5.349 +
5.350 + Step.switch_specify_solve p_ (pt, ip);
5.351 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
5.352 + (*if*) Pos.on_specification ([], state_pos) (*then*);
5.353 +
5.354 + Step.specify_do_next (pt, input_pos);
5.355 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
5.356 + val (_, (p_', tac)) = Specify.find_next_step ptp
5.357 + val ist_ctxt = Ctree.get_loc pt (p, p_)
5.358 +val _ =
5.359 + (*case*) tac (*of*);
5.360 +
5.361 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
5.362 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos))
5.363 + = (tac, (pt, (p, p_')));
5.364 +
5.365 + val (o_model, ctxt, i_model) =
5.366 +Specify_Step.complete_for id (pt, pos);
5.367 +"~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
5.368 + val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
5.369 + ...} = Calc.specify_data (ctree, pos);
5.370 + val ctxt = Ctree.get_ctxt ctree pos
5.371 + val (dI, _, _) = References.select_input o_refs refs;
5.372 + val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
5.373 + val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
5.374 + val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
5.375 + val thy = ThyC.get_theory ctxt dI
5.376 + val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
5.377 +\<close> ML \<open> (*\------------ step into me Specify_Problem ----------------------------------------//*)
5.378 +(*\------------------- step into me Specify_Problem ----------------------------------------//*)
5.379 +val (p,_,f,nxt,_,pt) = return_me_Specify_Problem
5.380 +
5.381 +val return_me_Add_Given_FunctionVariable
5.382 + = me nxt p c pt; val Add_Given "FunctionVariable a" = #4 return_me_Add_Given_FunctionVariable;
5.383 +\<close> ML \<open> (*/------------ step into me Specify_Method -----------------------------------------\\*)
5.384 +(*/------------------- step into me Specify_Method -----------------------------------------\\*)
5.385 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
5.386 + val ctxt = Ctree.get_ctxt pt p
5.387 + val (pt, p) =
5.388 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
5.389 + case Step.by_tactic tac (pt, p) of
5.390 + ("ok", (_, _, ptp)) => ptp;
5.391 +
5.392 + (*case*)
5.393 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
5.394 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
5.395 + (*if*) Pos.on_calc_end ip (*else*);
5.396 + val (_, probl_id, _) = Calc.references (pt, p);
5.397 +val _ =
5.398 + (*case*) tacis (*of*);
5.399 + (*if*) probl_id = Problem.id_empty (*else*);
5.400 +
5.401 + Step.switch_specify_solve p_ (pt, ip);
5.402 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
5.403 + (*if*) Pos.on_specification ([], state_pos) (*then*);
5.404 +
5.405 + Step.specify_do_next (pt, input_pos);
5.406 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
5.407 +
5.408 + val (_, (p_', tac)) =
5.409 + Specify.find_next_step ptp;
5.410 +"~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
5.411 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
5.412 + spec = refs, ...} = Calc.specify_data (pt, pos);
5.413 + val ctxt = Ctree.get_ctxt pt pos;
5.414 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
5.415 + (*if*) p_ = Pos.Pbl (*else*);
5.416 +
5.417 + Specify.for_method ctxt oris (o_refs, refs) (pbl, met);
5.418 +"~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
5.419 + = (ctxt, oris, (o_refs, refs), (pbl, met));
5.420 + val cmI = if mI = MethodC.id_empty then mI' else mI;
5.421 + val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
5.422 + val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0;
5.423 +val NONE =
5.424 + (*case*) find_first (I_Model.is_error o #5) met (*of*);
5.425 +
5.426 + (*case*)
5.427 + Specify.item_to_add (ThyC.get_theory ctxt
5.428 + (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
5.429 +"~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
5.430 + = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
5.431 +\<close> ML \<open> (*\------------ step into me Specify_Method -----------------------------------------//*)
5.432 +(*\------------------- step into me Specify_Method -----------------------------------------//*)
5.433 +val (p,_,f,nxt,_,pt) = return_me_Add_Given_FunctionVariable
5.434 +
5.435 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Input_Descript.Domain {0<..<r}" = nxt;
5.436 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "ErrorBound (\<epsilon> = 0)" = nxt;
5.437 +(*
5.438 + nxt would be Tactic.Apply_Method, which tries to determine a next step in the ***Program***,
5.439 + but the ***Program*** is not yet perfectly implemented.
5.440 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.441 +*)
5.442 \<close> ML \<open>
5.443 \<close> ML \<open>
5.444 \<close>