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

   Author: Walther Neuper

   (c) due to copyright terms

*)

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

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

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

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

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

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

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

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 (p''''',_,f,nxt''''',_,pt''''') = me nxt p [] pt; (*\<rightarrow>Add_Find "Biegelinie y"*)

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

(*+*)val Add_Given "Streckenlast q_0" = nxt;

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

  val ("ok", ([(Add_Given "Streckenlast q_0", _, _)], [], _)) = (*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*);

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

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 (sel, ct, (pt, pos as (p,_(*Frm, Pbl*)))) =

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

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

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

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

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

        val {ppc, where_, prls, ...} = Problem.from_store ctxt cpI;

(*+*)if Model_Pattern.to_string ppc = "[\"" ^

  "(#Given, (Traegerlaenge, l_l))\", \"" ^

  "(#Given, (Streckenlast, q_q))\", \"" ^

  "(#Find, (Biegelinie, b_b))\", \"" ^

  "(#Relate, (Randbedingungen, r_b))\"]"

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

(*+*)if O_Model.to_string 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 Add (2, [1], true, "#Given", Cor ((Const (\<^const_name>\<open>Streckenlast\<close>, _), [Free ("q_0", _)]),

      (Free ("q_q", _), [Free ("q_0", _)]))) = (*case*)

   I_Model.check_single ctxt sel oris pbl ppc ct (*of*);

"~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) = (ctxt, sel, oris, pbl, ppc, ct);

      val SOME t =(*case*) TermC.parseNEW ctxt str (*of*);

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

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

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

(*+*)O_Model.single_to_string ori';

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

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

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

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

             Add itm  (*return from add_single*);

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

	            val pbl' = I_Model.add_single thy itm pbl;

(*+*)if I_Model.to_string ctxt pbl' = "[\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";

(* this is under cleanup ...*)

              val tac' = I_Model.make_tactic sel (ct, pbl')

	            val (p, pt') =

	              case Specify_Step.add tac' (Istate_Def.Uistate, ctxt) (pt, (p, Pos.Pbl)) of

  	              ((p, Pos.Pbl), _, _, pt') => (p, pt')

  	            | _ => raise ERROR "by_Add_: uncovered case of Specify_Step.add"

  	            (* only for getting final p_ ..*)

	            val (pb, pre) = Pre_Conds.check prls where_ pbl' 0;

(*+*)if pre = [] then () else error "FINAL Pre_Conds.check' CHANGED 1";

(*+*)if pb = true then () else error "FINAL Pre_Conds.check' CHANGED 1";

(*-------------------- stop step into -------------------------------------------------------*)

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

(*[], 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"