1.1 --- a/src/Tools/isac/Build_Isac.thy Wed Sep 20 16:51:08 2023 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Sun Sep 24 20:04:41 2023 +0200
1.3 @@ -181,11 +181,16 @@
1.4 As next step we go bottom up from Thy_Info.get_theory and remove it.
1.5 Afterwards $ISABELLE_ISAC_TEST will be changed accordingly.
1.6 \<close>
1.7 -(**) (* evaluated in Test_Isac/_Short * )
1.8 +(**) (* evaluated in Test_Isac/_Short *)
1.9 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/000-comments.sml"
1.10 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/100-init-rootpbl.sml"
1.11 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml"
1.12 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/150-add-given-Equation.sml"
1.13 +ML \<open>
1.14 +\<close> ML \<open>
1.15 +
1.16 +\<close> ML \<open>
1.17 +\<close>
1.18 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml"
1.19 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/200-start-method.sml"
1.20 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method-NEXT_STEP.sml"
1.21 @@ -216,13 +221,7 @@
1.22 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/calculation.sml"
1.23 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/vscode-example.sml"
1.24
1.25 -( * evaluated in Test_Isac/_Short *)
1.26 -ML \<open>
1.27 -\<close> ML \<open>
1.28 -\<close> ML \<open>
1.29 -\<close> ML \<open>
1.30 -\<close> ML \<open>
1.31 -\<close>
1.32 +(* evaluated in Test_Isac/_Short *)
1.33
1.34 section \<open>check presence of definitions from directories\<close>
1.35
2.1 --- a/src/Tools/isac/MathEngBasic/model-def.sml Wed Sep 20 16:51:08 2023 +0200
2.2 +++ b/src/Tools/isac/MathEngBasic/model-def.sml Sun Sep 24 20:04:41 2023 +0200
2.3 @@ -47,9 +47,14 @@
2.4 val i_model_empty : i_model_single
2.5 val i_model_empty_TEST: i_model_single_TEST
2.6
2.7 +(*T_TESTold* )
2.8 val max_variants: i_model_TEST -> variant list * i_model_TEST list
2.9 +( *T_TEST*)
2.10 + val max_variants: o_model -> i_model_TEST -> variants
2.11 +(*T_TESTnew*)
2.12
2.13 (*from isac_test for Minisubpbl*)
2.14 + val all_variants: ('a * variants * 'c * 'd * 'e) list -> variants
2.15 val filter_variants': i_model_TEST -> variant -> i_model_TEST
2.16 val cnt_corrects: i_model_TEST -> int
2.17 val arrange_args: int list -> int * variant list -> (int * variant) list
2.18 @@ -133,6 +138,10 @@
2.19
2.20 (** max_variants **)
2.21
2.22 +fun all_variants model =
2.23 + map (fn (_, variants, _, _, _) => variants) model
2.24 + |> flat
2.25 + |> distinct op =
2.26 fun filter_variants' i_singles n =
2.27 filter (fn (_, variants, _, _, _) => member op= variants n) i_singles
2.28 fun cnt_corrects i_model =
2.29 @@ -140,6 +149,7 @@
2.30 fun arrange_args [] _ = []
2.31 | arrange_args (sum :: ss) (cnt, all) = (sum, nth cnt all) :: (arrange_args ss (cnt + 1, all))
2.32
2.33 +(*T_TESTold* )
2.34 fun max_variants i_model =
2.35 let
2.36 val all_variants =
2.37 @@ -163,6 +173,29 @@
2.38 in
2.39 (maxes, max_i_models)
2.40 end
2.41 +( *T_TEST*)
2.42 +(*in case of i_model max_variants = [] we take of o_model all_variants *)
2.43 +fun max_variants o_model i_model =
2.44 + let
2.45 + val all_variants =
2.46 + map (fn (_, variants, _, _, _) => variants) i_model
2.47 + |> flat
2.48 + |> distinct op =
2.49 + val variants_separated = map (filter_variants' i_model) all_variants
2.50 + val sums_corr = map (cnt_corrects) variants_separated
2.51 + val sum_variant_s = arrange_args sums_corr (1, all_variants)
2.52 +
2.53 + val max_first = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
2.54 + val maxes = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
2.55 + |> map snd
2.56 + in
2.57 + if maxes = []
2.58 + then map (fn (_, variants, _, _, _) => variants) o_model
2.59 + |> flat
2.60 + |> distinct op =
2.61 + else maxes
2.62 + end
2.63 +(*T_TESTnew*)
2.64
2.65
2.66 (** definitions for O_Model.T **)
3.1 --- a/src/Tools/isac/Specify/i-model.sml Wed Sep 20 16:51:08 2023 +0200
3.2 +++ b/src/Tools/isac/Specify/i-model.sml Sun Sep 24 20:04:41 2023 +0200
3.3 @@ -66,7 +66,9 @@
3.4 T_TEST * T_TEST
3.5 (*^^^--- s_make_complete SHALL REPLACE ALL THESE ---vvv*)
3.6 val complete: O_Model.T -> (*Problem*)T -> (*MethodC*)T -> Model_Pattern.T -> T
3.7 +(*
3.8 val complete_method: O_Model.T * Model_Pattern.T * Model_Pattern.T * T -> T * T
3.9 +*)
3.10 val complete': Model_Pattern.T -> O_Model.single -> single
3.11 val fill_method: O_Model.T -> T_TEST -> Model_Pattern.T -> T_TEST
3.12
3.13 @@ -417,7 +419,7 @@
3.14
3.15 (*
3.16 Survey on completion of i-models.
3.17 - one most general version, , shall replace all old versions
3.18 + one most general version, I_Model.s_make_complete, shall replace all old versions
3.19
3.20 Divide functionality of I_Model.of_max_variant into parts in order for re-use in is_complete
3.21 I_Model.max_variants
3.22 @@ -535,7 +537,7 @@
3.23 (i, vnts, true, m_field, (Cor_TEST (descr, ts), Position.none))
3.24 fun fill_method o_model pbl_imod met_patt =
3.25 let
3.26 - val (pbl_max_vnts, _) = Model_Def.max_variants pbl_imod;
3.27 + val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
3.28 val from_pbl = map (fn (_, (descr, _)) =>
3.29 Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) met_patt
3.30 val from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
3.31 @@ -562,7 +564,7 @@
3.32
3.33 fun s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt) =
3.34 let
3.35 - val (pbl_max_vnts, _) = Model_Def.max_variants pbl_imod;
3.36 + val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
3.37 val i_from_pbl = map (fn (_, (descr, _)) =>
3.38 Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt
3.39 val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
3.40 @@ -574,19 +576,20 @@
3.41 else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
3.42
3.43 val i_from_met = map (fn (_, (descr, _)) =>
3.44 - (Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod)) met_patt
3.45 - val (met_max_vnts, _) = Model_Def.max_variants i_from_met;
3.46 - val met_max_vnt = hd met_max_vnts (*need only one for solve-phase*)
3.47 + Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt
3.48 + val met_max_vnts = Model_Def.max_variants o_model i_from_met;
3.49 + val max_vnt = hd met_max_vnts (*need only one for solve-phase*)
3.50
3.51 val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
3.52 if is_empty_single_TEST i_single
3.53 then
3.54 - case Pre_Conds.get_descr_vnt' feedb [met_max_vnt] o_model of
3.55 - [] => raise ERROR (msg [met_max_vnt] feedb)
3.56 + case Pre_Conds.get_descr_vnt' feedb [max_vnt] o_model of
3.57 + [] => raise ERROR (msg [max_vnt] feedb)
3.58 | o_singles => map transfer_terms o_singles
3.59 else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
3.60 in
3.61 - (pbl_from_o_model, met_from_pbl)
3.62 + (filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) pbl_from_o_model,
3.63 + met_from_pbl)
3.64 end
3.65
3.66 (**)end(**);
4.1 --- a/src/Tools/isac/Specify/pre-conditions.sml Wed Sep 20 16:51:08 2023 +0200
4.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml Sun Sep 24 20:04:41 2023 +0200
4.3 @@ -177,10 +177,11 @@
4.4 (i.e. was not transferred pbl_mod by \<open>fun get_descr_vnt\<close>).
4.5 *)
4.6 fun get_descr_vnt' feedb vnts o_model =
4.7 - filter (fn (_, vnts', _, descr', _) =>
4.8 - case get_dscr' feedb of
4.9 - SOME descr => if descr' = descr andalso inter op= vnts' vnts <> [] then true else false
4.10 - | NONE => false) o_model
4.11 + filter (fn (_, vnts', _, descr', _) =>
4.12 + case get_dscr' feedb of
4.13 + SOME descr => if descr' = descr andalso inter op= vnts' vnts <> []
4.14 + then true else false
4.15 + | NONE => false) o_model
4.16
4.17 (* all_lhs_atoms: term list -> bool*)
4.18 fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>
4.19 @@ -329,7 +330,7 @@
4.20 fun environment_TEST model_patt i_model = of_max_variant model_patt i_model |> #2
4.21
4.22 (** check pre-conditions **)
4.23 -
4.24 +(*OLD*)
4.25 fun check_pos ctxt where_rls where_POS (model_patt, i_model) =
4.26 let
4.27 val (_, _, (_, env_eval)) = of_max_variant model_patt
4.28 @@ -342,6 +343,20 @@
4.29 in
4.30 (foldl and_ (true, map (fn ((bool, _: term), _: Position.T) => bool) evals), display)
4.31 end;
4.32 +(*---* )
4.33 +fun check_pos ctxt where_rls where_POS (model_patt, i_model) =
4.34 + let
4.35 + val (_, (_, env_eval)) = make_environments model_patt
4.36 + (filter (fn (_, _, _, m_field ,_) => m_field = "#Given") i_model)
4.37 + val full_subst = if env_eval = []
4.38 + then map (fn (t, pos) => ((true, t), pos)) where_POS
4.39 + else map (fn (t, pos) => (TermC.subst_atomic_all env_eval t, pos)) where_POS;
4.40 + val evals = map (fn ((bool_t), pos) => (eval ctxt where_rls bool_t, pos)) full_subst;
4.41 + val display = map (fn ((t, pos), ((bool, _), _)) => (bool, (t, pos))) (where_POS ~~ evals)
4.42 + in
4.43 + (foldl and_ (true, map (fn ((bool, _: term), _: Position.T) => bool) evals), display)
4.44 + end;
4.45 +( *NEW*)
4.46
4.47 (*takes the envs resulting from of_max_variant*)
4.48 fun check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval)) =
5.1 --- a/src/Tools/isac/Specify/specify.sml Wed Sep 20 16:51:08 2023 +0200
5.2 +++ b/src/Tools/isac/Specify/specify.sml Sun Sep 24 20:04:41 2023 +0200
5.3 @@ -192,16 +192,20 @@
5.4 val _ = if p_ <> Pos.Pbl
5.5 then raise ERROR ("###finish_phase: only impl.for Pbl, called with " ^ Pos.pos'2str pos)
5.6 else ()
5.7 - val (oris, ospec, probl, spec) = case Ctree.get_obj I pt p of
5.8 - Ctree.PblObj {origin = (oris, ospec, _), probl, spec, ...} => (oris, ospec, probl, spec)
5.9 + val (oris, ospec, probl, spec, meth) = case Ctree.get_obj I pt p of
5.10 + Ctree.PblObj {origin = (oris, ospec, _), probl, spec, meth, ...} => (oris, ospec, probl, spec, meth)
5.11 | _ => raise ERROR "finish_phase: unvered case get_obj"
5.12 val (_, pI, mI) = References.select_input ospec spec
5.13 val ctxt = Ctree.get_ctxt pt pos
5.14 val mpc = (#model o MethodC.from_store ctxt) mI
5.15 val model = (#model o Problem.from_store ctxt) pI
5.16 +(*OLD* )
5.17 val (pits, mits) = I_Model.complete_method (oris, mpc, model, probl)
5.18 - val pt = Ctree.update_pblppc pt p pits
5.19 - val pt = Ctree.update_metppc pt p mits
5.20 +( *---*)
5.21 + val (pits, mits) = I_Model.s_make_complete oris (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (model, mpc)
5.22 +(*NEW*)
5.23 + val pt = Ctree.update_pblppc pt p (I_Model.TEST_to_OLD pits)
5.24 + val pt = Ctree.update_metppc pt p (I_Model.TEST_to_OLD mits)
5.25 in (pt, (p, Pos.Met)) end
5.26
5.27 (*
6.1 --- a/src/Tools/isac/Specify/step-specify.sml Wed Sep 20 16:51:08 2023 +0200
6.2 +++ b/src/Tools/isac/Specify/step-specify.sml Sun Sep 24 20:04:41 2023 +0200
6.3 @@ -24,18 +24,25 @@
6.4
6.5 fun by_tactic_input (tac as Tactic.Model_Problem) (pt, pos as (p, _)) =
6.6 let
6.7 - val (oris, ospec, probl, spec, ctxt) = case get_obj I pt p of
6.8 - PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} => (oris, ospec, probl, spec, ctxt)
6.9 + val (oris, ospec, probl, spec, ctxt, meth) = case get_obj I pt p of
6.10 + PblObj {origin = (oris, ospec, _), probl, spec, ctxt, meth, ...} => (oris, ospec, probl, spec, ctxt, meth)
6.11 | _ => raise ERROR "by_tactic_input Model_Problem; uncovered case get_obj"
6.12 val (_, pI, mI) = References.select_input ospec spec
6.13 val mpc = (#model o MethodC.from_store ctxt) mI (* just for reuse I_Model.complete_method *)
6.14 val {cas, model, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
6.15 +(*OLD* )
6.16 val pbl = I_Model.init model (* fill in descriptions *)
6.17 +( *---*)
6.18 + val pbl = I_Model.init_TEST oris model (* fill in descriptions *)
6.19 +(*NEW*)
6.20 val (pbl, met) = case cas of
6.21 NONE => (pbl, [])
6.22 +(*OLD* )
6.23 | _ => I_Model.complete_method (oris, mpc, model, probl)
6.24 - (*----------------------------------------------------------------*)
6.25 - val tac_ = Tactic.Model_Problem' (pI, pbl, met)
6.26 +( *---*)
6.27 + | _ => I_Model.s_make_complete oris (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (model, mpc)
6.28 +(*NEW*)
6.29 + val tac_ = Tactic.Model_Problem' (pI, I_Model.TEST_to_OLD pbl, I_Model.TEST_to_OLD met)
6.30 val (pos,c,_,pt) = Specify_Step.add tac_ (Istate_Def.Uistate, ctxt) (pt, pos)
6.31 in
6.32 ("ok",([(tac, tac_, (pos, (Istate_Def.Uistate, ContextC.empty)))], c, (pt,pos)))
7.1 --- a/test/Tools/isac/Knowledge/biegelinie-4.sml Wed Sep 20 16:51:08 2023 +0200
7.2 +++ b/test/Tools/isac/Knowledge/biegelinie-4.sml Sun Sep 24 20:04:41 2023 +0200
7.3 @@ -219,10 +219,14 @@
7.4 = Step.specify_do_next ptp;
7.5 val ("ok", ([(Add_Find "Biegelinie y", _, _)], _, ptp))
7.6 = Step.specify_do_next ptp;
7.7 +(*/---broken elementwise input to lists---\* )
7.8 val ("ok", ([(Add_Relation "Randbedingungen [y 0 = 0]", _, _)], _, ptp))
7.9 = Step.specify_do_next ptp;
7.10 val ("ok", ([(Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]", _, _)], _, ptp))
7.11 = Step.specify_do_next ptp;
7.12 +( *\---broken elementwise input to lists---/*)
7.13 +val ("ok", ([(Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]", _, _)], _, ptp))
7.14 + = Step.specify_do_next ptp;
7.15
7.16 (*** Problem model is complete ============================================================ ***)
7.17 val PblObj {probl, ...} = get_obj I (fst ptp) [];
8.1 --- a/test/Tools/isac/MathEngine/mathengine-stateless.sml Wed Sep 20 16:51:08 2023 +0200
8.2 +++ b/test/Tools/isac/MathEngine/mathengine-stateless.sml Sun Sep 24 20:04:41 2023 +0200
8.3 @@ -13,7 +13,6 @@
8.4 "----------- change to TermC.parse ctxt -----------------------";
8.5 "----------- tryrefine ----------------------------------";
8.6 "----------- search for Or_to_List ----------------------";
8.7 -"----------- check thy in Test_Code.init_calc @{context} ------------------";
8.8 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
8.9 "----------- improved fun getTactic for interSteps and numeral calculations --";
8.10 "--------------------------------------------------------";
8.11 @@ -93,60 +92,6 @@
8.12 | _ => error "Or_to_List broken ?"
8.13
8.14
8.15 -"----------- check thy in Test_Code.init_calc @{context} ------------------";
8.16 -"----------- check thy in Test_Code.init_calc @{context} ------------------";
8.17 -"----------- check thy in Test_Code.init_calc @{context} ------------------";
8.18 -"WN1109 with Inverse_Z_Transform.thy when starting tests with Test_Code.init_calc @{context} \n" ^
8.19 -"we got the message: ME_Isa: thy 'Build_Inverse_Z_Transform' not in system \n" ^
8.20 -"Below there are the steps which found out the reason: \n" ^
8.21 -"store_pbt mistakenly stored that theory.";
8.22 -val ctxt = Proof_Context.init_global @{theory Isac_Knowledge};
8.23 -val SOME t = ParseC.term_opt ctxt "filterExpression (X = 3 / (z - 1/4 + - 1/8 * (1/(z::real))))";
8.24 -val SOME t = ParseC.term_opt ctxt "stepResponse (x[n::real]::bool)";
8.25 -
8.26 -val fmz = ["filterExpression (X = 3 / (z - 1/4 + - 1/8 * (1/(z::real))))", "boundVariable z",
8.27 - "stepResponse (x[n::real]::bool)"];
8.28 -val (dI,pI,mI) = ("Isac_Knowledge", ["Inverse", "Z_Transform", "SignalProcessing"],
8.29 - ["SignalProcessing", "Z_Transform", "Inverse"]);
8.30 -
8.31 -val (p,_,fb,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI,pI,mI))];
8.32 -(*WAS ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
8.33 -(*old* )val ctxt = thy_id |> ThyC.get_theory ctxt |> Proof_Context.init_global
8.34 -( *new*)val thy = thy_id |> ThyC.get_theory ctxt (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*);
8.35 -
8.36 -"~~~~~ fun init_calc @{context} , args:"; val [(fmz, sp):Formalise.T] = [(fmz, (dI,pI,mI))];
8.37 - (*val ((pt, p), tacis) =*)
8.38 -Step_Specify.initialise' thy (fmz, sp);
8.39 -"~~~~~ fun initialise' , args:"; val (fmz, (dI, pI, mI)) = (fmz, sp);
8.40 - (*val (_, hdl, (dI, pI, mI), pors, pctxt) =*)
8.41 -Step_Specify.initialise thy (fmz, (dI, pI, mI));
8.42 -"~~~~~ fun initialise , args:"; val (fmz, (dI, pI, mI)) = (fmz, (dI, pI, mI));
8.43 - val thy = ThyC.get_theory @{context} dI
8.44 - val ctxt = Proof_Context.init_global thy;
8.45 - (*if*) mI = ["no_met"](*else*);
8.46 - val (pors, pctxt) = Problem.from_store ctxt pI |> #model |> O_Model.init thy fmz;
8.47 - val {cas, model, thy=thy',...} = Problem.from_store ctxt pI; (*take dI from _refined_ pbl*)
8.48 - "tracing bottom up"; Context.theory_name thy' = "Build_Inverse_Z_Transform"; (*WAS true*)
8.49 - val dI = Context.theory_name (ThyC.parent_of thy thy');
8.50 -"tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
8.51 - cas = NONE; (*true*)
8.52 - val hdl = pblterm dI pI;
8.53 - val (pt, _) = cappend_problem e_ctree [] (Istate.empty, pctxt) (fmz, (dI, pI, mI))
8.54 - (pors, (dI, pI, mI), hdl, ContextC.empty)
8.55 -;
8.56 -"~~~~~ fun Step_Specify.by_tactic_input, args:"; val ((tac as Model_Problem), (pt, pos as (p,p_))) = (Model_Problem, (pt, ([], Pbl)));
8.57 - val PblObj {origin = (oris, ospec, _), probl, spec, ctxt, ...} = get_obj I pt p;
8.58 -"tracing bottom up"; #1(ospec) = "Build_Inverse_Z_Transform"; (*WAS true*)
8.59 -
8.60 -"~~~~~ fun References.select_input, args:"; val ((odI, opI, omI), (dI, pI, mI)) = (ospec, spec);
8.61 -dI = ThyC.id_empty; (*true*)
8.62 -odI = "Build_Inverse_Z_Transform"; (*true*)
8.63 -dI = ThyC.id_empty; (*true*)
8.64 -"~~~~~ after fun References.select_input:";
8.65 - val (dI, pI, mI) = References.select_input ospec spec;
8.66 -"tracing bottom up"; dI = "Build_Inverse_Z_Transform"; (*WAS true*)
8.67 - val thy = ThyC.get_theory @{context} dI; (*caused ME_Isa: thy 'Build_Inverse_Z_Transform' not in system*)
8.68 -
8.69 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
8.70 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
8.71 "----------- identified error in fun getTactic, ThmC.string_of_thm ---------------";
9.1 --- a/test/Tools/isac/MathEngine/step.sml Wed Sep 20 16:51:08 2023 +0200
9.2 +++ b/test/Tools/isac/MathEngine/step.sml Sun Sep 24 20:04:41 2023 +0200
9.3 @@ -292,14 +292,23 @@
9.4 = Step.specify_do_next ptp;
9.5 val ("ok", ([(Add_Find "maximum A", _, _)], _, ptp))
9.6 = Step.specify_do_next ptp;
9.7 +(*/---broken elementwise input to lists---\* )
9.8 val ("ok", ([(Add_Find "valuesFor [a]", _, _)], _, ptp))
9.9 = Step.specify_do_next ptp;
9.10 val ("ok", ([(Add_Find "valuesFor [b]", _, _)], _, ptp))
9.11 = Step.specify_do_next ptp;
9.12 +( *\---broken elementwise input to lists---/*)
9.13 +val ("ok", ([(Add_Find "valuesFor [a, b]", _, _)], _, ptp))
9.14 + = Step.specify_do_next ptp;
9.15 +
9.16 +(*/---broken elementwise input to lists---\* )
9.17 val ("ok", ([(Add_Relation "relations [A = a * b]", _, _)], _, ptp))
9.18 = Step.specify_do_next ptp;
9.19 val ("ok", ([(Add_Relation "relations [(a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]", _, _)], _, ptp))
9.20 = Step.specify_do_next ptp;
9.21 +( *\---broken elementwise input to lists---/*)
9.22 +val ("ok", ([(Add_Relation "relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2]", _, _)], _, ptp))
9.23 + = Step.specify_do_next ptp;
9.24
9.25 (*** Problem model is complete ============================================================ ***)
9.26 val PblObj {probl, ...} = get_obj I (fst ptp) [];
10.1 --- a/test/Tools/isac/Specify/i-model.sml Wed Sep 20 16:51:08 2023 +0200
10.2 +++ b/test/Tools/isac/Specify/i-model.sml Sun Sep 24 20:04:41 2023 +0200
10.3 @@ -353,7 +353,7 @@
10.4 (*/------------------- step into s_make_complete -------------------------------------------\\*)
10.5 "~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt)) =
10.6 (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt));
10.7 - val (pbl_max_vnts, _) = Model_Def.max_variants pbl_imod;
10.8 + val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
10.9 val i_from_pbl = map (fn (_, (descr, _)) =>
10.10 Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;
10.11
10.12 @@ -421,7 +421,7 @@
10.13 "(0, [], false ,i_model_empty, (Sup_TEST AdditionalValues [], Position.T))]"
10.14 (*+*)then () else error "s_make_complete: from_met CHANGED";
10.15 ;
10.16 - val (met_max_vnts, _) = Model_Def.max_variants i_from_met;
10.17 + val met_max_vnts = Model_Def.max_variants o_model i_from_met;
10.18 (*+*)val [2] = met_max_vnts
10.19
10.20 val met_max_vnt = hd met_max_vnts (*need only one for solve-phase*)
11.1 --- a/test/Tools/isac/Specify/sub-problem.sml Wed Sep 20 16:51:08 2023 +0200
11.2 +++ b/test/Tools/isac/Specify/sub-problem.sml Sun Sep 24 20:04:41 2023 +0200
11.3 @@ -71,11 +71,12 @@
11.4 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Given "Streckenlast q_0"*)
11.5 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Find "Biegelinie y" = tac
11.6
11.7 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Relation "Randbedingungen [y 0 = 0]"*)
11.8 -(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*\<rightarrow>Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]"*)
11.9 (*/---broken elementwise input to lists---\* )
11.10 -? ? ?
11.11 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Relation "Randbedingungen [y 0 = 0]" = tac
11.12 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Relation "Randbedingungen [y L = 0, M_b 0 = 0, M_b L = 0]" = tac
11.13 ( *\---broken elementwise input to lists---/*)
11.14 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Add_Relation "Randbedingungen [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0]" = tac
11.15 +
11.16 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Theory "Biegelinie" = tac
11.17 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Problem ["Biegelinien"] = tac
11.18 (*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Method ["IntegrierenUndKonstanteBestimmen2"] = tac
12.1 --- a/test/Tools/isac/Test_Theory.thy Wed Sep 20 16:51:08 2023 +0200
12.2 +++ b/test/Tools/isac/Test_Theory.thy Sun Sep 24 20:04:41 2023 +0200
12.3 @@ -96,6 +96,7 @@
12.4 (**)
12.5 \<close> ML \<open>
12.6 \<close> ML \<open> (*\<longrightarrow> pre_conditions.sml | ? model-def.sml ?*)
12.7 +(*T_TESTold* )
12.8 fun max_variants i_model =
12.9 let
12.10 val all_variants =
12.11 @@ -146,6 +147,32 @@
12.12 (*of_max_variant*)
12.13 max_variants: (*Model_Pattern.T -> *) Model_Def.i_model_TEST ->
12.14 (variant list * Model_Def.i_model_TEST list)(* * Env.T * (env_subst * env_eval)*)
12.15 +;
12.16 +( *T_TEST*)
12.17 +(*in case of i_model max_variants = [] we take of o_model all_variants *)
12.18 +fun max_variants o_model i_model =
12.19 + let
12.20 + val all_variants =
12.21 + map (fn (_, variants, _, _, _) => variants) i_model
12.22 + |> flat
12.23 + |> distinct op =
12.24 + val variants_separated = map (filter_variants' i_model) all_variants
12.25 + val sums_corr = map (cnt_corrects) variants_separated
12.26 + val sum_variant_s = arrange_args sums_corr (1, all_variants)
12.27 +
12.28 + val max_first = rev (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
12.29 + val maxes = filter (fn (cnt, _) => curry op = (fst (hd max_first)) cnt) max_first
12.30 + |> map snd
12.31 + in
12.32 + if maxes = []
12.33 + then map (fn (_, variants, _, _, _) => variants) o_model
12.34 + |> flat
12.35 + |> distinct op =
12.36 + else maxes
12.37 + end
12.38 +;
12.39 + max_variants: Model_Def.o_model -> Model_Def.i_model_TEST -> variants
12.40 +(*T_TESTnew*)
12.41 \<close> ML \<open>
12.42 \<close> ML \<open> (*\<longrightarrow> pre-conditions.sml*)
12.43 \<close> ML \<open>
12.44 @@ -189,10 +216,11 @@
12.45 (i.e. was not transferred pbl_mod by \<open>fun get_descr_vnt\<close>).
12.46 *)
12.47 fun get_descr_vnt' feedb vnts o_model =
12.48 - filter (fn (_, vnts', _, descr', _) =>
12.49 - case get_dscr' feedb of
12.50 - SOME descr => if descr' = descr andalso inter op= vnts' vnts <> [] then true else false
12.51 - | NONE => false) o_model
12.52 + filter (fn (_, vnts', _, descr', _) =>
12.53 + case get_dscr' feedb of
12.54 + SOME descr => if descr' = descr andalso inter op= vnts' vnts <> []
12.55 + then true else false
12.56 + | NONE => false) o_model
12.57 ;
12.58 get_descr_vnt': feedback_TEST -> variants -> O_Model.T -> O_Model.T
12.59 \<close> ML \<open>
12.60 @@ -204,7 +232,7 @@
12.61 \<close> ML \<open>
12.62 fun fill_method o_model pbl_imod met_patt =
12.63 let
12.64 - val (pbl_max_vnts, _) = max_variants pbl_imod;
12.65 + val pbl_max_vnts = max_variants o_model pbl_imod;
12.66 val from_pbl = map (fn (_, (descr, _)) => get_descr_vnt descr pbl_max_vnts pbl_imod) met_patt
12.67 val from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
12.68 if is_empty_single_TEST i_single
12.69 @@ -224,9 +252,9 @@
12.70 \<close> ML \<open>
12.71 fun s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt) =
12.72 let
12.73 - val (pbl_max_vnts, _) = Model_Def.max_variants pbl_imod;
12.74 + val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
12.75 val i_from_pbl = map (fn (_, (descr, _)) =>
12.76 - (*Pre_Conds.*)get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt
12.77 + Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;
12.78 val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
12.79 if is_empty_single_TEST i_single
12.80 then
12.81 @@ -236,19 +264,20 @@
12.82 else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
12.83
12.84 val i_from_met = map (fn (_, (descr, _)) =>
12.85 - (*Pre_Conds.*)get_descr_vnt descr pbl_max_vnts met_imod) met_patt
12.86 - val (met_max_vnts, _) = Model_Def.max_variants i_from_met;
12.87 - val met_max_vnt = hd met_max_vnts (*need only one for solve-phase*)
12.88 + Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt
12.89 + val met_max_vnts = Model_Def.max_variants o_model i_from_met;
12.90 + val max_vnt = hd met_max_vnts (*need only one for solve-phase*)
12.91
12.92 val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
12.93 if is_empty_single_TEST i_single
12.94 then
12.95 - case get_descr_vnt' feedb [met_max_vnt] o_model of
12.96 - [] => raise ERROR (msg [met_max_vnt] feedb)
12.97 + case get_descr_vnt' feedb [max_vnt] o_model of
12.98 + [] => raise ERROR (msg [max_vnt] feedb)
12.99 | o_singles => map transfer_terms o_singles
12.100 else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
12.101 in
12.102 - (pbl_from_o_model, met_from_pbl)
12.103 + (filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) pbl_from_o_model,
12.104 + met_from_pbl)
12.105 end
12.106 \<close> ML \<open>
12.107 ;
12.108 @@ -256,6 +285,9 @@
12.109 I_Model.T_TEST * I_Model.T_TEST
12.110 \<close> ML \<open>
12.111 \<close> ML \<open>
12.112 +I_Model.init
12.113 +\<close> ML \<open>
12.114 +I_Model.init_TEST
12.115 \<close> ML \<open>
12.116 \<close> ML \<open> (*\<longrightarrow> lucas-interpreter.sml*)
12.117 fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
12.118 @@ -353,14 +385,13 @@
12.119 s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt);
12.120 \<close> ML \<open> (*/------------ step into s_make_complete -------------------------------------------\\*)
12.121 (*/------------------- step into s_make_complete -------------------------------------------\\*)
12.122 -(*.....~~~ fill_method....*)
12.123 "~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt)) =
12.124 (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt));
12.125 \<close> ML \<open>
12.126 - val (pbl_max_vnts, _) = Model_Def.max_variants pbl_imod;
12.127 + val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
12.128 \<close> ML \<open>
12.129 val i_from_pbl = map (fn (_, (descr, _)) =>
12.130 - (*Pre_Conds.*)get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;
12.131 + Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;
12.132 \<close> ML \<open> (*//----------- step into get_descr_vnt ---------------------------------------------\\*)
12.133 (*//------------------ step into get_descr_vnt ---------------------------------------------\\*)
12.134 "~~~~~ fun get_descr_vnt , args:"; val (descr, vnts, i_model) =
12.135 @@ -423,7 +454,7 @@
12.136 (*|------------------- continue s_make_complete ----------------------------------------------*)
12.137 \<close> ML \<open>
12.138 val i_from_met = map (fn (_, (descr, _)) =>
12.139 - (*Pre_Conds.*)get_descr_vnt descr pbl_max_vnts met_imod) met_patt
12.140 + Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt
12.141 \<close> ML \<open>
12.142 (*+*)if (i_from_met |> I_Model.to_string_TEST @{context}) = "[\n" ^
12.143 "(0, [], false ,i_model_empty, (Sup_TEST Constants [], Position.T)), \n" ^
12.144 @@ -437,7 +468,7 @@
12.145 "(0, [], false ,i_model_empty, (Sup_TEST AdditionalValues [], Position.T))]"
12.146 (*+*)then () else error "s_make_complete: from_met CHANGED";
12.147 \<close> ML \<open>
12.148 - val (met_max_vnts, _) = Model_Def.max_variants i_from_met;
12.149 + val met_max_vnts = Model_Def.max_variants o_model i_from_met;
12.150 (*+*)val [2] = met_max_vnts
12.151 \<close> ML \<open>
12.152 val met_max_vnt = hd met_max_vnts (*need only one for solve-phase*)
12.153 @@ -470,6 +501,235 @@
12.154 \<close>
12.155
12.156 section \<open>===================================================================================\<close>
12.157 +section \<open>===== i-model.sml .s_make_complete [][] ===========================================\<close>
12.158 +ML \<open>
12.159 +\<close> ML \<open>
12.160 +(* most general case: user activates some <complete specification> *)
12.161 +\<close> ML \<open>
12.162 +(*---vvvvv these would overwrite above definition ^^^* )
12.163 +open Ctree
12.164 +open Pos;
12.165 +open TermC;
12.166 +open Istate;
12.167 +open Tactic;
12.168 +open P_Model
12.169 +open Rewrite;
12.170 +open Step;
12.171 +open LItool;
12.172 +open LI;
12.173 +open Test_Code
12.174 +open Specify
12.175 +open Model_Def
12.176 +open Pre_Conds;
12.177 +open I_Model;
12.178 +( **)
12.179 +
12.180 +val (_(*example text*),
12.181 + (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
12.182 + "Extremum (A = 2 * u * v - u \<up> 2)" ::
12.183 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
12.184 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
12.185 + "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" :: (*INCORRECT 2 / v*)
12.186 +(*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
12.187 + "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
12.188 + "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
12.189 + "ErrorBound (\<epsilon> = (0::real))" :: []),
12.190 + refs as ("Diff_App",
12.191 + ["univariate_calculus", "Optimisation"],
12.192 + ["Optimisation", "by_univariate_calculus"])))
12.193 + = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
12.194 +
12.195 +val c = [];
12.196 +val (p,_,f,nxt,_,pt) =
12.197 + Test_Code.init_calc @{context} [(model, refs)]; val Model_Problem = nxt;
12.198 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
12.199 +\<close> ML \<open>
12.200 +\<close> ML \<open> (*//----------- setup test data for I_Model.s_make_complete -------------------------\\*)
12.201 +(*//------------------ setup test data for I_Model.s_make_complete -------------------------\\*)
12.202 +val (o_model, (pI, mI)) = case get_obj I pt (fst p) of
12.203 + PblObj {origin = (o_model, (_, pI, mI), _), ...}
12.204 + => (o_model, (pI, mI))
12.205 + | _ => raise ERROR ""
12.206 +\<close> ML \<open>
12.207 +val {model = pbl_patt, ...} = Problem.from_store ctxt pI;
12.208 +val {model = met_patt, ...} = MethodC.from_store ctxt mI;
12.209 +\<close> ML \<open>
12.210 +val pbl_imod = []
12.211 +val met_imod = []
12.212 +\<close> ML \<open>
12.213 +(*+*)if (o_model |> O_Model.to_string @{context}) = "[\n" ^
12.214 +(*+*) "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), \n" ^
12.215 +(*+*) "(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), \n" ^
12.216 +(*+*) "(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), \n" ^
12.217 +(*+*) "(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), \n" ^
12.218 +(*+*) "(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), \n" ^
12.219 +(*+*) "(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), \n" ^
12.220 +(*+*) "(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), \n" ^
12.221 +(*+*) "(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n" ^
12.222 +(*+*) "(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), \n" ^
12.223 +(*+*) "(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), \n" ^
12.224 +(*+*) "(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), \n" ^
12.225 +(*+*) "(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
12.226 +then () else error "setup test data for I_Model.s_make_complete CHANGED";
12.227 +(*\\------------------ setup test data for I_Model.s_make_complete -------------------------//*)
12.228 +\<close> ML \<open> (*\\----------- setup test data for I_Model.s_make_complete -------------------------//*)
12.229 +\<close> ML \<open>
12.230 +val return_s_make_complete =
12.231 + s_make_complete o_model (pbl_imod, met_imod) (pbl_patt, met_patt);
12.232 +\<close> ML \<open> (*/------------ step into s_make_complete -------------------------------------------\\*)
12.233 +(*/------------------- step into s_make_complete -------------------------------------------\\*)
12.234 +"~~~~~ fun s_make_complete , args:"; val (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt)) =
12.235 + (o_model, (pbl_imod, met_imod), (pbl_patt, met_patt));
12.236 +\<close> ML \<open>
12.237 + val pbl_max_vnts = Model_Def.max_variants o_model pbl_imod;
12.238 +\<close> ML \<open>
12.239 + val i_from_pbl = map (fn (_, (descr, _)) =>
12.240 + Pre_Conds.get_descr_vnt descr pbl_max_vnts pbl_imod) pbl_patt;
12.241 +\<close> ML \<open> (*//----------- step into get_descr_vnt ---------------------------------------------\\*)
12.242 +(*//------------------ step into get_descr_vnt ---------------------------------------------\\*)
12.243 +"~~~~~ fun get_descr_vnt , args:"; val (descr, vnts, i_model) =
12.244 + (@{term Constants}, pbl_max_vnts, pbl_imod);
12.245 +\<close> ML \<open>
12.246 + val equal_descr(*for (*+*)filter (fn (_, vnts',..*): I_Model.T_TEST =
12.247 + filter (fn (_, _, _, _, (feedb, _)) => case get_dscr' feedb of NONE => false
12.248 + | SOME descr' => if descr = descr' then true else false) i_model
12.249 +\<close> ML \<open>
12.250 +(*+*)filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) (equal_descr: I_Model.T_TEST)
12.251 +(*+*): I_Model.T_TEST
12.252 +\<close> ML \<open>
12.253 +val return_get_descr_vnt_1 =
12.254 + case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
12.255 + [] => (0, [], false, "i_model_empty", (Sup_TEST (descr, []), Position.none))
12.256 + | items => Library.the_single items (*only applied to model_patt, which has each descr once*)
12.257 +(*\\------------------ step into get_descr_vnt ---------------------------------------------//*)
12.258 +\<close> ML \<open> (*\\----------- step into get_descr_vnt ---------------------------------------------//*)
12.259 +\<close> ML \<open>
12.260 +(*+*)if return_get_descr_vnt_1 = nth 1 i_from_pbl
12.261 +(*+*)then () else error "return_get_descr_vnt_1 <> nth 1 i_from_pbl";
12.262 +\<close> ML \<open>
12.263 +(*+*)if (i_from_pbl |> I_Model.to_string_TEST @{context}) = "[\n" ^
12.264 + "(0, [], false ,i_model_empty, (Sup_TEST Constants [], Position.T)), \n" ^
12.265 + "(0, [], false ,i_model_empty, (Sup_TEST Maximum, Position.T)), \n" ^
12.266 + "(0, [], false ,i_model_empty, (Sup_TEST AdditionalValues [], Position.T)), \n" ^
12.267 + "(0, [], false ,i_model_empty, (Sup_TEST Extremum, Position.T)), \n" ^
12.268 + "(0, [], false ,i_model_empty, (Sup_TEST SideConditions [], Position.T))]"
12.269 +(*+*)then () else error "I_Model.s_make_complete > i_from_pbl CHANGED";
12.270 +\<close> ML \<open>
12.271 +\<close> ML \<open> (*|------------ continue s_make_complete ----------------------------------------------*)
12.272 +(*|------------------- continue s_make_complete ----------------------------------------------*)
12.273 +\<close> ML \<open>
12.274 + val pbl_from_o_model = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
12.275 + if is_empty_single_TEST i_single
12.276 + then
12.277 + case get_descr_vnt' feedb pbl_max_vnts o_model of
12.278 +(*-----------^^^^^^^^^^^^^^-----------------------------*)
12.279 + [] => raise ERROR (msg pbl_max_vnts feedb)
12.280 + | o_singles => map transfer_terms o_singles
12.281 + else [i_single (*fetched before from pbl_imod*)])) i_from_pbl |> flat
12.282 +\<close> ML \<open>
12.283 +(*+*)val [1, 2, 3] = vnts;
12.284 +(*+*)if (pbl_from_o_model |> I_Model.to_string_TEST @{context}) = "[\n" ^
12.285 + "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
12.286 + "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
12.287 + "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
12.288 + "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
12.289 + "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
12.290 + "(6, [3], true ,#Relate, (Cor_TEST SideConditions [u / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>] , pen2str, Position.T))]"
12.291 +then () else error "pbl_from_o_model CHANGED"
12.292 +\<close> ML \<open>
12.293 +\<close> ML \<open>
12.294 +\<close> ML \<open> (*//----------- step into map ((fn i_single -----------------------------------------\\*)
12.295 +(*//------------------ step into map ((fn i_single -----------------------------------------\\*)
12.296 +"~~~~~ fun map nth 1 ((fn i_single , args:"; val (i_single as (_, _, _, _, (feedb, _))) =
12.297 + (nth 1 i_from_pbl);
12.298 + (*if*) is_empty_single_TEST i_single (*then*);
12.299 + (*case*) get_descr_vnt' feedb pbl_max_vnts o_model;
12.300 +\<close> ML \<open>
12.301 +(*+*)val (0, [], false, "i_model_empty", (Sup_TEST (Const ("Input_Descript.Constants", _), []), _))
12.302 + = i_single
12.303 +(*+*)val true = is_empty_single_TEST i_single
12.304 +\<close> ML \<open>
12.305 +val return_get_descr_vnt'= (*case*)
12.306 + get_descr_vnt' feedb pbl_max_vnts o_model (*of*);
12.307 +\<close> ML \<open> (*\\----------- step into map ((fn i_single -----------------------------------------//*)
12.308 +(*\\------------------ step into map ((fn i_single -----------------------------------------//*)
12.309 +
12.310 +\<close> ML \<open> (*|------------ continue s_make_complete ----------------------------------------------*)
12.311 +(*|------------------- continue s_make_complete ----------------------------------------------*)
12.312 +\<close> ML \<open>
12.313 + val i_from_met = map (fn (_, (descr, _)) =>
12.314 + Pre_Conds.get_descr_vnt descr pbl_max_vnts met_imod) met_patt
12.315 +\<close> ML \<open>
12.316 +(*+*)val [1, 2, 3] = pbl_max_vnts (*..? ? GOON*)
12.317 +\<close> ML \<open>
12.318 +(*+*)if (i_from_met |> I_Model.to_string_TEST @{context}) = "[\n" ^
12.319 + "(0, [], false ,i_model_empty, (Sup_TEST Constants [], Position.T)), \n" ^
12.320 + "(0, [], false ,i_model_empty, (Sup_TEST Maximum, Position.T)), \n" ^
12.321 + "(0, [], false ,i_model_empty, (Sup_TEST Extremum, Position.T)), \n" ^
12.322 + "(0, [], false ,i_model_empty, (Sup_TEST SideConditions [], Position.T)), \n" ^
12.323 + "(0, [], false ,i_model_empty, (Sup_TEST FunctionVariable, Position.T)), \n" ^
12.324 + "(0, [], false ,i_model_empty, (Sup_TEST Input_Descript.Domain, Position.T)), \n" ^
12.325 + "(0, [], false ,i_model_empty, (Sup_TEST ErrorBound, Position.T)), \n" ^
12.326 + "(0, [], false ,i_model_empty, (Sup_TEST AdditionalValues [], Position.T))]"
12.327 +(*+*)then () else error "s_make_complete: i_from_met CHANGED";
12.328 +\<close> ML \<open>
12.329 + val met_max_vnts = Model_Def.max_variants o_model i_from_met;
12.330 +(*+*)val [1, 2, 3]: variant list = met_max_vnts
12.331 +\<close> ML \<open>
12.332 + val max_vnt = hd met_max_vnts (*need only one for solve-phase*)
12.333 +\<close> ML \<open>
12.334 + val met_from_pbl = map ((fn i_single as (_, _, _, _, (feedb, _)) =>
12.335 + if is_empty_single_TEST i_single
12.336 + then
12.337 + case get_descr_vnt' feedb [max_vnt] o_model of
12.338 + [] => raise ERROR (msg [max_vnt] feedb)
12.339 + | o_singles => map transfer_terms o_singles
12.340 + else [i_single (*fetched before from met_imod*)])) i_from_met |> flat
12.341 +\<close> ML \<open>
12.342 +(*+*)val 1 = max_vnt;
12.343 +(*+*)if (met_from_pbl |> I_Model.to_string_TEST @{context}) = "[\n" ^
12.344 + "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
12.345 + "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
12.346 + "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
12.347 + "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
12.348 + "(7, [1], true ,#undef, (Cor_TEST FunctionVariable a , pen2str, Position.T)), \n" ^
12.349 + "(10, [1, 2], true ,#undef, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
12.350 + "(12, [1, 2, 3], true ,#undef, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
12.351 + "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]"
12.352 +(*+*)then () else error "s_make_complete: met_from_pbl CHANGED";
12.353 +\<close> ML \<open>
12.354 +\<close> ML \<open>
12.355 +val return_s_make_complete_step as (pbl_imod_step, met_imod_step)=
12.356 + (filter (fn (_, vnts', _, _, _) => member op = vnts' max_vnt) pbl_from_o_model,
12.357 + met_from_pbl)
12.358 +\<close> ML \<open> (*\------------ step into s_make_complete -------------------------------------------//*)
12.359 +(*\------------------- step into s_make_complete -------------------------------------------//*)
12.360 +if return_s_make_complete = return_s_make_complete_step
12.361 +then () else error "s_make_complete: stewise construction <> value of fun"
12.362 +;
12.363 +(* final test ... ----------------------------------------------------------------------------*)
12.364 +(pbl_imod_step |> I_Model.to_string_TEST @{context},
12.365 + met_imod_step |> I_Model.to_string_TEST @{context}) =
12.366 + ("[\n" ^
12.367 + "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
12.368 + "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
12.369 + "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T)), \n" ^
12.370 + "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
12.371 + "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T))]",
12.372 + "[\n" ^
12.373 + "(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] , pen2str, Position.T)), \n" ^
12.374 + "(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A , pen2str, Position.T)), \n" ^
12.375 + "(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) , pen2str, Position.T)), \n" ^
12.376 + "(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] , pen2str, Position.T)), \n" ^
12.377 + "(7, [1], true ,#undef, (Cor_TEST FunctionVariable a , pen2str, Position.T)), \n" ^
12.378 + "(10, [1, 2], true ,#undef, (Cor_TEST Input_Descript.Domain {0<..<r} , pen2str, Position.T)), \n" ^
12.379 + "(12, [1, 2, 3], true ,#undef, (Cor_TEST ErrorBound (\<epsilon> = 0) , pen2str, Position.T)), \n" ^
12.380 + "(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] , pen2str, Position.T))]")
12.381 +
12.382 +\<close> ML \<open>
12.383 +\<close>
12.384 +
12.385 +section \<open>===================================================================================\<close>
12.386 section \<open>===== ===========================================================================\<close>
12.387 ML \<open>
12.388 \<close> ML \<open>