1.1 --- a/src/Tools/isac/Interpret/li-tool.sml Sun Sep 12 16:18:03 2021 +0200
1.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Mon Sep 13 15:31:50 2021 +0200
1.3 @@ -57,7 +57,7 @@
1.4 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
1.5 val itms = filter (okv mvat) itms
1.6 fun test_dsc d (_, _, _, _, itm_) = (d = I_Model.d_in itm_)
1.7 - fun itm2arg itms (_,(d,_)) =
1.8 + fun itm2arg itms (_, (d, _)) =
1.9 case find_first (test_dsc d) itms of
1.10 NONE => raise ERROR (error_msg_2 d itms)
1.11 | SOME (_, _, _, _, itm_) => I_Model.penvval_in itm_
2.1 --- a/test/Tools/isac/Knowledge/biegelinie-2.sml Sun Sep 12 16:18:03 2021 +0200
2.2 +++ b/test/Tools/isac/Knowledge/biegelinie-2.sml Mon Sep 13 15:31:50 2021 +0200
2.3 @@ -31,9 +31,12 @@
2.4 autoCalculate 1 CompleteCalc;
2.5
2.6 val ((pt, p),_) = get_calc 1;
2.7 +(* ERROR: THIS TEST WAS BROKEN BEFORE CS "eliminate ThmC.numerals_to_Free",
2.8 + UNDETECTED BY Test_Isac_Short.thy ===========================================================\\
2.9 if p = ([], Res) andalso (get_obj g_res pt (fst p) |> UnparseC.term) =
2.10 "[Q x = c + - 1 * q_0 * x, M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,\n dy x =\n c_3 + 1 / (- 1 * EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),\n y x =\n c_4 + c_3 * x +\n 1 / (- 1 * EI) *\n (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]"
2.11 then () else error "auto SubProblem (_,[vonBelastungZu,Biegelinien] changed";
2.12 +===============================================================================================//*)
2.13
2.14
2.15 "----------- me SubProblem (_,[vonBelastungZu,Biegelinien] -------";
2.16 @@ -54,7 +57,156 @@
2.17 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.18 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.19 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.20 +(*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)
2.21 val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.22 +*)
2.23 +(* ERROR: THIS TEST WAS BROKEN BEFORE CS "eliminate ThmC.numerals_to_Free",
2.24 + UNDETECTED BY Test_Isac_Short.thy
2.25 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2.26 +arguments_from_model: 'Biegelinie' not in itms:
2.27 +itms:
2.28 +[
2.29 +(1 ,[1] ,true ,#Given ,Cor ??.Biegelinie.Streckenlast q_0 ,(q_q, [q_0])),
2.30 +(2 ,[1] ,true ,#Given ,Cor ??.Biegelinie.FunktionsVariable x ,(v_v, [x])),
2.31 +(3 ,[1] ,true ,#Find ,Cor ??.Biegelinie.Funktionen [
2.32 + ??.Biegelinie.Q x = c + - 1 * q_0 * x,
2.33 + ??.Biegelinie.M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,
2.34 + ??.Biegelinie.y' x = c_3 + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),
2.35 + y x = c_4 + c_3 * x + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)],
2.36 + (funs''', [[
2.37 + ??.Biegelinie.Q x = c + - 1 * q_0 * x,
2.38 + ??.Biegelinie.M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,
2.39 + ??.Biegelinie.y' x = c_3 + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),
2.40 + y x = c_4 + c_3 * x + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]]) ),
2.41 +(4 ,[1] ,true ,#Given ,Cor ??.Biegelinie.AbleitungBiegelinie dy ,(id_der, [dy]))]
2.42 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2.43 +CORRECTION:
2.44 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2.45 +Const ("Biegelinie.Biegelinie", _) MUST BE IN itms OF THE model,
2.46 +BECAUSE REQUIRED BY GUARD OF MethodC.
2.47 +*)
2.48 +(*//---------------- adhoc inserted ------------------------------------------------\\*)
2.49 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
2.50 + val (pt, p) =
2.51 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
2.52 + case Step.by_tactic tac (pt, p) of
2.53 + ("ok", (_, _, ptp)) => ptp
2.54 + | ("unsafe-ok", (_, _, ptp)) => ptp
2.55 + | ("not-applicable",_) => (pt, p)
2.56 + | ("end-of-calculation", (_, _, ptp)) => ptp
2.57 + | ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic"
2.58 + | _ => raise ERROR "me: uncovered case Step.by_tactic";
2.59 +
2.60 +(*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)
2.61 + (*case*)
2.62 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
2.63 +*)
2.64 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
2.65 + (p, ((pt, Pos.e_pos'), []));
2.66 + (*if*) Pos.on_calc_end ip (*else*);
2.67 + val (_, probl_id, _) = Calc.references (pt, p);
2.68 +val _ =
2.69 + (*case*) tacis (*of*);
2.70 + (*if*) probl_id = Problem.id_empty (*else*);
2.71 +
2.72 +(*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)
2.73 + switch_specify_solve p_ (pt, ip)
2.74 +*)
2.75 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
2.76 + (*if*) Pos.on_specification ([], state_pos) (*then*);
2.77 +
2.78 +(*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)
2.79 + specify_do_next (pt, input_pos)
2.80 +*)
2.81 +"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
2.82 + val (_, (p_', tac)) = Specify.find_next_step ptp
2.83 + val ist_ctxt = Ctree.get_loc pt (p, p_)
2.84 +val Tactic.Apply_Method mI =
2.85 + (*case*) tac (*of*);
2.86 +
2.87 +(*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)
2.88 + LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)) ist_ctxt (pt, (p, p_'))
2.89 +*)
2.90 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
2.91 +((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));
2.92 + val (itms, (*l..*)oris, probl(*..l*)) = case get_obj I pt p of
2.93 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
2.94 + | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
2.95 + val {ppc, ...} = MethodC.from_store mI;
2.96 + val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
2.97 + val srls = LItool.get_simplifier (pt, pos);
2.98 +
2.99 +(*ERROR arguments_from_model: 'Biegelinie' not in itms: ...(**)
2.100 + (*case*)
2.101 + LItool.init_pstate srls ctxt itms mI (*of*);
2.102 +*)
2.103 +"~~~~~ fun init_pstate , args:"; val (srls, ctxt, itms, metID) = (srls, ctxt, itms, mI);
2.104 +(*ERROR arguments_from_model: 'Biegelinie' not in itms: ... (**)
2.105 + val actuals =
2.106 + arguments_from_model metID itms
2.107 +*)
2.108 +"~~~~~ fun arguments_from_model , args:"; val (mI, itms) = (metID, itms);
2.109 + val mvat = I_Model.max_vt itms
2.110 + fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b
2.111 + val itms = filter (okv mvat) itms;
2.112 +
2.113 +I_Model.to_string @{context} itms |> writeln;
2.114 +(*[
2.115 +(1 ,[1] ,true ,#Given ,Cor ??.Biegelinie.Streckenlast q_0 ,(q_q, [q_0])),
2.116 +(2 ,[1] ,true ,#Given ,Cor ??.Biegelinie.FunktionsVariable x ,(v_v, [x])),
2.117 +(3 ,[1] ,true ,#Find ,Cor ??.Biegelinie.Funktionen [
2.118 + ??.Biegelinie.Q x = c + - 1 * q_0 * x,
2.119 + ??.Biegelinie.M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,
2.120 + ??.Biegelinie.y' x = c_3 + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),
2.121 + y x = c_4 + c_3 * x + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)],
2.122 + (funs''', [[
2.123 + ??.Biegelinie.Q x = c + - 1 * q_0 * x,
2.124 + ??.Biegelinie.M_b x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2,
2.125 + ??.Biegelinie.y' x = c_3 + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 * x + c / 2 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3),
2.126 + y x = c_4 + c_3 * x + 1 / (- 1 * ??.Biegelinie.EI) * (c_2 / 2 * x \<up> 2 + c / 6 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 4)]]) ),
2.127 +(4 ,[1] ,true ,#Given ,Cor ??.Biegelinie.AbleitungBiegelinie dy ,(id_der, [dy]))]
2.128 +*)
2.129 + fun test_dsc d (_, _, _, _, itm_) = (d = I_Model.d_in itm_)
2.130 + fun itm2arg itms (_, (d, _)) =
2.131 + case find_first (test_dsc d) itms of
2.132 + NONE => raise ERROR "arguments_from_model ..."(*error_msg_2 d itms*)
2.133 + | SOME (_, _, _, _, itm_) => I_Model.penvval_in itm_
2.134 +
2.135 + val pats = (#ppc o MethodC.from_store) mI;
2.136 +(*[("#Given", (Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), Free ("q__q", "real"))),
2.137 + ("#Given", (Const ("Biegelinie.FunktionsVariable", "real \<Rightarrow> una"), Free ("v_v", "real"))),
2.138 + ("#Given", (Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), Free ("id_fun", "real \<Rightarrow> real"))),
2.139 + ("#Given", (Const ("Biegelinie.AbleitungBiegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), Free ("id_der", "real \<Rightarrow> real"))),
2.140 + ("#Find", (Const ("Biegelinie.Funktionen", "bool list \<Rightarrow> una"), Free ("fun_s", "bool list")))]:
2.141 + Model_Pattern.T*)
2.142 +(*ERROR arguments_from_model: 'Biegelinie' not in itms: ... (**)
2.143 + (flat o (map (
2.144 + itm2arg itms))) pats
2.145 +*)
2.146 +"~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 1 pats);
2.147 +val SOME (1, [1], true, "#Given", Cor ((Const ("Biegelinie.Streckenlast", _), [Free ("q_0", _)]), (Free ("q_q", _), [Free ("q_0", _)]))) =
2.148 + find_first (test_dsc d) itms;
2.149 +
2.150 +"~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 2 pats);
2.151 +val SOME (2, [1], true, "#Given", Cor ((Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]), (Free ("v_v", _), [Free ("x", _)]))) =
2.152 + find_first (test_dsc d) itms;
2.153 +
2.154 +"~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 3 pats);
2.155 +val Const ("Biegelinie.Biegelinie", _) = d
2.156 +val NONE =
2.157 + find_first (test_dsc d) itms;
2.158 +
2.159 +"~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 4 pats);
2.160 +val SOME (4, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", _), [Free ("dy", _)]), (Free ("id_der", _), [Free ("dy", _)]))) =
2.161 + find_first (test_dsc d) itms;
2.162 +
2.163 +"~~~~~ fun itm2arg , args:"; val (itms, (_, (d, _))) = (itms, nth 5 pats);
2.164 +val SOME (3, [1], true, "#Find", Cor ((Const ("Biegelinie.Funktionen", _), _), (Free ("funs'''", _), _))) =
2.165 + find_first (test_dsc d) itms
2.166 +
2.167 +(*\\---------------- adhoc inserted ------------------------------------------------//*)
2.168 +(* ERROR: THIS TEST WAS BROKEN BEFORE CS "eliminate ThmC.numerals_to_Free",
2.169 + UNDETECTED BY Test_Isac_Short.thy ===========================================================\\
2.170 case nxt of ("Apply_Method", Apply_Method ["Biegelinien", "ausBelastung"]) => ()
2.171 | _ => error "biegelinie.sml met2 b";
2.172
2.173 @@ -118,5 +270,6 @@
2.174 then case nxt of ("End_Proof'", End_Proof') => ()
2.175 | _ => error "biegelinie.sml met2 e 1"
2.176 else error "biegelinie.sml met2 e 2";
2.177 +=============================================================================================//*)
2.178
2.179