(* Title:  test/../script.sml

   Author: Walther Neuper 050908

   (c) copyright due to lincense terms.

*)

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

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

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

"----------- fun specific_from_prog ----------------------------";

"----------- fun implicit_take, fun get_first_argument -------------------------";

"----------- fun from_prog ---------------------------------------";

"----------- fun specific_from_prog ----------------------------";

"----------- fun de_esc_underscore -------------------------------";

"----------- fun go ----------------------------------------------";

"----------- fun formal_args -------------------------------------";

"----------- fun dsc_valT ----------------------------------------";

"----------- fun arguments_from_model ---------------------------------------";

"----------- fun init_pstate -----------------------------------------------------------------";

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

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

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

val thy =  @{theory Isac_Knowledge};

"----------- fun specific_from_prog ----------------------------";

"----------- fun specific_from_prog ----------------------------";

"----------- fun specific_from_prog ----------------------------";

reset_states ();

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

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

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

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalcHead;

autoCalculate 1 (Steps 1);

autoCalculate 1 (Steps 1);

val ((pt, p), _) = get_calc 1; show_pt pt;

val appltacs = specific_from_prog pt p;

case appltacs of 

  [Rewrite ("radd_commute", radd_commute), 

  Rewrite ("add.assoc", add_assoc), Calculate "TIMES"]

  => if (UnparseC.term o Thm.prop_of) radd_commute = "?m + ?n = ?n + ?m" andalso 

        (UnparseC.term o Thm.prop_of) add_assoc = "?a + ?b + ?c = ?a + (?b + ?c)" then ()

        else error "script.sml fun specific_from_prog diff.behav. 2"

| _ => error "script.sml fun specific_from_prog diff.behav. 1";

trace_LI := true;

trace_LI := false;

applyTactic 1 p (hd appltacs);

val ((pt, p), _) = get_calc 1; show_pt pt;

val appltacs = specific_from_prog pt p;

(*applyTactic 1 p (hd appltacs); WAS scan_dn1: call by ([3], Pbl)*)

"~~~~~ fun applyTactic, args:"; val ((cI:calcID), ip, tac) = (1, p, (hd appltacs));

val ((pt, _), _) = get_calc cI;

val p = get_pos cI 1;

Step.by_tactic;

Step.by_tactic tac;

(*Step.by_tactic tac (pt, ip); (*WAS scan_dn1: call by ([3], Pbl)*)*)

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

  val Appl m = applicable_in p pt tac ; (*Appl*)

  (*if*) Tactic.for_specify' m; (*false*)

