lucin: fix Test_Isac, rename aux-funs in lucas-interpreter.
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
7 signature MATH_ENGINE =
9 type NEW (* TODO: refactor "fun me" with calcstate and remove *)
10 val me : Solve.tac'_ -> Ctree.pos' -> NEW ->
11 Ctree.ctree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Selem.safe * Ctree.ctree
12 val autocalc : Ctree.pos' list -> Ctree.pos' -> (Ctree.state) * Generate.taci list ->
13 Solve.auto -> string * Ctree.pos' list * (Ctree.state)
15 Tac.tac -> Ctree.state -> string * (Generate.taci list * Ctree.pos' list * (Ctree.state))
16 val step : Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate'
17 val detailstep : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
18 val get_pblID : Ctree.state -> Celem.pblID option
20 val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * Rule.scr * Model.itm list * (bool * term) list
21 val initcontext_pbl : Ctree.ctree -> Ctree.pos' -> bool * string list * term * Model.itm list * (bool * term) list
22 val context_met : Celem.metID -> Ctree.ctree -> Ctree.pos -> bool * Celem.metID * Rule.scr * Model.itm list * (bool * term) list
23 val context_pbl : Celem.pblID -> Ctree.ctree -> Ctree.pos -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
24 val set_method : Celem.metID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
25 val set_problem : Celem.pblID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
26 val set_theory : Rule.thyID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
27 val tryrefine : Celem.pblID -> Ctree.ctree -> Ctree.pos' -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
28 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
29 val CalcTreeTEST : Selem.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Tac.tac) * Selem.safe * Ctree.ctree
30 val f2str : Generate.mout -> Rule.cterm'
31 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
33 datatype lOc_ = ERror of string | UNsafe of Chead.calcstate' | Updated of Chead.calcstate'
34 val loc_solve_ : string * Tac.tac_ -> Ctree.ctree * Ctree.pos' -> lOc_
35 val loc_specify_ : Tac.tac_ -> Ctree.state -> lOc_
36 val nxt_specify_: Ctree.ctree * Ctree.pos' -> Chead.calcstate'
37 val TESTg_form : Ctree.state -> Generate.mout
38 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
40 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
45 structure Math_Engine(**): MATH_ENGINE(**) =
49 fun get_pblID (pt, (p, _): Ctree.pos') =
50 let val p' = Ctree.par_pblobj pt p
51 val (_, pI, _) = Ctree.get_obj Ctree.g_spec pt p'
52 val (_, (_, oI, _), _) = Ctree.get_obj Ctree.g_origin pt p'
54 if pI <> Celem.e_pblID
57 if oI <> Celem.e_pblID then SOME oI else NONE end;
60 ERror of string (*after loc_specify, loc_solve*)
61 | UNsafe of Chead.calcstate' (*after loc_specify, loc_solve*)
62 | Updated of Chead.calcstate' (*after loc_specify, loc_solve*)
64 fun loc_specify_ m (pt, pos) =
66 val (p, _, f, _, _, pt) = Chead.specify m pos [] pt;
68 case f of (Generate.Error' e) => ERror e | _ => Updated ([], [], (pt,p))
71 (* TODO push return-value cs' into solve and rename solve->loc_solve?_? *)
72 fun loc_solve_ m (pt, pos) =
74 val (msg, cs') = Solve.solve m (pt, pos);
76 case msg of "ok" => Updated cs' | msg => ERror msg
81 | Nexts of Chead.calcstate (**)
83 (* locate a tactic in a script and apply it if possible;
84 report of tacs' applicability in tacis; pt is dropped in setNextTactic*)
85 fun locatetac _ (ptp as (_, ([], Ctree.Res))) = ("end-of-calculation", ([], [], ptp))
86 | locatetac tac (ptp as (pt, p)) =
88 val (mI, m) = Solve.mk_tac'_ tac;
90 case Applicable.applicable_in p pt m of
91 Chead.Notappl _ => ("not-applicable", ([],[], ptp): Chead.calcstate')
94 val x = if member op = Solve.specsteps mI
95 then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
98 ERror _ => ("failure", ([], [], ptp))
99 (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
100 | UNsafe cs' => ("unsafe-ok", cs')
101 | Updated (cs' as (_, _, (_, p'))) => (*ev.SEVER.tacs like Begin_Trans*)
102 (if p' = ([], Ctree.Res) then "end-of-calculation" else "ok", cs')
103 (*for SEVER.tacs user to ask ? *)
107 (* iterated by nxt_me; there (the resulting) ptp dropped
108 may call nxt_solve Apply_Method --- thus evaluated here after solve.sml *)
109 fun nxt_specify_ (ptp as (pt, (p, p_))) =
111 val (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) =
112 case Ctree.get_obj I pt p of
113 pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _),
114 probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)
115 | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj"
117 if Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin
120 ["no_met"] => Chead.nxt_specif (Tac.Refine_Tacitly pI') (pt, (p, Ctree.Pbl))
121 | _ => Chead.nxt_specif Tac.Model_Problem (pt, (p, Ctree.Pbl))
124 val cpI = if pI = Celem.e_pblID then pI' else pI;
125 val cmI = if mI = Celem.e_metID then mI' else mI;
126 val {ppc, prls, where_, ...} = Specify.get_pbt cpI;
127 val pre = Stool.check_preconds "thy 100820" prls where_ probl;
128 val pb = foldl and_ (true, map fst pre);
129 (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*)
131 Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)
134 Tac.Apply_Method mI =>
135 LucinNEW.begin_end_prog (Tac.Apply_Method' (mI, NONE, Selem.e_istate, Selem.e_ctxt)) (Selem.e_istate, Selem.e_ctxt) ptp
136 | _ => Chead.nxt_specif tac ptp
140 (* specify a new method; WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' *)
141 fun set_method mI ptp =
144 case Chead.nxt_specif (Tac.Specify_Method mI) ptp of
145 ([(_, Tac.Specify_Method' (_, _, mits), _)], [], (pt, (p, _))) => (mits, pt, p)
146 | _ => error "set_method: case 1 uncovered"
147 val pre = [] (*...from Specify_Method'*)
148 val complete = true (*...from Specify_Method'*)
149 (*from Specify_Method' ? vvv, vvv ?*)
151 case Ctree.get_obj I pt p of
152 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
153 | Ctree.PrfObj _ => error "set_method: case 2 uncovered"
155 (pt, (complete, Ctree.Met, hdf, mits, pre, spec) : Ctree.ocalhd)
158 (* specify a new problem; WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' *)
159 fun set_problem pI ptp =
161 val (complete, pits, pre, pt, p) =
162 case Chead.nxt_specif (Tac.Specify_Problem pI) ptp of
163 ([(_, Tac.Specify_Problem' (_, (complete, (pits, pre))),_)], _, (pt, (p,_)))
164 => (complete, pits, pre, pt, p)
165 | _ => error "set_problem: case 1 uncovered"
166 (*from Specify_Problem' ? vvv, vvv ?*)
168 case Ctree.get_obj I pt p of
169 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
170 | Ctree.PrfObj _ => error "set_problem: case 2 uncovered"
172 (pt, (complete, Ctree.Pbl, hdf, pits, pre, spec) : Ctree.ocalhd)
175 fun set_theory tI ptp =
177 val (complete, pits, pre, pt, p) =
178 case Chead.nxt_specif (Tac.Specify_Theory tI) ptp of
179 ([(_, Tac.Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _)))
180 => (complete, pits, pre, pt, p)
181 | _ => error "set_theory: case 1 uncovered"
182 (*from Specify_Theory' ? vvv, vvv ?*)
184 case Ctree.get_obj I pt p of
185 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
186 | Ctree.PrfObj _ => error "set_theory: case 2 uncovered"
187 in (pt, (complete, Ctree.Pbl, hdf, pits, pre, spec) : Ctree.ocalhd) end;
189 (* does a step forward; returns tactic used, ctree updated.
190 TODO.WN0512 redesign after specify-phase became more separated from solve-phase *)
191 fun step (ip as (_, p_)) (ptp as (pt,p), tacis) =
192 let val pIopt = get_pblID (pt,ip);
194 if ip = ([], Ctree.Res)
195 then ("end-of-calculation", (tacis, [], ptp): Chead.calcstate')
199 if ip = p (*the request is done where ptp waits for*)
201 let val (pt',c',p') = Generate.generate tacis (pt,[],p)
202 in ("ok", (tacis, c', (pt', p'))) end
203 else (case (if member op = [Ctree.Pbl, Ctree.Met] p_
204 then nxt_specify_ (pt, ip) else LucinNEW.do_solve_step (pt, ip))
205 handle ERROR msg => (writeln ("*** " ^ msg);
206 ([], [], ptp)) (*e.g. Add_Given "equality///"*) of
207 cs as ([],_,_) => ("helpless", cs)
209 | _ => (case pIopt of
210 NONE => ("no-fmz-spec", ([], [], ptp))
211 | SOME _ => (*vvvvvv: Apply_Method without init_form*)
212 (case if member op = [Ctree.Pbl, Ctree.Met] p_
213 andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p))
214 then nxt_specify_ (pt, ip)
215 else (LucinNEW.do_solve_step (pt,ip))
216 handle ERROR msg => (writeln ("*** " ^ msg);
217 ([],[],ptp)) (*e.g. Add_Given "equality///"*) of
218 cs as ([],_,_) =>("helpless", cs) (*FIXXME del.handle*)
222 (* does several steps within one calculation as given by "type auto";
223 the steps may arbitrarily go into and leave different phases,
224 i.e. specify-phase and solve-phase
225 TODO.WN0512 ? redesign after the phases have been more separated
226 at the fron-end in 05:
227 eg. CompleteCalcHead could be done by a separate fun !!!*)
228 fun autocalc c ip cs (Solve.Step s) =
231 let val (str, (_, c', ptp)) = step ip cs; (* autoord = 1, probably does 1 step too much*)
232 in (str, c@c', ptp) end
234 let val (str, (_, c', ptp as (_, p))) = step ip cs;
237 then autocalc (c@c') p (ptp, []) (Solve.Step (s - 1))
238 else (str, c@c', ptp) end
239 (* handles autoord <= 3, autoord > 3 handled by all_solve, complete_solve *)
240 | autocalc c (pos as (_, p_)) ((pt, _), _(*tacis could help 1x in solve*)) auto =
241 if Solve.autoord auto > 3 andalso Ctree.just_created (pt, pos)
243 let val ptp = Chead.all_modspec (pt, pos);
244 in Solve.all_solve auto c ptp end (*... auto = 4 | 5 | 6 *)
246 if member op = [Ctree.Pbl, Ctree.Met] p_
248 if not (Chead.is_complete_mod (pt, pos))
250 let val ptp = Chead.complete_mod (pt, pos) (*... auto = 2 | 3 *)
252 if Solve.autoord auto < 3 then ("ok", c, ptp)
254 if not (Chead.is_complete_spec ptp)
256 let val ptp = Chead.complete_spec ptp
258 if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
260 else if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
263 if not (Chead.is_complete_spec (pt,pos))
265 let val ptp = Chead.complete_spec (pt, pos)
267 if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
270 if Solve.autoord auto = 3 then ("ok", c, (pt, pos)) else Solve.all_solve auto c (pt, pos)
271 else Solve.complete_solve auto c (pt, pos);
273 (*.initialiye matching; before 'tryMatch' get the pblID to match with:
274 if no pbl has been specified, take the init from origin.*)
275 fun initcontext_pbl pt (p, _) =
277 val (probl, os, pI, hdl, pI') =
278 case Ctree.get_obj I pt p of
279 Ctree.PblObj {probl, origin = (os, (_, pI, _), hdl), spec=(_, pI', _), ...}
280 => (probl, os, pI, hdl, pI')
281 | Ctree.PrfObj _ => error "initcontext_pbl: uncovered case"
283 if pI' = Celem.e_pblID
284 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
286 val {ppc, where_, prls, ...} = Specify.get_pbt pblID
287 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") probl (ppc, where_, prls) os
289 (model_ok, pblID, hdl, pbl, pre)
292 fun initcontext_met pt (p,_) =
294 val (meth, os, mI, mI') =
295 case Ctree.get_obj I pt p of
296 Ctree.PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI')
297 | Ctree.PrfObj _ => error "initcontext_met: uncovered case"
298 val metID = if mI' = Celem.e_metID
299 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
301 val {ppc, pre, prls, scr, ...} = Specify.get_met metID
302 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") meth (ppc,pre,prls) os
304 (model_ok, metID, scr, pbl, pre)
307 (* match the model of a problem at pos p with the model-pattern of the problem with pblID *)
308 fun context_pbl pI pt p =
310 val (probl, os, hdl) =
311 case Ctree.get_obj I pt p of
312 Ctree.PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl)
313 | Ctree.PrfObj _ => error "context_pbl: uncovered case"
314 val {ppc,where_,prls,...} = Specify.get_pbt pI
315 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") probl (ppc,where_,prls) os
317 (model_ok, pI, hdl, pbl, pre)
320 fun context_met mI pt p =
323 case Ctree.get_obj I pt p of
324 Ctree.PblObj {meth, origin = (os, _, _),...} => (meth, os)
325 | Ctree.PrfObj _ => error "context_met: uncovered case"
326 val {ppc,pre,prls,scr,...} = Specify.get_met mI
327 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") meth (ppc,pre,prls) os
329 (model_ok, mI, scr, pbl, pre)
332 fun tryrefine pI pt (p,_) =
334 val (probl, os, hdl) =
335 case Ctree.get_obj I pt p of
336 Ctree.PblObj {probl, origin = (os, _, hdl), ...} => (probl, os, hdl)
337 | Ctree.PrfObj _ => error "context_met: uncovered case"
339 case Specify.refine_pbl (Celem.assoc_thy "Isac") pI probl of
340 NONE => (*copy from context_pbl*)
342 val {ppc,where_,prls,...} = Specify.get_pbt pI
343 val (_, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") probl (ppc,where_,prls) os
345 (false, pI, hdl, pbl, pre)
347 | SOME (pI, (pbl, pre)) => (true, pI, hdl, pbl, pre)
350 fun detailstep pt (pos as (p, _)) =
352 val nd = Ctree.get_nd pt p
353 val cn = Ctree.children nd
357 if (Tac.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)]
358 then Solve.detailrls pt pos
359 else ("no-Rewrite_Set...", Ctree.EmptyPtree, Ctree.e_pos')
360 else ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Ctree.Res))
364 (*** for mathematics authoring on sml-toplevel; no XML ***)
368 (* 15.8.03 for me with loc_specify/solve, nxt_specify/solve
369 delete as soon as TESTg_form -> _mout_ dropped *)
372 val (form, _, _) = Chead.pt_extract ptp
375 Ctree.Form t => Generate.FormKF (Rule.term2str t)
376 | Ctree.ModSpec (_, p_, _, gfr, pre, _) =>
378 (case p_ of Ctree.Pbl => Generate.Problem []
379 | Ctree.Met => Generate.Method []
380 | _ => error "TESTg_form: uncovered case",
381 Specify.itms2itemppc (Celem.assoc_thy"Isac") gfr pre))
384 (* create a calc-tree; for use within sml: thus "^^^" NOT decoded to "^" etc;
385 compare "fun CalcTree" which DOES decode *)
386 fun CalcTreeTEST [(fmz, sp)] =
388 val ((pt, p), tacis) = Chead.nxt_specify_init_calc (fmz, sp)
389 val tac = case tacis of [] => Tac.Empty_Tac | _ => (#1 o hd) tacis
390 val f = TESTg_form (pt,p)
391 in (p, []:NEW, f, (Tac.tac2IDstr tac, tac), Selem.Sundef, pt) end
392 | CalcTreeTEST _ = error "CalcTreeTEST: uncovered case"
394 (*for tests > 15.8.03 after separation setnexttactic / nextTac:
395 external view: me should be used by math-authors as done so far
396 internal view: loc_specify/solve, nxt_specify/solve used
397 i.e. same as in setnexttactic / nextTac*)
398 (*ENDE TESTPHASE 08/10.03:
399 NEW loeschen, eigene Version von locatetac, step
400 meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *)
402 fun me (_, tac) p _(*NEW remove*) pt =
405 (*locatetac is here for testing by me; step would suffice in me*)
406 case locatetac tac (pt,p) of
407 ("ok", (_, _, ptp)) => ptp
408 | ("unsafe-ok", (_, _, ptp)) => ptp
409 | ("not-applicable",_) => (pt, p)
410 | ("end-of-calculation", (_, _, ptp)) => ptp
411 | ("failure", _) => error "sys-error"
412 | _ => error "me: uncovered case"
414 (case step p ((pt, Ctree.e_pos'),[]) of
415 ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
416 | ("helpless", _) => ("helpless: cannot propose tac", [])
417 | ("no-fmz-spec", _) => error "no-fmz-spec"
418 | ("end-of-calculation", (ts, _, _)) => ("", ts)
419 | _ => error "me: uncovered case")
420 handle ERROR msg => raise ERROR msg
423 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
424 | _ => if p = ([], Ctree.Res) then Tac.End_Proof' else Tac.Empty_Tac;
425 in (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *),
426 (Tac.tac2IDstr tac, tac), Selem.Sundef, pt)
429 (* for quick test-print-out, until 'type inout' is removed *)
430 fun f2str (Generate.FormKF cterm') = cterm'
431 | f2str _ = error "f2str: uncovered case in fun.def.";