1 (* Title: solve an example by interpreting a method's script
2 Author: Walther Neuper 1999
3 (c) copyright due to lincense terms.
6 signature SOLVE_PHASE =
8 datatype auto = CompleteCalc | CompleteCalcHead | CompleteModel | CompleteSubpbl
9 | CompleteToSubpbl | Step of int
10 val autoord : auto -> int
12 val mk_tac'_ : Tactic.input -> string * Tactic.input
13 val specsteps : string list
15 val all_solve : auto -> Ctree.pos' list -> Ctree.state ->
16 string * Ctree.pos' list * (Ctree.ctree * (int list * Ctree.pos_))
18 auto -> Ctree.pos' list -> Ctree.state -> string * Ctree.pos' list * Ctree.state
19 val solve : string * Tactic.T -> Ctree.state -> string * Chead.calcstate'
21 val inform : Chead.calcstate' -> string -> string * Chead.calcstate'
23 val detailrls : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
24 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
25 val get_form : tac'_ -> Ctree.pos' -> Ctree.ctree -> Generate.mout
26 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
28 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
30 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
35 structure Solve(**): SOLVE_PHASE(**) =
41 type tac'_ = mstID * Tactic.input; (*DG <-> ME*)
43 fun mk_tac'_ m = case m of (* scr not cleaned -- will disappear eventually *)
44 Tactic.Init_Proof (ppc, spec) => ("Init_Proof", Tactic.Init_Proof (ppc, spec ))
45 | Tactic.Model_Problem => ("Model_Problem", Tactic.Model_Problem)
46 | Tactic.Refine_Tacitly pblID => ("Refine_Tacitly", Tactic.Refine_Tacitly pblID)
47 | Tactic.Refine_Problem pblID => ("Refine_Problem", Tactic.Refine_Problem pblID)
48 | Tactic.Add_Given cterm' => ("Add_Given", Tactic.Add_Given cterm')
49 | Tactic.Del_Given cterm' => ("Del_Given", Tactic.Del_Given cterm')
50 | Tactic.Add_Find cterm' => ("Add_Find", Tactic.Add_Find cterm')
51 | Tactic.Del_Find cterm' => ("Del_Find", Tactic.Del_Find cterm')
52 | Tactic.Add_Relation cterm' => ("Add_Relation", Tactic.Add_Relation cterm')
53 | Tactic.Del_Relation cterm' => ("Del_Relation", Tactic.Del_Relation cterm')
55 | Tactic.Specify_Theory domID => ("Specify_Theory", Tactic.Specify_Theory domID)
56 | Tactic.Specify_Problem pblID => ("Specify_Problem", Tactic.Specify_Problem pblID)
57 | Tactic.Specify_Method metID => ("Specify_Method", Tactic.Specify_Method metID)
58 | Tactic.Apply_Method metID => ("Apply_Method", Tactic.Apply_Method metID)
59 | Tactic.Check_Postcond pblID => ("Check_Postcond", Tactic.Check_Postcond pblID)
60 | Tactic.Free_Solve => ("Free_Solve", Tactic.Free_Solve)
62 | Tactic.Rewrite_Inst (subs, thm') => ("Rewrite_Inst", Tactic.Rewrite_Inst (subs, thm'))
63 | Tactic.Rewrite thm' => ("Rewrite", Tactic.Rewrite thm')
64 | Tactic.Rewrite_Asm thm' => ("Rewrite_Asm", Tactic.Rewrite_Asm thm')
65 | Tactic.Rewrite_Set_Inst (subs, rls')
66 => ("Rewrite_Set_Inst", Tactic.Rewrite_Set_Inst (subs, rls'))
67 | Tactic.Rewrite_Set rls' => ("Rewrite_Set", Tactic.Rewrite_Set rls')
68 | Tactic.End_Ruleset => ("End_Ruleset", Tactic.End_Ruleset)
70 | Tactic.End_Detail => ("End_Detail", Tactic.End_Detail)
71 | Tactic.Detail_Set rls' => ("Detail_Set", Tactic.Detail_Set rls')
72 | Tactic.Detail_Set_Inst (s, rls') => ("Detail_Set_Inst", Tactic.Detail_Set_Inst (s, rls'))
74 | Tactic.Calculate op_ => ("Calculate", Tactic.Calculate op_)
75 | Tactic.Substitute sube => ("Substitute", Tactic.Substitute sube)
76 | Tactic.Apply_Assumption cts' => ("Apply_Assumption", Tactic.Apply_Assumption cts')
78 | Tactic.Take cterm' => ("Take", Tactic.Take cterm')
79 | Tactic.Take_Inst cterm' => ("Take_Inst", Tactic.Take_Inst cterm')
80 | Tactic.Subproblem (domID, pblID) => ("Subproblem", Tactic.Subproblem (domID, pblID))
82 | Tactic.Subproblem_Full(spec,cts')=> ("Subproblem_Full", Tactic.Subproblem_Full(spec,cts'))
84 | Tactic.End_Subproblem => ("End_Subproblem", Tactic.End_Subproblem)
85 | Tactic.CAScmd cterm' => ("CAScmd", Tactic.CAScmd cterm')
87 | Tactic.Split_And => ("Split_And", Tactic.Split_And)
88 | Tactic.Conclude_And => ("Conclude_And", Tactic.Conclude_And)
89 | Tactic.Split_Or => ("Split_Or", Tactic.Split_Or)
90 | Tactic.Conclude_Or => ("Conclude_Or", Tactic.Conclude_Or)
91 | Tactic.Begin_Trans => ("Begin_Trans", Tactic.Begin_Trans)
92 | Tactic.End_Trans => ("End_Trans", Tactic.End_Trans)
93 | Tactic.Begin_Sequ => ("Begin_Sequ", Tactic.Begin_Sequ)
94 | Tactic.End_Sequ => ("End_Sequ", Tactic.Begin_Sequ)
95 | Tactic.Split_Intersect => ("Split_Intersect", Tactic.Split_Intersect)
96 | Tactic.End_Intersect => ("End_Intersect", Tactic.End_Intersect)
97 | Tactic.Check_elementwise cterm' => ("Check_elementwise", Tactic.Check_elementwise cterm')
98 | Tactic.Or_to_List => ("Or_to_List", Tactic.Or_to_List)
99 | Tactic.Collect_Trues => ("Collect_Results", Tactic.Collect_Trues)
101 | Tactic.Empty_Tac => ("Empty_Tac", Tactic.Empty_Tac)
102 | Tactic.Tac string => ("Tac", Tactic.Tac string)
103 | Tactic.End_Proof' => ("End_Proof'", Tactic.End_Proof')
104 | _ => error "mk_tac'_: uncovered case";
106 type squ = ctree; (* TODO: safe etc. *)
108 val specsteps = ["Init_Proof", "Refine_Tacitly", "Refine_Problem", "Model_Problem",
109 "Add_Given", "Del_Given", "Add_Find", "Del_Find", "Add_Relation", "Del_Relation",
110 "Specify_Theory", "Specify_Problem", "Specify_Method"];
112 (*FIXME.WN050821 compare solve ... begin_end_prog:
113 WN190811: solve ("Apply_Method",.. used by root-pbl + by locate_input_tactic !!!
115 fun solve ("Apply_Method", m as Tactic.Apply_Method' (mI, _, _, ctxt)) (pt, (pos as (p, _))) =
117 val itms = case get_obj I pt p of
118 PblObj {meth=itms, ...} => itms
119 | _ => error "solve Apply_Method: uncovered case get_obj"
120 val thy' = get_obj g_domID pt p;
121 val thy = Celem.assoc_thy thy';
122 val srls = Lucin.get_simplifier (pt, pos)
123 val (is, env, ctxt, sc) = case Lucin.init_pstate srls ctxt itms mI of
124 (is as Istate.Pstate {env, ...}, ctxt, sc) => (is, env, ctxt, sc)
125 | _ => error "solve Apply_Method: uncovered case init_pstate"
126 val ini = Lucin.init_form thy sc env;
131 let val (pos,c,_, pt) =
132 Generate.generate1 thy (Tactic.Apply_Method' (mI, SOME t, is, ctxt))
133 (is, ctxt) (lev_on p, Frm)(*implicit Take*) pt;
134 in ("ok",([(Tactic.Apply_Method mI, Tactic.Apply_Method' (mI, SOME t, is, ctxt),
135 ((lev_on p, Frm), (is, ctxt)))], c, (pt, pos)))
137 | NONE => (*execute first tac in the Program, compare solve m*)
139 val (m', (is', ctxt'), _) =
140 LucinNEW.determine_next_tactic (thy', srls) (pt, (p, Res)) sc (is, ctxt);
142 case LucinNEW.locate_input_tactic sc (pt, (p, Res)) is' ctxt' m' of
143 LucinNEW.Safe_Step (istate, ctxt, tac) =>
145 val (p'', _, _,pt') =
146 Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
147 (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
148 (istate, ctxt) (lev_on p, Pbl) pt;
150 ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))],
151 [(*ctree NOT cut*)], (pt', p'')))
153 | _ => (* NotLocatable, but applicable_in from the beginning *)
156 Generate.generate_hard (Celem.assoc_thy "Isac_Knowledge") m (p, Frm) pt;
158 ("not-found-in-script",([(Lucin.tac_2tac m, m, (pos, (is, ctxt)))], ps, (pt, p)))
162 | solve ("Free_Solve", Tactic.Free_Solve') (pt, po as (p, _)) =
164 val p' = lev_dn_ (p, Res);
165 val pt = update_metID pt (par_pblobj pt p) Celem.e_metID;
167 ("ok", ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, (po, (Istate.Uistate, ContextC.e_ctxt)))], [], (pt,p')))
169 | solve ("Check_Postcond", Tactic.Check_Postcond' (pI, _)) (pt, (p, p_)) =
171 val pp = par_pblobj pt p
173 (case get_obj g_tac pt p of (*assumes Check_elementwise IMMEDIATELY BEFORE Check_Postcond*)
174 Tactic.Check_elementwise _ => (*collects and instantiates asms*)
175 (snd o (get_obj g_result pt)) p
176 | _ => get_assumptions_ pt (p,p_))
177 handle _ => [] (*WN.27.5.03 asms in subpbls not completely clear*)
178 val metID = get_obj g_metID pt pp;
179 val {srls = srls, scr = sc, ...} = Specify.get_met metID;
180 val (loc, pst, ctxt) = case get_loc pt (p, p_) of
181 loc as (Istate.Pstate pst, ctxt) => (loc, pst, ctxt)
182 | _ => error "solve Check_Postcond: uncovered case get_loc"
184 val thy' = get_obj g_domID pt pp;
185 val thy = Celem.assoc_thy thy';
186 val (_, _, (scval, _(*scsaf*))) = LucinNEW.determine_next_tactic (thy', srls) (pt, (p, p_)) sc loc;
187 (* Telem.safe should go on to Check_Postcond' vvvvv *)
192 val is = Istate.Pstate (pst |> Istate.upd_act scval |> Istate.upd_appy Istate.Skip_)
193 val tac_ = Tactic.Check_Postcond' (pI, (scval, asm))
194 (*extend Tactic.Check_Postcond' (pI, (scval, asm), scsaf) ^^^^^ *)
195 val (pos, ps, _, pt) = Generate.generate1 thy tac_ (is, ctxt) (pp, Res) pt;
196 in ("ok", ([(Tactic.Check_Postcond pI, tac_, ((pp, Res), (is, ctxt)))], ps, (pt, pos))) end
198 let (*resume script of parpbl, transfer value of subpbl-script*)
199 val ppp = par_pblobj pt (lev_up p);
200 val thy' = get_obj g_domID pt ppp;
201 val thy = Celem.assoc_thy thy';
202 val (pst', ctxt') = case get_loc pt (pp, Frm) of
203 (Istate.Pstate pst', ctxt') => (pst', ctxt')
204 | _ => error "solve Check_Postcond resume script of parpbl: uncovered case get_loc"
205 val ctxt'' = ContextC.from_subpbl_to_caller ctxt scval ctxt'
206 val ((p, p_), ps, _, pt) = Generate.generate1 thy (Tactic.Check_Postcond' (pI, (scval, asm)))
207 (Istate.Pstate (pst' |> Istate.upd_act scval |> Istate.upd_appy Istate.Skip_), ctxt'') (pp,Res) pt;
208 in ("ok", ([(Tactic.Check_Postcond pI, Tactic.Check_Postcond'(pI, (scval, asm)),
209 ((pp, Res), (Istate.Pstate (pst' |> Istate.upd_act scval |> Istate.upd_appy Istate.Skip_), ctxt'')))], ps, (pt, (p, p_)))) end
211 | solve (_, Tactic.End_Proof'') (pt, (p, p_)) =
212 ("end-proof", ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, (([], Res), (Istate.Uistate, ContextC.e_ctxt)))], [], (pt, (p, p_))))
213 | solve (_, Tactic.End_Detail' t) (pt, (p, p_)) = (* could be done by generate1 ?!? *)
214 let (*Rewrite_Set* done at Detail_Set*: this result is already in ctree*)
215 val pr = (lev_up p, Res)
217 ("ok", ([(Tactic.End_Detail, Tactic.End_Detail' t , ((p, p_), get_loc pt (p, p_)))], [], (pt, pr)))
219 (* ======== general case as fall htrough ======== *)
220 | solve (_, m) (pt, po as (p, p_)) =
221 if Celem.e_metID = get_obj g_metID pt (par_pblobj pt p) (*29.8.02: could be detail, too !!*)
224 val ctxt = get_ctxt pt po
225 val ((p,p_),ps,_,pt) = Generate.generate1 (Celem.assoc_thy (get_obj g_domID pt (par_pblobj pt p)))
226 m (Istate.e_istate, ctxt) (p, p_) pt;
227 in ("no-method-specified", (*Free_Solve*)
228 ([(Tactic.Empty_Tac, Tactic.Empty_Tac_, ((p, p_), (Istate.Uistate, ctxt)))], ps, (pt, (p, p_))))
232 val thy' = get_obj g_domID pt (par_pblobj pt p);
233 val (_, is, sc) = Lucin.from_pblobj_or_detail' thy' (p,p_) pt;
235 case LucinNEW.locate_input_tactic sc (pt, po) (fst is) (snd is) m of
236 LucinNEW.Safe_Step (istate, ctxt, tac) =>
241 | _ => error ("solve: call by " ^ pos'2str (p, p_));
242 val (p'', _, _,pt') =
243 Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
244 (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
245 (istate, ctxt) (p', p_) pt;
247 ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))],
248 [(*ctree NOT cut*)], (pt', p'')))
250 | LucinNEW.Unsafe_Step (istate, ctxt, tac) =>
255 | _ => error ("solve: call by " ^ pos'2str (p, p_));
256 val (p'', _, _,pt') =
257 Generate.generate1 (Celem.assoc_thy "Isac_Knowledge") tac
258 (* DEL.^^^^^ ContextC.insert_assumptions asms' ctxt 2nd, fst in Lucin.associate *)
259 (istate, ctxt) (p', p_) pt;
261 ("ok", ([(Lucin.tac_2tac tac, tac, (p'', (istate, ctxt)))],
262 [(*ctree NOT cut*)], (pt', p'')))
264 | _ => (* NotLocatable *)
266 val (p,ps, _, pt) = Generate.generate_hard (Celem.assoc_thy "Isac_Knowledge") m (p, p_) pt;
268 ("not-found-in-script", ([(Lucin.tac_2tac m, m, (po, is))], ps, (pt, p)))
272 (* tell how may steps of a calculation should be done by "fun autocalc"
273 FIXXXME040624: does NOT match interfaces/ITOCalc.java
274 TODO.WN0512 redesign togehter with autocalc ? *)
276 Step of int (*1 do #int steps (may stop in model/specify)
277 IS VERY INEFFICIENT IN MODEL/SPECIY *)
278 | CompleteModel (*2 complete modeling
279 if model complete, finish specifying *)
280 | CompleteCalcHead (*3 complete model/specify in one go *)
281 | CompleteToSubpbl (*4 stop at the next begin of a subproblem,
282 if none, complete the actual (sub)problem *)
283 | CompleteSubpbl (*5 complete the actual (sub)problem (incl.ev.subproblems) *)
284 | CompleteCalc; (*6 complete the calculation as a whole *)
286 fun autoord (Step _ ) = 1
287 | autoord CompleteModel = 2
288 | autoord CompleteCalcHead = 3
289 | autoord CompleteToSubpbl = 4
290 | autoord CompleteSubpbl = 5
291 | autoord CompleteCalc = 6;
293 fun complete_solve auto c (ptp as (_, p as (_, p_))) =
295 then ("end-of-calculation", [], ptp)
297 if member op = [Pbl,Met] p_
300 val ptp = Chead.all_modspec ptp
301 val (_, c', ptp) = all_solve auto c ptp
302 in complete_solve auto (c @ c') ptp end
304 case LucinNEW.do_solve_step ptp of
305 ((Tactic.Subproblem _, _, _) :: _, c', ptp') =>
307 then ("ok", c @ c', ptp)
310 val ptp = Chead.all_modspec ptp'
311 val (_, c'', ptp) = all_solve auto (c @ c') ptp
312 in complete_solve auto (c @ c'@ c'') ptp end
313 | ((Tactic.Check_Postcond _, _, _) :: _, c', ptp' as (_, p')) =>
314 if autoord auto < 6 orelse p' = ([], Res)
315 then ("ok", c @ c', ptp')
316 else complete_solve auto (c @ c') ptp'
317 | ((Tactic.End_Detail, _, _) :: _, c', ptp') =>
319 then ("ok", c @ c', ptp')
320 else complete_solve auto (c @ c') ptp'
321 | (_, c', ptp') => complete_solve auto (c @ c') ptp'
322 and all_solve auto c (ptp as (pt, pos as (p,_)): ctree * pos') =
324 val (_, _, mI) = get_obj g_spec pt p
325 val ctxt = get_ctxt pt pos
326 val (_, c', ptp) = LucinNEW.begin_end_prog (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ctxt)) (Istate.e_istate, ctxt) ptp
328 complete_solve auto (c @ c') ptp
331 (* aux.fun for detailrls with Rrls, reverse rewriting *)
332 fun rul_terms_2nds _ nds _ [] = nds
333 | rul_terms_2nds thy nds t ((rule, res as (t', _)) :: rts) =
334 (append_atomic [] (Istate.e_istate, ContextC.e_ctxt) t (Tactic.rule2tac thy [] rule) res Complete EmptyPtree) ::
335 (rul_terms_2nds thy nds t' rts);
337 (* detail steps done internally by Rewrite_Set* into ctree by use of a script *)
338 fun detailrls pt (pos as (p, _)) =
340 val t = get_obj g_form pt p
341 val tac = get_obj g_tac pt p
342 val rls = (assoc_rls o Tactic.rls_of) tac
343 val ctxt = get_ctxt pt pos
346 Rule.Rrls {scr = Rule.Rfuns {init_state, ...}, ...} =>
348 val (_, _, _, rul_terms) = init_state t
349 val newnds = rul_terms_2nds (Proof_Context.theory_of ctxt) [] t rul_terms
350 val pt''' = ins_chn newnds pt p
351 in ("detailrls", pt''', (p @ [length newnds], Res)) end
354 val is = Generate.init_istate tac t
355 (*TODO.WN060602 Pstate (["(t_, Problem (Isac,[equation,univar]))"]
356 is wrong for simpl, but working ?!? *)
357 val tac_ = Tactic.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
358 val pos' = ((lev_on o lev_dn) p, Frm)
359 val thy = Celem.assoc_thy "Isac_Knowledge"
360 val (_, _, _, pt') = Generate.generate1 thy tac_ (is, ctxt) pos' pt (* implicit Take *)
361 val (_,_, (pt'', _)) = complete_solve CompleteSubpbl [] (pt', pos')
362 val newnds = children (get_nd pt'' p)
363 val pt''' = ins_chn newnds pt p (*complete_solve cuts branches after*)
364 in ("detailrls", pt''', (p @ [length newnds], Res)) end
367 fun get_form (mI, m) (p,p_) pt =
368 case Applicable.applicable_in (p, p_) pt m of
369 Chead.Notappl e => Generate.Error' e
371 if member op = specsteps mI
373 let val (_, _, f, _, _, _) = Chead.specify m (p, p_) [] pt
375 else Generate.EmptyMout;
377 fun inform (next_cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =
379 val ctxt = get_ctxt pt pos (*see TODO.thy*)
381 case TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr of
382 NONE => ("syntax error in '" ^ istr ^ "'", Chead.e_calcstate' (*TODO: previous cs'*))
385 val f_in = Thm.term_of f_in
386 val pos_pred = lev_back(*'*) pos
387 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
388 val f_succ = Ctree.get_curr_formula (pt, pos);
391 then ("same-formula", next_cs) (* ctree not cut with replaceFormula *)
393 case Inform.cas_input f_in of
394 SOME (pt, _) => ("ok",([], [], (pt, (p, Ctree.Met))))
395 | NONE => (*/-------------------------------------- NEW fun locate_input_formula------*)
397 val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
398 val {scr = prog, ...} = Specify.get_met metID
399 val istate = get_istate pt pos
400 val ctxt = get_ctxt pt pos
402 case LucinNEW.locate_input_formula prog (pt, pos) istate ctxt f_in of
403 LucinNEW.Step (cstate, _(*istate*), _(*ctxt*)) =>
404 ("ok" , ([], [], cstate (* already contains istate, ctxt *)))
405 | LucinNEW.Not_Derivable calcstate' =>
407 val pp = Ctree.par_pblobj pt p
408 val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
409 {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
410 | _ => error "inform: uncovered case of get_met"
411 val {env, ...} = Ctree.get_istate pt pos |> Istate.the_pstate
413 case Inform.check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
414 SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
415 | NONE => ("no derivation found", calcstate')