1.1 --- a/test/Tools/isac/Minisubpbl/200-start-method.sml Mon Sep 25 08:39:43 2023 +0200
1.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method.sml Tue Sep 26 15:57:12 2023 +0200
1.3 @@ -63,14 +63,18 @@
1.4 LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) ist_ctxt (pt, (p, p_'));
1.5 "~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
1.6 ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));
1.7 - val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
1.8 - PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
1.9 - | _ => error "LI.by_tactic Apply_Method': uncovered case get_obj"
1.10 - val {model, ...} = MethodC.from_store ctxt mI;
1.11 - val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
1.12 + val (itms, oris, probl, o_spec, spec) = case get_obj I pt p of
1.13 + PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ...}
1.14 + => (itms, oris, probl, o_spec, spec)
1.15 + | _ => raise ERROR ""
1.16 + val (_, pI', _) = References.select_input o_spec spec
1.17 + val {model = pbl_patt, ...} = Problem.from_store ctxt pI';
1.18 + val {model = met_patt, ...} = MethodC.from_store ctxt mI;
1.19 + val (_, itms) = I_Model.s_make_complete oris
1.20 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pbl_patt, met_patt)
1.21
1.22 val (is, env, ctxt, prog) = case
1.23 - LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI of
1.24 + LItool.init_pstate ctxt itms mI of
1.25 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
1.26 | _ => error "LI.by_tactic Apply_Method': uncovered case init_pstate"
1.27 val ini = LItool.implicit_take ctxt prog env;