1.1 --- a/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml	Sun Dec 10 17:35:07 2023 +0100
     1.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml	Mon Dec 11 09:24:02 2023 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4  (* Title:  "Minisubpbl/200-start-method-NEXT_STEP.sml"
     1.5     Author: Walther Neuper 1105
     1.6 -   (c) copyright due to lincense terms.
     1.7 +   (c) copyright due to lincense terms. 
     1.8  *)
     1.9  
    1.10  open Ctree;
    1.11 @@ -67,35 +67,29 @@
    1.12      val (_, (i_model, _)) = 
    1.13     M_Match.by_i_models ctxt o_model' (I_Model.OLD_to_POS i_prob,
    1.14                              I_Model.OLD_to_POS i_prob) (m_patt, where_, where_rls);
    1.15 -"~~~~~ fun by_i_models , args:"; val (ctxt, pbl, (pbt, where_, where_rls), oris) =
    1.16 -  (ctxt, i_prob, (m_patt, where_, where_rls), o_model');
    1.17 - (*0*)val mv = Pre_Conds.max_variant pbl;
    1.18 +"~~~~~ fun by_i_models , args:"; val (ctxt, o_model, (pbl_imod, met_imod), (met_patt, where_, where_rls)) =
    1.19 +  (ctxt, o_model, (I_Model.OLD_to_POS i_prob,(*<--? --v?*)
    1.20 +                            I_Model.OLD_to_POS i_prob), (m_patt, where_, where_rls));
    1.21 +     val met_imod = I_Model.fill_method o_model (pbl_imod, met_imod) met_patt
    1.22  
    1.23 -      fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;
    1.24 -      fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
    1.25 -				SOME _ => false | NONE => true;
    1.26 - (*1*)val mis = (filter (notmem pbl)) pbt;
    1.27 -
    1.28 -      fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
    1.29 -      fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
    1.30 - (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
    1.31 -      val news = (flat o (map (oris2itms oris))) mis;
    1.32 - (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
    1.33 -      val newitms = filter mem_vat news;
    1.34 - (*4*)val itms' = pbl @ newitms;
    1.35 -
    1.36 -      val (pb, where_') = Pre_Conds.check ctxt where_rls where_ 
    1.37 -        (pbt, I_Model.OLD_to_POS itms');
    1.38 +    val (check, preconds) =
    1.39 + Pre_Conds.check ctxt where_rls where_ (met_patt, met_imod);
    1.40  "~~~~~ fun check , args:"; val (ctxt, where_rls, where_, (model_patt, i_model)) =
    1.41 -  (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_POS itms'));
    1.42 +  (ctxt, where_rls, where_, (met_patt, met_imod));
    1.43        val (env_model, (env_subst, env_eval)) = make_environments model_patt i_model
    1.44        val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
    1.45        val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
    1.46        val full_subst = if env_eval = [] then pres_subst_other
    1.47          else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
    1.48  
    1.49 -(*+*)val "Test" = ctxt |> Proof_Context.theory_of |> ThyC.id_of
    1.50 -(*+*)val Rule_Set.Repeat {id = "prls_met_test_squ_sub", ...} = where_rls
    1.51 +(*+isa==isa2*)val "Test" = ctxt |> Proof_Context.theory_of |> ThyC.id_of
    1.52 +(*+isa==isa2*)val Rule_Set.Repeat {id = "prls_met_test_squ_sub", ...} = where_rls
    1.53 +(*+isa==isa2*)val [Const ("Test.precond_rootmet", _) $ Free ("v_v", _)] = where_
    1.54 +(*+*)val         "[\"(#Given, (equality, e_e))\", \"(#Given, (solveFor, v_v))\", \"(#Find, (solutions, v_v'i'))\"]"
    1.55 + = model_patt |> Model_Pattern.to_string ctxt(*+*)
    1.56 +(*+*)val         "[\n(1, [1], true ,#Given, (Cor_POS equality (x + 1 = 2) , pen2str, Position.T)), \n(2, [1], true ,#Given, (Cor_POS solveFor x , pen2str, Position.T)), \n(3, [1], true ,#Find, (Cor_POS solutions L , pen2str, Position.T))]"
    1.57 + = i_model |> I_Model.to_string_POS ctxt(*+*)
    1.58 +
    1.59  (*+*)val [(true, tTEST as Const ("Test.precond_rootmet", _) $ Free ("x", xxx))] = full_subst
    1.60  
    1.61  (*+*)val ctxt = Config.put rewrite_trace true ctxt;