1.1 --- a/src/Tools/isac/Test_Code/test-code.sml Mon Jun 29 16:01:01 2020 +0200
1.2 +++ b/src/Tools/isac/Test_Code/test-code.sml Mon Jun 29 17:27:34 2020 +0200
1.3 @@ -18,6 +18,9 @@
1.4 val me_trace: Calc.T -> Tactic.input -> (Calc.T -> Tactic.input -> unit) ->
1.5 Calc.T * Tactic.input * Test_Out.mout
1.6
1.7 + val CalcTreeTEST': Formalise.T list -> Tactic.input * Calc.T
1.8 + val me': Tactic.input * Calc.T -> Tactic.input * Calc.T
1.9 +
1.10 val tac2tac_ : Ctree.ctree -> Pos.pos' -> Tactic.input -> Tactic.T
1.11 end
1.12
1.13 @@ -134,23 +137,22 @@
1.14 val _ = if quiet tac then () else
1.15 writeln ("========= " ^ Pos.pos'2str p ^ "========= Step.by_tactic: " ^ Tactic.input_to_string tac ^ " ==================================");
1.16 val (pt', p') =
1.17 - (*Step.by_tactic is here for testing by me; do_next would suffice for doing steps*)
1.18 case Step.by_tactic tac (pt, p) of
1.19 ("ok", (_, _, ptp)) => ptp
1.20 | ("unsafe-ok", (_, _, ptp)) => ptp
1.21 | ("not-applicable",_) => (pt, p)
1.22 | ("end-of-calculation", (_, _, ptp)) => ptp
1.23 - | ("failure", _) => raise ERROR "sys-raise ERROR"
1.24 + | ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic"
1.25 | _ => raise ERROR "me: uncovered case Step.by_tactic"
1.26 val _ = trace (pt', p') tac
1.27 val (_, ts, (pt'', p'')) =
1.28 - (*step's correct ctree is not tested in me, but in autocalc or Step.by_term*)
1.29 (case Step.do_next p' ((pt', Pos.e_pos'), []) of
1.30 ("ok", (ts as [(_, _, _)(*, _, _, ...*)], _, (pt'', p''))) => ("", ts, (pt'', p''))
1.31 | ("helpless", _) => ("helpless: cannot propose tac", [], Ctree.e_state)
1.32 - | ("dummy", (ts as (_, _, _) :: _, _, _)) => ("", ts, Ctree.e_state) (*intermed.from specify*)
1.33 + | ("dummy", (ts as (_, _, _) :: _, _, _)) => ("", ts, Ctree.e_state)
1.34 | ("end-of-calculation", (ts, _, _)) => ("", ts, Ctree.e_state)
1.35 - | _ => raise ERROR "me: uncovered case do_next")
1.36 + | ("failure", _) => raise ERROR "sys-raise ERROR by Step.do_next"
1.37 + | _ => raise ERROR "me: uncovered case Step.do_next")
1.38 val tac'' =
1.39 case ts of
1.40 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
1.41 @@ -167,4 +169,40 @@
1.42 Applicable.Yes m' => m'
1.43 | Applicable.No _ => raise ERROR ("tac2mstp': fails with" ^ Tactic.input_to_string m);
1.44
1.45 +
1.46 +(** me' for |> **)
1.47 +
1.48 +fun CalcTreeTEST' [(fmz, sp)] =
1.49 + let
1.50 + val ((pt, p), _) = Step_Specify.nxt_specify_init_calc (fmz, sp)
1.51 + in
1.52 + (Tactic.Model_Problem, (pt, p)) (* thus <Output> shows Tactic on top *)
1.53 + end
1.54 +| CalcTreeTEST' _ = raise ERROR "CalcTreeTEST': uncovered case"
1.55 +
1.56 +fun me' (tac, (pt, p)) = (* thus <Output> shows Tactic on top *)
1.57 + let
1.58 + val (pt', p') =
1.59 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
1.60 + case Step.by_tactic tac (pt, p) of
1.61 + ("ok", (_, _, ptp)) => ptp
1.62 + | ("unsafe-ok", (_, _, ptp)) => ptp
1.63 + | ("not-applicable",_) => (pt, p)
1.64 + | ("end-of-calculation", (_, _, ptp)) => ptp
1.65 + | ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic"
1.66 + | _ => raise ERROR "me: uncovered case Step.by_tactic"
1.67 + val tac' =
1.68 + (*step's correct ctree is not tested in me, but in autocalc or Step.by_term*)
1.69 + (case Step.do_next p' ((pt', Pos.e_pos'), []) of
1.70 + ("ok", ((tac', _, _) :: _, _, _)) => tac'
1.71 + | ("helpless", _) => Tactic.Empty_Tac
1.72 + | ("dummy", ((tac', _, _) :: _, _, _)) => tac'
1.73 + | ("end-of-calculation", _) => Tactic.End_Proof'
1.74 + | ("failure", _) => raise ERROR "sys-raise ERROR by Step.do_next"
1.75 + | _ => raise ERROR "me: uncovered case Step.do_next")
1.76 + in
1.77 + (tac', (pt', p')) (* thus <Output> shows Tactic on top *)
1.78 + (* ^^^^----- is the next step after "(pt', p')", but we prefer ----------------^^^^^^^^^^^^^ *)
1.79 + end
1.80 +
1.81 (**)end(**)
2.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Mon Jun 29 16:01:01 2020 +0200
2.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Mon Jun 29 17:27:34 2020 +0200
2.3 @@ -5,7 +5,7 @@
2.4 "table of contents ---------------------------------------------------------------------------";
2.5 "---------------------------------------------------------------------------------------------";
2.6 "----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. auto TODO investigate failure ------";
2.7 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me ---------------------------------";
2.8 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' --------------------------------";
2.9 "---------------------------------------------------------------------------------------------";
2.10 "---------------------------------------------------------------------------------------------";
2.11 "---------------------------------------------------------------------------------------------";
2.12 @@ -72,320 +72,57 @@
2.13 ( * NOTE: ^^^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^^^ *)
2.14
2.15
2.16 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
2.17 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
2.18 -"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me -----";
2.19 -"----- Bsp 7.70 with me";
2.20 -val fmz = ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
2.21 - "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]",
2.22 - "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]",
2.23 - "AbleitungBiegelinie dy"];
2.24 -val (dI',pI',mI') = ("Biegelinie", ["Biegelinien"],
2.25 - ["IntegrierenUndKonstanteBestimmen2"]);
2.26 -val p = e_pos'; val c = [];
2.27 -(*//----------------------------------vvv CalcTreeTEST ----------------------------------------\\*)
2.28 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; (*nxt = Model_Problem*)
2.29 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' --------------------------------";
2.30 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' --------------------------------";
2.31 +"----------- IntegrierenUndKonstanteBestimmen2: Bsp.7.70. me' --------------------------------";
2.32
2.33 -(*+*)val PblObj {probl, meth, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt (fst p);
2.34 -(*+*)writeln (O_Model.to_string oris); (*[
2.35 -(1, ["1"], #Given,Traegerlaenge, ["L"]),
2.36 -(2, ["1"], #Given,Streckenlast, ["q_0"]),
2.37 -(3, ["1"], #Find,Biegelinie, ["y"]),
2.38 -(4, ["1"], #Relate,Randbedingungen, ["[y 0 = 0]", "[y L = 0]", "[M_b 0 = 0]", "[M_b L = 0]"]),
2.39 -(5, ["1"], #undef,FunktionsVariable, ["x"]),
2.40 -(6, ["1"], #undef,GleichungsVariablen, ["[c]", "[c_2]", "[c_3]", "[c_4]"]),
2.41 -(7, ["1"], #undef,AbleitungBiegelinie, ["dy"])]*)
2.42 -(*+*)I_Model.to_string @{context} probl = "[]";
2.43 -(*+*)I_Model.to_string @{context} meth = "[]";
2.44 -(*\\----------------------------------^^^ CalcTreeTEST ----------------------------------------//*)
2.45 +val (tac as Model_Problem (*["Biegelinien"]*), (pt, p as ([], Pbl))) =
2.46 +CalcTreeTEST' [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y",
2.47 + "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x",
2.48 + "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"],
2.49 +("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))]
2.50
2.51 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Traegerlaenge L"*)
2.52 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "Streckenlast q_0"*)
2.53 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Biegelinie y"*)
2.54 -(*[], 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*)
2.55 -(*[], 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]"*)
2.56 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)
2.57 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["Biegelinien"]*)
2.58 -(*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Method ["IntegrierenUndKonstanteBestimmen2"]*)
2.59 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)
2.60 -(*----------- 10 -----------*)
2.61 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]"*)
2.62 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "AbleitungBiegelinie dy*)
2.63 -(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Apply_Method ["IntegrierenUndKonstanteBestimmen2"*)
2.64 + val (tac as Model_Problem (*["vonBelastungZu", "Biegelinien"]*), (pt, p as ([1], Pbl))) =
2.65 + (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
2.66 + (*INVISIBLE: SubProblem (''Biegelinie'', [''vonBelastungZu'', ''Biegelinien''])*)
2.67 + |> me'
2.68 + val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p as ([1, 2], Res))) =
2.69 + (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me';
2.70 + val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p as ([1, 3, 2], Res))) =
2.71 + (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me';
2.72
2.73 -(*//----------------------------------vvv Apply_Method ["IntegrierenUndKonstanteBestimmen2"----\\*)
2.74 -(*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Model_Problem*)
2.75 -(*AMBIGUITY in creating the environment from formal args. of partial_function "Biegelinie.Biegelinie2Script"
2.76 -and the actual args., ie. items of the guard of "["IntegrierenUndKonstanteBestimmen2"]" by "assoc_by_type":
2.77 -formal arg. "b" type-matches with several...actual args. "["dy", "y"]"
2.78 -selected "dy"
2.79 -with
2.80 -formals: ["l", "q", "v", "b", "s", "vs", "id_abl"]
2.81 -actuals: ["L", "q_0", "x", "[c, c_2, c_3, c_4]", "dy", "y", "[y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]"]*)
2.82 + val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p as ([1, 4], Res))) =
2.83 + (tac, (pt, p)) |> me' |> me';
2.84 + val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p as ([1, 5, 1], Res))) =
2.85 + (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me';
2.86
2.87 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
2.88 - val (pt''', p''') =
2.89 - (*Step.by_tactic is here for testing by me; Step.do_next would suffice in me*)
2.90 - case Step.by_tactic tac (pt,p) of
2.91 - ("ok", (_, _, ptp)) => ptp
2.92 -;
2.93 -(*+*)p = ([], Met);
2.94 -(*+*)p''' = ([1], Pbl);
2.95 -(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''' (fst p''');
2.96 -(*+*)(*MISSING after Step.by_tactic:*)
2.97 -(*+*)writeln (O_Model.to_string oris); (*[
2.98 -(1, ["1"], #Given,Streckenlast, ["q_0"]),
2.99 -(2, ["1"], #Given,FunktionsVariable, ["x"]),
2.100 -(3, ["1"], #Find,Funktionen, ["funs'''"])]
2.101 -MISSING:
2.102 - Biegelinie
2.103 - AbleitungBiegelinie
2.104 -*)
2.105 -"~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
2.106 -val Applicable.Yes m = (*case*) Step.check m (pt, p) (*of*);
2.107 -(*if*) member op = Solve.specsteps mI = false; (*else*)
2.108 + val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p as ([1, 7], Res))) =
2.109 + (tac, (pt, p)) |> me' |> me' |> me';
2.110 + val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p as ([1, 8, 2], Res))) =
2.111 + (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me';
2.112
2.113 -loc_solve_ (mI,m) ptp;
2.114 -"~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos)) = (m, ptp);
2.115 + val (tac as Subproblem ("Biegelinie", ["named", "integrate", "function"]), (pt, p as ([1, 8], Res))) =
2.116 + (tac, (pt, p)) |> me';
2.117 + val (tac as Check_Postcond ["named", "integrate", "function"], (pt, p as ([1, 9, 1], Res))) =
2.118 + (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me';
2.119
2.120 - Step_Solve.by_tactic m (pt, pos);
2.121 -"~~~~~ fun Step_Solve.by_tactic , args:"; val (m as Tactic.Apply_Method' (mI, _, _, ctxt)), (pt, (pos as (p, _))))
2.122 - = (m, (pt, pos));
2.123 -val {srls, ...} = Method.from_store mI;
2.124 - val itms = case get_obj I pt p of
2.125 - PblObj {meth=itms, ...} => itms
2.126 - | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case get_obj"
2.127 - val thy' = get_obj g_domID pt p;
2.128 - val thy = ThyC.get_theory thy';
2.129 - val srls = LItool.get_simplifier (pt, pos)
2.130 - val (is, env, ctxt, sc) = case LItool.init_pstate srls ctxt itms mI of
2.131 - (is as Istate.Pstate ist, ctxt, sc) => (is, get_env ist, ctxt, sc)
2.132 - | _ => error "Step_Solve.by_tactic Apply_Method: uncovered case init_pstate"
2.133 - val ini = LItool.implicit_take sc env;
2.134 - val p = lev_dn p;
2.135 -val NONE = (*case*) ini (*of*);
2.136 - val (m', (is', ctxt'), _) = LI.find_next_step sc (pt, (p, Res)) is ctxt;
2.137 - val d = Rule_Set.empty (*FIXME: get simplifier from domID*);
2.138 - val Safe_Step ((pt', p'), _, _, _) = (*case*) locate_input_tactic sc (pt,(p, Res)) is' ctxt' m' (*of*);
2.139 -Safe_Step : state * Istate.T * Proof.context * Tactic.T -> input_tactic_result;
2.140 + val (tac as Check_Postcond ["vonBelastungZu", "Biegelinien"], (pt, p as ([1, 9], Res))) =
2.141 + (tac, (pt, p)) |> me';
2.142
2.143 -(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt' (fst p');
2.144 -(*+*)(*MISSING after locate_input_tactic:*)
2.145 -(*+*)writeln (O_Model.to_string oris); (*[
2.146 -(1, ["1"], #Given,Streckenlast, ["q_0"]),
2.147 -(2, ["1"], #Given,FunktionsVariable, ["x"]),
2.148 -(3, ["1"], #Find,Funktionen, ["funs'''"])]
2.149 -MISSING:
2.150 - Biegelinie
2.151 - AbleitungBiegelinie
2.152 -*)
2.153 -"~~~~~ fun locate_input_tactic , args:"; val () = ();
2.154 + val (tac as Subproblem ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"]), (pt, p as ([1], Res))) =
2.155 + (tac, (pt, p)) |> me';
2.156
2.157 -(*+*)val c = [];
2.158 -(*\\----------------------------------^^^ Apply_Method ["IntegrierenUndKonstanteBestimmen2"----//*)
2.159 + (*INVISIBLE: SubProblem (''Biegelinie'', [''makeFunctionTo'', ''"equation''])*)
2.160 + val (tac as Model_Problem (*[''makeFunctionTo'', ''"equation'']*), (pt, p as ([2], Pbl))) =
2.161 + (tac, (pt, p)) |> me'
2.162
2.163 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Add_Given "Streckenlast q_0"*)
2.164 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Given "FunktionsVariable x"*)
2.165 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Add_Find "Funktionen funs'''"*)
2.166 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Theory "Biegelinie"*)
2.167 -(*[1], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = Specify_Problem ["vonBelastungZu", "Biegelinien"]*)
2.168 -(*[1], Pbl*)val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt; (*nxt = Specify_Method ["Biegelinien", "ausBelastung"]*)
2.169 -(*----------- 20 -----------*)
2.170 -(*//------------------------------------------------vvv Specify_Method ["Biegelinien", "ausBelastung"]-\\*)
2.171 -(*[1], Pbl*)(*ERROR val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt'''''; (*nxt = Apply_Method ["Biegelinien", "ausBelastung"]*)
2.172 -ERROR arguments_from_model: 'Biegelinie' not in itms*)
2.173 + (*INVISIBLE: SubProblem (''Biegelinie'', [''makeFunctionTo'', ''"equation''])*)
2.174 + val (tac as Model_Problem (*[''makeFunctionTo'', ''"equation'']*), (pt, p as ([2, 1], Pbl))) =
2.175 + (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me'
2.176 + (* ERROR for a long time -----vvvvvvvvvvvvvvvvvvvvvvvv.. (should be evaluated!) *)
2.177 + 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))) =
2.178 + (tac, (pt, p)) |> me' |> me' |> me' |> me' |> me' |> me' |> me' |> me';
2.179
2.180 -(*SubProblem (_, [''vonBelastungZu'', ''Biegelinien''], _)
2.181 - [REAL q, REAL v, REAL_REAL b, REAL_REAL id_abl]
2.182 - ^^^^^^^^^^^ ..ERROR arguments_from_model: 'Biegelinie' not in itms*)
2.183 -(*+*)val PblObj {meth, probl, spec = (thy, _ , metID), origin = (oris, _, _), ...} = get_obj I pt''''' (fst p''''');
2.184 -(*+*)if O_Model.to_string oris =
2.185 -(*+*) "[\n(1, [\"1\"], #Given,Streckenlast, [\"q_0\"]),\n(2, [\"1\"], #Given,FunktionsVariable, [\"x\"]),\n(3, [\"1\"], #Find,Funktionen, [\"funs'''\"])]"
2.186 -(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed oris";
2.187 -writeln (O_Model.to_string oris); (*[
2.188 -(1, ["1"], #Given,Streckenlast, ["q_0"]),
2.189 -(2, ["1"], #Given,FunktionsVariable, ["x"]),
2.190 -(3, ["1"], #Find,Funktionen, ["funs'''"])]*)
2.191 -(*+*)if I_Model.to_string @{context} probl = "[\n(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),\n(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),\n(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]"
2.192 -(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed probl";
2.193 -writeln (I_Model.to_string @{context} probl); (*[
2.194 -(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),
2.195 -(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),
2.196 -(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))]*)
2.197 -(*+*)if I_Model.to_string @{context} meth = "[]"
2.198 -(*+*)then () else error "([1], Pbl) Specify_Problem ['vonBelastungZu', 'Biegelinien'] changed meth";
2.199 -writeln (I_Model.to_string @{context} meth); (*[]*)
2.200 -
2.201 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt''''', p''''', c, pt''''');
2.202 -(* val (pt, p) = *)
2.203 - (*Step.by_tactic is here for testing by me; Step.do_next would suffice in me*)
2.204 - case Step.by_tactic tac (pt,p) of
2.205 - ("ok", (_, _, ptp)) => ptp
2.206 -;
2.207 -"~~~~~ fun Step.by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
2.208 -val Applicable.Yes m = (*case*) Step.check m (pt, p)(*of*);
2.209 -(*if*) member op = Solve.specsteps mI = true; (*then*)
2.210 -
2.211 -(*val Updated (_, _, (ctree, pos')) =*) loc_specify_ m ptp; (*creates meth-itms*)
2.212 -"~~~~~ fun loc_specify_ , args:"; val (m, (pt, pos)) = (m, ptp);
2.213 -(* val (p, _, f, _, _, pt) =*) Specification.specify m pos [] pt;
2.214 -
2.215 -"~~~~~ fun specify , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pos as (p, _)), _, pt) = (m, pos, [], pt);
2.216 - val (oris, dI', pI', mI', dI, pI, pbl, met, ctxt) = case get_obj I pt p of
2.217 - PblObj {origin= (oris, (dI', pI', mI'), _), spec= (dI, pI, _), probl = pbl, meth = met, ctxt, ...} =>
2.218 - (oris, dI', pI', mI', dI, pI, pbl, met, ctxt)
2.219 - val {ppc, pre, prls,...} = Method.from_store mID
2.220 - val thy = ThyC.get_theory dI
2.221 - val dI'' = if dI = ThyC.id_empty then dI' else dI
2.222 - val pI'' = if pI = Problem.id_empty then pI' else pI
2.223 -;
2.224 -(*+*)writeln (O_Model.to_string oris); (*[
2.225 -(1, ["1"], #Given,Streckenlast, ["q_0"]),
2.226 -(2, ["1"], #Given,FunktionsVariable, ["x"]),
2.227 -(3, ["1"], #Find,Funktionen, ["funs'''"])]*)
2.228 -(*+*)writeln (Model_Pattern.to_string' ppc);
2.229 -(*["(#Given, (Streckenlast, q__q))
2.230 -", "(#Given, (FunktionsVariable, v_v))
2.231 -", "(#Given, (Biegelinie, id_fun))
2.232 -", "(#Given, (AbleitungBiegelinie, id_abl))
2.233 -", "(#Find, (Funktionen, fun_s))"]*)
2.234 -(*+*)writeln (Model_Pattern.to_string' ((#ppc o Problem.from_store) pI));
2.235 -(*["(#Given, (Streckenlast, q_q))
2.236 -", "(#Given, (FunktionsVariable, v_v))
2.237 -", "(#Find, (Funktionen, funs'''))"]*)
2.238 - val oris = O_Model.add thy ppc oris
2.239 - val met = if met = [] then pbl else met
2.240 - val (_, (itms, pre')) = Specify.match_itms_oris thy met (ppc, pre, prls ) oris
2.241 -;
2.242 -(*+*)writeln (I_Model.to_string @{context} itms); (*[
2.243 -(1 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0])),
2.244 -(2 ,[1] ,true ,#Given ,Cor FunktionsVariable x ,(v_v, [x])),
2.245 -(3 ,[1] ,true ,#Find ,Cor Funktionen funs''' ,(funs''', [funs''']))] *)
2.246 -
2.247 -(*//----------- hack for funpack: generalise handling of meths which extend problem items -----\\*)
2.248 -val itms =
2.249 - if mI' = ["Biegelinien", "ausBelastung"]
2.250 - then itms @
2.251 - [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
2.252 - [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
2.253 - (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
2.254 - [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
2.255 - (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
2.256 - [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
2.257 - (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
2.258 - [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
2.259 - else itms
2.260 -(*\\----------- hack for funpack: generalise handling of meths which extend problem items -----//*)
2.261 -
2.262 -val itms' = itms @
2.263 - [(4, [1], true, "#Given", Cor ((@{term "Biegelinie"},
2.264 - [@{term "y::real \<Rightarrow> real"}]),
2.265 - (@{term "id_fun::real \<Rightarrow> real"},
2.266 - [@{term "y::real \<Rightarrow> real"}] ))),
2.267 - (5, [1], true, "#Given", Cor ((@{term "AbleitungBiegelinie"},
2.268 - [@{term "dy::real \<Rightarrow> real"}]),
2.269 - (@{term "id_abl::real \<Rightarrow> real"},
2.270 - [@{term "dy::real \<Rightarrow> real"}] )))]
2.271 -val itms'' = itms @
2.272 - [(4, [1], true, "#Given", Cor ((Const ("Biegelinie.Biegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
2.273 - [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
2.274 - (Free ("id_fun", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
2.275 - [Free ("y", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] ))),
2.276 - (5, [1], true, "#Given", Cor ((Const ("Biegelinie.AbleitungBiegelinie", Type ("fun", [Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]), Type ("Input_Descript.una", [])])),
2.277 - [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))]),
2.278 - (Free ("id_abl", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])])),
2.279 - [Free ("dy", Type ("fun", [Type ("Real.real", []), Type ("Real.real", [])]))] )))]
2.280 -;
2.281 -if itms' = itms'' then () else error "itms BUIT BY HAND ARE BROKEN";
2.282 -(*//-----------------------------------------^^^ Specify_Method ["Biegelinien", "ausBelastung"]-\\*)
2.283 -
2.284 -val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt''''';
2.285 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.286 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.287 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.288 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.289 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.290 -(*----------- 30 -----------*)
2.291 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.292 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.293 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.294 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.295 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.296 -(*----------- 40 -----------*)
2.297 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.298 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.299 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.300 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.301 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.302 -(*----------- 50 -----------*)
2.303 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.304 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.305 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.306 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.307 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.308 -(*----------- 60 -----------*)
2.309 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.310 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.311 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.312 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.313 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.314 -(*----------- 70 -----------*)
2.315 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.316 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.317 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.318 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.319 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.320 -(*----------- 80 -----------*)
2.321 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.322 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.323 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.324 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.325 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.326 -(*----------- 90 -----------*)
2.327 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.328 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.329 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.330 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.331 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.332 -(*---------- 100 -----------*)
2.333 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.334 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.335 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.336 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.337 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.338 -(*---------- 110 -----------*)
2.339 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.340 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.341 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.342 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.343 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.344 -(*---------- 120 -----------*)
2.345 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.346 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.347 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.348 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.349 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.350 -(*---------- 130 -----------*)
2.351 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.352 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.353 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.354 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.355 -val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.356 -
2.357 -if p = ([3], Pbl)
2.358 -then
2.359 - case nxt of
2.360 - ("Add_Given", Add_Given "solveForVars [c_2, c_3, c_4]") =>
2.361 - (case f of
2.362 - Test_Out.PpcKF
2.363 - (Problem [],
2.364 - {Find = [Incompl "solution []"], Given =
2.365 - [Correct
2.366 - "equalities\n [0 = -1 * c_4 / -1,\n 0 =\n (-24 * c_4 * EI + -24 * L * c_3 * EI + 12 * L ^^^ 2 * c_2 +\n 4 * L ^^^ 3 * c +\n -1 * L ^^^ 4 * q_0) /\n (-24 * EI),\n 0 = c_2, 0 = (2 * c_2 + 2 * L * c + -1 * L ^^^ 2 * q_0) / 2]",
2.367 - Incompl "solveForVars [c]"],
2.368 - Relate = [], Where = [], With = []}) => ()
2.369 - | _ => error "Bsp.7.70 me changed 1")
2.370 - | _ => error "Bsp.7.70 me changed 2"
2.371 -else error "Bsp.7.70 me changed 3";
2.372 -(* NOTE: ^^^^^^^^^^^^^^^^^ no progress already in isabisac15, but not noticed ^^^^^^^^^^^^^^^^^ *)
2.373 -
2.374 +if p = ([2, 1, 1], Frm) andalso (Calc.current_formula (pt, p) |> UnparseC.term) =
2.375 + "y x =\nc_4 + c_3 * x +\n1 / (-1 * EI) *\n(c_2 / 2 * x ^^^ 2 + c / 6 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
2.376 +then () else error "";
3.1 --- a/test/Tools/isac/Test_Isac.thy Mon Jun 29 16:01:01 2020 +0200
3.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Jun 29 17:27:34 2020 +0200
3.3 @@ -306,7 +306,7 @@
3.4 ML_file "Knowledge/biegelinie-1.sml"
3.5 ML_file "Knowledge/biegelinie-2.sml" (*Test_Isac_Short*)
3.6 ML_file "Knowledge/biegelinie-3.sml" (*Test_Isac_Short*)
3.7 -(*ML_file "Knowledge/biegelinie-4.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*)
3.8 + ML_file "Knowledge/biegelinie-4.sml"
3.9 ML_file "Knowledge/algein.sml"
3.10 ML_file "Knowledge/diophanteq.sml"
3.11 (*ML_file "Knowledge/inverse_z_transform.sml"hangs with ML_system_64 = "true"---Test_Isac_Short*)
4.1 --- a/test/Tools/isac/Test_Isac_Short.thy Mon Jun 29 16:01:01 2020 +0200
4.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Mon Jun 29 17:27:34 2020 +0200
4.3 @@ -307,7 +307,7 @@
4.4 ML_file "Knowledge/biegelinie-1.sml"
4.5 (*ML_file "Knowledge/biegelinie-2.sml" Test_Isac_Short*)
4.6 (*ML_file "Knowledge/biegelinie-3.sml" Test_Isac_Short*)
4.7 -(*ML_file "Knowledge/biegelinie-4.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*)
4.8 + ML_file "Knowledge/biegelinie-4.sml"
4.9 ML_file "Knowledge/algein.sml"
4.10 ML_file "Knowledge/diophanteq.sml"
4.11 (*ML_file "Knowledge/inverse_z_transform.sml"hangs with ML_system_64 = "true"---Test_Isac_Short*)