1 (* The _functional_ mathematics engine, ie. without a state.
2 Input and output are Isabelle's formulae as strings.
3 (c) Walther Neuper 2000
6 use"ME/mathengine.sml";
10 signature MATHENGINE =
13 (* datatype nxt_ = HElpless | Nexts of CalcHead.calcstate *)
19 | UNsafe of CalcHead.calcstate'
20 | Updated of CalcHead.calcstate' *)
24 pos' * NEW * mout * (string * tac) * safe * ptree
26 val TESTg_form : ptree * (int list * pos_) -> mout
30 (ptree * pos') * taci list ->
31 auto -> string * pos' list * (ptree * pos')
32 val detailstep : ptree -> pos' -> string * ptree * pos'
33 (* val e_tac_ : tac_ *)
34 val f2str : mout -> cterm'
35 (* val get_pblID : ptree * pos' -> pblID Library.option *)
36 val initmatch : ptree -> pos' -> ptform
38 string * tac_ -> ptree * (int list * pos_) -> lOc_ *)
39 (* val loc_specify_ : tac_ -> ptree * pos' -> lOc_ *)
40 val locatetac : (*tests only*)
42 ptree * (posel list * pos_) ->
43 string * (taci list * pos' list * (ptree * (posel list * pos_)))
48 ptree -> pos' * NEW * mout * tac'_ * safe * ptree
50 val nxt_specify_ : ptree * (int list * pos_) -> calcstate'(*tests only*)
51 val set_method : metID -> ptree * pos' -> ptree * ocalhd
52 val set_problem : pblID -> ptree * pos' -> ptree * ocalhd
53 val set_theory : thyID -> ptree * pos' -> ptree * ocalhd
54 val step : pos' -> calcstate -> string * calcstate'
55 val trymatch : pblID -> ptree -> pos' -> ptform
56 val tryrefine : pblID -> ptree -> pos' -> ptform
61 (*------------------------------------------------------------------*)
62 structure MathEngine : MATHENGINE =
64 (*------------------------------------------------------------------*)
66 fun get_pblID (pt, (p,_):pos') =
67 let val p' = par_pblobj pt p
68 val (_,pI,_) = get_obj g_spec pt p'
69 val (_,(_,oI,_),_) = get_obj g_origin pt p'
70 in if pI <> e_pblID then Some pI
71 else if oI <> e_pblID then Some oI
73 (*fun get_pblID (pt, (p,_):pos') =
74 ((snd3 o (get_obj g_spec pt)) (par_pblobj pt p));*)
77 (*----------------------vvv--------------------dummies for test*)
78 val e_tac_ = Tac_ (Pure.thy,"","","");
80 ERror of string (*after loc_specify, loc_solve*)
81 | UNsafe of calcstate' (*after loc_specify, loc_solve*)
82 | Updated of calcstate'; (*after loc_specify, loc_solve*)
83 fun loc_specify_ m (pt,pos) =
86 let val (p,_,f,_,s,pt) = specify m pos [] pt;
87 (* val (_,_,_,_,_,pt')= specify m pos [] pt;
90 (Error' (Error_ e)) => ERror e
91 | _ => Updated ([], [], (pt,p)) end;
93 fun loc_solve_ m (pt,pos) =
94 (* val (m, pos) = ((mI,m), ip);
95 val (m,(pt,pos) ) = ((mI,m), ptp);
97 let val (msg, cs') = solve m (pt, pos);
98 (* val (tacis,dels,(pt',p')) = cs';
99 (writeln o istate2str) (get_istate pt' p');
100 (term2str o fst) (get_obj g_result pt' (fst p'));
109 | Nexts of calcstate; (**)
111 (*report applicability of tac in tacis; pt is dropped in setNextTactic*)
112 fun locatetac _ (ptp as (_,([],Res))) = ("end-of-calculation", ([], [], ptp))
113 | locatetac tac (ptp as (pt, p)) =
114 (* val ptp as (pt, p) = (pt, ip);
115 val ptp as (pt, p) = (pt, p);
117 let val (mI,m) = mk_tac'_ tac;
118 in case applicable_in p pt m of
119 Notappl e => ("not-applicable", ([],[], ptp):calcstate')
121 (* val Appl m = applicable_in p pt m;
123 let val x = if mI mem specsteps
124 then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
126 ERror e => ("failure", ([], [], ptp))
127 (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
128 | UNsafe cs' => ("unsafe-ok", cs')
129 | Updated (cs' as (_,_,(_,p'))) =>
130 (*ev.SEVER.tacs like Begin_Trans*)
131 (if p' = ([],Res) then "end-of-calculation" else "ok",
132 cs')(*for -"- user to ask ? *)
137 (*------------------------------------------------------------------
138 fun init_detail ptp = e_calcstate;(*15.8.03.MISSING-->solve.sml!?*)
139 (*----------------------------------------------------from solve.sml*)
140 | nxt_solv (Detail_Set'(thy', rls, t)) (pt, p) =
141 let (*val rls = the (assoc(!ruleset',rls'))
142 handle _ => raise error ("solve: '"^rls'^"' not known");*)
143 val thy = assoc_thy thy';
146 Rrls {scr=sc as Rfuns {init_state=ii,...},...} =>
147 (e_rls, sc, RrlsState (ii t))
148 | Rls {srls=srls,scr=sc as Script s,...} =>
149 (srls, sc, ScrState ([(one_scr_arg s,t)], [],
150 None, e_term, Sundef, true));
151 val pt = update_tac pt (fst p) (Detail_Set (id_rls rls));
152 val (p,cid,_,pt) = generate1 thy (Begin_Trans' t) is p pt;
153 val nx = (tac_2tac o fst3) (next_tac (thy',srls) (pt,p) sc is);
154 val aopt = applicable_in p pt nx;
156 Notappl s => raise error ("solve Detail_Set: "^s)
157 (* val Appl m = aopt;
159 | Appl m => solve ("discardFIXME",m) p pt end
160 ------------------------------------------------------------------*)
163 (*iterated by nxt_me; there (the resulting) ptp dropped
164 may call nxt_solve Apply_Method --- thus evaluated here after solve.sml*)
165 fun nxt_specify_ (ptp as (pt, pos as (p,p_))) =
166 (* val (ptp as (pt, pos as (p,p_))) = ptp;
167 val (ptp as (pt, pos as (p,p_))) = (pt,ip);
169 let val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
170 probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
171 in if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
173 ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p,Pbl))
174 | _ => nxt_specif Model_Problem (pt, (p,Pbl))
175 else let val cpI = if pI = e_pblID then pI' else pI;
176 val cmI = if mI = e_metID then mI' else mI;
177 val {ppc,prls,where_,...} = get_pbt cpI;
178 val pre = check_preconds thy prls where_ probl;
179 val pb = foldl and_ (true, map fst pre);
180 (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
182 nxt_spec p_ pb oris (dI',pI',mI') (probl,meth)
183 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
186 (* val Apply_Method mI = tac;
188 nxt_solv (Apply_Method' (mI, None, e_istate)) e_istate ptp
189 | _ => nxt_specif tac ptp end
193 (*.specify a new method;
194 WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' .*)
195 fun set_method (mI:metID) ptp =
196 let val ([(_, Specify_Method' (_, _, mits), _)], [], (pt, pos as (p,_))) =
197 nxt_specif (Specify_Method mI) ptp
198 val pre = [] (*...from Specify_Method'*)
199 val complete = true (*...from Specify_Method'*)
200 (*from Specify_Method' ? vvv, vvv ?*)
201 val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
202 in (pt, (complete, Met, hdf, mits, pre, spec):ocalhd) end;
204 (* val ([(_, Specify_Method' (_, _, mits), _)], [],_) =
205 nxt_specif (Specify_Method mI) ptp;
208 (*.specify a new problem;
209 WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' .*)
210 fun set_problem pI (ptp: ptree * pos') =
211 let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)],
212 _, (pt, pos as (p,_))) = nxt_specif (Specify_Problem pI) ptp
213 (*from Specify_Problem' ? vvv, vvv ?*)
214 val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
215 in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end;
217 fun set_theory (tI:thyID) (ptp: ptree * pos') =
218 let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)],
219 _, (pt, pos as (p,_))) = nxt_specif (Specify_Theory tI) ptp
220 (*from Specify_Theory' ? vvv, vvv ?*)
221 val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
222 in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end;
224 (*.does a step forward; returns tactic used, ctree updated.
225 TODO.WN0512 redesign after specify-phase became more separated from solve-phase
229 (* val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs);
230 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[]));
231 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (get_pos 1 1, get_calc 1);
233 fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =
234 let val pIopt = get_pblID (pt,ip);
235 in if p = ([],Res) orelse ip = ([],Res)
236 then ("end-of-calculation",(tacis, [], ptp):calcstate') else
239 (* val((tac,_,_)::_) = tacis;
241 if ip = p (*the request is done where ptp waits for*)
242 then let val (pt',c',p') = generate tacis (pt,[],p)
243 in ("ok", (tacis, c', (pt', p'))) end
244 else (case (if p_ mem [Pbl,Met]
245 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
246 handle _ => ([],[],ptp)(*e.g.by Add_Given "equality///"*)
247 of cs as ([],_,_) => ("helpless", cs)
249 | _ => (case pIopt of
250 None => ("no-fmz-spec", ([], [], ptp))
252 (* val Some pI = pIopt;
253 val cs = (if p_ mem [Pbl,Met] andalso is_none (get_obj g_env pt (fst p))
254 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
255 handle _ => ([], ptp);
257 (case (if p_ mem [Pbl,Met]
258 andalso is_none (get_obj g_env pt (fst p))
259 (*^^^^^^^^: Apply_Method without init_form*)
260 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip) )
261 handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality/"*)
262 of cs as ([],_,_) =>("helpless", cs)(*FIXXMEdel.handle*)
266 (* (nxt_solve_ (pt,ip)) handle e => print_exn e ;
270 (*.does several steps within one calculation as given by "type auto";
271 the steps may arbitrarily go into and leave different phases,
272 i.e. specify-phase and solve-phase.*)
273 (*TODO.WN0512 ? redesign after the phases have been more separated
274 at the fron-end in 05:
275 eg. CompleteCalcHead could be done by a separate fun !!!*)
276 (* val (ip, cs as (ptp as (pt,p),tacis)) = (get_pos cI 1, get_calc cI);
278 val (c, ip, cs as (ptp as (_,p),tacis), Step s) =
279 ([]:pos' list, pold, get_calc cI, auto);
281 fun autocalc c ip (cs as (ptp as (_,p),tacis)) (Step s) =
283 then let val (str, (_, c', ptp)) = step ip cs;(*1*)
284 (*at least does 1 step, ev.1 too much*)
285 in (str, c@c', ptp) end
286 else let val (str, (_, c', ptp as (_, p))) = step ip cs;
288 then autocalc (c@c') p (ptp,[]) (Step (s-1))
289 else (str, c@c', ptp) end
290 (*handles autoord <= 3, autoord > 3 handled by all_/complete_solve*)
291 | autocalc c (pos as (_,p_)) ((pt,_), _(*tacis would help 1x in solve*))auto=
292 (* val (c:pos' list, (pos as (_,p_)),((pt,_),_),auto) =
293 ([], pold, get_calc cI, auto);
295 if autoord auto > 3 andalso just_created (pt, pos)
296 then let val ptp = all_modspec (pt, pos);
297 in all_solve auto c ptp end
300 then if not (is_complete_mod (pt, pos))
301 then let val ptp = complete_mod (pt, pos)
302 in if autoord auto < 3 then ("ok", c, ptp)
304 if not (is_complete_spec ptp)
305 then let val ptp = complete_spec ptp
306 in if autoord auto = 3 then ("ok", c, ptp)
307 else all_solve auto c ptp
309 else if autoord auto = 3 then ("ok", c, ptp)
310 else all_solve auto c ptp
313 if not (is_complete_spec (pt,pos))
314 then let val ptp = complete_spec (pt, pos)
315 in if autoord auto = 3 then ("ok", c, ptp)
316 else all_solve auto c ptp
318 else if autoord auto = 3 then ("ok", c, (pt, pos))
319 else all_solve auto c (pt, pos)
320 else complete_solve auto c (pt, pos);
321 (* val pbl = get_obj g_pbl (fst ptp) [];
322 val (oris,_,_) = get_obj g_origin (fst ptp) [];
329 (*.initialiye matching; before 'tryMatch' get the pblID to match with:
330 if no pbl has been specified, take the init from origin.*)
331 fun initmatch pt (pos as (p,_):pos') =
332 let val PblObj {probl,origin=(os,(_,pI,_),_),spec=(dI',pI',mI'),...} =
334 val pblID = if pI' = e_pblID
335 then (*TODO.WN051125 (#init o get_pbt) pI <<<*)
336 takelast (2, pI) (*FIXME.WN051125 a hack, impl.^^^*)
338 val spec = (dI',pblID,mI')
339 val {ppc,where_,prls,...} = get_pbt pblID
340 val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac.thy") probl
342 in ModSpec (ocalhd_complete pbl pre spec,
343 Pbl, e_term, pbl, pre, spec) end;
345 (*.match the model of a problem at pos p
346 with the model-pattern of the problem with pblID*)
347 fun trymatch pI pt (pos as (p,_):pos') =
348 let val PblObj {probl,origin=(os,_,_),spec=(dI,_,mI),...} = get_obj I pt p
349 val spec = (dI,pI,mI)
350 val {ppc,where_,prls,...} = get_pbt pI
351 val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac.thy") probl
353 in ModSpec (ocalhd_complete pbl pre spec,
354 Pbl, e_term, pbl, pre, spec) end;
356 fun tryrefine pI pt (pos as (p,_):pos') =
357 let val PblObj {probl,origin=(os,_,_),spec=(dI,_,mI),...} = get_obj I pt p
358 in case refine_pbl (assoc_thy "Isac.thy") pI probl of
359 None => (*copy from trymatch*)
360 let val {ppc,where_,prls,...} = get_pbt pI
361 val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac.thy")
362 probl (ppc,where_,prls) os
363 in ModSpec (ocalhd_complete pbl pre (dI,pI,mI),
364 Pbl, e_term, pbl, pre, (dI,pI,mI)) end
365 | Some (pI, (pbl, pre)) =>
366 ModSpec (ocalhd_complete pbl pre (dI,pI,mI),
367 Pbl, e_term, pbl, pre, (dI,pI,mI))
370 (* val pos as (p,p_) = ip;
371 val (pt, (pos as (p,p_):pos')) = (pt, ip);
373 fun detailstep pt (pos as (p,p_):pos') =
374 let val nd = get_nd pt p
376 in if null cn andalso (is_rewset o (get_obj g_tac nd)) [] (*subnode!*)
377 then detailrls pt pos
378 else ("donesteps", pt(*, get_formress [] ((lev_on o lev_dn) p) cn*),
379 (p @ [length (children (get_nd pt p))], Res) )
384 (***. for mathematics authoring on sml-toplevel; no XML .***)
387 (* val sp = (dI',pI',mI');
390 (*15.8.03 for me with loc_specify/solve, nxt_specify/solve
391 delete as soon as TESTg_form -> _mout_ dropped*)
395 let val (form,_,_) = pt_extract ptp
397 Form t => Form' (FormKF (~1,EdUndef,0,Nundef,term2str t))
398 | ModSpec (_,p_, head, gfr, pre, _) =>
399 Form' (PpcKF (0,EdUndef,0,Nundef,
400 (case p_ of Pbl => Problem[] | Met => Method[],
401 itms2itemppc (assoc_thy"Isac.thy") gfr pre)))
404 (*.create a calc-tree; for use within sml: thus ^^^ NOT decoded to ^;
405 compare "fun CalcTree" which DOES decode.*)
406 fun CalcTreeTEST [(fmz, sp):fmz] =
407 (* val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))];
408 val [(fmz, sp):fmz] = [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
410 let val cs as ((pt,p), tacis) = nxt_specify_init_calc (fmz, sp)
411 val tac = case tacis of [] => Empty_Tac | _ => (#1 o hd) tacis
412 val f = TESTg_form (pt,p)
413 in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end;
415 (*for tests > 15.8.03 after separation setnexttactic / nextTac:
416 external view: me should be used by math-authors as done so far
417 internal view: loc_specify/solve, nxt_specify/solve used
418 i.e. same as in setnexttactic / nextTac*)
419 (*ENDE TESTPHASE 08/10.03:
420 NEW loeschen, eigene Version von locatetac, step
421 meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *)
424 fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) =
425 (* val (_,tac) = nxt;
427 (* val (msg, (tacis, pos's, (pt',p'))) = locatetac tac (pt,p);
428 f2str (TESTg_form (pt', p'));
429 (writeln o (itms2str thy)) (get_obj g_pbl pt' (fst p'));
430 writeln( istate2str (get_istate pt' ([3],Res)));
431 term2str (fst (get_obj g_result pt' [3]));
432 val (pt,p) = (pt',p');
434 (*locatetac is here for testing by me; step would suffice in me*)
435 case locatetac tac (pt,p) of
436 ("ok", (_, _, ptp)) => ptp
437 | ("unsafe-ok", (_, _, ptp)) => ptp
438 | ("not-applicable",_) => (pt, p)
439 | ("end-of-calculation", (_, _, ptp)) => ptp
440 | ("failure",_) => raise error "sys-error";
442 (* val (eee, (ts, _, (pt'',_))) = step p ((pt, e_pos'),[]);
444 (case step p ((pt, e_pos'),[]) of
445 ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)
446 | ("helpless",_) => ("helpless: cannot propose tac", [])
447 | ("no-fmz-spec",_) => raise error "no-fmz-spec"
448 | ("end-of-calculation", (ts, _, _)) => ("",ts))
449 handle _ => raise error "sys-error";
450 val tac = case ts of tacis as (_::_) =>
451 let val (tac,_,_) = last_elem tacis
453 | _ => if p = ([],Res) then End_Proof'
455 (*form output comes from locatetac*)
456 in(p:pos',[]:NEW, TESTg_form (pt, p),
457 (tac2IDstr tac, tac):tac'_, Sundef, pt) end;
459 (*for quick test-print-out, until 'type inout' is removed*)
460 fun f2str (Form' (FormKF (_, _, _, _, cterm'))) = cterm';
464 (*------------------------------------------------------------------*)
467 (*------------------------------------------------------------------*)