signature SPECIFY_NEW =

sig

  val find_next_tactic: Ctree.state -> string * (Pos.pos_ * Tactic.input)

end

(**)

structure SpecifyNEW(**): SPECIFY_NEW(**) =

struct

(**)

open Pos

open Chead

(* was Chead.nxt_spec *)

fun find_next_tactic (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' = Rule.e_domID andalso dI = Rule.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 = Rule.e_domID then dI' else dI)) fd itm_))

      	     | NONE => 

      	       (case nxt_add (Celem.assoc_thy (if dI = Rule.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 = Rule.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 = Rule.e_domID then dI' else dI)) fd itm_))

          | NONE => 

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

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

            | NONE => 

      	      (if dI = Rule.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_tactic called with " ^ Pos.pos_2str p_)

      end

  end

end