(* Title:  "Minisubpbl/150-add-given-Equation.sml"

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

*)

open Pos

open Ctree

open Tactic

open Test_Code

val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];

val (dI',pI',mI') =

  ("Test", ["sqroot-test", "univariate", "equation", "test"],

   ["Test", "squ-equ-test-subpbl1"]);

val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; (*nxt = ("Model_Problem"*)

                                       val Model_Problem = nxt

val return_me_Model_Problem =

           me nxt p [] pt;

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

"~~~~~ fun me , args:"; val (tac, (p:Pos.pos'), (_:Test_Code.NEW), (pt:Ctree.ctree)) = (nxt, p, [], pt);

    val (pt, p) = 

      (*ERROR Specify.item_to_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt ... see 100-init-rootpbl.sml*)

	    case Step.by_tactic tac (pt,p) of

		    ("ok", (_, _, ptp)) => ptp;

val return_do_next = (*case*)

      Step.do_next p ((pt, Pos.e_pos'), []) (*of*);

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

"~~~~~ fun do_next , args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) =

  (p, ((pt, e_pos'),[]));

    val pIopt = get_pblID (pt,ip);

    (*if*) ip = ([],Res); (* = false*)

      val _ = (*case*) tacis (*of*);

      val SOME _ = (*case*) pIopt (*of*);

    val ("ok", ([(Add_Given "equality (x + 1 = 2)", _, _)], [], _)) =

      Step.switch_specify_solve p_ (pt, ip);

"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));

      (*if*) Pos.on_specification ([], state_pos) (*then*);

    val return_specify_do_next as ("ok", ([(Add_Given "equality (x + 1 = 2)", _, _)], [], _)) =

      Step.specify_do_next (pt, input_pos);

(*+ keep for fun specify_do_next \<longrightarrow>fun switch_specify_solve*)val (pt'''''_', input_pos'''''_') =

                           (pt, input_pos);

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

"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);

    val (_, (p_', tac as Add_Given "equality (x + 1 = 2)")) = Specify.find_next_step ptp

    val ist_ctxt =  Ctree.get_loc pt (p, p_)

val _ =

    (*case*) tac (*of*);

    val ("ok", ([(Add_Given "equality (x + 1 = 2)", _, _)], [], _)) =

      Step_Specify.by_tactic_input tac (pt, (p, p_'))  (*return from specify_do_next*);

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

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

val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next;

(*|------------------- continue with me_Model_Problem ----------------------------------------*)

val tacis as (_::_) =

        (*case*) ts (*of*);

          val (tac, _, _) = last_elem tacis

val return_me_Model_Problem =

      (p, [] : NEW, TESTg_form ctxt (pt, p) (* form output comes from Step.by_tactic *), 

  	    tac, Celem.Sundef, pt)

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

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

                                       val Add_Given "equality (x + 1 = 2)" = nxt

(*ERROR me: uncovered case Step.by_tactic* )

val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "solveFor x" = nxt;

( *ERROR me: uncovered case Step.by_tactic*)