(* Title:  "Specify/i-model.sml"

   Author: Walther Neuper

   (c) due to copyright terms

*)

"-----------------------------------------------------------------------------------------------";

"table of contents -----------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"----------- investigate fun add_single in I_Model ---------------------------------------------";

"----------- build I_Model.init_TEST -----------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

"-----------------------------------------------------------------------------------------------";

open I_Model;

"----------- investigate fun add_single in I_Model -------------------------------------------";

"----------- investigate fun add_single in I_Model -------------------------------------------";

"----------- investigate fun add_single in I_Model -------------------------------------------";

val f_model = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",

	"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",

	"FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",

  "AbleitungBiegelinie dy"];

val f_spec = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);

(*[], Pbl*)val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(f_model, f_spec)]; (*\<rightarrow>Model_Problem*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "Traegerlaenge L"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = Add_Given "Streckenlast q_0"*)

(*[], Pbl*)val return_me_Add_Given =

           me nxt p [] pt; (*\<rightarrow>Add_Find "Biegelinie y"*)

(*/------------------- step into me Add_Given ----------------------------------------------\\*)

"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, [], pt);

val ("ok", (_, _, ptp)) = (*case*)

      Step.by_tactic tac (pt, p) (*of*);

"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));

  val Applicable.Yes tac' = (*case*)

      Step.check tac (pt, p) (*of*);

	    (*if*) Tactic.for_specify' tac' (*then*);

Step_Specify.by_tactic tac' ptp;

"~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp);

val ("ok", ([(Add_Given "Streckenlast q_0", _, _)], [], _)) = (*case*)

   Specify.by_Add_ "#Given" ct (pt, p);

"~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) =

  ("#Given", ct, (pt, p));

    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)

;

(*+*)if O_Model.to_string @{context} oris = "[\n" ^

  "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^

  "(2, [\"1\"], #Given, Streckenlast, [\"q_0\"]), \n" ^

  "(3, [\"1\"], #Find, Biegelinie, [\"y\"]), \n" ^

  "(4, [\"1\"], #Relate, Randbedingungen, [\"[y 0 = 0]\", \"[y L = 0]\", \"[M_b 0 = 0]\", \"[M_b L = 0]\"]), \n" ^

  "(5, [\"1\"], #undef, FunktionsVariable, [\"x\"]), \n" ^

  "(6, [\"1\"], #undef, GleichungsVariablen, [\"[c]\", \"[c_2]\", \"[c_3]\", \"[c_4]\"]), \n" ^

  "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"

(*+*)then () else error "INITIAL O_Model CHANGED";

(*+*)if I_Model.to_string ctxt pbl = "[\n" ^

  "(0 ,[] ,false ,#Given ,Inc Streckenlast ,(??.empty, [])), \n" ^

  "(0 ,[] ,false ,#Find ,Inc Biegelinie ,(??.empty, [])), \n" ^

  "(0 ,[] ,false ,#Relate ,Inc Randbedingungen [] ,(??.empty, [])), \n" ^

  "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L]))]"

(*+*)then () else error "INITIAL I_Model CHANGED";

val return_check_single = (*case*)

   I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);

(*//------------------ step into check_single ----------------------------------------------\\*)

"~~~~~ fun check_single , args <>[]:"; val (ctxt, m_field, o_model, i_model, m_patt, str)

  = (ctxt, m_field, oris, i_model, m_patt, ct);

      val (t as (descriptor $ _)) = Syntax.read_term ctxt str

        handle ERROR msg => error (msg (*^ Position.here pp*))

val SOME m_field' =

        (*case*) Model_Pattern.get_field descriptor m_patt (*of*);

          (*if*) m_field <> m_field' (*else*);

(**)val ("", ori', all) =(**)

          (*case*) O_Model.contains ctxt m_field o_model t (*of*);

(*+*)O_Model.single_to_string @{context} ori';

(*+*)val [Free ("q_0", _)] = all;

(**)val ("", itm) =(**)

 (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*);

(*+*)val (2, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]), (Free ("q_q", _), [Free ("q_0", _)]))) = itm

