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
12 (* datatype nxt_ = HElpless | Nexts of CalcHead.calcstate *)
18 | UNsafe of CalcHead.calcstate'
19 | Updated of CalcHead.calcstate' *)
23 pos' * NEW * mout * (string * tac) * safe * ptree
25 val TESTg_form : ptree * (int list * pos_) -> mout
29 (ptree * pos') * taci list ->
30 auto -> string * pos' list * (ptree * pos')
31 val detailstep : ptree -> pos' -> string * ptree * pos'
32 (* val e_tac_ : tac_ *)
33 val f2str : mout -> cterm'
34 (* val get_pblID : ptree * pos' -> pblID option *)
35 val initmatch : ptree -> pos' -> ptform
37 string * tac_ -> ptree * (int list * pos_) -> lOc_ *)
38 (* val loc_specify_ : tac_ -> ptree * pos' -> lOc_ *)
39 val locatetac : (*tests only*)
41 ptree * (posel list * pos_) ->
42 string * (taci list * pos' list * (ptree * (posel list * pos_)))
47 ptree -> pos' * NEW * mout * tac'_ * safe * ptree
49 val nxt_specify_ : ptree * (int list * pos_) -> calcstate'(*tests only*)
50 val set_method : metID -> ptree * pos' -> ptree * ocalhd
51 val set_problem : pblID -> ptree * pos' -> ptree * ocalhd
52 val set_theory : thyID -> ptree * pos' -> ptree * ocalhd
53 val step : pos' -> calcstate -> string * calcstate'
54 val trymatch : pblID -> ptree -> pos' -> ptform
55 val tryrefine : pblID -> ptree -> pos' -> ptform
60 (*------------------------------------------------------------------(**)
61 structure MathEngine : MATHENGINE =
63 (**)------------------------------------------------------------------*)
65 fun get_pblID (pt, (p,_):pos') =
66 let val p' = par_pblobj pt p
67 val (_,pI,_) = get_obj g_spec pt p'
68 val (_,(_,oI,_),_) = get_obj g_origin pt p'
69 in if pI <> e_pblID then SOME pI
70 else if oI <> e_pblID then SOME oI
72 (*fun get_pblID (pt, (p,_):pos') =
73 ((snd3 o (get_obj g_spec pt)) (par_pblobj pt p));*)
76 (*--vvv--dummies for test*)
77 val e_tac_ = Tac_ (Pure.thy,"","","");
79 ERror of string (*after loc_specify, loc_solve*)
80 | UNsafe of calcstate' (*after loc_specify, loc_solve*)
81 | Updated of calcstate'; (*after loc_specify, loc_solve*)
82 fun loc_specify_ m (pt,pos) =
85 let val (p,_,f,_,s,pt) = specify m pos [] pt;
86 (* val (_,_,_,_,_,pt')= specify m pos [] pt;
89 (Error' (Error_ e)) => ERror e
90 | _ => Updated ([], [], (pt,p)) end;
92 (*. TODO push return-value cs' into solve and rename solve->loc_solve?_? .*)
93 (* val (m, pos) = ((mI,m), ip);
94 val (m,(pt,pos) ) = ((mI,m), ptp);
96 fun loc_solve_ m (pt,pos) =
97 let val (msg, cs') = solve m (pt, pos);
98 (* val (tacis,dels,(pt',p')) = cs';
99 (tracing o istate2str) (get_istate pt' p');
100 (term2str o fst) (get_obj g_result pt' (fst p'));
109 | Nexts of calcstate; (**)
111 (*. locate a tactic in a script and apply it if possible .*)
112 (*report applicability of tac in tacis; pt is dropped in setNextTactic*)
113 fun locatetac _ (ptp as (_,([],Res))) = ("end-of-calculation", ([], [], ptp))
114 | locatetac tac (ptp as (pt, p)) =
115 let val (mI,m) = mk_tac'_ tac;
116 in case applicable_in p pt m of
117 Notappl e => ("not-applicable", ([],[], ptp):calcstate')
120 val x = if member op = specsteps mI
121 then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
123 ERror e => ("failure", ([], [], ptp))
124 (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
125 | UNsafe cs' => ("unsafe-ok", cs')
126 | Updated (cs' as (_,_,(_,p'))) => (*ev.SEVER.tacs like Begin_Trans*)
127 (if p' = ([],Res) then "end-of-calculation" else "ok", cs')
128 (*for SEVER.tacs user to ask ? *)
132 (*iterated by nxt_me; there (the resulting) ptp dropped
133 may call nxt_solve Apply_Method --- thus evaluated here after solve.sml*)
134 fun nxt_specify_ (ptp as (pt, pos as (p,p_))) =
135 let val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
136 probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
138 if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
141 ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
142 | _ => nxt_specif Model_Problem (pt, (p,Pbl))
145 val cpI = if pI = e_pblID then pI' else pI;
146 val cmI = if mI = e_metID then mI' else mI;
147 val {ppc, prls, where_, ...} = get_pbt cpI;
148 val pre = check_preconds "thy 100820" prls where_ probl;
149 val pb = foldl and_ (true, map fst pre);
150 (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
151 val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth)
152 (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
155 nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
156 | _ => nxt_specif tac ptp end
159 (*.specify a new method;
160 WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' .*)
161 fun set_method (mI:metID) ptp =
162 let val ([(_, Specify_Method' (_, _, mits), _)], [], (pt, pos as (p,_))) =
163 nxt_specif (Specify_Method mI) ptp
164 val pre = [] (*...from Specify_Method'*)
165 val complete = true (*...from Specify_Method'*)
166 (*from Specify_Method' ? vvv, vvv ?*)
167 val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
168 in (pt, (complete, Met, hdf, mits, pre, spec):ocalhd) end;
170 (*.specify a new problem;
171 WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' .*)
172 fun set_problem pI (ptp: ptree * pos') =
173 let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)],
174 _, (pt, pos as (p,_))) = nxt_specif (Specify_Problem pI) ptp
175 (*from Specify_Problem' ? vvv, vvv ?*)
176 val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
177 in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end;
179 fun set_theory (tI:thyID) (ptp: ptree * pos') =
180 let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)],
181 _, (pt, pos as (p,_))) = nxt_specif (Specify_Theory tI) ptp
182 (*from Specify_Theory' ? vvv, vvv ?*)
183 val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
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
191 (* val (ip as (_,p_), (ptp as (pt,p), tacis)) = (get_pos 1 1, get_calc 1);
192 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (pos, cs);
193 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[]));
194 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs);
196 fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =
197 let val pIopt = get_pblID (pt,ip);
199 if (*p = ([],Res) orelse*) ip = ([],Res)
200 then ("end-of-calculation",(tacis, [], ptp):calcstate')
204 if ip = p (*the request is done where ptp waits for*)
206 let val (pt',c',p') = generate tacis (pt,[],p)
207 in ("ok", (tacis, c', (pt', p'))) end
208 else (case (if member op = [Pbl,Met] p_
209 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
210 handle _ => ([],[],ptp)(*e.g. Add_Given "equality///"*) of
211 cs as ([],_,_) => ("helpless", cs)
213 | _ => (case pIopt of
214 NONE => ("no-fmz-spec", ([], [], ptp))
216 (case (if member op = [Pbl,Met] p_
217 andalso is_none (get_obj g_env pt (fst p))
218 (*^^^^^^^^: Apply_Method without init_form*)
219 then nxt_specify_ (pt,ip)
220 else nxt_solve_ (pt,ip) )
221 handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality///"*) of
222 cs as ([],_,_) =>("helpless", cs)(*FIXXMEdel.handle*)
226 (* (nxt_solve_ (pt,ip)) handle e => print_exn e ;
233 (*.does several steps within one calculation as given by "type auto";
234 the steps may arbitrarily go into and leave different phases,
235 i.e. specify-phase and solve-phase.*)
236 (*TODO.WN0512 ? redesign after the phases have been more separated
237 at the fron-end in 05:
238 eg. CompleteCalcHead could be done by a separate fun !!!*)
239 (* val (ip, cs as (ptp as (pt,p),tacis)) = (get_pos cI 1, get_calc cI);
240 val (ip, cs as (ptp as (pt,p),tacis)) = (pold, get_calc cI);
241 val (c, ip, cs as (ptp as (_,p),tacis), Step s) =
242 ([]:pos' list, pold, get_calc cI, auto);
244 fun autocalc c ip (cs as (ptp as (_,p),tacis)) (Step s) =
246 then let val (str, (_, c', ptp)) = step ip cs;(*1*)
247 (*at least does 1 step, ev.1 too much*)
248 in (str, c@c', ptp) end
249 else let val (str, (_, c', ptp as (_, p))) = step ip cs;
251 then autocalc (c@c') p (ptp,[]) (Step (s-1))
252 else (str, c@c', ptp) end
253 (*handles autoord <= 3, autoord > 3 handled by all_/complete_solve*)
254 | autocalc c (pos as (_,p_)) ((pt,_), _(*tacis would help 1x in solve*))auto=
255 (* val (c:pos' list, (pos as (_,p_)),((pt,_),_),auto) =
256 ([], pold, get_calc cI, auto);
258 if autoord auto > 3 andalso just_created (pt, pos)
259 then let val ptp = all_modspec (pt, pos);
260 in all_solve auto c ptp end
262 if member op = [Pbl, Met] p_
263 then if not (is_complete_mod (pt, pos))
264 then let val ptp = complete_mod (pt, pos)
265 in if autoord auto < 3 then ("ok", c, ptp)
267 if not (is_complete_spec ptp)
268 then let val ptp = complete_spec ptp
269 in if autoord auto = 3 then ("ok", c, ptp)
270 else all_solve auto c ptp
272 else if autoord auto = 3 then ("ok", c, ptp)
273 else all_solve auto c ptp
276 if not (is_complete_spec (pt,pos))
277 then let val ptp = complete_spec (pt, pos)
278 in if autoord auto = 3 then ("ok", c, ptp)
279 else all_solve auto c ptp
281 else if autoord auto = 3 then ("ok", c, (pt, pos))
282 else all_solve auto c (pt, pos)
283 else complete_solve auto c (pt, pos);
284 (* val pbl = get_obj g_pbl (fst ptp) [];
285 val (oris,_,_) = get_obj g_origin (fst ptp) [];
292 (*.initialiye matching; before 'tryMatch' get the pblID to match with:
293 if no pbl has been specified, take the init from origin.*)
294 (*fun initmatch pt (pos as (p,_):pos') =
295 let val PblObj {probl,origin=(os,(_,pI,_),_),spec=(dI',pI',mI'),...} =
297 val pblID = if pI' = e_pblID
298 then (*TODO.WN051125 (#init o get_pbt) pI <<<*)
299 takelast (2, pI) (*FIXME.WN051125 a hack, impl.^^^*)
301 val spec = (dI',pblID,mI')
302 val {ppc,where_,prls,...} = get_pbt pblID
303 val (model_ok, (pbl, pre)) =
304 match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
305 in ModSpec (ocalhd_complete pbl pre spec,
306 Pbl, e_term, pbl, pre, spec) end;*)
307 fun initcontext_pbl pt (pos as (p,_):pos') =
308 let val PblObj {probl,origin=(os,(_,pI,_),hdl),spec=(dI',pI',mI'),...} =
310 val pblID = if pI' = e_pblID
311 then (*TODO.WN051125 (#init o get_pbt) pI <<<*)
312 takelast (2, pI) (*FIXME.WN051125 a hack, impl.^^^*)
314 val {ppc,where_,prls,...} = get_pbt pblID
315 val (model_ok, (pbl, pre)) =
316 match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
317 in (model_ok, pblID, hdl, pbl, pre) end;
319 fun initcontext_met pt (pos as (p,_):pos') =
320 let val PblObj {meth,origin=(os,(_,_,mI), _),spec=(_, _, mI'),...} =
322 val metID = if mI' = e_metID
323 then (*TODO.WN051125 (#init o get_pbt) pI <<<*)
324 takelast (2, mI) (*FIXME.WN051125 a hack, impl.^^^*)
326 val {ppc,pre,prls,scr,...} = get_met metID
327 val (model_ok, (pbl, pre)) =
328 match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
329 in (model_ok, metID, scr, pbl, pre) end;
331 (*.match the model of a problem at pos p
332 with the model-pattern of the problem with pblID*)
333 fun context_pbl pI pt (p:pos) =
334 let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p
335 val {ppc,where_,prls,...} = get_pbt pI
336 val (model_ok, (pbl, pre)) =
337 match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
338 in (model_ok, pI, hdl, pbl, pre) end;
340 fun context_met mI pt (p:pos) =
341 let val PblObj {meth,origin=(os,_,hdl),...} = get_obj I pt p
342 val {ppc,pre,prls,scr,...} = get_met mI
343 val (model_ok, (pbl, pre)) =
344 match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
345 in (model_ok, mI, scr, pbl, pre) end
348 (* val (pI, pt, pos as (p,_)) = (pblID, pt, p);
350 fun tryrefine pI pt (pos as (p,_):pos') =
351 let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p
352 in case refine_pbl (assoc_thy "Isac") pI probl of
353 NONE => (*copy from context_pbl*)
354 let val {ppc,where_,prls,...} = get_pbt pI
355 val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac")
356 probl (ppc,where_,prls) os
357 in (false, pI, hdl, pbl, pre) end
358 | SOME (pI, (pbl, pre)) =>
359 (true, pI, hdl, pbl, pre)
362 (* val (pt, (pos as (p,p_):pos')) = (pt, ip);
364 fun detailstep pt (pos as (p,p_):pos') =
365 let val nd = get_nd pt p
368 then if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)]
369 then detailrls pt pos
370 else ("no-Rewrite_Set...", EmptyPtree, e_pos')
371 else ("donesteps", pt(*, get_formress [] ((lev_on o lev_dn) p) cn*),
372 (p @ [length (children (get_nd pt p))], Res) )
377 (***. for mathematics authoring on sml-toplevel; no XML .***)
380 (* val sp = (dI',pI',mI');
383 (*15.8.03 for me with loc_specify/solve, nxt_specify/solve
384 delete as soon as TESTg_form -> _mout_ dropped*)
388 let val (form,_,_) = pt_extract ptp
390 Form t => Form' (FormKF (~1,EdUndef,0,Nundef,term2str t))
391 | ModSpec (_,p_, head, gfr, pre, _) =>
392 Form' (PpcKF (0,EdUndef,0,Nundef,
393 (case p_ of Pbl => Problem[] | Met => Method[],
394 itms2itemppc (assoc_thy"Isac") gfr pre)))
397 (*.create a calc-tree; for use within sml: thus ^^^ NOT decoded to ^;
398 compare "fun CalcTree" which DOES decode.*)
399 fun CalcTreeTEST [(fmz, sp):fmz] =
400 (* val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))];
401 val [(fmz, sp):fmz] = [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
403 let val cs as ((pt,p), tacis) = nxt_specify_init_calc (fmz, sp)
404 val tac = case tacis of [] => Empty_Tac | _ => (#1 o hd) tacis
405 val f = TESTg_form (pt,p)
406 in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end;
408 (*for tests > 15.8.03 after separation setnexttactic / nextTac:
409 external view: me should be used by math-authors as done so far
410 internal view: loc_specify/solve, nxt_specify/solve used
411 i.e. same as in setnexttactic / nextTac*)
412 (*ENDE TESTPHASE 08/10.03:
413 NEW loeschen, eigene Version von locatetac, step
414 meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *)
416 (* val ((_,tac), p, _, pt) = (nxt, p, c, pt);
418 fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) =
421 (*locatetac is here for testing by me; step would suffice in me*)
422 case locatetac tac (pt,p) of
423 ("ok", (_, _, ptp)) => ptp
424 | ("unsafe-ok", (_, _, ptp)) => ptp
425 | ("not-applicable",_) => (pt, p)
426 | ("end-of-calculation", (_, _, ptp)) => ptp
427 | ("failure",_) => error "sys-error";
428 val (_, ts) = (*WN101102 NOT tested, if step would create _same_ ptp*)
429 (case step p ((pt, e_pos'),[]) of
430 ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)
431 | ("helpless",_) => ("helpless: cannot propose tac", [])
432 | ("no-fmz-spec",_) => error "no-fmz-spec"
433 | ("end-of-calculation", (ts, _, _)) => ("",ts))
434 handle _ => error "sys-error";
437 tacis as (_::_) => let val (tac,_,_) = last_elem tacis in tac end
438 | _ => if p = ([],Res) then End_Proof' else Empty_Tac;
439 (*form output comes from locatetac*)
440 in (p:pos', []:NEW, TESTg_form (pt, p),
441 (tac2IDstr tac, tac):tac'_, Sundef, pt) end;
443 (*for quick test-print-out, until 'type inout' is removed*)
444 fun f2str (Form' (FormKF (_, _, _, _, cterm'))) = cterm';
448 (*------------------------------------------------------------------(**)
451 (**)------------------------------------------------------------------*)