1.1 --- a/src/Tools/isac/Build_Isac.thy Tue Aug 29 09:04:36 2023 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Aug 30 06:37:56 2023 +0200
1.3 @@ -181,7 +181,7 @@
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 @@ -216,7 +216,7 @@
1.13 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/calculation.sml"
1.14 ML_file "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/vscode-example.sml"
1.15
1.16 -(**)
1.17 +( **)
1.18 ML \<open>
1.19 \<close> ML \<open>
1.20 \<close> ML \<open>
2.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Tue Aug 29 09:04:36 2023 +0200
2.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Wed Aug 30 06:37:56 2023 +0200
2.3 @@ -501,10 +501,10 @@
2.4
2.5 fun by_tactic (Tactic.Apply_Method' (mI, _, _, _)) (_, ctxt) (pt, pos as (p, _)) =
2.6 let
2.7 - val (itms, oris, probl) = case get_obj I pt p of
2.8 +(*new*)val (itms, oris, probl) = case get_obj I pt p of
2.9 PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
2.10 | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
2.11 - val {model, ...} = MethodC.from_store ctxt mI;
2.12 +(*new*)val {model, ...} = MethodC.from_store ctxt mI;
2.13 val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
2.14 val (is, env, ctxt, prog) = case LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI of
2.15 (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
3.1 --- a/src/Tools/isac/Specify/i-model.sml Tue Aug 29 09:04:36 2023 +0200
3.2 +++ b/src/Tools/isac/Specify/i-model.sml Wed Aug 30 06:37:56 2023 +0200
3.3 @@ -49,21 +49,29 @@
3.4 -> message * single
3.5 val get_field_term: theory -> O_Model.single -> single -> m_field * TermC.as_string
3.6
3.7 - val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
3.8 - Model_Def.i_model_TEST * Env.T * (Pre_Conds.env_subst * Pre_Conds.env_eval)
3.9 +(*
3.10 + val of_max_variant: Model_Pattern.T -> T_TEST ->
3.11 + T_TEST * Env.T * (Pre_Conds.env_subst * Pre_Conds.env_eval)
3.12 +*)
3.13 + val of_max_variant: Model_Pattern.T -> T_TEST ->
3.14 + (bool * Model_Def.variant * T_TEST) * Env.T * (Pre_Conds.env_subst * Pre_Conds.env_eval)
3.15
3.16 +(*REN make_complete*)
3.17 val complete: O_Model.T -> (*Problem*)T -> (*MethodC*)T -> Model_Pattern.T -> T
3.18 val add: single -> T -> T
3.19 val complete_method: O_Model.T * Model_Pattern.T * Model_Pattern.T * T -> T * T
3.20 val is_error: feedback -> bool
3.21 +(*REN complete_internal*)
3.22 val complete': Model_Pattern.T -> O_Model.single -> single
3.23
3.24 val is_complete: T -> bool
3.25 - val is_complete_variant: int -> T_TEST-> bool
3.26 + val is_complete_variant: Model_Def.variant -> T_TEST-> bool
3.27 val to_p_model: theory -> feedback -> string
3.28 - val eq1: ''a -> 'b * (''a * 'c) -> bool
3.29
3.30 (*from isac_test for Minisubpbl*)
3.31 + val eq1: ''a -> 'b * (''a * 'c) -> bool
3.32 + val filter_outs: O_Model.T -> T -> O_Model.T
3.33 + val filter_outs_TEST: O_Model.T -> T_TEST -> O_Model.T
3.34 val feedback_to_string: Proof.context -> feedback -> string
3.35 val feedback_TEST_to_string: Proof.context -> feedback_TEST -> string
3.36
3.37 @@ -399,6 +407,7 @@
3.38 | NONE => (i, v, true, f, Cor ((d, ts), (d, ts)))
3.39
3.40 (*filter out oris which have same description in itms*)
3.41 +(* ---------------------------------- type problems ---vv---------vv
3.42 fun filter_outs oris [] = oris
3.43 | filter_outs oris (i::itms) =
3.44 let
3.45 @@ -406,6 +415,29 @@
3.46 in
3.47 filter_outs ors itms
3.48 end
3.49 +*)
3.50 +(*with types..*)
3.51 +(*T_TESTold*)
3.52 +fun filter_outs oris [] = oris
3.53 + | filter_outs oris (i::itms) =
3.54 + let
3.55 + val ors = filter_out ((curry op = ((descriptor o
3.56 + (#5: single -> feedback)) i)) o
3.57 + (#4: O_Model.single -> O_Model.descriptor)) oris
3.58 + in
3.59 + filter_outs ors itms
3.60 + end
3.61 +(*T_TEST*)
3.62 +fun filter_outs_TEST oris [] = oris
3.63 + | filter_outs_TEST oris (i::itms) =
3.64 + let
3.65 + val ors = filter_out ((curry op = ((descriptor_TEST o
3.66 + ((#1 o #5): single_TEST -> feedback_TEST) ) i) ) o
3.67 + (#4: O_Model.single -> O_Model.descriptor) ) oris
3.68 + in
3.69 + filter_outs_TEST ors itms
3.70 + end
3.71 +(*T_TESTnew*)
3.72
3.73 (*filter oris which are in pbt, too*)
3.74 fun filter_pbt oris pbt =
3.75 @@ -448,7 +480,7 @@
3.76 itms @ (map (complete' met) os)
3.77 end
3.78
3.79 -(*complete model and guard of a calc-head*)
3.80 +(*complete model and guard of a calc-head WN230829 replaced by complete_pos*)
3.81 fun complete_method (oris, mpc, model, probl) =
3.82 let
3.83 val pits = filter_out ((curry op= false) o (#3)) probl
3.84 @@ -464,7 +496,7 @@
3.85 fun is_complete ([]: T) = false
3.86 | is_complete itms = foldl and_ (true, (map #3 itms))
3.87
3.88 -(*for PIDE*)
3.89 +(*for PIDE: are all feedback Cor ? MISSING: Pre_Conds.check *)
3.90 fun is_complete_variant no_model_items i_model =
3.91 no_model_items = length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model)
3.92
4.1 --- a/src/Tools/isac/Specify/pre-conditions.sml Tue Aug 29 09:04:36 2023 +0200
4.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml Wed Aug 30 06:37:56 2023 +0200
4.3 @@ -21,8 +21,8 @@
4.4 val max_variant: Model_Def.i_model -> Model_Def.variant
4.5 val environment_TEST: Model_Pattern.T -> Model_Def.i_model_TEST -> Env.T
4.6
4.7 - val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
4.8 - Model_Def.i_model_TEST * Env.T * (env_subst * env_eval)
4.9 + val of_max_variant: Model_Pattern.single list -> Model_Def.i_model_TEST ->
4.10 + (bool * Model_Def.variant * Model_Def.i_model_TEST) * Env.T * (env_subst * env_eval)
4.11
4.12 val check_pos: Proof.context -> Rule_Set.T -> unchecked_pos ->
4.13 Model_Pattern.T * Model_Def.i_model_TEST -> checked_pos
4.14 @@ -233,7 +233,7 @@
4.15 fun cnt_corrects i_model =
4.16 fold (curry op +) (map (fn (_, _, _, _, (Cor_TEST _, _)) => 1 | _ => 0) i_model) 0;
4.17
4.18 -fun of_max_variant _ [] = ([], [], ([], []))
4.19 +fun of_max_variant _ [] = ((false, 0, []), [], ([], []))
4.20 | of_max_variant model_patt i_model =
4.21 let
4.22 val all_variants =
4.23 @@ -253,7 +253,9 @@
4.24 val subst_eval_list = make_envs_preconds equal_givens
4.25 val (env_subst, env_eval) = split_list subst_eval_list
4.26 in
4.27 - (i_model_max, env_model, (env_subst, env_eval))
4.28 + ((length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model_max)
4.29 + = length model_patt, max_variant, i_model_max),
4.30 + env_model, (env_subst, env_eval))
4.31 end
4.32
4.33 (*extract the environment from an I_Model.of_max_variant*)
5.1 --- a/src/Tools/isac/Specify/specify.sml Tue Aug 29 09:04:36 2023 +0200
5.2 +++ b/src/Tools/isac/Specify/specify.sml Wed Aug 30 06:37:56 2023 +0200
5.3 @@ -206,17 +206,17 @@
5.4
5.5 (*
5.6 do all specification in one single step:
5.7 - bypass completion of Problem.model and go immediately for MethodC: I_Model.complete'
5.8 + bypass input of Problem.model and go immediately for MethodC: I_Model.complete'
5.9 *)
5.10 fun do_all (pt, (*old* )pos as( *old*) (p, _)) =
5.11 let
5.12 val (o_model, o_refs as (_, _, met_id), ctxt) = case Ctree.get_obj I pt p of
5.13 Ctree.PblObj {origin = (o_model, o_refs, _), ctxt, ...}
5.14 => (o_model, o_refs, ctxt)
5.15 - | _ => raise ERROR "do_all: uncovered case get_obj"
5.16 + | _ => raise ERROR "Specify.do_all: uncovered case get_obj"
5.17 val mod_pat = MethodC.from_store ctxt met_id |> #model
5.18 val i_model = map (I_Model.complete' mod_pat) o_model
5.19 - (*no parse, ^^^ takes existing terms; ctxt already created by O_Model.init*)
5.20 + (*no parse, ^^^ takes existing terms; ctxt already created by O_Model.init*)
5.21 val (pt, _) = Ctree.cupdate_problem pt p (o_refs, i_model, i_model, ctxt)
5.22 in
5.23 (pt, (p, Pos.Met))
6.1 --- a/test/Tools/isac/Interpret/li-tool.sml Tue Aug 29 09:04:36 2023 +0200
6.2 +++ b/test/Tools/isac/Interpret/li-tool.sml Wed Aug 30 06:37:56 2023 +0200
6.3 @@ -425,7 +425,9 @@
6.4 (*bieg*)val "[\"\n(l_l, L)\", \"\n(q_q, q_0)\", \"\n(r_b, [y 0 = 0, y L = 0, M_b 0 = 0, M_b L = 0])\", \"\n(fun_var, x)\", \"\n(id_der, y')\", \"\n(id_momentum, M_b)\", \"\n(id_lat_force, Q)\", \"\n(vs, [c, c_2, c_3, c_4])\", \"\n(b_b, y)\"]"
6.5 = env_model |> Subst.to_string @{context}
6.6 (*bieg*)val "[]" = env_subst |> Subst.to_string @{context}
6.7 -val return_of_max_variant_step = (i_model_max, env_model, (env_subst, env_eval))
6.8 +val return_of_max_variant_step = ((length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model_max)
6.9 + = length model_patt, max_variant, i_model_max),
6.10 + env_model, (env_subst, env_eval))
6.11 ;
6.12 (*+*)if return_of_max_variant_step = return_of_max_variant then () else error "<>";
6.13 (*\\\----------------- step into of_max_variant --------------------------------------------//*)
7.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Tue Aug 29 09:04:36 2023 +0200
7.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Wed Aug 30 06:37:56 2023 +0200
7.3 @@ -155,8 +155,6 @@
7.4 val cmI = if mI = MethodC.id_empty then mI' else mI;
7.5 val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
7.6 val {model = mpc, ...} = MethodC.from_store ctxt cmI;
7.7 -(*//------------------ adhoc inserted fun of_max_variant -----------------------------------\\*)
7.8 -(*\\------------------ adhoc inserted fun check ----------------------------------------//*)
7.9
7.10 val return_check_OLD =
7.11 check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
7.12 @@ -169,10 +167,6 @@
7.13 "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) =
7.14 (model_patt, i_model);
7.15
7.16 -(*with OLD code* )
7.17 -(*+*)val "[\n(0, [], false ,#Given, (Inc_TEST Constants [__=__, __=__], Position.T)), \n(0, [], false ,#Find, (Inc_TEST Maximum __, Position.T)), \n(0, [], false ,#Find, (Inc_TEST AdditionalValues [__, __], Position.T)), \n(0, [], false ,#Relate, (Inc_TEST Extremum (__=__), Position.T)), \n(0, [], false ,#Relate, (Inc_TEST SideConditions [__=__, __=__], Position.T))]"
7.18 - = i_model |> I_Model.to_string_TEST @ {context}
7.19 -( *with OLD code*)
7.20 (*+*)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))]"
7.21 = i_model |> I_Model.to_string_TEST @{context}
7.22 val all_variants =
8.1 --- a/test/Tools/isac/Specify/pre-conditions.sml Tue Aug 29 09:04:36 2023 +0200
8.2 +++ b/test/Tools/isac/Specify/pre-conditions.sml Wed Aug 30 06:37:56 2023 +0200
8.3 @@ -17,7 +17,7 @@
8.4 (*see Outer_Syntax: val (model, where_) = Model_Pattern.parse_pos_empty ctxt model_input*)
8.5 open Model_Def;
8.6 open Pre_Conds;
8.7 -open I_Model
8.8 +open I_Model;
8.9 (*//------------------ test data setup -----------------------------------------------------\\*)
8.10 val thy = @{theory Calculation}
8.11
9.1 --- a/test/Tools/isac/Specify/specify.sml Tue Aug 29 09:04:36 2023 +0200
9.2 +++ b/test/Tools/isac/Specify/specify.sml Wed Aug 30 06:37:56 2023 +0200
9.3 @@ -172,9 +172,10 @@
9.4 fastype_of: Bound
9.5 B.0 *)( **)
9.6 (*\------------------ Specification of Problem and MethodC model is complete, Solution starts/*)
9.7 +;"? show section title below ?";
9.8
9.9
9.10 -"----------- revise Specify.do_all -------------------------------------------------------------";
9.11 +(**** revise Specify.do_all ############################################################## ****);
9.12 "----------- revise Specify.do_all -------------------------------------------------------------";
9.13 "----------- revise Specify.do_all -------------------------------------------------------------";
9.14 (* from Minisubplb/100-init-rootpbl.sml:
9.15 @@ -988,7 +989,7 @@
9.16 "(#Given, (FunktionsVariable, v_v))\", \"" ^
9.17 "(#Find, (Funktionen, funs'''))\"]"
9.18 (*+*)then () else error "associate_input' Model_Pattern of Subproblem CHANGED";
9.19 -(* root-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv ------------------------------------- \<up> *)
9.20 +(* root-vvvvvvvvvvvvvvvvvvvvvvvvvvvvvvvv ------------------------------------- \<up>*)
9.21 (*+*)if (Problem.from_store ctxt ["Biegelinien"] |> #model |> Model_Pattern.to_string @{context}) = "[\"" ^
9.22 "(#Given, (Traegerlaenge, l_l))\", \"" ^
9.23 "(#Given, (Streckenlast, q_q))\", \"" ^
10.1 --- a/test/Tools/isac/Test_Theory.thy Tue Aug 29 09:04:36 2023 +0200
10.2 +++ b/test/Tools/isac/Test_Theory.thy Wed Aug 30 06:37:56 2023 +0200
10.3 @@ -59,11 +59,1000 @@
10.4 \<close> ML \<open>
10.5 \<close>
10.6
10.7 -(** )ML_file "BaseDefinitions/libraryC.sml" (**)check file with test under repair below( **)
10.8 section \<open>===================================================================================\<close>
10.9 -section \<open>===== ===========================================================================\<close>
10.10 +section \<open>===== src/../pre-conditions.sml ===================================================\<close>
10.11 +ML \<open>
10.12 +open Model_Def
10.13 +open Pre_Conds
10.14 +open I_Model
10.15 +\<close> ML \<open>
10.16 +fun of_max_variant _ [] = ((false, 0, []), [], ([], []))
10.17 + | of_max_variant model_patt i_model =
10.18 + let
10.19 + val all_variants =
10.20 + map (fn (_, variants, _, _, _) => variants) i_model
10.21 + |> flat
10.22 + |> distinct op =
10.23 + val variants_separated = map (filter_variants' i_model) all_variants
10.24 + val sums_corr = map (cnt_corrects) variants_separated
10.25 + val sum_variant_s = arrange_args sums_corr (1, all_variants)
10.26 + val (_, max_variant) = hd (*..crude decision, up to improvement *)
10.27 + (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
10.28 + val i_model_max =
10.29 + filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
10.30 + val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
10.31 + val env_model = make_env_model equal_descr_pairs
10.32 + val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
10.33 + val subst_eval_list = make_envs_preconds equal_givens
10.34 + val (env_subst, env_eval) = split_list subst_eval_list
10.35 + in
10.36 + ((length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model_max)
10.37 + = length model_patt, max_variant, i_model_max),
10.38 + env_model, (env_subst, env_eval))
10.39 + end
10.40 +\<close> ML \<open>
10.41 +of_max_variant:
10.42 + Model_Pattern.single list ->
10.43 + (int * variant list * bool * m_field * (i_model_feedback_TEST * Position.T)) list ->
10.44 + (bool * variant * (int * variant list * bool * m_field * (i_model_feedback_TEST * Position.T)) list) * (term * term) list * ((term * term) list * (term * term) list)
10.45 +\<close> ML \<open>
10.46 +of_max_variant: Model_Pattern.single list -> Model_Def.i_model_TEST ->
10.47 + (bool * variant * Model_Def.i_model_TEST) * Env.T * (env_subst * env_eval)
10.48 +\<close> ML \<open>
10.49 +
10.50 +\<close> ML \<open>
10.51 +\<close>
10.52 +
10.53 +(**)ML_file "Minisubpbl/150a-add-given-Maximum.sml" (** )check file with test under repair below( **)
10.54 +section \<open>===================================================================================\<close>
10.55 +section \<open>===== Minisubpbl/150a-add-given-Maximum.sml ======================================\<close>
10.56 ML \<open>
10.57 \<close> ML \<open>
10.58 +(* Title: "Minisubpbl/150a-add-given-Maximum.sml"
10.59 + Author: Walther Neuper 1105
10.60 + (c) copyright due to lincense terms.
10.61 +
10.62 +COMPARE Specify/specify.sml --- specify-phase: low level functions ---
10.63 +
10.64 +ATTENTION: the file creates buffer overflow if copied in one piece !
10.65 +
10.66 +Note: This test --- steps into me --- more than once, to a somewhat extreme extent;
10.67 + in order not to get lost while working in Test_Some etc,
10.68 + re-introduce ML (*--- step into XXXXX ---*) and Co.
10.69 + and use Sidekick for orientation.
10.70 + Nesting is indicated by /--- //-- ///- at the left margin of the comments.
10.71 +*)
10.72 +
10.73 +open Ctree;
10.74 +open Pos;
10.75 +open TermC;
10.76 +open Istate;
10.77 +open Tactic;
10.78 +open I_Model;
10.79 +open P_Model
10.80 +open Rewrite;
10.81 +open Step;
10.82 +open LItool;
10.83 +open LI;
10.84 +open Test_Code
10.85 +open Specify
10.86 +open ME_Misc
10.87 +open Pre_Conds;
10.88 +
10.89 +val (_(*example text*),
10.90 + (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
10.91 + "Extremum (A = 2 * u * v - u \<up> 2)" ::
10.92 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
10.93 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
10.94 + "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" :: (*INCORRECT 2 / v*)
10.95 +(*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in example*)
10.96 + "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
10.97 + "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
10.98 + "ErrorBound (\<epsilon> = (0::real))" :: []),
10.99 + refs as ("Diff_App",
10.100 + ["univariate_calculus", "Optimisation"],
10.101 + ["Optimisation", "by_univariate_calculus"])))
10.102 + = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
10.103 +
10.104 +val c = [];
10.105 +val return_init_calc =
10.106 + Test_Code.init_calc @{context} [(model, refs)]; (*val Model_Problem = nxt;*)
10.107 +(*/------------------- step into init_calc -------------------------------------------------\\*)
10.108 +"~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))]) =
10.109 + (@{context}, [(model, refs)]);
10.110 + val thy = thy_id |> ThyC.get_theory ctxt
10.111 + val ((pt, p), tacis) = Step_Specify.initialise' thy (model, refs)
10.112 + val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
10.113 + val f =
10.114 + TESTg_form ctxt (pt,p);
10.115 +"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p));
10.116 + val (form, _, _) =
10.117 + ME_Misc.pt_extract ctxt ptp;
10.118 +"~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_ as Pbl(*Frm,Pbl*)))) = (ctxt, ptp);
10.119 + val ppobj = Ctree.get_obj I pt p
10.120 + val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;
10.121 + (*if*) Ctree.is_pblobj ppobj (*then*);
10.122 + pt_model ppobj p_ ;
10.123 +"~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}), Pbl_) =
10.124 + (ppobj, p_);
10.125 + val (_, pI, _) = Ctree.get_somespec' spec spec';
10.126 +(* val where_ = if pI = Problem.id_empty then []*)
10.127 + (*if*) pI = Problem.id_empty (*else*);
10.128 + val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
10.129 + val (_, where_) =
10.130 + Pre_Conds.check ctxt where_rls where_
10.131 + (model, I_Model.OLD_to_TEST probl);
10.132 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
10.133 + (ctxt, where_rls, where_, (model, I_Model.OLD_to_TEST probl));
10.134 + val (_, _, (env_subst, env_eval)) =
10.135 + of_max_variant model_patt i_model;
10.136 +"~~~~~ fun of_max_variant , args:"; val (_, []) = (model_patt, i_model);
10.137 +(*\------------------- step into init_calc -------------------------------------------------//*)
10.138 +val (p,_,f,nxt,_,pt) = return_init_calc;
10.139 +
10.140 +(*+*)val PblObj {ctxt, probl, ...} = get_obj I pt [];
10.141 +(*+*)Proof_Context.theory_of ctxt (*= {Pure, .., Diff_App}*);
10.142 +(*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term ctxt "r"
10.143 +(*+*)val [] = probl
10.144 +
10.145 +val return_me_Model_Problem =
10.146 + me nxt p c pt; val Add_Given "Constants [r = 7]" = #4 return_me_Model_Problem;
10.147 +(*/------------------- step into me Model_Problem ------------------------------------------\\*)
10.148 +"~~~~~ fun me , args:"; val (tac, (p:Pos.pos'), (_:Test_Code.NEW), (pt:Ctree.ctree)) = (nxt, p, c, pt);
10.149 + val ctxt = Ctree.get_ctxt pt p
10.150 +val return_by_tactic = case
10.151 + Step.by_tactic tac (pt,p) of
10.152 + ("ok", (_, _, ptp)) => ptp;
10.153 +
10.154 +(*//------------------ step into by_tactic -------------------------------------------------\\*)
10.155 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
10.156 +val Applicable.Yes tac' = (*case*)
10.157 + Step.check tac (pt, p) (*of*);
10.158 +(*+*)val Model_Problem' _ = tac';
10.159 +"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
10.160 + (*if*) Tactic.for_specify tac (*then*);
10.161 +
10.162 +Specify_Step.check tac (ctree, pos);
10.163 +"~~~~~ fun check , args:"; val (Tactic.Model_Problem, (pt, pos as (p, _))) =
10.164 + (tac, (ctree, pos));
10.165 + val (o_model, pI', ctxt) = case Ctree.get_obj I pt p of
10.166 + Ctree.PblObj {origin = (o_model, (_, pI', _), _), ctxt, ...} => (o_model, pI', ctxt)
10.167 + val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
10.168 + val pbl = I_Model.init_TEST o_model model_patt;
10.169 +
10.170 +val return_check =
10.171 + Applicable.Yes (Tactic.Model_Problem' (pI', I_Model.TEST_to_OLD pbl, []));
10.172 +(*\\------------------ step into by_tactic -------------------------------------------------//*)
10.173 +val (pt, p) = return_by_tactic;
10.174 +
10.175 +val return_do_next = (*case*)
10.176 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
10.177 +(*//------------------ step into do_next ---------------------------------------------------\\*)
10.178 +"~~~~~ fun do_next , args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) =
10.179 + (p, ((pt, e_pos'),[]));
10.180 + val pIopt = get_pblID (pt,ip);
10.181 + (*if*) ip = ([],Res); (* = false*)
10.182 + val _ = (*case*) tacis (*of*);
10.183 + val SOME _ = (*case*) pIopt (*of*);
10.184 +
10.185 + val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
10.186 + Step.switch_specify_solve p_ (pt, ip);
10.187 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
10.188 + (*if*) Pos.on_specification ([], state_pos) (*then*);
10.189 +
10.190 + val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
10.191 + Step.specify_do_next (pt, input_pos);
10.192 +(*///----------------- step into specify_do_next -------------------------------------------\\*)
10.193 +"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
10.194 +
10.195 +(* val (_, (p_', tac)) =*)
10.196 +val return_find_next_step = (*keep for continuing specify_do_next*)
10.197 + Specify.find_next_step ptp;
10.198 +(*////---------------- step into find_next_step --------------------------------------------\\*)
10.199 +"~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
10.200 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
10.201 + spec = refs, ...} = Calc.specify_data (pt, pos);
10.202 + val ctxt = Ctree.get_ctxt pt pos;
10.203 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
10.204 + (*if*) p_ = Pos.Pbl (*then*);
10.205 +
10.206 + Specify.for_problem ctxt oris (o_refs, refs) (pbl, met);
10.207 +(*/////--------------- step into for_problem -----------------------------------------------\\*)
10.208 +"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
10.209 + = (ctxt, oris, (o_refs, refs), (pbl, met));
10.210 + val cdI = if dI = ThyC.id_empty then dI' else dI;
10.211 + val cpI = if pI = Problem.id_empty then pI' else pI;
10.212 + val cmI = if mI = MethodC.id_empty then mI' else mI;
10.213 + val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
10.214 + val {model = mpc, ...} = MethodC.from_store ctxt cmI;
10.215 +
10.216 + val return_check_OLD =
10.217 + check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
10.218 +(*//////-------------- step into check -------------------------------------------------\\*)
10.219 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
10.220 + (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
10.221 + val return_of_max_variant =
10.222 + of_max_variant model_patt i_model;
10.223 +\<close> ML \<open>(*///// //------ step into of_max_variant --------------------------------------------\\*)
10.224 +(*///// //------------ step into of_max_variant --------------------------------------------\\*)
10.225 +"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) =
10.226 + (model_patt, i_model);
10.227 +
10.228 +(*+*)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))]"
10.229 + = i_model |> I_Model.to_string_TEST @{context}
10.230 + val all_variants =
10.231 + map (fn (_, variants, _, _, _) => variants) i_model
10.232 + |> flat
10.233 + |> distinct op =
10.234 + val variants_separated = map (filter_variants' i_model) all_variants
10.235 + val sums_corr = map (cnt_corrects) variants_separated
10.236 + val sum_variant_s = arrange_args sums_corr (1, all_variants)
10.237 +(*+*)val [(0, 1), (0, 2), (0, 3)] = sum_variant_s
10.238 + val (_, max_variant) = hd (*..crude decision, up to improvement *)
10.239 + (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
10.240 + val i_model_max =
10.241 + filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
10.242 + val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
10.243 +(*for building make_env_s -------------------------------------------------------------------\*)
10.244 +(*!!!*) val ("#Given", (descr, term), pos) =
10.245 + Model_Pattern.split_descriptor ctxt ("#Given", @{term "Constants [r = (7::real)]"}, Position.none)
10.246 +(*!!!*) val patt = equal_descr_pairs |> hd |> #1
10.247 +(*!!!*)val equal_descr_pairs =
10.248 + (patt,
10.249 + (1, [1, 2, 3], true, "#Given", (Cor_TEST ((descr, (*!*)TermC.isalist2list(*!*) term),
10.250 + (TermC.empty, [])), pos)))
10.251 + :: tl equal_descr_pairs
10.252 +(*for building make_env_s -------------------------------------------------------------------/*)
10.253 +
10.254 + val env_model = make_env_model equal_descr_pairs;
10.255 +(*///// ///----------- step into make_env_model --------------------------------------------\\*)
10.256 +"~~~~~ fun make_env_model , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
10.257 +
10.258 +val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
10.259 + => (mk_env_model id feedb));
10.260 +val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 4 equal_descr_pairs;
10.261 +(*\\\\\ \\\----------- step into make_env_model --------------------------------------------//*)
10.262 +\<close> ML \<open>(*||||| ||------ contine of_max_variant ------------------------------------------------*)
10.263 +(*||||| ||------------ contine of_max_variant ------------------------------------------------*)
10.264 +
10.265 + val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
10.266 + val subst_eval_list = make_envs_preconds equal_givens
10.267 +val return_make_envs_preconds =
10.268 + make_envs_preconds equal_givens;
10.269 +(*///// ///----------- step into make_envs_preconds ----------------------------------------\\*)
10.270 +"~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
10.271 +val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb)
10.272 +;
10.273 +xxx: (Model_Pattern.single * I_Model.single_TEST) -> ((term * term) * (term * term)) list;
10.274 +val return_discern_feedback =
10.275 + discern_feedback id feedb;
10.276 +(*nth 1 equal_descr_pairs* )
10.277 +"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb);
10.278 +( *nth 2 equal_descr_pairs*)
10.279 +"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Inc_TEST ((descr, ts), _))) = (id, feedb);
10.280 +
10.281 +(*nth 1 equal_descr_pairs* )
10.282 +(*+*)val [((Const ("fixes", typ1), Free ("r", typ2)),
10.283 + (Free ("r", typ3), value))] = return_discern_feedback
10.284 +(*+*)val true = typ1 = typ2
10.285 +(*+*)val true = typ3 = HOLogic.realT
10.286 +(*+*)val "7" = UnparseC.term @{context} value
10.287 +( *nth 2 equal_descr_pairs*)
10.288 +(*+*)val [] = return_discern_feedback
10.289 +
10.290 +val return_discern_typ =
10.291 + discern_typ id (descr, ts);
10.292 +"~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));
10.293 +(*nth 1 equal_descr_pairs* )
10.294 +(*+*)val [((Const ("fixes", typ1), Free ("r", typ2)),
10.295 + (Free ("r", typ3), value))] = return_discern_typ
10.296 +(*+*)val true = typ1 = typ2
10.297 +(*+*)val true = typ3 = HOLogic.realT
10.298 +(*+*)val "7" = UnparseC.term @{context} value
10.299 +( *nth 2 equal_descr_pairs*)
10.300 +(*+*)val [] = return_discern_typ;
10.301 +(**)
10.302 + switch_type id ts;
10.303 +"~~~~~ fun switch_type , args:"; val (Const (descr_string, _), ts) = (descr, ts);
10.304 +
10.305 +(*nth 1 equal_descr_pairs* )
10.306 +val return_switch_type_TEST = Const (descr_string, ts |> hd |> TermC.lhs |> type_of)
10.307 +
10.308 +(*+*)val Const ("Input_Descript.Constants", typ) = return_switch_type_TEST
10.309 +(*+*)val Type ("Real.real", []) = typ
10.310 +( *nth 2 equal_descr_pairs*)
10.311 +(*+*)val return_switch_type_TEST = descr
10.312 +(**)
10.313 +(*\\\\\ \\\----------- step into make_envs_preconds ----------------------------------------//*)
10.314 +\<close> ML \<open>(*||||| ||------ contine of_max_variant ------------------------------------------------*)
10.315 +(*||||| ||------------ contine of_max_variant ------------------------------------------------*)
10.316 + val subst_eval_list = make_envs_preconds equal_givens
10.317 + val (env_subst, env_eval) = split_list subst_eval_list
10.318 +\<close> ML \<open>
10.319 +val xxx = (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false)
10.320 +\<close> ML \<open>
10.321 +xxx: I_Model.single_TEST -> bool
10.322 +\<close> ML \<open>
10.323 +i_model_max
10.324 +\<close> ML \<open>
10.325 +length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model_max)
10.326 += length model_patt
10.327 +\<close> ML \<open>
10.328 +\<close> ML \<open>
10.329 +val return_of_max_variant = ((length (filter (fn (_, _, _, _, (Cor_TEST _, _)) => true | _ => false) i_model_max)
10.330 + = length model_patt, max_variant, i_model_max),
10.331 + env_model, (env_subst, env_eval));
10.332 +\<close> ML \<open>
10.333 +return_of_max_variant: (bool * variant * T_TEST) * Env.T * (env_subst * env_eval)
10.334 +\<close> ML \<open>
10.335 +\<close> ML \<open>(*\\\\\ \\------ step into of_max_variant --------------------------------------------//*)
10.336 +(*\\\\\ \\------------ step into of_max_variant --------------------------------------------//*)
10.337 + val (i_model_max, env_model, (env_subst, env_eval)) = return_of_max_variant
10.338 +(*!!!/----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---\*)
10.339 + val (i_max_variant, env_model, (env_subst, env_eval)) = (i_model_max, [], ([], []))
10.340 +(*!!!\----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---/*)
10.341 +(*||||||-------------- contine check -----------------------------------------------------*)
10.342 + val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
10.343 + val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
10.344 + val full_subst = if env_eval = [] then pres_subst_other
10.345 + else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
10.346 + val evals = map (eval ctxt where_rls) full_subst
10.347 +val return_ = (i_model_max, env_subst, env_eval)
10.348 +(*\\\\\\\------------- step into check -------------------------------------------------//*)
10.349 +val (preok, _) = return_check_OLD;
10.350 +
10.351 +(*|||||--------------- contine for_problem ---------------------------------------------------*)
10.352 + (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
10.353 + (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
10.354 +val NONE =
10.355 + (*case*) find_first (I_Model.is_error o #5) pbl (*of*);
10.356 +
10.357 + (*case*)
10.358 + Specify.item_to_add (ThyC.get_theory ctxt
10.359 + (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
10.360 +"~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
10.361 + = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl);
10.362 + fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
10.363 + | false_and_not_Sup (_, _, false, _, _) = true
10.364 + | false_and_not_Sup _ = false
10.365 +
10.366 + val v = if itms = [] then 1 else Pre_Conds.max_variant itms
10.367 + val vors = if v = 0 then oris
10.368 + else filter ((fn variant =>
10.369 + fn (_, variants, m_field, _, _) => member op= variants variant andalso m_field <> "#undef")
10.370 + v) oris
10.371 +
10.372 +(*+*)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]\"])]"
10.373 +(*+*) = vors |> O_Model.to_string @{context}
10.374 +
10.375 + val vits = if v = 0 then itms (* because of dsc without dat *)
10.376 + else filter ((fn variant =>
10.377 + fn (_, variants, _, _, _) => member op= variants variant)
10.378 + v) itms; (* itms..vat *)
10.379 +
10.380 + val icl = filter false_and_not_Sup vits; (* incomplete *)
10.381 +
10.382 + (*if*) icl = [] (*else*);
10.383 +(*+*)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)]"
10.384 + = icl |> I_Model.to_string @{context}
10.385 +(*+*)val "(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] , pen2str)"
10.386 + = hd icl |> I_Model.single_to_string @{context}
10.387 +
10.388 +(*++*)val feedback = (fn (_, _, _, _, feedback) => feedback) (hd icl)
10.389 +(*++*)val Const ("Input_Descript.Constants", _) = I_Model.descriptor feedback
10.390 +(*++*)val [] = I_Model.o_model_values feedback
10.391 +
10.392 +(*+*)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]\"])]"
10.393 +(*+*) = vors |> O_Model.to_string @{context}
10.394 +
10.395 +val SOME ori =
10.396 + (*case*) find_first ((fn (_, _, _, _, feedback) => fn (_, _, _, d, ts) =>
10.397 + d = I_Model.descriptor feedback andalso subset op = (I_Model.o_model_values feedback, ts))
10.398 + (hd icl)) vors (*of*);
10.399 +
10.400 +(*+*)val "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"])" =
10.401 +(*+*) ori |> O_Model.single_to_string @{context}
10.402 +(*\\\\\--------------- step into for_problem -----------------------------------------------//*)
10.403 +(*\\\\---------------- step into find_next_step --------------------------------------------//*)
10.404 +(*|||----------------- continuing specify_do_next --------------------------------------------*)
10.405 +val (_, (p_', tac)) = return_find_next_step (*kept for continuing specify_do_next*)
10.406 +
10.407 + val ist_ctxt = Ctree.get_loc pt (p, p_)
10.408 +(*+*)val Add_Given "Constants [r = 7]" = tac
10.409 +val _ =
10.410 + (*case*) tac (*of*);
10.411 +
10.412 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
10.413 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =
10.414 + (tac, (pt, (p, p_')));
10.415 +
10.416 + Specify.by_Add_ "#Given" ct ptp;
10.417 +"~~~~~ fun by_Add_ , args:"; val (m_field, ct ,(pt, pos as (_, p_))) =
10.418 + ("#Given", ct, ptp);
10.419 + val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
10.420 + val (i_model, m_patt) =
10.421 + if p_ = Pos.Met then
10.422 + (met,
10.423 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
10.424 + else
10.425 + (pbl,
10.426 + (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model);
10.427 +
10.428 + (*case*)
10.429 + I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
10.430 +"~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, (str(*, pos*))) =
10.431 + (ctxt, m_field, oris, i_model, m_patt, ct);
10.432 + val (t as (descriptor $ _)) = Syntax.read_term ctxt str
10.433 +
10.434 +(*+*)val "Constants [r = 7]" = UnparseC.term @{context} t;
10.435 +
10.436 + val SOME m_field' =
10.437 + (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
10.438 + (*if*) m_field <> m_field' (*else*);
10.439 +
10.440 +(*+*)val "#Given" = m_field; val "#Given" = m_field'
10.441 +
10.442 +val ("", ori', all) =
10.443 + (*case*) O_Model.contains ctxt m_field o_model t (*of*);
10.444 +
10.445 +(*+*)val (_, _, _, _, vals) = hd o_model;
10.446 +(*+*)val "Constants [r = 7]" = UnparseC.term @{context} (@{term Constants} $ (hd vals));
10.447 +(*+*)if "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), " ^
10.448 +(*+*) "\n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), " ^
10.449 +(*+*) "\n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), " ^
10.450 +(*+*) "\n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), " ^
10.451 +(*+*) "\n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), " ^
10.452 +(*+*) "\n(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), " ^
10.453 +(*+*) "\n(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), " ^
10.454 +(*+*) "\n(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), " ^
10.455 +(*+*) "\n(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), " ^
10.456 +(*+*) "\n(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), " ^
10.457 +(*+*) "\n(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
10.458 +(*+*)= O_Model.to_string @{context} o_model then () else error "o_model CHANGED";
10.459 +
10.460 + (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*);
10.461 +"~~~~~ fun is_notyet_input , args:"; val (ctxt, itms, all, (i, v, f, d, ts), pbt) =
10.462 + (ctxt, i_model, all, ori', m_patt);
10.463 +val SOME (_, (_, pid)) =
10.464 + (*case*) find_first (eq1 d) pbt (*of*);
10.465 +(*local*)fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (I_Model.descriptor itm_);(*local*)
10.466 +val SOME (_, _, _, _, itm_) =
10.467 + (*case*) find_first (eq3 f d) itms (*of*);
10.468 +val ts' = inter op = (o_model_values itm_) ts;
10.469 + (*if*) subset op = (ts, ts') (*else*);
10.470 +val return_is_notyet_input = ("",
10.471 + ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts));
10.472 +"~~~~~ fun ori_2itm , args:"; val (itm_, pid, all, (id, vt, fd, d, ts)) =
10.473 + (itm_, pid, all, (i, v, f, d, subtract op = ts' ts));
10.474 + val ts' = union op = (o_model_values itm_) ts;
10.475 + val pval = [Input_Descript.join'''' (d, ts')]
10.476 + val complete = if eq_set op = (ts', all) then true else false
10.477 +
10.478 +(*+*)val "Inc Constants [] , pen2str" = itm_ |> I_Model.feedback_to_string @{context}
10.479 +(*\\\----------------- step into specify_do_next -------------------------------------------//*)
10.480 +(*\\------------------ step into do_next ---------------------------------------------------//*)
10.481 +val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next
10.482 +
10.483 +(*|------------------- continue with me_Model_Problem ----------------------------------------*)
10.484 +
10.485 +val tacis as (_::_) =
10.486 + (*case*) ts (*of*);
10.487 + val (tac, _, _) = last_elem tacis
10.488 +
10.489 +val return_Model_Problem = (p, [] : NEW, TESTg_form ctxt (pt, p), tac, Celem.Sundef, pt);
10.490 +(*//------------------ step into TESTg_form ------------------------------------------------\\*)
10.491 +"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt, p));
10.492 +
10.493 + val (form, _, _) =
10.494 + ME_Misc.pt_extract ctxt ptp;
10.495 +"~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_(*Frm,Pbl*)))) = (ctxt, ptp);
10.496 + val ppobj = Ctree.get_obj I pt p
10.497 + val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;
10.498 + (*if*) Ctree.is_pblobj ppobj (*then*);
10.499 +
10.500 + pt_model ppobj p_;
10.501 +"~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}),
10.502 + Pbl(*Frm,Pbl*)) = (ppobj, p_);
10.503 + val (_, pI, _) = Ctree.get_somespec' spec spec';
10.504 + (*if*) pI = Problem.id_empty (*else*);
10.505 +(* val where_ = if pI = Problem.id_empty then []*)
10.506 +(* else *)
10.507 +(* let *)
10.508 + val {where_rls, where_, model, ...} = Problem.from_store ctxt pI
10.509 + val (_, where_) = (*Pre_Conds.*)check ctxt where_rls where_ (model, I_Model.OLD_to_TEST probl)
10.510 +(* in where_ end *)
10.511 + val allcorrect = I_Model.is_complete probl andalso foldl and_ (true, (map #1 where_))
10.512 +val return_pt_model = Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, where_, spec)
10.513 +
10.514 +(*|------------------- continue with TESTg_form ----------------------------------------------*)
10.515 +val Ctree.ModSpec (spec as (_, p_, _, gfr, where_, _)) =
10.516 + (*case*) form (*of*);
10.517 + Test_Out.PpcKF ( (Test_Out.Problem [],
10.518 + P_Model.from (Proof_Context.theory_of ctxt) gfr where_));
10.519 +
10.520 + P_Model.from (Proof_Context.theory_of ctxt) gfr where_;
10.521 +"~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
10.522 + fun coll model [] = model
10.523 + | coll model ((_, _, _, field, itm_) :: itms) =
10.524 + coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
10.525 +
10.526 + val gfr = coll P_Model.empty itms;
10.527 +"~~~~~ fun coll , args:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: itms))
10.528 + = (P_Model.empty, itms);
10.529 +
10.530 +(*+*)val 4 = length itms;
10.531 +(*+*)val itm = nth 1 itms;
10.532 +
10.533 + coll P_Model.empty [itm];
10.534 +"~~~~~ fun coll , iterate:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: []))
10.535 + = (P_Model.empty, [itm]);
10.536 +
10.537 + (add_sel_ppc thy field model (item_from_feedback thy itm_));
10.538 +"~~~~~ fun add_sel_ppc , args:"; val ((_: theory), sel, {Given = gi, Where = wh, Find = fi, With = wi, Relate = re}, x )
10.539 + = (thy, field, model, (item_from_feedback thy itm_));
10.540 +
10.541 + P_Model.item_from_feedback thy itm_;
10.542 +"~~~~~ fun item_from_feedback , args:"; val (thy, (I_Model.Inc ((d, ts), _))) = (thy, itm_);
10.543 + P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)));
10.544 +(*\\------------------ step into TESTg_form ------------------------------------------------//*)
10.545 +(*\------------------- step into me Model_Problem ------------------------------------------//*)
10.546 +val (p, _, f, nxt, _, pt) = return_me_Model_Problem
10.547 +
10.548 +(*-------------------- contine me's ----------------------------------------------------------*)
10.549 +val return_me_add_find_Constants = me nxt p c pt;
10.550 + val Add_Find "Maximum A" = #4 return_me_add_find_Constants;
10.551 +(*/------------------- step into me_add_find_Constants -------------------------------------\\*)
10.552 +"~~~~~ fun me , args:"; val (tac as Add_Given "Constants [r = 7]", p, _(*NEW remove*), pt) =
10.553 + (nxt, p, c, pt);
10.554 + val ctxt = Ctree.get_ctxt pt p
10.555 +(*+*)val PblObj {probl = (1, [1, 2, 3], false, "#Given", Inc
10.556 + ((Const ("Input_Descript.Constants", _), []), _)) :: _, ...} = get_obj I pt (fst p)
10.557 +(*-------------------------------------------^^--*)
10.558 +val return_step_by_tactic = (*case*)
10.559 + Step.by_tactic tac (pt, p) (*of*);
10.560 +(*//------------------ step into Step.by_tactic --------------------------------------------\\*)
10.561 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
10.562 +val Applicable.Yes tac' =
10.563 + (*case*) Specify_Step.check tac (pt, p) (*of*);
10.564 + (*if*) Tactic.for_specify' tac' (*then*);
10.565 +Step_Specify.by_tactic tac' ptp;
10.566 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Add_Given' (ct, _)), (pt, p)) = (tac', ptp);
10.567 +
10.568 + Specify.by_Add_ "#Given" ct (pt, p);
10.569 +"~~~~~ fun by_Add_ , args:"; val (m_field, ct, (pt, pos as (_, p_))) = ("#Given", ct, (pt, p));
10.570 + val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos);
10.571 +(* val (i_model, m_patt) =*)
10.572 + (*if*) p_ = Pos.Met (*else*);
10.573 +val return_by_Add_ =
10.574 + (pbl,
10.575 + (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model)
10.576 +val I_Model.Add i_single =
10.577 + (*case*) I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
10.578 +
10.579 + val i_model' =
10.580 + I_Model.add_single (Proof_Context.theory_of ctxt) i_single i_model;
10.581 +"~~~~~ fun add_single , args:"; val (thy, itm, model) =
10.582 + ((Proof_Context.theory_of ctxt), i_single, i_model);
10.583 + fun eq_untouched d (0, _, _, _, itm_) = (d = I_Model.descriptor itm_)
10.584 + | eq_untouched _ _ = false
10.585 + val model' = case I_Model.seek_ppc (#1 itm) model of
10.586 + SOME _ => overwrite_ppc thy itm model (*itm updated in is_notyet_input WN.11.03*)
10.587 +
10.588 +(*||------------------ contine Step.by_tactic ------------------------------------------------*)
10.589 +(*\\------------------ step into Step.by_tactic --------------------------------------------//*)
10.590 +val ("ok", (_, _, ptp)) = return_step_by_tactic;
10.591 +
10.592 + val (pt, p) = ptp;
10.593 + (*case*)
10.594 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
10.595 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
10.596 + (p, ((pt, Pos.e_pos'), []));
10.597 + (*if*) Pos.on_calc_end ip (*else*);
10.598 + val (_, probl_id, _) = Calc.references (pt, p);
10.599 +val _ =
10.600 + (*case*) tacis (*of*);
10.601 + (*if*) probl_id = Problem.id_empty (*else*);
10.602 +
10.603 + switch_specify_solve p_ (pt, ip);
10.604 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
10.605 + (*if*) Pos.on_specification ([], state_pos) (*then*);
10.606 +
10.607 + specify_do_next (pt, input_pos);
10.608 +"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
10.609 + val (_, (p_', tac)) =
10.610 + Specify.find_next_step ptp;
10.611 +"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
10.612 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
10.613 + spec = refs, ...} = Calc.specify_data (pt, pos);
10.614 + val ctxt = Ctree.get_ctxt pt pos;
10.615 +
10.616 +(*+*)val (1, [1, 2, 3], true, "#Given", Cor ((Const ("Input_Descript.Constants", _), ts ), _)) :: _
10.617 + = pbl
10.618 +(*+*)val "[[r = 7]]" = UnparseC.terms @{context} ts;
10.619 +(*-----ML-^------^-HOL*)
10.620 +
10.621 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
10.622 + (*if*) p_ = Pos.Pbl (*then*);
10.623 +
10.624 + for_problem ctxt oris (o_refs, refs) (pbl, met);
10.625 +"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
10.626 + (ctxt, oris, (o_refs, refs), (pbl, met));
10.627 + val cpI = if pI = Problem.id_empty then pI' else pI;
10.628 + val cmI = if mI = MethodC.id_empty then mI' else mI;
10.629 + val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
10.630 + val {model = mpc, ...} = MethodC.from_store ctxt cmI
10.631 +
10.632 + val (preok, _) =
10.633 +Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
10.634 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
10.635 + (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
10.636 +
10.637 + val (_, _, (env_subst, env_eval)) = of_max_variant model_patt i_model;
10.638 +"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
10.639 + val all_variants =
10.640 + map (fn (_, variants, _, _, _) => variants) i_model
10.641 + |> flat
10.642 + |> distinct op =
10.643 + val variants_separated = map (filter_variants' i_model) all_variants
10.644 + val sums_corr = map (cnt_corrects) variants_separated
10.645 + val sum_variant_s = arrange_args sums_corr (1, all_variants)
10.646 + val (_, max_variant) = hd (*..crude decision, up to improvement *)
10.647 + (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
10.648 + val i_model_max =
10.649 + filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
10.650 + val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
10.651 + val env_model = make_env_model equal_descr_pairs
10.652 + val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
10.653 +
10.654 + val subst_eval_list =
10.655 + make_envs_preconds equal_givens;
10.656 +"~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens);
10.657 +val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) =>
10.658 + discern_feedback id feedb)
10.659 +val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 1 equal_givens;
10.660 +"~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor_TEST ((descr, ts), _))) = (id, feedb);
10.661 +
10.662 + discern_typ id (descr, ts);
10.663 +"~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts));
10.664 +(*|------------------- contine me_add_find_Constants -----------------------------------------*)
10.665 +(*\------------------- step into me_add_find_Constants -------------------------------------//*)
10.666 +val (p,_,f,nxt,_,pt) = return_me_add_find_Constants;
10.667 +(*/########################## before destroying elementwise input of lists ##################\* )
10.668 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u]" = nxt;
10.669 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [v]" = nxt;
10.670 +( *\########################## before destroying elementwise input of lists ##################/*)
10.671 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u, v]" = nxt;
10.672 +
10.673 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)" = nxt;
10.674 +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;
10.675 +val return_me_Add_Relation_SideConditions
10.676 + = me nxt p c pt;
10.677 +(*+*)val (_, _, _, Specify_Theory "Diff_App", _, _) = return_me_Add_Relation_SideConditions; (*###############*)
10.678 +(*/------------------- step into me Add_Relation_SideConditions ----------------------------\\*)
10.679 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
10.680 + val ctxt = Ctree.get_ctxt pt p;
10.681 +(**) val (pt, p) = (**)
10.682 + (**)case(**) Step.by_tactic tac (pt, p) (**)of(**)
10.683 +(**) ("ok", (_, _, ptp)) => ptp (**) ;
10.684 +
10.685 + (*case*)
10.686 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
10.687 +(*//------------------ step into do_next ---------------------------------------------------\\*)
10.688 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
10.689 + = (p, ((pt, Pos.e_pos'), [])) (*of*);
10.690 + (*if*) Pos.on_calc_end ip (*else*);
10.691 + val (_, probl_id, _) = Calc.references (pt, p);
10.692 + (*case*) tacis (*of*);
10.693 + (*if*) probl_id = Problem.id_empty (*else*);
10.694 +
10.695 + Step.switch_specify_solve p_ (pt, ip);
10.696 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
10.697 + (*if*) Pos.on_specification ([], state_pos) (*then*);
10.698 + Step.specify_do_next (pt, input_pos);
10.699 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
10.700 +(*isa------ERROR: Refine_Problem INSTEAD
10.701 + isa2: Specify_Theory "Diff_App"*)
10.702 + val (_, (p_', tac as Specify_Theory "Diff_App")) =
10.703 +(*ERROR------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
10.704 + Specify.find_next_step ptp;
10.705 +"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
10.706 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
10.707 + spec = refs, ...} = Calc.specify_data (pt, pos);
10.708 + val ctxt = Ctree.get_ctxt pt pos;
10.709 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
10.710 + (*if*) p_ = Pos.Pbl (*then*);
10.711 +
10.712 +val ("dummy", (Pbl, tac as Specify_Theory "Diff_App")) =
10.713 +(*ERROR------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
10.714 + for_problem ctxt oris (o_refs, refs) (pbl, met);
10.715 +"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
10.716 + (ctxt, oris, (o_refs, refs), (pbl, met));
10.717 + val cpI = if pI = Problem.id_empty then pI' else pI;
10.718 + val cmI = if mI = MethodC.id_empty then mI' else mI;
10.719 + val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
10.720 + val {model = mpc, ...} = MethodC.from_store ctxt cmI
10.721 +
10.722 +(*+*)val [Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
10.723 + Free ("fixes", _)] = where_
10.724 +
10.725 + val (preok, _) =
10.726 + Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
10.727 +(*///----------------- step into check -------------------------------------------------\\*)
10.728 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
10.729 + (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
10.730 +(*+*)val "[0 < fixes]" = pres |> UnparseC.terms @{context}
10.731 +(*+*)val "[\"(#Given, (Constants, fixes))\", \"(#Find, (Maximum, maxx))\", \"(#Find, (AdditionalValues, vals))\", \"(#Relate, (Extremum, extr))\", \"(#Relate, (SideConditions, sideconds))\"]"
10.732 +(*+*) = model_patt |> Model_Pattern.to_string @{context}
10.733 +(*+*)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))]"
10.734 + = i_model |> I_Model.to_string_TEST @{context}
10.735 +
10.736 +val return_of_max_variant as (_, _, (env_subst, env_eval)) =
10.737 + of_max_variant model_patt i_model
10.738 +
10.739 +(*+*)val [(Free ("fixes", T1), Free ("r", T2))] = env_subst (*?!? Const*)
10.740 +(*+*)val Type ("Real.real", []) = T1
10.741 +(*+*)val Type ("Real.real", []) = T2
10.742 +
10.743 +(*+*)val [(Free ("r", T2), Const ("Num.numeral_class.numeral", _) $ _)] = env_eval
10.744 +(*+*)val Type ("Real.real", []) = T2
10.745 +
10.746 +val (_, _, (env_subst, env_eval)) = return_of_max_variant;
10.747 +(*|||----------------- contine check -----------------------------------------------------*)
10.748 + val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
10.749 +
10.750 +(*|||----------------- contine check -----------------------------------------------------*)
10.751 +(*+*)val [(true, Const ("Orderings.ord_class.less", _) $
10.752 + Const ("Groups.zero_class.zero", _) $ Free ("r", _))] = pres_subst
10.753 +
10.754 + val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
10.755 +(*+*)val [(true,
10.756 + Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
10.757 + (Const ("Num.numeral_class.numeral", _) $ _))] = full_subst
10.758 +
10.759 + val evals = map (eval ctxt where_rls) full_subst
10.760 +val return_check_OLD = (foldl and_ (true, map fst evals), pres_subst)
10.761 +(*\\\----------------- step into check -------------------------------------------------\\*)
10.762 +
10.763 + val (preok as true, _) = return_check_OLD
10.764 +(*+---------------^^^^*)
10.765 +(*\\------------------ step into do_next ---------------------------------------------------\\*)
10.766 +(*\------------------- step into me_Add_Relation_SideConditions ----------------------------//*)
10.767 +val (p, _, f, nxt, _, pt) = return_me_Add_Relation_SideConditions
10.768 + val Specify_Theory "Diff_App" = nxt;
10.769 +
10.770 +val return_me_Specify_Theory
10.771 + = me nxt p c pt; val Specify_Problem ["univariate_calculus", "Optimisation"] = #4 return_me_Specify_Theory;
10.772 +(*/------------------- step into me Specify_Theory -----------------------------------------\\*)
10.773 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
10.774 + val ctxt = Ctree.get_ctxt pt p;
10.775 +(* val (pt, p) = *)
10.776 + (*case*) Step.by_tactic tac (pt, p) (*of*);
10.777 +(* ("ok", (_, _, ptp)) => ptp *)
10.778 +val return_Step_by_tactic =
10.779 + Step.by_tactic tac (pt, p);
10.780 +(*//------------------ step into Step_by_tactic --------------------------------------------\\*)
10.781 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
10.782 + (*case*) Specify_Step.check tac (pt, p) (*of*);
10.783 +
10.784 +(*||------------------ contine Step_by_tactic ------------------------------------------------*)
10.785 +(*\\------------------ step into Step_by_tactic --------------------------------------------//*)
10.786 +
10.787 +val ("ok", (_, _, ptp)) = return_Step_by_tactic;
10.788 +(*|------------------- continue me Specify_Theory --------------------------------------------*)
10.789 +
10.790 +val ("ok", (ts as (_, _, _) :: _, _, _)) =
10.791 + (*case*)
10.792 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
10.793 +(*//------------------ step into do_next ---------------------------------------------------\\*)
10.794 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
10.795 + = (p, ((pt, Pos.e_pos'), [])) (*of*);
10.796 + (*if*) Pos.on_calc_end ip (*else*);
10.797 + val (_, probl_id, _) = Calc.references (pt, p);
10.798 +val _ =
10.799 + (*case*) tacis (*of*);
10.800 + (*if*) probl_id = Problem.id_empty (*else*);
10.801 +
10.802 + Step.switch_specify_solve p_ (pt, ip);
10.803 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
10.804 + (*if*) Pos.on_specification ([], state_pos) (*then*);
10.805 +
10.806 + Step.specify_do_next (pt, input_pos);
10.807 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
10.808 + val (_, (p_', tac)) = Specify.find_next_step ptp
10.809 + val ist_ctxt = Ctree.get_loc pt (p, p_);
10.810 + (*case*) tac (*of*);
10.811 +
10.812 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
10.813 +(*+*)val Specify_Theory "Diff_App" = tac;
10.814 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Theory dI), (pt, pos as (_, Pbl)))
10.815 + = (tac, (pt, (p, p_')));
10.816 + val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
10.817 + PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
10.818 + (oris, dI, dI', pI', probl, ctxt)
10.819 + val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
10.820 + val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
10.821 +(*\\------------------ step into do_next ---------------------------------------------------//*)
10.822 +(*\------------------- step into me Specify_Theory -----------------------------------------//*)
10.823 +val (p,_,f,nxt,_,pt) = return_me_Specify_Theory;
10.824 +
10.825 +val return_me_Specify_Problem (* keep for continuing me *)
10.826 + = me nxt p c pt; val Specify_Method ["Optimisation", "by_univariate_calculus"] = #4 return_me_Specify_Problem;
10.827 +(*/------------------- step into me Specify_Problem ----------------------------------------\\*)
10.828 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
10.829 + val ctxt = Ctree.get_ctxt pt p
10.830 +
10.831 +(** ) val ("ok", (_, _, ptp as (pt, p))) =( **)
10.832 +(**) val return_by_tactic =(**) (*case*)
10.833 + Step.by_tactic tac (pt, p) (*of*);
10.834 +(*//------------------ step into by_tactic -------------------------------------------------\\*)
10.835 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
10.836 +
10.837 + (*case*)
10.838 + Step.check tac (pt, p) (*of*);
10.839 +"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
10.840 + (*if*) Tactic.for_specify tac (*then*);
10.841 +
10.842 +Specify_Step.check tac (ctree, pos);
10.843 +"~~~~~ fun check , args:"; val ((Tactic.Specify_Problem pID), (pt, pos as (p, _)))
10.844 + = (tac, (ctree, pos));
10.845 + val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
10.846 + Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
10.847 + => (oris, dI, pI, dI', pI', itms)
10.848 + val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
10.849 +(*\\------------------ step into by_tactic -------------------------------------------------//*)
10.850 +val ("ok", (_, _, ptp as (pt, p))) = return_by_tactic (* kept for continuing me *);
10.851 +
10.852 + (*case*)
10.853 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
10.854 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
10.855 + (*if*) Pos.on_calc_end ip (*else*);
10.856 + val (_, probl_id, _) = Calc.references (pt, p);
10.857 +val _ =
10.858 + (*case*) tacis (*of*);
10.859 + (*if*) probl_id = Problem.id_empty (*else*);
10.860 +
10.861 + Step.switch_specify_solve p_ (pt, ip);
10.862 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
10.863 + (*if*) Pos.on_specification ([], state_pos) (*then*);
10.864 +
10.865 + Step.specify_do_next (pt, input_pos);
10.866 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
10.867 + val (_, (p_', tac)) = Specify.find_next_step ptp
10.868 + val ist_ctxt = Ctree.get_loc pt (p, p_)
10.869 +val _ =
10.870 + (*case*) tac (*of*);
10.871 +
10.872 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
10.873 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos))
10.874 + = (tac, (pt, (p, p_')));
10.875 +
10.876 + val (o_model, ctxt, i_model) =
10.877 +Specify_Step.complete_for id (pt, pos);
10.878 +"~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
10.879 + val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
10.880 + ...} = Calc.specify_data (ctree, pos);
10.881 + val ctxt = Ctree.get_ctxt ctree pos
10.882 + val (dI, _, _) = References.select_input o_refs refs;
10.883 + val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
10.884 + val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
10.885 + val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
10.886 + val thy = ThyC.get_theory ctxt dI
10.887 + val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
10.888 +(*\------------------- step into me Specify_Problem ----------------------------------------//*)
10.889 +val (p,_,f,nxt,_,pt) = return_me_Specify_Problem
10.890 +
10.891 +val return_me_Add_Given_FunctionVariable
10.892 + = me nxt p c pt; val Add_Given "FunctionVariable a" = #4 return_me_Add_Given_FunctionVariable;
10.893 +(*/------------------- step into me Specify_Method -----------------------------------------\\*)
10.894 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
10.895 + val ctxt = Ctree.get_ctxt pt p
10.896 + val (pt, p) =
10.897 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
10.898 + case Step.by_tactic tac (pt, p) of
10.899 + ("ok", (_, _, ptp)) => ptp;
10.900 +
10.901 + (*case*)
10.902 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
10.903 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
10.904 + (*if*) Pos.on_calc_end ip (*else*);
10.905 + val (_, probl_id, _) = Calc.references (pt, p);
10.906 +val _ =
10.907 + (*case*) tacis (*of*);
10.908 + (*if*) probl_id = Problem.id_empty (*else*);
10.909 +
10.910 + Step.switch_specify_solve p_ (pt, ip);
10.911 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
10.912 + (*if*) Pos.on_specification ([], state_pos) (*then*);
10.913 +
10.914 + Step.specify_do_next (pt, input_pos);
10.915 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
10.916 +
10.917 + val (_, (p_', tac)) =
10.918 + Specify.find_next_step ptp;
10.919 +"~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
10.920 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
10.921 + spec = refs, ...} = Calc.specify_data (pt, pos);
10.922 + val ctxt = Ctree.get_ctxt pt pos;
10.923 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
10.924 + (*if*) p_ = Pos.Pbl (*else*);
10.925 +
10.926 + Specify.for_method ctxt oris (o_refs, refs) (pbl, met);
10.927 +"~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (_, met))
10.928 + = (ctxt, oris, (o_refs, refs), (pbl, met));
10.929 + val cmI = if mI = MethodC.id_empty then mI' else mI;
10.930 + val {model, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
10.931 + val (preok, _) = Pre_Conds.check ctxt where_rls where_ (model, I_Model.OLD_to_TEST met);
10.932 +val NONE =
10.933 + (*case*) find_first (I_Model.is_error o #5) met (*of*);
10.934 +
10.935 + (*case*)
10.936 + Specify.item_to_add (ThyC.get_theory ctxt
10.937 + (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
10.938 +"~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
10.939 + = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
10.940 +(*\------------------- step into me Specify_Method -----------------------------------------//*)
10.941 +val (p,_,f,nxt,_,pt) = return_me_Add_Given_FunctionVariable
10.942 +
10.943 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Input_Descript.Domain {0<..<r}" = nxt;
10.944 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "ErrorBound (\<epsilon> = 0)" = nxt;
10.945 +
10.946 +(* ------------------- step into UNTIL A PROGRAM IS REQUIRED (not yet impl. ---------------- )*)
10.947 +\<close> ML \<open>(*/------------- step into me_Add_Given_ErrorBound------------------------------------\\*)
10.948 +(*/------------------- step into me_Add_Given_ErrorBound------------------------------------\\*)
10.949 +"~~~~~ fun me , args:"; val (tac, p, _(*NEW remove*), pt) = (nxt, p, c, pt);
10.950 + val ctxt = Ctree.get_ctxt pt p
10.951 + val (pt, p) =
10.952 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
10.953 + case Step.by_tactic tac (pt, p) of
10.954 + ("ok", (_, _, ptp)) => ptp;
10.955 +(*ERROR due to missing program in creating the environment from formal args* )
10.956 + (*case*)
10.957 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
10.958 +( *ERROR*)
10.959 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis) ) =
10.960 + (p, ((pt, Pos.e_pos'), []));
10.961 + (*if*) Pos.on_calc_end ip (*else*);
10.962 + val (_, probl_id, _) = Calc.references (pt, p);
10.963 +val _ =
10.964 + (*case*) tacis (*of*);
10.965 + (*if*) probl_id = Problem.id_empty (*else*);
10.966 +
10.967 +(*ERROR due to missing program in creating the environment from formal args* )
10.968 + switch_specify_solve p_ (pt, ip);
10.969 +( *ERROR*)
10.970 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
10.971 + (*if*) Pos.on_specification ([], state_pos) (*then*);
10.972 +
10.973 +(*ERROR due to missing program in creating the environment from formal args* )
10.974 + specify_do_next (pt, input_pos)
10.975 +( *ERROR*)
10.976 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
10.977 + val (_, (p_', tac as Apply_Method ["Optimisation", "by_univariate_calculus"])) =
10.978 + (*-------------------^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ not yet impl.*)
10.979 + Specify.find_next_step ptp
10.980 + val ist_ctxt = Ctree.get_loc pt (p, p_)
10.981 +
10.982 +val Tactic.Apply_Method (mI as ["Optimisation", "by_univariate_calculus"]) =
10.983 + (*case*) tac (*of*);
10.984 +(*ERROR due to missing program in creating the environment from formal args* )
10.985 + LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
10.986 + ist_ctxt (pt, (p, p_'))
10.987 +( *ERROR*)
10.988 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
10.989 + ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)), ist_ctxt, (pt, (p, p_')));
10.990 + val (itms, oris, probl) = case get_obj I pt p of
10.991 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
10.992 + val {model, ...} = MethodC.from_store ctxt mI;
10.993 + (*if*) itms <> [] (*then*);
10.994 + val itms = I_Model.complete oris probl [] model
10.995 +
10.996 +(*+*)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] ,true ,#Given ,Cor FunctionVariable a , pen2str), \n(10 ,[1, 2] ,true ,#Given ,Cor Input_Descript.Domain {0<..<r} , pen2str), \n(12 ,[1, 2, 3] ,true ,#Given ,Cor ErrorBound (\<epsilon> = 0) , pen2str)]"
10.997 + = itms |> I_Model.to_string @{context}
10.998 +(*+*)val 8 = length itms
10.999 +(*+*)val 8 = length model
10.1000 +\<close> ML \<open>(*\------------- step into me_Add_Given_ErrorBound------------------------------------//*)
10.1001 +(*\------------------- step into me_Add_Given_ErrorBound------------------------------------//*)
10.1002 +
10.1003
10.1004 \<close> ML \<open>
10.1005 \<close>