Walther@60763: (* Title: "Minisubpbl/100a-init-rootpbl-Maximum.sml" Walther@60763: Author: Walther Neuper 1105 Walther@60763: (c) copyright due to lincense terms. Walther@60763: Walther@60763: COMPARE Specify/specify.sml --- specify-phase: low level functions --- Walther@60763: Walther@60763: ATTENTION: the file creates buffer overflow if copied in one piece ! Walther@60763: Walther@60763: Note: This test --- steps into me --- more than once, to a somewhat extreme extent; Walther@60763: in order not to get lost while working in Test_Some etc, Walther@60763: re-introduce ML (*--- step into XXXXX ---*) and Co. Walther@60763: and use Sidekick for orientation. Walther@60763: Nesting is indicated by /--- //-- ///- at the left margin of the comments. Walther@60763: *) Walther@60763: (*/------- these overwrite definitions in section above ---\*) Walther@60763: open Ctree; Walther@60763: open Pos; Walther@60763: open TermC; Walther@60763: open Istate; Walther@60763: open Tactic; Walther@60763: open I_Model; Walther@60763: open P_Model Walther@60763: open Rewrite; Walther@60763: open Step; Walther@60763: open LItool; Walther@60763: open LI; Walther@60763: open Test_Code Walther@60763: open Specify Walther@60763: open ME_Misc Walther@60763: open Pre_Conds; Walther@60763: (*\------- these overwrite definitions in section above ---/*) Walther@60763: Walther@60763: val (_(*example text*), Walther@60763: (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" :: Walther@60763: "Extremum (A = 2 * u * v - u \ 2)" :: Walther@60763: "SideConditions [((u::real) / 2) \ 2 + (2 / v) \ 2 = r \ 2]" :: Walther@60763: "SideConditions [((u::real) / 2) \ 2 + (2 / v) \ 2 = r \ 2]" :: Walther@60763: "SideConditions [(u::real) / 2 = r * sin \, 2 / v = r * cos \]" :: Walther@60763: (*---------------------------------------------,(v::real) / 2 = r * cos \]" --- ERROR in example*) Walther@60763: "FunctionVariable a" :: "FunctionVariable b" :: "FunctionVariable \" :: Walther@60763: "Domain {0 <..< r}" :: "Domain {0 <..< r}" :: "Domain {0 <..< \ / 2}" :: Walther@60763: "ErrorBound (\ = (0::real))" :: []), Walther@60763: refs as ("Diff_App", Walther@60763: ["univariate_calculus", "Optimisation"], Walther@60763: ["Optimisation", "by_univariate_calculus"]))) Walther@60763: = Store.get (Know_Store.get_expls @{theory}) ["Diff_App-No.123a"] ["Diff_App-No.123a"]; Walther@60763: Walther@60763: val c = []; Walther@60763: val return_init_calc = Walther@60763: Test_Code.init_calc @{context} [(model, refs)]; (*val Model_Problem = nxt;*) Walther@60763: (*/------------------- step into init_calc -------------------------------------------------\\*) Walther@60763: "~~~~~ fun init_calc , args:"; val (ctxt, [(model, refs as (thy_id, _, _))]) = Walther@60763: (@{context}, [(model, refs)]); Walther@60763: val thy = thy_id |> ThyC.get_theory ctxt Walther@60763: val ((pt, p), tacis) = Step_Specify.initialise' thy (model, refs) Walther@60763: val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis Walther@60763: val f = Walther@60763: TESTg_form ctxt (pt,p); Walther@60763: "~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt,p)); Walther@60763: val (form, _, _) = Walther@60763: ME_Misc.pt_extract ctxt ptp; Walther@60763: "~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_ as Pbl(*Frm,Pbl*)))) = (ctxt, ptp); Walther@60763: val ppobj = Ctree.get_obj I pt p Walther@60763: val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p; Walther@60763: Walther@60763: (*if*) Ctree.is_pblobj ppobj (*then*); Walther@60763: pt_model ppobj p_ ; Walther@60763: "~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}), Pbl_) = Walther@60763: (ppobj, p_); Walther@60763: val (_, pI, _) = Ctree.get_somespec' spec spec'; Walther@60763: (* val where_ = if pI = Problem.id_empty then []*) Walther@60763: (*if*) pI = Problem.id_empty (*else*); Walther@60763: val {where_rls, where_, model, ...} = Problem.from_store ctxt pI Walther@60763: val (_, where_) = Walther@60763: Pre_Conds.check ctxt where_rls where_ Walther@60782: (model, I_Model.OLD_to probl); Walther@60763: "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) = Walther@60782: (ctxt, where_rls, where_, (model, I_Model.OLD_to probl)); Walther@60763: val (env_model, (env_subst, env_eval)) = Walther@60763: make_environments model_patt i_model; Walther@60763: "~~~~~ fun make_environments , args:"; val (_, []) = (model_patt, i_model); Walther@60763: (*\------------------- step into init_calc -------------------------------------------------//*) Walther@60763: val (p,_,f,nxt,_,pt) = return_init_calc; Walther@60763: Walther@60763: (*+*)val PblObj {ctxt, probl, ...} = get_obj I pt []; Walther@60763: (*+*)Proof_Context.theory_of ctxt (*= {Pure, .., Diff_App}*); Walther@60763: (*+*)val Free ("r", Type ("Real.real", [])) = Syntax.read_term ctxt "r" Walther@60763: (*+*)val [] = probl Walther@60763: Walther@60763: val return_me_Model_Problem = Walther@60763: me nxt p c pt; val Add_Given "Constants [r = 7]" = #4 return_me_Model_Problem; Walther@60763: (*/------------------- step into me_Model_Problem ------------------------------------------\\*) Walther@60763: "~~~~~ fun me , args:"; val (tac as Model_Problem, (p:Pos.pos'), (_:Test_Code.NEW), (pt:Ctree.ctree)) = (nxt, p, c, pt); Walther@60763: val ctxt = Ctree.get_ctxt pt p Walther@60766: Walther@60763: val return_by_tactic = case Walther@60763: Step.by_tactic tac (pt,p) of Walther@60763: ("ok", (_, _, ptp)) => ptp; Walther@60763: (*//------------------ step into by_tactic -------------------------------------------------\\*) Walther@60763: "~~~~~ fun by_tactic , args:"; val (tac, (ptp as (pt, p))) = (tac, (pt,p)); Walther@60766: Walther@60763: val Applicable.Yes tac' = (*case*) Walther@60763: Step.check tac (pt, p) (*of*); Walther@60763: "~~~~~ fun check , args:"; val (tac, (ctree, pos)) = (tac, (pt, p)); Walther@60763: (*if*) Tactic.for_specify tac (*then*); Walther@60763: Walther@60763: Specify_Step.check tac (ctree, pos); Walther@60763: "~~~~~ fun check , args:"; val (Tactic.Model_Problem, (pt, pos as (p, _))) = Walther@60763: (tac, (ctree, pos)); Walther@60766: val (ctxt, o_model, pI') = case Ctree.get_obj I pt p of Walther@60766: Ctree.PblObj {ctxt, origin = (o_model, (_, pI', _), _), ...} => (ctxt, o_model, pI') Walther@60766: | _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj" Walther@60763: val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI' Walther@60782: val pbl = I_Model.init ctxt o_model model_patt Walther@60763: Walther@60763: val return_check = Walther@60763: Applicable.Yes (Tactic.Model_Problem' (pI', I_Model.TEST_to_OLD pbl, [])); Walther@60763: (*\\------------------ step into by_tactic -------------------------------------------------//*) Walther@60763: val (pt, p) = return_by_tactic; Walther@60763: Walther@60763: val return_do_next = (*case*) Walther@60763: Step.do_next p ((pt, Pos.e_pos'), []) (*of*); Walther@60763: (*//------------------ step into do_next ---------------------------------------------------\\*) Walther@60763: "~~~~~ fun do_next , args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) = Walther@60763: (p, ((pt, e_pos'),[])); Walther@60763: val pIopt = get_pblID (pt,ip); Walther@60763: (*if*) ip = ([],Res); (* = false*) Walther@60763: val _ = (*case*) tacis (*of*); Walther@60763: val SOME _ = (*case*) pIopt (*of*); Walther@60763: Walther@60763: val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) = Walther@60763: Step.switch_specify_solve p_ (pt, ip); Walther@60763: "~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip)); Walther@60763: (*if*) Pos.on_specification ([], state_pos) (*then*); Walther@60763: Walther@60763: val ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) = Walther@60763: Step.specify_do_next (pt, input_pos); Walther@60763: (*///----------------- step into specify_do_next -------------------------------------------\\*) Walther@60763: "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos); Walther@60763: Walther@60763: (* val (_, (p_', tac)) =*) Walther@60763: val return_find_next_step = (*keep for continuing specify_do_next*) Walther@60763: Specify.find_next_step ptp; Walther@60763: (*////---------------- step into find_next_step --------------------------------------------\\*) Walther@60763: "~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp); Walther@60763: val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl, Walther@60763: spec = refs, ...} = Calc.specify_data (pt, pos); Walther@60763: val ctxt = Ctree.get_ctxt pt pos; Walther@60763: (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*); Walther@60763: (*if*) p_ = Pos.Pbl (*then*); Walther@60763: Walther@60763: val return_for_problem as ("dummy", (Pbl, Add_Given "Constants [r = 7]")) = Walther@60782: Specify.for_problem ctxt oris (o_refs, refs) (pbl, I_Model.OLD_to met); Walther@60763: (*/////--------------- step into for_problem -----------------------------------------------\\*) Walther@60763: "~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) Walther@60763: = (ctxt, oris, (o_refs, refs), (pbl, met)); Walther@60763: val cdI = if dI = ThyC.id_empty then dI' else dI; Walther@60763: val cpI = if pI = Problem.id_empty then pI' else pI; Walther@60763: val cmI = if mI = MethodC.id_empty then mI' else mI; Walther@60763: val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI; Walther@60763: val {model = mpc, ...} = MethodC.from_store ctxt cmI; Walther@60763: Walther@60763: val return_check = Walther@60782: Pre_Conds.check ctxt where_rls where_ (pbt, I_Model.OLD_to pbl); Walther@60763: (*//////-------------- step into check -------------------------------------------------\\*) Walther@60763: "~~~~~ fun check , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) = Walther@60782: (ctxt, where_rls, where_, (pbt, I_Model.OLD_to pbl)); Walther@60763: val return_make_environments = Walther@60763: make_environments model_patt i_model; Walther@60763: (*///// //------------ step into of_max_variant --------------------------------------------\\*) Walther@60763: "~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = Walther@60763: (model_patt, i_model); Walther@60763: Walther@60782: (*+*)val "[\n(1, [1, 2, 3], false ,#Given, (Inc Constants [] [__=__, __=__], Position.T)), \n(2, [1, 2, 3], false ,#Find, (Inc Maximum __, Position.T)), \n(3, [1, 2, 3], false ,#Find, (Inc AdditionalValues [] [__, __], Position.T)), \n(4, [1, 2, 3], false ,#Relate, (Inc Extremum (__=__), Position.T)), \n(5, [1, 2], false ,#Relate, (Inc SideConditions [] [__=__, __=__], Position.T))]" Walther@60782: = i_model |> I_Model.to_string ctxt Walther@60763: val all_variants = Walther@60763: map (fn (_, variants, _, _, _) => variants) i_model Walther@60763: |> flat Walther@60763: |> distinct op = Walther@60763: val variants_separated = map (filter_variants' i_model) all_variants Walther@60763: val sums_corr = map (Model_Def.cnt_corrects) variants_separated Walther@60763: val sum_variant_s = Model_Def.arrange_args sums_corr (1, all_variants) Walther@60763: (*+*)val [(0, 1), (0, 2), (0, 3)] = sum_variant_s Walther@60763: val (_, max_variant) = hd (*..crude decision, up to improvement *) Walther@60763: (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s) Walther@60763: val i_model_max = Walther@60763: filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model Walther@60763: val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat Walther@60763: (*for building make_env_s -------------------------------------------------------------------\*) Walther@60763: (*!!!*) val ("#Given", (descr, term), pos) = Walther@60763: Model_Pattern.split_descriptor ctxt ("#Given", @{term "Constants [r = (7::real)]"}, Position.none) Walther@60763: (*!!!*) val patt = equal_descr_pairs |> hd |> #1 Walther@60763: (*!!!*)val equal_descr_pairs = Walther@60763: (patt, Walther@60782: (1, [1, 2, 3], true, "#Given", (Cor ((descr, (*!*)TermC.isalist2list(*!*) term)), pos))) Walther@60763: :: tl equal_descr_pairs Walther@60763: (*for building make_env_s -------------------------------------------------------------------/*) Walther@60763: Walther@60763: val env_model = make_env_model equal_descr_pairs; Walther@60763: (*///// ///----------- step into make_env_model --------------------------------------------\\*) Walther@60763: "~~~~~ fun make_env_model , args:"; val (equal_descr_pairs) = (equal_descr_pairs); Walther@60763: Walther@60763: val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) Walther@60763: => (mk_env_model id feedb)); Walther@60763: val ((_, (_, id)), (_, _, _, _, (feedb, _))) = nth 4 equal_descr_pairs; Walther@60763: (*\\\\\ \\\----------- step into make_env_model --------------------------------------------//*) Walther@60763: (*||||| ||------------ contine of_max_variant ------------------------------------------------*) Walther@60763: Walther@60763: val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs Walther@60763: val subst_eval_list = make_envs_preconds equal_givens Walther@60763: val return_make_envs_preconds = Walther@60763: make_envs_preconds equal_givens; Walther@60763: (*///// ///----------- step into make_envs_preconds ----------------------------------------\\*) Walther@60763: "~~~~~ fun make_envs_preconds , args:"; val (equal_givens) = (equal_givens); Walther@60763: val xxx = (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) Walther@60763: ; Walther@60782: xxx: (Model_Pattern.single * I_Model.single) -> ((term * term) * (term * term)) list; Walther@60763: val return_discern_feedback = Walther@60763: discern_feedback id feedb; Walther@60763: (*nth 1 equal_descr_pairs* ) Walther@60782: "~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Cor ((descr, ts), _))) = (id, feedb); Walther@60763: ( *nth 2 equal_descr_pairs*) Walther@60782: "~~~~~ fun discern_feedback , args:"; val (id, (Model_Def.Inc ((descr, ts)))) = (id, feedb); Walther@60763: Walther@60763: (*nth 1 equal_descr_pairs* ) Walther@60763: (*+*)val [((Const ("fixes", typ1), Free ("r", typ2)), Walther@60763: (Free ("r", typ3), value))] = return_discern_feedback Walther@60763: (*+*)val true = typ1 = typ2 Walther@60763: (*+*)val true = typ3 = HOLogic.realT Walther@60763: (*+*)val "7" = UnparseC.term ctxt value Walther@60763: ( *nth 2 equal_descr_pairs*) Walther@60763: (*+*)val [] = return_discern_feedback Walther@60763: Walther@60763: val return_discern_typ = Walther@60763: discern_typ id (descr, ts); Walther@60763: "~~~~~ fun discern_typ , args:"; val (id, (descr, ts)) = (id, (descr, ts)); Walther@60763: (*nth 1 equal_descr_pairs* ) Walther@60763: (*+*)val [((Const ("fixes", typ1), Free ("r", typ2)), Walther@60763: (Free ("r", typ3), value))] = return_discern_typ Walther@60763: (*+*)val true = typ1 = typ2 Walther@60763: (*+*)val true = typ3 = HOLogic.realT Walther@60763: (*+*)val "7" = UnparseC.term ctxt value Walther@60763: ( *nth 2 equal_descr_pairs*) Walther@60763: (*+*)val [] = return_discern_typ; Walther@60763: (**) Walther@60763: switch_type id ts; Walther@60763: "~~~~~ fun switch_type , args:"; val (Const (descr_string, _), ts) = (descr, ts); Walther@60763: Walther@60763: (*nth 1 equal_descr_pairs* ) Walther@60782: val return_switch_type = Const (descr_string, ts |> hd |> TermC.lhs |> type_of) Walther@60763: Walther@60782: (*+*)val Const ("Input_Descript.Constants", typ) = return_switch_type Walther@60763: (*+*)val Type ("Real.real", []) = typ Walther@60763: ( *nth 2 equal_descr_pairs*) Walther@60782: (*+*)val return_switch_type = descr Walther@60763: (**) Walther@60763: (*\\\\\ \\\----------- step into make_envs_preconds ----------------------------------------//*) Walther@60763: (*||||| ||------------ contine of_max_variant ------------------------------------------------*) Walther@60763: val subst_eval_list = make_envs_preconds equal_givens Walther@60763: val (env_subst, env_eval) = split_list subst_eval_list Walther@60763: val make_environments = (i_model_max, env_model, (env_subst, env_eval)); (*GOON*) Walther@60763: (*\\\\\ \\------------ step into of_max_variant --------------------------------------------//*) Walther@60763: val (i_model_max, env_model, (env_subst, env_eval)) = make_environments Walther@60763: (*!!!/----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---\*) Walther@60763: val (i_max_variant, env_model, (env_subst, env_eval)) = (i_model_max, [], ([], [])) Walther@60763: (*!!!\----- we had a helpful argument for constructing env_model and (env_subst, env_eval)---/*) Walther@60763: (*||||| |------------- contine check -----------------------------------------------------*) Walther@60763: val pres_subst = map (TermC.subst_atomic_all env_subst) pres; Walther@60763: val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst); Walther@60763: val full_subst = if env_eval = [] then pres_subst_other Walther@60763: else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other) Walther@60763: val evals = map (eval ctxt where_rls) full_subst Walther@60763: val return_ = (i_model_max, env_subst, env_eval) Walther@60763: (*\\\\\ \------------- step into check -----------------------------------------------------//*) Walther@60763: val (preok, _) = return_check; Walther@60763: Walther@60763: (*|||||--------------- contine.. for_problem -------------------------------------------------*) Walther@60763: val false = Walther@60763: (*if*) dI' = ThyC.id_empty andalso dI = ThyC.id_empty (*else*); Walther@60763: val false = Walther@60763: (*if*) pI' = Problem.id_empty andalso pI = Problem.id_empty (*else*); Walther@60763: val NONE = Walther@60763: (*case*) find_first (fn (_, _, _, _, feedb) => I_Model.is_error feedb) pbl (*of*); Walther@60763: Walther@60763: (** )val SOME (fd, ct') as ("#Given", "Constants [r = 7]") =( **) Walther@60763: (**)val return_item_to_add as SOME ("#Given", xxx) =(**) (*case*) Walther@60782: Specify.item_to_add ctxt oris (I_Model.OLD_to pbl) (*of*); Walther@60763: (*///// /------------- step into item_to_add -----------------------------------------------\\*) Walther@60763: (*==================== see test/../i_model.sml --- fun item_to_add ---========================*) Walther@60763: (*\\\\\ \------------- step into item_to_add -----------------------------------------------//*) Walther@60763: val SOME (fd, ct') = return_item_to_add Walther@60763: (*+*)val ("#Given", "Constants [r = 7]") = (fd, ct') (*from NEW item_to_add*) Walther@60763: Walther@60763: (*|||||--------------- continue.. for_problem ------------------------------------------------*) Walther@60763: val return_for_problem_step as ("dummy", (Pbl, Add_Given "Constants [r = 7]")) Walther@60763: = ("dummy", (Pos.Pbl, P_Model.mk_additem fd ct')) Walther@60763: (** )return_for_problem_step = return_for_problem( *..would require equality types*) Walther@60763: (*\\\\\--------------- step into for_problem -----------------------------------------------//*) Walther@60763: val return_find_next_step as ("dummy", (Pbl, Add_Given "Constants [r = 7]")) Walther@60763: = return_for_problem Walther@60763: (*\\\\---------------- step into find_next_step --------------------------------------------//*) Walther@60763: (*|||----------------- continue.. specify_do_next --------------------------------------------*) Walther@60763: val (_, (p_', tac as Add_Given "Constants [r = 7]")) = return_find_next_step Walther@60763: Walther@60763: val ist_ctxt = Ctree.get_loc pt (p, p_) Walther@60763: (*+*)val Add_Given "Constants [r = 7]" = tac Walther@60763: val _ = Walther@60763: (*case*) tac (*of*); Walther@60763: Walther@60763: val return_by_tactic_input as ("ok", ([(Add_Given "Constants [r = 7]", _, _)], [], _)) = Walther@60763: Step_Specify.by_tactic_input tac (pt, (p, p_')); Walther@60763: "~~~~~ fun by_tactic_input , args:"; val ((Tactic.Add_Given ct), ptp) = Walther@60763: (tac, (pt, (p, p_'))); Walther@60763: Walther@60763: Specify.by_Add_ "#Given" ct ptp; Walther@60763: "~~~~~ fun by_Add_ , args:"; val (m_field, ct ,(pt, pos as (_, p_))) = Walther@60763: ("#Given", ct, ptp); Walther@60763: val (met, oris, (_, pI', mI'), pbl, (_, pI, mI), ctxt) = SpecificationC.get_data (pt, pos) Walther@60763: val (i_model, m_patt) = Walther@60763: if p_ = Pos.Met then Walther@60763: (met, Walther@60763: (if mI = MethodC.id_empty then mI' else mI) |> MethodC.from_store ctxt |> #model) Walther@60763: else Walther@60763: (pbl, Walther@60763: (if pI = Problem.id_empty then pI' else pI) |> Problem.from_store ctxt |> #model); Walther@60763: Walther@60763: (*case*) Walther@60773: I_Model.check_single ctxt m_field oris (I_Model.TEST_to_OLD i_model) m_patt ct (*of*); Walther@60763: "~~~~~ fun check_single , args:"; val (ctxt, m_field, o_model, i_model, m_patt, (str(*, pos*))) = Walther@60763: (ctxt, m_field, oris, i_model, m_patt, ct); Walther@60763: val (t as (descriptor $ _)) = Syntax.read_term ctxt str Walther@60763: Walther@60763: (*+*)val "Constants [r = 7]" = UnparseC.term ctxt t; Walther@60763: Walther@60763: val SOME m_field' = Walther@60763: (*case*) Model_Pattern.get_field descriptor m_patt (*of*); Walther@60763: (*if*) m_field <> m_field' (*else*); Walther@60763: Walther@60763: (*+*)val "#Given" = m_field; val "#Given" = m_field' Walther@60763: Walther@60763: val ("", ori', all) = Walther@60763: (*case*) O_Model.contains ctxt m_field o_model t (*of*); Walther@60763: Walther@60763: (*+*)val (_, _, _, _, vals) = hd o_model; Walther@60763: (*+*)val "Constants [r = 7]" = UnparseC.term ctxt (@{term Constants} $ (hd vals)); Walther@60763: (*+*)if "[\n(1, [\"1\", \"2\", \"3\"], #Given, Constants, [\"[r = 7]\"]), " ^ Walther@60763: (*+*) "\n(2, [\"1\", \"2\", \"3\"], #Find, Maximum, [\"A\"]), " ^ Walther@60763: (*+*) "\n(3, [\"1\", \"2\", \"3\"], #Find, AdditionalValues, [\"[u]\", \"[v]\"]), " ^ Walther@60763: (*+*) "\n(4, [\"1\", \"2\", \"3\"], #Relate, Extremum, [\"A = 2 * u * v - u \ 2\"]), " ^ Walther@60763: (*+*) "\n(5, [\"1\", \"2\"], #Relate, SideConditions, [\"[(u / 2) \ 2 + (2 / v) \ 2 = r \ 2]\"]), " ^ Walther@60763: (*+*) "\n(6, [\"3\"], #Relate, SideConditions, [\"[u / 2 = r * sin \]\", \"[2 / v = r * cos \]\"]), " ^ Walther@60763: (*+*) "\n(7, [\"1\"], #undef, FunctionVariable, [\"a\"]), " ^ Walther@60763: (*+*) "\n(8, [\"2\"], #undef, FunctionVariable, [\"b\"]), \n(9, [\"3\"], #undef, FunctionVariable, [\"\\"]), " ^ Walther@60763: (*+*) "\n(10, [\"1\", \"2\"], #undef, Input_Descript.Domain, [\"{0<.. / 2}\"]), " ^ Walther@60763: (*+*) "\n(12, [\"1\", \"2\", \"3\"], #undef, ErrorBound, [\"\ = 0\"])]" Walther@60763: (*+*)= O_Model.to_string ctxt o_model then () else error "o_model CHANGED"; Walther@60763: Walther@60763: (*case*) is_notyet_input ctxt i_model all ori' m_patt (*of*); Walther@60763: "~~~~~ fun is_notyet_input , args:"; val (ctxt, itms, all, (i, v, f, d, ts), pbt) = Walther@60763: (ctxt, i_model, all, ori', m_patt); Walther@60763: val SOME (_, (_, pid)) = Walther@60773: (*case*) find_first (fn (_, (d', _)) => d = d') pbt Walther@60773: val SOME (_, _, _, _, (feedb, _)) = Walther@60773: (*case*) find_first (fn (_, _, _, f', (feedb, _)) => Walther@60782: f = f' andalso d = (descriptor feedb)) itms Walther@60777: val ts' = inter op = (feedb_values feedb) ts Walther@60773: val false = Walther@60773: (*if*) subset op = (ts, ts') Walther@60773: Walther@60773: val return_is_notyet_input = ("", Walther@60778: single_from_o feedb pid all (i, v, f, d, subtract op = ts' ts)); Walther@60778: "~~~~~ fun single_from_o , args:"; val (feedb, pid, all, (id, vt, fd, d, ts)) = Walther@60773: (feedb, pid, all, (i, v, f, d, subtract op = ts' ts)); Walther@60777: val ts' = union op = (feedb_values feedb) ts; Walther@60763: val pval = [Input_Descript.join'''' (d, ts')] Walther@60763: val complete = if eq_set op = (ts', all) then true else false Walther@60763: Walther@60782: (*+*)val "Inc Constants [] [__=__, __=__]" = feedb |> I_Model.feedback_to_string ctxt Walther@60763: (*\\\----------------- step into specify_do_next -------------------------------------------//*) Walther@60763: (*\\------------------ step into do_next ---------------------------------------------------//*) Walther@60763: val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next Walther@60763: Walther@60763: (*|------------------- continue with me_Model_Problem ----------------------------------------*) Walther@60763: val tacis as (_::_) = Walther@60763: (*case*) ts (*of*); Walther@60763: val (tac, _, _) = last_elem tacis Walther@60763: Walther@60763: val return_Model_Problem = (p, [] : NEW, TESTg_form ctxt (pt, p), tac, Celem.Sundef, pt); Walther@60763: (*//------------------ step into TESTg_form ------------------------------------------------\\*) Walther@60763: "~~~~~ fun TESTg_form , args:"; val (ctxt, ptp) = (ctxt, (pt, p)); Walther@60763: Walther@60763: val (form, _, _) = Walther@60763: ME_Misc.pt_extract ctxt ptp; Walther@60763: "~~~~~ fun pt_extract , args:"; val (ctxt, (pt, (p, p_(*Frm,Pbl*)))) = (ctxt, ptp); Walther@60763: val ppobj = Ctree.get_obj I pt p Walther@60763: val f = if Ctree.is_pblobj ppobj then pt_model ppobj p_ else Ctree.get_obj pt_form pt p; Walther@60763: (*if*) Ctree.is_pblobj ppobj (*then*); Walther@60763: Walther@60763: pt_model ppobj p_; Walther@60763: "~~~~~ fun pt_model , args:"; val ((Ctree.PblObj {probl, spec, origin = (_, o_spec, hdl), ctxt, ...}), Walther@60763: Pbl(*Frm,Pbl*)) = (ppobj, p_); Walther@60763: val (_, _, met_id) = References.select_input o_spec spec Walther@60782: val (allcorr, _) = Pre_Conds.check_internal ctxt (I_Model.OLD_to probl) (Pos.Met, met_id) Walther@60773: Walther@60782: val return_pt_model = Ctree.ModSpec (allcorr, Pos.Pbl, hdl, I_Model.OLD_to probl, Walther@60773: (*where_*)[(*Problem.from_store in check*)], spec) Walther@60763: Walther@60763: (*|------------------- continue with TESTg_form ----------------------------------------------*) Walther@60763: val Ctree.ModSpec (spec as (_, p_, _, gfr, where_, _)) = Walther@60763: (*case*) form (*of*); Walther@60763: Test_Out.PpcKF ( (Test_Out.Problem [], Walther@60763: P_Model.from (Proof_Context.theory_of ctxt) gfr where_)); Walther@60763: Walther@60763: P_Model.from (Proof_Context.theory_of ctxt) gfr where_; Walther@60763: "~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_); Walther@60763: fun coll model [] = model Walther@60763: | coll model ((_, _, _, field, itm_) :: itms) = Walther@60763: coll (add_sel_ppc thy field model (item_from_feedback thy itm_)) itms; Walther@60763: Walther@60773: val gfr = coll P_Model.empty (I_Model.TEST_to_OLD itms); Walther@60763: "~~~~~ fun coll , args:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: itms)) Walther@60773: = (P_Model.empty, I_Model.TEST_to_OLD itms); Walther@60763: Walther@60763: (*+*)val 4 = length itms; Walther@60763: (*+*)val itm = nth 1 itms; Walther@60763: Walther@60763: coll P_Model.empty [itm]; Walther@60763: "~~~~~ fun coll , iterate:"; val (model, ((aaa, bbb_,ccc_, field, itm_) :: [])) Walther@60763: = (P_Model.empty, [itm]); Walther@60763: Walther@60763: (add_sel_ppc thy field model (item_from_feedback thy itm_)); Walther@60763: "~~~~~ fun add_sel_ppc , args:"; val ((_: theory), sel, {Given = gi, Where = wh, Find = fi, With = wi, Relate = re}, x ) Walther@60763: = (thy, field, model, (item_from_feedback thy itm_)); Walther@60763: Walther@60763: P_Model.item_from_feedback thy itm_; Walther@60763: "~~~~~ fun item_from_feedback , args:"; val (thy, (I_Model.Inc ((d, ts), _))) = (thy, itm_); Walther@60763: P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts))); Walther@60763: (*\\------------------ step into TESTg_form ------------------------------------------------//*) Walther@60763: (*\------------------- step into me_Model_Problem ------------------------------------------//*) Walther@60763: val (p, _, f, nxt, _, pt) = return_me_Model_Problem Walther@60763: Walther@60763: (*+++*)val {probl, ...} = Calc.specify_data (pt, pos); Walther@60763: (*+++*)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)]" Walther@60763: = probl |> I_Model.to_string ctxt Walther@60763: (*-------------------- contine me's ----------------------------------------------------------*) Walther@60763: val return_me_add_find_Constants = me nxt p c pt; Walther@60763: val Add_Find "Maximum A" = #4 return_me_add_find_Constants; Walther@60763: (*/------------------- step into me_add_find_Constants -------------------------------------\\*) Walther@60763: (*==================== done in "Minisubpbl/150a-add-given-Maximum.sml" subsequently =======================*)