1.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Tue Oct 03 16:33:54 2023 +0200
1.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Wed Oct 25 12:34:12 2023 +0200
1.3 @@ -788,8 +788,10 @@
1.4 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos))
1.5 = (tac, (pt, (p, p_')));
1.6
1.7 - val (o_model, ctxt, i_model) =
1.8 +(**)val return_complete_for =(**)
1.9 +(** ) val (o_model, ctxt, i_model) =( **)
1.10 Specify_Step.complete_for id (pt, pos);
1.11 +(*//------------------ step into complete_for ----------------------------------------------\\*)
1.12 "~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
1.13 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
1.14 ...} = Calc.specify_data (ctree, pos);
1.15 @@ -798,23 +800,123 @@
1.16 val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
1.17 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
1.18 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
1.19 - val thy = ThyC.get_theory ctxt dI
1.20 - val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
1.21 +
1.22 +(**)val return_match_itms_oris = (**)
1.23 +(** )val (_, (i_model, _)) = ( **)
1.24 + M_Match.match_itms_oris ctxt o_model' (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST i_prob)
1.25 + (m_patt, where_, where_rls);
1.26 +(*///----------------- step into match_itms_oris -------------------------------------------\\*)
1.27 +"~~~~~ fun match_itms_oris, args:"; val (ctxt, o_model, (pbl_imod, met_imod), (m_patt, where_, where_rls)) =
1.28 + (ctxt, o_model', (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST i_prob), (m_patt, where_, where_rls));
1.29 +
1.30 +(**)val return_fill_method =(**)
1.31 +(** )val met_imod =( **)
1.32 + fill_method o_model (pbl_imod, met_imod) m_patt;
1.33 +(*////--------------- step into fill_method -----------------------------------------------\\*)
1.34 +"~~~~~ fun fill_method , args:"; val (o_model, (pbl_imod, met_imod), met_patt) =
1.35 + (o_model, (pbl_imod, met_imod), m_patt);
1.36 +
1.37 + val pbl_max_vnts as [2, 1] = Model_Def.max_variants o_model pbl_imod
1.38 +
1.39 + (*probably pbl/met_imod = [], so take met_patt; if empty return Sup*)
1.40 + val i_from_met = map (fn (_, (descr, _)) => (*order from met_patt*)
1.41 + Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt (*\<longrightarrow> right order for args*)
1.42 +(*+MET: Sup..*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
1.43 + = i_from_met |> I_Model.to_string_TEST @{context}
1.44 +
1.45 + val met_max_vnts as [2, 1] = Model_Def.max_variants o_model i_from_met;
1.46 + val max_vnt as 2 = hd (inter op= pbl_max_vnts met_max_vnts);
1.47 + (*add items from pbl_imod (without overwriting existing items in met_imod)*)
1.48 +
1.49 +val return_add_other = map (
1.50 + add_other max_vnt pbl_imod) i_from_met;
1.51 +(*/////-------------- step into add_other -------------------------------------------------\\*)
1.52 +"~~~~~ fun add_other_5 , args:"; val (max_vnt, i1_model, (i2, _, bool2, m_field2, (Sup_TEST (descr2, ts2), pos2))) =
1.53 + (max_vnt, pbl_imod, nth 5 i_from_met);
1.54 +(*+*)val Const ("Input_Descript.FunctionVariable", _) = descr2;
1.55 +
1.56 +val (_, vnts1, _, _, (feedb1, _)) = (i2, [], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2))
1.57 +val SOME (descr1 as (Const ("Input_Descript.FunctionVariable", _)) ) =
1.58 + get_dscr' feedb1
1.59 +val true =
1.60 + descr1 = descr2
1.61 +val true =
1.62 + Model_Def.member_vnt vnts1 max_vnt
1.63 +val NONE =
1.64 + find_first (fn (_, vnts1, _, _, (feedb1, _)) => case get_dscr' feedb1 of
1.65 + NONE => false
1.66 + | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model
1.67 +
1.68 +val return_add_other_1 = (i2, [max_vnt], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2))
1.69 +val check as true = return_add_other_1 = nth 5 return_add_other
1.70 +(*\\\\\-------------- step into add_other -------------------------------------------------//*)
1.71 + val i_from_pbl = return_add_other
1.72 +(*\\\\---------------- step into fill_method -----------------------------------------------//*)
1.73 +val return_fill_method_step = filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) i_from_met
1.74 +
1.75 +(*+MET: dropped ALL DUE TO is_empty_single_TEST*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]" =
1.76 + return_fill_method_step |> I_Model.to_string_TEST @{context}
1.77 +(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
1.78 + = return_fill_method |> I_Model.to_string_TEST @{context};
1.79 +return_fill_method_step = return_fill_method; (*latter is correct, did not investigate further*)
1.80 +(*\\\----------------- step into match_itms_oris -------------------------------------------//*)
1.81 +val (_, (i_model, _)) = return_match_itms_oris;
1.82 +
1.83 +(*||------------------ continue. complete_for ------------------------------------------------*)
1.84 + val (o_model, ctxt, i_model) = return_complete_for
1.85 +(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
1.86 + = i_model |> I_Model.to_string_TEST @{context}
1.87 +(*+isa2:MET.Mis* ) val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(7 ,[1] ,false ,#Given ,Mis FunctionVariable funvar), \n(10 ,[1, 2] ,false ,#Given ,Mis Input_Descript.Domain doma), \n(12 ,[1, 2, 3] ,false ,#Given ,Mis ErrorBound err)]" =
1.88 + i_model |> I_Model.to_string @{context} ( *+isa2*)
1.89 +(*\\------------------ step into complete_for ----------------------------------------------//*)
1.90 + val (o_model, ctxt, i_model) = return_complete_for
1.91 +
1.92 +(*|------------------- continue. complete_for ------------------------------------------------*)
1.93 +val return_complete_for_step = (o_model', ctxt', i_model)
1.94 +
1.95 +val (o_model'_step, i_model_step) = (#1 return_complete_for_step, #3 return_complete_for_step)
1.96 +val (o_model', i_model) = (#1 return_complete_for, #3 return_complete_for)
1.97 +;
1.98 +if (o_model'_step, i_model_step) = (o_model', i_model)
1.99 +then () else error "return_complete_for_step <> return_complete_for";
1.100 (*\------------------- step into me Specify_Problem ----------------------------------------//*)
1.101 val (p,_,f,nxt,_,pt) = return_me_Specify_Problem
1.102
1.103 -val return_me_Add_Given_FunctionVariable
1.104 - = me nxt p c pt; val Add_Given "FunctionVariable a" = #4 return_me_Add_Given_FunctionVariable;
1.105 -(*/------------------- step into me Specify_Method -----------------------------------------\\*)
1.106 +val return_me_Specify_Method
1.107 + = me nxt p c pt; val Add_Given "FunctionVariable b" = #4 return_me_Specify_Method;
1.108 +(*/------------------- step into me_Specify_Method -----------------------------------------\\*)
1.109 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
1.110 +
1.111 +(*+isa==isa2*)val "[]" =(*+*) get_obj g_met pt (fst p) |> I_Model.to_string @{context}
1.112 +
1.113 val ctxt = Ctree.get_ctxt pt p
1.114 val (pt, p) =
1.115 - (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
1.116 case Step.by_tactic tac (pt, p) of
1.117 ("ok", (_, _, ptp)) => ptp;
1.118
1.119 +(*quick step into --> me_Specify_Method*)
1.120 +(*+*)val Specify_Method ["Optimisation", "by_univariate_calculus"] = tac;
1.121 +(* Step.by_tactic*)
1.122 +"~~~~~ fun by_tactic , args:"; val () = ();
1.123 +(* Step.check*)
1.124 +"~~~~~ fun check , args:"; val () = ();
1.125 +(*Specify_Step.check (Tactic.Specify_Method*)
1.126 +"~~~~~ fun check , args:"; val () = ();
1.127 +(*Specify_Step.complete_for*)
1.128 +"~~~~~ fun complete_for , args:"; val () = ();
1.129 +(* M_Match.match_itms_oris*)
1.130 +"~~~~~ fun match_itms_oris , args:"; val () = ();
1.131 +
1.132 +(*+*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(0 ,[2] ,false ,i_model_empty ,Sup FunctionVariable), \n(0 ,[2] ,false ,i_model_empty ,Sup Input_Descript.Domain), \n(0 ,[2] ,false ,i_model_empty ,Sup ErrorBound), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str)]"
1.133 + = get_obj g_met pt (fst p) |> I_Model.to_string @{context};
1.134 +(*
1.135 +(*+isa: METHOD.drop* )val"[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str)]" =( *+isaALLcorrect*)
1.136 +(*+isa2:METHOD.Mis*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(7 ,[1] ,false ,#Given ,Mis FunctionVariable funvar), \n(10 ,[1, 2] ,false ,#Given ,Mis Input_Descript.Domain doma), \n(12 ,[1, 2, 3] ,false ,#Given ,Mis ErrorBound err)]" =(*isa2*)
1.137 + get_obj g_met pt (fst p) |> I_Model.to_string @ {context};
1.138 +*)
1.139 (*case*)
1.140 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
1.141 +(*//------------------ step into Step.do_next ----------------------------------------------\\*)
1.142 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
1.143 (*if*) Pos.on_calc_end ip (*else*);
1.144 val (_, probl_id, _) = Calc.references (pt, p);
1.145 @@ -823,10 +925,12 @@
1.146 (*if*) probl_id = Problem.id_empty (*else*);
1.147
1.148 Step.switch_specify_solve p_ (pt, ip);
1.149 +(*///----------------- step into Step.switch_specify_solve ---------------------------------\\*)
1.150 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
1.151 (*if*) Pos.on_specification ([], state_pos) (*then*);
1.152
1.153 Step.specify_do_next (pt, input_pos);
1.154 +(*////---------------- step into Step.specify_do_next --------------------------------------\\*)
1.155 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
1.156
1.157 val (_, (p_', tac)) =
1.158 @@ -838,7 +942,14 @@
1.159 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
1.160 (*if*) p_ = Pos.Pbl (*else*);
1.161
1.162 +(*+*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(0 ,[2] ,false ,i_model_empty ,Sup FunctionVariable), \n(0 ,[2] ,false ,i_model_empty ,Sup Input_Descript.Domain), \n(0 ,[2] ,false ,i_model_empty ,Sup ErrorBound), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str)]"
1.163 + = met |> I_Model.to_string @{context};
1.164 +(*isa2* )val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(7 ,[1] ,false ,#Given ,Mis FunctionVariable funvar), \n(10 ,[1, 2] ,false ,#Given ,Mis Input_Descript.Domain doma), \n(12 ,[1, 2, 3] ,false ,#Given ,Mis ErrorBound err)]"
1.165 + =( *isa2*) met |> I_Model.to_string @{context};
1.166 +
1.167 +(*isa2*)val ("dummy", (Met, Add_Given "FunctionVariable b")) =(*isa2*)
1.168 Specify.for_method ctxt oris (o_refs, refs) (pbl, met);
1.169 +(*///// /------------- step into Step.for_method -------------------------------------------\\*)
1.170 "~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (_, met))
1.171 = (ctxt, oris, (o_refs, refs), (pbl, met));
1.172 val cmI = if mI = MethodC.id_empty then mI' else mI;
1.173 @@ -847,13 +958,14 @@
1.174 val NONE =
1.175 (*case*) find_first (I_Model.is_error o #5) met (*of*);
1.176
1.177 +(*isa2*)val SOME ("#Given", "FunctionVariable b") =(*isa2*)
1.178 (*case*)
1.179 Specify.item_to_add (ThyC.get_theory ctxt
1.180 (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
1.181 "~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
1.182 = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
1.183 -(*\------------------- step into me Specify_Method -----------------------------------------//*)
1.184 -val (p,_,f,nxt,_,pt) = return_me_Add_Given_FunctionVariable
1.185 +(*\------------------- step into me_Specify_Method -----------------------------------------//*)
1.186 +val (p,_,f,nxt,_,pt) = return_me_Specify_Method
1.187
1.188 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Input_Descript.Domain {0<..<r}" = nxt;
1.189 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "ErrorBound (\<epsilon> = 0)" = nxt;