(* Title:  Specify/specify.sml

   Author: Walther Neuper

*)

signature SPECIFY =

sig

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

  val do_all: Calc.T -> Calc.T 

  val finish_phase: Calc.T -> Calc.T

  val item_to_add: Proof.context -> O_Model.T -> I_Model.T_POS -> 

    (Model_Def.m_field * TermC.as_string) option

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

(*from isac_test for Minisubpbl*)

  val for_problem: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T_POS ->

    string * (Pos.pos_ * Tactic.input)

  val for_method: Proof.context -> O_Model.T -> References.T * References.T -> I_Model.T * I_Model.T ->

    string * (Pos.pos_ * Tactic.input)

  val select_inc_lists: I_Model.T_POS -> I_Model.T_POS

\<^isac_test>\<open>

(**)

\<close>

end

(**)

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

struct

(**)

fun select_inc_lists i_model =

  let

    (* filter problem like with Const ("Input_Descript.solutions", _) *)

    val filt = (fn (_, _, _, _, (I_Model.Inc_POS (descr, _::_) , _)) => Model_Def.is_list_descr descr

      | _ => false)

  in

    (filter filt i_model) @ (filter_out filt i_model)

  end

fun item_to_add ctxt o_model i_model =

  let

    val max_vnt = last_elem (*this decides, for which variant initially help is given*)

      (Model_Def.max_variants o_model i_model)

    val o_vnts = filter (fn (_, vnts, _, _, _) => member op= vnts max_vnt) o_model

    val i_to_select = i_model

      |> filter_out (fn (_, vnts, _, _, (I_Model.Cor_POS _, _)) => member op= vnts max_vnt | _ => false)

      |> select_inc_lists

  in

    if i_to_select = [] then NONE

    else

      case I_Model.fill_from_o o_vnts (hd i_to_select) of

        SOME (_, _, _, m_field, (feedb, _)) =>

          SOME (m_field, feedb |> I_Model.feedb_args_to_string ctxt)

      | NONE => raise ERROR "item_to_add: NONE not.impl."

  end

(** find a next step in the specify-phase **)

(*

  here should be mutual recursion between for_problem ctxt and for_method

*)

fun for_problem ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (pbl, met) =

  let

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

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

    val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;

    val {model = mpc, ...} = MethodC.from_store ctxt cmI

    val (preok, _) = Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_POS pbl);

  in

    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 (fn (_, _, _, _, feedb) => I_Model.is_error feedb) pbl of

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

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

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

      | NONE => 

        (case item_to_add ctxt oris (I_Model.OLD_to_POS 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'))

           (*this is an ERROR fall through ------^^^^^^^^^^^^^^^^^^^^^ for Pre_Conds, redesign ?*)

           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 = MethodC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Method mI'))

           else

            case find_first (fn (_, _, _, _, feedb) => I_Model.is_error feedb) (I_Model.TEST_to_OLD met) of

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

                 ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory ctxt dI) fd itm_))

            | NONE => 

              (case item_to_add ctxt oris met of

    	          SOME (fd, ct') =>

                   ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*30.8.01: where_?!?*)

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

  end

fun for_method ctxt oris ((dI', pI', mI'), (dI, pI, mI)) (_, met) =

  let

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

    val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI;

    val (preok, _) = Pre_Conds.check ctxt where_rls where_ (mpc, I_Model.OLD_to_POS met);

  in

    (case find_first (fn (_, _, _, _, feedb) => I_Model.is_error feedb) met of

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

        ("dummy", (Pos.Met, P_Model.mk_delete (ThyC.get_theory ctxt

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

    | NONE => 

      case item_to_add ctxt oris (I_Model.OLD_to_POS 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))))

  end

(*

  on finding a next step switching from problem to method or vice versa is possible,

  because the user is free to switch and edit the respective models independently.

TODO: this free switch is NOT yet implemented; e.g. 

  preok is relevant for problem + method, i.e. in for_problem ctxt + for_method

*)

fun find_next_step (pt, pos as (_, p_)) =

  let

    val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,

      spec = refs, ...} = Calc.specify_data (pt, pos);

    val ctxt = Ctree.get_ctxt pt pos

  in

    if Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin then

      case mI' of

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

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

    else if p_ = Pos.Pbl then

      for_problem ctxt oris (o_refs, refs) (pbl, I_Model.OLD_to_POS met)

    else

      for_method ctxt oris (o_refs, refs) (pbl, met)

  end

(** tools **)

fun by_Add_  m_field ct (pt, pos as (_, p_)) =

  let

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

    val (i_model, m_patt) =

       if p_ = Pos.Met then

         (met,

           (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)

       else

         (pbl,

           (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)

    in

      case I_Model.check_single ctxt m_field oris i_model m_patt ct of

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

	        let

	          val i_model' = I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model

            val tac' = I_Model.make_tactic m_field (ct, i_model')

	          val  (_, _, _, pt') =  Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, pos)

	        in

            ("ok", ([(Tactic.input_from_T ctxt tac', tac', (pos, (Istate_Def.Uistate, ctxt)))],

              [], (pt', pos)))

          end

      | I_Model.Err msg => (msg, ([], [], (pt, pos)))

    end

(* 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, meth) = case Ctree.get_obj I pt p of

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

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

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

  	val ctxt = Ctree.get_ctxt pt pos

  	val (pits, mits) = I_Model.s_make_complete ctxt oris

  	 (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (pI, mI)

  	val pt = Ctree.update_pblppc pt p (I_Model.TEST_to_OLD pits)

  	val pt = Ctree.update_metppc pt p (I_Model.TEST_to_OLD mits)

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

(*

  do all specification in one single step:

  bypass input of Problem.model and go immediately for MethodC: I_Model.complete'

*)

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

  let

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

      Ctree.PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ctxt, ...}

        => (itms, oris, probl, o_spec, spec, ctxt)

    | _ => raise ERROR "Specify.do_all: no PblObj"

    val (_, pbl_id', met_id') = References.select_input o_refs spec

    val (pbl_imod, met_imod) = I_Model.s_make_complete ctxt oris

      (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS itms) (pbl_id', met_id')

    val (pt, _) = Ctree.cupdate_problem pt p

      (o_refs, I_Model.TEST_to_OLD pbl_imod, I_Model.TEST_to_OLD met_imod, ctxt)

  in

    (pt, (p, Pos.Met))

  end

(**)end(**)