(* 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: theory -> O_Model.T -> Model_Pattern.T -> I_Model.T ->

     (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 ->

     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)

 \<^isac_test>\<open>

 (**)

 \<close>

 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.descriptor 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

     (* m_field is in ------vvvv *)

   | item_to_add thy oris _ itms =

     let

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

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

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

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

         (I_Model.descriptor (#5 (itm: I_Model.single))) = d andalso subset op = (I_Model.o_model_values (#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 Pre_Conds.max_variant itms

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

       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.get_field_term 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.get_field_term thy ori (hd icl))

     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_TEST 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 (I_Model.is_error o #5) 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 (ThyC.get_theory ctxt

             (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'))

            (*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 (I_Model.is_error o #5) met of

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

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

             | NONE => 

               (case item_to_add (ThyC.get_theory ctxt dI) oris mpc 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_TEST met);

   in

     (case find_first (I_Model.is_error o #5) 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 (ThyC.get_theory ctxt 

           (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))))

   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, 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_TEST probl, I_Model.OLD_to_TEST 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_TEST probl, I_Model.OLD_to_TEST 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(**)