signature SPECIFY_NEW =

sig

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

  val nxt_specify_init_calc : Selem.fmz -> Chead.calcstate

(* ---- 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 SpecifyNEW(**): SPECIFY_NEW(**) =

struct

(**)

open Pos

open Ctree

open Chead

(* was Chead.nxt_spec *)

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

  let

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

  	  case Ctree.get_obj I pt p of

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

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

      | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj"

  in

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

    then 

      case mI' of

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

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

    else

      let 

        val cpI = if pI = Celem.e_pblID then pI' else pI;

  	    val cmI = if mI = Celem.e_metID then mI' else mI;

  	    val {ppc = pbt, prls, where_, ...} = Specify.get_pbt cpI;

  	    val pre = Stool.check_preconds "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 Specify.get_met) cmI

      in

        case p_ of

          Pbl =>

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

           else if pI' = Celem.e_pblID andalso pI = Celem.e_pblID then ("dummy", (Pbl, Tactic.Specify_Problem pI'))

           else

             case find_first (is_error o #5) pbl of

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

      	         ("dummy", (Pbl, mk_delete (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) fd itm_))

      	     | NONE => 

      	       (case nxt_add (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) oris pbt pbl of

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

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

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

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

      		        else if pI = Celem.e_pblID then ("dummy", (Pbl, Tactic.Specify_Problem pI'))

      		        else if mI = Celem.e_metID then ("dummy", (Pbl, Tactic.Specify_Method mI'))

      		        else

      			        case find_first (is_error o #5) met of

      			          SOME (_, _, _, fd, itm_) => ("dummy", (Met, mk_delete (Celem.assoc_thy dI) fd itm_))

      			        | NONE => 

      			          (case nxt_add (Celem.assoc_thy dI) oris mpc met of

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

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

        | Met =>

          (case find_first (is_error o #5) met of

            SOME (_,_,_,fd,itm_) => ("dummy", (Met, mk_delete (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) fd itm_))

          | NONE => 

            case nxt_add (Celem.assoc_thy (if dI = ThyC.e_domID then dI' else dI)) oris mpc met of

      	      SOME (fd,ct') => ("dummy", (Met, mk_additem fd ct'))

            | NONE => 

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

      	       else if pI = Celem.e_pblID then ("dummy", (Met, Tactic.Specify_Problem pI'))

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

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

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

      end

  end

(* create a calc-tree with oris via an cas.refined pbl *)

fun nxt_specify_init_calc ([], (dI, pI, mI)) =

    if pI <> [] 

    then (* from pbl-browser or from CAS cmd with pI=[e_pblID] *)

	    let 

        val {cas, met, ppc, thy, ...} = Specify.get_pbt pI

	      val dI = if dI = "" then ThyC.theory2theory' thy else dI

	      val mI = if mI = [] then hd met else mI

	      val hdl = case cas of NONE => Auto_Prog.pblterm dI pI | SOME t => t

	      val (pt, _) = cappend_problem e_ctree [] (Istate_Def.Uistate, ContextC.empty) ([], (dI, pI, mI))

				  ([], (dI,pI,mI), hdl, ContextC.empty)

	      val pt = update_spec pt [] (dI, pI, mI)

	      val pits = Generate.init_pbl' ppc

	      val pt = update_pbl pt [] pits

	    in ((pt, ([] , Pbl)), []) end

    else 

      if mI <> [] 

      then (* from met-browser *)

	      let 

          val {ppc, ...} = Specify.get_met mI

	        val dI = if dI = "" then "Isac_Knowledge" else dI

	        val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty) ([], (dI, pI, mI))

	          ([], (dI, pI, mI), Rule.e_term, ContextC.empty)

	        val pt = update_spec pt [] (dI, pI, mI)

	        val mits = Generate.init_pbl' ppc

	        val pt = update_met pt [] mits

	      in ((pt, ([], Met)), []) end

      else (* new example, pepare for interactive modeling *)

	      let

	        val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, ContextC.empty)

	          ([], Celem.e_spec) ([], Celem.e_spec, Rule.e_term, ContextC.empty)

	      in ((pt, ([], Pbl)), []) end

  | nxt_specify_init_calc (fmz, (dI, pI, mI)) = 

    let           (* both """"""""""""""""""""""""" either empty or complete *)

	    val thy = Celem.assoc_thy dI

	    val (pI, (pors, pctxt), mI) = 

	      if mI = ["no_met"] 

	      then 

          let 

            val (pors, pctxt) = Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy;

		        val pI' = Specify.refine_ori' pors pI;

		      in (pI', (pors(*refinement over models with diff.precond only*), pctxt),

		        (hd o #met o Specify.get_pbt) pI')

		      end

	      else (pI, Specify.get_pbt pI |> #ppc |> Specify.prep_ori fmz thy, mI)

	    val {cas, ppc, thy = thy', ...} = Specify.get_pbt pI (*take dI from _refined_ pbl*)

	    val dI = ThyC.theory2theory' (Stool.common_subthy (thy, thy'))

	    val hdl = case cas of

		    NONE => Auto_Prog.pblterm dI pI

		  | SOME t => subst_atomic ((vars_of_pbl_' ppc) ~~~ vals_of_oris pors) t

      val (pt, _) = cappend_problem e_ctree [] (Istate_Def.empty, pctxt) (fmz, (dI, pI, mI))

        (pors, (dI, pI, mI), hdl, pctxt)

    in

      ((pt, ([], Pbl)), fst3 (Step_Specify.by_tactic_input Tactic.Model_Problem (pt, ([], Pbl))))

    end

end