prep. cleanup LItool.resume_prog
1 (* Title: "Minisubpbl/200-start-method.sml"
2 Author: Walther Neuper 1105
3 (c) copyright due to lincense terms.
6 "----------- Minisubplb/200-start-method.sml -------------------------------------------------";
7 "----------- Minisubplb/200-start-method.sml -------------------------------------------------";
8 "----------- Minisubplb/200-start-method.sml -------------------------------------------------";
9 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
11 ("Test", ["sqroot-test","univariate","equation","test"],
12 ["Test","squ-equ-test-subpbl1"]);
13 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
14 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
15 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
16 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
17 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
18 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt = ("Specify_Problem",..*)
19 "~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
20 val (p'''',_,f'''',nxt'''',_,pt'''') = me nxt p [] pt; (* (@1) nxt'''' = ("Specify_Method",..*)
21 (*me nxt'''' p'''' [] pt''''; "ERROR in creating the environment..", SHOULD BE("Apply_Method",.*)
22 "~~~~~ we continue with (@1) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
23 val (p, f, nxt, pt) = (p'''',f'''',nxt'''',pt'''');
24 "~~~~~ fun me, args:"; val tac = nxt;
26 (*Step.by_tactic is here for testing by me; Step.do_next would suffice in me*)
27 case Step.by_tactic tac (pt,p) of
28 ("ok", (_, _, ptp)) => ptp | _ => error "CHANGED --- Minisubplb/200-start-method 1"
29 (* Step.do_next p ((pt, e_pos'),[]) ..ERROR = ("helpless",*)
30 "~~~~~ fun Step.do_next, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) =
31 (p, ((pt, e_pos'),[]));
32 val pIopt = get_pblID (pt,ip);
33 ip = ([],Res) (*= false*);
36 member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)) (*= true*);
37 (*nxt_specify_ (pt, ip) ..ERROR in creating the environment..*);
39 val (p, f, nxt, pt) = (p'''',f'''',nxt'''',pt'''');
40 "~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
41 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* (@2) nxt = ("Apply_Method",..*)
43 val (p'''',_,f'''',nxt'''',_,pt'''') = me nxt p [] pt;
45 "~~~~~ we continue with (@2) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
46 "~~~~~ fun me, args:"; val tac = nxt;
47 val ("ok", (_, _, (pt''''',p'''''))) = Step.by_tactic tac (pt,p);
48 "~~~~~ fun Step.by_tactic, args:"; val ptp as (pt, p) = (pt, p);
49 val Appl m = applicable_in p pt tac; (*m = Apply_Method'..*)
50 (*if*) Tactic.for_specify' m; (*false*)
51 "~~~~~ fun loc_solve_ , args:"; val (m, (pt, pos) ) = (m, ptp);
52 "~~~~~ fun Step_Solve.by_tactic , args:"; val (Apply_Method' (mI,_,_,_), pos as (p,_)) = (m, pos);
53 val PblObj {meth, ctxt, ...} = get_obj I pt p;
54 val thy' = get_obj g_domID pt p;
55 val thy = assoc_thy thy';
56 val {srls, pre, prls, ...} = get_met mI;
57 val pres = check_preconds thy prls pre meth |> map snd;
58 val ctxt = ctxt |> ContextC.insert_assumptions pres;
59 val (is'''' as Pstate {env = env'''',...}, _, sc'''') = init_pstate srls ctxt meth mI;
60 "~~~~~ fun init_pstate , args:"; val (srls, thy, itms, metID) = (srls, thy, meth, mI)
61 val actuals = itms2args thy metID itms
62 val scr as Prog sc = (#scr o get_met) metID
63 val formals = formal_args sc
64 (*expects same sequence of (actual) args in itms and (formal) args in met*)
65 fun msg_miss sc metID caller f formals actuals =
66 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
67 "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"" ^ caller ^ "\":\n" ^
68 "formal arg \"" ^ Rule.term2str f ^ "\" doesn't mach an actual arg.\n" ^
70 (string_of_int o length) formals ^ " formal args: " ^ Rule.terms2str formals ^ "\n" ^
71 (string_of_int o length) actuals ^ " actual args: " ^ Rule.terms2str actuals
72 fun msg_ambiguous sc metID f aas formals actuals =
73 "AMBIGUITY in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^
74 "and the actual args., ie. items of the guard of \"" ^ Celem.metID2str metID ^ "\" by \"assoc_by_type\":\n" ^
75 "formal arg. \"" ^ Rule.term2str f ^ "\" type-matches with several..." ^
76 "actual args. \"" ^ Rule.terms2str aas ^ "\"\n" ^
77 "selected \"" ^ Rule.term2str (hd aas) ^ "\"\n" ^
79 "formals: " ^ Rule.terms2str formals ^ "\n" ^
80 "actuals: " ^ Rule.terms2str actuals
81 fun assoc_by_type f aa =
82 case filter (curry (fn (f, a) => type_of f = type_of a) f) aa of
83 [] => error (msg_miss sc metID "assoc_by_type" f formals actuals)
85 | aas as (a :: _) => (writeln (msg_ambiguous sc metID f aas formals actuals); (f, a));
86 fun relate_args _ (f::_) [] = error (msg_miss sc metID "relate_args" f formals actuals)
87 | relate_args env [] _ = env (*may drop Find?*)
88 | relate_args env (f::ff) (aas as (a::aa)) =
89 if type_of f = type_of a
90 then relate_args (env @ [(f, a)]) ff aa
92 let val (f, a) = assoc_by_type f aas
93 in relate_args (env @ [(f, a)]) ff (remove op = a aas) end
94 val env = relate_args [] formals actuals;
95 (*val _ = trace_istate env;*)
96 val {pre, prls, ...} = Specify.get_met metID;
97 val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd;
98 val ctxt = ctxt |> ContextC.insert_assumptions pres;
100 "~~~~~ continue Step_Solve.by_tactic";
101 val ini = init_form thy sc'''' env'''';
105 generate1 (Apply_Method' (mI, SOME t, is'''', ctxt))
106 (is'''', ctxt) (pt, (lev_on p, Frm))(*implicit Take*);
107 ("ok",([(Apply_Method mI, Apply_Method' (mI, SOME t, is'''', ctxt),
108 ((lev_on p, Frm), (is'''', ctxt)))], c, (pt,pos)):calcstate');
110 val ctxt = get_ctxt pt pos;
111 val SOME known_x = parseNEW ctxt "x+z+z"; (*x has declare_constraints to real*)
112 val SOME unknown = parseNEW ctxt "a+b+c";
113 if type_of known_x = Type ("Real.real",[]) then ()
114 else error "x+1=2 after start root-pbl wrong type-inference for known_x";
115 if type_of unknown = TFree ("'a", ["Groups.plus"]) then ()
116 else error "x+1=2 after start root-pbl wrong type-inference for unknown";
118 "~~~~~ continue me (@3) after Step.by_tactic";
119 val (pt, p) = (pt''''',p''''');
120 "~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~";
121 "~~~~~ fun Step.do_next, args:"; val ((ip as (_, p_)), (ptp as (pt,p), tacis)) = (p, ((pt, Pos.e_pos'),[]));
122 val pIopt = get_pblID (pt,ip);
123 ip = ([], Pos.Res) (* = false*);
124 case tacis of [] => ();
125 case pIopt of SONE => ();
126 member op = [Pos.Pbl, Pos.Met] p_ andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) (* = false*);
127 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt,ip);
128 Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (* = false*);
129 val thy' = get_obj g_domID pt (par_pblobj pt p);
130 val (is, sc) = LItool.resume_prog thy' (p,p_) pt;
131 "~~~~~ fun find_next_step , args:"; val ((ptp as(pt, (p, _))), (Rule.Prog prog), (Istate.Pstate ist, ctxt))
132 = ((pt, pos), sc, is);
133 (*case*) scan_to_tactic (prog, (ptp, ctxt)) (Istate.Pstate ist) (*of*);
134 "~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Istate.Pstate (ist as {path, ...})))
135 = ((prog, (ptp, ctxt)), (Istate.Pstate ist));
136 (*if*) path = [] (*then*);
137 scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
138 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const ("HOL.Let"(*1*), _) $ e $ (Abs (i, T, b)))) =
139 (cc, (trans_scan_dn ist), (Program.body_of prog));
140 (*case*) scan_dn cc (ist |> path_down [L, R]) e (*of*);
141 "~~~~~ fun scan_dn , args:"; val (cc, ist, (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a))
142 = (cc, (ist |> path_down [L, R]), e);
143 (*case*) scan_dn cc (ist |> path_down_form ([L, L, R], a)) e1 (*of*);
144 "~~~~~ fun scan_dn , args:"; val (cc, (ist as {act_arg, ...}), (Const ("Tactical.Try"(*2*), _) $ e))
145 = (cc, (ist |> path_down_form ([L, L, R], a)), e1);
146 (*case*) scan_dn cc (ist |> path_down [R]) e (*of*);
147 "~~~~~ fun scan_dn , args:"; val (((pt, p), ctxt), (ist as {eval, ...}), t) =
148 (cc, (ist |> path_down [R]), e);
149 val (Program.Tac stac, a') =
150 (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
151 val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) stac;
153 "~~~~~ fun tac_from_prog , args:"; val (_, _, (Const ("Prog_Tac.Rewrite'_Set",_) $ rls $ _)) =
154 (pt, (Proof_Context.theory_of ctxt), stac);
156 (*+*)case LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) stac of (Rewrite_Set "norm_equation") => ()
157 (*+*)| _ => error "tac_from_prog changed"
159 "~~~~~ continue last scan_dn";
160 val Applicable.Appl m' = Applicable.applicable_in p pt m;
161 "~~~~~ fun result, args:"; val (m) = (m');
162 "~~~~~ fun rep_tac_, args:"; val (Tactic.Rewrite_Set' (thy', put, rls, f, (f', _))) = (m);
164 val lhs = Const ("Prog_Tac.Rewrite'_Set", [HOLogic.stringT, fT] ---> fT)
165 $ HOLogic.mk_string (Rule.id_rls rls) $ f;
166 (* ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ here was Free (Rule.id_rls rls, idT) *)
168 val (p,_,f,nxt,_,pt) = me nxt p'''' [] pt''''; (*nxt = ("Rewrite_Set"*)
169 case nxt of (Rewrite_Set _) => ()
170 | _ => error "minisubpbl: Method not started in root-problem";