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 : tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * Ctree.mout * tac'_ * safe * ptree
14 pos' list -> pos' -> (ptree * pos') * Ctree.taci list -> auto -> string * pos' list * (ptree * pos')
16 tac -> ptree * (posel list * pos_) -> string * (Ctree.taci list * pos' list * (ptree * pos'))
17 val step : pos' -> Chead.calcstate -> string * Chead.calcstate'
19 ptree -> pos' -> string * ptree * pos' val get_pblID : ptree * pos' -> pblID option
21 val initcontext_met : ptree -> pos' -> bool * string list * scr * itm list * (bool * term) list
22 val initcontext_pbl : ptree -> pos' -> bool * string list * term * itm list * (bool * term) list
23 val context_met : metID -> ptree -> pos -> bool * metID * scr * itm list * (bool * term) list
24 val context_pbl : pblID -> ptree -> pos -> bool * pblID * term * itm list * (bool * term) list
25 val set_method : metID -> ptree * pos' -> ptree * ocalhd
26 val set_problem : pblID -> ptree * pos' -> ptree * ocalhd
27 val set_theory : thyID -> ptree * pos' -> ptree * ocalhd
28 val tryrefine : pblID -> ptree -> pos' -> bool * pblID * term * itm list * (bool * term) list
30 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
33 val CalcTreeTEST : fmz list -> pos' * NEW * Ctree.mout * (string * tac) * safe * ptree
34 val f2str : Ctree.mout -> cterm'
35 val loc_solve_ : string * tac_ -> ptree * (pos * pos_) -> lOc_
36 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
40 structure Math_Engine(**): MATH_ENGINE(**) =
44 fun get_pblID (pt, (p, _):pos') =
45 let val p' = par_pblobj pt p
46 val (_, pI, _) = get_obj g_spec pt p'
47 val (_, (_, oI, _), _) = get_obj g_origin pt p'
52 if oI <> e_pblID then SOME oI else NONE end;
54 (* introduced for test only *)
55 val e_tac_ = Tac_ (Pure.thy, "", "", "");
57 ERror of string (*after loc_specify, loc_solve*)
58 | UNsafe of Chead.calcstate' (*after loc_specify, loc_solve*)
59 | Updated of Chead.calcstate' (*after loc_specify, loc_solve*)
61 fun loc_specify_ m (pt,pos) =
63 val (p, _, f, _, _, pt) = Chead.specify m pos [] pt;
65 case f of (Ctree.Error' e) => ERror e | _ => Updated ([], [], (pt,p))
68 (* TODO push return-value cs' into solve and rename solve->loc_solve?_? *)
69 fun loc_solve_ m (pt, pos) =
71 val (msg, cs') = solve m (pt, pos);
73 case msg of "ok" => Updated cs' | msg => ERror msg
78 | Nexts of Chead.calcstate (**)
80 (* locate a tactic in a script and apply it if possible;
81 report of tacs' applicability in tacis; pt is dropped in setNextTactic*)
82 fun locatetac _ (ptp as (_, ([], Res))) = ("end-of-calculation", ([], [], ptp))
83 | locatetac tac (ptp as (pt, p)) =
85 val (mI, m) = mk_tac'_ tac;
87 case applicable_in p pt m of
88 Chead.Notappl _ => ("not-applicable", ([],[], ptp): Chead.calcstate')
91 val x = if member op = specsteps mI
92 then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
95 ERror _ => ("failure", ([], [], ptp))
96 (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
97 | UNsafe cs' => ("unsafe-ok", cs')
98 | Updated (cs' as (_, _, (_, p'))) => (*ev.SEVER.tacs like Begin_Trans*)
99 (if p' = ([],Res) then "end-of-calculation" else "ok", cs')
100 (*for SEVER.tacs user to ask ? *)
104 (* iterated by nxt_me; there (the resulting) ptp dropped
105 may call nxt_solve Apply_Method --- thus evaluated here after solve.sml *)
106 fun nxt_specify_ (ptp as (pt, (p, p_))) =
108 val (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) =
109 case get_obj I pt p of
110 pblobj as (PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
111 probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)
112 | PrfObj _ => error "nxt_specify_: not on PrfObj"
114 if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
117 ["no_met"] => Chead.nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
118 | _ => Chead.nxt_specif Model_Problem (pt, (p,Pbl))
121 val cpI = if pI = e_pblID then pI' else pI;
122 val cmI = if mI = e_metID then mI' else mI;
123 val {ppc, prls, where_, ...} = get_pbt cpI;
124 val pre = check_preconds "thy 100820" prls where_ probl;
125 val pb = foldl and_ (true, map fst pre);
126 (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
128 Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o get_met) cmI) (dI, pI, mI)
132 nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
133 | _ => Chead.nxt_specif tac ptp
137 (* specify a new method; WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' *)
138 fun set_method (mI:metID) ptp =
141 case Chead.nxt_specif (Specify_Method mI) ptp of
142 ([(_, Specify_Method' (_, _, mits), _)], [], (pt, (p,_))) => (mits, pt, p)
143 | _ => error "set_method: case 1 uncovered"
144 val pre = [] (*...from Specify_Method'*)
145 val complete = true (*...from Specify_Method'*)
146 (*from Specify_Method' ? vvv, vvv ?*)
148 case get_obj I pt p of
149 PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
150 | PrfObj _ => error "set_method: case 2 uncovered"
152 (pt, (complete, Met, hdf, mits, pre, spec) : ocalhd)
155 (* specify a new problem; WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' *)
156 fun set_problem pI (ptp: ptree * pos') =
158 val (complete, pits, pre, pt, p) =
159 case Chead.nxt_specif (Specify_Problem pI) ptp of
160 ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)], _, (pt, (p,_)))
161 => (complete, pits, pre, pt, p)
162 | _ => error "set_problem: case 1 uncovered"
163 (*from Specify_Problem' ? vvv, vvv ?*)
165 case get_obj I pt p of
166 PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
167 | PrfObj _ => error "set_problem: case 2 uncovered"
169 (pt, (complete, Pbl, hdf, pits, pre, spec) : ocalhd)
172 fun set_theory (tI:thyID) (ptp: ptree * pos') =
174 val (complete, pits, pre, pt, p) =
175 case Chead.nxt_specif (Specify_Theory tI) ptp of
176 ([(_, Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _)))
177 => (complete, pits, pre, pt, p)
178 | _ => error "set_theory: case 1 uncovered"
179 (*from Specify_Theory' ? vvv, vvv ?*)
181 case get_obj I pt p of
182 PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
183 | PrfObj _ => error "set_theory: case 2 uncovered"
184 in (pt, (complete, Pbl, hdf, pits, pre, spec) : ocalhd) end;
186 (* does a step forward; returns tactic used, ctree updated.
187 TODO.WN0512 redesign after specify-phase became more separated from solve-phase *)
188 fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis): Chead.calcstate) =
189 let val pIopt = get_pblID (pt,ip);
192 then ("end-of-calculation", (tacis, [], ptp): Chead.calcstate')
196 if ip = p (*the request is done where ptp waits for*)
198 let val (pt',c',p') = Ctree.generate tacis (pt,[],p)
199 in ("ok", (tacis, c', (pt', p'))) end
200 else (case (if member op = [Pbl, Met] p_
201 then nxt_specify_ (pt, ip) else nxt_solve_ (pt, ip))
202 handle ERROR msg => (writeln ("*** " ^ msg);
203 ([], [], ptp)) (*e.g. Add_Given "equality///"*) of
204 cs as ([],_,_) => ("helpless", cs)
206 | _ => (case pIopt of
207 NONE => ("no-fmz-spec", ([], [], ptp))
208 | SOME _ => (*vvvvvv: Apply_Method without init_form*)
209 (case if member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p))
210 then nxt_specify_ (pt, ip)
211 else (nxt_solve_ (pt,ip))
212 handle ERROR msg => (writeln ("*** " ^ msg);
213 ([],[],ptp)) (*e.g. Add_Given "equality///"*) of
214 cs as ([],_,_) =>("helpless", cs) (*FIXXME del.handle*)
218 (* does several steps within one calculation as given by "type auto";
219 the steps may arbitrarily go into and leave different phases,
220 i.e. specify-phase and solve-phase
221 TODO.WN0512 ? redesign after the phases have been more separated
222 at the fron-end in 05:
223 eg. CompleteCalcHead could be done by a separate fun !!!*)
224 fun autocalc c ip cs (Step s) =
227 let val (str, (_, c', ptp)) = step ip cs; (* autoord = 1, probably does 1 step too much*)
228 in (str, c@c', ptp) end
230 let val (str, (_, c', ptp as (_, p))) = step ip cs;
233 then autocalc (c@c') p (ptp, []) (Step (s - 1))
234 else (str, c@c', ptp) end
235 (* handles autoord <= 3, autoord > 3 handled by all_solve, complete_solve *)
236 | autocalc c (pos as (_, p_)) ((pt, _), _(*tacis could help 1x in solve*)) auto =
237 if autoord auto > 3 andalso just_created (pt, pos)
239 let val ptp = Chead.all_modspec (pt, pos);
240 in all_solve auto c ptp end (*... auto = 4 | 5 | 6 *)
242 if member op = [Pbl, Met] p_
244 if not (Chead.is_complete_mod (pt, pos))
246 let val ptp = Chead.complete_mod (pt, pos) (*... auto = 2 | 3 *)
248 if autoord auto < 3 then ("ok", c, ptp)
250 if not (Chead.is_complete_spec ptp)
252 let val ptp = Chead.complete_spec ptp
254 if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
256 else if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
259 if not (Chead.is_complete_spec (pt,pos))
261 let val ptp = Chead.complete_spec (pt, pos)
263 if autoord auto = 3 then ("ok", c, ptp) else all_solve auto c ptp
266 if autoord auto = 3 then ("ok", c, (pt, pos)) else all_solve auto c (pt, pos)
267 else complete_solve auto c (pt, pos);
269 (*.initialiye matching; before 'tryMatch' get the pblID to match with:
270 if no pbl has been specified, take the init from origin.*)
271 fun initcontext_pbl pt (p, _) =
273 val (probl, os, pI, hdl, pI') =
274 case get_obj I pt p of
275 PblObj {probl, origin = (os, (_, pI, _), hdl), spec=(_, pI', _), ...}
276 => (probl, os, pI, hdl, pI')
277 | PrfObj _ => error "initcontext_pbl: uncovered case"
280 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
282 val {ppc, where_, prls, ...} = get_pbt pblID
283 val (model_ok, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
285 (model_ok, pblID, hdl, pbl, pre)
288 fun initcontext_met pt (p,_) =
290 val (meth, os, mI, mI') =
291 case get_obj I pt p of
292 PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI')
293 | PrfObj _ => error "initcontext_met: uncovered case"
294 val metID = if mI' = e_metID
295 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
297 val {ppc, pre, prls, scr, ...} = get_met metID
298 val (model_ok, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
300 (model_ok, metID, scr, pbl, pre)
303 (* match the model of a problem at pos p with the model-pattern of the problem with pblID *)
304 fun context_pbl pI pt (p:pos) =
306 val (probl, os, hdl) =
307 case get_obj I pt p of
308 PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl)
309 | PrfObj _ => error "context_pbl: uncovered case"
310 val {ppc,where_,prls,...} = get_pbt pI
311 val (model_ok, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
313 (model_ok, pI, hdl, pbl, pre)
316 fun context_met mI pt (p:pos) =
319 case get_obj I pt p of
320 PblObj {meth, origin = (os, _, _),...} => (meth, os)
321 | PrfObj _ => error "context_met: uncovered case"
322 val {ppc,pre,prls,scr,...} = get_met mI
323 val (model_ok, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
325 (model_ok, mI, scr, pbl, pre)
328 fun tryrefine pI pt (p,_) =
330 val (probl, os, hdl) =
331 case get_obj I pt p of
332 PblObj {probl, origin = (os, _, hdl), ...} => (probl, os, hdl)
333 | PrfObj _ => error "context_met: uncovered case"
335 case refine_pbl (assoc_thy "Isac") pI probl of
336 NONE => (*copy from context_pbl*)
338 val {ppc,where_,prls,...} = get_pbt pI
339 val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
341 (false, pI, hdl, pbl, pre)
343 | SOME (pI, (pbl, pre)) => (true, pI, hdl, pbl, pre)
346 fun detailstep pt (pos as (p, _):pos') =
353 if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)]
354 then detailrls pt pos
355 else ("no-Rewrite_Set...", EmptyPtree, e_pos')
356 else ("donesteps", pt, (p @ [length (children (get_nd pt p))], Res))
360 (*** for mathematics authoring on sml-toplevel; no XML ***)
364 (* 15.8.03 for me with loc_specify/solve, nxt_specify/solve
365 delete as soon as TESTg_form -> _mout_ dropped *)
368 val (form, _, _) = Chead.pt_extract ptp
371 Form t => Ctree.FormKF (term2str t)
372 | ModSpec (_,p_, _, gfr, pre, _) => Ctree.PpcKF (
373 (case p_ of Pbl => Ctree.Problem [] | Met => Ctree.Method []
374 | _ => error "TESTg_form: uncovered case",
375 itms2itemppc (assoc_thy"Isac") gfr pre))
378 (* create a calc-tree; for use within sml: thus "^^^" NOT decoded to "^" etc;
379 compare "fun CalcTree" which DOES decode *)
380 fun CalcTreeTEST [(fmz, sp)] =
382 val ((pt, p), tacis) = Chead.nxt_specify_init_calc (fmz, sp)
383 val tac = case tacis of [] => Empty_Tac | _ => (#1 o hd) tacis
384 val f = TESTg_form (pt,p)
385 in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end
386 | CalcTreeTEST _ = error "CalcTreeTEST: uncovered case"
388 (*for tests > 15.8.03 after separation setnexttactic / nextTac:
389 external view: me should be used by math-authors as done so far
390 internal view: loc_specify/solve, nxt_specify/solve used
391 i.e. same as in setnexttactic / nextTac*)
392 (*ENDE TESTPHASE 08/10.03:
393 NEW loeschen, eigene Version von locatetac, step
394 meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *)
396 fun me (_, tac) p _(*NEW remove*) pt =
399 (*locatetac is here for testing by me; step would suffice in me*)
400 case locatetac tac (pt,p) of
401 ("ok", (_, _, ptp)) => ptp
402 | ("unsafe-ok", (_, _, ptp)) => ptp
403 | ("not-applicable",_) => (pt, p)
404 | ("end-of-calculation", (_, _, ptp)) => ptp
405 | ("failure", _) => error "sys-error"
406 | _ => error "me: uncovered case"
408 (case step p ((pt, e_pos'),[]) of
409 ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
410 | ("helpless", _) => ("helpless: cannot propose tac", [])
411 | ("no-fmz-spec", _) => error "no-fmz-spec"
412 | ("end-of-calculation", (ts, _, _)) => ("", ts)
413 | _ => error "me: uncovered case")
414 handle ERROR msg => raise ERROR msg
417 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
418 | _ => if p = ([], Res) then End_Proof' else Empty_Tac;
419 in (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *),
420 (tac2IDstr tac, tac):tac'_, Sundef, pt)
423 (* for quick test-print-out, until 'type inout' is removed *)
424 fun f2str (Ctree.FormKF cterm') = cterm';