signature SPECIFY =

sig

  val find_next_step: Calc.T -> string * (Pos.pos_ * Tactic.input)

  val find_next_step': Pos.pos_ -> bool -> O_Model.T -> References.T -> I_Model.T * I_Model.T ->

    Model_Pattern.T * Model_Pattern.T -> References.T -> Pos.pos_ * Tactic.input

  val do_all: Calc.T -> Calc.T 

  val finish_phase: Calc.T -> Calc.T

  val item_to_add: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T ->

    (Model_Def.m_field * TermC.as_string) option

  val item_to_add': theory -> O_Model.T -> Model_Pattern.T -> I_Model.T ->

    (Model_Def.m_field * TermC.as_string) option

(*TODO: vvvvvvvvvvvvvv unify code*)

  val by_tactic_input': string -> TermC.as_string -> Calc.T -> Calc.state_post

  val by_tactic': string -> TermC.as_string -> Calc.T -> string * Calc.state_post

(*TODO: ^^^^^^^^^^^^^^ unify code*)

(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

  (*NONE*)

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

  (*NONE*)

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

end

(**)

structure Specify(**): SPECIFY(**) =

struct

(**)

(*

  select an item in oris, notyet input in itms 

  (precondition: in itms are only I_Model.Cor, I_Model.Sup, I_Model.Inc)

args of item_to_add'

  thy : for?

  oris: from formalization 'type fmz', structured for efficient access 

  pbt : the problem-pattern to be matched with oris in order to get itms

  itms: already input items

*)

fun item_to_add' thy [] pbt itms = (*root (only) ori...fmz=[]*)

    let

      fun test_d d (i, _, _, _, itm_) = (d = (I_Model.d_in itm_)) andalso i <> 0

      fun is_elem itms (_, (d, _)) = 

        case find_first (test_d d) itms of SOME _ => true | NONE => false

    in

      case filter_out (is_elem itms) pbt of

        (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, []))

      | _ => NONE

    end

  | item_to_add' thy oris _ itms =

    let

(*OLD*)fun testr_vt v ori = Library.member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"

