(* Title:  Specify/step-specify.sml

   Author: Walther Neuper 2019

   (c) due to copyright terms

*)

signature STEP_SPECIFY =

sig

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

(*TODO: vvvvvvvvvvvvvv unify code*)

  val by_tactic_input: Tactic.input -> Calc.T -> Calc.state_post

  val by_tactic: Tactic.T -> Calc.T -> string * Calc.state_post

(*TODO: ^^^^^^^^^^^^^^ unify code*)

  val hack_until_review_Specify_1: Method.id -> I_Model.T -> I_Model.T

  val hack_until_review_Specify_2: Method.id -> I_Model.T -> I_Model.T

(* ---- keep, probably required later in devel. ----------------------------------------------- *)

  val nxt_specify_init_calc: Formalise.T -> Calc.T * State_Steps.T

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

end

(**)

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

struct

(**)

open Pos

open Ctree

open Specification

(*

  hack until review of Specify:

  introduction of Lucas-Interpretation to Isabelle's functioj package enforced

  to make additional variables on the right hand side to arguments of programs.

  These additional arguments are partially handled by these hacks.

*)

fun hack_until_review_Specify_1 metID itms = 

(**)

  if metID = ["Biegelinien", "ausBelastung"]

  then itms @

    [(4, [1], true, "#Given", I_Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),

        [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),

      (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),

        [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),

    (5, [1], true, "#Given", I_Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),

        [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),

      (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),

        [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]

  else (**) itms

fun hack_until_review_Specify_2 metID itms = 

(**)

  if metID = ["IntegrierenUndKonstanteBestimmen2"]

  then itms @

    [(4, [1], true, "#Given", I_Model.Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),

        [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),

      (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),

        [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),

    (5, [1], true, "#Given", I_Model.Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),

        [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),

      (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),

        [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]

  else (**) itms

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

      | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"

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

      val mpc = (#ppc o Method.from_store) mI (* just for reuse I_Model.complete_method *)

      val {cas, ppc, ...} = Problem.from_store pI

      val pbl = I_Model.init 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, [])

  		| _ => I_Model.complete_method (oris, mpc, ppc, probl)

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

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

      val (pos,c,_,pt) = Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, pos)

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

  | by_tactic_input (Tactic.Add_Given ct) ptp = Specify.by_tactic_input' "#Given" ct ptp

  | by_tactic_input (Tactic.Add_Find  ct) ptp = Specify.by_tactic_input' "#Find"  ct ptp

  | by_tactic_input (Tactic.Add_Relation ct) ptp = Specify.by_tactic_input'"#Relate" ct ptp

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

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

      | _ => raise ERROR "by_tactic_input Refine_Tacitly: uncovered case get_obj"

      val opt = Refine.refine_ori oris pI

    in 

      case opt of

	      SOME pI' => 

	        let 

            val {met, ...} = Problem.from_store pI'

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

	          val mI = if length met = 0 then Method.id_empty else hd met

	          val (pos, c, _, pt) = 

		          Specify_Step.add (Tactic.Refine_Tacitly' (pI, pI', dI, mI,(*pbl*)[])) (Istate_Def.Uistate, ctxt) (pt, pos)

	        in

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

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

          end

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

    end

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

      | _ => raise ERROR "by_tactic_input Refine_Problem: uncovered case get_obj"

	    val thy = if dI' = ThyC.id_empty then dI else dI'

    in 

      case Refine.problem (ThyC.get_theory thy) pI probl of

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

	    | SOME rfd => 

	      let 

          val (pos,c,_,pt) = Specify_Step.add (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos)

	      in

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

        end

    end

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

      | _ => raise ERROR ""

	    val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');

      val {ppc,where_,prls,...} = Problem.from_store pI

	    val pbl = 

	      if pI' = Problem.id_empty andalso pI = Problem.id_empty

	      then (false, (I_Model.init ppc, []))

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

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

	    val (c, pt) =

	      case Specify_Step.add (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) (pt, pos) of

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

  	    | _ => raise ERROR ""

    in

      ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, pbl), (pos, (Istate_Def.Uistate, ContextC.empty)))], 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_input (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)

      | _ => raise ERROR "by_tactic_input Specify_Method: uncovered case get_obj"

      val {ppc,pre,prls,...} = Method.from_store mID

      val thy = ThyC.get_theory dI

      val oris = O_Model.add thy ppc oris

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

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

      val itms = hack_until_review_Specify_2 mID itms

      val (pos, c, _, pt) = 

	      Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)

    in

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

    end    

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

    let

      val ctxt = get_ctxt pt pos

	    val (pos, c, _, pt) = 

	      Specify_Step.add (Tactic.Specify_Theory' dI)  (Istate_Def.Uistate, ctxt) (pt, pos)

    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_input (Tactic.Specify_Theory dI) (pt, pos as (_, Met)) =

    let

      val ctxt = get_ctxt pt pos

	    val (pos, c, _, pt) = Specify_Step.add (Tactic.Specify_Theory' dI) (Istate_Def.Uistate, ctxt) (pt, pos)

    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_input m' _ = raise ERROR ("by_tactic_input: not impl. for " ^ Tactic.input_to_string m')

fun by_tactic (Tactic.Model_Problem' (_, pbl, met)) (pt, pos as (p, _))  =

    let 

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

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

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

      | _ => raise ERROR "Step_Solve.by_tactic (Model_Problem': uncovered case get_obj"

      val thy' = if dI = ThyC.id_empty then dI' else dI

      val thy = ThyC.get_theory thy'

      val {ppc, prls, where_, ...} = Problem.from_store pI'

      val pre = Pre_Conds.check' thy prls where_ pbl

      val pb = foldl and_ (true, map fst pre)

      val ((p, _), _, _, pt) =

        Specify_Step.add (Tactic.Model_Problem'([],pbl,met)) (Istate_Def.Uistate, ctxt) (pt, pos)

      val (_, _) = Specify.find_next_step' Pbl pb oris (dI', pI', mI') (pbl, met) 

		    (ppc,(#ppc o Method.from_store) mI') (dI',pI',mI');

    in

      ("ok", ([], [], (pt, (p, Pbl))))

    end

    (* called only if no_met is specified *)     

  | by_tactic (Tactic.Refine_Tacitly' (pI, pIre, _, _, _)) (pt, pos) =

      let

        val {met, thy,...} = Problem.from_store pIre

        val (domID, metID) = (Context.theory_name thy, if length met = 0 then Method.id_empty else hd met)

        val ((p,_), _, _, pt) = 

	        Specify_Step.add (Tactic.Refine_Tacitly' (pI, pIre, domID, metID, [(*pbl*)]))

            (Istate_Def.Uistate, ContextC.empty) (pt, pos)

(* deprecated^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)

      in 

        ("ok", ([], [], (pt,(p, Pbl))))

      end

  | by_tactic (Tactic.Refine_Problem' rfd) (pt, pos)  =

      let

        val ctxt = get_ctxt pt pos

        val (pos, _, _, pt) =

          Specify_Step.add (Tactic.Refine_Problem' rfd) (Istate_Def.Uistate, ctxt) (pt, pos)

      in

        ("ok", ([], [], (pt,pos)))

      end

    (*WN110515 initialise ctxt again from itms and add preconds*)

  | by_tactic (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (pt, pos as (p, _)) =

      let

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

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

            (oris, dI', pI', mI', dI, mI, ctxt, met)

        | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"

        val (p, pt) =

          case  Specify_Step.add (Tactic.Specify_Problem' (pI, (ok, (itms, pre)))) (Istate_Def.Uistate, ctxt) (pt, pos) of

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

          | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case generate1 (WARNING WHY ?)"

      in

        ("ok", ([], [], (pt, (p, Pbl))))

      end    

    (*WN110515 initialise ctxt again from itms and add preconds*)

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

      let

(*OLD*) val (oris, _, _, mI', dI, _, pbl, met, ctxt) = case get_obj I pt p of

(*OLD*)   PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>

(*OLD*)      (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)

(*OLD*) | _ => raise ERROR "Step_Solve.by_tactic (Specify_Problem': uncovered case get_obj"

(*OLD*) val {ppc, pre, prls, ...} = Method.from_store mID

(*OLD*) val thy = ThyC.get_theory dI

(*OLD*) val oris = O_Model.add thy ppc oris

(*OLD*) val met = if met = [] then pbl else met (*nonsense, DEL ! ! ! ! ! ! ! ! ! ! ! ! ! ! !*)

(*OLD*) val (_, (itms, _)) = M_Match.match_itms_oris thy met (ppc, pre, prls) oris

(*OLD*) val itms = hack_until_review_Specify_1 mI' itms

(*OLD*) val (pos, _, _, pt) =

(*OLD*)   Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)

(*---*)

(*NEW* ) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,

(*NEW*)    ...} =Calc.specify_data (pt, pos);

(*NEW*) val (dI, _, mID) = References.select o_refs refs;

(*NEW*) val {ppc = m_patt, pre, prls, ...} = Method.from_store mID

(*NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))

(*NEW*) val (o_model', ctxt') = O_Model.complete_for_from m_patt root_model (o_model, ctxt)

(*NEW*) val thy = ThyC.get_theory dI

(*NEW*) val (_, (i_model, _)) = M_Match.match_itms_oris thy i_prob (m_patt, pre, prls) o_model';

(*NEW*) val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (mID, o_model', i_model))

(*NEW*)   (Istate_Def.Uistate, ctxt') (pt, pos)

( *NEW*)in

        ("ok", ([], [], (pt, pos)))

      end    

  | by_tactic (Tactic.Add_Given' (ct, _)) (pt, p)  = Specify.by_tactic' "#Given" ct (pt, p)

  | by_tactic (Tactic.Add_Find'  (ct, _)) (pt, p) = Specify.by_tactic' "#Find" ct (pt, p)

  | by_tactic (Tactic.Add_Relation' (ct, _)) (pt, p) = Specify.by_tactic'"#Relate" ct (pt, p)

  | by_tactic (Tactic.Specify_Theory' domID) (pt, (p,p_)) =

      let

        val p_ = case p_ of Met => Met | _ => Pbl

        val thy = ThyC.get_theory domID

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

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

             (oris, dI', pI', mI', dI, pI, mI, pbl, met, ctxt)

        | _ => raise ERROR "Step_Solve.by_tactic (Specify_Theory': uncovered case get_obj"

        val _ = case p_ of Met => met | _ => pbl

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

        val {prls = per, ppc, where_ = pwh, ...} = Problem.from_store cpI

        val cmI = if mI = Method.id_empty then mI' else mI

        val {prls = mer, ppc = mpc, pre= mwh, ...} = Method.from_store cmI

        val pre = case p_ of

          Met => (Pre_Conds.check' thy mer mwh met)

        | _ => (Pre_Conds.check' thy per pwh pbl)

        val pb = foldl and_ (true, map fst pre)

      in

        if domID = dI

        then

          let val (p_, _) = Specify.find_next_step' p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (dI, pI, mI)

	        in

            ("ok", ([], [], (pt, (p, p_))))

          end

        else (*FIXME: check ppc wrt. (new!) domID ..? still parsable?*)

	        let 

	          val ((p, p_), _, _, pt) = Specify_Step.add (Tactic.Specify_Theory' domID) (Istate_Def.Uistate, ctxt) (pt, (p,p_))

	          val (p_, _) = Specify.find_next_step' p_ pb oris (dI', pI', mI') (pbl, met) (ppc, mpc) (domID, pI, mI)

	        in

            ("ok", ([], [], (pt, (p, p_))))

          end                

      end

  | by_tactic _ _ = raise ERROR "Step_Specify.by_tactic uncovered pattern in fun.def"

(* was fun Specification.specify *)

(* 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, ...} = Problem.from_store pI

	      val dI = if dI = "" then Context.theory_name 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 = I_Model.init ppc

	      val pt = update_pbl pt [] pits

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

    else 

      if mI <> [] 

      then (* from met-browser *)

	      let 

          val {ppc, ...} = Method.from_store 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), TermC.empty, ContextC.empty)

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

	        val mits = I_Model.init 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) 

	          ([], References.empty) ([], References.empty, TermC.empty, ContextC.empty)

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

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

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

	    val thy = ThyC.get_theory dI

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

	      if mI = ["no_met"] 

	      then 

          let 

            val (pors(*, pctxt*)) = Problem.from_store pI |> #ppc |> O_Model.init fmz thy;

            val pctxt = ContextC.initialise' thy fmz;

		        val pI' = Refine.refine_ori' pors pI;

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

		        (hd o #met o Problem.from_store) pI')

		      end

	      else

	        let

	          val pors = Problem.from_store pI |> #ppc |> O_Model.init fmz thy;

            val pctxt = ContextC.initialise' thy fmz;

	        in (pI, (pors, pctxt), mI) end;

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

	    val dI = Context.theory_name (ThyC.sub_common (thy, thy'))

	    val hdl = case cas of

		    NONE => Auto_Prog.pblterm dI pI

		  | SOME t => subst_atomic ((Model_Pattern.variables ppc) ~~~ O_Model.values 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 (by_tactic_input Tactic.Model_Problem (pt, ([], Pbl))))

    end

(**)end(**)