323 else |
323 else |
324 (pbl, |
324 (pbl, |
325 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model); |
325 (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model); |
326 |
326 |
327 (*case*) |
327 (*case*) |
328 I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*); |
328 I_Model.check_single ctxt m_field oris (I_Model.TEST_to_OLD i_model) m_patt ct (*of*); |
329 "~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, (str(*, pos*))) = |
329 "~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, (str(*, pos*))) = |
330 (ctxt, m_field, oris, i_model, m_patt, ct); |
330 (ctxt, m_field, oris, i_model, m_patt, ct); |
331 val (t as (descriptor $ _)) = Syntax.read_term ctxt str |
331 val (t as (descriptor $ _)) = Syntax.read_term ctxt str |
332 |
332 |
333 (*+*)val "Constants [r = 7]" = UnparseC.term ctxt t; |
333 (*+*)val "Constants [r = 7]" = UnparseC.term ctxt t; |
358 |
358 |
359 (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*); |
359 (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*); |
360 "~~~~~ fun is_notyet_input , args:"; val (ctxt, itms, all, (i, v, f, d, ts), pbt) = |
360 "~~~~~ fun is_notyet_input , args:"; val (ctxt, itms, all, (i, v, f, d, ts), pbt) = |
361 (ctxt, i_model, all, ori', m_patt); |
361 (ctxt, i_model, all, ori', m_patt); |
362 val SOME (_, (_, pid)) = |
362 val SOME (_, (_, pid)) = |
363 (*case*) find_first (eq1 d) pbt (*of*); |
363 (*case*) find_first (fn (_, (d', _)) => d = d') pbt |
364 (*local*)fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (I_Model.descriptor itm_);(*local*) |
364 val SOME (_, _, _, _, (feedb, _)) = |
365 val SOME (_, _, _, _, itm_) = |
365 (*case*) find_first (fn (_, _, _, f', (feedb, _)) => |
366 (*case*) find_first (eq3 f d) itms (*of*); |
366 f = f' andalso d = (descriptor_POS feedb)) itms |
367 val ts' = inter op = (o_model_values itm_) ts; |
367 val ts' = inter op = (values_POS' feedb) ts |
368 (*if*) subset op = (ts, ts') (*else*); |
368 val false = |
369 val return_is_notyet_input = ("", |
369 (*if*) subset op = (ts, ts') |
370 ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts)); |
370 |
371 "~~~~~ fun ori_2itm , args:"; val (itm_, pid, all, (id, vt, fd, d, ts)) = |
371 val return_is_notyet_input = ("", |
372 (itm_, pid, all, (i, v, f, d, subtract op = ts' ts)); |
372 ori_2itm feedb pid all (i, v, f, d, subtract op = ts' ts)); |
373 val ts' = union op = (o_model_values itm_) ts; |
373 "~~~~~ fun ori_2itm , args:"; val (feedb, pid, all, (id, vt, fd, d, ts)) = |
|
374 (feedb, pid, all, (i, v, f, d, subtract op = ts' ts)); |
|
375 val ts' = union op = (values_POS' feedb) ts; |
374 val pval = [Input_Descript.join'''' (d, ts')] |
376 val pval = [Input_Descript.join'''' (d, ts')] |
375 val complete = if eq_set op = (ts', all) then true else false |
377 val complete = if eq_set op = (ts', all) then true else false |
376 |
378 |
377 (*+*)val "Inc Constants [] , pen2str" = itm_ |> I_Model.feedback_to_string ctxt |
379 (*+*)val "Inc_POS Constants [] [__=__, __=__]" = feedb |> I_Model.feedback_POS_to_string ctxt |
378 (*\\\----------------- step into specify_do_next -------------------------------------------//*) |
380 (*\\\----------------- step into specify_do_next -------------------------------------------//*) |
379 (*\\------------------ step into do_next ---------------------------------------------------//*) |
381 (*\\------------------ step into do_next ---------------------------------------------------//*) |
380 val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next |
382 val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next |
381 |
383 |
382 (*|------------------- continue with me_Model_Problem ----------------------------------------*) |
384 (*|------------------- continue with me_Model_Problem ----------------------------------------*) |
398 pt_model ppobj p_; |
400 pt_model ppobj p_; |
399 "~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, o_spec, hdl), ctxt, ...}), |
401 "~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, o_spec, hdl), ctxt, ...}), |
400 Pbl(*Frm,Pbl*)) = (ppobj, p_); |
402 Pbl(*Frm,Pbl*)) = (ppobj, p_); |
401 val (_, _, met_id) = References.select_input o_spec spec |
403 val (_, _, met_id) = References.select_input o_spec spec |
402 val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to_POS probl) (Pos.Met, met_id) |
404 val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to_POS probl) (Pos.Met, met_id) |
403 val return_pt_model = Ctree.ModSpec (allcorr, Pos.Pbl, hdl, probl, (*where_*)[(*Problem.from_store in check*)], spec) |
405 |
|
406 val return_pt_model = Ctree.ModSpec (allcorr, Pos.Pbl, hdl, I_Model.OLD_to_POS probl, |
|
407 (*where_*)[(*Problem.from_store in check*)], spec) |
404 |
408 |
405 (*|------------------- continue with TESTg_form ----------------------------------------------*) |
409 (*|------------------- continue with TESTg_form ----------------------------------------------*) |
406 val Ctree.ModSpec (spec as (_, p_, _, gfr, where_, _)) = |
410 val Ctree.ModSpec (spec as (_, p_, _, gfr, where_, _)) = |
407 (*case*) form (*of*); |
411 (*case*) form (*of*); |
408 Test_Out.PpcKF ( (Test_Out.Problem [], |
412 Test_Out.PpcKF ( (Test_Out.Problem [], |
412 "~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_); |
416 "~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_); |
413 fun coll model [] = model |
417 fun coll model [] = model |
414 | coll model ((_, _, _, field, itm_) :: itms) = |
418 | coll model ((_, _, _, field, itm_) :: itms) = |
415 coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms; |
419 coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms; |
416 |
420 |
417 val gfr = coll P_Model.empty itms; |
421 val gfr = coll P_Model.empty (I_Model.TEST_to_OLD itms); |
418 "~~~~~ fun coll , args:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: itms)) |
422 "~~~~~ fun coll , args:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: itms)) |
419 = (P_Model.empty, itms); |
423 = (P_Model.empty, I_Model.TEST_to_OLD itms); |
420 |
424 |
421 (*+*)val 4 = length itms; |
425 (*+*)val 4 = length itms; |
422 (*+*)val itm = nth 1 itms; |
426 (*+*)val itm = nth 1 itms; |
423 |
427 |
424 coll P_Model.empty [itm]; |
428 coll P_Model.empty [itm]; |