362 val SOME (_, (_, pid)) = |
362 val SOME (_, (_, pid)) = |
363 (*case*) find_first (fn (_, (d', _)) => d = d') pbt |
363 (*case*) find_first (fn (_, (d', _)) => d = d') pbt |
364 val SOME (_, _, _, _, (feedb, _)) = |
364 val SOME (_, _, _, _, (feedb, _)) = |
365 (*case*) find_first (fn (_, _, _, f', (feedb, _)) => |
365 (*case*) find_first (fn (_, _, _, f', (feedb, _)) => |
366 f = f' andalso d = (descriptor_POS feedb)) itms |
366 f = f' andalso d = (descriptor_POS feedb)) itms |
367 val ts' = inter op = (values_POS' feedb) ts |
367 val ts' = inter op = (feedb_values feedb) ts |
368 val false = |
368 val false = |
369 (*if*) subset op = (ts, ts') |
369 (*if*) subset op = (ts, ts') |
370 |
370 |
371 val return_is_notyet_input = ("", |
371 val return_is_notyet_input = ("", |
372 ori_2itm feedb 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 "~~~~~ fun ori_2itm , args:"; val (feedb, pid, all, (id, vt, fd, d, 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)); |
374 (feedb, pid, all, (i, v, f, d, subtract op = ts' ts)); |
375 val ts' = union op = (values_POS' feedb) ts; |
375 val ts' = union op = (feedb_values feedb) ts; |
376 val pval = [Input_Descript.join'''' (d, ts')] |
376 val pval = [Input_Descript.join'''' (d, ts')] |
377 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 |
378 |
378 |
379 (*+*)val "Inc_POS Constants [] [__=__, __=__]" = feedb |> I_Model.feedback_POS_to_string ctxt |
379 (*+*)val "Inc_POS Constants [] [__=__, __=__]" = feedb |> I_Model.feedback_POS_to_string ctxt |
380 (*\\\----------------- step into specify_do_next -------------------------------------------//*) |
380 (*\\\----------------- step into specify_do_next -------------------------------------------//*) |