(* Title:  Interpret/li-tool.sml

   Author: Walther Neuper 050908

   (c) copyright due to lincense terms.

*)

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

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

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

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

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

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

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

open Ctree;

open Pos;

open TermC;

open Istate;

open Tactic;

open Program;

open Auto_Prog;

open Fetch_Tacs;

open Pre_Conds;

open I_Model;

open P_Model

open Rewrite;

open Step;

open LItool;

open LI;

open Test_Code

open Specify

open Solve

open Prog_Tac

open Kernel

open ME_Misc

val thy =  @{theory Isac_Knowledge};

(** -------- 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) = Test_Code.init_calc @{context} [(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 Applicable.Yes m = Step.check tac (pt, p);

 (*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 {prog_rls, ...} = MethodC.from_store ctxt mI;

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

val thy' = get_obj g_domID pt p;

val thy = ThyC.get_theory @{context} thy';

val prog_rls = LItool.get_simplifier (pt, pos)

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

val ini = implicit_take @{context} 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 ------------";

*)

 States.reset ();

 CalcTree @{context} [(["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,_),_) = States.get_calc 1;

 Test_Tool.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 => [Tactic.Tac str];

 case tacs of [Tactic.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 ----------------------------";

 States.reset ();

 CalcTree @{context} [(["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, _), _) = States.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;

...

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

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

*)

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

 (*if*) Pos.on_specification (p, p_) (*else*);

        val pp = par_pblobj pt p

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

        val thy = ThyC.get_theory @{context} thy'

        val metID = get_obj g_metID pt pp

        val metID' =

          if metID = MethodC.id_empty 

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

          else metID

        val {program=Prog sc,prog_rls,asm_rls,rew_ord=ro,...} = MethodC.from_store ctxt 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, pos)) o rep_stacexpr o #1 o

           (check_leaf "selrul" ctxt prog_rls (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 op = o flat o (map (Tactic.applicable thy ro asm_rls f))) alltacs

...

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

### Tactic.applicable: 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 (TermC.parse thy)) "a+b";

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

> val plus_a = TermC.sub_at [L] t; 

> val b = TermC.sub_at [R] t; 

> val plus = TermC.sub_at [L,L] t; 

> val a = TermC.sub_at [L,R] t;

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

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

> val pl_pl_a_b = TermC.sub_at [L] t; 

> val c = TermC.sub_at [R] t; 

> val a = TermC.sub_at [L,R,L,R] t; 

> val b = TermC.sub_at [L,R,R] t; 

*)

(** -------- fun formal_args ----------------------------------- **)

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

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

(*

> formal_args program;

  [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 (TermC.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 (TermC.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={model=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 -----------------------------------------------------------------";

(*

  This test is deeply nested (down into details of creating environments).

  In order to make Sidekick show the structure add to each

  *                    (*/...\*) and        (*\.../*)

  * a companion  > ML < (*/...\*) and > ML < (*\.../*)

  Note the wrong ^----^ delimiters.

*)

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]",

(*

  Now follow items for ALL SubProblems,

  since ROOT MethodC must provide values for "actuals" of ALL SubProblems.

  See Biegelinie.thy subsection \<open>Survey on Methods\<close>.

*)

(*

  Items for MethodC "IntegrierenUndKonstanteBestimmen2"

*)

	    "FunktionsVariable x",

    (*"Biegelinie y",          ..already input for Problem above*)

      "AbleitungBiegelinie y'",

      "Biegemoment M_b",

      "Querkraft Q",

(*

  Item for Problem "LINEAR/system", which by [''no_met''] involves refinement

*)

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

];

val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],

		     ["IntegrierenUndKonstanteBestimmen2"]);

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

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

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

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

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

(*/---broken elementwise input to lists---\* )

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

                                        (*isa* ) val Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" = nxt

                                        ( *isa2*) val Add_Relation "Randbedingungen [y 0 = 0]" = nxt

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

                                        (*isa*) val Specify_Theory "Biegelinie" = nxt

                                        (*isa2* ) val Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]" = nxt( **)

( *\---broken elementwise input to lists---/*)

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

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

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

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

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

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

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

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

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

(*[], Met*)val return_me_Add_Given_GleichungsVariablen

                                = me nxt p c pt; (*val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt*)

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

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

      val ctxt = Ctree.get_ctxt pt p

val ("ok", (_, _, ptp as (pt, p))) =

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

        (*case*)

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

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

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

  (*if*) Pos.on_calc_end ip (*else*);

      val (_, probl_id, _) = Calc.references (pt, p);

val _ =

      (*case*) tacis (*of*);

        (*if*) probl_id = Problem.id_empty (*else*);

           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*);

           specify_do_next (pt, input_pos);

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

    val (_, (p_', tac)) = Specify.find_next_step ptp

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

val Tactic.Apply_Method mI =

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

  	    LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))

  	      ist_ctxt (pt, (p, p_'));

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

  ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));

      val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)

          PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)

        | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"

      val {model, ...} = MethodC.from_store ctxt mI;

      val itms = if itms <> [] then itms else I_Model.complete oris probl [] model

;

(*+*)if (itms |> I_Model.to_string @{context}) = "[\n" ^

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

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

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

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

  "(5 ,[1] ,true ,#Given ,Cor FunktionsVariable x , pen2str), \n" ^

  "(6 ,[1] ,true ,#Given ,Cor AbleitungBiegelinie y' , pen2str), \n" ^

  "(7 ,[1] ,true ,#Given ,Cor Biegemoment M_b , pen2str), \n" ^

  "(8 ,[1] ,true ,#Given ,Cor Querkraft Q , pen2str), \n" ^

  "(9 ,[1] ,true ,#Given ,Cor GleichungsVariablen [c, c_2, c_3, c_4] , pen2str)]"

(*+*)then () else error "init_pstate: initial i_model changed";

    (*case*)

    LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI (*of*);

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

"~~~~~ fun init_pstate , args:"; val (ctxt, i_model, met_id) = (ctxt, (I_Model.OLD_to_TEST itms), mI);

    val (model_patt, program, prog, prog_rls, where_, where_rls) =

      case MethodC.from_store ctxt met_id of

        {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...}=>

          (model_patt, program, prog, prog_rls, where_, where_rls)

    val return_of_max_variant = 

           of_max_variant model_patt i_model;

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

"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);

    val all_variants =

        map (fn (_, variants, _, _, _) => variants) i_model

        |> flat

        |> distinct op =

    val variants_separated = map (filter_variants' i_model) all_variants

    val sums_corr = map (cnt_corrects) variants_separated

    val sum_variant_s = arrange_args sums_corr (1, all_variants)

    val (_, max_variant) = hd (*..crude decision, up to improvement *)

      (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)

    val i_model_max =

      filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model

    val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat

;

(*+*)if (equal_descr_pairs |> descr_pairs_to_string @{context}) = "[" ^

(*defined: in program+model--vvvv--,----------------------------------------- in problem ---vvv*)

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

    "(Cor_TEST Traegerlaenge L , pen2str, Position.T))), " ^

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

    "(Cor_TEST Streckenlast q_0 , pen2str, Position.T))), " ^

  "((#Given, (Randbedingungen, r_b)), (4, [1], true ,#Relate, " ^

    "(Cor_TEST Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0] , pen2str, Position.T))), " ^

  "((#Given, (FunktionsVariable, fun_var)), (5, [1], true ,#Given, " ^

    "(Cor_TEST FunktionsVariable x , pen2str, Position.T))), " ^

  "((#Given, (AbleitungBiegelinie, id_der)), (6, [1], true ,#Given, " ^

    "(Cor_TEST AbleitungBiegelinie y' , pen2str, Position.T))), " ^

  "((#Given, (Biegemoment, id_momentum)), (7, [1], true ,#Given, " ^

    "(Cor_TEST Biegemoment M_b , pen2str, Position.T))), " ^

  "((#Given, (Querkraft, id_lat_force)), (8, [1], true ,#Given, " ^

    "(Cor_TEST Querkraft Q , pen2str, Position.T))), " ^

  "((#Given, (GleichungsVariablen, vs)), (9, [1], true ,#Given, " ^

    "(Cor_TEST GleichungsVariablen [c, c_2, c_3, c_4] , pen2str, Position.T))), " ^

  "((#Find, (Biegelinie, b_b)), (3, [1], true ,#Find, (" ^

    "Cor_TEST Biegelinie y , pen2str, Position.T)))]"

then () else error "of_max_variant: equal_descr_pairs CHANGED";

    val return_make_env_model = make_env_model equal_descr_pairs;

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

"~~~~~ fun make_env_model , args:"; val (equal_descr_pairs) = (equal_descr_pairs);

"~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 4 equal_descr_pairs;

"~~~~~ fun mk_env_model , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb);

           handle_lists id (descr, ts);

"~~~~~ fun handle_lists , args:"; val (id, (descr, ts)) = (id, (descr, ts));

(*+*)val "[x]" = ts |> UnparseC.terms @{context}

;

  (*if*) Model_Pattern.is_list_descr descr (*else*);

val return_handle_lists_step = [(id, Library.the_single ts)]

(*+*)val "[\"\n(fun_var, x)\"]" = return_handle_lists_step |> Subst.to_string @{context}

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

    val env_model = return_make_env_model

(*+*)val "[\"\n(l_l, L)\", \"\n(q_q, q_0)\", \"\n(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\", \"\n(fun_var, x)\", \"\n(id_der, y')\", \"\n(id_momentum, M_b)\", \"\n(id_lat_force, Q)\", \"\n(vs, [c, c_2, c_3, c_4])\", \"\n(b_b, y)\"]"

 = env_model |> Subst.to_string @{context}

(*|||----------------- contine of_max_variant ------------------------------------------------*)

    val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs

    val subst_eval_list = make_envs_preconds equal_givens

    val (env_subst, env_eval) = split_list subst_eval_list

(*bieg*)val "[\"\n(l_l, L)\", \"\n(q_q, q_0)\", \"\n(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\", \"\n(fun_var, x)\", \"\n(id_der, y')\", \"\n(id_momentum, M_b)\", \"\n(id_lat_force, Q)\", \"\n(vs, [c, c_2, c_3, c_4])\", \"\n(b_b, y)\"]"

 = env_model |> Subst.to_string @{context}

(*bieg*)val "[]" = env_subst |> Subst.to_string @{context}

val return_of_max_variant_step = (i_model_max, env_model, (env_subst, env_eval))

;

(*+*)if return_of_max_variant_step = return_of_max_variant then () else error "<>";

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

    val (_, env_model, (env_subst, env_eval)) = return_of_max_variant

(*||------------------ contine init_pstate ---------------------------------------------------*)

    val actuals = map snd env_model

(*+*) val "[L, q_0, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0], x, y', M_b, Q, [c, c_2, c_3, c_4], y]"

(*-----------------///--------------------------------------------------------------------------^^*)

 = actuals |> UnparseC.terms @{context}

    val formals = Program.formal_args prog

(*+*)val "[l_l, q_q, r_b, fun_var, id_der, id_momentum, id_lat_force, vs, b_b]"

 = formals |> UnparseC.terms @{context}

(*+*)val 9 = length formals

    val preconds =

      Pre_Conds.check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval))

    val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));

    val ist = Istate.e_pstate

      |> Istate.set_eval prog_rls

      |> Istate.set_env_true (relate_args [] formals actuals ctxt prog met_id formals actuals)

;

(*+*)(relate_args [] formals actuals ctxt prog met_id formals actuals)

;

val return_init_pstate = (Istate.Pstate ist, ctxt, program)

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

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

val (p,_,f,nxt,_,pt) = return_me_Add_Given_GleichungsVariablen;

                                                 val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt

(* final test ... ----------------------------------------------------------------------------*)

(*+*)val ([], Met) = p

(*+*)val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt