prepare 2: adapt LItool.init_pstate to I_Model with Position.T
authorwneuper <Walther.Neuper@jku.at>
Tue, 23 May 2023 08:34:53 +0200
changeset 6071129ff4e97cad9
parent 60710 21ae85b023bb
child 60712 8e882ca73d18
prepare 2: adapt LItool.init_pstate to I_Model with Position.T

a monster changeset: startet too ambitiously, very successfully -- and didn't want to re-do all that
test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy
test/Tools/isac/Interpret/li-tool.sml
test/Tools/isac/Knowledge/biegelinie-4.sml
test/Tools/isac/Test_Isac_Short.thy
     1.1 --- a/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy	Tue May 23 07:56:29 2023 +0200
     1.2 +++ b/test/Tools/isac/BridgeJEdit/Test_VSCode_Example.thy	Tue May 23 08:34:53 2023 +0200
     1.3 @@ -77,12 +77,12 @@
     1.4  (*reminder for Template.show ----------------------------------------------------------------\*)
     1.5                      val ((_, _, _), (_, pbl_id as ["univariate_calculus", "Optimisation"], _)) =
     1.6                        References.for_eval_model (thy_id, probl_id, meth_id) spec_ref o_ref
     1.7 +                    val {model = model_patt, where_ = where_ctree, where_rls, ...} =
     1.8 +                      Problem.from_store ctxt pbl_id;
     1.9  
    1.10                      val (_, env_eval) = Pre_Conds.sep_variants_envs_OLD model_patt probl
    1.11 -                    (*------------------- must be completed first ---^^^^^*)
    1.12 +                    (*------------------- must be completed first -----------------^^^^^*)
    1.13  
    1.14 -                    val {model = model_patt, where_ = where_ctree, where_rls, ...} =
    1.15 -                      Problem.from_store ctxt pbl_id;
    1.16                      val _ =
    1.17                        case I_Model.is_complete_OLD ctxt model_patt where_rls where_ctree probl of
    1.18                          NONE => writeln "I_Model.is_complete_OLD --> NONE"
     2.1 --- a/test/Tools/isac/Interpret/li-tool.sml	Tue May 23 07:56:29 2023 +0200
     2.2 +++ b/test/Tools/isac/Interpret/li-tool.sml	Tue May 23 08:34:53 2023 +0200
     2.3 @@ -46,7 +46,7 @@
     2.4  val thy' = get_obj g_domID pt p;
     2.5  val thy = ThyC.get_theory @{context} thy';
     2.6  val prog_rls = LItool.get_simplifier (pt, pos)
     2.7 -val (is as Pstate {env, ...}, ctxt, sc) = init_pstate prog_rls ctxt itms mI;
     2.8 +val (is as Pstate {env, ...}, ctxt, sc) = init_pstate ctxt (I_Model.OLD_to_TEST itms) mI;
     2.9  val ini = implicit_take @{context} sc env;
    2.10  "----- fun implicit_take, args:"; val (Prog sc) = sc;
    2.11  "----- fun get_first_argument, args:"; val (y, h $ body) = (thy, sc);
    2.12 @@ -245,7 +245,7 @@
    2.13  (*+*)val ctxt = get_ctxt pt''''' p''''';
    2.14  (*+*)val prog_rls = get_simplifier (pt''''', p''''');
    2.15  "~~~~~ fun init_pstate , args:"; val (prog_rls, thy, itms, metID) = (prog_rls, ThyC.get_theory @{context} thy, meth, metID);
    2.16 -val (Pstate st, ctxt, Prog _) = init_pstate prog_rls ctxt itms metID;
    2.17 +val (Pstate st, ctxt, Prog _) = init_pstate ctxt (I_Model.OLD_to_TEST itms) metID;
    2.18  if pstate2str st =
    2.19     "([\"\n(l_l, L)\", \"\n(q_q, q_0)\", \"\n(fun_var, x)\", \"\n(b_b, dy)\", \"\n(r_b, [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_der, y)\"], [], erls_IntegrierenUndK.., NONE, \n??.empty, ORundef, false, true)"
    2.20  then () else error "init_pstate changed for Biegelinie";
     3.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml	Tue May 23 07:56:29 2023 +0200
     3.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml	Tue May 23 08:34:53 2023 +0200
     3.3 @@ -121,7 +121,7 @@
     3.4      val (tac as Model_Problem (*[''makeFunctionTo'', ''"equation'']*), (pt, p as ([2, 1], Pbl))) =
     3.5      (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
     3.6        (* ERROR for a long time -----vvvvvvvvvvvvvvvvvvvvvvvv.. (should be evaluated!) *)
     3.7 -      val (tac as Substitute ["x = (argument_in lhs (NTH 1 [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]))"], (pt, p as ([2, 1, 1], Frm))) =
     3.8 +      val (tac as Substitute ["x = 0"], (pt, p as ([2, 1, 1], Frm))) =
     3.9        (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me';
    3.10  
    3.11  if p = ([2, 1, 1], Frm) andalso (Calc.current_formula (pt, p) |> UnparseC.term @{context}) =
     4.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Tue May 23 07:56:29 2023 +0200
     4.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Tue May 23 08:34:53 2023 +0200
     4.3 @@ -362,6 +362,7 @@
     4.4    ML_file "Knowledge/biegelinie-4.sml"
     4.5  ML \<open>
     4.6  \<close> ML \<open>
     4.7 +\<close> ML \<open>
     4.8  \<close>
     4.9    ML_file "Knowledge/algein.sml"
    4.10  ML \<open>