test/Tools/isac/Minisubpbl/200-start-method.sml
changeset 60754 bac1b22385e4
parent 60725 25233d8f7019
child 60757 9f4d7a352426
     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;