(*\\------------------ step into check_single ----------------------------------------------//*)

val return_check_single = Add itm;

"~~~~~ from fun check_single \<longrightarrow>fun by_Add_ , return:"; val (I_Model.Add i_single) = (return_check_single);

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

;

(*+*)if I_Model.to_string ctxt i_model' = "[\n" ^

  "(0 ,[] ,false ,#Find ,Inc Biegelinie ,(??.empty, [])), \n" ^

  "(0 ,[] ,false ,#Relate ,Inc Randbedingungen [] ,(??.empty, [])), \n" ^

  "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])), \n" ^

  "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0]))]"

(*+*)then () else error "FINAL I_Model CHANGED";

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

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

              [], (pt', pos)));

(*-------------------- stop into me Add_Given ------------------------------------------------*)

(*\------------------- step into me Add_Given ----------------------------------------------//*)

                                val (p,_,f,nxt,_,pt) = return_me_Add_Given

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]"*)

(* final test ...*)

if p = ([], Pbl) then

  case nxt of Add_Relation "Randbedingungen [y 0 = 0]" => () | _ => error "investigate fun add_single CHANGED 1"

else error "investigate fun add_single CHANGED 2"

"----------- build I_Model.init_TEST -----------------------------------------------------------";

"----------- build I_Model.init_TEST -----------------------------------------------------------";

"----------- build I_Model.init_TEST -----------------------------------------------------------";

(*/---------------------------------------- mimic input from PIDE -----------------------------\*)

(* Test_Example "Diff_App-No.123a" (*complete Model, empty References*) *)

val in_refs as (thy_id, probl_id, meth_id) = ("__", "__/__", "__/__")

val thy = @{theory}

val model_input = (*type Position.T is hidden, thus redefinition*)

 [("#Given", [("Constants [r = 7]", Position.none)]),

  ("#Where", [("0 < r", Position.none)]),

  ("#Find",

   [("Maximum A", Position.none), ("AdditionalValues [u, v]", Position.none)]),

  ("#Relate",

   [("Extremum (A = 2 * u * v - u \<up> 2)", Position.none),

    ("SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]", Position.none)])]

: (Model_Pattern.m_field * (string * Position.T) list) list

val example_id = "Diff_App-No.123a";

(*----------------------------------------- init state -----------------------------------------*)

set_data Ctree.EmptyPtree thy;

(*\---------------------------------------- mimic input from PIDE -----------------------------/*)

val Ctree.EmptyPtree =

              (*case*) the_data thy (*of*);

(* Calculation..*)

"~~~~~ fun init_ctree_TEST , args:"; val (thy, example_id) = (thy, example_id);

      val example_id' = References_Def.explode_id example_id

      val (_, (formalise as (model, refs as (thy_id, probl_id, meth_id)))) =

        Store.get (Know_Store.get_expls @{theory}) example_id' example_id' 

      val {model = model_patt, ...} = Problem.from_store (Proof_Context.init_global thy) probl_id

      val (o_model, ctxt) = O_Model.init thy model model_patt

;

(*+*)o_model: O_Model.T; (* |> O_Model.to_string @{context}*)

(*+*)val ("Diff_App", ["univariate_calculus", "Optimisation"], ["Optimisation", "by_univariate_calculus"]) =

(*+*)  refs

      val empty_i_model = I_Model.init_TEST ctxt model_patt;

(*+*)if I_Model.to_string @{context} empty_i_model =

(*+*)  "[\n(0 ,[] ,false ,#Given ,Syn Constants [__=__, __=__]), \n" ^

(*+*)  "(0 ,[] ,false ,#Find ,Syn Maximum __), \n" ^

(*+*)  "(0 ,[] ,false ,#Find ,Syn AdditionalValues [__, __]), \n" ^

(*+*)  "(0 ,[] ,false ,#Relate ,Syn Extremum __), \n" ^

(*+*)  "(0 ,[] ,false ,#Relate ,Syn SideConditions [__=__, __=__])]"

(*+*)then () else error "final test of build I_Model.init_TEST FAILED";