(*loc_solve_ (mI,m) ptp; (*Argument: (mI, m) : string * tac Reason: Can't unify tac_ with tac*)*)

"~~~~~ fun loc_solve_, args:"; val (m ,(pt,pos)) = (m, ptp);

(*val (msg, cs') = Step_Solve.by_tactic m (pt, pos);

(*Argument: m : string * tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)

m;

(pt, pos);

"~~~~~ fun Step_Solve.by_tactic , args:"; val (m, (pt, po as (p,p_))) = (m, (pt, pos));

(*solve has still p_!!!!!!!!!!!!!!!!!!!!!!!!!*)

e_metID = get_obj g_metID pt (par_pblobj pt p); (*false*)

val ctxt = get_ctxt pt po;

(*generate1 m (Istate.empty, ctxt) (p,p_) pt;

(*Argument: m : tac Reason: Can't unify tac_ with tac (Different type constructors)*)*)

(ThyC.get_theory (get_obj g_domID pt (par_pblobj pt p)));

ThyC.get_theory;

(* ERROR  which has NOT be created by this change set

(1) actual         : ERROR exception PTREE "get_obj f EmptyPtree" raised (line 289 of "~~/src/Tools/isac/MathEngBasic/ctree-basic.sml")

(2) in 927379190abd: generate1: not impl.for Empty_Tac

in case (2) exn.ERROR _ was caught, while in case (1) exn.Ptree is not caught before toplevel

autoCalculate 1 CompleteCalc; (* ONE ERROR *)

==============================^^^^^^^^^^^^^*)

"----------- fun implicit_take, fun get_first_argument -------------------------";

"----------- fun implicit_take, fun get_first_argument -------------------------";

"----------- fun implicit_take, fun get_first_argument -------------------------";

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) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

"~~~~~ fun me, args:"; val tac = nxt;

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

val Appl m = applicable_in p pt tac;

 (*if*) Tactic.for_specify' m; (*false*)

"~~~~~ fun loc_solve_, args:"; val (m, (pt, pos) ) = (m, ptp);

"~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,ctxt), pos as (p,_))

  = (m, pos);

val {srls, ...} = get_met mI;

val PblObj {meth=itms, ...} = get_obj I pt p;

val thy' = get_obj g_domID pt p;

val thy = ThyC.get_theory thy';

val srls = LItool.get_simplifier (pt, pos)

val (is as Pstate {env, ...}, ctxt, sc) = init_pstate srls ctxt itms mI;

val ini = implicit_take sc env;

"----- fun implicit_take, args:"; val (Prog sc) = sc;

"----- fun get_first_argument, args:"; val (y, h $ body) = (thy, sc);

case get_first_argument sc of SOME (Free ("e_e", _)) => ()

| _ => error "script: Const (?, ?) in script (as term) changed";;

"----------- fun from_prog ---------------------------------------";

"----------- fun from_prog ---------------------------------------";

"----------- fun from_prog ---------------------------------------";

(* compare test/../interface.sml

"--------- getTactic, fetchApplicableTactics ------------";

*)

 reset_states ();

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

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

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

 Iterator 1;

 moveActiveRoot 1;

 autoCalculate 1 CompleteCalc;

 val ((pt,_),_) = get_calc 1;

 show_pt pt;

(*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)

 val tacs = from_prog pt ([],Pbl);

 case tacs of [Apply_Method ["Test", "squ-equ-test-subpbl1"]] => ()

 | _ => error "script.sml: diff.behav. in from_prog ([],Pbl)";

 val tacs = from_prog pt ([1],Res);

 case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",

      Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),

      Check_elementwise "Assumptions"] => ()

 | _ => error "script.sml: diff.behav. in from_prog ([1],Res)";

 val tacs = from_prog pt ([3],Pbl);

 case tacs of [Apply_Method ["Test", "solve_linear"]] => ()

 | _ => error "script.sml: diff.behav. in from_prog ([3],Pbl)";

 val tacs = from_prog pt ([3,1],Res);

 case tacs of [Rewrite_Set_Inst (["(''bdv'', x)"], "isolate_bdv"), Rewrite_Set "Test_simplify"] => ()

 | _ => error "script.sml: diff.behav. in from_prog ([3,1],Res)";

 val tacs = from_prog pt ([3],Res);

 case tacs of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",

      Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),

      Check_elementwise "Assumptions"] => ()

 | _ => error "script.sml: diff.behav. in from_prog ([3],Res)";

 val tacs = (from_prog pt ([],Res)) handle PTREE str => [Tac str];

 case tacs of [Tac "no tactics applicable at the end of a calculation"] => ()

 | _ => error "script.sml: diff.behav. in from_prog ([],Res)";

"----------- fun specific_from_prog ----------------------------";

"----------- fun specific_from_prog ----------------------------";

"----------- fun specific_from_prog ----------------------------";

 reset_states ();

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

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

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

 Iterator 1;

 moveActiveRoot 1;

 autoCalculate 1 CompleteCalc;

(*UC\label{SOLVE:MANUAL:TACTIC:listall} UC 30.3.2.2 p.175*)

 fetchApplicableTactics 1 99999 ([],Pbl);

 fetchApplicableTactics 1 99999 ([1],Res);

"~~~~~ fun fetchApplicableTactics, args:"; val (cI, (scope:int), (p:pos')) = (1, 99999, ([1],Res));

val ((pt, _), _) = get_calc cI;

(*version 1:*)

case from_prog pt p of [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify",

  Subproblem ("Test", ["LINEAR", "univariate", "equation", "test"]),

  Check_elementwise "Assumptions"] => ()

| _ => error "fetchApplicableTactics ([1],Res) changed";

(*version 2:*)

(*WAS:

specific_from_prog pt p;

...

### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])' 

### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"' 

*)

"~~~~~ fun specific_from_prog , args:"; val (pt, (p, p_)) = (pt, p);

Pos.on_specification p_ = false;

        val pp = par_pblobj pt p

        val thy' = (get_obj g_domID pt pp):ThyC.id

        val thy = ThyC.get_theory thy'

        val metID = get_obj g_metID pt pp

        val metID' =

          if metID = e_metID 

          then (thd3 o snd3) (get_obj g_origin pt pp)

          else metID

        val {scr=Prog sc,srls,erls,rew_ord'=ro,...} = get_met metID'

        val Pstate ist = get_istate_LI pt (p,p_)

        val ctxt = get_ctxt pt (p, p_)

        val alltacs = (*we expect at least 1 stac in a script*)

          map ((LItool.tac_from_prog pt thy) o rep_stacexpr o #1 o

           (check_leaf "selrul" ctxt srls (get_subst ist) )) (stacpbls sc)

        val f =

          (case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p

          | _ => error "");

(*WN120611 stopped and took version 1 again for fetchApplicableTactics !

(distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs

...

### atomic_appl_tacs: not impl. for tac='Subproblem(Test,["LINEAR","univariate","equation","test"])' 

### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"' 

*)

"----------- fun de_esc_underscore -------------------------------";

"----------- fun de_esc_underscore -------------------------------";

"----------- fun de_esc_underscore -------------------------------";

(*

> val str = "Rewrite_Set_Inst";

> val esc = esc_underscore str;

val it = "Rewrite'_Set'_Inst" : string

> val des = de_esc_underscore esc;

 val des = de_esc_underscore esc;*)

"----------- fun go ----------------------------------------------";

"----------- fun go ----------------------------------------------";

"----------- fun go ----------------------------------------------";

(*

> val t = (Thm.term_of o the o (parse thy)) "a+b";

val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term

> val plus_a = at_location [L] t; 

> val b = at_location [R] t; 

> val plus = at_location [L,L] t; 

> val a = at_location [L,R] t;

> val t = (Thm.term_of o the o (parse thy)) "a+b+c";

val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c","RealDef.real") : term

> val pl_pl_a_b = at_location [L] t; 

> val c = at_location [R] t; 

> val a = at_location [L,R,L,R] t; 

> val b = at_location [L,R,R] t; 

*)

"----------- fun formal_args -------------------------------------";

"----------- fun formal_args -------------------------------------";

"----------- fun formal_args -------------------------------------";

(*

> formal_args scr;

  [Free ("f_","RealDef.real"),Free ("v_","RealDef.real"),

   Free ("eqs_","bool List.list")] : term list

*)

"----------- fun dsc_valT ----------------------------------------";

"----------- fun dsc_valT ----------------------------------------";

"----------- fun dsc_valT ----------------------------------------";

(*> val t = (Thm.term_of o the o (parse thy)) "equality";

> val T = type_of t;

val T = "bool => Tools.una" : typ

> val dsc = dsc_valT t;

val dsc = "una" : string

> val t = (Thm.term_of o the o (parse thy)) "fixedValues";

> val T = type_of t;

val T = "bool List.list => Tools.nam" : typ

> val dsc = dsc_valT t;

val dsc = "nam" : string*)

"----------- fun arguments_from_model ---------------------------------------";

"----------- fun arguments_from_model ---------------------------------------";

"----------- fun arguments_from_model ---------------------------------------";

(*

> val sc = ... Solve_root_equation ...

> val mI = ("Program","sqrt-equ-test");

> val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];

> val ts = arguments_from_model thy mI itms;

> map (UnparseC.term_in_thy thy) ts;

["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list

*)

"----------- fun init_pstate -----------------------------------------------------------------";

"----------- fun init_pstate -----------------------------------------------------------------";

"----------- fun init_pstate -----------------------------------------------------------------";

val fmz = ["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 (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],

		     ["IntegrierenUndKonstanteBestimmen2"]);

val p = e_pos'; val c = [];

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

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

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

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Biegelinie y"*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)

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

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["Biegelinien"]*)

(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)

(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)

(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)

(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "AbleitungBiegelinie dy"*)

(*[], Met*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt''''' = Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)

(*+*)val PblObj {meth, spec = (thy, _ , metID), ...} = get_obj I pt''''' (fst p''''');

(*+*)val ctxt = get_ctxt pt''''' p''''';

(*+*)val srls = get_simplifier (pt''''', p''''');

"~~~~~ fun init_pstate , args:"; val (srls, thy, itms, metID) = (srls, ThyC.get_theory thy, meth, metID);

val (Pstate st, ctxt, Prog _) = init_pstate srls ctxt itms metID;

if pstate2str st =

   "([\"\n(l, L)\",\"\n(q, q_0)\",\"\n(v, x)\",\"\n(b, dy)\",\"\n(s, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\",\"\n(vs, [c, c_2, c_3, c_4])\",\"\n(id_abl, y)\"], [], erls_IntegrierenUndK.., NONE, \n??.empty, ORundef, false, true)"

then () else error "init_pstate changed for Biegelinie";

(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Model_Problem*)

if p = ([1], Pbl) 

then case nxt of Model_Problem => () | _ => error "Biegelinie 7.70 changed 1"

else error "modeling root-problem of Biegelinie 7.70 changed";