walther@59781
|
1 |
(* Title: "Minisubpbl/200-start-method-NEXT_STEP.sml"
|
walther@59781
|
2 |
Author: Walther Neuper 1105
|
walther@59781
|
3 |
(c) copyright due to lincense terms.
|
walther@59781
|
4 |
*)
|
walther@59781
|
5 |
|
Walther@60710
|
6 |
open Ctree;
|
Walther@60596
|
7 |
open Pos;
|
Walther@60596
|
8 |
open TermC;
|
Walther@60710
|
9 |
open Istate;
|
Walther@60710
|
10 |
open Tactic;
|
Walther@60710
|
11 |
open I_Model;
|
Walther@60710
|
12 |
open Pre_Conds;
|
Walther@60710
|
13 |
open Rewrite;
|
Walther@60710
|
14 |
open Step;
|
Walther@60710
|
15 |
open LItool;
|
Walther@60710
|
16 |
open LI;
|
Walther@60596
|
17 |
|
walther@59781
|
18 |
"----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
|
walther@59781
|
19 |
"----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
|
walther@59781
|
20 |
"----------- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
|
Walther@60712
|
21 |
tracing "--- Minisubplb/200-start-method-NEXT_STEP.sml ---------------------------------------";
|
walther@59997
|
22 |
val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
|
walther@59781
|
23 |
val (dI',pI',mI') =
|
walther@59997
|
24 |
("Test", ["sqroot-test", "univariate", "equation", "test"],
|
walther@59997
|
25 |
["Test", "squ-equ-test-subpbl1"]);
|
Walther@60571
|
26 |
val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
|
Walther@60725
|
27 |
(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Model_Problem = tac
|
Walther@60725
|
28 |
(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Theory "Test" = tac
|
Walther@60725
|
29 |
(*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Specify_Problem ["sqroot-test", "univariate", "equation", "test"] = tac
|
Walther@60682
|
30 |
|
Walther@60682
|
31 |
(*[], Met*)val return_Step_do_next_Specify_Problem = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
|
Walther@60682
|
32 |
(*/------------------- step into Step.do_next_Specify_Problem ------------------------------\\*)
|
Walther@60682
|
33 |
"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
|
Walther@60682
|
34 |
(p, ((pt, e_pos'), []));
|
Walther@60682
|
35 |
(*if*) Pos.on_calc_end ip (*else*);
|
Walther@60682
|
36 |
val (_, probl_id, _) = Calc.references (pt, p);
|
Walther@60682
|
37 |
val _ =
|
Walther@60682
|
38 |
(*case*) tacis (*of*);
|
Walther@60682
|
39 |
(*if*) probl_id = Problem.id_empty (*else*);
|
Walther@60682
|
40 |
|
Walther@60682
|
41 |
Step.switch_specify_solve p_ (pt, ip);
|
Walther@60682
|
42 |
"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
|
Walther@60682
|
43 |
(*if*) Pos.on_specification ([], state_pos) (*then*);
|
Walther@60682
|
44 |
|
Walther@60682
|
45 |
Step.specify_do_next (pt, input_pos);
|
Walther@60682
|
46 |
"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
|
Walther@60682
|
47 |
val (_, (p_', tac)) = Specify.find_next_step ptp
|
Walther@60682
|
48 |
val ist_ctxt = Ctree.get_loc pt (p, p_)
|
Walther@60682
|
49 |
val _ =
|
Walther@60682
|
50 |
(*case*) tac (*of*);
|
Walther@60682
|
51 |
|
Walther@60682
|
52 |
Step_Specify.by_tactic_input tac (pt, (p, p_'));
|
Walther@60682
|
53 |
"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos)) =
|
Walther@60682
|
54 |
(tac, (pt, (p, p_')));
|
Walther@60682
|
55 |
|
Walther@60682
|
56 |
val (o_model, ctxt, i_model) =
|
Walther@60682
|
57 |
Specify_Step.complete_for id (pt, pos);
|
Walther@60682
|
58 |
"~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
|
Walther@60682
|
59 |
val {origin = (o_model, _, _), probl = i_prob, ctxt,
|
Walther@60682
|
60 |
...} = Calc.specify_data (ctree, pos);
|
Walther@60682
|
61 |
val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
|
Walther@60682
|
62 |
val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
|
Walther@60682
|
63 |
val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
|
Walther@60682
|
64 |
|
Walther@60682
|
65 |
val (_, (i_model, _)) =
|
Walther@60682
|
66 |
M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
|
Walther@60682
|
67 |
"~~~~~ fun match_itms_oris , args:"; val (ctxt, pbl, (pbt, where_, where_rls), oris) =
|
Walther@60682
|
68 |
(ctxt, i_prob, (m_patt, where_, where_rls), o_model');
|
Walther@60705
|
69 |
(*0*)val mv = Pre_Conds.max_variant pbl;
|
Walther@60682
|
70 |
|
Walther@60682
|
71 |
fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;
|
Walther@60682
|
72 |
fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
|
Walther@60682
|
73 |
SOME _ => false | NONE => true;
|
Walther@60682
|
74 |
(*1*)val mis = (filter (notmem pbl)) pbt;
|
Walther@60730
|
75 |
|
Walther@60682
|
76 |
fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
|
Walther@60682
|
77 |
fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
|
Walther@60682
|
78 |
(*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
|
Walther@60682
|
79 |
val news = (flat o (map (oris2itms oris))) mis;
|
Walther@60682
|
80 |
(*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
|
Walther@60682
|
81 |
val newitms = filter mem_vat news;
|
Walther@60682
|
82 |
(*4*)val itms' = pbl @ newitms;
|
Walther@60682
|
83 |
|
Walther@60741
|
84 |
val (pb, where_') = Pre_Conds.check ctxt where_rls where_
|
Walther@60730
|
85 |
(pbt, I_Model.OLD_to_TEST itms');
|
Walther@60741
|
86 |
"~~~~~ fun check , args:"; val (ctxt, where_rls, where_, (model_patt, i_model)) =
|
Walther@60730
|
87 |
(ctxt, where_rls, where_, (pbt, I_Model.OLD_to_TEST itms'));
|
Walther@60730
|
88 |
val (_, env_model, (env_subst, env_eval)) = of_max_variant model_patt i_model
|
Walther@60730
|
89 |
val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
|
Walther@60730
|
90 |
val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
|
Walther@60730
|
91 |
val full_subst = if env_eval = [] then pres_subst_other
|
Walther@60730
|
92 |
else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
|
Walther@60682
|
93 |
|
Walther@60730
|
94 |
(*+*)val "Test" = ctxt |> Proof_Context.theory_of |> ThyC.id_of
|
Walther@60682
|
95 |
(*+*)val Rule_Set.Repeat {id = "prls_met_test_squ_sub", ...} = where_rls
|
Walther@60730
|
96 |
(*+*)val [(true, tTEST as Const ("Test.precond_rootmet", _) $ Free ("x", xxx))] = full_subst
|
Walther@60682
|
97 |
|
Walther@60682
|
98 |
(*+*)val ctxt = Config.put rewrite_trace true ctxt;
|
Walther@60682
|
99 |
val evals = map (
|
Walther@60731
|
100 |
Pre_Conds.eval ctxt where_rls) full_subst;
|
Walther@60705
|
101 |
(* (*declare [[rewrite_trace = true]]*)
|
Walther@60682
|
102 |
@## rls: prls_met_test_squ_sub on: precond_rootmet x
|
Walther@60682
|
103 |
@### try calc: "Test.precond_rootmet"
|
Walther@60682
|
104 |
@#### eval asms: "(precond_rootmet x) = True"
|
Walther@60682
|
105 |
@### calc. to: True
|
Walther@60682
|
106 |
@### try calc: "Test.precond_rootmet"
|
Walther@60682
|
107 |
@### try calc: "Test.precond_rootmet"
|
Walther@60682
|
108 |
*)
|
Walther@60682
|
109 |
(*+*)val ctxt = Config.put rewrite_trace false ctxt;
|
Walther@60682
|
110 |
|
Walther@60682
|
111 |
"~~~~~ fun eval_precond_rootmet , args:"; val ((thmid:string), _, (t as (Const (\<^const_name>\<open>Test.precond_rootmet\<close>, _) $ arg)), ctxt) =
|
Walther@60682
|
112 |
("aaa", "bbb", tTEST, ctxt);
|
Walther@60682
|
113 |
SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg) "",
|
Walther@60682
|
114 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
|
Walther@60682
|
115 |
;
|
Walther@60682
|
116 |
(TermC.mk_thmid thmid (UnparseC.term ctxt arg)) "";
|
Walther@60682
|
117 |
"~~~~~ fun mk_thmid , args:"; val (thmid, n1, n2) = (thmid, (UnparseC.term ctxt arg), "");
|
Walther@60682
|
118 |
thmid ^ (cut_longid n1) ^ "_" ^ (cut_longid n2);
|
Walther@60682
|
119 |
|
Walther@60682
|
120 |
(cut_longid n2);
|
Walther@60682
|
121 |
"~~~~~ fun cut_longid , args:"; val (dn) = (n2);
|
Walther@60682
|
122 |
(*\------------------- step into Step.do_next_Specify_Problem ------------------------------//*)
|
Walther@60725
|
123 |
val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Specify_Problem; val Specify_Method ["Test", "squ-equ-test-subpbl1"] = tac;
|
Walther@60710
|
124 |
|
Walther@60710
|
125 |
(*[1], Frm*)val return_Step_do_next_Specify_Method = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
|
Walther@60710
|
126 |
(*/------------------- step into Specify_Method --------------------------------------------\\*)
|
Walther@60710
|
127 |
"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
|
Walther@60710
|
128 |
(p, ((pt, e_pos'), []));
|
Walther@60710
|
129 |
(*if*) Pos.on_calc_end ip (*else*);
|
Walther@60710
|
130 |
val (_, probl_id, _) = Calc.references (pt, p);
|
Walther@60710
|
131 |
val _ =
|
Walther@60710
|
132 |
(*case*) tacis (*of*);
|
Walther@60710
|
133 |
(*if*) probl_id = Problem.id_empty (*else*);
|
Walther@60710
|
134 |
|
Walther@60710
|
135 |
switch_specify_solve p_ (pt, ip);
|
Walther@60710
|
136 |
"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
|
Walther@60710
|
137 |
(*if*) Pos.on_specification ([], state_pos) (*then*);
|
Walther@60710
|
138 |
|
Walther@60710
|
139 |
specify_do_next (pt, input_pos);
|
Walther@60710
|
140 |
"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
|
Walther@60710
|
141 |
val (_, (p_', tac)) = Specify.find_next_step ptp
|
Walther@60710
|
142 |
val ist_ctxt = Ctree.get_loc pt (p, p_)
|
Walther@60710
|
143 |
(*+*)val Tactic.Apply_Method mI =
|
Walther@60710
|
144 |
(*case*) tac (*of*);
|
Walther@60710
|
145 |
|
Walther@60710
|
146 |
LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
|
Walther@60710
|
147 |
ist_ctxt (pt, (p, p_'));
|
Walther@60710
|
148 |
"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _))) =
|
Walther@60710
|
149 |
((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)),
|
Walther@60710
|
150 |
ist_ctxt, (pt, (p, p_')));
|
Walther@60754
|
151 |
val (itms, oris, probl, o_spec, spec) = case get_obj I pt p of
|
Walther@60754
|
152 |
PblObj {meth = itms, origin = (oris, o_spec, _), probl, spec, ...}
|
Walther@60754
|
153 |
=> (itms, oris, probl, o_spec, spec)
|
Walther@60754
|
154 |
| _ => raise ERROR ""
|
Walther@60754
|
155 |
val (_, pI', _) = References.select_input o_spec spec
|
Walther@60757
|
156 |
val (_, itms) = I_Model.s_make_complete ctxt oris
|
Walther@60757
|
157 |
(I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST itms) (pI', mI)
|
Walther@60710
|
158 |
|
Walther@60710
|
159 |
val (is, env, ctxt, prog) = case
|
Walther@60754
|
160 |
LItool.init_pstate ctxt itms mI of
|
Walther@60710
|
161 |
(is as Pstate {env, ...}, ctxt, program) => (is, env, ctxt, program)
|
Walther@60710
|
162 |
val return_init_pstate = (is, env, ctxt, prog)
|
Walther@60710
|
163 |
(*#------------------- un-hide local of init_pstate -----------------------------------------\*)
|
Walther@60710
|
164 |
fun msg_miss ctxt sc metID caller f formals actuals =
|
Walther@60710
|
165 |
"ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
|
Walther@60710
|
166 |
"and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"" ^ caller ^ "\":\n" ^
|
Walther@60710
|
167 |
"formal arg \"" ^ UnparseC.term ctxt f ^ "\" doesn't match any actual arg.\n" ^
|
Walther@60710
|
168 |
"with:\n" ^
|
Walther@60710
|
169 |
(string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms ctxt formals ^ "\n" ^
|
Walther@60710
|
170 |
(string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms ctxt actuals
|
Walther@60710
|
171 |
fun msg_miss_type ctxt sc metID f formals actuals =
|
Walther@60710
|
172 |
"ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
|
Walther@60710
|
173 |
"and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
|
Walther@60710
|
174 |
"formal arg \"" ^ UnparseC.term ctxt f ^ "\" of type \"" ^ UnparseC.typ ctxt (type_of f) ^
|
Walther@60710
|
175 |
"\" doesn't mach any actual arg.\nwith:\n" ^
|
Walther@60710
|
176 |
(string_of_int o length) formals ^ " formal args: " ^ UnparseC.terms ctxt formals ^ "\n" ^
|
Walther@60710
|
177 |
(string_of_int o length) actuals ^ " actual args: " ^ UnparseC.terms ctxt actuals ^ "\n" ^
|
Walther@60710
|
178 |
" with types: " ^ (strs2str o (map ((UnparseC.typ ctxt) o type_of))) actuals
|
Walther@60710
|
179 |
fun msg_ambiguous ctxt sc metID f aas formals actuals =
|
Walther@60710
|
180 |
"AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
|
Walther@60710
|
181 |
"and the actual args., ie. items of the guard of \"" ^ MethodC.id_to_string metID ^ "\" by \"assoc_by_type\":\n" ^
|
Walther@60710
|
182 |
"formal arg. \"" ^ UnparseC.term ctxt f ^ "\" type-matches with several..." ^
|
Walther@60710
|
183 |
"actual args. \"" ^ UnparseC.terms ctxt aas ^ "\"\n" ^
|
Walther@60710
|
184 |
"selected \"" ^ UnparseC.term ctxt (hd aas) ^ "\"\n" ^
|
Walther@60710
|
185 |
"with\n" ^
|
Walther@60710
|
186 |
"formals: " ^ UnparseC.terms ctxt formals ^ "\n" ^
|
Walther@60710
|
187 |
"actuals: " ^ UnparseC.terms ctxt actuals
|
Walther@60710
|
188 |
fun trace_init ctxt metID =
|
Walther@60710
|
189 |
if Config.get ctxt LI_trace
|
Walther@60710
|
190 |
then tracing("@@@ program \"" ^ strs2str metID ^ "\"")
|
Walther@60710
|
191 |
else ();
|
Walther@60710
|
192 |
|
Walther@60710
|
193 |
fun assoc_by_type ctxt f aa prog met_id formals actuals =
|
Walther@60710
|
194 |
case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
|
Walther@60710
|
195 |
[] => raise ERROR (msg_miss_type ctxt prog met_id f formals actuals)
|
Walther@60710
|
196 |
| [a] => (f, a)
|
Walther@60710
|
197 |
| aas as (a :: _) => (writeln (msg_ambiguous ctxt prog met_id f aas formals actuals); (f, a));
|
Walther@60710
|
198 |
(*
|
Walther@60710
|
199 |
fun assoc_formals_actuals: at "PIDE turn 11" ONLY syntax revised, NOT semantics
|
Walther@60710
|
200 |
Env.T -> (* [] for building return Env.T *)
|
Walther@60710
|
201 |
term list -> (* changed during building return Env.T *)
|
Walther@60710
|
202 |
term list -> (* changed during building return Env.T *)
|
Walther@60710
|
203 |
Proof.context -> (* *)
|
Walther@60710
|
204 |
term -> (* program code *)
|
Walther@60710
|
205 |
MethodC.id -> (* for error msg *)
|
Walther@60710
|
206 |
term list -> (* original value, unchanged *)
|
Walther@60710
|
207 |
term list -> (* original value, unchanged *)
|
Walther@60710
|
208 |
Env.T (* return Env.T *)
|
Walther@60710
|
209 |
*)
|
Walther@60710
|
210 |
fun relate_args _ (f::_) [] ctxt prog met_id formals actuals =
|
Walther@60710
|
211 |
raise ERROR (msg_miss ctxt prog met_id "relate_args" f formals actuals)
|
Walther@60710
|
212 |
| relate_args env [] _ _ _ _ _ _ = env (*may drop Find?*)
|
Walther@60710
|
213 |
| relate_args env (f::ff) (aas as (a::aa)) ctxt prog met_id formals actuals =
|
Walther@60710
|
214 |
if type_of f = type_of a
|
Walther@60710
|
215 |
then relate_args (env @ [(f, a)]) ff aa ctxt prog met_id formals actuals
|
Walther@60710
|
216 |
else
|
Walther@60710
|
217 |
let val (f, a) = assoc_by_type ctxt f aas prog met_id formals actuals
|
Walther@60710
|
218 |
in relate_args (env @ [(f, a)]) ff (remove op = a aas) ctxt prog met_id formals actuals end
|
Walther@60710
|
219 |
;
|
Walther@60710
|
220 |
(*+*)relate_args: Env.T -> term list -> term list -> Proof.context -> term -> MethodC.id ->
|
Walther@60710
|
221 |
term list -> term list -> Env.T;
|
Walther@60710
|
222 |
(*#------------------- un-hide local of init_pstate -----------------------------------------/*)
|
Walther@60710
|
223 |
|
Walther@60710
|
224 |
(*//------------------ step into init_pstate NEW -------------------------------------------\\*)
|
Walther@60710
|
225 |
val (_, ctxt, i_model, met_id) = (prog_rls, ctxt, itms, mI);
|
Walther@60710
|
226 |
"~~~~~ fun init_pstate , args:"; val (ctxt, i_model, met_id) =
|
Walther@60754
|
227 |
(ctxt, i_model, met_id);
|
Walther@60710
|
228 |
val (model_patt, program, prog, prog_rls, where_, where_rls) =
|
Walther@60710
|
229 |
case MethodC.from_store ctxt met_id of
|
Walther@60710
|
230 |
{model = model_patt, program = program as Rule.Prog prog, prog_rls, where_, where_rls,...} =>
|
Walther@60710
|
231 |
(model_patt, program, prog, prog_rls, where_, where_rls)
|
Walther@60710
|
232 |
| _ => raise ERROR ("init_pstate with " ^ MethodC.id_to_string met_id)
|
Walther@60710
|
233 |
|
Walther@60729
|
234 |
val (_, env_model, (env_subst, env_eval)) = I_Model.of_max_variant model_patt i_model;
|
Walther@60729
|
235 |
val actuals = map snd env_model
|
Walther@60710
|
236 |
(*+*)val "[x + 1 = 2, x, L]" = actuals |> UnparseC.terms @{context}
|
Walther@60710
|
237 |
|
Walther@60729
|
238 |
val formals = Program.formal_args prog
|
Walther@60710
|
239 |
(*+*)val "[e_e, v_v]" = (formals |> UnparseC.terms @{context})
|
Walther@60710
|
240 |
|
Walther@60710
|
241 |
(*+*)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})" =
|
Walther@60710
|
242 |
(prog |> UnparseC.term @{context})
|
Walther@60710
|
243 |
|
Walther@60741
|
244 |
val preconds = Pre_Conds.check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval))
|
Walther@60710
|
245 |
|
Walther@60710
|
246 |
(*||------------------ continue init_pstate NEW --------------------------------------------\\*)
|
Walther@60710
|
247 |
val ctxt = ctxt |> ContextC.insert_assumptions (map snd (snd preconds));
|
Walther@60710
|
248 |
val ist = Istate.e_pstate
|
Walther@60710
|
249 |
|> Istate.set_eval prog_rls
|
Walther@60710
|
250 |
|> Istate.set_env_true (relate_args [] formals actuals ctxt prog met_id formals actuals);
|
Walther@60710
|
251 |
(*+*) (relate_args [] formals actuals ctxt prog met_id formals actuals);
|
Walther@60710
|
252 |
(*+*)val "[\"\n(e_e, x + 1 = 2)\", \"\n(v_v, x)\"]" =
|
Walther@60710
|
253 |
(relate_args [] formals actuals ctxt prog met_id formals actuals)
|
Walther@60710
|
254 |
|> Subst.to_string @{context}
|
Walther@60710
|
255 |
|
Walther@60710
|
256 |
val return_init_pstate_steps = (* = return_init_pstate*)
|
Walther@60710
|
257 |
(Istate.Pstate ist, ctxt, program)
|
Walther@60710
|
258 |
(*\\------------------ step into init_pstate NEW -------------------------------------------//*)
|
Walther@60710
|
259 |
val (is, env, ctxt, prog) = return_init_pstate;
|
Walther@60710
|
260 |
|
Walther@60710
|
261 |
(*|------------------- continuing Specify_Method ---------------------------------------------*)
|
Walther@60710
|
262 |
(*\------------------- step into Specify_Method --------------------------------------------//*)
|
Walther@60725
|
263 |
val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Specify_Method; val Apply_Method ["Test", "squ-equ-test-subpbl1"] = tac;
|
Walther@60682
|
264 |
|
Walther@60725
|
265 |
(*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []); val Rewrite_Set "norm_equation" = tac
|
walther@60324
|
266 |
|
Walther@60725
|
267 |
(*[1], Res*)val return_Step_do_next_Rewrite_Set = Step.do_next p ((pt, e_pos'), []);
|
Walther@60682
|
268 |
(*/------------------- step into Apply_Method ----------------------------------------------\\*)
|
Walther@60710
|
269 |
"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
|
Walther@60710
|
270 |
(p ,((pt, e_pos'), []));
|
Walther@60596
|
271 |
(*if*) Pos.on_calc_end ip (*else*);
|
Walther@60596
|
272 |
val (_, probl_id, _) = Calc.references (pt, p);
|
Walther@60596
|
273 |
val _ =
|
Walther@60596
|
274 |
(*case*) tacis (*of*);
|
Walther@60596
|
275 |
(*if*) probl_id = Problem.id_empty (*else*);
|
walther@60324
|
276 |
|
Walther@60596
|
277 |
Step.switch_specify_solve p_ (pt, ip);
|
Walther@60596
|
278 |
"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos))
|
Walther@60596
|
279 |
= (p_, (pt, ip));
|
Walther@60596
|
280 |
(*if*) Pos.on_specification ([], state_pos) (*else*);
|
walther@60324
|
281 |
|
Walther@60596
|
282 |
LI.do_next (pt, input_pos);
|
Walther@60596
|
283 |
"~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
|
Walther@60596
|
284 |
(*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
|
Walther@60596
|
285 |
val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
|
Walther@60682
|
286 |
|
Walther@60682
|
287 |
val return_LI_find_next_step = (*case*)
|
Walther@60682
|
288 |
LI.find_next_step sc (pt, pos) ist ctxt (*of*);
|
Walther@60682
|
289 |
(*//------------------ step into LI.find_next_step -----------------------------------------\\*)
|
Walther@60682
|
290 |
"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Istate.Pstate ist), ctxt) =
|
Walther@60682
|
291 |
(sc, (pt, pos), ist, ctxt);
|
Walther@60682
|
292 |
(*.. this showed that we have ContextC.empty*)
|
Walther@60710
|
293 |
(*\\------------------ step into LI.find_next_step -----------------------------------------//*)
|
Walther@60682
|
294 |
val LI.Next_Step (ist, ctxt, tac) = return_LI_find_next_step;
|
walther@60324
|
295 |
|
Walther@60596
|
296 |
LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
|
Walther@60596
|
297 |
"~~~~~ fun by_tactic , args:"; val (tac_, ic, (pt, pos))
|
Walther@60596
|
298 |
= (tac, (ist, Tactic.insert_assumptions tac ctxt), ptp);
|
Walther@60596
|
299 |
val pos = next_in_prog' pos
|
walther@60324
|
300 |
|
Walther@60596
|
301 |
val (pos', c, _, pt) =
|
Walther@60596
|
302 |
Solve_Step.add_general tac_ ic (pt, pos);
|
Walther@60596
|
303 |
"~~~~~ fun add_general , args:"; val (tac, ic, cs)
|
Walther@60596
|
304 |
= (tac_, ic, (pt, pos));
|
Walther@60596
|
305 |
(*if*) Tactic.for_specify' tac (*else*);
|
walther@60324
|
306 |
|
Walther@60596
|
307 |
Solve_Step.add tac ic cs;
|
Walther@60596
|
308 |
"~~~~~ fun add , args:"; val ((Tactic.Rewrite_Set' (_, _, rls', f, (f', asm))), (is, ctxt), (pt, (p, _)))
|
Walther@60596
|
309 |
= (tac, ic, cs);
|
Walther@60596
|
310 |
val (pt, c) = Ctree.cappend_atomic pt p (is, ctxt) f
|
Walther@60596
|
311 |
(Tactic.Rewrite_Set (Rule_Set.id rls')) (f', asm) Ctree.Complete
|
Walther@60596
|
312 |
val pt = Ctree.update_branch pt p Ctree.TransitiveB
|
walther@59851
|
313 |
|
Walther@60596
|
314 |
val return =
|
Walther@60675
|
315 |
((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term ctxt f'), pt)
|
Walther@60682
|
316 |
(*\------------------- step into Apply_Method ----------------------------------------------//*)
|
Walther@60710
|
317 |
val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Rewrite_Set
|
Walther@60529
|
318 |
|
Walther@60596
|
319 |
(* final test ... ----------------------------------------------------------------------------*)
|
Walther@60682
|
320 |
(*+*)val ([2], Res) = p;
|
Walther@60682
|
321 |
Test_Tool.show_pt_tac pt; (*[
|
Walther@60596
|
322 |
([], Frm), solve (x + 1 = 2, x)
|
Walther@60596
|
323 |
. . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
|
Walther@60596
|
324 |
([1], Frm), x + 1 = 2
|
Walther@60596
|
325 |
. . . . . . . . . . Rewrite_Set "norm_equation",
|
Walther@60596
|
326 |
([1], Res), x + 1 + - 1 * 2 = 0
|
Walther@60596
|
327 |
. . . . . . . . . . Rewrite_Set "Test_simplify",
|
Walther@60596
|
328 |
([2], Res), - 1 + x = 0
|
Walther@60596
|
329 |
. . . . . . . . . . Check_Postcond ["sqroot-test", "univariate", "equation", "test"]] ..INCORRECT
|
Walther@60730
|
330 |
*)
|