1.1 --- a/src/Tools/isac/MathEngine/step.sml Wed May 27 16:20:06 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngine/step.sml Thu May 28 12:52:25 2020 +0200
1.3 @@ -82,26 +82,6 @@
1.4
1.5 (* does a step forward; returns tactic used, ctree updated (i.e. with NEW term/calchead) *)
1.6 fun do_next (ip as (_, p_)) (ptp as (pt, p), tacis) =
1.7 -(*OLD*)let
1.8 -(*OLD*) val pIopt = Ctree.get_pblID (pt, ip);
1.9 -(*OLD*)in
1.10 -(*OLD*) if ip = ([], Pos.Res) then
1.11 -(*OLD*) ("end-of-calculation", (tacis, [], ptp): Calc.state_post)
1.12 -(*OLD*) else
1.13 -(*OLD*) case tacis of
1.14 -(*OLD*) (_ :: _) =>
1.15 -(*OLD*) if ip = p (*the request is done where ptp waits for*)
1.16 -(*OLD*) then
1.17 -(*OLD*) let
1.18 -(*OLD*) val (pt', c', p') = Solve_Step.s_add_general tacis (pt, [], p)
1.19 -(*OLD*) in ("ok", (tacis, c', (pt', p'))) end
1.20 -(*OLD*) else
1.21 -(*OLD*) switch_specify_solve p_ (pt, ip)
1.22 -(*OLD*) | _ => case pIopt of
1.23 -(*OLD*) NONE => ("no-fmz-spec", ([], [], ptp))
1.24 -(*OLD*) | SOME _ => switch_specify_solve p_ (pt, ip)
1.25 -(*OLD*)end;
1.26 -(*---* )
1.27 (*NEW*)if Pos.on_calc_end ip then
1.28 (*NEW*) ("end-of-calculation", (tacis, [], ptp): Calc.state_post)
1.29 (*NEW*)else
1.30 @@ -124,7 +104,7 @@
1.31 (*NEW*) ("no-fmz-spec", ([], [], ptp))
1.32 (*NEW*) else switch_specify_solve p_ (pt, ip)
1.33 (*NEW*) end
1.34 -( *NEW*)
1.35 +(*NEW*)
1.36
1.37 (** locate an input tactic **)
1.38
2.1 --- a/src/Tools/isac/Specify/i-model.sml Wed May 27 16:20:06 2020 +0200
2.2 +++ b/src/Tools/isac/Specify/i-model.sml Thu May 28 12:52:25 2020 +0200
2.3 @@ -306,27 +306,30 @@
2.4 end
2.5 (* for Method: #undef completed vvvvv vvvvvv term_as_string *)
2.6 (*OLD*)| check_single ctxt m_field o_model i_model m_patt str =
2.7 -(*NEW* ) | check_single ctxt _(*m_field*) o_model i_model m_patt str =
2.8 +(*/NEW* ) | check_single ctxt _(*m_field*) o_model i_model m_patt str =
2.9 ( *NEW*)
2.10 case TermC.parseNEW ctxt str of
2.11 NONE => Err ("ERROR I_Model.check_single: syntax error in \"" ^ str ^ "\"")
2.12 -(*OLD*)| SOME t =>
2.13 -(*NEW* )| SOME (t as (descriptor $ _)) =>
2.14 +(*OLD* )| SOME t =>
2.15 +( *NEW*)| SOME (t as (descriptor $ _)) =>
2.16 (*NEW*) (case Model_Pattern.get_field descriptor m_patt of
2.17 (*NEW*) NONE => Err ("ERROR I_Model.check_single: unknown descriptor \"" ^
2.18 - UnparseC.term_in_ctxt ctxt descriptor ^ "\"")
2.19 -(*NEW*) | SOME m_field => (*redes: re-introduce m_patt as argument of check_single*)
2.20 -( *NEW*)
2.21 +(*NEW*) UnparseC.term_in_ctxt ctxt descriptor ^ "\"")
2.22 +(*NEW*) | SOME m_field' =>
2.23 +(*NEW*) if m_field <> m_field' then
2.24 +(*NEW*) Err ("ERROR I_Model.check_single: \"" ^ UnparseC.term_in_ctxt ctxt t ^ "\"" ^
2.25 +(*NEW*) "\" not for field \"" ^ m_field ^ "\"")
2.26 +(*NEW*) else
2.27 case O_Model.is_known ctxt m_field o_model t of
2.28 ("", ori', all) =>
2.29 (case is_notyet_input ctxt i_model all ori' m_patt of
2.30 ("", itm) => Add itm
2.31 | (msg, _) => Err ("ERROR I_Model.check_single: is_notyet_input: " ^ msg))
2.32 | (msg, _, _) => Err ("ERROR I_Model.check_single: is_known: " ^ msg)
2.33 -(*NEW* ))
2.34 +(*NEW*))
2.35 (*NEW*)| SOME t => Err ("ERROR I_Model.check_single: impossible for input \"" ^
2.36 (*NEW*) UnparseC.term_in_ctxt ctxt t ^ "\"");
2.37 -( *NEW*)
2.38 +(*NEW*)
2.39
2.40 (** add input **)
2.41
3.1 --- a/src/Tools/isac/Specify/specify.sml Wed May 27 16:20:06 2020 +0200
3.2 +++ b/src/Tools/isac/Specify/specify.sml Thu May 28 12:52:25 2020 +0200
3.3 @@ -117,19 +117,19 @@
3.4 (*TODO: unify*)
3.5 fun find_next_step (pt, (p, p_)) =
3.6 let
3.7 -(*OLD*)val (pblobj, met, origin, oris, dI', pI', mI', pbl, dI, pI, mI) =
3.8 +(*OLD* )val (pblobj, met, origin, oris, dI', pI', mI', pbl, dI, pI, mI) =
3.9 (*OLD*) case Ctree.get_obj I pt p of
3.10 (*OLD*) pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
3.11 (*OLD*) probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)
3.12 (*OLD*) | Ctree.PrfObj _ => raise ERROR "nxt_specify_: not on PrfObj"
3.13 (*OLD*)in
3.14 (*OLD*) if Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin then
3.15 -(*OLD* )
3.16 +( *OLD*)
3.17 (*NEW*)val pblobj as {meth = met, origin = origin as (oris, (dI', pI', mI'), _), probl = pbl,
3.18 (*NEW*) spec = (dI, pI, mI), ctxt, ...} = Calc.specify_data (pt, (p, p_));
3.19 (*NEW*)in
3.20 (*NEW*) if Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin then
3.21 -( *NEW*)
3.22 +(*NEW*)
3.23 case mI' of
3.24 ["no_met"] => ("ok", (Pos.Pbl, Tactic.Refine_Tacitly pI'))
3.25 | _ => ("ok", (Pos.Pbl, Tactic.Model_Problem))
4.1 --- a/src/Tools/isac/Specify/step-specify.sml Wed May 27 16:20:06 2020 +0200
4.2 +++ b/src/Tools/isac/Specify/step-specify.sml Thu May 28 12:52:25 2020 +0200
4.3 @@ -249,7 +249,7 @@
4.4 (*OLD*) Specify_Step.add (Tactic.Specify_Method' (mID, oris, itms)) (Istate_Def.Uistate, ctxt) (pt, pos)
4.5 (*---* )
4.6 (*NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,
4.7 -(*NEW*) ...} = Calc.specify_data (pt, pos);
4.8 +(*NEW*) ...} =Calc.specify_data (pt, pos);
4.9 (*NEW*) val (dI, _, mID) = References.select o_refs refs;
4.10 (*NEW*) val {ppc = m_patt, pre, prls, ...} = Method.from_store mID
4.11 (*NEW*) val {origin = (root_model, _, _), ...} = Calc.specify_data (pt, ([], Und))
5.1 --- a/test/Tools/isac/Interpret/step-solve.sml Wed May 27 16:20:06 2020 +0200
5.2 +++ b/test/Tools/isac/Interpret/step-solve.sml Thu May 28 12:52:25 2020 +0200
5.3 @@ -56,6 +56,7 @@
5.4 "AbleitungBiegelinie dy"];
5.5 val spec = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]);
5.6 (*[], Pbl*)val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, spec)];(*\<rightarrow>Model_Problem*)
5.7 +(*---------- HERE IS MISSING LINE ... \<rightarrow>Add_Given "Traegerlaenge L" !!!!! *)
5.8 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Given "Streckenlast q_0"*)
5.9 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Find "Biegelinie y"*)
5.10 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]", ERROR MISSING step: M_b 0 = 0*)
5.11 @@ -101,5 +102,5 @@
5.12 | _ =>
5.13 (case nxt of
5.14 Specify_Theory "Biegelinie" => ()
5.15 - | _ => error "CHANGED 1")
5.16 -else error "CHANGED 2"
5.17 + | _ => error "final test CHANGED 1")
5.18 +else error "final test CHANGED 2"
6.1 --- a/test/Tools/isac/Test_Some.thy Wed May 27 16:20:06 2020 +0200
6.2 +++ b/test/Tools/isac/Test_Some.thy Thu May 28 12:52:25 2020 +0200
6.3 @@ -56,7 +56,7 @@
6.4 ML \<open>
6.5 "~~~~~ fun xxx , args:"; val () = ();
6.6 "~~~~~ and xxx , args:"; val () = ();
6.7 -"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
6.8 +"~~~~~ fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
6.9 (*if*) (*then*); (*else*); (*case*) (*of*); (*return from xxx*);
6.10 "xx"
6.11 ^ "xxx" (*+*) (*!for return!*) (*isa*) (*REP*) (**)
6.12 @@ -92,8 +92,20 @@
6.13 section \<open>===================================================================================\<close>
6.14 ML \<open>
6.15 \<close> ML \<open>
6.16 -fun on_calc_end ([], Res) = true
6.17 - | on_calc_end _ = false;
6.18 +\<close> ML \<open>
6.19 +\<close> ML \<open>
6.20 +\<close>
6.21 +
6.22 +section \<open>===================================================================================\<close>
6.23 +ML \<open>
6.24 +\<close> ML \<open>
6.25 +\<close> ML \<open>
6.26 +\<close> ML \<open>
6.27 +\<close>
6.28 +
6.29 +section \<open>===================================================================================\<close>
6.30 +ML \<open>
6.31 +\<close> ML \<open>
6.32 \<close> ML \<open>
6.33 \<close> ML \<open>
6.34 \<close>
6.35 @@ -173,7 +185,7 @@
6.36 (*+*)val (_, ["Biegelinien"], _) = spec;
6.37 (*\------------------- initial check for whole me ------------------------------------------/*)
6.38 \<close> ML \<open>
6.39 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
6.40 +"~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
6.41 \<close> ML \<open>
6.42 (*/------------------- begin step into Step.by_tactic --------------------------------------\*)
6.43 val (pt'''''_', p'''''_') =
6.44 @@ -196,28 +208,30 @@
6.45 (*+*)then () else error "o_model AFTER Specify_Method NOTok CHANGED";
6.46 \<close> ML \<open>
6.47 \<close> ML \<open>
6.48 -(*\------------------- initial check forStep.by_tactic -------------------------------------/*)
6.49 +(*\------------------- initial check for Step.by_tactic ------------------------------------/*)
6.50 (*\------------------- step into Step.by_tactic --------------------------------------------/*)
6.51 +
6.52 +\<close> ML \<open>
6.53 (*/------------------- step into Step.do_next ----------------------------------------------\*)
6.54 (**)val ("dummy", ([(Add_Given "FunktionsVariable x", _, _)], _, _)) = (**)
6.55 (*case*)
6.56 Step.do_next p'''''_' ((pt'''''_', Pos.e_pos'), []) (*of*);
6.57 \<close> ML \<open>
6.58 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
6.59 +"~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
6.60 (p'''''_', ((pt'''''_', Pos.e_pos'), []));
6.61 \<close> ML \<open>
6.62 -(*NEW*)(*if*) Pos.on_calc_end ip (*else*);
6.63 +(*.NEW*)(*if*) Pos.on_calc_end ip (*else*);
6.64 \<close> ML \<open>
6.65 -(*NEW*) val (_, probl_id, _) = Calc.references (pt, p);
6.66 +(*.NEW*) val (_, probl_id, _) = Calc.references (pt, p);
6.67 \<close> ML \<open>
6.68 (*-"-*) val _ = (*case*) tacis (*of*);
6.69 \<close> ML \<open>
6.70 -(*NEW*) (*if*) probl_id = Problem.id_empty (*else*);
6.71 +(*.NEW*) (*if*) probl_id = Problem.id_empty (*else*);
6.72 \<close> ML \<open>
6.73 (**)val ("dummy", ([(Add_Given "FunktionsVariable x", _, _)], _, _)) = (**)
6.74 -(*NEW*) switch_specify_solve p_ (pt, ip)
6.75 +(*.NEW*) switch_specify_solve p_ (pt, ip)
6.76 \<close> ML \<open>
6.77 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
6.78 +"~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
6.79 \<close> ML \<open>
6.80 (*if*) Pos.on_specification ([], state_pos) (*then*);
6.81 \<close> ML \<open>
6.82 @@ -247,7 +261,7 @@
6.83 "(7 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]"
6.84 (*\------------------- check for entry to specify_do_next ----------------------------------/*)
6.85 \<close> ML \<open>
6.86 -"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
6.87 +"~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
6.88 \<close> ML \<open>
6.89 \<close> ML \<open>
6.90 (**)val (_, (p_', Add_Given "FunktionsVariable x")) =(**)
6.91 @@ -255,10 +269,10 @@
6.92 \<close> ML \<open>
6.93 "~~~~~ fun find_next_step , args:"; val (pt, (p, p_)) = (ptp);
6.94 \<close> ML \<open>
6.95 -(*NEW*)val pblobj as {meth = met, origin = origin as (oris, (dI', pI', mI'), _),
6.96 -(*NEW*) probl = pbl, spec = (dI, pI, mI), ctxt, ...} = Calc.specify_data (pt, (p, p_));
6.97 +(*.NEW*)val pblobj as {meth = met, origin = origin as (oris, (dI', pI', mI'), _),
6.98 +(*.NEW*) probl = pbl, spec = (dI, pI, mI), ctxt, ...} = Calc.specify_data (pt, (p, p_));
6.99 \<close> ML \<open>
6.100 -(*NEW*)(*if*) Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin (*else*);
6.101 +(*.NEW*)(*if*) Ctree.just_created (pt, (p, p_)) andalso origin <> Ctree.e_origin (*else*);
6.102 \<close> ML \<open>
6.103 val cpI = if pI = Problem.id_empty then pI' else pI;
6.104 val cmI = if mI = Method.id_empty then mI' else mI;
6.105 @@ -285,7 +299,7 @@
6.106 (*case*) item_to_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
6.107 \<close> ML \<open>
6.108 (*redes: here we have all m_field ------------------vvvv *)
6.109 -"~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms) =
6.110 +"~~~~~ ~ fun item_to_add , args:"; val (thy, oris, _, itms) =
6.111 ((ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
6.112 \<close> ML \<open>
6.113 (*OLD*)fun testr_vt v ori = Library.member op= (#2 (ori : O_Model.single)) v (**)andalso (#3 ori) <> "#undef"(**)
6.114 @@ -338,13 +352,13 @@
6.115
6.116 SOME
6.117 (I_Model.geti_ct thy ori (hd icl)) (*return from item_to_add*);
6.118 -"~~~~~ fun geti_ct , args:"; val (thy, (_, _, _, d, ts), (_, _, _, fd, itm_)) = (thy, ori, (hd icl));
6.119 +"~~~~~ ~~ fun geti_ct , args:"; val (thy, (_, _, _, d, ts), (_, _, _, fd, itm_)) = (thy, ori, (hd icl));
6.120 \<close> ML \<open>
6.121 val rrrrr =
6.122 (fd, ((UnparseC.term_in_thy thy) o Input_Descript.join)
6.123 (d, subtract op = (ts_in itm_) ts)) (*return from geti_ct*);
6.124 \<close> ML \<open>
6.125 -"~~~~~ from fun geti_ct \<longrightarrow>fun item_to_add \<longrightarrow>fun find_next_step , return:"; val (SOME (fd, ct')) =
6.126 +"~~~~~ ~~ from fun geti_ct \<longrightarrow>fun item_to_add \<longrightarrow>fun find_next_step , return:"; val (SOME (fd, ct')) =
6.127 (SOME rrrrr);
6.128 \<close> ML \<open>
6.129 ("dummy", (Pos.Met, P_Model.mk_additem fd ct')) (*return from find_next_step*);
6.130 @@ -368,11 +382,11 @@
6.131 (*//ERROR by_tactic_input' Met: uncovered case of#undef*)
6.132 Specify.by_tactic_input' "#Given" ct ptp (*return from by_tactic_input*);
6.133 \<close> ML \<open>
6.134 -"~~~~~ fun by_tactic_input' , args:"; val (sel, ct, (ptp as (pt, (p, Pos.Met)))) = ("#Given", ct, ptp);
6.135 +"~~~~~ ~ fun by_tactic_input' , args:"; val (sel, ct, (ptp as (pt, (p, Pos.Met)))) = ("#Given", ct, ptp);
6.136 \<close> ML \<open>
6.137 -(*+*)ct = "FunktionsVariable x"
6.138 +(*+*)ct = "FunktionsVariable x";
6.139 \<close> ML \<open>
6.140 -(*NEW*)val sel = "#undef"; (* m_field may change from root- to sub-Model_Pattern *)
6.141 +(*///NEW* )val sel = "#undef"; (**) m_field may change from root- to sub-Model_Pattern *)
6.142 val (oris, dI', mI', dI, mI, met, ctxt) = case Ctree.get_obj I pt p of
6.143 Ctree.PblObj {origin = (oris, (dI', _, mI'), _), spec = (dI, _, mI), meth = met,ctxt, ...} =>
6.144 (oris, dI', mI', dI, mI, met, ctxt)
6.145 @@ -380,49 +394,18 @@
6.146 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI;
6.147 val cmI = if mI = Method.id_empty then mI' else mI;
6.148 \<close> ML \<open>
6.149 -(*/------------------- build new fun for Model_Pattern -------------------------------------\*)
6.150 -val descriptor = @{term "FunktionsVariable"}
6.151 -\<close> ML \<open>
6.152 -fun get_field descriptor m_patt =
6.153 - (filter ((curry (fn (desc, (_, (desc', _))) => desc = desc')) descriptor) m_patt
6.154 - |> the_single
6.155 - |> (fn (a, _) => SOME a))
6.156 - handle List.Empty => NONE
6.157 -(*\------------------- build new fun for Model_Pattern ------------------------------------/*)
6.158 -(*/------------------- build new fun for I_Model -------------------------------------\*)
6.159 -\<close> ML \<open>
6.160 -fun check_single ctxt _ o_model i_model m_patt str =
6.161 - case TermC.parseNEW ctxt str of
6.162 - NONE => Err ("ERROR I_Model.check_single: syntax error in \"" ^ str ^ "\"")
6.163 - | SOME (t as (descriptor $ _)) =>
6.164 -(*NEW*) (case get_field descriptor m_patt of
6.165 -(*NEW*) NONE => Err ("ERROR I_Model.check_single: unknown descriptor \"" ^
6.166 - UnparseC.term_in_ctxt ctxt descriptor ^ "\"")
6.167 -(*NEW*) | SOME m_field =>
6.168 -(*NEW*)
6.169 - case O_Model.is_known ctxt m_field o_model t of
6.170 - ("", ori', all) =>
6.171 - (case is_notyet_input ctxt i_model all ori' m_patt of
6.172 - ("", itm) => Add itm
6.173 - | (msg, _) => Err ("ERROR I_Model.check_single: is_notyet_input: " ^ msg))
6.174 - | (msg, _, _) => Err ("ERROR I_Model.check_single: is_known: " ^ msg))
6.175 -(*NEW*)| SOME t => Err ("ERROR I_Model.check_single: impossible for input \"" ^
6.176 -(*NEW*) UnparseC.term_in_ctxt ctxt t ^ "\"");
6.177 -(*\------------------- build new fun for I_Model ------------------------------------/*)
6.178 -\<close> ML \<open>
6.179 -(*--- should be -------"#Given"-vvv *)
6.180 -val Add (5, [1], true, "#undef", Cor ((Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]), (Free ("v", _), [Free ("x", _)]))) =
6.181 +val Add (5, [1], true, "#Given", Cor ((Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]), (Free ("v", _), [Free ("x", _)]))) =
6.182 (*case*)
6.183 I_Model.check_single ctxt sel oris met ((#ppc o Method.from_store) cmI) ct (*of*);
6.184 \<close> ML \<open>
6.185 -"~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
6.186 +"~~~~~ ~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
6.187 (ctxt, sel, oris, met, ((#ppc o Method.from_store) cmI), ct);
6.188 \<close> ML \<open>
6.189 (*OLD* )| SOME t =>
6.190 -( *NEW*) val SOME (t as (descriptor $ _)) = (*case*) TermC.parseNEW ctxt str (*of*);
6.191 +( *.NEW*) val SOME (t as (descriptor $ _)) = (*case*) TermC.parseNEW ctxt str (*of*);
6.192 \<close> ML \<open>
6.193 -(*NEW*) val SOME m_field = (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
6.194 -(*NEW*)
6.195 +(*.NEW*) val SOME m_field = (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
6.196 +(*.NEW*)
6.197 \<close> ML \<open>
6.198 (*+*)O_Model.to_string o_model = "[\n" ^
6.199 "(1, [\"1\"], #Given, Traegerlaenge, [\"L\"]), \n" ^
6.200 @@ -434,11 +417,11 @@
6.201 "(7, [\"1\"], #undef, AbleitungBiegelinie, [\"dy\"])]"
6.202 \<close> ML \<open>
6.203 (**)
6.204 -(*("[x] not for #Given", (0, [], "", Const ("empty", "??.'a"), [Const ("empty", "??.'a")]), [])*)
6.205 +val ("", (5, [1], "#Given", Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]), [Free ("x", _)]) =
6.206 (*case*)
6.207 O_Model.is_known ctxt m_field o_model t (*of*);
6.208 \<close> ML \<open>
6.209 -"~~~~~ fun is_known , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
6.210 +"~~~~~ ~~~ fun is_known , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
6.211 \<close> ML \<open>
6.212 val ots = (LibraryC.distinct o flat o (map #5)) ori
6.213 val oids = ((map (fst o dest_Free)) o LibraryC.distinct o flat o (map TermC.vars)) ots
6.214 @@ -453,7 +436,7 @@
6.215 \<close> ML \<open>
6.216 seek_oridts ctxt sel (d, ts) ori
6.217 \<close> ML \<open>
6.218 -"~~~~~ fun seek_oridts , args:"; val (ctxt, m_field, (descript, vals), ((id, vat, m_field', descript', vals') :: oris)) =
6.219 +"~~~~~ ~~~~ fun seek_oridts , args:"; val (ctxt, m_field, (descript, vals), ((id, vat, m_field', descript', vals') :: oris)) =
6.220 (ctxt, sel, (d, ts), ori);
6.221 \<close> ML \<open>
6.222 (*+*)val Add_Given "FunktionsVariable x" = tac
6.223 @@ -475,7 +458,8 @@
6.224 \<close> ML \<open>
6.225 (*+*)val (id, vat, m_field', descript', vals') = nth 5 ori
6.226 \<close> ML \<open>
6.227 -(*+*)m_field' = "#undef"; (*MUST BE *)
6.228 +(*+*)val (5, [1], "#Given", Const ("Biegelinie.FunktionsVariable", _), [Free ("x", _)]) =
6.229 + (id, vat, m_field', descript', vals')
6.230 \<close> ML \<open>
6.231 \<close> ML \<open>
6.232 (*-------------------- stop step into whole me ----------------------------------------------*)
6.233 @@ -518,11 +502,11 @@
6.234 (*+*)val Specify_Method ["Biegelinien", "ausBelastung"] = nxt;
6.235 (*+*)(* by ^^^^^^^^^^^^ "id_fun" and "id_abl" must be requested: PUT THEM INTO O_Model*)
6.236
6.237 -"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
6.238 +"~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
6.239
6.240 val ("ok", ([], [], (_, _))) = (*case*)
6.241 Step.by_tactic tac (pt, p) (*of*);
6.242 -"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
6.243 +"~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
6.244 val Applicable.Yes tac' = (*case*) check tac (pt, p) (*of*);
6.245 (*if*) Tactic.for_specify' tac' (*then*);
6.246
6.247 @@ -544,7 +528,7 @@
6.248 then () else error "[Biegelinien, ausBelastung] O_Model NOT EXTENDED BY Method";
6.249 (*\------------------- initial check for Step_Specify.by_tactic ----------------------------/*)
6.250 \<close> ML \<open>
6.251 -"~~~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt, pos as (p, _))) =
6.252 +"~~~ fun by_tactic , args:"; val ((Tactic.Specify_Method' (mID, _, _)), (pt, pos as (p, _))) =
6.253 (tac', ptp);
6.254 (*NEW*) val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = i_meth, ctxt,
6.255 (*NEW*) ...} =Calc.specify_data (pt, pos);
6.256 @@ -589,19 +573,9 @@
6.257 (*\------------------- check for entry to O_Model.complete_for -----------------------------/*)
6.258 \<close> ML \<open>
6.259 O_Model.complete_for_from m_patt o_model (root_model, ctxt);
6.260 -"~~~~~ fun complete_for_from , args:"; val (m_patt, root_model, (o_model, ctxt)) =
6.261 +"~~~~ fun complete_for_from , args:"; val (m_patt, root_model, (o_model, ctxt)) =
6.262 (m_patt, root_model, (o_model, ctxt));
6.263 \<close> ML \<open>
6.264 -(*/------------------- build new fun complete_for_from -------------------------------------\*)
6.265 -(*/----- values for building -------------\* )
6.266 -val d1 $ v1 = @{term "errorBound eee_val"};
6.267 -val d2 $ v2 = @{term "boundVariable bbb"};
6.268 -val root_model = root_model @ [(11, [1], "#undef", d1, [v1]), (22, [1], "#undef", d2, [v2])];
6.269 -
6.270 -val d $ v = @{term "errorBound eee_var"};
6.271 -val m_patt = m_patt @ [("#Relate", (d, v))];
6.272 -( *\----- values for building -------------/*)
6.273 -\<close> ML \<open>
6.274 val missing = m_patt |> filter_out
6.275 (fn (_, (descriptor, _)) => (Library.member op = (map #4 o_model) descriptor))
6.276 \<close> ML \<open>
6.277 @@ -616,8 +590,7 @@
6.278 |> add_id
6.279 |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)),
6.280 ctxt |> ContextC.add_constraints (add |> O_Model.values |> TermC.vars')) (*return from complete_for_from*);
6.281 -(*\------------------- build new fun complete_for_from -------------------------------------/*)
6.282 -"~~~~~ from fun complete_for_from \<longrightarrow>Step_Specify.by_tactic , return:"; val (o_model', ctxt') =
6.283 +"~~~~ from fun complete_for_from \<longrightarrow>Step_Specify.by_tactic , return:"; val (o_model', ctxt') =
6.284 ((o_model @ add)
6.285 |> map (fn (_, b, c, d, e) => (b, c, d, e))
6.286 |> add_id
6.287 @@ -652,7 +625,7 @@
6.288 (*+*)pos = ([1], Met);
6.289
6.290 ("ok", ([], [], (pt, pos))) (*return from Step_Specify.by_tactic*);
6.291 -"~~~~~ from Step_Specify.by_tactic \<longrightarrow>Step.by_tactic \<longrightarrow>fun me , return:"; val ("ok", (_, _, (pt, p))) =
6.292 +"~~~ from Step_Specify.by_tactic \<longrightarrow>Step.by_tactic \<longrightarrow>fun me , return:"; val ("ok", (_, _, (pt, p))) =
6.293 ("ok", ([], [], (pt, pos)));
6.294 (* val ("helpless", ([(xxxxx, _, _)], _, _)) = (*case*)*)
6.295 (* SHOULD BE ^^^^^^^^^^^^^^^^^^^^^^^^^^^ Add_Given "Biegelinie y" | Add_Given "AbleitungBiegelinie dy"*)
6.296 @@ -661,7 +634,7 @@
6.297 (*("helpless", ([], [], ..*)
6.298 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
6.299 \<close> ML \<open>
6.300 -"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
6.301 +"~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
6.302 (*NEW*)(*if*) on_calc_end ip (*else*);
6.303 (*NEW*) val (_, probl_id, _) = Calc.references (pt, p);
6.304 (*-"-*) val _ = (*case*) tacis (*of*);
6.305 @@ -672,12 +645,12 @@
6.306 (*NEW*)val ("dummy", ([(Add_Given "Biegelinie y", _, _)], _, _)) =
6.307 (*NEW*) switch_specify_solve p_ (pt, ip);
6.308 \<close> ML \<open>
6.309 -"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
6.310 +"~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
6.311 (*if*) Pos.on_specification ([], state_pos) (*then*);
6.312
6.313 val ("dummy", ([(Add_Given "Biegelinie y", _, _)], _, _)) =
6.314 specify_do_next (pt, input_pos);
6.315 -"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
6.316 +"~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
6.317
6.318 val (_, (p_', tac)) =
6.319 Specify.find_next_step ptp;
6.320 @@ -737,7 +710,7 @@
6.321 "(4 ,[1] ,false ,#Given ,Mis Biegelinie id_fun), \n" ^
6.322 "(5 ,[1] ,false ,#Given ,Mis AbleitungBiegelinie id_abl)]";
6.323
6.324 -"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) = (tac, (pt, (p, p_')));
6.325 +"~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) = (tac, (pt, (p, p_')));
6.326
6.327 \<close> ML \<open>
6.328 Specify.by_tactic_input' "#Given" ct ptp;
6.329 @@ -772,7 +745,7 @@
6.330 (*\------------------- check for entry to check_single -------------------------------------/*)
6.331 \<close> ML \<open>
6.332
6.333 -"~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
6.334 +"~~~~~ ~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, str) =
6.335 (ctxt, sel, oris, met, ((#ppc o Method.from_store) cmI), ct);
6.336 val SOME t = (*case*) TermC.parseNEW ctxt str (*of*);
6.337
6.338 @@ -781,7 +754,7 @@
6.339 (*("seek_oridts: input ('Biegelinie y') not found in oris (typed)", (0, [], "#Given", Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), [Free ("y", "real \<Rightarrow> real")]), [])*)
6.340 (*case*)
6.341 is_known ctxt m_field o_model t (*of*);
6.342 -"~~~~~ fun is_known , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
6.343 +"~~~~~ ~~ fun is_known , args:"; val (ctxt, sel, ori, t) = (ctxt, m_field, o_model, t);
6.344 val ots = (LibraryC.distinct o flat o (map #5)) ori
6.345 val oids = ((map (fst o dest_Free)) o LibraryC.distinct o flat o (map TermC.vars)) ots
6.346 val (d, ts) = Input_Descript.split t
6.347 @@ -791,7 +764,7 @@
6.348 (*if*) not (subset op = (map typeless ts, map typeless ots)) (*else*);
6.349
6.350 (*case*) O_Model.seek_orits ctxt sel ts ori (*of*);
6.351 -"~~~~~ fun seek_orits , args:"; val (ctxt, sel, ts, ((id, vat, sel', d, ts') :: oris)) = (ctxt, sel, ts, ori);
6.352 +"~~~~~ ~~~ fun seek_orits , args:"; val (ctxt, sel, ts, ((id, vat, sel', d, ts') :: oris)) = (ctxt, sel, ts, ori);
6.353
6.354 (*+/---------------- bypass recursion of seek_orits ----------------\*)
6.355 (*+*)O_Model.to_string oris = "[\n" ^