1 (* The _functional_ mathematics engine, ie. without a state.
2 Input and output are Isabelle's formulae as strings.
3 authors: Walther Neuper 2000
4 (c) due to copyright terms
9 signature MATH_ENGINE =
11 type NEW (* TODO: refactor "fun me" with calcstate and remove *)
12 val me : Solve.tac'_ -> Ctree.pos' -> NEW -> Ctree.ptree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Ctree.safe * Ctree.ptree
14 Ctree.pos' list -> Ctree.pos' -> (Ctree.ptree * Ctree.pos') * Generate.taci list -> Solve.auto -> string * Ctree.pos' list * (Ctree.ptree * Ctree.pos')
16 Ctree.tac -> Ctree.ptree * Ctree.pos' -> string * (Generate.taci list * Ctree.pos' list * (Ctree.ptree * Ctree.pos'))
17 val step : Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate'
19 Ctree.ptree -> Ctree.pos' -> string * Ctree.ptree * Ctree.pos'
20 val get_pblID : Ctree.ptree * Ctree.pos' -> pblID option
22 val initcontext_met : Ctree.ptree -> Ctree.pos' -> bool * string list * scr * itm list * (bool * term) list
23 val initcontext_pbl : Ctree.ptree -> Ctree.pos' -> bool * string list * term * itm list * (bool * term) list
24 val context_met : metID -> Ctree.ptree -> Ctree.pos -> bool * metID * scr * itm list * (bool * term) list
25 val context_pbl : pblID -> Ctree.ptree -> Ctree.pos -> bool * pblID * term * itm list * (bool * term) list
26 val set_method : metID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd
27 val set_problem : pblID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd
28 val set_theory : thyID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd
29 val tryrefine : pblID -> Ctree.ptree -> Ctree.pos' -> bool * pblID * term * itm list * (bool * term) list
31 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
34 val CalcTreeTEST : Ctree.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Ctree.tac) * Ctree.safe * Ctree.ptree
35 val f2str : Generate.mout -> cterm'
36 val loc_solve_ : string * Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> lOc_
37 val loc_specify_ : Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> lOc_
38 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
42 structure Math_Engine(**): MATH_ENGINE(**) =
46 fun get_pblID (pt, (p, _): Ctree.pos') =
47 let val p' = Ctree.par_pblobj pt p
48 val (_, pI, _) = Ctree.get_obj Ctree.g_spec pt p'
49 val (_, (_, oI, _), _) = Ctree.get_obj Ctree.g_origin pt p'
54 if oI <> e_pblID then SOME oI else NONE end;
56 (* introduced for test only *)
57 val e_tac_ = Ctree.Tac_ (Pure.thy, "", "", "");
59 ERror of string (*after loc_specify, loc_solve*)
60 | UNsafe of Chead.calcstate' (*after loc_specify, loc_solve*)
61 | Updated of Chead.calcstate' (*after loc_specify, loc_solve*)
63 fun loc_specify_ m (pt,pos) =
65 val (p, _, f, _, _, pt) = Chead.specify m pos [] pt;
67 case f of (Generate.Error' e) => ERror e | _ => Updated ([], [], (pt,p))
70 (* TODO push return-value cs' into solve and rename solve->loc_solve?_? *)
71 fun loc_solve_ m (pt, pos) =
73 val (msg, cs') = Solve.solve m (pt, pos);
75 case msg of "ok" => Updated cs' | msg => ERror msg
80 | Nexts of Chead.calcstate (**)
82 (* locate a tactic in a script and apply it if possible;
83 report of tacs' applicability in tacis; pt is dropped in setNextTactic*)
84 fun locatetac _ (ptp as (_, ([], Res))) = ("end-of-calculation", ([], [], ptp))
85 | locatetac tac (ptp as (pt, p)) =
87 val (mI, m) = Solve.mk_tac'_ tac;
89 case Applicable.applicable_in p pt m of
90 Chead.Notappl _ => ("not-applicable", ([],[], ptp): Chead.calcstate')
93 val x = if member op = Solve.specsteps mI
94 then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
97 ERror _ => ("failure", ([], [], ptp))
98 (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
99 | UNsafe cs' => ("unsafe-ok", cs')
100 | Updated (cs' as (_, _, (_, p'))) => (*ev.SEVER.tacs like Begin_Trans*)
101 (if p' = ([], Ctree.Res) then "end-of-calculation" else "ok", cs')
102 (*for SEVER.tacs user to ask ? *)
106 (* iterated by nxt_me; there (the resulting) ptp dropped
107 may call nxt_solve Apply_Method --- thus evaluated here after solve.sml *)
108 fun nxt_specify_ (ptp as (pt, (p, p_))) =
110 val (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) =
111 case Ctree.get_obj I pt p of
112 pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
113 probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)
114 | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj"
116 if Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin
119 ["no_met"] => Chead.nxt_specif (Ctree.Refine_Tacitly pI') (pt, (p, Ctree.Pbl))
120 | _ => Chead.nxt_specif Ctree.Model_Problem (pt, (p, Ctree.Pbl))
123 val cpI = if pI = e_pblID then pI' else pI;
124 val cmI = if mI = e_metID then mI' else mI;
125 val {ppc, prls, where_, ...} = Specify.get_pbt cpI;
126 val pre = check_preconds "thy 100820" prls where_ probl;
127 val pb = foldl and_ (true, map fst pre);
128 (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
130 Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
133 Ctree.Apply_Method mI =>
134 Solve.nxt_solv (Ctree.Apply_Method' (mI, NONE, Ctree.e_istate, Ctree.e_ctxt)) (Ctree.e_istate, Ctree.e_ctxt) ptp
135 | _ => Chead.nxt_specif tac ptp
139 (* specify a new method; WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' *)
140 fun set_method mI ptp =
143 case Chead.nxt_specif (Ctree.Specify_Method mI) ptp of
144 ([(_, Ctree.Specify_Method' (_, _, mits), _)], [], (pt, (p,_))) => (mits, pt, p)
145 | _ => error "set_method: case 1 uncovered"
146 val pre = [] (*...from Specify_Method'*)
147 val complete = true (*...from Specify_Method'*)
148 (*from Specify_Method' ? vvv, vvv ?*)
150 case Ctree.get_obj I pt p of
151 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
152 | Ctree.PrfObj _ => error "set_method: case 2 uncovered"
154 (pt, (complete, Ctree.Met, hdf, mits, pre, spec) : Ctree.ocalhd)
157 (* specify a new problem; WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' *)
158 fun set_problem pI ptp =
160 val (complete, pits, pre, pt, p) =
161 case Chead.nxt_specif (Ctree.Specify_Problem pI) ptp of
162 ([(_, Ctree.Specify_Problem' (_, (complete, (pits, pre))),_)], _, (pt, (p,_)))
163 => (complete, pits, pre, pt, p)
164 | _ => error "set_problem: case 1 uncovered"
165 (*from Specify_Problem' ? vvv, vvv ?*)
167 case Ctree.get_obj I pt p of
168 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
169 | Ctree.PrfObj _ => error "set_problem: case 2 uncovered"
171 (pt, (complete, Ctree.Pbl, hdf, pits, pre, spec) : Ctree.ocalhd)
174 fun set_theory tI ptp =
176 val (complete, pits, pre, pt, p) =
177 case Chead.nxt_specif (Ctree.Specify_Theory tI) ptp of
178 ([(_, Ctree.Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _)))
179 => (complete, pits, pre, pt, p)
180 | _ => error "set_theory: case 1 uncovered"
181 (*from Specify_Theory' ? vvv, vvv ?*)
183 case Ctree.get_obj I pt p of
184 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
185 | Ctree.PrfObj _ => error "set_theory: case 2 uncovered"
186 in (pt, (complete, Ctree.Pbl, hdf, pits, pre, spec) : Ctree.ocalhd) end;
188 (* does a step forward; returns tactic used, ctree updated.
189 TODO.WN0512 redesign after specify-phase became more separated from solve-phase *)
190 fun step (ip as (_, p_)) (ptp as (pt,p), tacis) =
191 let val pIopt = get_pblID (pt,ip);
193 if ip = ([], Ctree.Res)
194 then ("end-of-calculation", (tacis, [], ptp): Chead.calcstate')
198 if ip = p (*the request is done where ptp waits for*)
200 let val (pt',c',p') = Generate.generate tacis (pt,[],p)
201 in ("ok", (tacis, c', (pt', p'))) end
202 else (case (if member op = [Ctree.Pbl, Ctree.Met] p_
203 then nxt_specify_ (pt, ip) else Solve.nxt_solve_ (pt, ip))
204 handle ERROR msg => (writeln ("*** " ^ msg);
205 ([], [], ptp)) (*e.g. Add_Given "equality///"*) of
206 cs as ([],_,_) => ("helpless", cs)
208 | _ => (case pIopt of
209 NONE => ("no-fmz-spec", ([], [], ptp))
210 | SOME _ => (*vvvvvv: Apply_Method without init_form*)
211 (case if member op = [Ctree.Pbl, Ctree.Met] p_ andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p))
212 then nxt_specify_ (pt, ip)
213 else (Solve.nxt_solve_ (pt,ip))
214 handle ERROR msg => (writeln ("*** " ^ msg);
215 ([],[],ptp)) (*e.g. Add_Given "equality///"*) of
216 cs as ([],_,_) =>("helpless", cs) (*FIXXME del.handle*)
220 (* does several steps within one calculation as given by "type auto";
221 the steps may arbitrarily go into and leave different phases,
222 i.e. specify-phase and solve-phase
223 TODO.WN0512 ? redesign after the phases have been more separated
224 at the fron-end in 05:
225 eg. CompleteCalcHead could be done by a separate fun !!!*)
226 fun autocalc c ip cs (Solve.Step s) =
229 let val (str, (_, c', ptp)) = step ip cs; (* autoord = 1, probably does 1 step too much*)
230 in (str, c@c', ptp) end
232 let val (str, (_, c', ptp as (_, p))) = step ip cs;
235 then autocalc (c@c') p (ptp, []) (Solve.Step (s - 1))
236 else (str, c@c', ptp) end
237 (* handles autoord <= 3, autoord > 3 handled by all_solve, complete_solve *)
238 | autocalc c (pos as (_, p_)) ((pt, _), _(*tacis could help 1x in solve*)) auto =
239 if Solve.autoord auto > 3 andalso Ctree.just_created (pt, pos)
241 let val ptp = Chead.all_modspec (pt, pos);
242 in Solve.all_solve auto c ptp end (*... auto = 4 | 5 | 6 *)
244 if member op = [Ctree.Pbl, Ctree.Met] p_
246 if not (Chead.is_complete_mod (pt, pos))
248 let val ptp = Chead.complete_mod (pt, pos) (*... auto = 2 | 3 *)
250 if Solve.autoord auto < 3 then ("ok", c, ptp)
252 if not (Chead.is_complete_spec ptp)
254 let val ptp = Chead.complete_spec ptp
256 if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
258 else if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
261 if not (Chead.is_complete_spec (pt,pos))
263 let val ptp = Chead.complete_spec (pt, pos)
265 if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
268 if Solve.autoord auto = 3 then ("ok", c, (pt, pos)) else Solve.all_solve auto c (pt, pos)
269 else Solve.complete_solve auto c (pt, pos);
271 (*.initialiye matching; before 'tryMatch' get the pblID to match with:
272 if no pbl has been specified, take the init from origin.*)
273 fun initcontext_pbl pt (p, _) =
275 val (probl, os, pI, hdl, pI') =
276 case Ctree.get_obj I pt p of
277 Ctree.PblObj {probl, origin = (os, (_, pI, _), hdl), spec=(_, pI', _), ...}
278 => (probl, os, pI, hdl, pI')
279 | Ctree.PrfObj _ => error "initcontext_pbl: uncovered case"
282 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
284 val {ppc, where_, prls, ...} = Specify.get_pbt pblID
285 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
287 (model_ok, pblID, hdl, pbl, pre)
290 fun initcontext_met pt (p,_) =
292 val (meth, os, mI, mI') =
293 case Ctree.get_obj I pt p of
294 Ctree.PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI')
295 | Ctree.PrfObj _ => error "initcontext_met: uncovered case"
296 val metID = if mI' = e_metID
297 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
299 val {ppc, pre, prls, scr, ...} = Specify.get_met metID
300 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
302 (model_ok, metID, scr, pbl, pre)
305 (* match the model of a problem at pos p with the model-pattern of the problem with pblID *)
306 fun context_pbl pI pt p =
308 val (probl, os, hdl) =
309 case Ctree.get_obj I pt p of
310 Ctree.PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl)
311 | Ctree.PrfObj _ => error "context_pbl: uncovered case"
312 val {ppc,where_,prls,...} = Specify.get_pbt pI
313 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
315 (model_ok, pI, hdl, pbl, pre)
318 fun context_met mI pt p =
321 case Ctree.get_obj I pt p of
322 Ctree.PblObj {meth, origin = (os, _, _),...} => (meth, os)
323 | Ctree.PrfObj _ => error "context_met: uncovered case"
324 val {ppc,pre,prls,scr,...} = Specify.get_met mI
325 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
327 (model_ok, mI, scr, pbl, pre)
330 fun tryrefine pI pt (p,_) =
332 val (probl, os, hdl) =
333 case Ctree.get_obj I pt p of
334 Ctree.PblObj {probl, origin = (os, _, hdl), ...} => (probl, os, hdl)
335 | Ctree.PrfObj _ => error "context_met: uncovered case"
337 case Specify.refine_pbl (assoc_thy "Isac") pI probl of
338 NONE => (*copy from context_pbl*)
340 val {ppc,where_,prls,...} = Specify.get_pbt pI
341 val (_, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
343 (false, pI, hdl, pbl, pre)
345 | SOME (pI, (pbl, pre)) => (true, pI, hdl, pbl, pre)
348 fun detailstep pt (pos as (p, _)) =
350 val nd = Ctree.get_nd pt p
351 val cn = Ctree.children nd
355 if (Ctree.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)]
356 then Solve.detailrls pt pos
357 else ("no-Rewrite_Set...", Ctree.EmptyPtree, Ctree.e_pos')
358 else ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Ctree.Res))
362 (*** for mathematics authoring on sml-toplevel; no XML ***)
366 (* 15.8.03 for me with loc_specify/solve, nxt_specify/solve
367 delete as soon as TESTg_form -> _mout_ dropped *)
370 val (form, _, _) = Chead.pt_extract ptp
373 Ctree.Form t => Generate.FormKF (term2str t)
374 | Ctree.ModSpec (_, p_, _, gfr, pre, _) =>
376 (case p_ of Pbl => Generate.Problem [] | Met => Generate.Method []
377 | _ => error "TESTg_form: uncovered case",
378 Specify.itms2itemppc (assoc_thy"Isac") gfr pre))
381 (* create a calc-tree; for use within sml: thus "^^^" NOT decoded to "^" etc;
382 compare "fun CalcTree" which DOES decode *)
383 fun CalcTreeTEST [(fmz, sp)] =
385 val ((pt, p), tacis) = Chead.nxt_specify_init_calc (fmz, sp)
386 val tac = case tacis of [] => Ctree.Empty_Tac | _ => (#1 o hd) tacis
387 val f = TESTg_form (pt,p)
388 in (p, []:NEW, f, (Ctree.tac2IDstr tac, tac), Ctree.Sundef, pt) end
389 | CalcTreeTEST _ = error "CalcTreeTEST: uncovered case"
391 (*for tests > 15.8.03 after separation setnexttactic / nextTac:
392 external view: me should be used by math-authors as done so far
393 internal view: loc_specify/solve, nxt_specify/solve used
394 i.e. same as in setnexttactic / nextTac*)
395 (*ENDE TESTPHASE 08/10.03:
396 NEW loeschen, eigene Version von locatetac, step
397 meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *)
399 fun me (_, tac) p _(*NEW remove*) pt =
402 (*locatetac is here for testing by me; step would suffice in me*)
403 case locatetac tac (pt,p) of
404 ("ok", (_, _, ptp)) => ptp
405 | ("unsafe-ok", (_, _, ptp)) => ptp
406 | ("not-applicable",_) => (pt, p)
407 | ("end-of-calculation", (_, _, ptp)) => ptp
408 | ("failure", _) => error "sys-error"
409 | _ => error "me: uncovered case"
411 (case step p ((pt, Ctree.e_pos'),[]) of
412 ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
413 | ("helpless", _) => ("helpless: cannot propose tac", [])
414 | ("no-fmz-spec", _) => error "no-fmz-spec"
415 | ("end-of-calculation", (ts, _, _)) => ("", ts)
416 | _ => error "me: uncovered case")
417 handle ERROR msg => raise ERROR msg
420 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
421 | _ => if p = ([], Ctree.Res) then Ctree.End_Proof' else Ctree.Empty_Tac;
422 in (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *),
423 (Ctree.tac2IDstr tac, tac), Ctree.Sundef, pt)
426 (* for quick test-print-out, until 'type inout' is removed *)
427 fun f2str (Generate.FormKF cterm') = cterm';