(* Title:  "Minisubpbl/250-Rewrite_Set-from-method.sml"

   Author: Walther Neuper 1105

   (c) copyright due to lincense terms.

*)

"----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";

"----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";

"----------- Minisubpbl/800-append-on-Frm.sml ------------------------------------------------";

(*cp from -- appendFormula: on Frm + equ_nrls --- in Interpret.inform.sml --------------------*)

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"]);

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];(*Model_Problem*)

            (*autoCalculate 1 CompleteCalcHead;*)

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Given "equality (x + 1 = 2)"*)

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

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Add_Find "solutions L"*)

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Theory "Test"*)

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"]*)

 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)

 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p [] pt;(*Apply_Method ["Test", "squ-equ-test-subpbl1"])*);

            (*autoCalculate 1 (Steps 1);*)

 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Rewrite_Set", Rewrite_Set "norm_equation")*)

(*+*)Test_Tool.show_pt_tac pt;                                                                  (*isa==REP [

([], Frm), solve (x + 1 = 2, x)

. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],

([1], Frm), x + 1 = 2

. . . . . . . . . . Empty_Tac] *)

         (*appendFormula 1 "2+ - 1 + x = 2";*)

"~~~~~ fun appendFormula , args:"; val (ifo) = ("2+ - 1 + x = 2");

    val cs = (*get_calc cI*)  ((pt, p), [])  (*..continue fun me*)

    val pos = (*get_pos cI 1*)  p            (*..continue fun me*)

    val ("ok", cs' as (_, _, ptp''''')) = (*case*)

      Step.do_next pos cs (*of*);

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

    val pIopt = Ctree.get_pblID (pt, ip);

    (*if*) ip = ([], Pos.Res) (*else*);

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

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

      Step.switch_specify_solve p_ (pt, ip);

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

      (*if*) member op = [Pos.Pbl, Pos.Met] state_pos (*else*);

        LI.do_next (pt, input_pos);

"~~~~~ and do_next , args:"; val ((ptp as (pt, pos as (p, p_)))) = (pt, input_pos);

    (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);

        val thy' = get_obj g_domID pt (par_pblobj pt p);

	      val ((ist, ctxt), sc) = LItool.resume_prog thy' (p,p_) pt;

val Next_Step (ist, ctxt, tac) = (*case*)              (**..Ctree NOT updated yet**)

        LI.find_next_step sc (pt, pos) ist ctxt (*of*);

(*+*)val ("ok", ([(Rewrite_Set "norm_equation", _, (([1], Frm), _))], _, _)) =

        LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;

"~~~~~ fun by_tactic , args:"; val (tac_, is, (pt, pos)) = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp);

      val pos = next_in_prog' pos;

 	    (** )val (pos', c, _, pt) =( **)

      Step.add tac_ is (pt, pos);

"~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))

  = (tac_, is, (pt, pos));

(*+*)pos = ([1], Frm);

      (** )val (pt, c) =( **)

           cappend_atomic pt p (is, ContextC.insert_assumptions asm ctxt) f 

                     (Tactic.Rewrite_Set (Rule_Set.id rls')) (f',asm) Complete;

"~~~~~ fun cappend_atomic , args:"; val (pt, p: pos, ic_res, f, r, f', s)

  = (pt, p, (is, ContextC.insert_assumptions asm ctxt), f,

      (Tactic.Rewrite_Set (Rule_Set.id rls')), (f',asm), Complete);

  (*if*) existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) (*then*);

      val (ic_form, f) = (get_loc pt (p, Frm), get_obj g_form pt p)

	    val (pt, cs) = cut_tree(*!*)pt (p, Frm);

	    (** )val pt = ( **)

           append_atomic p (SOME ic_form, ic_res) f r f' s pt;

"~~~~~ fun append_atomic , args:"; val (p, (ic_form, ic_res), f, r, f', s, pt)

  = (p, (SOME ic_form, ic_res), f, r, f', s, pt);

      (*if*) existpt p pt andalso Tactic.is_empty (get_obj g_tac pt p) (*else*);

    val (iss, f) =

        ((ic_form, SOME ic_res), f); (*return from if*)

     insert_pt (PrfObj {form = f, tac = r, loc = iss, branch = NoBranch,

		   result = f', ostate = s}) pt p (*return from append_atomic*);

"~~~~~ from fun append_atomic \<longrightarrow>fun cappend_atomic , return:"; val (pt)

  = (insert_pt (PrfObj {form = f, tac = r, loc = iss, branch = NoBranch,

		   result = f', ostate = s}) pt p);

(*/--------------------- step into Deriv.embed -----------------------------------------------\*)

    val ("ok", ([], _, ptp''''' as (_, ([1], Res)))) =

    (*case*)

