1.1 --- a/TODO.md Tue Oct 03 16:33:54 2023 +0200
1.2 +++ b/TODO.md Wed Oct 25 12:34:12 2023 +0200
1.3 @@ -52,6 +52,14 @@
1.4
1.5 ***** priority of WN items is top down, most urgent/simple on top
1.6
1.7 +* WN: (*/---with M_Model.match_itms_oris broken elementwise input to lists---\*)
1.8 + (*\---with M_Model.match_itms_oris broken elementwise input to lists---/*)
1.9 + several tests marked in Test_Isac.thy, which have out-comments.
1.10 + repair them together with all <broken elementwise input to lists>
1.11 +* WN: review PblObh {meth, ...}
1.12 + * fill early (Model_Problem?) with Inc [] presents input-templates
1.13 + * try to minimise user's contact with Method:
1.14 + * M_Model.match_itms_oris can probably be replaced by i_Model.s_make_complete and Pre_Conds.check(?_*)
1.15 * WN: uncomment: I_Model.check_internal (*filter (fn (_, _, _, m_field ,_) ..*)
1.16 after I_Model.s_make_complete does NOT create m_field #undef, "i_model_empty";
1.17 see test/../i-model.sml --- setup test data for I_Model.s_make_complete ---
2.1 --- a/src/Tools/isac/Build_Isac.thy Tue Oct 03 16:33:54 2023 +0200
2.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Oct 25 12:34:12 2023 +0200
2.3 @@ -183,6 +183,7 @@
2.4 \<close>
2.5 (** ) (* evaluated in Test_Isac/_Short *)
2.6 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/000-comments.sml"
2.7 +(*ML_file "Minisubpbl/100-init-rootpbl-NEXT_STEP.sml"*)
2.8 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/100-init-rootpbl.sml"
2.9 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml"
2.10 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150-add-given-Equation.sml"
2.11 @@ -274,5 +275,11 @@
2.12 \<close> ML \<open>
2.13
2.14 \<close> ML \<open>
2.15 +I_Model.TEST_to_OLD
2.16 +\<close> ML \<open>
2.17 +I_Model.OLD_to_TEST
2.18 \<close>
2.19 +(*OLD*)
2.20 +(*---*)
2.21 +(*NEW*)
2.22 end
3.1 --- a/src/Tools/isac/Interpret/li-tool.sml Tue Oct 03 16:33:54 2023 +0200
3.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Oct 25 12:34:12 2023 +0200
3.3 @@ -303,6 +303,13 @@
3.4 | [a] => (f, a)
3.5 | aas as (a :: _) => (writeln (msg_ambiguous ctxt prog met_id f aas formals actuals); (f, a));
3.6
3.7 +(*
3.8 + The sequence of \<open>formals\<close> and \<open>actuals\<close> must be the same:
3.9 + the sequence of \<open>formals\<close> is given by the program,
3.10 + the sequence of \<open>actuals\<close> is given by the by theMethodC#model
3.11 +
3.12 + In case of equal sequence the \<open>fun relate\<close> could be simpler ...
3.13 +*)
3.14 fun relate_args _ (f::_) [] ctxt prog met_id formals actuals =
3.15 raise ERROR (msg_miss ctxt prog met_id "relate_args" f formals actuals)
3.16 | relate_args env [] _ _ _ _ _ _ = env (*may drop Find?*)
3.17 @@ -321,14 +328,11 @@
3.18 let
3.19 val (model_patt, program, prog, prog_rls, where_, where_rls) =
3.20 case MethodC.from_store ctxt met_id of
3.21 - {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...}=>
3.22 + {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...} =>
3.23 (model_patt, program, prog, prog_rls, where_, where_rls)
3.24 | _ => raise ERROR ("init_pstate with " ^ MethodC.id_to_string met_id)
3.25 -(*OLD* )
3.26 - val (_, env_model, (env_subst, env_eval)) = I_Model.of_max_variant model_patt i_model;
3.27 -( *---*)
3.28 val (env_model, (env_subst, env_eval)) = Pre_Conds.make_environments model_patt i_model;
3.29 -(*NEW*)
3.30 +
3.31 val actuals = map snd env_model
3.32 val formals = Program.formal_args prog
3.33 val preconds = Pre_Conds.check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval))
4.1 --- a/src/Tools/isac/MathEngBasic/model-def.sml Tue Oct 03 16:33:54 2023 +0200
4.2 +++ b/src/Tools/isac/MathEngBasic/model-def.sml Wed Oct 25 12:34:12 2023 +0200
4.3 @@ -47,6 +47,7 @@
4.4 val i_model_empty : i_model_single
4.5 val i_model_empty_TEST: i_model_single_TEST
4.6
4.7 + val member_vnt: variants -> variant -> bool
4.8 val max_variants: o_model -> i_model_TEST -> variants
4.9 val max_variant_TEST: i_model_TEST -> variant
4.10
4.11 @@ -135,10 +136,13 @@
4.12
4.13 (** max_variants **)
4.14
4.15 +fun member_vnt [] _ = true
4.16 + | member_vnt vnts vnt = member op= vnts vnt
4.17 +
4.18 fun all_variants model =
4.19 - map (fn (_, variants, _, _, _) => variants) model
4.20 - |> flat
4.21 - |> distinct op =
4.22 + map (fn (_, variants, _, _, _) => variants) model
4.23 + |> flat
4.24 + |> distinct op =
4.25 fun filter_variants' i_singles n =
4.26 filter (fn (_, variants, _, _, _) => member op= variants n) i_singles
4.27 fun cnt_corrects i_model =
5.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Tue Oct 03 16:33:54 2023 +0200
5.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Wed Oct 25 12:34:12 2023 +0200
5.3 @@ -10,8 +10,8 @@
5.4 val autocalc : Pos.pos' list -> Pos.pos' -> Calc.T * State_Steps.T ->
5.5 Solve.auto -> string * Pos.pos' list * Calc.T
5.6
5.7 - val initcontext_met : Ctree.ctree -> Pos.pos' -> bool * string list * Program.T * I_Model.T * Pre_Conds.T
5.8 - val initcontext_pbl : Ctree.ctree -> Pos.pos' -> bool * string list * term * I_Model.T * Pre_Conds.T
5.9 + val initcontext_met : Ctree.ctree -> Pos.pos' -> bool * string list * Program.T * I_Model.T_TEST * Pre_Conds.T
5.10 + val initcontext_pbl : Ctree.ctree -> Pos.pos' -> bool * string list * term * I_Model.T_TEST * Pre_Conds.T
5.11 val set_method : MethodC.id -> Calc.T -> Ctree.ctree * SpecificationC.T
5.12 val set_problem : Problem.id -> Calc.T -> Ctree.ctree * SpecificationC.T
5.13 val set_theory : ThyC.id -> Calc.T -> Ctree.ctree * SpecificationC.T
5.14 @@ -33,14 +33,14 @@
5.15 val (mits, pt, p) =
5.16 case Step_Specify.by_tactic_input (Tactic.Specify_Method mI) ptp of
5.17 (_, ([(_, Tactic.Specify_Method' (_, _, mits), _)], [], (pt, (p, _)))) => (mits, pt, p)
5.18 - | _ => raise ERROR "set_method: case 1 uncovered"
5.19 - val where_ = [] (*...from Specify_Method'*)
5.20 + | _ => raise ERROR "Math_Engine.set_method: case 1 uncovered"
5.21 + val where_ = [] (*...from Specify_Method'*)
5.22 val complete = true (*...from Specify_Method'*)
5.23 (*from Specify_Method' ? vvv, vvv ?*)
5.24 val (hdf, spec) =
5.25 case Ctree.get_obj I pt p of
5.26 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
5.27 - | Ctree.PrfObj _ => raise ERROR "set_method: case 2 uncovered"
5.28 + | Ctree.PrfObj _ => raise ERROR "Math_Engine.set_method: case 2 uncovered"
5.29 in
5.30 (pt, (complete, Pos.Met, hdf, mits, where_, spec) : SpecificationC.T)
5.31 end
5.32 @@ -129,43 +129,44 @@
5.33 if no pbl has been specified, take the init from origin.*)
5.34 fun initcontext_pbl pt (p, _) =
5.35 let
5.36 - val (probl, os, pI, hdl, pI', ctxt) =
5.37 + val (probl, meth, os, pI, hdl, pI', ctxt) =
5.38 case Ctree.get_obj I pt p of
5.39 - Ctree.PblObj {probl, origin = (os, (_, pI, _), hdl), spec = (_, pI', _), ctxt, ...}
5.40 - => (probl, os, pI, hdl, pI', ctxt)
5.41 + Ctree.PblObj {probl, meth, origin = (os, (_, pI, _), hdl), spec = (_, pI', _), ctxt, ...}
5.42 + => (probl, meth, os, pI, hdl, pI', ctxt)
5.43 | Ctree.PrfObj _ => raise ERROR "initcontext_pbl: uncovered case"
5.44 val pblID =
5.45 if pI' = Problem.id_empty
5.46 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
5.47 else pI'
5.48 val {model, where_, where_rls, ...} = Problem.from_store ctxt pblID
5.49 - val (model_ok, (pbl, where_)) = M_Match.match_itms_oris ctxt
5.50 - probl (model, where_, where_rls) os
5.51 + val (model_ok, (pbl, where_)) = M_Match.match_itms_oris ctxt os
5.52 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (model, where_, where_rls)
5.53 in
5.54 (model_ok, pblID, hdl, pbl, where_)
5.55 end
5.56
5.57 fun initcontext_met pt (p,_) =
5.58 let
5.59 - val (meth, os, mI, mI', ctxt) =
5.60 + val (probl, meth, os, mI, mI', ctxt) =
5.61 case Ctree.get_obj I pt p of
5.62 - Ctree.PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ctxt, ...} =>
5.63 - (meth, os, mI, mI', ctxt)
5.64 + Ctree.PblObj {probl, meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ctxt, ...} =>
5.65 + (probl, meth, os, mI, mI', ctxt)
5.66 | Ctree.PrfObj _ => raise ERROR "initcontext_met: uncovered case"
5.67 val metID = if mI' = MethodC.id_empty
5.68 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
5.69 else mI'
5.70 val {model, where_, where_rls, program, ...} = MethodC.from_store ctxt metID
5.71 - val (model_ok, (pbl, where_)) = M_Match.match_itms_oris ctxt meth (model,where_,where_rls) os
5.72 + val (model_ok, (pbl, where_)) = M_Match.match_itms_oris ctxt os
5.73 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (model, where_, where_rls)
5.74 in
5.75 (model_ok, metID, program, pbl, where_)
5.76 end
5.77
5.78 fun tryrefine pI pt (p,_) =
5.79 let
5.80 - val (probl, os, ospec, hdl, spec) =
5.81 + val (probl, meth, os, ospec, hdl, spec) =
5.82 case Ctree.get_obj I pt p of
5.83 - Ctree.PblObj {probl, origin = (os, ospec, hdl), spec, ...} => (probl, os, ospec, hdl, spec)
5.84 + Ctree.PblObj {probl, meth, origin = (os, ospec, hdl), spec, ...} => (probl, meth, os, ospec, hdl, spec)
5.85 | Ctree.PrfObj _ => raise ERROR "context_met: uncovered case"
5.86 val ctxt = spec
5.87 |> References.select_input ospec
5.88 @@ -173,14 +174,14 @@
5.89 |> Know_Store.get_via_last_thy
5.90 |> Proof_Context.init_global
5.91 in
5.92 - case Refine.problem (Know_Store.get_via_last_thy "Isac_Knowledge") pI probl of
5.93 + case Refine.problem (Know_Store.get_via_last_thy "Isac_Knowledge") pI (probl) of
5.94 NONE => (*copy from context_pbl*)
5.95 let
5.96 val {model, where_, where_rls, ...} = Problem.from_store ctxt pI
5.97 - val (_, (pbl, where_)) = M_Match.match_itms_oris ctxt probl
5.98 - (model, where_, where_rls) os
5.99 + val (_, (pbl, where_)) = M_Match.match_itms_oris ctxt os
5.100 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (model, where_, where_rls)
5.101 in
5.102 - (false, pI, hdl, pbl, where_)
5.103 + (false, pI, hdl, I_Model.TEST_to_OLD pbl, where_)
5.104 end
5.105 | SOME (pI, (pbl, where_)) => (true, pI, hdl, pbl, where_)
5.106 end
6.1 --- a/src/Tools/isac/Specify/i-model.sml Tue Oct 03 16:33:54 2023 +0200
6.2 +++ b/src/Tools/isac/Specify/i-model.sml Wed Oct 25 12:34:12 2023 +0200
6.3 @@ -57,6 +57,8 @@
6.4 val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string
6.5
6.6 val add: single -> T -> T
6.7 + val add_other: variant -> T_TEST -> single_TEST -> single_TEST
6.8 + val fill_method: O_Model.T -> T_TEST * T_TEST-> Model_Pattern.T -> T_TEST
6.9 val s_make_complete: Proof.context -> O_Model.T -> T_TEST * T_TEST -> Problem.id * MethodC.id ->
6.10 T_TEST * T_TEST
6.11 val s_are_complete: Proof.context -> O_Model.T -> T_TEST * T_TEST -> Problem.id * MethodC.id -> bool
6.12 @@ -441,6 +443,34 @@
6.13 handles superfluous items carelessly *)
6.14 fun add itm itms = if member eq_dsc itms itm then itms else itms @ [itm] (* @ new itm *)
6.15
6.16 +(*
6.17 + in case there is an item in i2_model(= met) with Sup_TEST,
6.18 + find_first an appropriate (variant, descriptor) item in i1_model(= pbl) and add it instead Sup_TEST,
6.19 + otherwise keep the items of i2_model.
6.20 +*)
6.21 +fun add_other max_vnt i1_model (i2, _, bool2, m_field2, (Sup_TEST (descr2, ts2), pos2)) =
6.22 + (case find_first (fn (_, vnts1, _, _, (feedb1, _)) => case Pre_Conds.get_dscr' feedb1 of
6.23 + NONE => false
6.24 + | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model of
6.25 + NONE =>
6.26 + (i2, [max_vnt], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2)) (*the present in i2_model*)
6.27 + | SOME i1_single => i1_single) (*shift the item from i1_model to i2_model*)
6.28 + | add_other _ _ i2_single = i2_single (*keep all the other items in i2_model*)
6.29 +
6.30 +fun fill_method o_model (pbl_imod, met_imod) met_patt =
6.31 + let
6.32 + val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod
6.33 + (*probably pbl/met_imod = [], so take met_patt; if empty return Sup*)
6.34 + val i_from_met = map (fn (_, (descr, _)) => (*order from met_patt*)
6.35 + Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt (*\<longrightarrow> right order for args*)
6.36 +
6.37 + val met_max_vnts = Model_Def.max_variants o_model i_from_met;
6.38 + val max_vnt = hd (inter op= pbl_max_vnts met_max_vnts);
6.39 + (*add items from pbl_imod (without overwriting existing items in met_imod)*)
6.40 + in
6.41 + map (add_other max_vnt pbl_imod) i_from_met
6.42 + end
6.43 +
6.44 fun msg vnts feedb = "get_descr_vnt' returns NONE: i.e. it does not find an item of o_model with\n" ^
6.45 "variants " ^ ints2str' vnts ^ " and descriptor " ^
6.46 (feedb |> Pre_Conds.get_dscr' |> the |> UnparseC.term (ContextC.for_ERROR ()))
7.1 --- a/src/Tools/isac/Specify/m-match.sml Tue Oct 03 16:33:54 2023 +0200
7.2 +++ b/src/Tools/isac/Specify/m-match.sml Wed Oct 25 12:34:12 2023 +0200
7.3 @@ -1,4 +1,4 @@
7.4 -(* Title: Specify/model.sml
7.5 +(* Title: Specify/m-match.sml
7.6 Author: Walther Neuper 110226
7.7 (c) due to copyright terms
7.8
7.9 @@ -22,8 +22,14 @@
7.10 bool * (I_Model.T * Pre_Conds.T) (*^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v--- type*)
7.11 (*val o_i_model: O_Model.T * I_Model.T -> Model_Pattern.T * term list * Rule_Set.T -> theory ->
7.12 bool * (I_Model.T * Pre_Conds.T) (*?values--^^^^^^^^^?*)*)
7.13 +(*OLD* )
7.14 val match_itms_oris: theory -> I_Model.T -> Model_Pattern.T * term list * Rule_Set.T ->
7.15 O_Model.T -> bool * (I_Model.T * Pre_Conds.T)
7.16 +( *---*)
7.17 + val match_itms_oris: Proof.context -> O_Model.T -> I_Model.T_TEST * I_Model.T_TEST ->
7.18 + Model_Pattern.T * Pre_Conds.unchecked * Rule_Def.rule_set ->
7.19 + bool * (I_Model.T_TEST * Pre_Conds.T)
7.20 +(*NEW*)
7.21
7.22 (*val arguments: theory -> Model_Pattern.T -> term list -> O_Model.T*)
7.23 val arguments: theory -> Model_Pattern.T -> term list -> O_Model.T
7.24 @@ -108,34 +114,18 @@
7.25
7.26 (** check a problem (ie. itm list) for matching a problemtype **)
7.27
7.28 -(* check a problem (or method) pbl (ie. itm list) for matching a problemtype pbt,
7.29 - for missing items get data from formalization (ie. ori list);
7.30 - takes the I_Model.variables for concluding completeness (could be another!)
7.31 -
7.32 - (0) determine the most frequent variant mv in pbl
7.33 - ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
7.34 - (2) filter (dsc(pbt) = dsc(oris)) oris; -> news;
7.35 - (3) newitms = filter (mv mem vat(news)) news
7.36 - (4) pbt @ newitms *)
7.37 -fun match_itms_oris ctxt pbl (pbt, where_, where_rls) oris =
7.38 - let
7.39 - (*0*)val mv = Pre_Conds.max_variant pbl;
7.40 -
7.41 - fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;
7.42 - fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
7.43 - SOME _ => false | NONE => true;
7.44 - (*1*)val mis = (filter (notmem pbl)) pbt;
7.45 -
7.46 - fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
7.47 - fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
7.48 - (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
7.49 - val news = (flat o (map (oris2itms oris))) mis;
7.50 - (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
7.51 - val newitms = filter mem_vat news;
7.52 - (*4*)val itms' = pbl @ newitms;
7.53 - val (pb, where_') = Pre_Conds.check ctxt where_rls where_
7.54 - (pbt, I_Model.OLD_to_TEST itms');
7.55 - in (length mis = 0 andalso pb, (itms', where_')) end;
7.56 +(*
7.57 + check a problem (or method) pbl (ie. itm list) for matching a problemtype pbt,
7.58 + for missing items get data from formalization (ie. ori list);
7.59 + takes the I_Model.variables for concluding completeness (could be another!)
7.60 +*)
7.61 +fun match_itms_oris ctxt o_model (pbl_imod, met_imod) (met_patt, where_, where_rls) =
7.62 + let
7.63 + val met_imod = I_Model.fill_method o_model (pbl_imod, met_imod) met_patt
7.64 + val (check, preconds) = Pre_Conds.check ctxt where_rls where_ (met_patt, met_imod)
7.65 + in
7.66 + (check, (met_imod, preconds))
7.67 + end
7.68
7.69
7.70 (** for use by math-authors **)
8.1 --- a/src/Tools/isac/Specify/o-model.sml Tue Oct 03 16:33:54 2023 +0200
8.2 +++ b/src/Tools/isac/Specify/o-model.sml Wed Oct 25 12:34:12 2023 +0200
8.3 @@ -221,8 +221,8 @@
8.4 case Model_Pattern.get_field descr m_patt of
8.5 SOME m_field => (a, b, m_field, descr, e)
8.6 | NONE => (a, b, "#undef", descr, e))
8.7 - |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
8.8 - |> add_enumerate (* for correct enumeration *)
8.9 + |> map (fn (_, b, c, d, e) => (b, c, d, e)) (* for correct enumeration *)
8.10 + |> add_enumerate (* for correct enumeration *)
8.11 |> map (fn (a, (b, c, d, e)) => (a, b, c, d, e)), (* for correct enumeration *)
8.12 ctxt |> ContextC.add_constraints (add |> values |> TermC.vars'))
8.13 end
9.1 --- a/src/Tools/isac/Specify/p-model.sml Tue Oct 03 16:33:54 2023 +0200
9.2 +++ b/src/Tools/isac/Specify/p-model.sml Wed Oct 25 12:34:12 2023 +0200
9.3 @@ -97,7 +97,8 @@
9.4 | "#Where" => {Given = gi, Where = wh @ [x], Find = fi, With = wi, Relate = re}
9.5 | "#Find" => {Given = gi, Where = wh, Find = fi @ [x], With = wi, Relate = re}
9.6 | "#Relate"=> {Given = gi, Where = wh, Find = fi, With = wi, Relate = re @ [x]}
9.7 - | "#undef" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)
9.8 + | "#undef" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)
9.9 + | "i_model_empty" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)
9.10 | _ => raise ERROR ("add_sel_ppc tried to select by \"" ^ sel ^ "\"")
9.11 fun add_where {Given = gi, Where = _, Find = fi, With = wi, Relate = re} wh =
9.12 {Given = gi, Where = wh, Find= fi , With = wi, Relate = re}
10.1 --- a/src/Tools/isac/Specify/pre-conditions.sml Tue Oct 03 16:33:54 2023 +0200
10.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml Wed Oct 25 12:34:12 2023 +0200
10.3 @@ -154,15 +154,18 @@
10.4 (* get_equal_descr: I_Model.T_TEST -> Model_Pattern.single -> (Model_Pattern.single * I_Model.single_TEST) list*)
10.5 fun get_equal_descr i_model (m_patt_single as (_, (descr, _))) =
10.6 let
10.7 - val equal_variants =
10.8 + val equal_descr =
10.9 filter (fn i_single => case get_descr i_single of
10.10 NONE => false (*--------vvvvv*)
10.11 - | SOME descr' => descr' = descr) (*probl_POS*) i_model
10.12 + | SOME descr' => descr' = descr) i_model
10.13 in
10.14 - (map (pair m_patt_single) equal_variants)
10.15 + (map (pair m_patt_single) equal_descr)
10.16 end
10.17
10.18 -(*get an appropriate (description, variant) item from pbl_imod, otherwise return empty item*)
10.19 +(*
10.20 + get an appropriate (description, variant)-item from i_model, otherwise return empty item,
10.21 + i.e. this function produces items with Sup.
10.22 +*)
10.23 fun get_descr_vnt descr vnts i_model =
10.24 let
10.25 val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false
11.1 --- a/src/Tools/isac/Specify/refine.sml Tue Oct 03 16:33:54 2023 +0200
11.2 +++ b/src/Tools/isac/Specify/refine.sml Wed Oct 25 12:34:12 2023 +0200
11.3 @@ -128,6 +128,8 @@
11.4
11.5 (* check a problem (ie. itm list) for matching a problemtype,
11.6 takes the Pre_Conds.max_variant for concluding completeness (could be another!) *)
11.7 +(* match_itms: theory -> I_Model.T -> Model_Pattern.T * unchecked * Rule_Def.rule_set ->
11.8 + bool * (I_Model.T * (bool * term) list)*)
11.9 fun match_itms thy itms (pbt, where_, where_rls) =
11.10 let
11.11 fun okv mvat (_, vats, b, _, _) = member op = vats mvat andalso b;
12.1 --- a/src/Tools/isac/Specify/specify-step.sml Tue Oct 03 16:33:54 2023 +0200
12.2 +++ b/src/Tools/isac/Specify/specify-step.sml Wed Oct 25 12:34:12 2023 +0200
12.3 @@ -9,8 +9,11 @@
12.4 sig
12.5 val check: Tactic.input -> Calc.T -> Applicable.T
12.6 val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Test_Out.T
12.7 -
12.8 +(*OLD* )
12.9 val complete_for: MethodC.id -> Calc.T -> O_Model.T * Proof.context * I_Model.T
12.10 +( *---*)
12.11 + val complete_for: MethodC.id -> Calc.T -> O_Model.T * Proof.context * I_Model.T_TEST
12.12 +(*NEW*)
12.13 end
12.14
12.15 (**)
12.16 @@ -20,6 +23,7 @@
12.17
12.18 fun complete_for mID (ctree, pos) =
12.19 let
12.20 +(*OLD* )
12.21 val {origin = (o_model, _, _), probl = i_prob, ctxt,
12.22 ...} = Calc.specify_data (ctree, pos);
12.23 val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
12.24 @@ -29,6 +33,20 @@
12.25 in
12.26 (o_model', ctxt', i_model)
12.27 end
12.28 +( *---*)
12.29 + val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = met_imod, ctxt,
12.30 + ...} = Calc.specify_data (ctree, pos);
12.31 + val ctxt = Ctree.get_ctxt ctree pos
12.32 + val (dI, _, _) = References.select_input o_refs refs;
12.33 + val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
12.34 + val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
12.35 + val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
12.36 + val (_, (i_model, _)) = M_Match.match_itms_oris ctxt o_model' (I_Model.OLD_to_TEST i_prob,
12.37 + I_Model.OLD_to_TEST i_prob) (m_patt, where_, where_rls);
12.38 + in
12.39 + (o_model', ctxt', i_model)
12.40 + end
12.41 +(*NEW*)
12.42
12.43 (*
12.44 check tactics (input by the user, mostly) for applicability
12.45 @@ -83,20 +101,27 @@
12.46 let
12.47 val (o_model, _, i_model) = complete_for mID (ctree, pos)
12.48 in
12.49 - Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model))
12.50 + Applicable.Yes (Tactic.Specify_Method' (mID, o_model, I_Model.TEST_to_OLD i_model))
12.51 end
12.52 | check (Tactic.Specify_Problem pID) (pt, pos as (p, _)) =
12.53 let
12.54 - val (oris, pI, pI', itms, ctxt) = case Ctree.get_obj I pt p of
12.55 - Ctree.PblObj {origin = (oris, (_, pI, _), _), spec = (_, pI', _), probl = itms, ctxt, ...}
12.56 - => (oris, pI, pI', itms, ctxt)
12.57 + val (oris, pI, pI', probl, meth, ctxt) = case Ctree.get_obj I pt p of
12.58 + Ctree.PblObj {origin = (oris, (_, pI, _), _), spec = (_, pI', _), probl, meth, ctxt, ...}
12.59 + => (oris, pI, pI', probl, meth, ctxt)
12.60 | _ => raise ERROR "Specify_Step.check Specify_Problem: uncovered case Ctree.get_obj"
12.61 val {model, where_, where_rls, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pID;
12.62 +(*OLD* )
12.63 val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty
12.64 then (false, (I_Model.init model, []))
12.65 else M_Match.match_itms_oris ctxt itms (model, where_, where_rls) oris;
12.66 +( *---*)
12.67 + val (check, (i_model, preconds)) = if pI' = Problem.id_empty andalso pI = Problem.id_empty
12.68 + then (false, (I_Model.OLD_to_TEST (I_Model.init model), []))
12.69 + else M_Match.match_itms_oris ctxt oris
12.70 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (model, where_, where_rls)
12.71 +(*NEW*)
12.72 in
12.73 - Applicable.Yes (Tactic.Specify_Problem' (pID, pbl))
12.74 + Applicable.Yes (Tactic.Specify_Problem' (pID, (check, (I_Model.TEST_to_OLD i_model, preconds))))
12.75 end
12.76 | check (Tactic.Specify_Theory dI)_ = Applicable.Yes (Tactic.Specify_Theory' dI)
12.77 | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
13.1 --- a/src/Tools/isac/Specify/specify.sml Tue Oct 03 16:33:54 2023 +0200
13.2 +++ b/src/Tools/isac/Specify/specify.sml Wed Oct 25 12:34:12 2023 +0200
13.3 @@ -1,3 +1,6 @@
13.4 +(* Title: Specify/specify.sml
13.5 + Author: Walther Neuper
13.6 +*)
13.7 signature SPECIFY =
13.8 sig
13.9 val find_next_step: Calc.T -> string * (Pos.pos_ * Tactic.input)
14.1 --- a/src/Tools/isac/Specify/step-specify.sml Tue Oct 03 16:33:54 2023 +0200
14.2 +++ b/src/Tools/isac/Specify/step-specify.sml Wed Oct 25 12:34:12 2023 +0200
14.3 @@ -84,31 +84,31 @@
14.4 end
14.5 | by_tactic_input (Tactic.Specify_Problem pI) (pt, pos as (p, _)) =
14.6 let
14.7 - val (oris, pI', probl, ctxt) = case get_obj I pt p of
14.8 - PblObj {origin = (oris, _, _), spec = (_ ,pI',_), probl, ctxt, ...} =>
14.9 - (oris, pI', probl, ctxt)
14.10 + val (oris, pI', probl, meth, ctxt) = case get_obj I pt p of
14.11 + PblObj {origin = (oris, _, _), spec = (_ ,pI',_), probl, meth, ctxt, ...} =>
14.12 + (oris, pI', probl, meth, ctxt)
14.13 | _ => raise ERROR ""
14.14 val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
14.15 - val pbl =
14.16 + val (check, (i_model, preconds)) =
14.17 if pI' = Problem.id_empty andalso pI = Problem.id_empty
14.18 - then (false, (I_Model.init model, []))
14.19 - else M_Match.match_itms_oris ctxt probl (model, where_, where_rls) oris
14.20 - (*FIXXXME~~~~~~~~~~~~~~~: take pbl and compare with new pI WN.8.03*)
14.21 + then (false, (I_Model.OLD_to_TEST (I_Model.init model), []))
14.22 + else M_Match.match_itms_oris ctxt oris
14.23 + (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (model, where_, where_rls)
14.24 val (c, pt) =
14.25 - case Specify_Step.add (Tactic.Specify_Problem' (pI, pbl)) (Istate_Def.Uistate, ctxt) (pt, pos) of
14.26 + case Specify_Step.add (Tactic.Specify_Problem' (pI, (check, (I_Model.TEST_to_OLD i_model, preconds)))) (Istate_Def.Uistate, ctxt) (pt, pos) of
14.27 ((_, Pbl), c, _, pt) => (c, pt)
14.28 | _ => raise ERROR ""
14.29 in
14.30 - ("ok", ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, pbl),
14.31 + ("ok", ([(Tactic.Specify_Problem pI, Tactic.Specify_Problem' (pI, (check, (I_Model.TEST_to_OLD i_model, preconds))),
14.32 (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt, pos)))
14.33 end
14.34 | by_tactic_input (Tactic.Specify_Method id) (pt, pos) =
14.35 let
14.36 val (o_model, ctxt, i_model) = Specify_Step.complete_for id (pt, pos)
14.37 - val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, i_model))
14.38 + val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, I_Model.TEST_to_OLD i_model))
14.39 (Istate_Def.Uistate, ctxt) (pt, pos)
14.40 in
14.41 - ("ok", ([(Tactic.Specify_Method id, Tactic.Specify_Method' (id, o_model, i_model),
14.42 + ("ok", ([(Tactic.Specify_Method id, Tactic.Specify_Method' (id, o_model, I_Model.TEST_to_OLD i_model),
14.43 (pos, (Istate_Def.Uistate, ContextC.empty)))], [], (pt, pos)))
14.44 end
14.45 | by_tactic_input (Tactic.Specify_Theory dI) (pt, pos as (_, Pbl)) =
14.46 @@ -184,7 +184,7 @@
14.47 | by_tactic (Tactic.Specify_Method' (id, _, _)) (pt, pos) =
14.48 let
14.49 val (o_model, ctxt, i_model) = Specify_Step.complete_for id (pt, pos)
14.50 - val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, i_model))
14.51 + val (pos, _, _, pt) = Specify_Step.add (Tactic.Specify_Method' (id, o_model, I_Model.TEST_to_OLD i_model))
14.52 (Istate_Def.Uistate, ctxt) (pt, pos)
14.53 in
14.54 ("ok", ([], [], (pt, pos)))
15.1 --- a/test/Tools/isac/Interpret/li-tool.sml Tue Oct 03 16:33:54 2023 +0200
15.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Wed Oct 25 12:34:12 2023 +0200
15.3 @@ -295,6 +295,15 @@
15.4 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "AbleitungBiegelinie y'" = nxt
15.5 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Biegemoment M_b" = nxt
15.6 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Querkraft Q" = nxt
15.7 +
15.8 +(*/---with M_Model.match_itms_oris broken elementwise input to lists---\*)
15.9 +(*NEW match_itms_oris*)
15.10 +(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c]" = nxt
15.11 +(*NEW*)(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c_2, c_3, c_4]" = nxt
15.12 +(*NEW*)(*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
15.13 +(*\---with M_Model.match_itms_oris broken elementwise input to lists---/*)
15.14 +
15.15 +(*--------------------- @ {context}----------------------------------------------
15.16 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "GleichungsVariablen [c, c_2, c_3, c_4]" = nxt
15.17
15.18 (*[], Met*)val return_me_Add_Given_GleichungsVariablen
15.19 @@ -453,3 +462,5 @@
15.20 (* final test ... ----------------------------------------------------------------------------*)
15.21 (*+*)val ([], Met) = p
15.22 (*+*)val Apply_Method ["IntegrierenUndKonstanteBestimmen2"] = nxt
15.23 + --------------------- @ {context}----------------------------------------------*)
15.24 +
16.1 --- a/test/Tools/isac/MathEngine/step.sml Tue Oct 03 16:33:54 2023 +0200
16.2 +++ b/test/Tools/isac/MathEngine/step.sml Wed Oct 25 12:34:12 2023 +0200
16.3 @@ -329,7 +329,7 @@
16.4 = Step.specify_do_next ptp;
16.5
16.6 (*** stepwise Specification: MethodC model ================================================ ***)
16.7 -val ("ok", ([(Add_Given "boundVariable a", _, _)], _, ptp))
16.8 +val ("ok", ([(Add_Given "boundVariable b", _, _)], _, ptp))
16.9 = Step.specify_do_next ptp;
16.10 val ("ok", ([(Add_Given "interval {x. 0 \<le> x \<and> x \<le> 2 * r}", _, _)], _, ptp))
16.11 = Step.specify_do_next ptp;
16.12 @@ -337,15 +337,10 @@
16.13 = Step.specify_do_next ptp;
16.14
16.15 val PblObj {meth, ...} = get_obj I (fst ptp) [];
16.16 -if I_Model.to_string @{context} meth = "[\n" ^
16.17 - "(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] , pen2str), \n" ^
16.18 - "(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A , pen2str), \n" ^
16.19 - "(3 ,[1, 2, 3] ,true ,#Find ,Cor valuesFor [a, b] , pen2str), \n" ^
16.20 - "(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str), \n" ^
16.21 - "(6 ,[1] ,true ,#Given ,Cor boundVariable a , pen2str), \n" ^
16.22 - "(9 ,[1, 2] ,true ,#Given ,Cor interval {x. 0 \<le> x \<and> x \<le> 2 * r} , pen2str), \n" ^
16.23 - "(11 ,[1, 2, 3] ,true ,#Given ,Cor errorBound (eps = 0) , pen2str)]"
16.24 -then () else error "I_Model.to_string meth CHANGED";
16.25 +
16.26 +(*+*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A , pen2str), \n(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor valuesFor [a, b] , pen2str), \n(7 ,[2] ,true ,#Given ,Cor boundVariable b , pen2str), \n(9 ,[1, 2] ,true ,#Given ,Cor interval {x. 0 \<le> x \<and> x \<le> 2 * r} , pen2str), \n(11 ,[1, 2, 3] ,true ,#Given ,Cor errorBound (eps = 0) , pen2str)]"
16.27 + = meth |> I_Model.to_string @{context}
16.28 +
16.29 (*** Specification of Problem and MethodC model is complete, Solution starts ============== ***)
16.30
16.31 (* Step.specify_do_next ptp;
17.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Tue Oct 03 16:33:54 2023 +0200
17.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Wed Oct 25 12:34:12 2023 +0200
17.3 @@ -788,8 +788,10 @@
17.4 "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos))
17.5 = (tac, (pt, (p, p_')));
17.6
17.7 - val (o_model, ctxt, i_model) =
17.8 +(**)val return_complete_for =(**)
17.9 +(** ) val (o_model, ctxt, i_model) =( **)
17.10 Specify_Step.complete_for id (pt, pos);
17.11 +(*//------------------ step into complete_for ----------------------------------------------\\*)
17.12 "~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
17.13 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
17.14 ...} = Calc.specify_data (ctree, pos);
17.15 @@ -798,23 +800,123 @@
17.16 val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
17.17 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
17.18 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
17.19 - val thy = ThyC.get_theory ctxt dI
17.20 - val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
17.21 +
17.22 +(**)val return_match_itms_oris = (**)
17.23 +(** )val (_, (i_model, _)) = ( **)
17.24 + M_Match.match_itms_oris ctxt o_model' (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST i_prob)
17.25 + (m_patt, where_, where_rls);
17.26 +(*///----------------- step into match_itms_oris -------------------------------------------\\*)
17.27 +"~~~~~ fun match_itms_oris, args:"; val (ctxt, o_model, (pbl_imod, met_imod), (m_patt, where_, where_rls)) =
17.28 + (ctxt, o_model', (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST i_prob), (m_patt, where_, where_rls));
17.29 +
17.30 +(**)val return_fill_method =(**)
17.31 +(** )val met_imod =( **)
17.32 + fill_method o_model (pbl_imod, met_imod) m_patt;
17.33 +(*////--------------- step into fill_method -----------------------------------------------\\*)
17.34 +"~~~~~ fun fill_method , args:"; val (o_model, (pbl_imod, met_imod), met_patt) =
17.35 + (o_model, (pbl_imod, met_imod), m_patt);
17.36 +
17.37 + val pbl_max_vnts as [2, 1] = Model_Def.max_variants o_model pbl_imod
17.38 +
17.39 + (*probably pbl/met_imod = [], so take met_patt; if empty return Sup*)
17.40 + val i_from_met = map (fn (_, (descr, _)) => (*order from met_patt*)
17.41 + Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt (*\<longrightarrow> right order for args*)
17.42 +(*+MET: Sup..*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
17.43 + = i_from_met |> I_Model.to_string_TEST @{context}
17.44 +
17.45 + val met_max_vnts as [2, 1] = Model_Def.max_variants o_model i_from_met;
17.46 + val max_vnt as 2 = hd (inter op= pbl_max_vnts met_max_vnts);
17.47 + (*add items from pbl_imod (without overwriting existing items in met_imod)*)
17.48 +
17.49 +val return_add_other = map (
17.50 + add_other max_vnt pbl_imod) i_from_met;
17.51 +(*/////-------------- step into add_other -------------------------------------------------\\*)
17.52 +"~~~~~ fun add_other_5 , args:"; val (max_vnt, i1_model, (i2, _, bool2, m_field2, (Sup_TEST (descr2, ts2), pos2))) =
17.53 + (max_vnt, pbl_imod, nth 5 i_from_met);
17.54 +(*+*)val Const ("Input_Descript.FunctionVariable", _) = descr2;
17.55 +
17.56 +val (_, vnts1, _, _, (feedb1, _)) = (i2, [], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2))
17.57 +val SOME (descr1 as (Const ("Input_Descript.FunctionVariable", _)) ) =
17.58 + get_dscr' feedb1
17.59 +val true =
17.60 + descr1 = descr2
17.61 +val true =
17.62 + Model_Def.member_vnt vnts1 max_vnt
17.63 +val NONE =
17.64 + find_first (fn (_, vnts1, _, _, (feedb1, _)) => case get_dscr' feedb1 of
17.65 + NONE => false
17.66 + | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model
17.67 +
17.68 +val return_add_other_1 = (i2, [max_vnt], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2))
17.69 +val check as true = return_add_other_1 = nth 5 return_add_other
17.70 +(*\\\\\-------------- step into add_other -------------------------------------------------//*)
17.71 + val i_from_pbl = return_add_other
17.72 +(*\\\\---------------- step into fill_method -----------------------------------------------//*)
17.73 +val return_fill_method_step = filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) i_from_met
17.74 +
17.75 +(*+MET: dropped ALL DUE TO is_empty_single_TEST*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]" =
17.76 + return_fill_method_step |> I_Model.to_string_TEST @{context}
17.77 +(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
17.78 + = return_fill_method |> I_Model.to_string_TEST @{context};
17.79 +return_fill_method_step = return_fill_method; (*latter is correct, did not investigate further*)
17.80 +(*\\\----------------- step into match_itms_oris -------------------------------------------//*)
17.81 +val (_, (i_model, _)) = return_match_itms_oris;
17.82 +
17.83 +(*||------------------ continue. complete_for ------------------------------------------------*)
17.84 + val (o_model, ctxt, i_model) = return_complete_for
17.85 +(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
17.86 + = i_model |> I_Model.to_string_TEST @{context}
17.87 +(*+isa2:MET.Mis* ) val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(7 ,[1] ,false ,#Given ,Mis FunctionVariable funvar), \n(10 ,[1, 2] ,false ,#Given ,Mis Input_Descript.Domain doma), \n(12 ,[1, 2, 3] ,false ,#Given ,Mis ErrorBound err)]" =
17.88 + i_model |> I_Model.to_string @{context} ( *+isa2*)
17.89 +(*\\------------------ step into complete_for ----------------------------------------------//*)
17.90 + val (o_model, ctxt, i_model) = return_complete_for
17.91 +
17.92 +(*|------------------- continue. complete_for ------------------------------------------------*)
17.93 +val return_complete_for_step = (o_model', ctxt', i_model)
17.94 +
17.95 +val (o_model'_step, i_model_step) = (#1 return_complete_for_step, #3 return_complete_for_step)
17.96 +val (o_model', i_model) = (#1 return_complete_for, #3 return_complete_for)
17.97 +;
17.98 +if (o_model'_step, i_model_step) = (o_model', i_model)
17.99 +then () else error "return_complete_for_step <> return_complete_for";
17.100 (*\------------------- step into me Specify_Problem ----------------------------------------//*)
17.101 val (p,_,f,nxt,_,pt) = return_me_Specify_Problem
17.102
17.103 -val return_me_Add_Given_FunctionVariable
17.104 - = me nxt p c pt; val Add_Given "FunctionVariable a" = #4 return_me_Add_Given_FunctionVariable;
17.105 -(*/------------------- step into me Specify_Method -----------------------------------------\\*)
17.106 +val return_me_Specify_Method
17.107 + = me nxt p c pt; val Add_Given "FunctionVariable b" = #4 return_me_Specify_Method;
17.108 +(*/------------------- step into me_Specify_Method -----------------------------------------\\*)
17.109 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
17.110 +
17.111 +(*+isa==isa2*)val "[]" =(*+*) get_obj g_met pt (fst p) |> I_Model.to_string @{context}
17.112 +
17.113 val ctxt = Ctree.get_ctxt pt p
17.114 val (pt, p) =
17.115 - (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
17.116 case Step.by_tactic tac (pt, p) of
17.117 ("ok", (_, _, ptp)) => ptp;
17.118
17.119 +(*quick step into --> me_Specify_Method*)
17.120 +(*+*)val Specify_Method ["Optimisation", "by_univariate_calculus"] = tac;
17.121 +(* Step.by_tactic*)
17.122 +"~~~~~ fun by_tactic , args:"; val () = ();
17.123 +(* Step.check*)
17.124 +"~~~~~ fun check , args:"; val () = ();
17.125 +(*Specify_Step.check (Tactic.Specify_Method*)
17.126 +"~~~~~ fun check , args:"; val () = ();
17.127 +(*Specify_Step.complete_for*)
17.128 +"~~~~~ fun complete_for , args:"; val () = ();
17.129 +(* M_Match.match_itms_oris*)
17.130 +"~~~~~ fun match_itms_oris , args:"; val () = ();
17.131 +
17.132 +(*+*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(0 ,[2] ,false ,i_model_empty ,Sup FunctionVariable), \n(0 ,[2] ,false ,i_model_empty ,Sup Input_Descript.Domain), \n(0 ,[2] ,false ,i_model_empty ,Sup ErrorBound), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str)]"
17.133 + = get_obj g_met pt (fst p) |> I_Model.to_string @{context};
17.134 +(*
17.135 +(*+isa: METHOD.drop* )val"[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str)]" =( *+isaALLcorrect*)
17.136 +(*+isa2:METHOD.Mis*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(7 ,[1] ,false ,#Given ,Mis FunctionVariable funvar), \n(10 ,[1, 2] ,false ,#Given ,Mis Input_Descript.Domain doma), \n(12 ,[1, 2, 3] ,false ,#Given ,Mis ErrorBound err)]" =(*isa2*)
17.137 + get_obj g_met pt (fst p) |> I_Model.to_string @ {context};
17.138 +*)
17.139 (*case*)
17.140 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
17.141 +(*//------------------ step into Step.do_next ----------------------------------------------\\*)
17.142 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
17.143 (*if*) Pos.on_calc_end ip (*else*);
17.144 val (_, probl_id, _) = Calc.references (pt, p);
17.145 @@ -823,10 +925,12 @@
17.146 (*if*) probl_id = Problem.id_empty (*else*);
17.147
17.148 Step.switch_specify_solve p_ (pt, ip);
17.149 +(*///----------------- step into Step.switch_specify_solve ---------------------------------\\*)
17.150 "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
17.151 (*if*) Pos.on_specification ([], state_pos) (*then*);
17.152
17.153 Step.specify_do_next (pt, input_pos);
17.154 +(*////---------------- step into Step.specify_do_next --------------------------------------\\*)
17.155 "~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
17.156
17.157 val (_, (p_', tac)) =
17.158 @@ -838,7 +942,14 @@
17.159 (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
17.160 (*if*) p_ = Pos.Pbl (*else*);
17.161
17.162 +(*+*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(0 ,[2] ,false ,i_model_empty ,Sup FunctionVariable), \n(0 ,[2] ,false ,i_model_empty ,Sup Input_Descript.Domain), \n(0 ,[2] ,false ,i_model_empty ,Sup ErrorBound), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str)]"
17.163 + = met |> I_Model.to_string @{context};
17.164 +(*isa2* )val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(7 ,[1] ,false ,#Given ,Mis FunctionVariable funvar), \n(10 ,[1, 2] ,false ,#Given ,Mis Input_Descript.Domain doma), \n(12 ,[1, 2, 3] ,false ,#Given ,Mis ErrorBound err)]"
17.165 + =( *isa2*) met |> I_Model.to_string @{context};
17.166 +
17.167 +(*isa2*)val ("dummy", (Met, Add_Given "FunctionVariable b")) =(*isa2*)
17.168 Specify.for_method ctxt oris (o_refs, refs) (pbl, met);
17.169 +(*///// /------------- step into Step.for_method -------------------------------------------\\*)
17.170 "~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (_, met))
17.171 = (ctxt, oris, (o_refs, refs), (pbl, met));
17.172 val cmI = if mI = MethodC.id_empty then mI' else mI;
17.173 @@ -847,13 +958,14 @@
17.174 val NONE =
17.175 (*case*) find_first (I_Model.is_error o #5) met (*of*);
17.176
17.177 +(*isa2*)val SOME ("#Given", "FunctionVariable b") =(*isa2*)
17.178 (*case*)
17.179 Specify.item_to_add (ThyC.get_theory ctxt
17.180 (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
17.181 "~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
17.182 = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
17.183 -(*\------------------- step into me Specify_Method -----------------------------------------//*)
17.184 -val (p,_,f,nxt,_,pt) = return_me_Add_Given_FunctionVariable
17.185 +(*\------------------- step into me_Specify_Method -----------------------------------------//*)
17.186 +val (p,_,f,nxt,_,pt) = return_me_Specify_Method
17.187
17.188 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Input_Descript.Domain {0<..<r}" = nxt;
17.189 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "ErrorBound (\<epsilon> = 0)" = nxt;
18.1 --- a/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Tue Oct 03 16:33:54 2023 +0200
18.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Wed Oct 25 12:34:12 2023 +0200
18.3 @@ -56,14 +56,17 @@
18.4 val (o_model, ctxt, i_model) =
18.5 Specify_Step.complete_for id (pt, pos);
18.6 "~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
18.7 - val {origin = (o_model, _, _), probl = i_prob, ctxt,
18.8 + val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = met_imod, ctxt,
18.9 ...} = Calc.specify_data (ctree, pos);
18.10 + val ctxt = Ctree.get_ctxt ctree pos
18.11 + val (dI, _, _) = References.select_input o_refs refs;
18.12 val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
18.13 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
18.14 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
18.15
18.16 - val (_, (i_model, _)) =
18.17 - M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
18.18 + val (_, (i_model, _)) =
18.19 + M_Match.match_itms_oris ctxt o_model' (I_Model.OLD_to_TEST i_prob,
18.20 + I_Model.OLD_to_TEST i_prob) (m_patt, where_, where_rls);
18.21 "~~~~~ fun match_itms_oris , args:"; val (ctxt, pbl, (pbt, where_, where_rls), oris) =
18.22 (ctxt, i_prob, (m_patt, where_, where_rls), o_model');
18.23 (*0*)val mv = Pre_Conds.max_variant pbl;
19.1 --- a/test/Tools/isac/Test_Isac.thy Tue Oct 03 16:33:54 2023 +0200
19.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Oct 25 12:34:12 2023 +0200
19.3 @@ -75,12 +75,12 @@
19.4 "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine" (* setup for refine.sml *)
19.5 "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
19.6 "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
19.7 -(**)
19.8 +(*Test_Isac.thy*)
19.9 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
19.10 "$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) (*Test_Isac_Short*)
19.11 "$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) (*Test_Isac_Short*)
19.12 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
19.13 -(**)
19.14 +(*Test_Isac.thy*)
19.15 "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/Test_VSCode_Example"
19.16
19.17 begin
19.18 @@ -168,8 +168,8 @@
19.19 val return_XXXXX = "XXXXX"
19.20 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
19.21 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
19.22 -\<close> ML \<open> (*||----------- contine XXXXX ---------------------------------------------------------*)
19.23 -(*||------------------ contine XXXXX ---------------------------------------------------------*)
19.24 +\<close> ML \<open> (*||----------- contine-- XXXXX -------------------------------------------------------*)
19.25 +(*||------------------ contine-- XXXXX -------------------------------------------------------*)
19.26 (*\\------------------ step into XXXXX -----------------------------------------------------//*)
19.27 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
19.28 val "XXXXX" = return_XXXXX;
19.29 @@ -266,23 +266,23 @@
19.30
19.31 ML_file "Specify/formalise.sml"
19.32 ML_file "Specify/o-model.sml"
19.33 - ML_file "Specify/i-model.sml"
19.34 + ML_file "Specify/i-model.sml" (* (BROKEN!) test on elementwise input to lists*)
19.35 ML_file "Specify/pre-conditions.sml"
19.36 ML_file "Specify/p-model.sml"
19.37 - ML_file "Specify/m-match.sml"
19.38 + ML_file "Specify/m-match.sml"
19.39 ML_file "Specify/refine.sml" (* requires setup from refine.thy *)
19.40 ML_file "Specify/test-out.sml"
19.41 ML_file "Specify/specify-step.sml"
19.42 ML_file "Specify/specification.sml"
19.43 ML_file "Specify/cas-command.sml"
19.44 ML_file "Specify/p-spec.sml"
19.45 - ML_file "Specify/specify.sml"
19.46 - ML_file "Specify/sub-problem.sml"
19.47 +(*ML_file "Specify/specify.sml ---with M_Model.match_itms_oris broken elementwise input to lists---*)
19.48 +(*ML_file "Specify/sub-problem.sml" biegel, |> me' with M_Model.match_itms_oris broken*)
19.49 ML_file "Specify/step-specify.sml"
19.50
19.51 ML_file "Interpret/istate.sml"
19.52 ML_file "Interpret/error-pattern.sml"
19.53 - ML_file "Interpret/li-tool.sml"
19.54 + ML_file "Interpret/li-tool.sml"(*---with M_Model.match_itms_oris broken elementwise input to lists---*)
19.55 ML_file "Interpret/lucas-interpreter.sml"
19.56 ML_file "Interpret/step-solve.sml"
19.57
19.58 @@ -308,7 +308,7 @@
19.59 ML_file "BridgeJEdit/vscode-example.sml"
19.60 (**)
19.61
19.62 - ML_file "Knowledge/delete.sml"
19.63 + ML_file "Knowledge/delete.sml"
19.64 ML_file "Knowledge/descript.sml"
19.65 ML_file "Knowledge/simplify.sml"
19.66 ML_file "Knowledge/poly-1.sml"
19.67 @@ -322,7 +322,7 @@
19.68 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
19.69 ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered----Test_Isac_Short*)
19.70 ML_file "Knowledge/rootrat.sml"
19.71 - ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
19.72 + ML_file "Knowledge/rootrateq.sml"(*one complicated equations not recovered from 2002 *)
19.73 (*ML_file "Knowledge/partial_fractions.sml" hangs with ML_system_64 = "true"---Test_Isac_Short*)
19.74 ML_file "Knowledge/polyeq-1.sml"
19.75 ML_file "Knowledge/polyeq-2.sml" (*Test_Isac_Short*)
19.76 @@ -344,7 +344,7 @@
19.77 ML_file "Knowledge/biegelinie-1.sml"
19.78 ML_file "Knowledge/biegelinie-2.sml" (*Test_Isac_Short*)
19.79 ML_file "Knowledge/biegelinie-3.sml" (*Test_Isac_Short*)
19.80 - ML_file "Knowledge/biegelinie-4.sml"
19.81 +(*ML_file "Knowledge/biegelinie-4.sml" (*with M_Model.match_itms_oris broken in |> me'*)*)
19.82 ML_file "Knowledge/algein.sml"
19.83 ML_file "Knowledge/diophanteq.sml"
19.84 (*ML_file "Knowledge/inverse_z_transform.sml"hangs with ML_system_64 = "true"---Test_Isac_Short*)
19.85 @@ -786,7 +786,11 @@
19.86 Up to the above Mercurial changeset 5100a9c3abf8 isac used CVS;
19.87 see https://intra.ist.tugraz.at/hg/isac containing a conversion to Mercurial.
19.88 \<close>
19.89 +ML \<open>
19.90 +\<close> ML \<open>
19.91
19.92 +\<close> ML \<open>
19.93 +\<close>
19.94 end
19.95 (*========== inhibit exn 130719 Isabelle2013 ===================================
19.96 ============ inhibit exn 130719 Isabelle2013 =================================*)
20.1 --- a/test/Tools/isac/Test_Isac_Short.thy Tue Oct 03 16:33:54 2023 +0200
20.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Wed Oct 25 12:34:12 2023 +0200
20.3 @@ -75,12 +75,12 @@
20.4 "$ISABELLE_ISAC_TEST/Tools/isac/Specify/refine" (* setup for refine.sml *)
20.5 "$ISABELLE_ISAC_TEST/Tools/isac/ProgLang/calculate" (* setup for evaluate.sml *)
20.6 "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate" (* setup for integrate.sml*)
20.7 -(** )
20.8 +(*Test_Isac_Short.thy* )
20.9 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
20.10 (*"$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*) Test_Isac_Short*)
20.11 (*"$ISABELLE_ISAC/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*) Test_Isac_Short*)
20.12 (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
20.13 -( **)
20.14 +( *Test_Isac_Short.thy*)
20.15 "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/Test_VSCode_Example"
20.16
20.17 begin
20.18 @@ -164,6 +164,7 @@
20.19 (*//------------------ build fun XXXXX -----------------------------------------------------\\*)
20.20 (*\\------------------ build fun XXXXX -----------------------------------------------------//*)
20.21 \<close> ML \<open> (*\\----------- build fun XXXXX -----------------------------------------------------//*)
20.22 +
20.23 val return_XXXXX = "XXXXX"
20.24 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
20.25 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
20.26 @@ -275,13 +276,13 @@
20.27 ML_file "Specify/specification.sml"
20.28 ML_file "Specify/cas-command.sml"
20.29 ML_file "Specify/p-spec.sml"
20.30 - ML_file "Specify/specify.sml"
20.31 - ML_file "Specify/sub-problem.sml"
20.32 +(*ML_file "Specify/specify.sml ---with M_Model.match_itms_oris broken elementwise input to lists---*)
20.33 +(*ML_file "Specify/sub-problem.sml" biegel, |> me' with M_Model.match_itms_oris broken*)
20.34 ML_file "Specify/step-specify.sml"
20.35
20.36 ML_file "Interpret/istate.sml"
20.37 ML_file "Interpret/error-pattern.sml"
20.38 - ML_file "Interpret/li-tool.sml"
20.39 + ML_file "Interpret/li-tool.sml"(*---with M_Model.match_itms_oris broken elementwise input to lists---*)
20.40 ML_file "Interpret/lucas-interpreter.sml"
20.41 ML_file "Interpret/step-solve.sml"
20.42
20.43 @@ -343,7 +344,7 @@
20.44 ML_file "Knowledge/biegelinie-1.sml"
20.45 (*ML_file "Knowledge/biegelinie-2.sml" Test_Isac_Short*)
20.46 (*ML_file "Knowledge/biegelinie-3.sml" Test_Isac_Short*)
20.47 - ML_file "Knowledge/biegelinie-4.sml"
20.48 +(*ML_file "Knowledge/biegelinie-4.sml" (*with M_Model.match_itms_oris broken in |> me'*)*)
20.49 ML_file "Knowledge/algein.sml"
20.50 ML_file "Knowledge/diophanteq.sml"
20.51 (*ML_file "Knowledge/inverse_z_transform.sml"hangs with ML_system_64 = "true"---Test_Isac_Short*)
20.52 @@ -787,7 +788,7 @@
20.53 \<close>
20.54 ML \<open>
20.55 \<close> ML \<open>
20.56 -\<close> ML \<open>
20.57 +
20.58 \<close> ML \<open>
20.59 \<close>
20.60 end
21.1 --- a/test/Tools/isac/Test_Theory.thy Tue Oct 03 16:33:54 2023 +0200
21.2 +++ b/test/Tools/isac/Test_Theory.thy Wed Oct 25 12:34:12 2023 +0200
21.3 @@ -68,7 +68,1144 @@
21.4 \<close>
21.5
21.6 section \<open>===================================================================================\<close>
21.7 +section \<open>===== new code match_itms_oris ====================================================\<close>
21.8 +ML \<open>
21.9 +\<close> ML \<open>
21.10 +open Ctree;
21.11 +open Pos;
21.12 +open TermC;
21.13 +open Istate;
21.14 +open Tactic;
21.15 +open I_Model;
21.16 +open P_Model
21.17 +open Rewrite;
21.18 +open Step;
21.19 +open LItool;
21.20 +open LI;
21.21 +open Test_Code
21.22 +open Specify
21.23 +open ME_Misc
21.24 +open Pre_Conds;
21.25 +\<close> ML \<open> (*//----------- build fun match_itms_oris -------------------------------------------\\*)
21.26 +(*//------------------ build fun match_itms_oris -------------------------------------------\\*)
21.27 +\<close> ML \<open>
21.28 +\<close> text \<open> (*\<longrightarrow> model-def.sml*)
21.29 +fun member_vnt [] _ = true
21.30 + | member_vnt vnts vnt = member op= vnts vnt
21.31 +;
21.32 +member_vnt: variants -> variant -> bool
21.33 +\<close> ML \<open>
21.34 +\<close> text \<open> (*\<longrightarrow> i-model.sml <> Pre_Conds.get_descr_vnt*)
21.35 +(*
21.36 + in case there is an item in i2_model = met with Sup_TEST,
21.37 + find_first an appropriate (variant, descriptor) item in i1_model = pbl and add it instead Sup_TEST,
21.38 + otherwise keep the items of i2_model.
21.39 +*)
21.40 +fun add_other max_vnt i1_model (i2, _, bool2, m_field2, (Sup_TEST (descr2, ts2), pos2)) =
21.41 + (case find_first (fn (_, vnts1, _, _, (feedb1, _)) => case Pre_Conds.get_dscr' feedb1 of
21.42 + NONE => false
21.43 + | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model of
21.44 + NONE =>
21.45 + (i2, [max_vnt], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2)) (*the present in i2_model*)
21.46 + | SOME i1_single => i1_single) (*shift the item from i1_model to i2_model*)
21.47 + | add_other _ _ i2_single = i2_single (*keep all the other items in i2_model*)
21.48 +;
21.49 +add_other: variant -> I_Model.T_TEST -> I_Model.single_TEST -> I_Model.single_TEST
21.50 +\<close> ML \<open>
21.51 +\<close> text \<open> (*\<longrightarrow> i-model.sml*)
21.52 +(*
21.53 + Establish the order of items (wrt. descriptor) in the method's i_model as given by meth_patt,
21.54 + i.e as required by the formal arguments of the program.
21.55 + Missing items are inserted as Sup(erfluous).
21.56 +/-TODO-----------------------^^-Inc [] ------- output with input-template automatically------\
21.57 +\-TODO---------------------------------------------------------------------------------------/
21.58 + In order to maintain what the user sees as Model, copy the items from the problem's i_model
21.59 + to the method's i_model.
21.60 +*)
21.61 +(*compare fun s_make_complete*)
21.62 +fun fill_method o_model (pbl_imod, met_imod) met_patt =
21.63 + let
21.64 + val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod
21.65 + (*probably pbl/met_imod = [], so take met_patt; if empty return Sup*)
21.66 + val i_from_met = map (fn (_, (descr, _)) => (*order from met_patt*)
21.67 + Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt (*\<longrightarrow> right order for args*)
21.68 +
21.69 + val met_max_vnts = Model_Def.max_variants o_model i_from_met;
21.70 + val max_vnt = hd (inter op= pbl_max_vnts met_max_vnts);
21.71 + (*add items from pbl_imod (without overwriting existing items in met_imod)*)
21.72 + in
21.73 + map (add_other max_vnt pbl_imod) i_from_met
21.74 + end
21.75 +;
21.76 +fill_method: O_Model.T -> I_Model.T_TEST * I_Model.T_TEST-> Model_Pattern.T ->
21.77 + I_Model.T_TEST
21.78 +\<close> ML \<open>
21.79 +\<close> ML \<open> (*\<longrightarrow> m-match.sml*)
21.80 +(*the OLD version built upon a wrong idea with find missing items from o_model*)
21.81 +\<close> ML \<open>
21.82 +(*OLD*)
21.83 +(*---*)
21.84 +fun match_itms_oris ctxt o_model (pbl_imod, met_imod) (met_patt, where_, where_rls) =
21.85 + let
21.86 + val met_imod = I_Model.fill_method o_model (pbl_imod, met_imod) met_patt
21.87 + val (check, preconds) = Pre_Conds.check ctxt where_rls where_ (met_patt, met_imod)
21.88 + in
21.89 + (check, (met_imod, preconds))
21.90 + end
21.91 +(*NEW*)
21.92 +;
21.93 +match_itms_oris: Proof.context -> O_Model.T -> I_Model.T_TEST * I_Model.T_TEST ->
21.94 + Model_Pattern.T * Pre_Conds.unchecked * Rule_Def.rule_set ->
21.95 + bool * (I_Model.T_TEST * Pre_Conds.T)
21.96 +\<close> ML \<open>
21.97 +(*\\------------------ build fun match_itms_oris -------------------------------------------//*)
21.98 +\<close> ML \<open> (*\\----------- build fun match_itms_oris -------------------------------------------//*)
21.99 +\<close> ML \<open>
21.100 +\<close>
21.101 +
21.102 +(*ML_file "Minisubpbl/100-init-rootpbl-NEXT_STEP.sml" (*get from isa-a-.. -----------------*)
21.103 +section \<open>===================================================================================\<close>
21.104 section \<open>===== ============================================================================\<close>
21.105 +ML \<open>
21.106 +\<close> ML \<open>
21.107 +
21.108 +\<close> ML \<open>
21.109 +\<close>
21.110 +---------------------------------------------------------------------- testing unnecessary *)
21.111 +
21.112 +(*ML_file "Minisubpbl/150a-add-given-Maximum.sml"*)
21.113 +section \<open>===================================================================================\<close>
21.114 +section \<open>===== "Minisubpbl/150a-add-given-Maximum.sml" ====================================\<close>
21.115 +ML \<open>
21.116 +\<close> ML \<open>
21.117 +(* Title: "Minisubpbl/150a-add-given-Maximum.sml"
21.118 + Author: Walther Neuper 1105
21.119 + (c) copyright due to lincense terms.
21.120 +
21.121 +COMPARE Specify/specify.sml --- specify-phase: low level functions ---
21.122 +
21.123 +ATTENTION: the file creates buffer overflow if copied in one piece !
21.124 +
21.125 +Note: This test --- steps into me --- more than once, to a somewhat extreme extent;
21.126 + in order not to get lost while working in Test_Some etc,
21.127 + re-introduce ML (*--- step into XXXXX ---*) and Co.
21.128 + and use Sidekick for orientation.
21.129 + Nesting is indicated by /--- //-- ///- at the left margin of the comments.
21.130 +*)
21.131 +
21.132 +open Ctree;
21.133 +open Pos;
21.134 +open TermC;
21.135 +open Istate;
21.136 +open Tactic;
21.137 +open I_Model;
21.138 +open P_Model
21.139 +open Rewrite;
21.140 +open Step;
21.141 +open LItool;
21.142 +open LI;
21.143 +open Test_Code
21.144 +open Specify
21.145 +open ME_Misc
21.146 +open Pre_Conds;
21.147 +
21.148 +val (_(*example text*),
21.149 + (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
21.150 + "Extremum (A = 2 * u * v - u \<up> 2)" ::
21.151 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
21.152 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
21.153 + "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
21.154 +(*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
21.155 + "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
21.156 + "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
21.157 + "ErrorBound (\<epsilon> = (0::real))" :: []),
21.158 + refs as ("Diff_App",
21.159 + ["univariate_calculus", "Optimisation"],
21.160 + ["Optimisation", "by_univariate_calculus"])))
21.161 + = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
21.162 +
21.163 +val c = [];
21.164 +val return_init_calc =
21.165 + Test_Code.init_calc @{context} [(model, refs)]; (*val Model_Problem = nxt;*)
21.166 +(*/------------------- step into init_calc -------------------------------------------------\\*)
21.167 +"~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))]) =
21.168 + (@{context}, [(model, refs)]);
21.169 + val thy = thy_id |> ThyC.get_theory ctxt
21.170 + val ((pt, p), tacis) = Step_Specify.initialise' thy (model, refs)
21.171 + val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
21.172 + val f =
21.173 + TESTg_form ctxt (pt,p);
21.174 +"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p));
21.175 + val (form, _, _) =
21.176 + ME_Misc.pt_extract ctxt ptp;
21.177 +"~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_ as Pbl(*Frm,Pbl*)))) = (ctxt, ptp);
21.178 + val ppobj = Ctree.get_obj I pt p
21.179 + val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;
21.180 + (*if*) Ctree.is_pblobj ppobj (*then*);
21.181 + pt_model ppobj p_ ;
21.182 +"~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}), Pbl_) =
21.183 + (ppobj, p_);
21.184 + val (_, pI, _) = Ctree.get_somespec' spec spec';
21.185 +(* val where_ = if pI = Problem.id_empty then []*)
21.186 + (*if*) pI = Problem.id_empty (*else*);
21.187 + val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
21.188 + val (_, where_) =
21.189 + Pre_Conds.check ctxt where_rls where_
21.190 + (model, I_Model.OLD_to_TEST probl);
21.191 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
21.192 + (ctxt, where_rls, where_, (model, I_Model.OLD_to_TEST probl));
21.193 + val (env_model, (env_subst, env_eval)) =
21.194 + make_environments model_patt i_model;
21.195 +"~~~~~ fun make_environments , args:"; val (_, []) = (model_patt, i_model);
21.196 +(*\------------------- step into init_calc -------------------------------------------------//*)
21.197 +val (p,_,f,nxt,_,pt) = return_init_calc;
21.198 +
21.199 +(*+*)val PblObj {ctxt, probl, ...} = get_obj I pt [];
21.200 +(*+*)Proof_Context.theory_of ctxt (*= {Pure, .., Diff_App}*);
21.201 +(*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term ctxt "r"
21.202 +(*+*)val [] = probl
21.203 +
21.204 +val return_me_Model_Problem =
21.205 + me nxt p c pt; val Add_Given "Constants [r = 7]" = #4 return_me_Model_Problem;
21.206 +(*/------------------- step into me Model_Problem ------------------------------------------\\*)
21.207 +"~~~~~ fun me , args:"; val (tac, (p:Pos.pos'), (_:Test_Code.NEW), (pt:Ctree.ctree)) = (nxt, p, c, pt);
21.208 + val ctxt = Ctree.get_ctxt pt p
21.209 +val return_by_tactic = case
21.210 + Step.by_tactic tac (pt,p) of
21.211 + ("ok", (_, _, ptp)) => ptp;
21.212 +
21.213 +(*//------------------ step into by_tactic -------------------------------------------------\\*)
21.214 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
21.215 +val Applicable.Yes tac' = (*case*)
21.216 + Step.check tac (pt, p) (*of*);
21.217 +(*+*)val Model_Problem' _ = tac';
21.218 +"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
21.219 + (*if*) Tactic.for_specify tac (*then*);
21.220 +
21.221 +Specify_Step.check tac (ctree, pos);
21.222 +"~~~~~ fun check , args:"; val (Tactic.Model_Problem, (pt, pos as (p, _))) =
21.223 + (tac, (ctree, pos));
21.224 + val (o_model, pI', ctxt) = case Ctree.get_obj I pt p of
21.225 + Ctree.PblObj {origin = (o_model, (_, pI', _), _), ctxt, ...} => (o_model, pI', ctxt)
21.226 + val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
21.227 + val pbl = I_Model.init_TEST o_model model_patt;
21.228 +
21.229 +val return_check =
21.230 + Applicable.Yes (Tactic.Model_Problem' (pI', I_Model.TEST_to_OLD pbl, []));
21.231 +(*\\------------------ step into by_tactic -------------------------------------------------//*)
21.232 +val (pt, p) = return_by_tactic;
21.233 +
21.234 +val return_do_next = (*case*)
21.235 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
21.236 +(*//------------------ step into do_next ---------------------------------------------------\\*)
21.237 +"~~~~~ fun do_next , args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) =
21.238 + (p, ((pt, e_pos'),[]));
21.239 + val pIopt = get_pblID (pt,ip);
21.240 + (*if*) ip = ([],Res); (* = false*)
21.241 + val _ = (*case*) tacis (*of*);
21.242 + val SOME _ = (*case*) pIopt (*of*);
21.243 +
21.244 + val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
21.245 + Step.switch_specify_solve p_ (pt, ip);
21.246 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
21.247 + (*if*) Pos.on_specification ([], state_pos) (*then*);
21.248 +
21.249 + val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
21.250 + Step.specify_do_next (pt, input_pos);
21.251 +(*///----------------- step into specify_do_next -------------------------------------------\\*)
21.252 +"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
21.253 +
21.254 +(* val (_, (p_', tac)) =*)
21.255 +val return_find_next_step = (*keep for continuing specify_do_next*)
21.256 + Specify.find_next_step ptp;
21.257 +(*////---------------- step into find_next_step --------------------------------------------\\*)
21.258 +"~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
21.259 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
21.260 + spec = refs, ...} = Calc.specify_data (pt, pos);
21.261 + val ctxt = Ctree.get_ctxt pt pos;
21.262 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
21.263 + (*if*) p_ = Pos.Pbl (*then*);
21.264 +
21.265 + Specify.for_problem ctxt oris (o_refs, refs) (pbl, met);
21.266 +(*/////--------------- step into for_problem -----------------------------------------------\\*)
21.267 +"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
21.268 + = (ctxt, oris, (o_refs, refs), (pbl, met));
21.269 + val cdI = if dI = ThyC.id_empty then dI' else dI;
21.270 + val cpI = if pI = Problem.id_empty then pI' else pI;
21.271 + val cmI = if mI = MethodC.id_empty then mI' else mI;
21.272 + val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
21.273 + val {model = mpc, ...} = MethodC.from_store ctxt cmI;
21.274 +
21.275 + val return_check_OLD =
21.276 + check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
21.277 +(*//////-------------- step into check -------------------------------------------------\\*)
21.278 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
21.279 + (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
21.280 + val return_make_environments =
21.281 + make_environments model_patt i_model;
21.282 +(*///// //------------ step into of_max_variant --------------------------------------------\\*)
21.283 +"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) =
21.284 + (model_patt, i_model);
21.285 +
21.286 +(*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc_TEST Constants [] [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc_TEST AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc_TEST SideConditions [] [__=__, __=__], Position.T))]"
21.287 + = i_model |> I_Model.to_string_TEST @{context}
21.288 + val all_variants =
21.289 + map (fn (_, variants, _, _, _) => variants) i_model
21.290 + |> flat
21.291 + |> distinct op =
21.292 + val variants_separated = map (filter_variants' i_model) all_variants
21.293 + val sums_corr = map (Model_Def.cnt_corrects) variants_separated
21.294 + val sum_variant_s = Model_Def.arrange_args sums_corr (1, all_variants)
21.295 +(*+*)val [(0, 1), (0, 2), (0, 3)] = sum_variant_s
21.296 + val (_, max_variant) = hd (*..crude decision, up to improvement *)
21.297 + (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
21.298 + val i_model_max =
21.299 + filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
21.300 + val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
21.301 +(*for building make_env_s -------------------------------------------------------------------\*)
21.302 +(*!!!*) val ("#Given", (descr, term), pos) =
21.303 + Model_Pattern.split_descriptor ctxt ("#Given", @{term "Constants [r = (7::real)]"}, Position.none)
21.304 +(*!!!*) val patt = equal_descr_pairs |> hd |> #1
21.305 +(*!!!*)val equal_descr_pairs =
21.306 + (patt,
21.307 + (1, [1, 2, 3], true, "#Given", (Cor_TEST ((descr, (*!*)TermC.isalist2list(*!*) term)), pos)))
21.308 + :: tl equal_descr_pairs
21.309 +(*for building make_env_s -------------------------------------------------------------------/*)
21.310 +
21.311 + val env_model = make_env_model equal_descr_pairs;
21.312 +(*///// ///----------- step into make_env_model --------------------------------------------\\*)
21.313 +"~~~~~ fun make_env_model , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
21.314 +
21.315 +val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
21.316 + => (mk_env_model id feedb));
21.317 +val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 4 equal_descr_pairs;
21.318 +(*\\\\\ \\\----------- step into make_env_model --------------------------------------------//*)
21.319 +(*||||| ||------------ contine of_max_variant ------------------------------------------------*)
21.320 +
21.321 + val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
21.322 + val subst_eval_list = make_envs_preconds equal_givens
21.323 +val return_make_envs_preconds =
21.324 + make_envs_preconds equal_givens;
21.325 +(*///// ///----------- step into make_envs_preconds ----------------------------------------\\*)
21.326 +"~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
21.327 +val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb)
21.328 +;
21.329 +xxx: (Model_Pattern.single * I_Model.single_TEST) -> ((term * term) * (term * term)) list;
21.330 +val return_discern_feedback =
21.331 + discern_feedback id feedb;
21.332 +(*nth 1 equal_descr_pairs* )
21.333 +"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb);
21.334 +( *nth 2 equal_descr_pairs*)
21.335 +"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Inc_TEST ((descr, ts)))) = (id, feedb);
21.336 +
21.337 +(*nth 1 equal_descr_pairs* )
21.338 +(*+*)val [((Const ("fixes", typ1), Free ("r", typ2)),
21.339 + (Free ("r", typ3), value))] = return_discern_feedback
21.340 +(*+*)val true = typ1 = typ2
21.341 +(*+*)val true = typ3 = HOLogic.realT
21.342 +(*+*)val "7" = UnparseC.term @{context} value
21.343 +( *nth 2 equal_descr_pairs*)
21.344 +(*+*)val [] = return_discern_feedback
21.345 +
21.346 +val return_discern_typ =
21.347 + discern_typ id (descr, ts);
21.348 +"~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));
21.349 +(*nth 1 equal_descr_pairs* )
21.350 +(*+*)val [((Const ("fixes", typ1), Free ("r", typ2)),
21.351 + (Free ("r", typ3), value))] = return_discern_typ
21.352 +(*+*)val true = typ1 = typ2
21.353 +(*+*)val true = typ3 = HOLogic.realT
21.354 +(*+*)val "7" = UnparseC.term @{context} value
21.355 +( *nth 2 equal_descr_pairs*)
21.356 +(*+*)val [] = return_discern_typ;
21.357 +(**)
21.358 + switch_type id ts;
21.359 +"~~~~~ fun switch_type , args:"; val (Const (descr_string, _), ts) = (descr, ts);
21.360 +
21.361 +(*nth 1 equal_descr_pairs* )
21.362 +val return_switch_type_TEST = Const (descr_string, ts |> hd |> TermC.lhs |> type_of)
21.363 +
21.364 +(*+*)val Const ("Input_Descript.Constants", typ) = return_switch_type_TEST
21.365 +(*+*)val Type ("Real.real", []) = typ
21.366 +( *nth 2 equal_descr_pairs*)
21.367 +(*+*)val return_switch_type_TEST = descr
21.368 +(**)
21.369 +(*\\\\\ \\\----------- step into make_envs_preconds ----------------------------------------//*)
21.370 +(*||||| ||------------ contine of_max_variant ------------------------------------------------*)
21.371 + val subst_eval_list = make_envs_preconds equal_givens
21.372 + val (env_subst, env_eval) = split_list subst_eval_list
21.373 +val make_environments = (i_model_max, env_model, (env_subst, env_eval)); (*GOON*)
21.374 +(*\\\\\ \\------------ step into of_max_variant --------------------------------------------//*)
21.375 + val (i_model_max, env_model, (env_subst, env_eval)) = make_environments
21.376 +(*!!!/----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---\*)
21.377 + val (i_max_variant, env_model, (env_subst, env_eval)) = (i_model_max, [], ([], []))
21.378 +(*!!!\----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---/*)
21.379 +(*||||||-------------- contine check -----------------------------------------------------*)
21.380 + val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
21.381 + val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
21.382 + val full_subst = if env_eval = [] then pres_subst_other
21.383 + else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
21.384 + val evals = map (eval ctxt where_rls) full_subst
21.385 +val return_ = (i_model_max, env_subst, env_eval)
21.386 +(*\\\\\\\------------- step into check -------------------------------------------------//*)
21.387 +val (preok, _) = return_check_OLD;
21.388 +
21.389 +(*|||||--------------- contine for_problem ---------------------------------------------------*)
21.390 + (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
21.391 + (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
21.392 +val NONE =
21.393 + (*case*) find_first (I_Model.is_error o #5) pbl (*of*);
21.394 +
21.395 + (*case*)
21.396 + Specify.item_to_add (ThyC.get_theory ctxt
21.397 + (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
21.398 +"~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
21.399 + = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl);
21.400 + fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
21.401 + | false_and_not_Sup (_, _, false, _, _) = true
21.402 + | false_and_not_Sup _ = false
21.403 +
21.404 + val v = if itms = [] then 1 else Pre_Conds.max_variant itms
21.405 + val vors = if v = 0 then oris
21.406 + else filter ((fn variant =>
21.407 + fn (_, variants, m_field, _, _) => member op= variants variant andalso m_field <> "#undef")
21.408 + v) oris
21.409 +
21.410 +(*+*)val "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"])]"
21.411 +(*+*) = vors |> O_Model.to_string @{context}
21.412 +
21.413 + val vits = if v = 0 then itms (* because of dsc without dat *)
21.414 + else filter ((fn variant =>
21.415 + fn (_, variants, _, _, _) => member op= variants variant)
21.416 + v) itms; (* itms..vat *)
21.417 +
21.418 + val icl = filter false_and_not_Sup vits; (* incomplete *)
21.419 +
21.420 + (*if*) icl = [] (*else*);
21.421 +(*+*)val "[\n(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] , pen2str), \n(2 ,[1, 2, 3] ,false ,#Find ,Inc Maximum , pen2str), \n(3 ,[1, 2, 3] ,false ,#Find ,Inc AdditionalValues [] , pen2str), \n(4 ,[1, 2, 3] ,false ,#Relate ,Inc Extremum , pen2str), \n(5 ,[1, 2] ,false ,#Relate ,Inc SideConditions [] , pen2str)]"
21.422 + = icl |> I_Model.to_string @{context}
21.423 +(*+*)val "(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] , pen2str)"
21.424 + = hd icl |> I_Model.single_to_string @{context}
21.425 +
21.426 +(*++*)val feedback = (fn (_, _, _, _, feedback) => feedback) (hd icl)
21.427 +(*++*)val Const ("Input_Descript.Constants", _) = I_Model.descriptor feedback
21.428 +(*++*)val [] = I_Model.o_model_values feedback
21.429 +
21.430 +(*+*)val "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"])]"
21.431 +(*+*) = vors |> O_Model.to_string @{context}
21.432 +
21.433 +val SOME ori =
21.434 + (*case*) find_first ((fn (_, _, _, _, feedback) => fn (_, _, _, d, ts) =>
21.435 + d = I_Model.descriptor feedback andalso subset op = (I_Model.o_model_values feedback, ts))
21.436 + (hd icl)) vors (*of*);
21.437 +
21.438 +(*+*)val "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"])" =
21.439 +(*+*) ori |> O_Model.single_to_string @{context}
21.440 +(*\\\\\--------------- step into for_problem -----------------------------------------------//*)
21.441 +(*\\\\---------------- step into find_next_step --------------------------------------------//*)
21.442 +(*|||----------------- continuing specify_do_next --------------------------------------------*)
21.443 +val (_, (p_', tac)) = return_find_next_step (*kept for continuing specify_do_next*)
21.444 +
21.445 + val ist_ctxt = Ctree.get_loc pt (p, p_)
21.446 +(*+*)val Add_Given "Constants [r = 7]" = tac
21.447 +val _ =
21.448 + (*case*) tac (*of*);
21.449 +
21.450 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
21.451 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =
21.452 + (tac, (pt, (p, p_')));
21.453 +
21.454 + Specify.by_Add_ "#Given" ct ptp;
21.455 +"~~~~~ fun by_Add_ , args:"; val (m_field, ct ,(pt, pos as (_, p_))) =
21.456 + ("#Given", ct, ptp);
21.457 + val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
21.458 + val (i_model, m_patt) =
21.459 + if p_ = Pos.Met then
21.460 + (met,
21.461 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
21.462 + else
21.463 + (pbl,
21.464 + (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model);
21.465 +
21.466 + (*case*)
21.467 + I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
21.468 +"~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, (str(*, pos*))) =
21.469 + (ctxt, m_field, oris, i_model, m_patt, ct);
21.470 + val (t as (descriptor $ _)) = Syntax.read_term ctxt str
21.471 +
21.472 +(*+*)val "Constants [r = 7]" = UnparseC.term @{context} t;
21.473 +
21.474 + val SOME m_field' =
21.475 + (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
21.476 + (*if*) m_field <> m_field' (*else*);
21.477 +
21.478 +(*+*)val "#Given" = m_field; val "#Given" = m_field'
21.479 +
21.480 +val ("", ori', all) =
21.481 + (*case*) O_Model.contains ctxt m_field o_model t (*of*);
21.482 +
21.483 +(*+*)val (_, _, _, _, vals) = hd o_model;
21.484 +(*+*)val "Constants [r = 7]" = UnparseC.term @{context} (@{term Constants} $ (hd vals));
21.485 +(*+*)if "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), " ^
21.486 +(*+*) "\n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), " ^
21.487 +(*+*) "\n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), " ^
21.488 +(*+*) "\n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), " ^
21.489 +(*+*) "\n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), " ^
21.490 +(*+*) "\n(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), " ^
21.491 +(*+*) "\n(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), " ^
21.492 +(*+*) "\n(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), " ^
21.493 +(*+*) "\n(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), " ^
21.494 +(*+*) "\n(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), " ^
21.495 +(*+*) "\n(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
21.496 +(*+*)= O_Model.to_string @{context} o_model then () else error "o_model CHANGED";
21.497 +
21.498 + (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*);
21.499 +"~~~~~ fun is_notyet_input , args:"; val (ctxt, itms, all, (i, v, f, d, ts), pbt) =
21.500 + (ctxt, i_model, all, ori', m_patt);
21.501 +val SOME (_, (_, pid)) =
21.502 + (*case*) find_first (eq1 d) pbt (*of*);
21.503 +(*local*)fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (I_Model.descriptor itm_);(*local*)
21.504 +val SOME (_, _, _, _, itm_) =
21.505 + (*case*) find_first (eq3 f d) itms (*of*);
21.506 +val ts' = inter op = (o_model_values itm_) ts;
21.507 + (*if*) subset op = (ts, ts') (*else*);
21.508 +val return_is_notyet_input = ("",
21.509 + ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts));
21.510 +"~~~~~ fun ori_2itm , args:"; val (itm_, pid, all, (id, vt, fd, d, ts)) =
21.511 + (itm_, pid, all, (i, v, f, d, subtract op = ts' ts));
21.512 + val ts' = union op = (o_model_values itm_) ts;
21.513 + val pval = [Input_Descript.join'''' (d, ts')]
21.514 + val complete = if eq_set op = (ts', all) then true else false
21.515 +
21.516 +(*+*)val "Inc Constants [] , pen2str" = itm_ |> I_Model.feedback_to_string @{context}
21.517 +(*\\\----------------- step into specify_do_next -------------------------------------------//*)
21.518 +(*\\------------------ step into do_next ---------------------------------------------------//*)
21.519 +val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next
21.520 +
21.521 +(*|------------------- continue with me_Model_Problem ----------------------------------------*)
21.522 +
21.523 +val tacis as (_::_) =
21.524 + (*case*) ts (*of*);
21.525 + val (tac, _, _) = last_elem tacis
21.526 +
21.527 +val return_Model_Problem = (p, [] : NEW, TESTg_form ctxt (pt, p), tac, Celem.Sundef, pt);
21.528 +(*//------------------ step into TESTg_form ------------------------------------------------\\*)
21.529 +"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt, p));
21.530 +
21.531 + val (form, _, _) =
21.532 + ME_Misc.pt_extract ctxt ptp;
21.533 +"~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_(*Frm,Pbl*)))) = (ctxt, ptp);
21.534 + val ppobj = Ctree.get_obj I pt p
21.535 + val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;
21.536 + (*if*) Ctree.is_pblobj ppobj (*then*);
21.537 +
21.538 + pt_model ppobj p_;
21.539 +"~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, o_spec, hdl), ctxt, ...}),
21.540 + Pbl(*Frm,Pbl*)) = (ppobj, p_);
21.541 + val (_, _, met_id) = References.select_input o_spec spec
21.542 + val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to_TEST probl) (Pos.Met, met_id)
21.543 +val return_pt_model = Ctree.ModSpec (allcorr, Pos.Pbl, hdl, probl, (*where_*)[(*Problem.from_store in check*)], spec)
21.544 +
21.545 +(*|------------------- continue with TESTg_form ----------------------------------------------*)
21.546 +val Ctree.ModSpec (spec as (_, p_, _, gfr, where_, _)) =
21.547 + (*case*) form (*of*);
21.548 + Test_Out.PpcKF ( (Test_Out.Problem [],
21.549 + P_Model.from (Proof_Context.theory_of ctxt) gfr where_));
21.550 +
21.551 +\<close> ML \<open>
21.552 + P_Model.from (Proof_Context.theory_of ctxt) gfr where_;
21.553 +"~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
21.554 + fun coll model [] = model
21.555 + | coll model ((_, _, _, field, itm_) :: itms) =
21.556 + coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
21.557 +
21.558 + val gfr = coll P_Model.empty itms;
21.559 +"~~~~~ fun coll , args:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: itms))
21.560 + = (P_Model.empty, itms);
21.561 +
21.562 +(*+*)val 4 = length itms;
21.563 +(*+*)val itm = nth 1 itms;
21.564 +
21.565 + coll P_Model.empty [itm];
21.566 +"~~~~~ fun coll , iterate:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: []))
21.567 + = (P_Model.empty, [itm]);
21.568 +
21.569 + (add_sel_ppc thy field model (item_from_feedback thy itm_));
21.570 +"~~~~~ fun add_sel_ppc , args:"; val ((_: theory), sel, {Given = gi, Where = wh, Find = fi, With = wi, Relate = re}, x )
21.571 + = (thy, field, model, (item_from_feedback thy itm_));
21.572 +
21.573 + P_Model.item_from_feedback thy itm_;
21.574 +"~~~~~ fun item_from_feedback , args:"; val (thy, (I_Model.Inc ((d, ts), _))) = (thy, itm_);
21.575 + P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)));
21.576 +(*\\------------------ step into TESTg_form ------------------------------------------------//*)
21.577 +(*\------------------- step into me Model_Problem ------------------------------------------//*)
21.578 +val (p, _, f, nxt, _, pt) = return_me_Model_Problem
21.579 +
21.580 +(*-------------------- contine me's ----------------------------------------------------------*)
21.581 +val return_me_add_find_Constants = me nxt p c pt;
21.582 + val Add_Find "Maximum A" = #4 return_me_add_find_Constants;
21.583 +(*/------------------- step into me_add_find_Constants -------------------------------------\\*)
21.584 +"~~~~~ fun me , args:"; val (tac as Add_Given "Constants [r = 7]", p, _(*NEW remove*), pt) =
21.585 + (nxt, p, c, pt);
21.586 + val ctxt = Ctree.get_ctxt pt p
21.587 +(*+*)val PblObj {probl = (1, [1, 2, 3], false, "#Given", Inc
21.588 + ((Const ("Input_Descript.Constants", _), []), _)) :: _, ...} = get_obj I pt (fst p)
21.589 +(*-------------------------------------------^^--*)
21.590 +val return_step_by_tactic = (*case*)
21.591 + Step.by_tactic tac (pt, p) (*of*);
21.592 +(*//------------------ step into Step.by_tactic --------------------------------------------\\*)
21.593 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
21.594 +val Applicable.Yes tac' =
21.595 + (*case*) Specify_Step.check tac (pt, p) (*of*);
21.596 + (*if*) Tactic.for_specify' tac' (*then*);
21.597 +Step_Specify.by_tactic tac' ptp;
21.598 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp);
21.599 +
21.600 + Specify.by_Add_ "#Given" ct (pt, p);
21.601 +"~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, (pt, p));
21.602 + val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
21.603 +(* val (i_model, m_patt) =*)
21.604 + (*if*) p_ = Pos.Met (*else*);
21.605 +val return_by_Add_ =
21.606 + (pbl,
21.607 + (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
21.608 +val I_Model.Add i_single =
21.609 + (*case*) I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
21.610 +
21.611 + val i_model' =
21.612 + I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model;
21.613 +"~~~~~ fun add_single , args:"; val (thy, itm, model) =
21.614 + ((Proof_Context.theory_of ctxt), i_single, i_model);
21.615 + fun eq_untouched d (0, _, _, _, itm_) = (d = I_Model.descriptor itm_)
21.616 + | eq_untouched _ _ = false
21.617 + val model' = case I_Model.seek_ppc (#1 itm) model of
21.618 + SOME _ => overwrite_ppc thy itm model (*itm updated in is_notyet_input WN.11.03*)
21.619 +
21.620 +(*||------------------ contine Step.by_tactic ------------------------------------------------*)
21.621 +(*\\------------------ step into Step.by_tactic --------------------------------------------//*)
21.622 +val ("ok", (_, _, ptp)) = return_step_by_tactic;
21.623 +
21.624 + val (pt, p) = ptp;
21.625 + (*case*)
21.626 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
21.627 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
21.628 + (p, ((pt, Pos.e_pos'), []));
21.629 + (*if*) Pos.on_calc_end ip (*else*);
21.630 + val (_, probl_id, _) = Calc.references (pt, p);
21.631 +val _ =
21.632 + (*case*) tacis (*of*);
21.633 + (*if*) probl_id = Problem.id_empty (*else*);
21.634 +
21.635 + switch_specify_solve p_ (pt, ip);
21.636 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
21.637 + (*if*) Pos.on_specification ([], state_pos) (*then*);
21.638 +
21.639 + specify_do_next (pt, input_pos);
21.640 +"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
21.641 + val (_, (p_', tac)) =
21.642 + Specify.find_next_step ptp;
21.643 +"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
21.644 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
21.645 + spec = refs, ...} = Calc.specify_data (pt, pos);
21.646 + val ctxt = Ctree.get_ctxt pt pos;
21.647 +
21.648 +(*+*)val (1, [1, 2, 3], true, "#Given", Cor ((Const ("Input_Descript.Constants", _), ts ), _)) :: _
21.649 + = pbl
21.650 +(*+*)val "[[r = 7]]" = UnparseC.terms @{context} ts;
21.651 +(*-----ML-^------^-HOL*)
21.652 +
21.653 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
21.654 + (*if*) p_ = Pos.Pbl (*then*);
21.655 +
21.656 + for_problem ctxt oris (o_refs, refs) (pbl, met);
21.657 +"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
21.658 + (ctxt, oris, (o_refs, refs), (pbl, met));
21.659 + val cpI = if pI = Problem.id_empty then pI' else pI;
21.660 + val cmI = if mI = MethodC.id_empty then mI' else mI;
21.661 + val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
21.662 + val {model = mpc, ...} = MethodC.from_store ctxt cmI
21.663 +
21.664 + val (preok, _) =
21.665 +Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
21.666 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
21.667 + (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
21.668 +
21.669 + val (_, (env_subst, env_eval)) = Pre_Conds.make_environments model_patt i_model;
21.670 +"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
21.671 + val all_variants =
21.672 + map (fn (_, variants, _, _, _) => variants) i_model
21.673 + |> flat
21.674 + |> distinct op =
21.675 + val variants_separated = map (filter_variants' i_model) all_variants
21.676 + val sums_corr = map (Model_Def.cnt_corrects) variants_separated
21.677 + val sum_variant_s = Model_Def.arrange_args sums_corr (1, all_variants)
21.678 + val (_, max_variant) = hd (*..crude decision, up to improvement *)
21.679 + (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
21.680 + val i_model_max =
21.681 + filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
21.682 + val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
21.683 + val env_model = make_env_model equal_descr_pairs
21.684 + val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
21.685 +
21.686 + val subst_eval_list =
21.687 + make_envs_preconds equal_givens;
21.688 +"~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
21.689 +val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) =>
21.690 + discern_feedback id feedb)
21.691 +val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 1 equal_givens;
21.692 +"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts)))) = (id, feedb);
21.693 +
21.694 + discern_typ id (descr, ts);
21.695 +"~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));
21.696 +(*|------------------- contine me_add_find_Constants -----------------------------------------*)
21.697 +(*\------------------- step into me_add_find_Constants -------------------------------------//*)
21.698 +val (p,_,f,nxt,_,pt) = return_me_add_find_Constants;
21.699 +(*/########################## before destroying elementwise input of lists ##################\* )
21.700 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u]" = nxt;
21.701 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [v]" = nxt;
21.702 +( *\########################## before destroying elementwise input of lists ##################/*)
21.703 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u, v]" = nxt;
21.704 +
21.705 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)" = nxt;
21.706 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" = nxt;
21.707 +val return_me_Add_Relation_SideConditions
21.708 + = me nxt p c pt;
21.709 +(*+*)val (_, _, _, Specify_Theory "Diff_App", _, _) = return_me_Add_Relation_SideConditions; (*###############*)
21.710 +(*/------------------- step into me Add_Relation_SideConditions ----------------------------\\*)
21.711 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
21.712 + val ctxt = Ctree.get_ctxt pt p;
21.713 +(**) val (pt, p) = (**)
21.714 + (**)case(**) Step.by_tactic tac (pt, p) (**)of(**)
21.715 +(**) ("ok", (_, _, ptp)) => ptp (**) ;
21.716 +
21.717 + (*case*)
21.718 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
21.719 +(*//------------------ step into do_next ---------------------------------------------------\\*)
21.720 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
21.721 + = (p, ((pt, Pos.e_pos'), [])) (*of*);
21.722 + (*if*) Pos.on_calc_end ip (*else*);
21.723 + val (_, probl_id, _) = Calc.references (pt, p);
21.724 + (*case*) tacis (*of*);
21.725 + (*if*) probl_id = Problem.id_empty (*else*);
21.726 +
21.727 + Step.switch_specify_solve p_ (pt, ip);
21.728 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
21.729 + (*if*) Pos.on_specification ([], state_pos) (*then*);
21.730 + Step.specify_do_next (pt, input_pos);
21.731 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
21.732 +(*isa------ERROR: Refine_Problem INSTEAD
21.733 + isa2: Specify_Theory "Diff_App"*)
21.734 + val (_, (p_', tac as Specify_Theory "Diff_App")) =
21.735 +(*ERROR------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
21.736 + Specify.find_next_step ptp;
21.737 +"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
21.738 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
21.739 + spec = refs, ...} = Calc.specify_data (pt, pos);
21.740 + val ctxt = Ctree.get_ctxt pt pos;
21.741 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
21.742 + (*if*) p_ = Pos.Pbl (*then*);
21.743 +
21.744 +val ("dummy", (Pbl, tac as Specify_Theory "Diff_App")) =
21.745 +(*ERROR------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
21.746 + for_problem ctxt oris (o_refs, refs) (pbl, met);
21.747 +"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
21.748 + (ctxt, oris, (o_refs, refs), (pbl, met));
21.749 + val cpI = if pI = Problem.id_empty then pI' else pI;
21.750 + val cmI = if mI = MethodC.id_empty then mI' else mI;
21.751 + val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
21.752 + val {model = mpc, ...} = MethodC.from_store ctxt cmI
21.753 +
21.754 +(*+*)val [Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
21.755 + Free ("fixes", _)] = where_
21.756 +
21.757 + val (preok, _) =
21.758 + Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
21.759 +(*///----------------- step into check -------------------------------------------------\\*)
21.760 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
21.761 + (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
21.762 +(*+*)val "[0 < fixes]" = pres |> UnparseC.terms @{context}
21.763 +(*+*)val "[\"(#Given, (Constants, fixes))\", \"(#Find, (Maximum, maxx))\", \"(#Find, (AdditionalValues, vals))\", \"(#Relate, (Extremum, extr))\", \"(#Relate, (SideConditions, sideconds))\"]"
21.764 +(*+*) = model_patt |> Model_Pattern.to_string @{context}
21.765 +(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]"
21.766 + = i_model |> I_Model.to_string_TEST @{context}
21.767 +
21.768 +val return_make_environments as (_, (env_subst, env_eval)) =
21.769 + Pre_Conds.make_environments model_patt i_model
21.770 +
21.771 +(*+*)val [(Free ("fixes", T1), Free ("r", T2))] = env_subst (*?!? Const*)
21.772 +(*+*)val Type ("Real.real", []) = T1
21.773 +(*+*)val Type ("Real.real", []) = T2
21.774 +
21.775 +(*+*)val [(Free ("r", T2), Const ("Num.numeral_class.numeral", _) $ _)] = env_eval
21.776 +(*+*)val Type ("Real.real", []) = T2
21.777 +
21.778 +val (_, (env_subst, env_eval)) = return_make_environments;
21.779 +(*|||----------------- contine check -----------------------------------------------------*)
21.780 + val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
21.781 +
21.782 +(*|||----------------- contine check -----------------------------------------------------*)
21.783 +(*+*)val [(true, Const ("Orderings.ord_class.less", _) $
21.784 + Const ("Groups.zero_class.zero", _) $ Free ("r", _))] = pres_subst
21.785 +
21.786 + val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
21.787 +(*+*)val [(true,
21.788 + Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
21.789 + (Const ("Num.numeral_class.numeral", _) $ _))] = full_subst
21.790 +
21.791 + val evals = map (eval ctxt where_rls) full_subst
21.792 +val return_check_OLD = (foldl and_ (true, map fst evals), pres_subst)
21.793 +(*\\\----------------- step into check -------------------------------------------------\\*)
21.794 +
21.795 + val (preok as true, _) = return_check_OLD
21.796 +(*+---------------^^^^*)
21.797 +(*\\------------------ step into do_next ---------------------------------------------------\\*)
21.798 +(*\------------------- step into me_Add_Relation_SideConditions ----------------------------//*)
21.799 +val (p, _, f, nxt, _, pt) = return_me_Add_Relation_SideConditions
21.800 + val Specify_Theory "Diff_App" = nxt;
21.801 +
21.802 +val return_me_Specify_Theory
21.803 + = me nxt p c pt; val Specify_Problem ["univariate_calculus", "Optimisation"] = #4 return_me_Specify_Theory;
21.804 +(*/------------------- step into me Specify_Theory -----------------------------------------\\*)
21.805 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
21.806 + val ctxt = Ctree.get_ctxt pt p;
21.807 +(* val (pt, p) = *)
21.808 + (*case*) Step.by_tactic tac (pt, p) (*of*);
21.809 +(* ("ok", (_, _, ptp)) => ptp *)
21.810 +val return_Step_by_tactic =
21.811 + Step.by_tactic tac (pt, p);
21.812 +(*//------------------ step into Step_by_tactic --------------------------------------------\\*)
21.813 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
21.814 + (*case*) Specify_Step.check tac (pt, p) (*of*);
21.815 +
21.816 +(*||------------------ contine Step_by_tactic ------------------------------------------------*)
21.817 +(*\\------------------ step into Step_by_tactic --------------------------------------------//*)
21.818 +
21.819 +val ("ok", (_, _, ptp)) = return_Step_by_tactic;
21.820 +(*|------------------- continue me Specify_Theory --------------------------------------------*)
21.821 +
21.822 +val ("ok", (ts as (_, _, _) :: _, _, _)) =
21.823 + (*case*)
21.824 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
21.825 +(*//------------------ step into do_next ---------------------------------------------------\\*)
21.826 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
21.827 + = (p, ((pt, Pos.e_pos'), [])) (*of*);
21.828 + (*if*) Pos.on_calc_end ip (*else*);
21.829 + val (_, probl_id, _) = Calc.references (pt, p);
21.830 +val _ =
21.831 + (*case*) tacis (*of*);
21.832 + (*if*) probl_id = Problem.id_empty (*else*);
21.833 +
21.834 + Step.switch_specify_solve p_ (pt, ip);
21.835 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
21.836 + (*if*) Pos.on_specification ([], state_pos) (*then*);
21.837 +
21.838 + Step.specify_do_next (pt, input_pos);
21.839 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
21.840 + val (_, (p_', tac)) = Specify.find_next_step ptp
21.841 + val ist_ctxt = Ctree.get_loc pt (p, p_);
21.842 + (*case*) tac (*of*);
21.843 +
21.844 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
21.845 +(*+*)val Specify_Theory "Diff_App" = tac;
21.846 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Theory dI), (pt, pos as (_, Pbl)))
21.847 + = (tac, (pt, (p, p_')));
21.848 + val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
21.849 + PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
21.850 + (oris, dI, dI', pI', probl, ctxt)
21.851 + val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
21.852 + val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
21.853 +(*\\------------------ step into do_next ---------------------------------------------------//*)
21.854 +(*\------------------- step into me Specify_Theory -----------------------------------------//*)
21.855 +val (p,_,f,nxt,_,pt) = return_me_Specify_Theory;
21.856 +
21.857 +val return_me_Specify_Problem (* keep for continuing me *)
21.858 + = me nxt p c pt; val Specify_Method ["Optimisation", "by_univariate_calculus"] = #4 return_me_Specify_Problem;
21.859 +\<close> ML \<open>(*/------------- step into me_Specify_Problem ----------------------------------------\\*)
21.860 +(*/------------------- step into me_Specify_Problem ----------------------------------------\\*)
21.861 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
21.862 + val ctxt = Ctree.get_ctxt pt p
21.863 +
21.864 +(** ) val ("ok", (_, _, ptp as (pt, p))) =( **)
21.865 +(**) val return_by_tactic =(**) (*case*)
21.866 + Step.by_tactic tac (pt, p) (*of*);
21.867 +(*//------------------ step into by_tactic -------------------------------------------------\\*)
21.868 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
21.869 +
21.870 + (*case*)
21.871 + Step.check tac (pt, p) (*of*);
21.872 +"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
21.873 + (*if*) Tactic.for_specify tac (*then*);
21.874 +
21.875 +Specify_Step.check tac (ctree, pos);
21.876 +"~~~~~ fun check , args:"; val ((Tactic.Specify_Problem pID), (pt, pos as (p, _)))
21.877 + = (tac, (ctree, pos));
21.878 + val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
21.879 + Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
21.880 + => (oris, dI, pI, dI', pI', itms)
21.881 + val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
21.882 +(*\\------------------ step into by_tactic -------------------------------------------------//*)
21.883 +val ("ok", (_, _, ptp as (pt, p))) = return_by_tactic (* kept for continuing me *);
21.884 +
21.885 + (*case*)
21.886 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
21.887 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
21.888 + (*if*) Pos.on_calc_end ip (*else*);
21.889 + val (_, probl_id, _) = Calc.references (pt, p);
21.890 +val _ =
21.891 + (*case*) tacis (*of*);
21.892 + (*if*) probl_id = Problem.id_empty (*else*);
21.893 +
21.894 + Step.switch_specify_solve p_ (pt, ip);
21.895 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
21.896 + (*if*) Pos.on_specification ([], state_pos) (*then*);
21.897 +
21.898 + Step.specify_do_next (pt, input_pos);
21.899 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
21.900 + val (_, (p_', tac)) = Specify.find_next_step ptp
21.901 + val ist_ctxt = Ctree.get_loc pt (p, p_)
21.902 +val _ =
21.903 + (*case*) tac (*of*);
21.904 +
21.905 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
21.906 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos))
21.907 + = (tac, (pt, (p, p_')));
21.908 +
21.909 +\<close> ML \<open>
21.910 +(**)val return_complete_for =(**)
21.911 +(** ) val (o_model, ctxt, i_model) =( **)
21.912 +Specify_Step.complete_for id (pt, pos);
21.913 +\<close> ML \<open> (*//----------- step into complete_for ----------------------------------------------\\*)
21.914 +(*//------------------ step into complete_for ----------------------------------------------\\*)
21.915 +"~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
21.916 +
21.917 +(*+*)val ["Optimisation", "by_univariate_calculus"] = mID
21.918 +(*OLD* )
21.919 + val {origin = (o_model, _, _), probl = i_prob, ctxt,
21.920 + ...} = Calc.specify_data (ctree, pos);
21.921 + val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
21.922 + val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
21.923 + val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
21.924 +( *---*)
21.925 + val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = met_imod, ctxt,
21.926 + ...} = Calc.specify_data (ctree, pos);
21.927 + val ctxt = Ctree.get_ctxt ctree pos
21.928 + val (dI, _, _) = References.select_input o_refs refs;
21.929 + val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
21.930 + val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
21.931 + val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
21.932 +(*NEW*)
21.933 +\<close> ML \<open>
21.934 +(**)val return_match_itms_oris = (**)
21.935 +(** )val (_, (i_model, _)) = ( **)
21.936 +(*OLD* )
21.937 + M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
21.938 +( *---*)
21.939 + match_itms_oris ctxt o_model' (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST i_prob)
21.940 + (m_patt, where_, where_rls);
21.941 +(*NEW*)
21.942 +\<close> ML \<open> (*///---------- step into match_itms_oris -------------------------------------------\\*)
21.943 +(*///----------------- step into match_itms_oris -------------------------------------------\\*)
21.944 +\<close> ML \<open> (*\<longrightarrow> m-match.sml*)
21.945 +"~~~~~ fun match_itms_oris, args:"; val (ctxt, o_model, (pbl_imod, met_imod), (m_patt, where_, where_rls)) =
21.946 + (ctxt, o_model', (I_Model.OLD_to_TEST i_prob, I_Model.OLD_to_TEST i_prob), (m_patt, where_, where_rls));
21.947 +\<close> ML \<open>
21.948 +(**)val return_fill_method =(**)
21.949 +(** )val met_imod =( **)
21.950 + fill_method o_model (pbl_imod, met_imod) m_patt;
21.951 +\<close> ML \<open> (*////-------- step into fill_method -----------------------------------------------\\*)
21.952 +(*////--------------- step into fill_method -----------------------------------------------\\*)
21.953 +"~~~~~ fun fill_method , args:"; val (o_model, (pbl_imod, met_imod), met_patt) =
21.954 + (o_model, (pbl_imod, met_imod), m_patt);
21.955 +
21.956 + val pbl_max_vnts as [2, 1] = Model_Def.max_variants o_model pbl_imod
21.957 + (*probably pbl/met_imod = [], so take met_patt; if empty return Sup*)
21.958 + val i_from_met = map (fn (_, (descr, _)) => (*order from met_patt*)
21.959 + Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt (*\<longrightarrow> right order for args*)
21.960 +(*+MET: Sup..*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
21.961 + = i_from_met |> I_Model.to_string_TEST @{context}
21.962 +
21.963 + val met_max_vnts as [2, 1] = Model_Def.max_variants o_model i_from_met;
21.964 + val max_vnt as 2 = hd (inter op= pbl_max_vnts met_max_vnts);
21.965 + (*add items from pbl_imod (without overwriting existing items in met_imod)*)
21.966 +
21.967 +val return_add_other = map (
21.968 + add_other max_vnt pbl_imod) i_from_met;
21.969 +\<close> ML \<open> (*/////------- step into add_other -------------------------------------------------\\*)
21.970 +(*/////-------------- step into add_other -------------------------------------------------\\*)
21.971 +"~~~~~ fun add_other_5 , args:"; val (max_vnt, i1_model, (i2, _, bool2, m_field2, (Sup_TEST (descr2, ts2), pos2))) =
21.972 + (max_vnt, pbl_imod, nth 5 i_from_met);
21.973 +\<close> ML \<open>
21.974 +(*+*)val Const ("Input_Descript.FunctionVariable", _) = descr2;
21.975 +\<close> ML \<open>
21.976 +val (_, vnts1, _, _, (feedb1, _)) = (i2, [], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2))
21.977 +\<close> ML \<open>
21.978 +val SOME (descr1 as (Const ("Input_Descript.FunctionVariable", _)) ) =
21.979 + get_dscr' feedb1
21.980 +val true =
21.981 + descr1 = descr2
21.982 +val true =
21.983 + Model_Def.member_vnt vnts1 max_vnt
21.984 +val NONE =
21.985 + find_first (fn (_, vnts1, _, _, (feedb1, _)) => case get_dscr' feedb1 of
21.986 + NONE => false
21.987 + | SOME descr1 => descr1 = descr2 andalso Model_Def.member_vnt vnts1 max_vnt) i1_model
21.988 +\<close> ML \<open>
21.989 +val return_add_other_1 = (i2, [max_vnt], bool2, m_field2, (Sup_TEST (descr2, ts2), pos2))
21.990 +val check as true = return_add_other_1 = nth 5 return_add_other
21.991 +\<close> ML \<open> (*\\\\\------- step into add_other -------------------------------------------------//*)
21.992 +(*\\\\\-------------- step into add_other -------------------------------------------------//*)
21.993 + val i_from_pbl = return_add_other
21.994 +\<close> ML \<open>
21.995 +\<close> ML \<open> (*\\\\--------- step into fill_method -----------------------------------------------//*)
21.996 +(*\\\\---------------- step into fill_method -----------------------------------------------//*)
21.997 +val return_fill_method_step = filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) i_from_met
21.998 +\<close> ML \<open>
21.999 +(*+MET: dropped ALL DUE TO is_empty_single_TEST*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]" =
21.1000 + return_fill_method_step |> I_Model.to_string_TEST @{context}
21.1001 +\<close> ML \<open>
21.1002 +(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
21.1003 + = return_fill_method |> I_Model.to_string_TEST @{context};
21.1004 +\<close> ML \<open>
21.1005 +return_fill_method_step = return_fill_method (*latter is correct, did not investigate further*)
21.1006 +(*\\\----------------- step into match_itms_oris -------------------------------------------//*)
21.1007 +\<close> ML \<open> (*\\\---------- step into match_itms_oris -------------------------------------------//*)
21.1008 +val (_, (i_model, _)) = return_match_itms_oris;
21.1009 +\<close> ML \<open>
21.1010 +\<close> ML \<open>(*||------------ continue. complete_for ------------------------------------------------*)
21.1011 +(*||------------------ continue. complete_for ------------------------------------------------*)
21.1012 + val (o_model, ctxt, i_model) = return_complete_for
21.1013 +\<close> ML \<open>
21.1014 +(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n(0, [2], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
21.1015 + = i_model |> I_Model.to_string_TEST @{context}
21.1016 +\<close> ML \<open>
21.1017 +(*
21.1018 +val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(0 ,[2] ,false ,i_model_empty ,Sup FunctionVariable), \n(0 ,[2] ,false ,i_model_empty ,Sup Input_Descript.Domain), \n(0 ,[2] ,false ,i_model_empty ,Sup ErrorBound), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str)]"
21.1019 + = i_model |> I_Model.to_string @{context}
21.1020 +*)
21.1021 +(*+isa2:MET.Mis* ) val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(7 ,[1] ,false ,#Given ,Mis FunctionVariable funvar), \n(10 ,[1, 2] ,false ,#Given ,Mis Input_Descript.Domain doma), \n(12 ,[1, 2, 3] ,false ,#Given ,Mis ErrorBound err)]" =
21.1022 + i_model |> I_Model.to_string @{context} ( *+isa2*)
21.1023 +\<close> ML \<open> (*\\----------- step into complete_for ----------------------------------------------//*)
21.1024 +(*\\------------------ step into complete_for ----------------------------------------------//*)
21.1025 + val (o_model, ctxt, i_model) = return_complete_for
21.1026 +\<close> ML \<open>
21.1027 +\<close> ML \<open> (*|------------ continue. complete_for ------------------------------------------------*)
21.1028 +(*|------------------- continue. complete_for ------------------------------------------------*)
21.1029 +val return_complete_for_step = (o_model', ctxt', i_model)
21.1030 +\<close> ML \<open>
21.1031 +val (o_model'_step, i_model_step) = (#1 return_complete_for_step, #3 return_complete_for_step)
21.1032 +val (o_model', i_model) = (#1 return_complete_for, #3 return_complete_for)
21.1033 +\<close> ML \<open>
21.1034 +if (o_model'_step, i_model_step) = (o_model', i_model)
21.1035 +then () else error "return_complete_for_step <> return_complete_for";
21.1036 +\<close> ML \<open>(*\------------- step into me Specify_Problem ----------------------------------------//*)
21.1037 +(*\------------------- step into me Specify_Problem ----------------------------------------//*)
21.1038 +val (p,_,f,nxt,_,pt) = return_me_Specify_Problem
21.1039 +
21.1040 +\<close> ML \<open>
21.1041 +val return_me_Specify_Method
21.1042 + = me nxt p c pt; val Add_Given "FunctionVariable b" = #4 return_me_Specify_Method;
21.1043 +(*/------------------- step into me_Specify_Method -----------------------------------------\\*)
21.1044 +\<close> ML \<open>(*/------------- step into me_Specify_Method -----------------------------------------\\*)
21.1045 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
21.1046 +
21.1047 +(*+isa==isa2*)val "[]" =(*+*) get_obj g_met pt (fst p) |> I_Model.to_string @{context}
21.1048 +
21.1049 + val ctxt = Ctree.get_ctxt pt p
21.1050 + val (pt, p) =
21.1051 + case Step.by_tactic tac (pt, p) of
21.1052 + ("ok", (_, _, ptp)) => ptp;
21.1053 +
21.1054 +\<close> ML \<open>
21.1055 +(*quick step into --> me_Specify_Method*)
21.1056 +(*+*)val Specify_Method ["Optimisation", "by_univariate_calculus"] = tac;
21.1057 +(* Step.by_tactic*)
21.1058 +"~~~~~ fun by_tactic , args:"; val () = ();
21.1059 +(* Step.check*)
21.1060 +"~~~~~ fun check , args:"; val () = ();
21.1061 +(*Specify_Step.check (Tactic.Specify_Method*)
21.1062 +"~~~~~ fun check , args:"; val () = ();
21.1063 +(*Specify_Step.complete_for*)
21.1064 +"~~~~~ fun complete_for , args:"; val () = ();
21.1065 +(* M_Match.match_itms_oris*)
21.1066 +"~~~~~ fun match_itms_oris , args:"; val () = ();
21.1067 +\<close> ML \<open>
21.1068 +(*+*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(0 ,[2] ,false ,i_model_empty ,Sup FunctionVariable), \n(0 ,[2] ,false ,i_model_empty ,Sup Input_Descript.Domain), \n(0 ,[2] ,false ,i_model_empty ,Sup ErrorBound), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str)]"
21.1069 + = get_obj g_met pt (fst p) |> I_Model.to_string @{context};
21.1070 +\<close> text \<open>
21.1071 +(*+isa: METHOD.drop* )val"[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str)]" =( *+isaALLcorrect*)
21.1072 +(*+isa2:METHOD.Mis*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(7 ,[1] ,false ,#Given ,Mis FunctionVariable funvar), \n(10 ,[1, 2] ,false ,#Given ,Mis Input_Descript.Domain doma), \n(12 ,[1, 2, 3] ,false ,#Given ,Mis ErrorBound err)]" =(*isa2*)
21.1073 + get_obj g_met pt (fst p) |> I_Model.to_string @ {context};
21.1074 +\<close> ML \<open>
21.1075 +
21.1076 +\<close> ML \<open>
21.1077 + (*case*)
21.1078 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
21.1079 +(*//------------------ step into Step.do_next ----------------------------------------------\\*)
21.1080 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
21.1081 + (*if*) Pos.on_calc_end ip (*else*);
21.1082 + val (_, probl_id, _) = Calc.references (pt, p);
21.1083 +val _ =
21.1084 + (*case*) tacis (*of*);
21.1085 + (*if*) probl_id = Problem.id_empty (*else*);
21.1086 +
21.1087 + Step.switch_specify_solve p_ (pt, ip);
21.1088 +(*///----------------- step into Step.switch_specify_solve ---------------------------------\\*)
21.1089 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
21.1090 + (*if*) Pos.on_specification ([], state_pos) (*then*);
21.1091 +
21.1092 + Step.specify_do_next (pt, input_pos);
21.1093 +(*////---------------- step into Step.specify_do_next --------------------------------------\\*)
21.1094 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
21.1095 +
21.1096 + val (_, (p_', tac)) =
21.1097 + Specify.find_next_step ptp;
21.1098 +"~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
21.1099 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
21.1100 + spec = refs, ...} = Calc.specify_data (pt, pos);
21.1101 + val ctxt = Ctree.get_ctxt pt pos;
21.1102 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
21.1103 + (*if*) p_ = Pos.Pbl (*else*);
21.1104 +
21.1105 +\<close> ML \<open>
21.1106 +(*+*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(0 ,[2] ,false ,i_model_empty ,Sup FunctionVariable), \n(0 ,[2] ,false ,i_model_empty ,Sup Input_Descript.Domain), \n(0 ,[2] ,false ,i_model_empty ,Sup ErrorBound), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str)]"
21.1107 + = met |> I_Model.to_string @{context};
21.1108 +(*isa2* )val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor Constants [r = 7] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor Maximum A , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor AdditionalValues [u, v] , pen2str), \n(4 ,[1, 2, 3] ,true ,#Relate ,Cor Extremum (A = 2 * u * v - u \<up> 2) , pen2str), \n(5 ,[1, 2] ,true ,#Relate ,Cor SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str), \n(7 ,[1] ,false ,#Given ,Mis FunctionVariable funvar), \n(10 ,[1, 2] ,false ,#Given ,Mis Input_Descript.Domain doma), \n(12 ,[1, 2, 3] ,false ,#Given ,Mis ErrorBound err)]"
21.1109 + =( *isa2*) met |> I_Model.to_string @{context};
21.1110 +
21.1111 +\<close> ML \<open>
21.1112 +(*isa2*)val ("dummy", (Met, Add_Given "FunctionVariable b")) =(*isa2*)
21.1113 + Specify.for_method ctxt oris (o_refs, refs) (pbl, met);
21.1114 +(*///// /------------- step into Step.for_method -------------------------------------------\\*)
21.1115 +"~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (_, met))
21.1116 + = (ctxt, oris, (o_refs, refs), (pbl, met));
21.1117 + val cmI = if mI = MethodC.id_empty then mI' else mI;
21.1118 + val {model, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
21.1119 + val (preok, _) = Pre_Conds.check ctxt where_rls where_ (model, I_Model.OLD_to_TEST met);
21.1120 +val NONE =
21.1121 + (*case*) find_first (I_Model.is_error o #5) met (*of*);
21.1122 +
21.1123 +(*isa2*)val SOME ("#Given", "FunctionVariable b") =(*isa2*)
21.1124 + (*case*)
21.1125 + Specify.item_to_add (ThyC.get_theory ctxt
21.1126 + (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
21.1127 +"~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
21.1128 + = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
21.1129 +(*\------------------- step into me_Specify_Method -----------------------------------------//*)
21.1130 +\<close> ML \<open>(*\------------- step into me_Specify_Method -----------------------------------------//*)
21.1131 +
21.1132 +val (p,_,f,nxt,_,pt) = return_me_Specify_Method
21.1133 +
21.1134 +\<close> ML \<open>
21.1135 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Input_Descript.Domain {0<..<r}" = nxt;
21.1136 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "ErrorBound (\<epsilon> = 0)" = nxt;
21.1137 +
21.1138 +
21.1139 +\<close> ML \<open>
21.1140 +\<close>
21.1141 +
21.1142 +(*ML_file "Minisubpbl/biegel ? ? ?.sml"*)
21.1143 +section \<open>===================================================================================\<close>
21.1144 +section \<open>===== ===========================================================================\<close>
21.1145 ML \<open>
21.1146 \<close> ML \<open>
21.1147