54 (tac, (pt, (p, p_'))); |
54 (tac, (pt, (p, p_'))); |
55 |
55 |
56 val (o_model, ctxt, i_model) = |
56 val (o_model, ctxt, i_model) = |
57 Specify_Step.complete_for id (pt, pos); |
57 Specify_Step.complete_for id (pt, pos); |
58 "~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos)); |
58 "~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos)); |
59 val {origin = (o_model, _, _), probl = i_prob, ctxt, |
59 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = met_imod, ctxt, |
60 ...} = Calc.specify_data (ctree, pos); |
60 ...} = Calc.specify_data (ctree, pos); |
|
61 val ctxt = Ctree.get_ctxt ctree pos |
|
62 val (dI, _, _) = References.select_input o_refs refs; |
61 val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID |
63 val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID |
62 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und)) |
64 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und)) |
63 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt) |
65 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt) |
64 |
66 |
65 val (_, (i_model, _)) = |
67 val (_, (i_model, _)) = |
66 M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model'; |
68 M_Match.match_itms_oris ctxt o_model' (I_Model.OLD_to_TEST i_prob, |
|
69 I_Model.OLD_to_TEST i_prob) (m_patt, where_, where_rls); |
67 "~~~~~ fun match_itms_oris , args:"; val (ctxt, pbl, (pbt, where_, where_rls), oris) = |
70 "~~~~~ fun match_itms_oris , args:"; val (ctxt, pbl, (pbt, where_, where_rls), oris) = |
68 (ctxt, i_prob, (m_patt, where_, where_rls), o_model'); |
71 (ctxt, i_prob, (m_patt, where_, where_rls), o_model'); |
69 (*0*)val mv = Pre_Conds.max_variant pbl; |
72 (*0*)val mv = Pre_Conds.max_variant pbl; |
70 |
73 |
71 fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.descriptor itm_; |
74 fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.descriptor itm_; |