Step_Solve.by_term ptp (encode ifo) (*of*);

"~~~~~ fun by_term , args:"; val ((pt, pos as (p, _)), istr) = (ptp, (encode ifo));

  val SOME f_in =(*case*) TermC.parseNEW (get_ctxt pt pos) istr (*of*);

      val pos_pred = lev_back(*'*) pos

  	  val f_pred = Ctree.get_curr_formula (pt, pos_pred);

  	  val f_succ = Ctree.get_curr_formula (pt, pos);

      (*if*) f_succ = f_in (*else*);

        val NONE =(*case*) CAS_Cmd.input f_in (*of*);

          (*case*)

        LI.locate_input_term (pt, pos) f_in (*of*);

"~~~~~ fun locate_input_term , args:"; val ((pt, pos), tm) = ((pt, pos), f_in);

   		val pos_pred = Pos.lev_back' pos (*f_pred ---"step pos cs"---> f_succ in appendFormula*)

   		val _(*f_pred*) = Ctree.get_curr_formula (pt, pos_pred);

	(*case*) compare_step ([], [], (pt, pos_pred)) tm (*of*);

"~~~~~ fun compare_step , args:"; val ((tacis, c, ptp as (pt, pos as (p, _))), ifo) = (([], [], (pt, pos_pred)), tm);

    val fo = Calc.current_formula ptp

	  val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))

	  val {rew_ord, erls, rules, ...} = Rule_Set.rep nrls

	  val (found, der) = Derive.steps rew_ord erls rules fo ifo; (*<---------------*)

    (*if*) found (*then*);

         val tacis' = map (State_Steps.make_single rew_ord erls) der;

		     val (c', ptp) =

    Derive.embed tacis' ptp;

"~~~~~ fun embed , args:"; val (tacis, (pt, pos as (p, Res))) = (tacis', ptp);

      val (res, asm) = (State_Steps.result o last_elem) tacis

    	val (ist, ctxt) = case Ctree.get_obj Ctree.g_loc pt p of

    	  (_, SOME (ist, ctxt)) => (ist, ctxt)

      | (_, NONE) => error "Derive.embed Frm: uncovered case get_obj"

    	val (f, _) = Ctree.get_obj Ctree.g_result pt p

    	val p = Pos.lev_on p(*---------------only difference to (..,Frm) above*);

    	val tacis = (Tactic.Begin_Trans, Tactic.Begin_Trans' f, ((p, Pos.Frm), (Istate_Def.Uistate, ctxt))) ::

    		(State_Steps.insert_pos ((Pos.lev_on o Pos.lev_dn) p) tacis) @ [(Tactic.End_Trans, Tactic.End_Trans' (res, asm), 

    			(Pos.pos_plus (length tacis) (Pos.lev_dn p, Pos.Res), (Ctree.new_val res ist, ctxt)))];

    	val {nrls, ...} = MethodC.from_store (Ctree.get_obj Ctree.g_metID pt (Ctree.par_pblobj pt p))

    	val (pt, c, pos as (p, _)) =

Solve_Step.s_add_general (rev tacis) (pt, [], (p, Res));

"~~~~~ fun s_add_general , args:"; val (tacis, (pt, c, _)) = ((rev tacis), (pt, [], (p, Res)));

(*+*)length tacis = 8;

(*+*)if State_Steps.to_string tacis = "[\"\n" ^

  "( End_Trans, End_Trans' xxx, ( ([2, 6], Res), Pstate ([\"\n(e_e, x + 1 = 2)\", \"\n" ^

  "(v_v, x)\"], [], empty, NONE, \n2 + - 1 + x = 2, ORundef, false, true) ))\", \"\n" ^

  "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2, 6], Res), Uistate ))\", \"\n" ^

  "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2, 5], Res), Uistate ))\", \"\n" ^

  "( Rewrite (\"sym_radd_left_commute\", \"?y + (?x + ?z) = ?x + (?y + ?z)\"), Rewrite' , ( ([2, 4], Res), Uistate ))\", \"\n" ^

  "( Rewrite (\"sym_radd_commute\", \"?n + ?m = ?m + ?n\"), Rewrite' , ( ([2, 3], Res), Uistate ))\", \"\n" ^

  "( Rewrite (\"#: 1 + x = - 1 + (2 + x)\", \"1 + x = - 1 + (2 + x)\"), Rewrite' , ( ([2, 2], Res), Uistate ))\", \"\n" ^

  "( Rewrite (\"radd_commute\", \"?m + ?n = ?n + ?m\"), Rewrite' , ( ([2, 1], Res), Uistate ))\", \"\n" ^

  "( Begin_Trans, Begin_Trans' xxx, ( ([2], Frm), Uistate ))\"]"

then () else error "Derive.embed CHANGED";

      val (tacis', (_, tac_, (p, is))) = split_last tacis

(*+*)val Begin_Trans' _ = tac_;

	    val (p',c',_,pt') = Specify_Step.add tac_ is (pt, p)

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

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

(*/--------------------- final test ----------------------------------------------------------\*)

val (SOME (Uistate, ctxt_frm), SOME (ist_res, ctxt_res)) = get_obj g_loc (fst ptp''''') (fst (snd ptp'''''))

;

if

  (ctxt_frm |> get_assumptions |> UnparseC.terms) = "[\"precond_rootmet x\"]"

  andalso

  (ctxt_res |> get_assumptions |> UnparseC.terms) = "[\"precond_rootmet x\"]"

  andalso

  Istate.string_of ist_res =

    "Pstate ([\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\"], [], empty, NONE, \n2 + - 1 + x = 2, ORundef, false, true)"

then () else error "/800-append-on-Frm.sml CHANGED";

Test_Tool.show_pt_tac (fst ptp''''');(*[

([], Frm), solve (x + 1 = 2, x)

. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],

([1], Frm), x + 1 = 2

. . . . . . . . . . Derive Test_simplify,

([1,1], Frm), x + 1 = 2

. . . . . . . . . . Rewrite ("radd_commute", "?m + ?n = ?n + ?m"),

([1,1], Res), 1 + x = 2

. . . . . . . . . . Rewrite ("#: 1 + x = - 1 + (2 + x)", "1 + x = - 1 + (2 + x)"),

([1,2], Res), - 1 + (2 + x) = 2

. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),

([1,3], Res), - 1 + (x + 2) = 2

. . . . . . . . . . Rewrite ("sym_radd_left_commute", "?y + (?x + ?z) = ?x + (?y + ?z)"),

([1,4], Res), x + (- 1 + 2) = 2

. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),

([1,5], Res), x + (2 + - 1) = 2

. . . . . . . . . . Rewrite ("sym_radd_commute", "?n + ?m = ?m + ?n"),

([1,6], Res), 2 + - 1 + x = 2

. . . . . . . . . . Tactic.input_to_string not impl. for ?!,

([1], Res), 2 + - 1 + x = 2

. . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"]] 

*)