1.1 --- a/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Wed Mar 08 17:47:07 2023 +0100
1.2 +++ b/test/Tools/isac/Minisubpbl/150a-add-given-Maximum.sml Fri Mar 31 12:07:52 2023 +0200
1.3 @@ -2,6 +2,8 @@
1.4 Author: Walther Neuper 1105
1.5 (c) copyright due to lincense terms.
1.6
1.7 +ATTENTION: the file creates buffer overflow if copied in one piece !
1.8 +
1.9 Note: This test --- steps into me --- more than once, to a somewhat extreme extent;
1.10 in order not to get lost while working in Test_Some etc,
1.11 re-introduce ML (*--- step into XXXXX ---*) and Co.
1.12 @@ -13,6 +15,8 @@
1.13 open Pos
1.14 open Ctree
1.15 open Tactic
1.16 +open Specify
1.17 +open I_Model
1.18
1.19 val (_(*example text*),
1.20 (model as ("Constants [r = (7::real)]" :: "Maximum A" :: "AdditionalValues [u, v]" ::
1.21 @@ -105,7 +109,7 @@
1.22 fun false_and_not_Sup (_, _, false, _, I_Model.Sup _) = false
1.23 | false_and_not_Sup (_, _, false, _, _) = true
1.24 | false_and_not_Sup _ = false
1.25 - val v = if itms = [] then 1 else I_Model.max_variant itms
1.26 + val v = if itms = [] then 1 else Pre_Conds.max_variant itms
1.27 val vors = if v = 0 then oris else filter (testr_vt v) oris
1.28 val vits =
1.29 if v = 0
1.30 @@ -191,6 +195,27 @@
1.31 Test_Out.PpcKF ( (Test_Out.Problem [],
1.32 P_Model.from (Proof_Context.theory_of ctxt) gfr where_));
1.33
1.34 +(*//------------------ inserted hidden code ------------------------------------------------\\*)
1.35 +fun item_from_feedback thy (I_Model.Cor ((d, ts), _)) = P_Model.Correct (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
1.36 + | item_from_feedback _ (I_Model.Syn c) = P_Model.SyntaxE c
1.37 + | item_from_feedback _ (I_Model.Typ c) = P_Model.TypeE c
1.38 + | item_from_feedback thy (I_Model.Inc ((d, ts), _)) = P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
1.39 + | item_from_feedback thy (I_Model.Sup (d, ts)) = P_Model.Superfl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)))
1.40 + | item_from_feedback thy (I_Model.Mis (d, pid)) = P_Model.Missing (UnparseC.term_in_thy thy d ^ " " ^ UnparseC.term_in_thy thy pid)
1.41 + | item_from_feedback _ _ = raise ERROR "item_from_feedback: uncovered definition"
1.42 +fun add_sel_ppc (_: theory) sel {Given = gi, Where = wh, Find = fi, With = wi, Relate = re} x =
1.43 + case sel of
1.44 + "#Given" => {Given = gi @ [x], Where = wh, Find = fi, With = wi,Relate = re}
1.45 + | "#Where" => {Given = gi, Where = wh @ [x], Find = fi, With = wi, Relate = re}
1.46 + | "#Find" => {Given = gi, Where = wh, Find = fi @ [x], With = wi, Relate = re}
1.47 + | "#Relate"=> {Given = gi, Where = wh, Find = fi, With = wi, Relate = re @ [x]}
1.48 + | "#undef" => {Given = gi @ [x], Where = wh, Find = fi, With = wi, Relate = re} (*ori2itmSup*)
1.49 + | _ => raise ERROR ("add_sel_ppc tried to select by \"" ^ sel ^ "\"")
1.50 +fun add_where {Given = gi, Where = _, Find = fi, With = wi, Relate = re} wh =
1.51 + {Given = gi, Where = wh, Find= fi ,With = wi, Relate = re}
1.52 +fun boolterm2item ctxt (true, term) = P_Model.Correct (UnparseC.term ctxt term)
1.53 + | boolterm2item ctxt(false, term) = P_Model.False (UnparseC.term ctxt term);
1.54 +(*\\------------------ inserted hidden code ------------------------------------------------//*)
1.55 P_Model.from (Proof_Context.theory_of ctxt) gfr where_;
1.56 "~~~~~ fun from , args:"; val (thy, itms, where_) = ((Proof_Context.theory_of ctxt), gfr, where_);
1.57 fun coll model [] = model
1.58 @@ -217,16 +242,65 @@
1.59 P_Model.Incompl (UnparseC.term_in_thy thy (Input_Descript.join (d, ts)));
1.60 (*\------------------- step into into me Model_Problem -------------------------------------//*)
1.61 val (p, _, f, nxt, _, pt) = return_me_Model_Problem
1.62 -
1.63 +(*after -------------- step into intoreturn_me_Add_Relation_SideConditions------------------//* )
1.64 +val (p, _, f, nxt, _, pt) = return_me_Add_Relation_SideConditions
1.65 +( **)
1.66 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "Maximum A" = nxt;
1.67 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [u]" = nxt;
1.68 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Find "AdditionalValues [v]" = nxt;
1.69 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Add_Relation "Extremum (A = 2 * u * v - u \<up> 2)" = nxt;
1.70 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;
1.71 -val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Theory "Diff_App" = nxt;
1.72 +val return_me_Add_Relation_SideConditions
1.73 + = me nxt p c pt;
1.74 +
1.75 +(*/------------------- step into me Add_Relation_SideConditions ----------------------------\\*)
1.76 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
1.77 + val ctxt = Ctree.get_ctxt pt p
1.78 + val (pt, p) =
1.79 + case Step.by_tactic tac (pt, p) of
1.80 + ("ok", (_, _, ptp)) => ptp;
1.81 + (*case*)
1.82 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
1.83 +(*//------------------ step into do_next ---------------------------------------------------\\*)
1.84 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
1.85 + = (p, ((pt, Pos.e_pos'), [])) (*of*);
1.86 + (*if*) Pos.on_calc_end ip (*else*);
1.87 + val (_, probl_id, _) = Calc.references (pt, p);
1.88 + (*case*) tacis (*of*);
1.89 + (*if*) probl_id = Problem.id_empty (*else*);
1.90 +
1.91 + Step.switch_specify_solve p_ (pt, ip);
1.92 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
1.93 + (*if*) Pos.on_specification ([], state_pos) (*then*);
1.94 + Step.specify_do_next (pt, input_pos);
1.95 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = (pt, input_pos);
1.96 +
1.97 + val (_, (p_', tac)) =
1.98 + Specify.find_next_step ptp (* ..Refine_Problem ["univariate_calculus",?*);
1.99 +"~~~~~ fun find_next_step , args:"; val (pt, pos as (_, p_)) = (ptp);
1.100 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
1.101 + spec = refs, ...} = Calc.specify_data (pt, pos);
1.102 + val ctxt = Ctree.get_ctxt pt pos;
1.103 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
1.104 + (*if*) p_ = Pos.Pbl (*then*);
1.105 +
1.106 + for_problem ctxt oris (o_refs, refs) (pbl, met);
1.107 +"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
1.108 + (ctxt, oris, (o_refs, refs), (pbl, met));
1.109 + val cpI = if pI = Problem.id_empty then pI' else pI;
1.110 + val cmI = if mI = MethodC.id_empty then mI' else mI;
1.111 + val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
1.112 + val {model = mpc, ...} = MethodC.from_store ctxt cmI
1.113 +
1.114 +(*+*)val [Const ("Orderings.ord_class.less", _) $ Const ("Groups.zero_class.zero", _) $
1.115 + Free ("fixes", _)] = where_
1.116 + val (preok, _) = Pre_Conds.check_TEST ctxt where_rls (unchecked_OLD_to_TEST where_) [(*works by chance*)]
1.117 +(*\------------------- step into me Add_Relation_SideConditions ----------------------------//*)
1.118 +val (p, _, f, nxt, _, pt) = return_me_Add_Relation_SideConditions
1.119 + val Specify_Theory "Diff_App" = nxt;
1.120 +
1.121 val return_me_Specify_Theory
1.122 = me nxt p c pt; val Specify_Problem ["univariate_calculus", "Optimisation"] = #4 return_me_Specify_Theory;
1.123 -
1.124 (*/------------------- step into me Specify_Theory -----------------------------------------\\*)
1.125 "~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt, p, c, pt);
1.126 val ctxt = Ctree.get_ctxt pt p