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"~/proto2/isac/src/sml/ME/mathengine.sml";
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 get_pblID : ptree * pos' -> pblID Library.option *)
36 string * tac_ -> ptree * (int list * pos_) -> lOc_ *)
37 (* val loc_specify_ : tac_ -> ptree * pos' -> lOc_ *)
38 val locatetac : (*tests only*)
40 ptree * (posel list * pos_) ->
41 string * (taci list * pos' list * (ptree * (posel list * pos_)))
46 ptree -> pos' * NEW * mout * tac'_ * safe * ptree
48 val nxt_specify_ : ptree * (int list * pos_) -> CalcHead.calcstate'
49 val step : pos' -> CalcHead.calcstate -> string * CalcHead.calcstate'
50 val trymatch : pblID -> ptree -> int list * 'a -> ptform
51 val tryrefine : pblID -> ptree -> int list * 'a -> ptform
57 structure mathengine : MATHENGINE =
60 fun get_pblID (pt, (p,_):pos') =
61 let val p' = par_pblobj pt p
62 val (_,pI,_) = get_obj g_spec pt p'
63 val (_,(_,oI,_),_) = get_obj g_origin pt p'
64 in if pI <> e_pblID then Some pI
65 else if oI <> e_pblID then Some oI
67 (*fun get_pblID (pt, (p,_):pos') =
68 ((snd3 o (get_obj g_spec pt)) (par_pblobj pt p));*)
71 (*----------------------vvv--------------------dummies for test*)
72 val e_tac_ = Tac_ (Pure.thy,"","","");
74 ERror of string (*after loc_specify, loc_solve*)
75 | UNsafe of calcstate' (*after loc_specify, loc_solve*)
76 | Updated of calcstate'; (*after loc_specify, loc_solve*)
77 fun loc_specify_ m (pt,pos) =
80 let val (p,_,f,_,s,pt) = specify m pos [] pt;
81 (* val (_,_,_,_,_,pt')= specify m pos [] pt;
84 (Error' (Error_ e)) => ERror e
85 | _ => Updated ([], [], (pt,p)) end;
87 fun loc_solve_ m (pt,pos) =
88 (* val (m, pos) = ((mI,m), ip);
89 val (m,(pt,pos) ) = ((mI,m), ptp);
91 let val (msg, cs') = solve m (pt, pos);
92 (* val (tacis,dels,(pt',p')) = cs';
93 (writeln o istate2str) (get_istate pt' p');
94 (term2str o fst) (get_obj g_result pt' (fst p'));
103 | Nexts of calcstate; (**)
105 (*report applicability of tac in tacis; pt is dropped in setNextTactic*)
106 fun locatetac _ (ptp as (_,([],Res))) = ("end-of-calculation", ([], [], ptp))
107 | locatetac tac (ptp as (pt, p)) =
108 (* val ptp as (pt, p) = (pt, ip);
109 val ptp as (pt, p) = (pt, p);
111 let val (mI,m) = mk_tac'_ tac;
112 in case applicable_in p pt m of
113 Notappl e => ("not-applicable", ([],[], ptp):calcstate')
115 (* val Appl m = applicable_in p pt m;
117 let val x = if mI mem specsteps
118 then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
120 ERror e => ("failure", ([], [], ptp))
121 (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
122 | UNsafe cs' => ("unsafe-ok", cs')
123 | Updated (cs' as (_,_,(_,p'))) =>
124 (*ev.SEVER.tacs like Begin_Trans*)
125 (if p' = ([],Res) then "end-of-calculation" else "ok",
126 cs')(*for -"- user to ask ? *)
131 (*------------------------------------------------------------------
132 fun init_detail ptp = e_calcstate;(*15.8.03.MISSING-->solve.sml!?*)
133 (*----------------------------------------------------from solve.sml*)
134 | nxt_solv (Detail_Set'(thy', rls, t)) (pt, p) =
135 let (*val rls = the (assoc(!ruleset',rls'))
136 handle _ => raise error ("solve: '"^rls'^"' not known");*)
137 val thy = assoc_thy thy';
140 Rrls {scr=sc as Rfuns {init_state=ii,...},...} =>
141 (e_rls, sc, RrlsState (ii t))
142 | Rls {srls=srls,scr=sc as Script s,...} =>
143 (srls, sc, ScrState ([(one_scr_arg s,t)], [],
144 None, e_term, Sundef, true));
145 val pt = update_tac pt (fst p) (Detail_Set (id_rls rls));
146 val (p,cid,_,pt) = generate1 thy (Begin_Trans' t) is p pt;
147 val nx = (tac_2tac o fst3) (next_tac (thy',srls) (pt,p) sc is);
148 val aopt = applicable_in p pt nx;
150 Notappl s => raise error ("solve Detail_Set: "^s)
151 (* val Appl m = aopt;
153 | Appl m => solve ("discardFIXME",m) p pt end
154 ------------------------------------------------------------------*)
157 (*iterated by nxt_me; there (the resulting) ptp dropped
158 may call nxt_solve Apply_Method --- thus evaluated here after solve.sml*)
159 fun nxt_specify_ (ptp as (pt, pos as (p,p_))) =
160 (* val (ptp as (pt, pos as (p,p_))) = ptp;
161 val (ptp as (pt, pos as (p,p_))) = (pt,ip);
163 let val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
164 probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
165 in if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
167 ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p,Pbl))
168 | _ => nxt_specif (Model_Problem pI') (pt, (p,Pbl))
169 else let val cpI = if pI = e_pblID then pI' else pI;
170 val cmI = if mI = e_metID then mI' else mI;
171 val {ppc,prls,where_,...} = get_pbt cpI;
172 val pre = check_preconds thy prls where_ probl;
173 val pb = foldl and_ (true, map fst pre);
174 (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
176 nxt_spec p_ pb oris (dI',pI',mI') (probl,meth)
177 (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
180 (* val Apply_Method mI = tac;
182 nxt_solv (Apply_Method' (mI, None, e_istate)) e_istate ptp
183 | _ => nxt_specif tac ptp end
187 (*WN11.9.03--- was only for hide, detail --> dialog ---------
191 -> (ptree * pos') * : always the latest ovewriting the others
192 (tac * tac_ * istate) list : new tacs found PREpended to others
193 -"- calcstate (typeinference doesn get it)
194 -> detail * detail ->
195 hid -> : handles packages of tacs (eg. modeling)
198 fun nxt_me _ _ _ Hmodel = raise error "nxt_me: not impl. for Hmodel"
199 | nxt_me _ _ _ Hspecify = raise error "nxt_me: not impl. for Hspecify"
200 | nxt_me _ _ _ Happly = raise error "nxt_me: not impl. for Happly"
201 (* val ((ptp as (_,(_,p_)), tacis), (hi, de)) = ((ptp, []), (hide, detail));
203 | nxt_me pI (ptp as (_,([],Res)), tacis) _ _ = Nexts (ptp, tacis)
204 | nxt_me pI ((ptp as (_,(_,p_)), tacis):calcstate) (hi, de) _(*Hundef,Htac*)=
205 (* val ((ptp as (_,(_,p_)), tacis), (hi, de)) = ((ptp, []), (hide, detail));
206 val ((ptp as (_,(_,p_)), [] ), (hi, de)) = ((ptp, []), (hide, detail));
208 let val x = (if p_ mem [Pbl,Met]
209 then nxt_specify_ ptp else nxt_solve_ ptp)
210 handle _ => (ptp, []) (*e.g. by Add_Given "equality"///*)
213 | (cs as (ptp, (tac,_,_)::_)) =>
214 let val (cs as (ptp, tacis' as (tac,_,_)::_)) =
215 if is_detail pI tac de then init_detail ptp else cs
216 in case is_hide pI tac hi of
217 Show => Nexts (ptp, tacis' @ tacis)
219 nxt_me pI (ptp, tacis' @ tacis) (hi, de) hid
222 ------------------------------------------------------------------*)
224 (*.does a step forward; returns tactic used, ctree updated
228 fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =
229 (* val (ip as (_,p_), (ptp as (pt,p), tacis)) = (get_pos 1 1, get_calc 1);
230 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs);
231 val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[]));
233 let val pIopt = get_pblID (pt,ip);
234 in if p = ([],Res) orelse ip = ([],Res)
235 then ("end-of-calculation",(tacis, [], ptp):calcstate') else
238 (* val((tac,_,_)::_) = tacis;
241 then let val (pt',c',p') = generate tacis (pt,[],p)
242 in ("ok", (tacis, c', (pt', p'))) end
243 else (case (if p_ mem [Pbl,Met]
244 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
245 handle _ => ([],[],ptp)(*e.g.by Add_Given "equality///"*)
246 of cs as ([],_,_) => ("helpless", cs)
248 | _ => (case pIopt of
249 None => ("no-fmz-spec", ([], [], ptp))
251 (* val Some pI = pIopt;
252 val cs = (if p_ mem [Pbl,Met] andalso is_none (get_obj g_env pt (fst p))
253 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
254 handle _ => ([], ptp);
256 (case (if p_ mem [Pbl,Met]
257 andalso is_none (get_obj g_env pt (fst p))
258 (*^^^^^^^^: Apply_Method without init_form*)
259 then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip) )
260 handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality/"*)
261 of cs as ([],_,_) => ("helpless", cs)
265 (* (nxt_solve_ (pt,ip)) handle e => print_exn e ;
269 (* is_complete_mod ptp;
270 is_complete_spec ptp;
271 get_obj g_form pt [1];
272 print_depth 11;pt;print_depth 3;
274 val (str, (_, (pt',p'))) = step ip cs;
275 get_obj g_form pt [1];
277 val (ip, cs as (ptp as (pt,p),tacis)) = (get_pos cI 1, get_calc cI);
279 val (c, ip, cs as (ptp as (_,p),tacis)) = ([]:pos' list, pold, get_calc cI);
282 fun autocalc c ip (cs as (ptp as (_,p),tacis)) (Step s) =
285 _::_ => (*if ip = p then ("ok", generate tacis ptp)##DONE IN step#
286 else*) let val (str, (_, c', ptp)) = step ip cs;(*1*)
287 (*at least does 1 step, ev.1 too much*)
288 in (str, c@c', ptp) end
289 | _ => let val (str, (_, c', ptp)) = step ip cs
290 in (str, c@c', ptp) end
292 _::_ => (*if ip = p then
293 let val ptp as (_, p) = generate tacis ptp
294 in autocalc p (ptp, []) (Step(s-1-(length tacis))) end
295 else*) let val (str, (_, c', ptp as (_, p))) = step ip cs;
297 then autocalc (c@c') p (ptp,[]) (Step(s-1))
298 else (str, c@c', ptp) end
299 | _ => let val (str, (_, c', ptp as (_, p))) = step ip cs;
301 then autocalc (c@c') p (ptp, []) (Step (s-1))
302 else (str, c@c', ptp) end)
303 (*handles autoord <= 3, autoord > 3 handled by all_/complete_solve*)
304 | autocalc c (pos as (_,p_)) ((pt,_), _(*tacis would help 1x in solve*))auto=
305 (* val (pos as (_,p_), ((pt,_), _)) = (get_pos cI 1, get_calc cI);
306 autocalc (get_pos cI 1) (get_calc cI) auto;
308 val (c:pos' list, (pos as (_,p_)),((pt,_),_),auto) =
309 ([], pold, get_calc cI, auto);
311 if autoord auto > 3 andalso just_created (pt, pos)
312 then let val ptp = all_modspec (pt, pos);
313 in all_solve auto c ptp end
316 then if not (is_complete_mod (pt, pos))
317 then let val ptp = complete_mod (pt, pos)
318 in if autoord auto < 3 then ("ok", c, ptp)
320 if not (is_complete_spec ptp)
321 then let val ptp = complete_spec ptp
322 in if autoord auto = 3 then ("ok", c, ptp)
323 else all_solve auto c ptp
325 else if autoord auto = 3 then ("ok", c, ptp)
326 else all_solve auto c ptp
329 if not (is_complete_spec (pt,pos))
330 then let val ptp = complete_spec (pt, pos)
331 in if autoord auto = 3 then ("ok", c, ptp)
332 else all_solve auto c ptp
334 else if autoord auto = 3 then ("ok", c, (pt, pos))
335 else all_solve auto c (pt, pos)
336 else complete_solve auto c (pt, pos);
337 (* val pbl = get_obj g_pbl (fst ptp) [];
338 val (oris,_,_) = get_obj g_origin (fst ptp) [];
345 fun trymatch pI pt (pos as (p,_)) =
346 let val PblObj {probl,origin=(os,_,_),spec=(dI,_,mI),...} = get_obj I pt p
347 val spec = (dI,pI,mI)
348 val {ppc,where_,prls,...} = get_pbt pI
349 val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac.thy") probl
351 in ModSpec (ocalhd_complete pbl pre spec,
352 Pbl, e_term, pbl, pre, spec) end;
354 fun tryrefine pI pt (pos as (p,_)) =
355 let val PblObj {probl,origin=(os,_,_),spec=(dI,_,mI),...} = get_obj I pt p
356 in case refine_pbl (assoc_thy "Isac.thy") pI probl of
357 None => (*copy from trymatch*)
358 let val {ppc,where_,prls,...} = get_pbt pI
359 val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac.thy")
360 probl (ppc,where_,prls) os
361 in ModSpec (ocalhd_complete pbl pre (dI,pI,mI),
362 Pbl, e_term, pbl, pre, (dI,pI,mI)) end
363 | Some (pI, (pbl, pre)) =>
364 ModSpec (ocalhd_complete pbl pre (dI,pI,mI),
365 Pbl, e_term, pbl, pre, (dI,pI,mI))
368 (* val pos as (p,p_) = ip;
370 fun detailstep pt (pos as (p,p_):pos') =
371 let val nd = get_nd pt p
373 in if null cn andalso (is_rewset o (get_obj g_tac nd)) [] (*subnode!*)
374 then detailrls pt pos
375 else ("donesteps", pt(*, get_formress [] ((lev_on o lev_dn) p) cn*),
376 (p @ [length (children (get_nd pt p))], Res) )
381 (***. for mathematics authoring on sml-toplevel; no XML .***)
384 (* val sp = (dI',pI',mI');
387 (*15.8.03 for me with loc_specify/solve, nxt_specify/solve
388 delete as soon as TESTg_form -> _mout_ dropped*)
392 let val (form,_,_) = pt_extract ptp
394 Form t => Form' (FormKF (~1,EdUndef,0,Nundef,term2str t))
395 | ModSpec (_,p_, head, gfr, pre, _) =>
396 Form' (PpcKF (0,EdUndef,0,Nundef,
397 (case p_ of Pbl => Problem[] | Met => Method[],
398 itms2itemppc (assoc_thy"Isac.thy") gfr pre)))
401 fun CalcTreeTEST [(fmz, sp):fmz] =
402 (* val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))];
404 let (*val _ = states:= []; WN050707*)
405 val cs as ((pt,p), (tac,_,_)::_) = nxt_specify_init_calc (fmz, sp);
406 val f = TESTg_form (pt,p);
407 (* val _ = (add_calc cs; IteratorTEST 1; moveActiveRootTEST 1);WN050707*)
408 in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end;
410 (*for tests > 15.8.03 after separation setnexttactic / nextTac:
411 external view: me should be used by math-authors as done so far
412 internal view: loc_specify/solve, nxt_specify/solve used
413 i.e. same as in setnexttactic / nextTac*)
414 (*ENDE TESTPHASE 08/10.03:
415 NEW loeschen, eigene Version von locatetac, step
416 meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *)
419 fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) =
420 (* val (_,tac) = nxt;
422 (* val (msg, (tacis, pos's, (pt',p'))) = locatetac tac (pt,p);
423 f2str (TESTg_form (pt', p'));
424 (writeln o (itms2str thy)) (get_obj g_pbl pt' (fst p'));
425 writeln( istate2str (get_istate pt' ([3],Res)));
426 term2str (fst (get_obj g_result pt' [3]));
427 val (pt,p) = (pt',p');
429 (*locatetac is here for testing by me; step would suffice in me*)
430 case locatetac tac (pt,p) of
431 ("ok", (_, _, ptp)) => ptp
432 | ("unsafe-ok", (_, _, ptp)) => ptp
433 | ("not-applicable",_) => (pt, p)
434 | ("end-of-calculation", (_, _, ptp)) => ptp
435 | ("failure",_) => raise error "sys-error";
437 (* val (eee, (ts, _, (pt'',_))) = step p ((pt, e_pos'),[]);
439 ((*step is abused for getting next tac, resulting pt dropped*)
440 case step p ((pt, e_pos'),[]) of
441 ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)
442 | ("helpless",_) => ("helpless: cannot propose tac", [])
443 | ("no-fmz-spec",_) => raise error "no-fmz-spec"
444 | ("end-of-calculation", (ts, _, _)) => ("",ts))
445 handle _ => raise error "sys-error";
446 val tac = case ts of ((tac,_,_)::_) => tac
447 | _ => if p = ([],Res) then End_Proof'
449 (*form output comes from locatetac*)
450 in (p:pos',[]:NEW, TESTg_form (pt, p),
451 (tac2IDstr tac, tac):tac'_, Sundef, pt) end;
458 fun f2str (Form' (FormKF (_, _, _, _, cterm'))) = cterm';