prepare 5: clarify three environments in the specify-phase, see (*2*) type env_subst
1.1 --- a/TODO.md Tue Jun 20 06:26:18 2023 +0200
1.2 +++ b/TODO.md Thu Jul 13 10:51:16 2023 +0200
1.3 @@ -52,6 +52,13 @@
1.4
1.5 ***** priority of WN items is top down, most urgent/simple on top
1.6
1.7 +* WN: introduction of I_Model.T_TEST is a huge step, which is partitioned into smaller steps, starting with
1.8 + changeset cb44eefd3c7b "repare 1 PIDE turn 11: .." and continued with "repare 1..n".
1.9 + After changeset 94242a19b04c "prepare 4: narrow I_Model.T -- _TEST" it seems no more possible to make the test(s)
1.10 + in test/../Test_Theory.thy run without braking too many tests. Thus
1.11 + minimal code in src/* is changed and marked by (*T_TESTold*)xxx(*T_TEST* )xxx( *T_TESTnew*)
1.12 + while the outcommenting shown is used for commits (where Test_Isac_Shorts runs without errors,
1.13 + but Test_Theory.thy doen't work).
1.14 * WN: ad CS "remove sep_variants_envs":
1.15 test/../i-model.sml (*/----- reactivate with CS "remove sep_variants_envs"-----\* )
1.16 * WN: DEL get_simplifier: is only used in test/*
2.1 --- a/src/Tools/isac/Specify/i-model.sml Tue Jun 20 06:26:18 2023 +0200
2.2 +++ b/src/Tools/isac/Specify/i-model.sml Thu Jul 13 10:51:16 2023 +0200
2.3 @@ -71,7 +71,9 @@
2.4 val is_complete_variant: int -> T_TEST-> bool
2.5
2.6 val of_max_variant: Model_Pattern.T -> T_TEST -> T_TEST * Pre_Conds.env_subst * Pre_Conds.env_eval
2.7 -
2.8 +(*
2.9 + val of_max_variant: Model_Pattern.T -> T_TEST -> T_TEST * Env.T
2.10 +*)
2.11 (*from isac_test for Minisubpbl*)
2.12 val penv_to_string: Proof.context -> T -> string
2.13
3.1 --- a/src/Tools/isac/Specify/pre-conditions.sml Tue Jun 20 06:26:18 2023 +0200
3.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml Thu Jul 13 10:51:16 2023 +0200
3.3 @@ -39,14 +39,19 @@
3.4 val check_variant_envs: Proof.context -> Rule_Set.T -> unchecked ->
3.5 env_subst -> env_eval -> checked
3.6
3.7 -(*val sep_variants_envs ?can be replaced by? of_max_variant TODO
3.8 - for that purpose compare with sep_variants_envs_OLD TODO*)
3.9 +(*val sep_variants_envs replaced by of_max_variant TODO
3.10 + for that purpose compare with sep_variants_envs_OLD TODO*)
3.11 val sep_variants_envs: Model_Pattern.T -> Model_Def.i_model_TEST ->
3.12 ((Model_Def.i_model_TEST * env_subst * env_eval) * Model_Def.variant) list
3.13 val sep_variants_envs_OLD: Model_Pattern.T -> Model_Def.i_model_TEST ->
3.14 env_subst * env_eval;
3.15 +
3.16 val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
3.17 Model_Def.i_model_TEST * env_subst * env_eval
3.18 +(*
3.19 + val of_max_variant: Model_Pattern.T -> Model_def.i_model_TEST -> Model_def.i_model_TEST * Env.T
3.20 + val mk_envs: Model_def.i_model_TEST -> unchecked -> env_subst * env_eval
3.21 +*)
3.22
3.23 (*from isac_test for Minisubpbl*)
3.24 val discern_feedback_subst: Model_Def.descriptor -> Model_Def.i_model_feedback_TEST -> Env.T;
3.25 @@ -94,8 +99,31 @@
3.26 type checked = bool * (bool * term) list
3.27 type checked_TEST = bool * (bool * (term * Position.T)) list
3.28
3.29 -type env_subst = Env.T (*eg. [(fixes, r)] .. with type adaptation, see switch_type*)
3.30 -type env_eval = Env.T (*eg. [(r, 7) ]*)
3.31 +(*
3.32 + we have three kinds of Env.T in the specification-phase:
3.33 +(*1*) Env.T produced by I_Model.of_max_variant and required to create O_Model.T, I_Model.T from
3.34 + Model_Pattern.T.
3.35 + Env.T / (Constants, fixes) in Model_Pattern.T
3.36 + e.g.[(fixes, [r = 7])] |
3.37 + > (Constants, [r = 7]) in O/I_Model.T *)
3.38 +
3.39 +(*2*) type env_subst = Env.T (* / 0 < fixes in Problem.{where_, ...}
3.40 + eg. [(fixes, r)] |
3.41 + > 0 < r *)
3.42 +(*3*) type env_eval = Env.T (* |
3.43 + eg. [(r, 7)] |
3.44 + > 0 < 7 \<longrightarrow> true
3.45 +
3.46 + (*1*) is required to produce (*2*) and (*3*); thus respective code is shifted to Pre_Conds.
3.47 + (*2*) and (*3*) is produced from I_Model.of_max_variant by restricting to "#Given".
3.48 +
3.49 + There is a typing problem, probably to be solved by a language for Specification in the future:
3.50 + term <fixes> in (*1*) has type "bool list"
3.51 + term <fixes> in (*2*) has type "real". So for the transition from (*1*) to (*2..3*)
3.52 + fun switch_type is required.
3.53 + The transition requires better modelling by a novel language for Specification.
3.54 +*)
3.55 +
3.56 type input = TermC.as_string list;
3.57
3.58 fun to_str ctxt (b, t) = pair2str (bool2str b, UnparseC.term ctxt t);
3.59 @@ -493,6 +521,12 @@
3.60 in
3.61 (i_model_max, env_subst, env_eval)
3.62 end
3.63 +(** )
3.64 +fun of_max_variant model_patt i_model =
3.65 +( **)
3.66 +(** )
3.67 +fun make_envs env_model i_max_variant precond =
3.68 +( **)
3.69
3.70
3.71 (** check pre-conditions **)
4.1 --- a/src/Tools/isac/Specify/specify-step.sml Tue Jun 20 06:26:18 2023 +0200
4.2 +++ b/src/Tools/isac/Specify/specify-step.sml Thu Jul 13 10:51:16 2023 +0200
4.3 @@ -42,6 +42,7 @@
4.4 | check (Tactic.Del_Find ct') _ = Applicable.Yes (Tactic.Del_Find' ct')
4.5 | check (Tactic.Del_Given ct') _ = Applicable.Yes (Tactic.Del_Given' ct')
4.6 | check (Tactic.Del_Relation ct') _ = Applicable.Yes (Tactic.Del_Relation' ct')
4.7 +(*T_TESTold*)
4.8 | check Tactic.Model_Problem (pt, pos as (p, _)) =
4.9 let
4.10 val (pI', ctxt) = case Ctree.get_obj I pt p of
4.11 @@ -50,6 +51,16 @@
4.12 val {model, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
4.13 val pbl = I_Model.init model
4.14 in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
4.15 +(*T_TEST* )
4.16 + | check Tactic.Model_Problem (pt, pos as (p, _)) =
4.17 + let
4.18 + val (o_model, pI') = case Ctree.get_obj I pt p of
4.19 + Ctree.PblObj {origin = (o_model, (_, pI', _), _), ...} => (o_model, pI')
4.20 + | _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj"
4.21 + val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
4.22 + val pbl = I_Model.init_TEST o_model model_patt
4.23 + in Applicable.Yes (Tactic.Model_Problem' (pI', I_Model.TEST_to_OLD pbl, [])) end
4.24 +( *T_TESTnew*)
4.25 | check (Tactic.Refine_Problem pI) (pt, (p, _)) =
4.26 let
4.27 val (dI, dI', itms, ctxt) = case Ctree.get_obj I pt p of
5.1 --- a/test/Tools/isac/Test_Theory.thy Tue Jun 20 06:26:18 2023 +0200
5.2 +++ b/test/Tools/isac/Test_Theory.thy Thu Jul 13 10:51:16 2023 +0200
5.3 @@ -22,8 +22,8 @@
5.4 val return_XXXXX = "XXXXX"
5.5 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
5.6 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
5.7 -\<close> ML \<open> (*------------- contine XXXXX ---------------------------------------------------------*)
5.8 -(*-------------------- contine XXXXX ---------------------------------------------------------*)
5.9 +\<close> ML \<open> (*||----------- contine XXXXX ---------------------------------------------------------*)
5.10 +(*||------------------ contine XXXXX ---------------------------------------------------------*)
5.11 (*\\------------------ step into XXXXX -----------------------------------------------------//*)
5.12 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
5.13 val "XXXXX" = return_XXXXX;
5.14 @@ -72,10 +72,1004 @@
5.15 \<close> ML \<open>
5.16 \<close>
5.17
5.18 -section \<open>===================================================================================\<close>
5.19 -section \<open>===================================================================================\<close>
5.20 +section \<open>====="Minisubpbl/150a-add-given-Maximum.sml"=======================================\<close>
5.21 ML \<open>
5.22 \<close> ML \<open>
5.23 +(* Title: "Minisubpbl/150a-add-given-Maximum.sml"
5.24 + Author: Walther Neuper 1105
5.25 + (c) copyright due to lincense terms.
5.26 +
5.27 +ATTENTION: the file creates buffer overflow if copied in one piece !
5.28 +
5.29 +Note: This test --- steps into me --- more than once, to a somewhat extreme extent;
5.30 + in order not to get lost while working in Test_Some etc,
5.31 + re-introduce ML (*--- step into XXXXX ---*) and Co.
5.32 + and use Sidekick for orientation.
5.33 + Nesting is indicated by /--- //-- ///- at the left margin of the comments.
5.34 +*)
5.35 +
5.36 +open Ctree;
5.37 +open Pos;
5.38 +open TermC;
5.39 +open Istate;
5.40 +open Tactic;
5.41 +open Pre_Conds;
5.42 +open I_Model;
5.43 +open P_Model
5.44 +open Rewrite;
5.45 +open Step;
5.46 +open LItool;
5.47 +open LI;
5.48 +open Test_Code
5.49 +open Specify
5.50 +open ME_Misc
5.51 +
5.52 +val (_(*example text*),
5.53 + (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
5.54 + "Extremum (A = 2 * u * v - u \<up> 2)" ::
5.55 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
5.56 + "SideConditions [((u::real) / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]" ::
5.57 + "SideConditions [(u::real) / 2 = r * sin \<alpha>, 2 / v = r * cos \<alpha>]" ::
5.58 +(*---------------------------------------------,(v::real) / 2 = r * cos \<alpha>]" --- ERROR in eample*)
5.59 + "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \<alpha>" ::
5.60 + "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \<pi> / 2}" ::
5.61 + "ErrorBound (\<epsilon> = (0::real))" :: []),
5.62 + refs as ("Diff_App",
5.63 + ["univariate_calculus", "Optimisation"],
5.64 + ["Optimisation", "by_univariate_calculus"])))
5.65 + = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"];
5.66 +
5.67 +\<close> ML \<open>
5.68 +val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(model, refs)]; (*val Model_Problem = nxt;*)
5.69 +val c = [];
5.70 +
5.71 +\<close> ML \<open>
5.72 +(*+*)val PblObj {ctxt, probl, ...} = get_obj I pt [];
5.73 +(*+*)Proof_Context.theory_of ctxt (*= {Pure, .., Diff_App}*);
5.74 +(*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term ctxt "r"
5.75 +(*+*)val [] = probl
5.76 +(*+-----^^^^*)
5.77 +
5.78 +\<close> text \<open> (*ERROR mk_env not reasonable for "Inc_TEST Constants [] [__=__, __=__]"*)
5.79 +val return_me_Model_Problem =
5.80 + me nxt p c pt; val Add_Given "Constants [r = 7]" = #4 return_me_Model_Problem;
5.81 +\<close> ML \<open> (*/------------ step into me Model_Problem ------------------------------------------\\*)
5.82 +(*/------------------- step into me Model_Problem ------------------------------------------\\*)
5.83 +"~~~~~ fun me , args:"; val (tac, (p:Pos.pos'), (_:Test_Code.NEW), (pt:Ctree.ctree)) = (nxt, p, c, pt);
5.84 + val ctxt = Ctree.get_ctxt pt p
5.85 +val return_by_tactic = case
5.86 + Step.by_tactic tac (pt,p) of
5.87 + ("ok", (_, _, ptp)) => ptp;
5.88 +\<close> ML \<open> (*//----------- step into by_tactic -------------------------------------------------\\*)
5.89 +(*//------------------ step into by_tactic -------------------------------------------------\\*)
5.90 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p));
5.91 +val Applicable.Yes tac' = (*case*)
5.92 + Step.check tac (pt, p) (*of*);
5.93 +(*+*)val Model_Problem' _ = tac';
5.94 +"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
5.95 + (*if*) Tactic.for_specify tac (*then*);
5.96 +
5.97 +Specify_Step.check tac (ctree, pos);
5.98 +"~~~~~ fun check , args:"; val (Tactic.Model_Problem, (pt, pos as (p, _))) =
5.99 + (tac, (ctree, pos));
5.100 + val (o_model, pI', ctxt) = case Ctree.get_obj I pt p of
5.101 + Ctree.PblObj {origin = (o_model, (_, pI', _), _), ctxt, ...} => (o_model, pI', ctxt)
5.102 + val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
5.103 + val pbl = I_Model.init_TEST o_model model_patt;
5.104 +
5.105 +val return_check =
5.106 + Applicable.Yes (Tactic.Model_Problem' (pI', I_Model.TEST_to_OLD pbl, []));
5.107 +(*\\------------------ step into by_tactic -------------------------------------------------//*)
5.108 +\<close> ML \<open> (*\\----------- step into by_tactic -------------------------------------------------//*)
5.109 +val (pt, p) = return_by_tactic;
5.110 +
5.111 +\<close> text \<open> (*ERROR mk_env not reasonable for "Inc_TEST Constants [] [__=__, __=__]"*)
5.112 +val return_do_next = (*case*)
5.113 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
5.114 +val ts = return_do_next |> #2 |> #1 |> hd (* keep for continuing me Model_Problem *)
5.115 +val continue_Model_Problem = (ts, (pt, p)) (* keep for continuing me Model_Problem *);
5.116 +\<close> ML \<open> (*//----------- step into do_next ---------------------------------------------------\\*)
5.117 +(*//------------------ step into do_next ---------------------------------------------------\\*)
5.118 +"~~~~~ fun do_next , args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) =
5.119 + (p, ((pt, e_pos'),[]));
5.120 + val pIopt = get_pblID (pt,ip);
5.121 + (*if*) ip = ([],Res); (* = false*)
5.122 + val _ = (*case*) tacis (*of*);
5.123 + val SOME _ = (*case*) pIopt (*of*);
5.124 +
5.125 +\<close> text \<open> (*ERROR mk_env not reasonable for "Inc_TEST Constants [] [__=__, __=__]"*)
5.126 + val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
5.127 + Step.switch_specify_solve p_ (pt, ip);
5.128 +\<close> ML \<open>
5.129 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
5.130 + (*if*) Pos.on_specification ([], state_pos) (*then*);
5.131 +
5.132 +\<close> text \<open> (*ERROR mk_env not reasonable for "Inc_TEST Constants [] [__=__, __=__]"*)
5.133 + val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) =
5.134 + Step.specify_do_next (pt, input_pos);
5.135 +\<close> ML \<open> (*///---------- step into specify_do_next -------------------------------------------\\*)
5.136 +(*///----------------- step into specify_do_next -------------------------------------------\\*)
5.137 +"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
5.138 +
5.139 +\<close> text \<open> (*ERROR mk_env not reasonable for "Inc_TEST Constants [] [__=__, __=__]"*)
5.140 +(* val (_, (p_', tac)) =*)
5.141 +val return_find_next_step = (*keep for continuing specify_do_next*)
5.142 + Specify.find_next_step ptp;
5.143 +\<close> ML \<open> (*////--------- step into find_next_step --------------------------------------------\\*)
5.144 +(*////---------------- step into find_next_step --------------------------------------------\\*)
5.145 +"~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
5.146 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
5.147 + spec = refs, ...} = Calc.specify_data (pt, pos);
5.148 + val ctxt = Ctree.get_ctxt pt pos;
5.149 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
5.150 + (*if*) p_ = Pos.Pbl (*then*);
5.151 +
5.152 +\<close> ML \<open> (*/////-------- step into for_problem -----------------------------------------------\\*)
5.153 +(*/////--------------- step into for_problem -----------------------------------------------\\*)
5.154 +\<close> text \<open> (*ERROR mk_env not reasonable for "Inc_TEST Constants [] [__=__, __=__]"*)
5.155 + Specify.for_problem ctxt oris (o_refs, refs) (pbl, met);
5.156 +\<close> ML \<open>
5.157 +"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
5.158 + = (ctxt, oris, (o_refs, refs), (pbl, met));
5.159 + val cpI = if pI = Problem.id_empty then pI' else pI;
5.160 + val cmI = if mI = MethodC.id_empty then mI' else mI;
5.161 + val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
5.162 + val {model = mpc, ...} = MethodC.from_store ctxt cmI
5.163 +\<close> ML \<open> (*//----------- adhoc inserted fun of_max_variant -----------------------------------\\*)
5.164 +(*//------------------ adhoc inserted fun of_max_variant -----------------------------------\\*)
5.165 +\<close> ML \<open>
5.166 +(*+*)val ttt = @{term "[r=(7::real)]"}
5.167 +(*+*)val (Const ("List.list.Cons", _) $ _ $ Const ("List.list.Nil", xxx)) = ttt
5.168 +(*+*)val Type ("List.list", [Type ("HOL.bool", [])]) = xxx
5.169 +\<close> ML \<open>
5.170 +fun element_typ (Const ("List.list.Cons", _) $ _ $
5.171 + Const ("List.list.Nil", Type ("List.list", [typ]))) = typ
5.172 + | element_typ t = type_of t
5.173 +;
5.174 +element_typ: term -> typ
5.175 +\<close> ML \<open>
5.176 +fun element_typ_ML [] = TermC.typ_empty
5.177 + | element_typ_ML (e :: _) =
5.178 +(**) if TermC.is_list e (*go sure during transition, delete afterwards*)
5.179 + then element_typ e
5.180 + else (**) type_of e
5.181 +;
5.182 +element_typ_ML: term list -> typ
5.183 +\<close> ML \<open>
5.184 +(*+*)val ts = [@{term "u::real"}, @{term "v::real"}];
5.185 +(*+*)val Type ("Real.real", []) = element_typ_ML ts;
5.186 +\<close> ML \<open>
5.187 +(*+*)TermC.list2isalist (element_typ_ML ts) ts
5.188 +\<close> ML \<open>
5.189 +\<close> ML \<open>
5.190 +\<close> ML \<open> (*GOON*)
5.191 +\<close> ML \<open>
5.192 +TermC.list2isalist: typ -> term list -> term;
5.193 +\<close> ML \<open>
5.194 +val true = TermC.is_list @{term "[r=7]"}
5.195 +\<close> ML \<open>
5.196 +fun list2isalist' ts =
5.197 +(**) if TermC.is_list ts (*go sure during transition, delete afterwards*)
5.198 + then TermC.list2isalist (element_typ_ML ts) ts
5.199 + else (**) TermC.list2isalist (element_typ_ML ts) ts
5.200 +;
5.201 +list2isalist'
5.202 +\<close> ML \<open>
5.203 +\<close> ML \<open>
5.204 +fun mk_env_mod id (Model_Def.Cor_TEST ((descr, ts), _)) = [(id, list2isalist' ts)]
5.205 +\<close> ML \<open>
5.206 +mk_env_mod: term -> Model_Def.i_model_feedback_TEST -> (term * term list) list
5.207 +(*We NEED -------------------------------------------> Env.T: (term * term) list*)
5.208 +\<close> ML \<open>
5.209 +(* mk_env_subst_DEL REPLACED BY--vvv THUS mk_env_subst_DEL IS UNCHANGED*)
5.210 +fun mk_env_model equal_descr_pairs =
5.211 + map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
5.212 + => (mk_env_mod id feedb)) equal_descr_pairs
5.213 + |> flat
5.214 +;
5.215 +mk_env_model: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> (term * term list) list
5.216 +(*We NEED -------------------------------------------------------------> Env.T: (term * term) list*)
5.217 +\<close> ML \<open>
5.218 +fun of_max_variant model_patt i_model =
5.219 + let
5.220 + val all_variants =
5.221 + map (fn (_, variants, _, _, _) => variants) i_model
5.222 + |> flat
5.223 + |> distinct op =
5.224 + val variants_separated = map (filter_variants' i_model) all_variants
5.225 + val sums_corr = map (cnt_corrects) variants_separated
5.226 + val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
5.227 + val (_, max_variant) = hd (*..crude decision, up to improvement *)
5.228 + (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
5.229 + val i_model_max =
5.230 + filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
5.231 + val equal_descr_pairs =
5.232 + map (get_equal_descr i_model) model_patt |> flat
5.233 + val env_model = mk_env_subst_DEL equal_descr_pairs
5.234 + in
5.235 + (i_model_max, env_model)
5.236 + end
5.237 +;
5.238 +of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST -> Model_Def.i_model_TEST * Env.T
5.239 +\<close> ML \<open>
5.240 +fun elment_type _ = 123
5.241 +\<close> ML \<open>
5.242 +Inc_TEST
5.243 +\<close> ML \<open>
5.244 +\<close> ML \<open>
5.245 +\<close> ML \<open>
5.246 +\<close> ML \<open>
5.247 +fun make_envs env_model i_max_variant precond = ([], [])
5.248 +;
5.249 +make_envs: Model_Def.i_model_TEST -> Env.T -> unchecked -> env_subst * env_eval
5.250 +\<close> ML \<open>
5.251 +fun check_OLD _ _ [] _ = (true, [])
5.252 + | check_OLD ctxt where_rls pres (model_patt, i_model) =
5.253 + let
5.254 +(** ) val (env_subst, env_eval) = sep_variants_envs_OLD model_patt i_model ( *OLD*)
5.255 +(*NEW*)
5.256 + val (i_max_variant, env_model) = of_max_variant model_patt i_model
5.257 + val (env_subst, env_eval) = make_envs i_max_variant env_model pres
5.258 +(*NEW*)
5.259 + val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
5.260 + val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
5.261 + val evals = map (eval ctxt where_rls) full_subst
5.262 + in
5.263 + (foldl and_ (true, map fst evals), pres_subst)
5.264 + end;
5.265 +(*\\------------------ adhoc inserted fun check_OLD ----------------------------------------//*)
5.266 +\<close> ML \<open> (*\\----------- adhoc inserted fun check_OLD ----------------------------------------//*)
5.267 +\<close> text \<open> (*ERROR mk_env not reasonable for "Inc_TEST Constants [] [__=__, __=__]"*)
5.268 + val return_check_OLD =
5.269 + Pre_Conds.check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
5.270 +\<close> ML \<open> (*//////------- step into check_OLD -------------------------------------------------\\*)
5.271 +(*//////-------------- step into check_OLD -------------------------------------------------\\*)
5.272 +"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
5.273 + (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
5.274 +\<close> text \<open> (*ERROR discern_feedback_subst not reasonable for "Inc_TEST Constants [] [__=__, __=__]"*)
5.275 + val return_of_max_variant =
5.276 + of_max_variant model_patt i_model
5.277 +\<close> ML \<open> (*///// //----- step into of_max_variant --------------------------------------------\\*)
5.278 +(*///// //------------ step into of_max_variant --------------------------------------------\\*)
5.279 +"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) =
5.280 + (model_patt, i_model);
5.281 +
5.282 +\<close> ML \<open> (*with NEW code*)
5.283 +(*+*)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))]"
5.284 + = i_model |> I_Model.to_string_TEST @{context}
5.285 +\<close> text \<open> (*with OLD code*)
5.286 +(*+*)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))]"
5.287 + = i_model |> I_Model.to_string_TEST @ {context}
5.288 +\<close> ML \<open>
5.289 +
5.290 + val all_variants =
5.291 + map (fn (_, variants, _, _, _) => variants) i_model
5.292 + |> flat
5.293 + |> distinct op =
5.294 + val variants_separated = map (filter_variants' i_model) all_variants
5.295 + val sums_corr = map (cnt_corrects) variants_separated
5.296 +\<close> ML \<open>
5.297 + val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
5.298 +\<close> ML \<open> (*with NEW code*)
5.299 +(*+*)val [(0, 1), (0, 2), (0, 3)] = sum_variant_s
5.300 +\<close> ML \<open>
5.301 + val (_, max_variant) = hd (*..crude decision, up to improvement *)
5.302 + (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
5.303 +\<close> ML \<open>
5.304 + val i_model_max =
5.305 + filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
5.306 + val i_model_max =
5.307 + filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
5.308 + val equal_descr_pairs =
5.309 + map (get_equal_descr i_model) model_patt
5.310 + |> flat
5.311 +\<close> text \<open> (*ERROR discern_feedback_subst not reasonable for "Inc_TEST Constants [] [__=__, __=__]"*)
5.312 + val env_model =
5.313 + mk_env_subst_DEL equal_descr_pairs;
5.314 +\<close> ML \<open> (*///// ///---- step into mk_env_subst_DEL ------------------------------------------\\*)
5.315 +(*///// ///----------- step into mk_env_subst_DEL ------------------------------------------\\*)
5.316 +"~~~~~ fun mk_env_subst_DEL , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
5.317 +
5.318 +val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
5.319 + => (discern_feedback_subst id feedb));
5.320 +\<close> ML \<open>
5.321 +val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 1 equal_descr_pairs;
5.322 +\<close> ML \<open>
5.323 +"~~~~~ fun discern_feedback_subst , args:"; val (id, (Model_Def.Inc_TEST ((descr, (*OLD* )[ts]
5.324 + ( *NEW*)ts(*NEW*)), _)) ) =
5.325 + (id, feedb);
5.326 +\<close> ML \<open>
5.327 +\<close> ML \<open>
5.328 +\<close> ML \<open>
5.329 +\<close> ML \<open>
5.330 +\<close> ML \<open>
5.331 +\<close> ML \<open>
5.332 +\<close> ML \<open>
5.333 +\<close> ML \<open>
5.334 +\<close> ML \<open>
5.335 +\<close> ML \<open>
5.336 +\<close> ML \<open>
5.337 +\<close> ML \<open> (*|||||||------ contine of_max_variant ------------------------------------------------*)
5.338 +(*|||||||------------- of_max_variant ------------------------------------------------*)
5.339 +\<close> text \<open> (*ERROR (env_model) has not been declared*)
5.340 + val return_of_max_variant = (i_model_max, env_model);
5.341 +\<close> ML \<open>
5.342 +"~~~~~ fun mk_env_eval_DEL , args:"; val (i_singles) = (i_model_max);
5.343 +
5.344 +val xxx =
5.345 + (fn (_, _, _, _, (feedb, _)) =>
5.346 + discern_feedback_eval feedb)
5.347 +val (_, _, _, _, (feedb, _)) = nth 1 i_singles;
5.348 +"~~~~~ fun discern_feedback_eval , args:"; val ((Model_Def.Inc_TEST ((descr, []), _))) =
5.349 + (feedb);
5.350 +val return_ = []
5.351 +(*\\\\\\\------------- step into of_max_variant --------------------------------------------//*)
5.352 +\<close> ML \<open> (*\\\\\\\------ step into of_max_variant --------------------------------------------//*)
5.353 +val (_, env_subst, env_eval) = return_of_max_variant;
5.354 +\<close> ML \<open> (*||||||------- contine check_OLD -----------------------------------------------------*)
5.355 +(*||||||-------------- contine check_OLD -----------------------------------------------------*)
5.356 + val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
5.357 + val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
5.358 + val evals = map (eval ctxt where_rls) full_subst
5.359 +val return_ = (i_model_max, env_subst, env_eval)
5.360 +(*\\\\\\\------------- step into check_OLD -------------------------------------------------//*)
5.361 +\<close> ML \<open> (*\\\\\\------- step into check_OLD -------------------------------------------------//*)
5.362 +val (preok, _) = return_check_OLD;
5.363 +\<close> ML \<open> (*|||||-------- contine for_problem ---------------------------------------------------*)
5.364 +(*|||||--------------- contine for_problem ---------------------------------------------------*)
5.365 + (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*);
5.366 + (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*);
5.367 +val NONE =
5.368 + (*case*) find_first (I_Model.is_error o #5) pbl (*of*);
5.369 +
5.370 + (*case*)
5.371 + Specify.item_to_add (ThyC.get_theory ctxt
5.372 + (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl (*of*);
5.373 +"~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
5.374 + = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, pbt, pbl);
5.375 + fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
5.376 + | false_and_not_Sup (_, _, false, _, _) = true
5.377 + | false_and_not_Sup _ = false
5.378 +
5.379 + val v = if itms = [] then 1 else Pre_Conds.max_variant itms
5.380 + val vors = if v = 0 then oris
5.381 + else filter ((fn variant =>
5.382 + fn (_, variants, m_field, _, _) => member op= variants variant andalso m_field <> "#undef")
5.383 + v) oris
5.384 +
5.385 +(*+*)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]\"])]"
5.386 +(*+*) = vors |> O_Model.to_string @{context}
5.387 +
5.388 + val vits = if v = 0 then itms (* because of dsc without dat *)
5.389 + else filter ((fn variant =>
5.390 + fn (_, variants, _, _, _) => member op= variants variant)
5.391 + v) itms; (* itms..vat *)
5.392 +
5.393 + val icl = filter false_and_not_Sup vits; (* incomplete *)
5.394 +
5.395 + (*if*) icl = [] (*else*);
5.396 +(*+*)val "[\n(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] ,(Constants, [])), \n(2 ,[1, 2, 3] ,false ,#Find ,Inc Maximum ,(Maximum, [])), \n(3 ,[1, 2, 3] ,false ,#Find ,Inc AdditionalValues [] ,(AdditionalValues, [])), \n(4 ,[1, 2, 3] ,false ,#Relate ,Inc Extremum ,(Extremum, [])), \n(5 ,[1, 2] ,false ,#Relate ,Inc SideConditions [] ,(SideConditions, []))]"
5.397 +(*+*) = icl |> I_Model.to_string @{context}
5.398 +(*+*)val "(1 ,[1, 2, 3] ,false ,#Given ,Inc Constants [] ,(Constants, []))"
5.399 +(*+*) = hd icl |> I_Model.single_to_string @{context}
5.400 +
5.401 +(*++*)val feedback = (fn (_, _, _, _, feedback) => feedback) (hd icl)
5.402 +(*++*)val Const ("Input_Descript.Constants", _) = I_Model.descriptor feedback
5.403 +(*++*)val [] = I_Model.o_model_values feedback
5.404 +
5.405 +(*+*)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]\"])]"
5.406 +(*+*) = vors |> O_Model.to_string @{context}
5.407 +
5.408 +val SOME ori =
5.409 + (*case*) find_first ((fn (_, _, _, _, feedback) => fn (_, _, _, d, ts) =>
5.410 + d = I_Model.descriptor feedback andalso subset op = (I_Model.o_model_values feedback, ts))
5.411 + (hd icl)) vors (*of*);
5.412 +
5.413 +(*+*)val "(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"])" =
5.414 +(*+*) ori |> O_Model.single_to_string @{context}
5.415 +\<close> ML \<open> (*\\\\\-------- step into for_problem -----------------------------------------------//*)
5.416 +(*\\\\\--------------- step into for_problem -----------------------------------------------//*)
5.417 +\<close> ML \<open> (*\\\\--------- step into find_next_step --------------------------------------------//*)
5.418 +(*\\\\---------------- step into find_next_step --------------------------------------------//*)
5.419 +\<close> ML \<open> (*|||---------- continuing specify_do_next --------------------------------------------*)
5.420 +(*|||----------------- continuing specify_do_next --------------------------------------------*)
5.421 +val (_, (p_', tac)) = return_find_next_step (*kept for continuing specify_do_next*)
5.422 +
5.423 + val ist_ctxt = Ctree.get_loc pt (p, p_)
5.424 +
5.425 +(*+*)val Add_Given "Constants [r = 7]" = tac
5.426 +val _ =
5.427 + (*case*) tac (*of*);
5.428 +
5.429 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
5.430 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) =
5.431 + (tac, (pt, (p, p_')));
5.432 +
5.433 + Specify.by_Add_ "#Given" ct ptp;
5.434 +"~~~~~ fun by_Add_ , args:"; val (m_field, ct ,(pt, pos as (_, p_))) =
5.435 + ("#Given", ct, ptp);
5.436 + val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos)
5.437 + val (i_model, m_patt) =
5.438 + if p_ = Pos.Met then
5.439 + (met,
5.440 + (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model)
5.441 + else
5.442 + (pbl,
5.443 + (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model);
5.444 +
5.445 + (*case*)
5.446 + I_Model.check_single ctxt m_field oris i_model m_patt ct (*of*);
5.447 +"~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, (str(*, pos*))) =
5.448 + (ctxt, m_field, oris, i_model, m_patt, ct);
5.449 + val (t as (descriptor $ _)) = Syntax.read_term ctxt str
5.450 +
5.451 +(*+*)val "Constants [r = 7]" = UnparseC.term @{context} t;
5.452 +
5.453 + val SOME m_field' =
5.454 + (*case*) Model_Pattern.get_field descriptor m_patt (*of*);
5.455 + (*if*) m_field <> m_field' (*else*);
5.456 +
5.457 +(*+*)val "#Given" = m_field; val "#Given" = m_field'
5.458 +
5.459 +val ("", ori', all) =
5.460 + (*case*) O_Model.contains ctxt m_field o_model t (*of*);
5.461 +
5.462 +(*+*)val (_, _, _, _, vals) = hd o_model;
5.463 +(*+*)val "Constants [r = 7]" = UnparseC.term @{context} (@{term Constants} $ (hd vals));
5.464 +(*+*)if "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), " ^
5.465 +(*+*) "\n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), " ^
5.466 +(*+*) "\n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), " ^
5.467 +(*+*) "\n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \<up> 2\"]), " ^
5.468 +(*+*) "\n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]\"]), " ^
5.469 +(*+*) "\n(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \<alpha>]\", \"[2 / v = r * cos \<alpha>]\"]), " ^
5.470 +(*+*) "\n(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), " ^
5.471 +(*+*) "\n(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #undef, FunctionVariable, [\"\<alpha>\"]), " ^
5.472 +(*+*) "\n(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<..<r}\"]), " ^
5.473 +(*+*) "\n(11, [\"3\"], #undef, Input_Descript.Domain, [\"{0<..<\<pi> / 2}\"]), " ^
5.474 +(*+*) "\n(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\<epsilon> = 0\"])]"
5.475 +(*+*)= O_Model.to_string @{context} o_model then () else error "o_model CHANGED";
5.476 +
5.477 + (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*);
5.478 +"~~~~~ fun is_notyet_input , args:"; val (ctxt, itms, all, (i, v, f, d, ts), pbt) =
5.479 + (ctxt, i_model, all, ori', m_patt);
5.480 +val SOME (_, (_, pid)) =
5.481 + (*case*) find_first (eq1 d) pbt (*of*);
5.482 +(*local*)fun eq3 f d (_, _, _, f', itm_) = f = f' andalso d = (I_Model.descriptor itm_);(*local*)
5.483 +val SOME (_, _, _, _, itm_) =
5.484 + (*case*) find_first (eq3 f d) itms (*of*);
5.485 +val ts' = inter op = (o_model_values itm_) ts;
5.486 + (*if*) subset op = (ts, ts') (*else*);
5.487 +val return_is_notyet_input = ("",
5.488 + ori_2itm itm_ pid all (i, v, f, d, subtract op = ts' ts));
5.489 +"~~~~~ fun ori_2itm , args:"; val (itm_, pid, all, (id, vt, fd, d, ts)) =
5.490 + (itm_, pid, all, (i, v, f, d, subtract op = ts' ts));
5.491 + val ts' = union op = (o_model_values itm_) ts;
5.492 + val pval = [Input_Descript.join'''' (d, ts')]
5.493 + val complete = if eq_set op = (ts', all) then true else false
5.494 +
5.495 +(*+*)val "Inc Constants [] ,(Constants, [])" = itm_ |> I_Model.feedback_to_string @{context}
5.496 +\<close> ML \<open> (*\\\---------- step into specify_do_next -------------------------------------------//*)
5.497 +(*\\\----------------- step into specify_do_next -------------------------------------------//*)
5.498 +\<close> ML \<open> (*\\----------- step into do_next ---------------------------------------------------//*)
5.499 +(*\\------------------ step into do_next ---------------------------------------------------//*)
5.500 +
5.501 +\<close> ML \<open>(*|------------- continue with me_Model_Problem ----------------------------------------*)
5.502 +(*|------------------- continue with me_Model_Problem ----------------------------------------*)
5.503 +val (ts, (pt, p)) = continue_Model_Problem;
5.504 +val ("ok", (ts as (_, _, _) :: _, _, _)) = return_do_next
5.505 +
5.506 +val tacis as (_::_) =
5.507 + (*case*) ts (*of*);
5.508 + val (tac, _, _) = last_elem tacis
5.509 +
5.510 +val return_Model_Problem = (p, [] : NEW,
5.511 + TESTg_form ctxt (pt, p), tac, Celem.Sundef, pt);
5.512 +\<close> ML \<open> (*//----------- step into TESTg_form ------------------------------------------------\\*)
5.513 +(*//------------------ step into TESTg_form ------------------------------------------------\\*)
5.514 +"~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt, p));
5.515 +
5.516 + val (form, _, _) =
5.517 + ME_Misc.pt_extract ctxt ptp;
5.518 +"~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_(*Frm,Pbl*)))) = (ctxt, ptp);
5.519 + val ppobj = Ctree.get_obj I pt p
5.520 + val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p;
5.521 + (*if*) Ctree.is_pblobj ppobj (*then*);
5.522 +
5.523 + pt_model ppobj p_;
5.524 +"~~~~~ fun pt_model , args:"; val ( (Ctree.PblObj {probl, origin = (_, spec', hdl), spec, ctxt, ...}), _(*Frm,Pbl*)) =
5.525 + (ppobj, p_);
5.526 + (*if*) probl = [] (*else*);
5.527 + val (_, pI, _) = Ctree.get_somespec' spec spec';
5.528 + (*if*) pI = Problem.id_empty (*else*);
5.529 + val {model, where_rls, where_, ...} = Problem.from_store ctxt pI
5.530 + val (_, where_) =
5.531 + Pre_Conds.check_OLD ctxt where_rls where_ (model, I_Model.OLD_to_TEST probl)
5.532 + val allcorrect = I_Model.is_complete probl andalso foldl and_ (true, (map #1 where_))
5.533 +val return_pt_model = Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, where_, spec)
5.534 +\<close> ML \<open>(*|------------- continue with TESTg_form ----------------------------------------------*)
5.535 +(*|------------------- continue with TESTg_form ----------------------------------------------*)
5.536 +val Ctree.ModSpec (spec as (_, p_, _, gfr, where_, _)) =
5.537 + (*case*) form (*of*);
5.538 + (*if*) Specification_Def.is_empty spec (*else*);
5.539 + Test_Out.PpcKF ( (Test_Out.Problem [],
5.540 + P_Model.from (Proof_Context.theory_of ctxt) gfr where_));
5.541 +
5.542 + P_Model.from (Proof_Context.theory_of ctxt) gfr where_;
5.543 +"~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
5.544 + fun coll model [] = model
5.545 + | coll model ((_, _, _, field, itm_) :: itms) =
5.546 + coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms;
5.547 +
5.548 + val gfr = coll P_Model.empty itms;
5.549 +"~~~~~ fun coll , args:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: itms))
5.550 + = (P_Model.empty, itms);
5.551 +
5.552 +(*+*)val 4 = length itms;
5.553 +(*+*)val itm = nth 1 itms;
5.554 +
5.555 + coll P_Model.empty [itm];
5.556 +"~~~~~ fun coll , iterate:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: []))
5.557 + = (P_Model.empty, [itm]);
5.558 +
5.559 + (add_sel_ppc thy field model (item_from_feedback thy itm_));
5.560 +"~~~~~ fun add_sel_ppc , args:"; val ((_: theory), sel, {Given = gi, Where = wh, Find = fi, With = wi, Relate = re}, x )
5.561 + = (thy, field, model, (item_from_feedback thy itm_));
5.562 +
5.563 + P_Model.item_from_feedback thy itm_;
5.564 +"~~~~~ fun item_from_feedback , args:"; val (thy, (I_Model.Inc ((d, ts), _))) = (thy, itm_);
5.565 + P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)));
5.566 +(*\\------------------ step into TESTg_form ------------------------------------------------//*)
5.567 +\<close> ML \<open> (*\\----------- step into TESTg_form ------------------------------------------------//*)
5.568 +\<close> ML \<open> (*\------------ step into me Model_Problem ------------------------------------------//*)
5.569 +(*\------------------- step into me Model_Problem ------------------------------------------//*)
5.570 +val (p, _, f, nxt, _, pt) = return_me_Model_Problem
5.571 +
5.572 +\<close> ML \<open> (*------------- contine me's ----------------------------------------------------------*)
5.573 +(*-------------------- contine me's ----------------------------------------------------------*)
5.574 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Maximum A" = nxt;
5.575 +
5.576 +(*/########################## before destroying elementwise input of lists ##################\* )
5.577 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u]" = nxt;
5.578 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [v]" = nxt;
5.579 +( *\########################## before destroying elementwise input of lists ##################/*)
5.580 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u, v]" = nxt;
5.581 +
5.582 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)" = nxt;
5.583 +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;
5.584 +val return_me_Add_Relation_SideConditions
5.585 + = me nxt p c pt;
5.586 +
5.587 +\<close> ML \<open>
5.588 +\<close> ML \<open>(*/------------- step into me Add_Relation_SideConditions ----------------------------\\*)
5.589 +(*/------------------- step into me Add_Relation_SideConditions ----------------------------\\*)
5.590 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
5.591 + val ctxt = Ctree.get_ctxt pt p
5.592 + val (pt, p) =
5.593 + case Step.by_tactic tac (pt, p) of
5.594 + ("ok", (_, _, ptp)) => ptp;
5.595 + (*case*)
5.596 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
5.597 +\<close> ML \<open> (*//----------- step into do_next ---------------------------------------------------\\*)
5.598 +(*//------------------ step into do_next ---------------------------------------------------\\*)
5.599 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
5.600 + = (p, ((pt, Pos.e_pos'), [])) (*of*);
5.601 + (*if*) Pos.on_calc_end ip (*else*);
5.602 + val (_, probl_id, _) = Calc.references (pt, p);
5.603 + (*case*) tacis (*of*);
5.604 + (*if*) probl_id = Problem.id_empty (*else*);
5.605 +
5.606 + Step.switch_specify_solve p_ (pt, ip);
5.607 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
5.608 + (*if*) Pos.on_specification ([], state_pos) (*then*);
5.609 + Step.specify_do_next (pt, input_pos);
5.610 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
5.611 +
5.612 +\<close> ML \<open> (*isa------ERROR: Refine_Problem INSTEAD
5.613 + isa2: Specify_Theory "Diff_App"*)
5.614 + val (_, (p_', tac as Refine_Problem ["univariate_calculus", "Optimisation"])) =
5.615 + Specify.find_next_step ptp;
5.616 +\<close> ML \<open>
5.617 +"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
5.618 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
5.619 + spec = refs, ...} = Calc.specify_data (pt, pos);
5.620 + val ctxt = Ctree.get_ctxt pt pos;
5.621 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
5.622 + (*if*) p_ = Pos.Pbl (*then*);
5.623 +\<close> ML \<open>
5.624 +\<close> ML \<open> (*isa: ERROR Refine_Problem INSTEAD
5.625 +DEL-----------isa2: Specify_Theory "Diff_App" #########################*)
5.626 +val ("dummy", (Pbl, Refine_Problem ["univariate_calculus", "Optimisation"])) =
5.627 + for_problem ctxt oris (o_refs, refs) (pbl, met);
5.628 +\<close> ML \<open>
5.629 +"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
5.630 + (ctxt, oris, (o_refs, refs), (pbl, met));
5.631 + val cpI = if pI = Problem.id_empty then pI' else pI;
5.632 + val cmI = if mI = MethodC.id_empty then mI' else mI;
5.633 + val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
5.634 + val {model = mpc, ...} = MethodC.from_store ctxt cmI
5.635 +
5.636 +(*+*)val [Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
5.637 + Free ("fixes", _)] = where_
5.638 +
5.639 +\<close> ML \<open>
5.640 + val (preok, _) = (*Pre_Conds.check_OLD \<longrightarrow> isa2: true*)
5.641 +Pre_Conds.check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
5.642 +\<close> ML \<open> (*///---------- step into check_OLD -------------------------------------------------\\*)
5.643 +(*///----------------- step into check_OLD -------------------------------------------------\\*)
5.644 +"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
5.645 + (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
5.646 +\<close> ML \<open>
5.647 +(*+*)val "[0 < fixes]" = pres |> UnparseC.terms @{context}
5.648 +(*+*)val "[\"(#Given, (Constants, fixes))\", \"(#Find, (Maximum, maxx))\", \"(#Find, (AdditionalValues, vals))\", \"(#Relate, (Extremum, extr))\", \"(#Relate, (SideConditions, sideconds))\"]"
5.649 +(*+*) = model_patt |> Model_Pattern.to_string @{context}
5.650 +\<close> ML \<open> (*isa*)
5.651 +(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] ,(fixes, [[r = 7]]), Position.T)), \n(2, [1, 2, 3], true ,#Find, (Cor_TEST Maximum A ,(maxx, [A]), Position.T)), \n(3, [1, 2, 3], true ,#Find, (Cor_TEST AdditionalValues [u, v] ,(vals, [[u, v]]), Position.T)), \n(4, [1, 2, 3], true ,#Relate, (Cor_TEST Extremum (A = 2 * u * v - u \<up> 2) ,(extr, [A = 2 * u * v - u \<up> 2]), Position.T)), \n(5, [1, 2], true ,#Relate, (Cor_TEST SideConditions [(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2] ,(sideconds, [[(u / 2) \<up> 2 + (2 / v) \<up> 2 = r \<up> 2]]), Position.T))]"
5.652 +(*+*) = i_model |> I_Model.to_string_TEST @{context}
5.653 +\<close> ML \<open> (*isa2* )
5.654 +(*+*)val "[\n(0 ,[] ,false ,#Given ,Inc Constants [] ,(??.empty, [])), \n(0 ,[] ,false ,#Find ,Inc Maximum ,(??.empty, [])), \n(0 ,[] ,false ,#Find ,Inc AdditionalValues [] ,(??.empty, [])), \n(0 ,[] ,false ,#Relate ,Inc Extremum ,(??.empty, [])), \n(0 ,[] ,false ,#Relate ,Inc SideConditions [] ,(??.empty, []))]"
5.655 +(*+*) = i_model |> I_Model.to_string @{context}( *+*)
5.656 +\<close> ML \<open>
5.657 +val return_of_max_variant as (_, env_subst, env_eval) =
5.658 + of_max_variant model_patt i_model true
5.659 +\<close> ML \<open> (*////--------- step into of_max_variant --------------------------------------------//*)
5.660 +(*////---------------- step into of_max_variant --------------------------------------------//*)
5.661 +\<close> ML \<open>
5.662 +(*-NO------vvvvvvvvvvvvvv_OLD, _TEST, DEL*)
5.663 +"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model, restrict_to_given) =
5.664 + (model_patt, i_model, true);
5.665 +\<close> ML \<open>
5.666 + val all_variants =
5.667 + map (fn (_, variants, _, _, _) => variants) i_model
5.668 + |> flat
5.669 + |> distinct op =
5.670 + val variants_separated = map (filter_variants' i_model) all_variants
5.671 + val sums_corr = map (cnt_corrects) variants_separated
5.672 + val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
5.673 + val (_, max_variant) = hd (*..crude decision, up to improvement *)
5.674 + (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
5.675 + val i_model_max =
5.676 + filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
5.677 + val i_model_max =
5.678 + if restrict_to_given
5.679 + then (filter (fn ((_, _, _, m_field, (_, _))) => m_field = "#Given") ) i_model_max
5.680 + else i_model_max
5.681 + val equal_descr_pairs =
5.682 + map (get_equal_descr i_model_max) model_patt
5.683 + |> flat
5.684 +\<close> ML \<open>
5.685 + val env_subst =
5.686 + mk_env_subst_DEL equal_descr_pairs
5.687 +\<close> ML \<open>
5.688 +(*+*)val "[\"\n(fixes, [r = 7])\"]" = env_subst |> Subst.to_string @{context} (*correct*)
5.689 +(*+*)val [(Free ("fixes", bbb(*"bool list"*)), _)] = env_subst; (*Given from Problem*)
5.690 +(*+*)val Type ("List.list", [Type ("HOL.bool", [])]) = bbb; (*---vvvvvvvvvvv*)
5.691 +\<close> ML \<open>
5.692 +\<close> ML \<open> (*/////-------- step into mk_env_subst_DEL ------------------------------------------\\*)
5.693 +(*/////--------------- step into mk_env_subst_DEL ------------------------------------------\\*)
5.694 +"~~~~~ fun mk_env_subst_DEL , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
5.695 +\<close> ML \<open>
5.696 +(*+*)val ["((#Given, (Constants, fixes)), (1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] ,(fixes, [[r = 7]]), Position.T)))"]
5.697 +(*+*) = equal_descr_pairs |> map (fn (pat_single, i_single) => pair2str (Model_Pattern.pat2str @{context} pat_single,
5.698 +(*+*) I_Model.single_to_string_TEST @{context} i_single))
5.699 +\<close> ML \<open>
5.700 +val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
5.701 + => (discern_feedback_subst id feedb));
5.702 +val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 1 equal_descr_pairs
5.703 +\<close> ML \<open>
5.704 + discern_feedback_subst id feedb;
5.705 +\<close> ML \<open>
5.706 +"~~~~~ fun discern_feedback_subst , args:"; val (id, (Model_Def.Cor_TEST ((descr, [ts]), _))) =
5.707 + (id, feedb);
5.708 +\<close> ML \<open>
5.709 + discern_type_subst (descr, id) [ts];
5.710 +"~~~~~ fun discern_type_subst , args:"; val ((descr, id), ts) = ((descr, id), [ts]);
5.711 +\<close> ML \<open>
5.712 +val (Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) =
5.713 + (*case*) type_of descr (*of*);
5.714 +\<close> ML \<open>
5.715 + (*if*) TermC.is_list (hd ts) (*then*);
5.716 +\<close> ML \<open>
5.717 +val return_discern_type_subst =
5.718 + [(id, ts |> map TermC.the_single |> TermC.list2isalist HOLogic.boolT)]
5.719 +(*==============================================^^^^^^^^^^^^*)
5.720 +\<close> ML \<open> (*|||||-------- contine mk_env_subst_DEL ----------------------------------------------*)
5.721 +(*|||||--------------- contine mk_env_subst_DEL ----------------------------------------------*)
5.722 +\<close> ML \<open>
5.723 +val return_mk_env_subst_DEL = return_discern_type_subst
5.724 + |> repair_env;
5.725 +\<close> ML \<open>
5.726 +i_model_max
5.727 +\<close> ML \<open>
5.728 +"~~~~~ fun repair_env , args:"; val (env) = (return_discern_type_subst);
5.729 +\<close> ML \<open>
5.730 +val xxx = (fn (id_inst, val_) => (switch_type id_inst (type_of val_), val_))
5.731 +\<close> ML \<open>
5.732 +"~~~~~ fun switch_type , args:"; val ((Free (id, _)), T) = nth 1 env;
5.733 +\<close> ML \<open>
5.734 +\<close> ML \<open>
5.735 +\<close> ML \<open>
5.736 +\<close> ML \<open>
5.737 +\<close> ML \<open>
5.738 +\<close> ML \<open>
5.739 +\<close> ML \<open>
5.740 +\<close> ML \<open>
5.741 +\<close> ML \<open>
5.742 +\<close> ML \<open>
5.743 +\<close> ML \<open>
5.744 +\<close> ML \<open>
5.745 +\<close> ML \<open>
5.746 +\<close> ML \<open>
5.747 +\<close> ML \<open>
5.748 +\<close> ML \<open>
5.749 +\<close> ML \<open>
5.750 +\<close> ML \<open>
5.751 +\<close> ML \<open> (*|||||-------- contine mk_env_subst_DEL ----------------------------------------------*)
5.752 +(*|||||--------------- contine mk_env_subst_DEL ----------------------------------------------*)
5.753 +\<close> ML \<open>
5.754 +\<close> ML \<open>
5.755 +(*\\\\\--------------- step into mk_env_subst_DEL ------------------------------------------//*)
5.756 +\<close> ML \<open> (*\\\\\-------- step into mk_env_subst_DEL ------------------------------------------//*)
5.757 +\<close> ML \<open>
5.758 +\<close> text \<open>
5.759 +(*+*)val "[\n(1, [1, 2, 3], true ,#Given, (Cor_TEST Constants [r = 7] ,(fixes, [[r = 7]]), Position.T))]"
5.760 +(*+*) = i_model_max |> I_Model.to_string_TEST @ {context}
5.761 +\<close> text \<open>
5.762 + val env_eval = mk_env_eval_DEL i_model_max
5.763 +\<close> text \<open>
5.764 +"~~~~~ fun mk_env_eval_DEL , args:"; val (i_singles) = (i_model_max);
5.765 +\<close> text \<open>
5.766 +val xxx = (fn (_, _, _, _, (feedb, _)) =>
5.767 + discern_feedback_eval feedb)
5.768 +val (_, _, _, _, (feedb, _)) = nth 1 i_singles
5.769 +\<close> text \<open>
5.770 +"~~~~~ fun discern_feedback_eval , args:"; val ((Model_Def.Cor_TEST ((descr, [ts]), _))) =
5.771 + (feedb);
5.772 +\<close> text \<open>
5.773 + discern_type_eval descr [ts];
5.774 +"~~~~~ fun discern_type_eval , args:"; val (descr, ts) = (descr, [ts]);
5.775 +\<close> text \<open>
5.776 +val (Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) =
5.777 + (*case*) type_of descr (*of*);
5.778 +\<close> text \<open>
5.779 +val return_discern_type_eval = ts |> map can_isalist2list |> flat |> flat |> map can_pair |> flat
5.780 +
5.781 +(*+*)val ["(r, 7)"] = return_discern_type_eval
5.782 +(*+*) |> map (fn (t1, t2) => pair2str (UnparseC.term @ {context} t1, UnparseC.term @ {context} t2));
5.783 +\<close> ML \<open> (*||||--------- contine of_max_variant ------------------------------------------------*)
5.784 +(*||||---------------- contine of_max_variant ------------------------------------------------*)
5.785 +\<close> ML \<open> (*\\\\--------- step into of_max_variant --------------------------------------------\\*)
5.786 +(*\\\\---------------- step into of_max_variant --------------------------------------------\\*)
5.787 +val (_, env_subst, env_eval) = return_of_max_variant;
5.788 +\<close> ML \<open>
5.789 +\<close> ML \<open> (*//=========== adhoc inserted shortcuts --------------------------------------------\\*)
5.790 +(*//------------------ adhoc inserted shortcuts --------------------------------------------\\*)
5.791 +(*+*)env_subst = [(@{term "(fixes::bool list)"}, @{term "[(r::real) = 7]"})];
5.792 +val env_subst = [(@{term "(fixes::bool list)"}, @{term "[(r::real) = 7]"})]
5.793 +(*+*)val "[\"\n(fixes, [r = 7])\"]" = env_subst |> Subst.to_string @{context}
5.794 +\<close> ML \<open>
5.795 +(*+*)env_eval = [(@{term "r::real"}, @{term "7::real"})];
5.796 +val env_eval = [(@{term "r::real"}, @{term "7::real"})]
5.797 +(*+*)val "[\"\n(r, 7)\"]" = env_eval |> Subst.to_string @{context};
5.798 +(*\\------------------ adhoc inserted shortcuts --------------------------------------------//*)
5.799 +\<close> ML \<open> (*\\=========== adhoc inserted shortcuts --------------------------------------------//*)
5.800 +\<close> ML \<open>
5.801 +\<close> ML \<open> (*|||---------- contine check_OLD -----------------------------------------------------*)
5.802 +(*|||----------------- contine check_OLD -----------------------------------------------------*)
5.803 + val pres_subst = map (
5.804 + TermC.subst_atomic_all env_subst) pres;
5.805 +\<close> ML \<open> (*//----------- step into subst_atomic_all ------------------------------------------\\*)
5.806 +(*//------------------ step into subst_atomic_all ------------------------------------------\\*)
5.807 +"~~~~~ fun subst_atomic_all , args:"; val (instl, t) = (env_subst, nth 1 pres);
5.808 +\<close> ML \<open>
5.809 +env_subst (*Free ("fixes", "bool list")*)
5.810 +\<close> ML \<open>
5.811 +pres
5.812 +\<close> ML \<open>
5.813 +t
5.814 +\<close> ML \<open>
5.815 +\<close> ML \<open>
5.816 +\<close> ML \<open>
5.817 +\<close> ML \<open>
5.818 +(*\\------------------ step into subst_atomic_all ------------------------------------------//*)
5.819 +\<close> ML \<open> (*\\----------- step into subst_atomic_all ------------------------------------------//*)
5.820 +\<close> ML \<open>
5.821 +\<close> ML \<open> (*|||---------- contine check_OLD -----------------------------------------------------*)
5.822 +(*|||----------------- contine check_OLD -----------------------------------------------------*)
5.823 +\<close> ML \<open>
5.824 +(*+*)val [(false, Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
5.825 +(*+*) Free ("fixes", rrr(*"real"*)))] = pres_subst (*NOT "fixes" \<longrightarrow> "[r = 7]" INcorrect*)
5.826 +(*+*)val Type ("Real.real", []) = rrr
5.827 +\<close> ML \<open>
5.828 + val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
5.829 +\<close> ML \<open>
5.830 +(*+*)val [Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
5.831 +(*+*) Free ("fixes", rrr(*"real"*))] = pres (*Where from Problem*)
5.832 +\<close> ML \<open>
5.833 +
5.834 + val evals = map (eval ctxt where_rls) full_subst
5.835 +\<close> ML \<open>
5.836 +\<close> ML \<open>
5.837 +\<close> ML \<open> (*\\\---------- step into check_OLD -------------------------------------------------\\*)
5.838 +(*\\\----------------- step into do_next ---------------------------------------------------\\*)
5.839 +\<close> ML \<open>(*\\------------ step into do_next ---------------------------------------------------//*)
5.840 +(*\\------------------ step into do_next ---------------------------------------------------//*)
5.841 +\<close> ML \<open>
5.842 +\<close> ML \<open>
5.843 +\<close> ML \<open>(*\------------- step into me_Add_Relation_SideConditions ----------------------------//*)
5.844 +(*\------------------- step into me_Add_Relation_SideConditions ----------------------------//*)
5.845 +val (p, _, f, nxt, _, pt) = return_me_Add_Relation_SideConditions
5.846 +\<close> ML \<open> val Empty_Tac = nxt; (*################################################*)
5.847 +\<close> text \<open>
5.848 + val Specify_Theory "Diff_App" = nxt;
5.849 +
5.850 +val return_me_Specify_Theory
5.851 + = me nxt p c pt; val Specify_Problem ["univariate_calculus", "Optimisation"] = #4 return_me_Specify_Theory;
5.852 +(*/------------------- step into me Specify_Theory -----------------------------------------\\*)
5.853 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
5.854 + val ctxt = Ctree.get_ctxt pt p
5.855 + val (pt, p) =
5.856 + case Step.by_tactic tac (pt, p) of
5.857 + ("ok", (_, _, ptp)) => ptp
5.858 +
5.859 +val ("ok", (ts as (_, _, _) :: _, _, _)) =
5.860 + (*case*)
5.861 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
5.862 +(*//------------------ step into do_next ---------------------------------------------------\\*)
5.863 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
5.864 + = (p, ((pt, Pos.e_pos'), [])) (*of*);
5.865 + (*if*) Pos.on_calc_end ip (*else*);
5.866 + val (_, probl_id, _) = Calc.references (pt, p);
5.867 +val _ =
5.868 + (*case*) tacis (*of*);
5.869 + (*if*) probl_id = Problem.id_empty (*else*);
5.870 +
5.871 + Step.switch_specify_solve p_ (pt, ip);
5.872 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
5.873 + (*if*) Pos.on_specification ([], state_pos) (*then*);
5.874 +
5.875 + Step.specify_do_next (pt, input_pos);
5.876 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
5.877 + val (_, (p_', tac)) = Specify.find_next_step ptp
5.878 + val ist_ctxt = Ctree.get_loc pt (p, p_);
5.879 + (*case*) tac (*of*);
5.880 +
5.881 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
5.882 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Problem pI), (pt, pos as (p, _)))
5.883 + = (tac, (pt, (p, p_')));
5.884 + val (oris, dI, dI', pI', probl, ctxt) = case get_obj I pt p of
5.885 + PblObj {origin = (oris, (dI,_,_),_), spec = (dI',pI',_), probl, ctxt, ...} =>
5.886 + (oris, dI, dI', pI', probl, ctxt)
5.887 + val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
5.888 + val {model, where_, where_rls,...} = Problem.from_store (Ctree.get_ctxt pt pos) pI
5.889 +(*\\------------------ step into do_next ---------------------------------------------------//*)
5.890 +(*\------------------- step into me Specify_Theory -----------------------------------------//*)
5.891 +val (p,_,f,nxt,_,pt) = return_me_Specify_Theory;
5.892 +
5.893 +val return_me_Specify_Problem (* keep for continuing me *)
5.894 + = me nxt p c pt; val Specify_Method ["Optimisation", "by_univariate_calculus"] = #4 return_me_Specify_Problem;
5.895 +(*/------------------- step into me Specify_Problem ----------------------------------------\\*)
5.896 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
5.897 + val ctxt = Ctree.get_ctxt pt p
5.898 +
5.899 +(** ) val ("ok", (_, _, ptp as (pt, p))) =( **)
5.900 +(**) val return_by_tactic =(**) (*case*)
5.901 + Step.by_tactic tac (pt, p) (*of*);
5.902 +(*//------------------ step into by_tactic -------------------------------------------------\\*)
5.903 +"~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
5.904 +
5.905 + (*case*)
5.906 + Step.check tac (pt, p) (*of*);
5.907 +"~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p));
5.908 + (*if*) Tactic.for_specify tac (*then*);
5.909 +
5.910 +Specify_Step.check tac (ctree, pos);
5.911 +"~~~~~ fun check , args:"; val ((Tactic.Specify_Problem pID), (pt, pos as (p, _)))
5.912 + = (tac, (ctree, pos));
5.913 + val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
5.914 + Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
5.915 + => (oris, dI, pI, dI', pI', itms)
5.916 + val thy = ThyC.get_theory ctxt (if dI' = ThyC.id_empty then dI else dI');
5.917 +(*\\------------------ step into by_tactic -------------------------------------------------//*)
5.918 +val ("ok", (_, _, ptp as (pt, p))) = return_by_tactic (* kept for continuing me *);
5.919 +
5.920 + (*case*)
5.921 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
5.922 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
5.923 + (*if*) Pos.on_calc_end ip (*else*);
5.924 + val (_, probl_id, _) = Calc.references (pt, p);
5.925 +val _ =
5.926 + (*case*) tacis (*of*);
5.927 + (*if*) probl_id = Problem.id_empty (*else*);
5.928 +
5.929 + Step.switch_specify_solve p_ (pt, ip);
5.930 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
5.931 + (*if*) Pos.on_specification ([], state_pos) (*then*);
5.932 +
5.933 + Step.specify_do_next (pt, input_pos);
5.934 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
5.935 + val (_, (p_', tac)) = Specify.find_next_step ptp
5.936 + val ist_ctxt = Ctree.get_loc pt (p, p_)
5.937 +val _ =
5.938 + (*case*) tac (*of*);
5.939 +
5.940 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
5.941 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos))
5.942 + = (tac, (pt, (p, p_')));
5.943 +
5.944 + val (o_model, ctxt, i_model) =
5.945 +Specify_Step.complete_for id (pt, pos);
5.946 +"~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
5.947 + val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
5.948 + ...} = Calc.specify_data (ctree, pos);
5.949 + val ctxt = Ctree.get_ctxt ctree pos
5.950 + val (dI, _, _) = References.select_input o_refs refs;
5.951 + val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
5.952 + val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
5.953 + val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
5.954 + val thy = ThyC.get_theory ctxt dI
5.955 + val (_, (i_model, _)) = M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
5.956 +(*\------------------- step into me Specify_Problem ----------------------------------------//*)
5.957 +val (p,_,f,nxt,_,pt) = return_me_Specify_Problem
5.958 +
5.959 +val return_me_Add_Given_FunctionVariable
5.960 + = me nxt p c pt; val Add_Given "FunctionVariable a" = #4 return_me_Add_Given_FunctionVariable;
5.961 +(*/------------------- step into me Specify_Method -----------------------------------------\\*)
5.962 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
5.963 + val ctxt = Ctree.get_ctxt pt p
5.964 + val (pt, p) =
5.965 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
5.966 + case Step.by_tactic tac (pt, p) of
5.967 + ("ok", (_, _, ptp)) => ptp;
5.968 +
5.969 + (*case*)
5.970 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
5.971 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, Pos.e_pos'), []));
5.972 + (*if*) Pos.on_calc_end ip (*else*);
5.973 + val (_, probl_id, _) = Calc.references (pt, p);
5.974 +val _ =
5.975 + (*case*) tacis (*of*);
5.976 + (*if*) probl_id = Problem.id_empty (*else*);
5.977 +
5.978 + Step.switch_specify_solve p_ (pt, ip);
5.979 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
5.980 + (*if*) Pos.on_specification ([], state_pos) (*then*);
5.981 +
5.982 + Step.specify_do_next (pt, input_pos);
5.983 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
5.984 +
5.985 + val (_, (p_', tac)) =
5.986 + Specify.find_next_step ptp;
5.987 +"~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
5.988 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
5.989 + spec = refs, ...} = Calc.specify_data (pt, pos);
5.990 + val ctxt = Ctree.get_ctxt pt pos;
5.991 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
5.992 + (*if*) p_ = Pos.Pbl (*else*);
5.993 +
5.994 + Specify.for_method ctxt oris (o_refs, refs) (pbl, met);
5.995 +"~~~~~ fun for_method , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met))
5.996 + = (ctxt, oris, (o_refs, refs), (pbl, met));
5.997 + val cmI = if mI = MethodC.id_empty then mI' else mI;
5.998 + val {model = mpc, where_rls, where_, ...} = MethodC.from_store ctxt cmI; (*..MethodC ?*)
5.999 + val (preok, _) = Pre_Conds.check ctxt where_rls where_ pbl 0;
5.1000 +val NONE =
5.1001 + (*case*) find_first (I_Model.is_error o #5) met (*of*);
5.1002 +
5.1003 + (*case*)
5.1004 + Specify.item_to_add (ThyC.get_theory ctxt
5.1005 + (if dI = ThyC.id_empty then dI' else dI)) oris mpc met (*of*);
5.1006 +"~~~~~ fun item_to_add , args:"; val (thy, oris, _, itms)
5.1007 + = ((ThyC.get_theory ctxt (if dI = ThyC.id_empty then dI' else dI)), oris, mpc, met);
5.1008 +(*\------------------- step into me Specify_Method -----------------------------------------//*)
5.1009 +val (p,_,f,nxt,_,pt) = return_me_Add_Given_FunctionVariable
5.1010 +
5.1011 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "Input_Descript.Domain {0<..<r}" = nxt;
5.1012 +val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Given "ErrorBound (\<epsilon> = 0)" = nxt;
5.1013 +(*
5.1014 + nxt would be Tactic.Apply_Method, which tries to determine a next step in the ***Program***,
5.1015 + but the ***Program*** is not yet perfectly implemented.
5.1016 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
5.1017 +*)
5.1018 \<close> ML \<open>
5.1019 \<close> ML \<open>
5.1020 \<close>