(*OLD*)fun testi_vt v itm = Library.member op= (#2 (itm : I_Model.single)) v

      fun test_id ids r = Library.member op= ids (#1 (r : O_Model.single))

      fun test_subset itm (_, _, _, d, ts) = 

        (I_Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.ts_in (#5 itm), ts)

      fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false

        | false_and_not_Sup (_, _, false, _, _) = true

        | false_and_not_Sup _ = false

      val v = if itms = [] then 1 else I_Model.max_vt itms

      val vors = if v = 0 then oris else filter (testr_vt v) oris  (* oris..vat *)

      val vits =

        if v = 0

        then itms                                 (* because of dsc without dat *)

  	    else filter (testi_vt v) itms;                             (* itms..vat *)

      val icl = filter false_and_not_Sup vits;                    (* incomplete *)

    in

      if icl = [] then

        case filter_out (test_id (map #1 vits)) vors of

          [] => NONE

        | miss => SOME (O_Model.getr_ct thy (hd miss))

      else

        case find_first (test_subset (hd icl)) vors of

          NONE => raise ERROR "item_to_add': types or dsc DO NOT MATCH BETWEEN fmz --- pbt"

        | SOME ori => SOME (I_Model.geti_ct thy ori (hd icl))

    end

(* preliminary doubling of code, ONLY difference SHALL BE in fun testr_vt *)

fun item_to_add thy [] pbt itms = (*root (only) ori...fmz=[]*)

    let

      fun test_d d (i, _, _, _, itm_) = (d = (I_Model.d_in itm_)) andalso i <> 0

      fun is_elem itms (_, (d, _)) = 

        case find_first (test_d d) itms of SOME _ => true | NONE => false

    in

      case filter_out (is_elem itms) pbt of

        (f, (d, _)) :: _ => SOME (f, ((UnparseC.term_in_thy thy) o Input_Descript.join) (d, []))

      | _ => NONE

    end

  | item_to_add thy oris _ itms =

    let

(*NEW*)fun testr_vt v ori = Library.member op= (#2 (ori : O_Model.single)) v (*andalso (#3 ori) <> "#undef"*)

(*OLD* )fun testr_vt v ori = Library.member op= (#2 (ori : O_Model.single)) v andalso (#3 ori) <> "#undef"

( *OLD*)fun testi_vt v itm = Library.member op= (#2 (itm : I_Model.single)) v

      fun test_id ids r = Library.member op= ids (#1 (r : O_Model.single))

      fun test_subset itm (_, _, _, d, ts) = 

        (I_Model.d_in (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.ts_in (#5 itm), ts)

      fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false

        | false_and_not_Sup (_, _, false, _, _) = true

        | false_and_not_Sup _ = false

      val v = if itms = [] then 1 else I_Model.max_vt itms

      val vors = if v = 0 then oris else filter (testr_vt v) oris  (* oris..vat *)

      val vits =

        if v = 0

        then itms                                 (* because of dsc without dat *)

  	    else filter (testi_vt v) itms;                             (* itms..vat *)

      val icl = filter false_and_not_Sup vits;                    (* incomplete *)

    in

      if icl = [] then

        case filter_out (test_id (map #1 vits)) vors of

          [] => NONE

        | miss => SOME (O_Model.getr_ct thy (hd miss))

      else

        case find_first (test_subset (hd icl)) vors of

          NONE => raise ERROR "item_to_add': types or dsc DO NOT MATCH BETWEEN fmz --- pbt"

        | SOME ori => SOME (I_Model.geti_ct thy ori (hd icl))

    end

(*TODO: unify*)

fun find_next_step (pt, (p, p_)) =

  let

(*OLD*)val (pblobj, met, origin, oris, dI', pI', mI', pbl, dI, pI, mI) = 

(*OLD*)  case Ctree.get_obj I pt p of

(*OLD*)    pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),

(*OLD*)	  probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)

(*OLD*)  | Ctree.PrfObj _ => raise ERROR "nxt_specify_: not on PrfObj"

(*OLD*)in

(*OLD*)  if Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin then

(*OLD*)

(*NEW* )val pblobj as {meth = met, origin = origin as (oris, (dI', pI', mI'), _), probl = pbl,

(*NEW*)  spec = (dI, pI, mI), ctxt, ...} = Calc.specify_data (pt, (p, p_));

(*NEW*)in

(*NEW*)  if Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin then

( *NEW*)

      case mI' of

        ["no_met"] => ("ok", (Pos.Pbl, Tactic.Refine_Tacitly pI'))

      | _ => ("ok", (Pos.Pbl, Tactic.Model_Problem))

    else

      let 

        (*NEW* ) References.select (dI', pI', mI') (dI, pI, mI) ( *NEW*)

        val cpI = if pI = Problem.id_empty then pI' else pI;

  	    val cmI = if mI = Method.id_empty then mI' else mI;

  	    val {ppc = pbt, prls, where_, ...} = Problem.from_store cpI;

  	    val pre = Pre_Conds.check' "thy 100820" prls where_ pbl;

  	    val preok = foldl and_ (true, map fst pre);

  	    (*FIXME.WN0308:    ~~~~~: just check true in itms of pbl/met?*)

        val mpc = (#ppc o Method.from_store) cmI

      in

        case p_ of

		    (*vvvvvvv---------------------------*)

          Pos.Pbl =>

          (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))

           else if pI' = Problem.id_empty andalso pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))

           else

             case find_first (I_Model.is_error o #5) pbl of

      	       SOME (_, _, _, fd, itm_) =>

      	         ("dummy", (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory

      	           (if dI = ThyC.id_empty then dI' else dI)) fd itm_))

      	     | NONE => 

      	       (case item_to_add' (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of

      	          SOME (fd, ct') => ("dummy", (Pos.Pbl, P_Model.mk_additem fd ct'))

      	        | NONE => (*pbl-items complete*)

      	          if not preok then ("dummy", (Pos.Pbl, Tactic.Refine_Problem pI'))

      	          else if dI = ThyC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))

      		        else if pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))

      		        else if mI = Method.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Method mI'))

      		        else

      			        case find_first (I_Model.is_error o #5) met of

      			          SOME (_, _, _, fd, itm_) => ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory dI) fd itm_))

      			        | NONE => 

      			          (case item_to_add (ThyC.get_theory dI) oris mpc met of

      				          SOME (fd, ct') => ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*30.8.01: pre?!?*)

      				        | NONE => ("dummy", (Pos.Met, Tactic.Apply_Method mI)))))

		    (*vvvvvvv---------------------------*)

        | Pos.Met =>

          (case find_first (I_Model.is_error o #5) met of

            SOME (_,_,_, fd, itm_) => ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_))

          | NONE => 

            case item_to_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of

      	      SOME (fd, ct') => ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*->->*)

            | NONE => 

      	      (if dI = ThyC.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Theory dI'))

      	       else if pI = Problem.id_empty then ("dummy", (Pos.Met, Tactic.Specify_Problem pI'))

      		     else if not preok then ("dummy", (Pos.Met, Tactic.Specify_Method mI))

      		     else ("dummy", (Pos.Met, Tactic.Apply_Method mI))))

        | p_ => raise ERROR ("Specify.find_next_step called with " ^ Pos.pos_2str p_)

      end

  end

(* 

  TODO: unify code with Specify.find_next_step ! ! ! USED ONLY to determine Pos.Pbl .. Pos.Met

   determine the next step of specification;

   not done here: Refine_Tacitly (otherwise *** unknown method: (..., no_met))

   eg. in rootpbl 'no_met': 

args:

  preok          predicates are _all_ ok (and problem matches completely)

  oris           immediately from formalization 

  (dI',pI',mI')  specification coming from author/parent-problem

  (pbl,          item lists specified by user

   met)          -"-, tacitly completed by copy_probl

  (dI,pI,mI)     specification explicitly done by the user

  (pbt, mpc)     problem type, guard of method

*)

		(*--------------vvvvvvv *)

fun find_next_step' Pos.Pbl preok oris (dI', pI', mI') (pbl, met) (pbt, mpc) (dI, pI, mI) = 

    (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI')

     else if pI' = Problem.id_empty andalso pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')

     else

       case find_first (I_Model.is_error o #5) pbl of

	       SOME (_, _, _, fd, itm_) =>

	         (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)

	     | NONE => 

	       (case item_to_add' (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of

	          SOME (fd, ct') => (Pos.Pbl, P_Model.mk_additem fd ct')

	        | NONE => (*pbl-items complete*)

	          if not preok then (Pos.Pbl, Tactic.Refine_Problem pI')

	          else if dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI')

		        else if pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI')

		        else if mI = Method.id_empty then (Pos.Pbl, Tactic.Specify_Method mI')

		        else

			        case find_first (I_Model.is_error o #5) met of

			          SOME (_, _, _, fd, itm_) => (Pos.Met, P_Model.mk_delete (ThyC.get_theory dI) fd itm_)

			        | NONE => 

			          (case item_to_add (ThyC.get_theory dI) oris mpc met of

				          SOME (fd, ct') => (Pos.Met, P_Model.mk_additem fd ct') (*30.8.01: pre?!?*)

				        | NONE => (Pos.Met, Tactic.Apply_Method mI))))

		(*--------------vvvvvvv *)

  | find_next_step' Pos.Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) = 

    (case find_first (I_Model.is_error o #5) met of

      SOME (_,_,_,fd,itm_) => (Pos.Met, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_)

    | NONE => 

      case item_to_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of

	      SOME (fd,ct') => (Pos.Met, P_Model.mk_additem fd ct')

      | NONE => 

	      (if dI = ThyC.id_empty then (Pos.Met, Tactic.Specify_Theory dI')

	       else if pI = Problem.id_empty then (Pos.Met, Tactic.Specify_Problem pI')

		     else if not preok then (Pos.Met, Tactic.Specify_Method mI)

		     else (Pos.Met, Tactic.Apply_Method mI)))

  | find_next_step' p _ _ _ _ _ _ = raise ERROR ("find_next_step': uncovered case with " ^ Pos.pos_2str p)

fun by_tactic' sel ct (pt, pos as (p, Pos.Met)) = 

      let

        val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = Specification.get_data (pt, pos)

        val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI

        val cpI = if pI = Problem.id_empty then pI' else pI

        val cmI = if mI = Method.id_empty then mI' else mI

        val {ppc, pre, prls, ...} = Method.from_store cmI

      in 

        case I_Model.check_single ctxt sel oris met ppc ct of

          I_Model.Add itm =>  (*..union old input *)

    	      let

              val met' = I_Model.add_single thy itm met

              val tac' = I_Model.get_tac sel (ct, met')

    	        val (p, pt') =

    	         case Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of

    	          ((p, Pos.Met), _, _, pt') => (p, pt')

    	        | _ => raise ERROR "by_tactic': uncovered case of generate1"

    	        val pre' = Pre_Conds.check' thy prls pre met'

    	        val pb = foldl and_ (true, map fst pre')

    	        val (p_, _) = find_next_step' Pos.Met pb oris (dI',pI',mI') (pbl,met') 

    	            ((#ppc o Problem.from_store) cpI,ppc) (dI,pI,mI);

    	      in 

              ("ok", ([], [], (pt', (p, p_))))

            end

        | I_Model.Err msg =>

    	      let

              val pre' = Pre_Conds.check' thy prls pre met

    	        val pb = foldl and_ (true, map fst pre')

    	        val (p_, _) = find_next_step' Pos.Met pb oris (dI',pI',mI') (pbl,met) 

    	          ((#ppc o Problem.from_store) cpI,(#ppc o Method.from_store) cmI) (dI,pI,mI);

    	      in

              (msg, ([], [], (pt, (p, p_))))

    	      end

      end

  | by_tactic' sel ct (pt, pos as (p, _(*Frm, Pbl*))) =

      let

        val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = Specification.get_data (pt, pos)

        val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI

        val cpI = if pI = Problem.id_empty then pI' else pI

        val cmI = if mI = Method.id_empty then mI' else mI

        val {ppc, where_, prls, ...} = Problem.from_store cpI

      in

        case I_Model.check_single ctxt sel oris pbl ppc ct of

          I_Model.Add itm => (*..union old input *)

	          let

	            val pbl' = I_Model.add_single thy itm pbl

              val tac' = I_Model.get_tac sel (ct, pbl')

	            val (p, pt') =

	              case Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of

  	              ((p, Pos.Pbl), _, _, pt') => (p, pt')

  	            | _ => raise ERROR "by_tactic': uncovered case of Specify_Step.add"

  	            (* only for getting final p_ ..*)

	            val pre = Pre_Conds.check' thy prls where_ pbl';

	            val pb = foldl and_ (true, map fst pre);

	            val (p_, _) = find_next_step' Pos.Pbl pb oris (dI',pI',mI')

	              (pbl',met) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI);

	          in

              ("ok", ([], [], (pt', (p, p_))))

            end

        | I_Model.Err msg =>

	          let

              val pre = Pre_Conds.check' thy prls where_ pbl

	            val pb = foldl and_ (true, map fst pre)

	            val (p_, _(*Tactic.input*)) = find_next_step' Pos.Pbl pb oris (dI', pI', mI')

	              (pbl, met) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI)

	          in

            (msg, ([], [], (pt, (p, p_))))

	          end

      end

(*FIXME.WN110515 declare_constraints for ct (without dsc) into PblObj{ctxt, ...}

  -- for input from scratch*)

fun by_tactic_input' sel ct (ptp as (pt, (p, Pos.Pbl))) = 

    let

      val (oris, dI', pI', dI, pI, pbl, ctxt) = case Ctree.get_obj I pt p of

        Ctree.PblObj {origin = (oris, (dI', pI', _), _), spec = (dI, pI, _), probl = pbl, ctxt, ...} =>

           (oris, dI', pI', dI, pI, pbl, ctxt)

      | _ => raise ERROR "specify (Specify_Theory': uncovered case get_obj"

      val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;

      val cpI = if pI = Problem.id_empty then pI' else pI;

    in

      case I_Model.check_single ctxt sel oris pbl ((#ppc o Problem.from_store) cpI) ct of

	      I_Model.Add itm (*..union old input *) =>

	        let

	          val pbl' = I_Model.add_single thy itm pbl

	          val (tac, tac_) = case sel of

		          "#Given" => (Tactic.Add_Given    ct, Tactic.Add_Given'   (ct, pbl'))

		        | "#Find"  => (Tactic.Add_Find     ct, Tactic.Add_Find'    (ct, pbl'))

		        | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, pbl'))

		        | sel => raise ERROR ("by_tactic_input': uncovered case of" ^ sel)

		        val (p, c, pt') =

		          case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of

  		          ((p, Pos.Pbl), c, _, pt') =>  (p, c, pt')

  		        | _ => raise ERROR "by_tactic_input': uncovered case generate1"

	        in

	          ([(tac, tac_, ((p, Pos.Pbl), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pos.Pbl)))

          end	       

	    | I_Model.Err msg => (*TODO.WN03 pass error-msgs to the frontend..

                     FIXME ..and dont abuse a tactic for that purpose*)

	        ([(Tactic.Tac msg, Tactic.Tac_ (ThyC.get_theory "Isac_Knowledge", msg,msg,msg),

	          (Pos.e_pos', (Istate_Def.empty, ContextC.empty)))], [], ptp) 

    end

  | by_tactic_input' sel ct (ptp as (pt, (p, Pos.Met))) = 

    let

(*NEW* ) *.specify_data ( *NEW*)

      val (oris, dI', mI', dI, mI, met, ctxt) = case Ctree.get_obj I pt p of

        Ctree.PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>

           (oris, dI', mI', dI, mI, met, ctxt)

      | _ => raise ERROR "by_tactic_input' Met: uncovered case get_obj"

(*NEW* ) References.select ( *NEW*)

      val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;

      val cmI = if mI = Method.id_empty then mI' else mI;

    in 

      case I_Model.check_single ctxt sel oris met ((#ppc o Method.from_store) cmI) ct of

        I_Model.Add itm (*..union old input *) =>

	        let

	          val met' = I_Model.add_single thy itm met;

	          val (tac,tac_) = case sel of

		          "#Given" => (Tactic.Add_Given    ct, Tactic.Add_Given'   (ct, met'))

		        | "#Find"  => (Tactic.Add_Find     ct, Tactic.Add_Find'    (ct, met'))

		        | "#Relate"=> (Tactic.Add_Relation ct, Tactic.Add_Relation'(ct, met'))

		        | sel => raise ERROR ("by_tactic_input' Met: uncovered case of" ^ sel)

	          val (p, c, pt') =

	            case Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Met)) of

  	            ((p, Pos.Met), c, _, pt') => (p, c, pt')

  		        | _ => raise ERROR "by_tactic_input': uncovered case generate1 (WARNING WHY ?)"

	        in

	          ([(tac, tac_, ((p, Pos.Met), (Istate_Def.Uistate, ctxt)))], c, (pt', (p, Pos.Met)))

	        end

      | I_Model.Err _ => ([(*tacis*)], [], ptp) (*nxt_me collects tacis until not hide; here just no progress*)

    end

  | by_tactic_input' _ _ (_, p) = raise ERROR ("by_tactic_input' not impl. for" ^ Pos.pos'2str p)

(* complete _NON_empty calc-head for autocalc (sub-)pbl from oris

  + met from fmz; assumes pos on PblObj, meth = []                    *)

fun finish_phase (pt, pos as (p, p_)) =

  let

    val _ = if p_ <> Pos.Pbl 

	    then raise ERROR ("###finish_phase: only impl.for Pbl, called with " ^ Pos.pos'2str pos)

	    else ()

	  val (oris, ospec, probl, spec) = case Ctree.get_obj I pt p of

	    Ctree.PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)

	  | _ => raise ERROR "finish_phase: unvered case get_obj"

  	val (_, pI, mI) = References.select ospec spec

  	val mpc = (#ppc o Method.from_store) mI

  	val ppc = (#ppc o Problem.from_store) pI

  	val (pits, mits) = I_Model.complete_method (oris, mpc, ppc, probl)

    val pt = Ctree.update_pblppc pt p pits

	  val pt = Ctree.update_metppc pt p mits

  in (pt, (p, Pos.Met)) end

(* do all specification in one single step:

   complete calc-head for autocalc (sub-)pbl from oris (+ met from fmz);

   oris and spec (incl. pbl-refinement) given from init_calc or SubProblem

*)

fun do_all (pt, (p, _)) =

  let

    val (pors, dI, pI, mI) = case Ctree.get_obj I pt p of

      Ctree.PblObj {origin = (pors, (dI, pI, mI), _), ...}

        => (pors, dI, pI, mI)

    | _ => raise ERROR "do_all: uncovered case get_obj"

	  val {ppc, ...} = Method.from_store mI

    val (_, vals) = O_Model.values' pors

	  val ctxt = ContextC.initialise dI vals

    val (pt, _) = Ctree.cupdate_problem pt p ((dI, pI, mI),

      map (I_Model.complete' ppc) pors, map (I_Model.complete' ppc) pors, ctxt)

  in

    (pt, (p, Pos.Met))

  end

(**)end(**)