(* Title:  Specify/step-specify.sml

    Author: Walther Neuper 2019

    (c) due to copyright terms

 *)

 signature STEP_SPECIFY =

 sig

   val by_tactic: Tactic.input -> Calc.T -> Chead.calcstate'

 (*val do_next: Step.specify_do_next requires Lucin.by_tactic, which is not yet known in Step_Specify*)

 end

 (**)

 structure Step_Specify(**): STEP_SPECIFY(**) =

 struct

 (**)

 open Pos

 open Ctree

 open Chead

 (* was fun Math_Engine.nxt_specify_ *)

 fun by_tactic (tac as Tactic.Model_Problem) (pt, pos as (p, _)) =

     let

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

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

       | _ => error "by_tactic Model_Problem; uncovered case get_obj"

       val (dI, pI, mI) = some_spec ospec spec

       val thy = Celem.assoc_thy dI

       val mpc = (#ppc o Specify.get_met) mI (* just for reuse complete_mod_ *)

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

       val pbl = Generate.init_pbl ppc (* fill in descriptions *)

       (*----------------if you think, this should be done by the Dialog 

        in the java front-end, search there for WN060225-modelProblem----*)

       val (pbl, met) = case cas of

         NONE => (pbl, [])

   		| _ => complete_mod_ (oris, mpc, ppc, probl)

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

       val tac_ = Tactic.Model_Problem' (pI, pbl, met)

       val (pos,c,_,pt) = Generate.generate1 thy tac_ (Istate_Def.Uistate, ctxt) pos pt

     in ([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos)) end

   | by_tactic (Tactic.Add_Given ct) ptp = nxt_specif_additem "#Given" ct ptp

   | by_tactic (Tactic.Add_Find  ct) ptp = nxt_specif_additem "#Find"  ct ptp

   | by_tactic (Tactic.Add_Relation ct) ptp = nxt_specif_additem"#Relate" ct ptp

     (*. called only if no_met is specified .*)     

   | by_tactic (Tactic.Refine_Tacitly pI) (ptp as (pt, pos as (p,_))) =

     let 

       val (oris, dI, ctxt) = case get_obj I pt p of

         (PblObj {origin = (oris, (dI, _, _), _), ctxt, ...}) => (oris, dI, ctxt)

       | _ => error "by_tactic Refine_Tacitly: uncovered case get_obj"

       val opt = Specify.refine_ori oris pI

     in 

       case opt of

 	      SOME pI' => 

 	        let 

             val {met, ...} = Specify.get_pbt pI'

 	          (*val pt = update_pbl pt p pbl ..done by Model_Problem*)

 	          val mI = if length met = 0 then Celem.e_metID else hd met

             val thy = Celem.assoc_thy dI

 	          val (pos, c, _, pt) = 

 		          Generate.generate1 thy (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) pos pt

 	        in

 	          ([(Tactic.Refine_Tacitly pI, Tactic.Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[]),

 	              (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos)) 

           end

 	    | NONE => ([], [], ptp)

     end

   | by_tactic (Tactic.Refine_Problem pI) (ptp as (pt, pos as (p,_))) =

     let

       val (dI, dI', probl, ctxt) = case get_obj I pt p of

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

           (dI, dI', probl, ctxt)

       | _ => error "by_tactic Refine_Problem: uncovered case get_obj"

 	    val thy = if dI' = Rule.e_domID then dI else dI'

     in 

       case Specify.refine_pbl (Celem.assoc_thy thy) pI probl of

 	      NONE => ([], [], ptp)

 	    | SOME rfd => 

 	      let 

           val (pos,c,_,pt) = Generate.generate1 (Celem.assoc_thy thy) (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) pos pt

 	      in

 	        ([(Tactic.Refine_Problem pI, Tactic.Refine_Problem' rfd, (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos))

         end

     end

   | by_tactic (Tactic.Specify_Problem pI) (pt, pos as (p,_)) =

     let

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

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

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

       | _ => error ""

 	    val thy = Celem.assoc_thy (if dI' = Rule.e_domID then dI else dI');

       val {ppc,where_,prls,...} = Specify.get_pbt pI

 	    val pbl = 

 	      if pI' = Celem.e_pblID andalso pI = Celem.e_pblID

 	      then (false, (Generate.init_pbl ppc, []))

 	      else Specify.match_itms_oris thy probl (ppc,where_,prls) oris

 	      (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)

 	    val (c, pt) = case Generate.generate1 thy (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) pos pt of

 	      ((_, Pbl), c, _, pt) => (c, pt)

 	    | _ => error ""

     in

       ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, pbl), (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt,pos))

     end

   (* transfers oris (not required in pbl) to met-model for script-env

      FIXME.WN.8.03: application of several mIDs to SAME model?       *)

   | by_tactic (Tactic.Specify_Method mID) (pt, pos as (p,_)) = 

     let

       val (oris, pbl, dI, met, ctxt) = case get_obj I pt p of

         PblObj {origin = (oris, _, _), probl = pbl, spec = (dI, _, _), meth=met, ctxt, ...}

           => (oris, pbl, dI, met, ctxt)

       | _ => error "by_tactic Specify_Method: uncovered case get_obj"

       val {ppc,pre,prls,...} = Specify.get_met mID

       val thy = Celem.assoc_thy dI

       val oris = Specify.add_field' thy ppc oris

       val met = if met=[] then pbl else met (* WN0602 what if more itms in met? *)

       val (_, (itms, _)) = Specify.match_itms_oris thy met (ppc,pre,prls ) oris

       val itms = Specify.hack_until_review_Specify_2 mID itms

       val (pos, c, _, pt) = 

 	      Generate.generate1 thy (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) pos pt

     in

       ([(Tactic.Specify_Method mID, Tactic.Specify_Method' (mID, oris, itms), (pos, (Istate_Def.Uistate, ContextC.e_ctxt)))], c, (pt, pos)) 

     end    

   | by_tactic (Tactic.Specify_Theory dI) (pt, pos as (_, Pbl)) =

     let

       val ctxt = get_ctxt pt pos

 	    val (pos, c, _, pt) = 

 	      Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") (Tactic.Specify_Theory' dI)  (Istate_Def.Uistate, ctxt) pos pt

     in (*FIXXXME: check if pbl can still be parsed*)

 	    ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate_Def.Uistate, ctxt)))], c,

 	      (pt, pos))

     end

   | by_tactic (Tactic.Specify_Theory dI) (pt, pos as (_, Met)) =

     let

       val ctxt = get_ctxt pt pos

 	    val (pos, c, _, pt) = Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) pos pt

     in  (*FIXXXME: check if met can still be parsed*)

 	    ([(Tactic.Specify_Theory dI, Tactic.Specify_Theory' dI, (pos, (Istate_Def.Uistate, ctxt)))], c, (pt, pos))

     end

   | by_tactic m' _ = error ("by_tactic: not impl. for " ^ Tactic.tac2str m')

 (**)end(**)