1.1 --- a/src/Tools/isac/Interpret/li-tool.sml Fri Jul 21 14:16:57 2023 +0200
1.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Wed Jul 26 11:12:55 2023 +0200
1.3 @@ -319,14 +319,17 @@
1.4 {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...}=>
1.5 (model_patt, program, prog, prog_rls, where_, where_rls)
1.6 | _ => raise ERROR ("init_pstate with " ^ MethodC.id_to_string met_id)
1.7 -(*T_TESTold*)
1.8 +(*T_TESTold* )
1.9 val (_, env_subst, env_eval) = I_Model.of_max_variant model_patt i_model;
1.10 -(*T_TEST* )
1.11 - val (_, _, (env_subst, env_eval)) = I_Model.of_max_variant model_patt i_model;
1.12 -( *T_TESTnew*)
1.13 val actuals = map snd env_subst
1.14 val formals = Program.formal_args prog
1.15 val preconds = Pre_Conds.check_from_store ctxt where_rls where_ env_subst env_eval
1.16 +( *T_TEST*)
1.17 + val (_, env_model, (env_subst, env_eval)) = I_Model.of_max_variant model_patt i_model;
1.18 + val actuals = map snd env_model
1.19 + val formals = Program.formal_args prog
1.20 + val preconds = Pre_Conds.check_from_store ctxt where_rls where_ env_subst env_eval
1.21 +(*T_TESTnew*)
1.22 val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));
1.23 val ist = Istate.e_pstate
1.24 |> Istate.set_eval prog_rls
2.1 --- a/src/Tools/isac/MathEngine/me-misc.sml Fri Jul 21 14:16:57 2023 +0200
2.2 +++ b/src/Tools/isac/MathEngine/me-misc.sml Wed Jul 26 11:12:55 2023 +0200
2.3 @@ -34,7 +34,7 @@
2.4 in
2.5 Ctree.ModSpec (allcorrect, Pos.Met, hdl, meth, where_, spec)
2.6 end
2.7 -(*T_TESTold*)
2.8 +(*T_TESTold* )
2.9 | pt_model (Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}) _(*Frm,Pbl*) =
2.10 let
2.11 val (_, pI, _) = Ctree.get_somespec' spec spec'
2.12 @@ -48,7 +48,7 @@
2.13 in
2.14 Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, where_, spec)
2.15 end
2.16 -(*T_TEST* )
2.17 +( *T_TEST*)
2.18 | pt_model (Ctree.PblObj {probl, spec, origin = (_, spec', hdl), ctxt, ...}) _(*Frm,Pbl*) =
2.19 let
2.20 val (_, pI, _) = Ctree.get_somespec' spec spec'
2.21 @@ -63,7 +63,7 @@
2.22 in
2.23 Ctree.ModSpec (allcorrect, Pos.Pbl, hdl, probl, where_, spec)
2.24 end
2.25 -( *T_TESTnew*)
2.26 +(*T_TESTnew*)
2.27 | pt_model _ _ = raise ERROR "pt_model: uncovered definition"
2.28
2.29 fun pt_form (Ctree.PrfObj {form, ...}) = Ctree.Form form
3.1 --- a/src/Tools/isac/Specify/i-model.sml Fri Jul 21 14:16:57 2023 +0200
3.2 +++ b/src/Tools/isac/Specify/i-model.sml Wed Jul 26 11:12:55 2023 +0200
3.3 @@ -70,12 +70,12 @@
3.4 Pre_Conds.unchecked -> T_TEST -> variants option
3.5 val is_complete_variant: int -> T_TEST-> bool
3.6
3.7 -(*T_TESTold*)
3.8 +(*T_TESTold* )
3.9 val of_max_variant: Model_Pattern.T -> T_TEST -> T_TEST * Pre_Conds.env_subst * Pre_Conds.env_eval
3.10 -(*T_TEST* )
3.11 +( *T_TEST*)
3.12 val of_max_variant:Model_Pattern.T -> Model_Def.i_model_TEST ->
3.13 Model_Def.i_model_TEST * Env.T * (Pre_Conds.env_subst * Pre_Conds.env_eval)
3.14 -( *T_TESTnew*)
3.15 +(*T_TESTnew*)
3.16
3.17 (*from isac_test for Minisubpbl*)
3.18 val penv_to_string: Proof.context -> T -> string
4.1 --- a/src/Tools/isac/Specify/pre-conditions.sml Fri Jul 21 14:16:57 2023 +0200
4.2 +++ b/src/Tools/isac/Specify/pre-conditions.sml Wed Jul 26 11:12:55 2023 +0200
4.3 @@ -46,13 +46,13 @@
4.4 val sep_variants_envs_OLD: Model_Pattern.T -> Model_Def.i_model_TEST ->
4.5 env_subst * env_eval;
4.6
4.7 -(*T_TESTold*)
4.8 +(*T_TESTold* )
4.9 val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST ->
4.10 Model_Def.i_model_TEST * env_subst * env_eval
4.11 -(*T_TEST* )
4.12 +( *T_TEST*)
4.13 val of_max_variant:Model_Pattern.T -> Model_Def.i_model_TEST ->
4.14 Model_Def.i_model_TEST * Env.T * (env_subst * env_eval)
4.15 -( *T_TESTnew*)
4.16 +(*T_TESTnew*)
4.17
4.18 (*from isac_test for Minisubpbl*)
4.19 val discern_feedback_subst: Model_Def.descriptor -> Model_Def.i_model_feedback_TEST -> Env.T;
4.20 @@ -500,19 +500,34 @@
4.21
4.22 (** of_max_variant **)
4.23
4.24 -(*T_TESTold*)
4.25 -(*T_TEST*)
4.26 +fun handle_lists id (descr, ts) =
4.27 + if Model_Pattern.is_list_descr descr
4.28 + then if length ts > 1 (*list with more than 1 element needs to collect by [.., .., ..]*)
4.29 + then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)] (*AdditValues [u, v]*)
4.30 + else if TermC.is_atom (Library.the_single ts)
4.31 + then [(id, Library.the_single ts)] (* solutions L, ...*)
4.32 + else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)](*Constants [r = 7]*)
4.33 + else [(id, Library.the_single ts)] (* solveFor x, Extremum (A = ...)*)
4.34 +
4.35 fun mk_env_model _ (Model_Def.Cor_TEST ((_, []), _)) = []
4.36 | mk_env_model id (Model_Def.Cor_TEST ((descr, ts), _)) =
4.37 +(*T_TEST.150* )
4.38 if Model_Pattern.is_list_descr descr
4.39 then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)]
4.40 else [(id, hd ts)]
4.41 +( *T_TEST*)
4.42 + handle_lists id (descr, ts)
4.43 +(*T_TEST.100*)
4.44 | mk_env_model _ (Model_Def.Syn_TEST _) = [] (*TODO handle correct list elements*)
4.45 | mk_env_model _ (Model_Def.Inc_TEST ((_, []), _)) = []
4.46 | mk_env_model id (Model_Def.Inc_TEST ((descr, ts), _)) =
4.47 +(*T_TEST.150* )
4.48 if Model_Pattern.is_list_descr descr
4.49 then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)]
4.50 else [(id, hd ts)]
4.51 +( *T_TEST*)
4.52 + handle_lists id (descr, ts)
4.53 +(*T_TEST.100*)
4.54 | mk_env_model _ (Model_Def.Sup_TEST _) = []
4.55 fun make_env_model equal_descr_pairs =
4.56 map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
4.57 @@ -563,12 +578,12 @@
4.58 fun cnt_corrects i_model =
4.59 fold (curry op +) (map (fn (_, _, _, _, (Cor_TEST _, _)) => 1 | _ => 0) i_model) 0;
4.60
4.61 -(*T_TESTold*)
4.62 +(*T_TESTold* )
4.63 fun of_max_variant model_patt i_model =
4.64 -(*T_TEST* )
4.65 +( *T_TEST*)
4.66 fun of_max_variant _ [] = ([], [], ([], []))
4.67 | of_max_variant model_patt i_model =
4.68 -( *T_TESTnew*)
4.69 +(*T_TESTnew*)
4.70 let
4.71 val all_variants =
4.72 map (fn (_, variants, _, _, _) => variants) i_model
4.73 @@ -582,13 +597,13 @@
4.74 val i_model_max =
4.75 filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
4.76 val equal_descr_pairs = map (get_equal_descr i_model) model_patt |> flat
4.77 -(*T_TESTold*)
4.78 +(*T_TESTold* )
4.79 val env_subst = mk_env_subst_DEL equal_descr_pairs
4.80 val env_eval = mk_env_eval_DEL i_model_max
4.81 in
4.82 (i_model_max, env_subst, env_eval)
4.83 end
4.84 -(*T_TEST* )
4.85 +( *T_TEST*)
4.86 val env_model = make_env_model equal_descr_pairs
4.87 val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
4.88 val subst_eval_list = make_envs_preconds equal_givens
4.89 @@ -596,7 +611,7 @@
4.90 in
4.91 (i_model_max, env_model, (env_subst, env_eval))
4.92 end
4.93 -( *T_TESTnew*)
4.94 +(*T_TESTnew*)
4.95
4.96
4.97 (** check pre-conditions **)
4.98 @@ -630,20 +645,24 @@
4.99 end
4.100
4.101
4.102 -(* expects the precondition from Problem, ie. needs substitution *)
4.103 +(* expects the precondition from Problem, ie. needs substitution by env_model*)
4.104 fun check_OLD _ _ [] _ = (true, [])
4.105 | check_OLD ctxt where_rls pres (model_patt, i_model) =
4.106 let
4.107 -(*T_TESTold*)
4.108 +(*T_TESTold* )
4.109 val (env_subst, env_eval) = sep_variants_envs_OLD model_patt i_model
4.110 -(*T_TEST* )
4.111 - val (_, _, (env_subst, env_eval)) = of_max_variant model_patt i_model
4.112 -( *T_TESTnew*)
4.113 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
4.114 val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
4.115 +( *T_TEST*)
4.116 + val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
4.117 + val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
4.118 + val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
4.119 + val full_subst = if env_eval = [] then pres_subst_other
4.120 + else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
4.121 +(*T_TESTnew*)
4.122 val evals = map (eval ctxt where_rls) full_subst
4.123 in
4.124 - (foldl and_ (true, map fst evals), pres_subst)
4.125 + (foldl and_ (true, map fst evals), pres_subst_other)
4.126 end;
4.127
4.128 fun unchecked_OLD_to_TEST pres = map (fn t => (t, Position.none)) pres
5.1 --- a/src/Tools/isac/Specify/specify-step.sml Fri Jul 21 14:16:57 2023 +0200
5.2 +++ b/src/Tools/isac/Specify/specify-step.sml Wed Jul 26 11:12:55 2023 +0200
5.3 @@ -42,7 +42,7 @@
5.4 | check (Tactic.Del_Find ct') _ = Applicable.Yes (Tactic.Del_Find' ct')
5.5 | check (Tactic.Del_Given ct') _ = Applicable.Yes (Tactic.Del_Given' ct')
5.6 | check (Tactic.Del_Relation ct') _ = Applicable.Yes (Tactic.Del_Relation' ct')
5.7 -(*T_TESTold*)
5.8 +(*T_TESTold* )
5.9 | check Tactic.Model_Problem (pt, pos as (p, _)) =
5.10 let
5.11 val (pI', ctxt) = case Ctree.get_obj I pt p of
5.12 @@ -51,7 +51,7 @@
5.13 val {model, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
5.14 val pbl = I_Model.init model
5.15 in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
5.16 -(*T_TEST* )
5.17 +( *T_TEST*)
5.18 | check Tactic.Model_Problem (pt, pos as (p, _)) =
5.19 let
5.20 val (o_model, pI') = case Ctree.get_obj I pt p of
5.21 @@ -60,7 +60,7 @@
5.22 val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
5.23 val pbl = I_Model.init_TEST o_model model_patt
5.24 in Applicable.Yes (Tactic.Model_Problem' (pI', I_Model.TEST_to_OLD pbl, [])) end
5.25 -( *T_TESTnew*)
5.26 +(*T_TESTnew*)
5.27 | check (Tactic.Refine_Problem pI) (pt, (p, _)) =
5.28 let
5.29 val (dI, dI', itms, ctxt) = case Ctree.get_obj I pt p of
6.1 --- a/src/Tools/isac/Specify/specify.sml Fri Jul 21 14:16:57 2023 +0200
6.2 +++ b/src/Tools/isac/Specify/specify.sml Wed Jul 26 11:12:55 2023 +0200
6.3 @@ -99,6 +99,7 @@
6.4 SOME (fd, ct') => ("dummy", (Pos.Pbl, P_Model.mk_additem fd ct'))
6.5 | NONE => (*pbl-items complete*)
6.6 if not preok then ("dummy", (Pos.Pbl, Tactic.Refine_Problem pI'))
6.7 + (*this is an ERROR fall through ------^^^^^^^^^^^^^^^^^^^^^ for Pre_Conds, redesign ?*)
6.8 else if dI = ThyC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Theory dI'))
6.9 else if pI = Problem.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Problem pI'))
6.10 else if mI = MethodC.id_empty then ("dummy", (Pos.Pbl, Tactic.Specify_Method mI'))
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/test/Tools/isac/Minisubpbl/100-init-rootpbl-NEXT_STEP.sml Wed Jul 26 11:12:55 2023 +0200
7.3 @@ -0,0 +1,429 @@
7.4 +(* Title: "Minisubpbl/100-init-rootpbl-NEXT_STEP.sml"
7.5 + Author: Walther Neuper 2307
7.6 +*)
7.7 +
7.8 +open Ctree;
7.9 +open Pos;
7.10 +open TermC;
7.11 +open Istate;
7.12 +open Tactic;
7.13 +open I_Model;
7.14 +open Pre_Conds;
7.15 +open Rewrite;
7.16 +open Step;
7.17 +open LItool;
7.18 +open LI;
7.19 +
7.20 +"----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
7.21 +"----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
7.22 +"----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
7.23 +tracing "--- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
7.24 +val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
7.25 +val (dI',pI',mI') =
7.26 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
7.27 + ["Test", "squ-equ-test-subpbl1"]);
7.28 +val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
7.29 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Model_Problem = tac
7.30 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Theory "Test" = tac
7.31 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Problem ["sqroot-test", "univariate", "equation", "test"] = tac
7.32 +
7.33 +(*[], Met*)val return_Step_do_next_Specify_Problem = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
7.34 +(*/------------------- step into Step.do_next_Specify_Problem ------------------------------\\*)
7.35 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
7.36 + (p, ((pt, e_pos'), []));
7.37 + (*if*) Pos.on_calc_end ip (*else*);
7.38 + val (_, probl_id, _) = Calc.references (pt, p);
7.39 +val _ =
7.40 + (*case*) tacis (*of*);
7.41 + (*if*) probl_id = Problem.id_empty (*else*);
7.42 +
7.43 + Step.switch_specify_solve p_ (pt, ip);
7.44 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
7.45 + (*if*) Pos.on_specification ([], state_pos) (*then*);
7.46 +
7.47 + Step.specify_do_next (pt, input_pos);
7.48 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
7.49 + val (_, (p_', tac)) = Specify.find_next_step ptp
7.50 + val ist_ctxt = Ctree.get_loc pt (p, p_)
7.51 +val _ =
7.52 + (*case*) tac (*of*);
7.53 +
7.54 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
7.55 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos)) =
7.56 + (tac, (pt, (p, p_')));
7.57 +
7.58 + val (o_model, ctxt, i_model) =
7.59 +Specify_Step.complete_for id (pt, pos);
7.60 +"~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
7.61 + val {origin = (o_model, _, _), probl = i_prob, ctxt,
7.62 + ...} = Calc.specify_data (ctree, pos);
7.63 + val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
7.64 + val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
7.65 + val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
7.66 +
7.67 + val (_, (i_model, _)) =
7.68 + M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
7.69 +"~~~~~ fun match_itms_oris , args:"; val (ctxt, pbl, (pbt, where_, where_rls), oris) =
7.70 + (ctxt, i_prob, (m_patt, where_, where_rls), o_model');
7.71 + (*0*)val mv = Pre_Conds.max_variant pbl;
7.72 +
7.73 + fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;
7.74 + fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
7.75 + SOME _ => false | NONE => true;
7.76 + (*1*)val mis = (filter (notmem pbl)) pbt;
7.77 + fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
7.78 + fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
7.79 + (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
7.80 + val news = (flat o (map (oris2itms oris))) mis;
7.81 + (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
7.82 + val newitms = filter mem_vat news;
7.83 + (*4*)val itms' = pbl @ newitms;
7.84 +
7.85 + val (pb, where_') =
7.86 + Pre_Conds.check ctxt where_rls where_ itms' mv;
7.87 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, pbl, (_)) =
7.88 + (ctxt, where_rls, where_, itms', mv);
7.89 + val env = Pre_Conds.environment pbl;
7.90 + val pres' = map (TermC.subst_atomic_all env) pres;
7.91 +
7.92 +(*+*)val "Test" = ctxt |> Proof_Context.theory_of |> ThyC.id_of
7.93 +(*+*)val Rule_Set.Repeat {id = "prls_met_test_squ_sub", ...} = where_rls
7.94 +(*+*)val [(true, tTEST as Const ("Test.precond_rootmet", _) $ Free ("x", xxx))] = pres'
7.95 +
7.96 +(*+*)val ctxt = Config.put rewrite_trace true ctxt;
7.97 + val evals = map (
7.98 + Pre_Conds.eval ctxt where_rls) pres';
7.99 +(* (*declare [[rewrite_trace = true]]*)
7.100 +@## rls: prls_met_test_squ_sub on: precond_rootmet x
7.101 +@### try calc: "Test.precond_rootmet"
7.102 +@#### eval asms: "(precond_rootmet x) = True"
7.103 +@### calc. to: True
7.104 +@### try calc: "Test.precond_rootmet"
7.105 +@### try calc: "Test.precond_rootmet"
7.106 +*)
7.107 +(*+*)val ctxt = Config.put rewrite_trace false ctxt;
7.108 +
7.109 +"~~~~~ fun eval_precond_rootmet , args:"; val ((thmid:string), _, (t as (Const (\<^const_name>\<open>Test.precond_rootmet\<close>, _) $ arg)), ctxt) =
7.110 + ("aaa", "bbb", tTEST, ctxt);
7.111 + SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg) "",
7.112 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
7.113 +;
7.114 + (TermC.mk_thmid thmid (UnparseC.term ctxt arg)) "";
7.115 +"~~~~~ fun mk_thmid , args:"; val (thmid, n1, n2) = (thmid, (UnparseC.term ctxt arg), "");
7.116 + thmid ^ (cut_longid n1) ^ "_" ^ (cut_longid n2);
7.117 +
7.118 + (cut_longid n2);
7.119 +"~~~~~ fun cut_longid , args:"; val (dn) = (n2);
7.120 +(*\------------------- step into Step.do_next_Specify_Problem ------------------------------//*)
7.121 +val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Specify_Problem; val Specify_Method ["Test", "squ-equ-test-subpbl1"] = tac;
7.122 +
7.123 +(*[1], Frm*)val return_Step_do_next_Specify_Method = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
7.124 +(*/------------------- step into Specify_Method --------------------------------------------\\*)
7.125 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
7.126 + (p, ((pt, e_pos'), []));
7.127 + (*if*) Pos.on_calc_end ip (*else*);
7.128 + val (_, probl_id, _) = Calc.references (pt, p);
7.129 +val _ =
7.130 + (*case*) tacis (*of*);
7.131 + (*if*) probl_id = Problem.id_empty (*else*);
7.132 +
7.133 + switch_specify_solve p_ (pt, ip);
7.134 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
7.135 + (*if*) Pos.on_specification ([], state_pos) (*then*);
7.136 +
7.137 + specify_do_next (pt, input_pos);
7.138 +"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
7.139 + val (_, (p_', tac)) = Specify.find_next_step ptp
7.140 + val ist_ctxt = Ctree.get_loc pt (p, p_)
7.141 +(*+*)val Tactic.Apply_Method mI =
7.142 + (*case*) tac (*of*);
7.143 +
7.144 + LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
7.145 + ist_ctxt (pt, (p, p_'));
7.146 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
7.147 + ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)),
7.148 + ist_ctxt, (pt, (p, p_')));
7.149 + val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
7.150 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
7.151 + | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
7.152 + val {model, ...} = MethodC.from_store ctxt mI;
7.153 + val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
7.154 +
7.155 + val (is, env, ctxt, prog) = case
7.156 + LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI of
7.157 + (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
7.158 +val return_init_pstate = (is, env, ctxt, prog)
7.159 +(*#------------------- un-hide local of init_pstate -----------------------------------------\*)
7.160 +fun msg_miss ctxt sc metID caller f formals actuals =
7.161 + "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
7.162 + "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"" ^ caller ^ "\":\n" ^
7.163 + "formal arg \"" ^ UnparseC.term ctxt f ^ "\" doesn't match any actual arg.\n" ^
7.164 + "with:\n" ^
7.165 + (string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms ctxt formals ^ "\n" ^
7.166 + (string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms ctxt actuals
7.167 +fun msg_miss_type ctxt sc metID f formals actuals =
7.168 + "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
7.169 + "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
7.170 + "formal arg \"" ^ UnparseC.term ctxt f ^ "\" of type \"" ^ UnparseC.typ ctxt (type_of f) ^
7.171 + "\" doesn't mach any actual arg.\nwith:\n" ^
7.172 + (string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms ctxt formals ^ "\n" ^
7.173 + (string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms ctxt actuals ^ "\n" ^
7.174 + " with types: " ^ (strs2str o (map ((UnparseC.typ ctxt) o type_of))) actuals
7.175 +fun msg_ambiguous ctxt sc metID f aas formals actuals =
7.176 + "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
7.177 + "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
7.178 + "formal arg. \"" ^ UnparseC.term ctxt f ^ "\" type-matches with several..." ^
7.179 + "actual args. \"" ^ UnparseC.terms ctxt aas ^ "\"\n" ^
7.180 + "selected \"" ^ UnparseC.term ctxt (hd aas) ^ "\"\n" ^
7.181 + "with\n" ^
7.182 + "formals: " ^ UnparseC.terms ctxt formals ^ "\n" ^
7.183 + "actuals: " ^ UnparseC.terms ctxt actuals
7.184 +fun trace_init ctxt metID =
7.185 + if Config.get ctxt LI_trace
7.186 + then tracing("@@@ program \"" ^ strs2str metID ^ "\"")
7.187 + else ();
7.188 +
7.189 +fun assoc_by_type ctxt f aa prog met_id formals actuals =
7.190 + case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
7.191 + [] => raise ERROR (msg_miss_type ctxt prog met_id f formals actuals)
7.192 + | [a] => (f, a)
7.193 + | aas as (a :: _) => (writeln (msg_ambiguous ctxt prog met_id f aas formals actuals); (f, a));
7.194 +(*
7.195 + fun assoc_formals_actuals: at "PIDE turn 11" ONLY syntax revised, NOT semantics
7.196 + Env.T -> (* [] for building return Env.T *)
7.197 + term list -> (* changed during building return Env.T *)
7.198 + term list -> (* changed during building return Env.T *)
7.199 + Proof.context -> (* *)
7.200 + term -> (* program code *)
7.201 + MethodC.id -> (* for error msg *)
7.202 + term list -> (* original value, unchanged *)
7.203 + term list -> (* original value, unchanged *)
7.204 + Env.T (* return Env.T *)
7.205 +*)
7.206 +fun relate_args _ (f::_) [] ctxt prog met_id formals actuals =
7.207 + raise ERROR (msg_miss ctxt prog met_id "relate_args" f formals actuals)
7.208 + | relate_args env [] _ _ _ _ _ _ = env (*may drop Find?*)
7.209 + | relate_args env (f::ff) (aas as (a::aa)) ctxt prog met_id formals actuals =
7.210 + if type_of f = type_of a
7.211 + then relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals
7.212 + else
7.213 + let val (f, a) = assoc_by_type ctxt f aas prog met_id formals actuals
7.214 + in relate_args (env @ [(f, a)]) ff (remove op = a aas) ctxt prog met_id formals actuals end
7.215 +;
7.216 +(*+*)relate_args: Env.T -> term list -> term list -> Proof.context -> term -> MethodC.id ->
7.217 + term list -> term list -> Env.T;
7.218 +(*#------------------- un-hide local of init_pstate -----------------------------------------/*)
7.219 +
7.220 +(*//------------------ step into init_pstate NEW -------------------------------------------\\*)
7.221 +val (_, ctxt, i_model, met_id) = (prog_rls, ctxt, itms, mI);
7.222 +"~~~~~ fun init_pstate , args:"; val (ctxt, i_model, met_id) =
7.223 + (ctxt, I_Model.OLD_to_TEST i_model, met_id);
7.224 + val (model_patt, program, prog, prog_rls, where_, where_rls) =
7.225 + case MethodC.from_store ctxt met_id of
7.226 + {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...} =>
7.227 + (model_patt, program, prog, prog_rls, where_, where_rls)
7.228 + | _ => raise ERROR ("init_pstate with " ^ MethodC.id_to_string met_id)
7.229 +
7.230 + val (i_model_max, env_subst, env_eval) =
7.231 + of_max_variant model_patt i_model;
7.232 +val return_of_max_variant = (i_model_max, env_subst, env_eval);
7.233 +(*///----------------- step into of_max_variant NEW ----------------------------------------\\*)
7.234 +"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
7.235 +
7.236 +(*+*)i_model: I_Model.T_TEST;
7.237 +
7.238 + val all_variants =
7.239 + map (fn (_, variants, _, _, _) => variants) i_model
7.240 + |> flat
7.241 + |> distinct op =
7.242 + val variants_separated = map (filter_variants' i_model) all_variants
7.243 + val sums_corr = map (cnt_corrects) variants_separated
7.244 +(*+*)val [3] = sums_corr;
7.245 +
7.246 + val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
7.247 +(*+*)val [(3, 1)] = sum_variant_s;
7.248 +
7.249 + val (_, max_variant) = hd (*..crude decision, up to improvement *)
7.250 + (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
7.251 +(*+*)val 1 = max_variant;
7.252 +
7.253 + val i_model_max =
7.254 + filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
7.255 +(*+*)val 3 = length i_model_max;
7.256 +
7.257 + val equal_descr_pairs =
7.258 + map (get_equal_descr i_model) model_patt
7.259 + |> flat
7.260 +(*+*)val 3 = length equal_descr_pairs; (*only 1 variant in this test*)
7.261 +
7.262 + val env_subst =
7.263 + Pre_Conds.mk_env_subst_DEL equal_descr_pairs;
7.264 +(*+*)(equal_descr_pairs |> descr_pairs_to_string @{context}) = "[" ^
7.265 + "((#Given, (equality, e_e)), " ^
7.266 + "(1, [1], true ,#Given, (Cor_TEST equality (x + 1 = 2) ,(e_e, [x + 1 = 2]), Position.T))), " ^
7.267 + "((#Given, (solveFor, v_v)), " ^
7.268 + "(2, [1], true ,#Given, (Cor_TEST solveFor x ,(v_v, [x]), Position.T))), " ^
7.269 + "((#Find, (solutions, v_v'i')), " ^
7.270 + "(3, [1], true ,#Find, (Cor_TEST solutions L ,(v_v'i', [L]), Position.T)))]";
7.271 +(*------------------------------------------------^^^^^^^^^^^^^--- NOT FOUND*)
7.272 +
7.273 +(*////--------- ------ step into mk_env_subst_DEL ------------------------------------------\\*)
7.274 +"~~~~~ fun mk_env_subst_DEL , args:"; val (equal_descr_pairs) = (equal_descr_pairs);
7.275 +
7.276 +val xxx =
7.277 + (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
7.278 + => (discern_feedback_subst id feedb));
7.279 +"~~~~~ fun xxx , args:"; val ((_, (_, id)), (_, _, _, _, (feedb, _))) = (nth 3 equal_descr_pairs);
7.280 +val [(Free ("v_v'i'", _), Free ("L", _))] =
7.281 + (discern_feedback_subst id feedb);
7.282 +"~~~~~ fun discern_feedback_subst , args:"; val (id, (Model_Def.Cor_TEST ((descr, [ts]), _)))
7.283 + = (id, feedb);
7.284 + discern_type_subst (descr, id) [ts];
7.285 +"~~~~~ fun discern_type_subst , args:"; val ((descr, id), ts) = ((descr, id), [ts]);
7.286 +val (Type ("fun", [Type ("List.list", [Type ("HOL.bool", [])]), _])) =
7.287 + (*case*) type_of descr (*of*);
7.288 + (*if*) TermC.is_list (hd ts) (*else*);
7.289 +
7.290 +val return_discern_type_subst_3 =
7.291 +(* if TermC.is_list (hd ts)
7.292 + then [(id, ts |> map TermC.the_single |> TermC.list2isalist HOLogic.boolT)]
7.293 + else*) [(id, Library.the_single ts)]
7.294 +
7.295 +(*\\\\---------------- step into mk_env_subst_DEL ------------------------------------------//*)
7.296 +(*+*)val "[\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\", \"\n(v_v'i', L)\"]" =
7.297 + env_subst |> Subst.to_string @{context}
7.298 +
7.299 +(*|||----------------- contine of_max_variant ------------------------------------------------*)
7.300 + val env_eval = Pre_Conds.mk_env_eval_DEL i_model_max
7.301 +(*+*)val [] =
7.302 + map (fn (t1, t2) => "(" ^ UnparseC.term @{context} t1 ^ ", " ^ UnparseC.term @{context} t2 ^ ")")
7.303 + env_eval
7.304 +
7.305 +val return_of_max_variant_step = (i_model_max, env_subst, env_eval);
7.306 +(*+*)if return_of_max_variant_step = return_of_max_variant then () else error "<>";
7.307 +(*\\\----------------- step into of_max_variant NEW ----------------------------------------\\*)
7.308 +val (i_model_max, env_subst, _) = return_of_max_variant
7.309 +
7.310 +(*||------------------ continue init_pstate NEW --------------------------------------------\\*)
7.311 + val actuals = map snd env_subst
7.312 +(*+*)val "[x + 1 = 2, x, L]" = actuals |> UnparseC.terms @{context}
7.313 +
7.314 + val formals = Program.formal_args prog
7.315 +(*+*)val "[e_e, v_v]" = (formals |> UnparseC.terms @{context})
7.316 +
7.317 +(*+*)val "minisubpbl e_e v_v =\n(let e_ea =\n (Try (Rewrite_Set ''norm_equation'') #>\n Try (Rewrite_Set ''Test_simplify''))\n e_e;\n L_La =\n SubProblem\n (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],\n [''Test'', ''solve_linear''])\n [BOOL e_e, REAL v_v]\n in Check_elementwise L_L {v_v. Assumptions})" =
7.318 + (prog |> UnparseC.term @{context})
7.319 +
7.320 + val preconds =
7.321 + Pre_Conds.check_from_store ctxt where_rls where_ env_subst env_eval
7.322 +val return_check_from_store = preconds
7.323 +(*+*)val (true, [(true, Const ("Test.precond_rootmet", _) $ Free ("x", _))]) = return_check_from_store;
7.324 +(*///----------------- step into check_from_store ------------------------------------------//*)
7.325 +"~~~~~ fun check_from_store , args:"; val (ctxt, where_rls, preconds, env_subst, env_eval) =
7.326 + (ctxt, where_rls, where_, env_subst, env_eval);
7.327 +
7.328 +(*+*)val "[precond_rootmet v_v]" = (where_ |> UnparseC.terms @{context})
7.329 +(*+*)val "[\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\", \"\n(v_v'i', L)\"]" = env_subst |> Subst.to_string @{context}
7.330 +(*+*)val [] = env_eval (*special case, Maximum-expl more general*)
7.331 +
7.332 + val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
7.333 +(*+*)val [(true, Const ("Test.precond_rootmet", _) $ Free ("x", _))] = pres_subst
7.334 +
7.335 + val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
7.336 +(*+*)val [(true, Const ("Test.precond_rootmet", _) $ Free ("x", _))] = full_subst
7.337 +
7.338 + val evals = map (eval ctxt where_rls) full_subst
7.339 +(*+*)val [(true, Const ("Test.precond_rootmet", _) $ Free ("x", _))] = evals
7.340 +
7.341 +val return_check_from_store_step = (foldl and_ (true, map fst evals), pres_subst)
7.342 +(*+*)val (true, [(true, Const ("Test.precond_rootmet", _) $ Free ("x", _))]) =
7.343 + return_check_from_store_step;
7.344 +(*+*)if return_check_from_store_step = return_check_from_store then () else error "<>";
7.345 +(*\\\----------------- step into check_from_store ------------------------------------------//*)
7.346 + val preconds = return_check_from_store
7.347 +
7.348 +(*||------------------ continue init_pstate NEW --------------------------------------------\\*)
7.349 + val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));
7.350 + val ist = Istate.e_pstate
7.351 + |> Istate.set_eval prog_rls
7.352 + |> Istate.set_env_true (relate_args [] formals actuals ctxt prog met_id formals actuals);
7.353 +(*+*) (relate_args [] formals actuals ctxt prog met_id formals actuals);
7.354 +(*+*)val "[\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\"]" =
7.355 + (relate_args [] formals actuals ctxt prog met_id formals actuals)
7.356 + |> Subst.to_string @{context}
7.357 +
7.358 +val return_init_pstate_steps = (* = return_init_pstate*)
7.359 + (Istate.Pstate ist, ctxt, program)
7.360 +(*\\------------------ step into init_pstate NEW -------------------------------------------//*)
7.361 +val (is, env, ctxt, prog) = return_init_pstate;
7.362 +
7.363 +(*|------------------- continuing Specify_Method ---------------------------------------------*)
7.364 +(*\------------------- step into Specify_Method --------------------------------------------//*)
7.365 +val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Specify_Method; val Apply_Method ["Test", "squ-equ-test-subpbl1"] = tac;
7.366 +
7.367 +(*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Rewrite_Set "norm_equation" = tac
7.368 +
7.369 +(*[1], Res*)val return_Step_do_next_Rewrite_Set = Step.do_next p ((pt, e_pos'), []);
7.370 +(*/------------------- step into Apply_Method ----------------------------------------------\\*)
7.371 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
7.372 + (p ,((pt, e_pos'), []));
7.373 + (*if*) Pos.on_calc_end ip (*else*);
7.374 + val (_, probl_id, _) = Calc.references (pt, p);
7.375 +val _ =
7.376 + (*case*) tacis (*of*);
7.377 + (*if*) probl_id = Problem.id_empty (*else*);
7.378 +
7.379 + Step.switch_specify_solve p_ (pt, ip);
7.380 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos))
7.381 + = (p_, (pt, ip));
7.382 + (*if*) Pos.on_specification ([], state_pos) (*else*);
7.383 +
7.384 + LI.do_next (pt, input_pos);
7.385 +"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
7.386 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
7.387 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
7.388 +
7.389 +val return_LI_find_next_step = (*case*)
7.390 + LI.find_next_step sc (pt, pos) ist ctxt (*of*);
7.391 +(*//------------------ step into LI.find_next_step -----------------------------------------\\*)
7.392 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Istate.Pstate ist), ctxt) =
7.393 + (sc, (pt, pos), ist, ctxt);
7.394 +(*.. this showed that we have ContextC.empty*)
7.395 +(*\\------------------ step into LI.find_next_step -----------------------------------------//*)
7.396 +val LI.Next_Step (ist, ctxt, tac) = return_LI_find_next_step;
7.397 +
7.398 + LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
7.399 +"~~~~~ fun by_tactic , args:"; val (tac_, ic, (pt, pos))
7.400 + = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp);
7.401 + val pos = next_in_prog' pos
7.402 +
7.403 + val (pos', c, _, pt) =
7.404 +Solve_Step.add_general tac_ ic (pt, pos);
7.405 +"~~~~~ fun add_general , args:"; val (tac, ic, cs)
7.406 + = (tac_, ic, (pt, pos));
7.407 + (*if*) Tactic.for_specify' tac (*else*);
7.408 +
7.409 +Solve_Step.add tac ic cs;
7.410 +"~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))
7.411 + = (tac, ic, cs);
7.412 + val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
7.413 + (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete
7.414 + val pt = Ctree.update_branch pt p Ctree.TransitiveB
7.415 +
7.416 +val return =
7.417 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term ctxt f'), pt)
7.418 +(*\------------------- step into Apply_Method ----------------------------------------------//*)
7.419 +val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Rewrite_Set
7.420 +
7.421 +(* final test ... ----------------------------------------------------------------------------*)
7.422 +(*+*)val ([2], Res) = p;
7.423 +Test_Tool.show_pt_tac pt; (*[
7.424 +([], Frm), solve (x + 1 = 2, x)
7.425 +. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
7.426 +([1], Frm), x + 1 = 2
7.427 +. . . . . . . . . . Rewrite_Set "norm_equation",
7.428 +([1], Res), x + 1 + - 1 * 2 = 0
7.429 +. . . . . . . . . . Rewrite_Set "Test_simplify",
7.430 +([2], Res), - 1 + x = 0
7.431 +. . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"]] ..INCORRECT
7.432 +*)
8.1 --- a/test/Tools/isac/Minisubpbl/150-add-given-Equation.sml Fri Jul 21 14:16:57 2023 +0200
8.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given-Equation.sml Wed Jul 26 11:12:55 2023 +0200
8.3 @@ -1,4 +1,4 @@
8.4 -(* Title: "Minisubpbl/150b-add-given-Equation.sml"
8.5 +(* Title: "Minisubpbl/150-add-given-Equation.sml"
8.6 Author: Walther Neuper 1105
8.7 (c) copyright due to lincense terms.
8.8 *)
8.9 @@ -14,16 +14,18 @@
8.10 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))]; (*nxt = ("Model_Problem"*)
8.11 val Model_Problem = nxt
8.12
8.13 -val return_me_Model_Problem = me nxt p [] pt;
8.14 -(*/------------------- step into me_Model_Problem ------------------------------------------\\*)
8.15 +val return_me_Model_Problem =
8.16 + me nxt p [] pt;
8.17 +(*/------------------- step into me Model_Problem ------------------------------------------\\*)
8.18 "~~~~~ fun me , args:"; val (tac, (p:Pos.pos'), (_:Test_Code.NEW), (pt:Ctree.ctree)) = (nxt, p, [], pt);
8.19 val (pt, p) =
8.20 (*ERROR Specify.item_to_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt ... see 100-init-rootpbl.sml*)
8.21 case Step.by_tactic tac (pt,p) of
8.22 ("ok", (_, _, ptp)) => ptp;
8.23
8.24 - (*case*)
8.25 +val return_do_next = (*case*)
8.26 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
8.27 +(*//------------------ step into do_next ---------------------------------------------------\\*)
8.28 "~~~~~ fun do_next , args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) =
8.29 (p, ((pt, e_pos'),[]));
8.30 val pIopt = get_pblID (pt,ip);
8.31 @@ -37,31 +39,36 @@
8.32
8.33 (*if*) Pos.on_specification ([], state_pos) (*then*);
8.34
8.35 - val ("ok", ([(Add_Given "equality (x + 1 = 2)", _, _)], [], _)) =
8.36 + val return_specify_do_next as ("ok", ([(Add_Given "equality (x + 1 = 2)", _, _)], [], _)) =
8.37 Step.specify_do_next (pt, input_pos);
8.38
8.39 (*+ keep for fun specify_do_next \<longrightarrow>fun switch_specify_solve*)val (pt'''''_', input_pos'''''_') =
8.40 (pt, input_pos);
8.41
8.42 +(*///----------------- step into specify_do_next -------------------------------------------\\*)
8.43 "~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
8.44 -
8.45 - val (_, (p_', tac)) = Specify.find_next_step ptp
8.46 + val (_, (p_', tac as Add_Given "equality (x + 1 = 2)")) = Specify.find_next_step ptp
8.47 val ist_ctxt = Ctree.get_loc pt (p, p_)
8.48 -
8.49 - val Add_Given "equality (x + 1 = 2)" = (*case*) tac (*of*);
8.50 +val _ =
8.51 + (*case*) tac (*of*);
8.52
8.53 val ("ok", ([(Add_Given "equality (x + 1 = 2)", _, _)], [], _)) =
8.54 Step_Specify.by_tactic_input tac (pt, (p, p_')) (*return from specify_do_next*);
8.55 -"~~~~~ fun specify_do_next \<longrightarrow>fun switch_specify_solve , return:"; val (result) =
8.56 - (Step.specify_do_next (pt'''''_', input_pos'''''_'));
8.57 +(*\\\----------------- step into specify_do_next -------------------------------------------//*)
8.58 +(*\\------------------ step into do_next ---------------------------------------------------//*)
8.59 +val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next;
8.60 +(*|------------------- continue with me_Model_Problem ----------------------------------------*)
8.61 +val tacis as (_::_) =
8.62 + (*case*) ts (*of*);
8.63 + val (tac, _, _) = last_elem tacis
8.64
8.65 - val scs as ("ok", _) = (*case*) result (*of*);
8.66 -
8.67 -"~~~~~ fun switch_specify_solve \<longrightarrow>fun Step.do_next , return:"; val ("ok", (tacis, c', (pt', p'))) =
8.68 - (scs);
8.69 -
8.70 - (*case*) tacis (*of*);
8.71 +val return_me_Model_Problem =
8.72 + (p, [] : NEW, TESTg_form ctxt (pt, p) (* form output comes from Step.by_tactic *),
8.73 + tac, Celem.Sundef, pt)
8.74 (*\------------------- step into me_Model_Problem ------------------------------------------//*)
8.75 val (p,_,f,nxt,_,pt) = return_me_Model_Problem
8.76 val Add_Given "equality (x + 1 = 2)" = nxt
8.77 +
8.78 +(*ERROR me: uncovered case Step.by_tactic* )
8.79 val (p,_,f,nxt,_,pt) = me nxt p [] pt; val Add_Given "solveFor x" = nxt;
8.80 +( *ERROR me: uncovered case Step.by_tactic*)
9.1 --- a/test/Tools/isac/Test_Theory.thy Fri Jul 21 14:16:57 2023 +0200
9.2 +++ b/test/Tools/isac/Test_Theory.thy Wed Jul 26 11:12:55 2023 +0200
9.3 @@ -72,15 +72,6 @@
9.4 \<close> ML \<open>
9.5 \<close>
9.6
9.7 -section \<open>===================================================================================\<close>
9.8 -section \<open>===== ============================================================================\<close>
9.9 -ML \<open>
9.10 -\<close> ML \<open>
9.11 -
9.12 -\<close> ML \<open>
9.13 -\<close> ML \<open>
9.14 -\<close>
9.15 -
9.16 section \<open>====="Minisubpbl/150a-add-given-Maximum.sml"=======================================\<close>
9.17 ML \<open>
9.18 \<close> ML \<open>
9.19 @@ -230,8 +221,6 @@
9.20 \<close> ML \<open>
9.21 val return_do_next = (*case*)
9.22 Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
9.23 -val ts = return_do_next |> #2 |> #1 |> hd (* keep for continuing me Model_Problem *)
9.24 -val continue_Model_Problem = (ts, (pt, p)) (* keep for continuing me Model_Problem *);
9.25 \<close> ML \<open> (*//----------- step into do_next ---------------------------------------------------\\*)
9.26 (*//------------------ step into do_next ---------------------------------------------------\\*)
9.27 "~~~~~ fun do_next , args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):Calc.state_pre)) =
9.28 @@ -282,21 +271,53 @@
9.29 \<close> ML \<open> (*//----------- adhoc inserted fun of_max_variant -----------------------------------\\*)
9.30 (*//------------------ adhoc inserted fun of_max_variant -----------------------------------\\*)
9.31 \<close> ML \<open>
9.32 +fun handle_lists id (descr, ts) =
9.33 + if Model_Pattern.is_list_descr descr
9.34 + then if length ts > 1 (*list with more than 1 element needs to collect by [.., .., ..]*)
9.35 + then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)] (*AdditValues [u, v]*)
9.36 + else if TermC.is_atom (Library.the_single ts)
9.37 + then [(id, Library.the_single ts)] (* solutions L, ...*)
9.38 + else [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)](*Constants [r = 7]*)
9.39 + else [(id, Library.the_single ts)] (* solveFor x, Extremum (A = ...)*)
9.40 +;
9.41 +handle_lists: term -> descriptor * term list -> (term * term) list
9.42 +\<close> ML \<open>
9.43 fun mk_env_model _ (Model_Def.Cor_TEST ((_, []), _)) = []
9.44 | mk_env_model id (Model_Def.Cor_TEST ((descr, ts), _)) =
9.45 +(*T_TEST.150* )
9.46 if Model_Pattern.is_list_descr descr
9.47 then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)]
9.48 else [(id, hd ts)]
9.49 +( *T_TEST*)
9.50 + handle_lists id (descr, ts)
9.51 +(*T_TEST.100*)
9.52 | mk_env_model _ (Model_Def.Syn_TEST _) = [] (*TODO handle correct list elements*)
9.53 | mk_env_model _ (Model_Def.Inc_TEST ((_, []), _)) = []
9.54 | mk_env_model id (Model_Def.Inc_TEST ((descr, ts), _)) =
9.55 +(*T_TEST.150* )
9.56 if Model_Pattern.is_list_descr descr
9.57 then [(id, TermC.list2isalist (Model_Pattern.typ_of_element descr) ts)]
9.58 else [(id, hd ts)]
9.59 +( *T_TEST*)
9.60 + handle_lists id (descr, ts)
9.61 +(*T_TEST.100*)
9.62 | mk_env_model _ (Model_Def.Sup_TEST _) = []
9.63 ;
9.64 mk_env_model: term -> Model_Def.i_model_feedback_TEST -> Env.T
9.65 \<close> ML \<open>
9.66 +val (id, (descr, ts)) = (@{term "v_v'i'::bool list"}, (@{term solutions}, [@{term "L::bool list"}]))
9.67 +\<close> ML \<open>
9.68 +\<close> ML \<open>
9.69 +\<close> ML \<open>
9.70 +is_atom (Library.the_single [@{term "r = (7::real)"}])
9.71 +\<close> ML \<open>
9.72 +\<close> ML \<open>
9.73 +\<close> ML \<open>
9.74 +\<close> ML \<open>
9.75 +\<close> ML \<open>
9.76 +\<close> ML \<open>
9.77 +\<close> ML \<open>
9.78 +\<close> ML \<open>
9.79 (* vvvvvvvvvvvv-- REPLACES mk_env_subst_DEL, THUS THE LATTER IS UNCHANGED*)
9.80 fun make_env_model equal_descr_pairs =
9.81 map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
9.82 @@ -381,13 +402,15 @@
9.83 (*T_TESTold* )
9.84 val (env_subst, env_eval) = sep_variants_envs_OLD model_patt i_model
9.85 ( *NEW*)
9.86 - val (_, _, (env_subst, env_eval)) = of_max_variant model_patt i_model
9.87 + val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
9.88 (*NEW*)
9.89 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
9.90 - val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
9.91 + val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
9.92 + val full_subst = if env_eval = [] then pres_subst_other
9.93 + else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
9.94 val evals = map (eval ctxt where_rls) full_subst
9.95 in
9.96 - (foldl and_ (true, map fst evals), pres_subst)
9.97 + (foldl and_ (true, map fst evals), pres_subst_other)
9.98 end
9.99 ;
9.100 check_OLD: Proof.context -> Rule_Def.rule_set -> term list -> Model_Pattern.T * I_Model.T_TEST ->
9.101 @@ -543,7 +566,9 @@
9.102 (*||||||-------------- contine check_OLD -----------------------------------------------------*)
9.103 \<close> ML \<open>
9.104 val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
9.105 - val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
9.106 + val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
9.107 + val full_subst = if env_eval = [] then pres_subst_other
9.108 + else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
9.109 val evals = map (eval ctxt where_rls) full_subst
9.110 val return_ = (i_model_max, env_subst, env_eval)
9.111 (*\\\\\\\------------- step into check_OLD -------------------------------------------------//*)
9.112 @@ -698,20 +723,19 @@
9.113 (*\\\----------------- step into specify_do_next -------------------------------------------//*)
9.114 \<close> ML \<open> (*\\----------- step into do_next ---------------------------------------------------//*)
9.115 (*\\------------------ step into do_next ---------------------------------------------------//*)
9.116 +val ("ok", (ts as (_, _, _) :: _, _, (pt, p))) = return_do_next
9.117 +\<close> ML \<open>
9.118
9.119 \<close> ML \<open>(*|------------- continue with me_Model_Problem ----------------------------------------*)
9.120 (*|------------------- continue with me_Model_Problem ----------------------------------------*)
9.121 -\<close> ML \<open> (*while make Test_Theory work*)
9.122 -val (ts, (pt, p)) = continue_Model_Problem;
9.123 -val ("ok", (ts as (_, _, _) :: _, _, _)) = return_do_next
9.124 +\<close> ML \<open>
9.125
9.126 val tacis as (_::_) =
9.127 (*case*) ts (*of*);
9.128 val (tac, _, _) = last_elem tacis
9.129
9.130 \<close> ML \<open>
9.131 -val return_Model_Problem = (p, [] : NEW,
9.132 - TESTg_form ctxt (pt, p), tac, Celem.Sundef, pt);
9.133 +val return_Model_Problem = (p, [] : NEW, TESTg_form ctxt (pt, p), tac, Celem.Sundef, pt);
9.134 \<close> ML \<open>
9.135 \<close> ML \<open> (*//----------- step into TESTg_form ------------------------------------------------\\*)
9.136 (*//------------------ step into TESTg_form ------------------------------------------------\\*)
9.137 @@ -1353,8 +1377,565 @@
9.138 \<close> ML \<open>
9.139 \<close>
9.140
9.141 +section \<open>===== "Minisubpbl/100-init-rootpbl-NEXT_STEP.sml" =================================\<close>
9.142 +ML \<open>
9.143 +\<close> ML \<open>
9.144 +(* Title: "Minisubpbl/100-init-rootpbl-NEXT_STEP.sml"
9.145 + Author: Walther Neuper 2307
9.146 +*)
9.147 +
9.148 +open Ctree;
9.149 +open Pos;
9.150 +open TermC;
9.151 +open Istate;
9.152 +open Tactic;
9.153 +open I_Model;
9.154 +open Pre_Conds;
9.155 +open Rewrite;
9.156 +open Step;
9.157 +open Specify;
9.158 +open LItool;
9.159 +open LI;
9.160 +
9.161 +"----------- Minisubpbl/100-init-rootpbl-NEXT_STEP.sml ---------------------------------------";
9.162 +"----------- Minisubpbl/100-init-rootpbl-NEXT_STEP.sml ---------------------------------------";
9.163 +"----------- Minisubpbl/100-init-rootpbl-NEXT_STEP.sml ---------------------------------------";
9.164 +tracing "--- Minisubplb/100-init-rootpbl-NEXT_STEP.sml ---------------------------------------";
9.165 +val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
9.166 +val (dI',pI',mI') =
9.167 + ("Test", ["sqroot-test", "univariate", "equation", "test"],
9.168 + ["Test", "squ-equ-test-subpbl1"]);
9.169 +val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
9.170 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Model_Problem = tac
9.171 +\<close> ML \<open>
9.172 +val return_do_next_Model_Problem as xxx =
9.173 + Step.do_next p ((pt, e_pos'), []);
9.174 +\<close> ML \<open>
9.175 +val return_do_next_Model_Problem as ("ok", ([(Specify_Theory "Test", _, _)], _, _))
9.176 + = Step.do_next p ((pt, e_pos'), []);
9.177 +\<close> ML \<open> (*/------------ step into do_next_Model_Problem -------------------------------------\\*)
9.178 +(*/------------------- step into do_next_Model_Problem -------------------------------------\\*)
9.179 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) = (p, ((pt, e_pos'), []));
9.180 +\<close> ML \<open>
9.181 + (*if*) Pos.on_calc_end ip (*else*);
9.182 +\<close> ML \<open>
9.183 + val (_, probl_id, _) = Calc.references (pt, p);
9.184 +\<close> ML \<open>
9.185 +val _ =
9.186 + (*case*) tacis (*of*);
9.187 +\<close> ML \<open>
9.188 + (*if*) probl_id = Problem.id_empty (*else*);
9.189 +\<close> ML \<open>
9.190 + switch_specify_solve p_ (pt, ip);
9.191 +\<close> ML \<open>
9.192 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
9.193 +\<close> ML \<open>
9.194 + (*if*) Pos.on_specification ([], state_pos) (*then*);
9.195 +\<close> ML \<open>
9.196 + specify_do_next (pt, input_pos);
9.197 +\<close> ML \<open>
9.198 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
9.199 +\<close> ML \<open>
9.200 + val (_, (p_', tac as Specify_Theory "Test")) =
9.201 + Specify.find_next_step ptp;
9.202 +\<close> ML \<open>
9.203 +"~~~~~ fun find_next_step , args:"; val ((pt, pos as (_, p_))) = (ptp);
9.204 +\<close> ML \<open>
9.205 + val {meth = met, origin = origin as (oris, o_refs as (_, pI', mI'), _), probl = pbl,
9.206 + spec = refs, ...} = Calc.specify_data (pt, pos);
9.207 + val ctxt = Ctree.get_ctxt pt pos
9.208 +\<close> ML \<open>
9.209 + (*if*) Ctree.just_created (pt, pos) andalso origin <> Ctree.e_origin (*else*);
9.210 +\<close> ML \<open>
9.211 + (*if*) p_ = Pos.Pbl (*then*);
9.212 +\<close> ML \<open>
9.213 + for_problem ctxt oris (o_refs, refs) (pbl, met);
9.214 +\<close> ML \<open>
9.215 +"~~~~~ fun for_problem , args:"; val (ctxt, oris, ((dI', pI', mI'), (dI, pI, mI)), (pbl, met)) =
9.216 + (ctxt, oris, (o_refs, refs), (pbl, met));
9.217 +\<close> ML \<open>
9.218 + val cpI = if pI = Problem.id_empty then pI' else pI;
9.219 + val cmI = if mI = MethodC.id_empty then mI' else mI;
9.220 + val {model = pbt, where_rls, where_, ...} = Problem.from_store ctxt cpI;
9.221 + val {model = mpc, ...} = MethodC.from_store ctxt cmI
9.222 +\<close> ML \<open> (*ERROR?---vvvvv*)
9.223 + val (preok as true, xxx) =
9.224 + Pre_Conds.check_OLD ctxt where_rls where_ (pbt, I_Model.OLD_to_TEST pbl);
9.225 +\<close> ML \<open>
9.226 +(*+*)val "[\n(1, [1], true ,#Given, (Cor_TEST equality (x + 1 = 2) ,(e_e, [x + 1 = 2]), Position.T)), \n(2, [1], true ,#Given, (Cor_TEST solveFor x ,(v_v, [x]), Position.T)), \n(3, [1], true ,#Find, (Cor_TEST solutions L ,(v_v'i', [L]), Position.T))]"
9.227 + = I_Model.OLD_to_TEST pbl |> I_Model.to_string_TEST @{context};
9.228 +(*+*)val "[precond_rootpbl v_v]" = where_ |> UnparseC.terms @{context};
9.229 +\<close> ML \<open>
9.230 +"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
9.231 + (ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST pbl));
9.232 +\<close> ML \<open>
9.233 + val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
9.234 +\<close> ML \<open>
9.235 + val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
9.236 +\<close> ML \<open>
9.237 +(*+*)val [] = env_subst
9.238 +(*+*)val [(false, Const ("Test.precond_rootpbl", _) $ Free ("v_v", _))] = pres_subst
9.239 +\<close> ML \<open>
9.240 + val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
9.241 +\<close> ML \<open>
9.242 +(*+*)val "[\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\", \"\n(v_v'i', L)\"]"
9.243 + = env_model |> Subst.to_string @{context}
9.244 +(*+*)val [(true, Const ("Test.precond_rootpbl", _) $ Free ("x", _))] = pres_subst_other
9.245 +\<close> ML \<open>
9.246 + val full_subst = if env_eval = [] then pres_subst_other
9.247 + else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
9.248 +\<close> ML \<open>
9.249 +(*+*)val [] = env_eval
9.250 +(*+*)val [(true, Const ("Test.precond_rootpbl", _) $ Free ("x", _))] = full_subst
9.251 +\<close> ML \<open>
9.252 + val evals = map (eval ctxt where_rls) full_subst
9.253 +\<close> ML \<open>
9.254 +(*+*)val [(true, Const ("Test.precond_rootpbl", _) $ Free ("x", _))] = evals
9.255 +\<close> ML \<open>
9.256 +val return_check_OLD = (foldl and_ (true, map fst evals), pres_subst_other)
9.257 +\<close> ML \<open>
9.258 +(*+*)val (true, [(true, Const ("Test.precond_rootpbl", _) $ Free ("x", _))]) = return_check_OLD
9.259 +\<close> ML \<open>
9.260 +\<close> ML \<open>
9.261 +\<close> ML \<open> (*|------------ contine do_next_Model_Problem -----------------------------------------*)
9.262 +(*|------------------- contine do_next_Model_Problem -----------------------------------------*)
9.263 +(*\------------------- step into do_next_Model_Problem -------------------------------------//*)
9.264 +\<close> ML \<open> (*\------------ step into do_next_Model_Problem -------------------------------------//*)
9.265 +val (_, ([(tac as Specify_Theory "Test", _, _)], _, (pt, p))) = return_do_next_Model_Problem;
9.266 +\<close> ML \<open>
9.267 +(*/################################### outcomment @{} ########################################*)
9.268 +(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Problem ["sqroot-test", "univariate", "equation", "test"] = tac
9.269 +
9.270 +(*[], Met*)val return_Step_do_next_Specify_Problem = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
9.271 +(*/------------------- step into Step.do_next_Specify_Problem ------------------------------\\*)
9.272 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
9.273 + (p, ((pt, e_pos'), []));
9.274 + (*if*) Pos.on_calc_end ip (*else*);
9.275 + val (_, probl_id, _) = Calc.references (pt, p);
9.276 +val _ =
9.277 + (*case*) tacis (*of*);
9.278 + (*if*) probl_id = Problem.id_empty (*else*);
9.279 +
9.280 +\<close> ML \<open>
9.281 + Step.switch_specify_solve p_ (pt, ip);
9.282 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
9.283 + (*if*) Pos.on_specification ([], state_pos) (*then*);
9.284 +
9.285 + Step.specify_do_next (pt, input_pos);
9.286 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
9.287 + val (_, (p_', tac)) = Specify.find_next_step ptp
9.288 + val ist_ctxt = Ctree.get_loc pt (p, p_)
9.289 +val _ =
9.290 + (*case*) tac (*of*);
9.291 +
9.292 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
9.293 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos)) =
9.294 + (tac, (pt, (p, p_')));
9.295 +
9.296 +\<close> ML \<open>
9.297 + val (o_model, ctxt, i_model) =
9.298 +Specify_Step.complete_for id (pt, pos);
9.299 +"~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
9.300 + val {origin = (o_model, _, _), probl = i_prob, ctxt,
9.301 + ...} = Calc.specify_data (ctree, pos);
9.302 + val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
9.303 + val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
9.304 + val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
9.305 +
9.306 + val (_, (i_model, _)) =
9.307 + M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
9.308 +"~~~~~ fun match_itms_oris , args:"; val (ctxt, pbl, (pbt, where_, where_rls), oris) =
9.309 + (ctxt, i_prob, (m_patt, where_, where_rls), o_model');
9.310 + (*0*)val mv = Pre_Conds.max_variant pbl;
9.311 +
9.312 + fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;
9.313 + fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
9.314 + SOME _ => false | NONE => true;
9.315 + (*1*)val mis = (filter (notmem pbl)) pbt;
9.316 + fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
9.317 + fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
9.318 + (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
9.319 + val news = (flat o (map (oris2itms oris))) mis;
9.320 + (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
9.321 + val newitms = filter mem_vat news;
9.322 + (*4*)val itms' = pbl @ newitms;
9.323 +
9.324 +\<close> ML \<open>
9.325 + val (pb, where_') =
9.326 + Pre_Conds.check_OLD ctxt where_rls where_ (m_patt, I_Model.OLD_to_TEST itms');
9.327 +\<close> ML \<open>
9.328 +"~~~~~ fun check_OLD , args:"; val (ctxt, where_rls, pres, (model_patt, i_model)) =
9.329 + (ctxt, where_rls, where_, (m_patt, I_Model.OLD_to_TEST itms'));
9.330 + val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
9.331 + val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
9.332 + val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
9.333 + val full_subst = if env_eval = [] then pres_subst_other
9.334 + else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
9.335 +
9.336 +\<close> ML \<open>
9.337 +(*+*)val "Test" = ctxt |> Proof_Context.theory_of |> ThyC.id_of
9.338 +(*+*)val Rule_Set.Repeat {id = "prls_met_test_squ_sub", ...} = where_rls
9.339 +(*+*)val [(true, tTEST as Const ("Test.precond_rootmet", _) $ Free ("x", xxx))] = pres_subst_other
9.340 +
9.341 +\<close> ML \<open>
9.342 +\<close> ML \<open>
9.343 +(*+*)val ctxt = Config.put rewrite_trace true ctxt;
9.344 + val evals = map (
9.345 + Pre_Conds.eval ctxt where_rls) full_subst;
9.346 +(*
9.347 +@## rls: prls_met_test_squ_sub on: precond_rootmet x
9.348 +@### try calc: "Test.precond_rootmet"
9.349 +@#### eval asms: "(precond_rootmet x) = True"
9.350 +@### calc. to: True
9.351 +@### try calc: "Test.precond_rootmet"
9.352 +@### try calc: "Test.precond_rootmet"
9.353 +*)
9.354 +(*+*)val ctxt = Config.put rewrite_trace false ctxt;
9.355 +
9.356 +\<close> ML \<open>
9.357 +"~~~~~ fun eval_precond_rootmet , args:"; val ((thmid:string), _, (t as (Const (\<^const_name>\<open>Test.precond_rootmet\<close>, _) $ arg)), ctxt) =
9.358 + ("aaa", "bbb", tTEST, ctxt);
9.359 + SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg) "",
9.360 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
9.361 +;
9.362 + (TermC.mk_thmid thmid (UnparseC.term ctxt arg)) "";
9.363 +\<close> ML \<open>
9.364 +"~~~~~ fun mk_thmid , args:"; val (thmid, n1, n2) = (thmid, (UnparseC.term ctxt arg), "");
9.365 + thmid ^ (cut_longid n1) ^ "_" ^ (cut_longid n2);
9.366 +
9.367 +\<close> ML \<open>
9.368 + (cut_longid n2);
9.369 +"~~~~~ fun cut_longid , args:"; val (dn) = (n2);
9.370 +(*\------------------- step into Step.do_next_Specify_Problem ------------------------------//*)
9.371 +val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Specify_Problem; val Specify_Method ["Test", "squ-equ-test-subpbl1"] = tac;
9.372 +
9.373 +\<close> text \<open> (*ERROR 2 formal args: [e_e, v_v], 0 actual args: []*)
9.374 +(*[1], Frm*)val return_Step_do_next_Specify_Method = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
9.375 +\<close> ML \<open>(*/------------- step into do_next_Specify_Method ------------------------------------\\*)
9.376 +(*/------------------- step into do_next_Specify_Method ------------------------------------\\*)
9.377 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
9.378 + (p, ((pt, e_pos'), []));
9.379 + (*if*) Pos.on_calc_end ip (*else*);
9.380 + val (_, probl_id, _) = Calc.references (pt, p);
9.381 +val _ =
9.382 + (*case*) tacis (*of*);
9.383 + (*if*) probl_id = Problem.id_empty (*else*);
9.384 +
9.385 +\<close> text \<open> (*ERROR 2 formal args: [e_e, v_v], 0 actual args: []*)
9.386 + switch_specify_solve p_ (pt, ip);
9.387 +\<close> ML \<open>
9.388 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
9.389 + (*if*) Pos.on_specification ([], state_pos) (*then*);
9.390 +
9.391 +\<close> text \<open> (*ERROR 2 formal args: [e_e, v_v], 0 actual args: []*)
9.392 + specify_do_next (pt, input_pos);
9.393 +\<close> ML \<open>
9.394 +"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
9.395 + val (_, (p_', tac)) = Specify.find_next_step ptp
9.396 + val ist_ctxt = Ctree.get_loc pt (p, p_)
9.397 +(*+*)val Tactic.Apply_Method mI =
9.398 + (*case*) tac (*of*);
9.399 +
9.400 +\<close> text \<open> (*ERROR 2 formal args: [e_e, v_v], 0 actual args: []*)
9.401 + LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
9.402 + ist_ctxt (pt, (p, p_'));
9.403 +\<close> ML \<open>
9.404 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
9.405 + ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)),
9.406 + ist_ctxt, (pt, (p, p_')));
9.407 + val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
9.408 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
9.409 + | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
9.410 + val {model, ...} = MethodC.from_store ctxt mI;
9.411 + val itms = if itms <> [] then itms else I_Model.complete oris probl [] model
9.412 +
9.413 +\<close> text \<open> (*ERROR 2 formal args: [e_e, v_v], 0 actual args: []*)
9.414 + val (is, env, ctxt, prog) = case
9.415 + LItool.init_pstate ctxt (I_Model.OLD_to_TEST itms) mI of
9.416 + (is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
9.417 +\<close> text \<open> (*ERROR (...) has not been declared*)
9.418 +val return_init_pstate = (is, env, ctxt, prog)
9.419 +\<close> ML \<open>
9.420 +(*#------------------- un-hide local of init_pstate -----------------------------------------\*)
9.421 +fun msg_miss ctxt sc metID caller f formals actuals =
9.422 + "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
9.423 + "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"" ^ caller ^ "\":\n" ^
9.424 + "formal arg \"" ^ UnparseC.term ctxt f ^ "\" doesn't match any actual arg.\n" ^
9.425 + "with:\n" ^
9.426 + (string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms ctxt formals ^ "\n" ^
9.427 + (string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms ctxt actuals
9.428 +fun msg_miss_type ctxt sc metID f formals actuals =
9.429 + "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
9.430 + "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
9.431 + "formal arg \"" ^ UnparseC.term ctxt f ^ "\" of type \"" ^ UnparseC.typ ctxt (type_of f) ^
9.432 + "\" doesn't mach any actual arg.\nwith:\n" ^
9.433 + (string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms ctxt formals ^ "\n" ^
9.434 + (string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms ctxt actuals ^ "\n" ^
9.435 + " with types: " ^ (strs2str o (map ((UnparseC.typ ctxt) o type_of))) actuals
9.436 +fun msg_ambiguous ctxt sc metID f aas formals actuals =
9.437 + "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
9.438 + "and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
9.439 + "formal arg. \"" ^ UnparseC.term ctxt f ^ "\" type-matches with several..." ^
9.440 + "actual args. \"" ^ UnparseC.terms ctxt aas ^ "\"\n" ^
9.441 + "selected \"" ^ UnparseC.term ctxt (hd aas) ^ "\"\n" ^
9.442 + "with\n" ^
9.443 + "formals: " ^ UnparseC.terms ctxt formals ^ "\n" ^
9.444 + "actuals: " ^ UnparseC.terms ctxt actuals
9.445 +fun trace_init ctxt metID =
9.446 + if Config.get ctxt LI_trace
9.447 + then tracing("@@@ program \"" ^ strs2str metID ^ "\"")
9.448 + else ();
9.449 +
9.450 +fun assoc_by_type ctxt f aa prog met_id formals actuals =
9.451 + case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
9.452 + [] => raise ERROR (msg_miss_type ctxt prog met_id f formals actuals)
9.453 + | [a] => (f, a)
9.454 + | aas as (a :: _) => (writeln (msg_ambiguous ctxt prog met_id f aas formals actuals); (f, a));
9.455 +(*
9.456 + fun assoc_formals_actuals: at "PIDE turn 11" ONLY syntax revised, NOT semantics
9.457 + Env.T -> (* [] for building return Env.T *)
9.458 + term list -> (* changed during building return Env.T *)
9.459 + term list -> (* changed during building return Env.T *)
9.460 + Proof.context -> (* *)
9.461 + term -> (* program code *)
9.462 + MethodC.id -> (* for error msg *)
9.463 + term list -> (* original value, unchanged *)
9.464 + term list -> (* original value, unchanged *)
9.465 + Env.T (* return Env.T *)
9.466 +*)
9.467 +\<close> ML \<open>
9.468 +fun relate_args _ (f::_) [] ctxt prog met_id formals actuals =
9.469 + raise ERROR (msg_miss ctxt prog met_id "relate_args" f formals actuals)
9.470 + | relate_args env [] _ _ _ _ _ _ = env (*may drop Find?*)
9.471 + | relate_args env (f::ff) (aas as (a::aa)) ctxt prog met_id formals actuals =
9.472 + if type_of f = type_of a
9.473 + then relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals
9.474 + else
9.475 + let val (f, a) = assoc_by_type ctxt f aas prog met_id formals actuals
9.476 + in relate_args (env @ [(f, a)]) ff (remove op = a aas) ctxt prog met_id formals actuals end
9.477 +;
9.478 +(*+*)relate_args: Env.T -> term list -> term list -> Proof.context -> term -> MethodC.id ->
9.479 + term list -> term list -> Env.T;
9.480 +(*#------------------- un-hide local of init_pstate -----------------------------------------/*)
9.481 +
9.482 +\<close> ML \<open>(*//------------ step into init_pstate -----------------------------------------------\\*)
9.483 +(*//------------------ step into init_pstate -----------------------------------------------\\*)
9.484 +(*//------------------ step into init_pstate -----------------------------------------------\\*)
9.485 +val (_, ctxt, i_model, met_id) = (prog_rls, ctxt, itms, mI);
9.486 +"~~~~~ fun init_pstate , args:"; val (ctxt, i_model, met_id) =
9.487 + (ctxt, I_Model.OLD_to_TEST i_model, met_id);
9.488 + val (model_patt, program, prog, prog_rls, where_, where_rls) =
9.489 + case MethodC.from_store ctxt met_id of
9.490 + {model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...} =>
9.491 + (model_patt, program, prog, prog_rls, where_, where_rls)
9.492 + | _ => raise ERROR ("init_pstate with " ^ MethodC.id_to_string met_id)
9.493 +
9.494 +\<close> ML \<open>
9.495 + val return_of_max_variant =
9.496 + I_Model.of_max_variant model_patt i_model;
9.497 +\<close> ML \<open>(*///----------- step into of_max_variant --------------------------------------------\\*)
9.498 +(*///----------------- step into of_max_variant --------------------------------------------\\*)
9.499 +"~~~~~ fun of_max_variant , args:"; val (model_patt, i_model) = (model_patt, i_model);
9.500 +
9.501 +(*+*)i_model: I_Model.T_TEST;
9.502 +
9.503 + val all_variants =
9.504 + map (fn (_, variants, _, _, _) => variants) i_model
9.505 + |> flat
9.506 + |> distinct op =
9.507 + val variants_separated = map (filter_variants' i_model) all_variants
9.508 + val sums_corr = map (cnt_corrects) variants_separated
9.509 +(*+*)val [3] = sums_corr;
9.510 +
9.511 + val sum_variant_s = arrange_args1 sums_corr (1, all_variants)
9.512 +(*+*)val [(3, 1)] = sum_variant_s;
9.513 +
9.514 + val (_, max_variant) = hd (*..crude decision, up to improvement *)
9.515 + (sort (fn ((i, _), (j, _)) => int_ord (i, j)) sum_variant_s)
9.516 +(*+*)val 1 = max_variant;
9.517 +
9.518 + val i_model_max =
9.519 + filter (fn (_, variants, _ , _ ,_) => member (op =) variants max_variant) i_model
9.520 +(*+*)val 3 = length i_model_max;
9.521 +
9.522 + val equal_descr_pairs =
9.523 + map (get_equal_descr i_model) model_patt
9.524 + |> flat
9.525 +(*+*)val 3 = length equal_descr_pairs; (*only 1 variant in this test*)
9.526 +
9.527 +\<close> ML \<open>
9.528 + val env_model = make_env_model equal_descr_pairs
9.529 + val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
9.530 +\<close> ML \<open>
9.531 +(*+*)val ([], []) = (env_subst, env_eval)
9.532 +\<close> ML \<open>
9.533 +(*+*)(equal_descr_pairs |> descr_pairs_to_string @{context}) = "[" ^
9.534 + "((#Given, (equality, e_e)), " ^
9.535 + "(1, [1], true ,#Given, (Cor_TEST equality (x + 1 = 2) ,(e_e, [x + 1 = 2]), Position.T))), " ^
9.536 + "((#Given, (solveFor, v_v)), " ^
9.537 + "(2, [1], true ,#Given, (Cor_TEST solveFor x ,(v_v, [x]), Position.T))), " ^
9.538 + "((#Find, (solutions, v_v'i')), " ^
9.539 + "(3, [1], true ,#Find, (Cor_TEST solutions L ,(v_v'i', [L]), Position.T)))]";
9.540 +(*------------------------------------------------^^^^^^^^^^^^^--- NOT FOUND*)
9.541 +\<close> ML \<open>(*|||----------- contine of_max_variant ------------------------------------------------*)
9.542 +(*|||----------------- contine of_max_variant ------------------------------------------------*)
9.543 + val subst_eval_list = make_envs_preconds equal_givens
9.544 + val (env_subst, env_eval) = split_list subst_eval_list
9.545 +
9.546 +\<close> ML \<open>
9.547 +val return_of_max_variant_step = (i_model_max, env_model, (env_subst, env_eval));
9.548 +(*+*)if return_of_max_variant_step = return_of_max_variant then () else error "<>";
9.549 +\<close> ML \<open>(*\\\----------- step into of_max_variant --------------------------------------------\\*)
9.550 +(*\\\----------------- step into of_max_variant --------------------------------------------\\*)
9.551 +val (i_model_max, env_model, (env_subst as [], env_eval as [])) = return_of_max_variant
9.552 +
9.553 +\<close> ML \<open>(*||------------ continue init_pstate ------------------------------------------------\\*)
9.554 +(*||------------------ continue init_pstate ------------------------------------------------\\*)
9.555 + val actuals = map snd env_model
9.556 +\<close> ML \<open>
9.557 +(*+*)val "[x + 1 = 2, x, L]" = actuals |> UnparseC.terms @{context}
9.558 +(*+*)val [_, Free ("x", _), Free ("L", typ)] = actuals
9.559 +\<close> ML \<open>
9.560 +(*+*)val Type ("List.list", [Type ("HOL.bool", [])]) = typ
9.561 +\<close> ML \<open>
9.562 + val formals = Program.formal_args prog
9.563 +(*+*)val "[e_e, v_v]" = (formals |> UnparseC.terms @{context})
9.564 +
9.565 +(*+*)val "minisubpbl e_e v_v =\n(let e_ea =\n (Try (Rewrite_Set ''norm_equation'') #>\n Try (Rewrite_Set ''Test_simplify''))\n e_e;\n L_La =\n SubProblem\n (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''],\n [''Test'', ''solve_linear''])\n [BOOL e_e, REAL v_v]\n in Check_elementwise L_L {v_v. Assumptions})" =
9.566 + (prog |> UnparseC.term @{context})
9.567 +
9.568 + val preconds =
9.569 + Pre_Conds.check_from_store ctxt where_rls where_ env_subst env_eval
9.570 +\<close> ML \<open>
9.571 +val return_check_from_store (*? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ?*) = preconds
9.572 +\<close> ML \<open>(*///----------- step into check_from_store ------------------------------------------//*)
9.573 +(*///----------------- step into check_from_store ------------------------------------------//*)
9.574 +"~~~~~ fun check_from_store , args:"; val (ctxt, where_rls, preconds, env_subst, env_eval) =
9.575 + (ctxt, where_rls, where_, env_subst, env_eval);
9.576 +
9.577 +(*+*)val "[precond_rootmet v_v]" = (where_ |> UnparseC.terms @{context})
9.578 +\<close> ML \<open>
9.579 +(*+*)val "[\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\", \"\n(v_v'i', L)\"]" = env_subst |> Subst.to_string @{context}
9.580 +\<close> ML \<open>
9.581 +(*+*)val [] = env_eval (*special case, Maximum-expl more general*)
9.582 +
9.583 + val pres_subst = map (TermC.subst_atomic_all env_subst) pres;
9.584 +(*+*)val [(true, Const ("Test.precond_rootmet", _) $ Free ("x", _))] = pres_subst
9.585 +
9.586 + val full_subst = map (fn (bool, t) => (bool, subst_atomic env_eval t)) pres_subst
9.587 +(*+*)val [(true, Const ("Test.precond_rootmet", _) $ Free ("x", _))] = full_subst
9.588 +
9.589 + val evals = map (eval ctxt where_rls) full_subst
9.590 +(*+*)val [(true, Const ("Test.precond_rootmet", _) $ Free ("x", _))] = evals
9.591 +
9.592 +val return_check_from_store_step = (foldl and_ (true, map fst evals), pres_subst)
9.593 +(*+*)val (true, [(true, Const ("Test.precond_rootmet", _) $ Free ("x", _))]) =
9.594 + return_check_from_store_step;
9.595 +(*+*)if return_check_from_store_step = return_check_from_store then () else error "<>";
9.596 +\<close> ML \<open>(*\\\----------- step into check_from_store ------------------------------------------//*)
9.597 +(*\\\----------------- step into check_from_store ------------------------------------------//*)
9.598 + val preconds = return_check_from_store
9.599 +
9.600 +\<close> ML \<open>(*||------------ continue init_pstate ------------------------------------------------\\*)
9.601 +(*||------------------ continue init_pstate ------------------------------------------------\\*)
9.602 + val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));
9.603 + val ist = Istate.e_pstate
9.604 + |> Istate.set_eval prog_rls
9.605 + |> Istate.set_env_true (relate_args [] formals actuals ctxt prog met_id formals actuals);
9.606 +(*+*) (relate_args [] formals actuals ctxt prog met_id formals actuals);
9.607 +(*+*)val "[\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\"]" =
9.608 + (relate_args [] formals actuals ctxt prog met_id formals actuals)
9.609 + |> Subst.to_string @{context}
9.610 +
9.611 +val return_init_pstate_steps = (* = return_init_pstate*)
9.612 + (Istate.Pstate ist, ctxt, program)
9.613 +\<close> ML \<open>(*\\------------ step into init_pstate -----------------------------------------------//*)
9.614 +(*\\------------------ step into init_pstate -----------------------------------------------//*)
9.615 +val (is, env, ctxt, prog) = return_init_pstate;
9.616 +
9.617 +\<close> ML \<open>(*|------------- continuing do_next_Specify_Method -------------------------------------*)
9.618 +(*|------------------- continuing do_next_Specify_Method -------------------------------------*)
9.619 +\<close> ML \<open>(*\------------- step into do_next_Specify_Method ------------------------------------//*)
9.620 +(*\------------------- step into do_next_Specify_Method ------------------------------------//*)
9.621 +\<close> ML \<open>
9.622 +val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Specify_Method; val Apply_Method ["Test", "squ-equ-test-subpbl1"] = tac;
9.623 +
9.624 +(*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Rewrite_Set "norm_equation" = tac
9.625 +
9.626 +(*[1], Res*)val return_Step_do_next_Rewrite_Set = Step.do_next p ((pt, e_pos'), []);
9.627 +\<close> ML \<open>(*/------------- step into do_next_Apply_Method --------------------------------------\\*)
9.628 +(*/------------------- step into do_next_Apply_Method --------------------------------------\\*)
9.629 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
9.630 + (p ,((pt, e_pos'), []));
9.631 +\<close> ML \<open>
9.632 + (*if*) Pos.on_calc_end ip (*else*);
9.633 + val (_, probl_id, _) = Calc.references (pt, p);
9.634 +val _ =
9.635 + (*case*) tacis (*of*);
9.636 + (*if*) probl_id = Problem.id_empty (*else*);
9.637 +
9.638 + Step.switch_specify_solve p_ (pt, ip);
9.639 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos))
9.640 + = (p_, (pt, ip));
9.641 + (*if*) Pos.on_specification ([], state_pos) (*else*);
9.642 +
9.643 + LI.do_next (pt, input_pos);
9.644 +"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
9.645 + (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
9.646 + val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
9.647 +
9.648 +val return_LI_find_next_step = (*case*)
9.649 + LI.find_next_step sc (pt, pos) ist ctxt (*of*);
9.650 +(*//------------------ step into LI.find_next_step -----------------------------------------\\*)
9.651 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Istate.Pstate ist), ctxt) =
9.652 + (sc, (pt, pos), ist, ctxt);
9.653 +(*.. this showed that we have ContextC.empty*)
9.654 +(*\\------------------ step into LI.find_next_step -----------------------------------------//*)
9.655 +val LI.Next_Step (ist, ctxt, tac) = return_LI_find_next_step;
9.656 +
9.657 + LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
9.658 +"~~~~~ fun by_tactic , args:"; val (tac_, ic, (pt, pos))
9.659 + = (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp);
9.660 + val pos = next_in_prog' pos
9.661 +
9.662 + val (pos', c, _, pt) =
9.663 +Solve_Step.add_general tac_ ic (pt, pos);
9.664 +"~~~~~ fun add_general , args:"; val (tac, ic, cs)
9.665 + = (tac_, ic, (pt, pos));
9.666 + (*if*) Tactic.for_specify' tac (*else*);
9.667 +
9.668 +Solve_Step.add tac ic cs;
9.669 +"~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))
9.670 + = (tac, ic, cs);
9.671 + val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
9.672 + (Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete
9.673 + val pt = Ctree.update_branch pt p Ctree.TransitiveB
9.674 +
9.675 +val return =
9.676 + ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term ctxt f'), pt)
9.677 +\<close> ML \<open>(*\------------- step into do_next_Apply_Method --------------------------------------//*)
9.678 +(*\------------------- step into do_next_Apply_Method --------------------------------------//*)
9.679 +val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Rewrite_Set
9.680 +
9.681 +(* final test ... ----------------------------------------------------------------------------*)
9.682 +(*+*)val ([2], Res) = p;
9.683 +Test_Tool.show_pt_tac pt; (*[
9.684 +([], Frm), solve (x + 1 = 2, x)
9.685 +. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
9.686 +([1], Frm), x + 1 = 2
9.687 +. . . . . . . . . . Rewrite_Set "norm_equation",
9.688 +([1], Res), x + 1 + - 1 * 2 = 0
9.689 +. . . . . . . . . . Rewrite_Set "Test_simplify",
9.690 +([2], Res), - 1 + x = 0
9.691 +. . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"]] ..INCORRECT
9.692 +*)
9.693 +(*/################################### outcomment @{} ########################################*)
9.694 +\<close> ML \<open>
9.695 +\<close>
9.696 +
9.697 +
9.698 section \<open>===================================================================================\<close>
9.699 -section \<open>===================================================================================\<close>
9.700 +section \<open>===== ============================================================================\<close>
9.701 ML \<open>
9.702 \<close> ML \<open>
9.703 \<close> ML \<open>