7 *) |
7 *) |
8 |
8 |
9 signature MATH_ENGINE = |
9 signature MATH_ENGINE = |
10 sig |
10 sig |
11 type NEW (* TODO: refactor "fun me" with calcstate and remove *) |
11 type NEW (* TODO: refactor "fun me" with calcstate and remove *) |
12 val me : tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * mout * tac'_ * safe * ptree |
12 val me : tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * Ctree.mout * tac'_ * safe * ptree |
13 val autocalc : |
13 val autocalc : |
14 pos' list -> pos' -> (ptree * pos') * taci list -> auto -> string * pos' list * (ptree * pos') |
14 pos' list -> pos' -> (ptree * pos') * Ctree.taci list -> auto -> string * pos' list * (ptree * pos') |
15 val locatetac : |
15 val locatetac : |
16 tac -> ptree * (posel list * pos_) -> string * (taci list * 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' |
17 val step : pos' -> Chead.calcstate -> string * Chead.calcstate' |
18 val detailstep : |
18 val detailstep : |
19 ptree -> pos' -> string * ptree * pos' val get_pblID : ptree * pos' -> pblID option |
19 ptree -> pos' -> string * ptree * pos' val get_pblID : ptree * pos' -> pblID option |
20 |
20 |
21 val initcontext_met : ptree -> pos' -> bool * string list * scr * itm list * (bool * term) list |
21 val initcontext_met : ptree -> pos' -> bool * string list * scr * itm list * (bool * term) list |
28 val tryrefine : pblID -> ptree -> pos' -> bool * pblID * term * itm list * (bool * term) list |
28 val tryrefine : pblID -> ptree -> pos' -> bool * pblID * term * itm list * (bool * term) list |
29 |
29 |
30 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
30 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
31 type nxt_ |
31 type nxt_ |
32 type lOc_ |
32 type lOc_ |
33 val CalcTreeTEST : fmz list -> pos' * NEW * mout * (string * tac) * safe * ptree |
33 val CalcTreeTEST : fmz list -> pos' * NEW * Ctree.mout * (string * tac) * safe * ptree |
34 val f2str : mout -> cterm' |
34 val f2str : Ctree.mout -> cterm' |
35 val loc_solve_ : string * tac_ -> ptree * (pos * pos_) -> lOc_ |
35 val loc_solve_ : string * tac_ -> ptree * (pos * pos_) -> lOc_ |
36 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
36 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
37 end |
37 end |
38 |
38 |
39 (**) |
39 (**) |
60 |
60 |
61 fun loc_specify_ m (pt,pos) = |
61 fun loc_specify_ m (pt,pos) = |
62 let |
62 let |
63 val (p, _, f, _, _, pt) = Chead.specify m pos [] pt; |
63 val (p, _, f, _, _, pt) = Chead.specify m pos [] pt; |
64 in |
64 in |
65 case f of (Error' (Error_ e)) => ERror e | _ => Updated ([], [], (pt,p)) |
65 case f of (Ctree.Error' (Ctree.Error_ e)) => ERror e | _ => Updated ([], [], (pt,p)) |
66 end |
66 end |
67 |
67 |
68 (* TODO push return-value cs' into solve and rename solve->loc_solve?_? *) |
68 (* TODO push return-value cs' into solve and rename solve->loc_solve?_? *) |
69 fun loc_solve_ m (pt, pos) = |
69 fun loc_solve_ m (pt, pos) = |
70 let |
70 let |
193 else |
193 else |
194 case tacis of |
194 case tacis of |
195 (_::_) => |
195 (_::_) => |
196 if ip = p (*the request is done where ptp waits for*) |
196 if ip = p (*the request is done where ptp waits for*) |
197 then |
197 then |
198 let val (pt',c',p') = generate tacis (pt,[],p) |
198 let val (pt',c',p') = Ctree.generate tacis (pt,[],p) |
199 in ("ok", (tacis, c', (pt', p'))) end |
199 in ("ok", (tacis, c', (pt', p'))) end |
200 else (case (if member op = [Pbl, Met] p_ |
200 else (case (if member op = [Pbl, Met] p_ |
201 then nxt_specify_ (pt, ip) else nxt_solve_ (pt, ip)) |
201 then nxt_specify_ (pt, ip) else nxt_solve_ (pt, ip)) |
202 handle ERROR msg => (writeln ("*** " ^ msg); |
202 handle ERROR msg => (writeln ("*** " ^ msg); |
203 ([], [], ptp)) (*e.g. Add_Given "equality///"*) of |
203 ([], [], ptp)) (*e.g. Add_Given "equality///"*) of |
366 fun TESTg_form ptp = |
366 fun TESTg_form ptp = |
367 let |
367 let |
368 val (form, _, _) = Chead.pt_extract ptp |
368 val (form, _, _) = Chead.pt_extract ptp |
369 in |
369 in |
370 case form of |
370 case form of |
371 Form t => Form' (FormKF (~1,EdUndef,0,Nundef,term2str t)) |
371 Form t => Ctree.Form' (Ctree.FormKF (~1,Ctree.EdUndef,0,Ctree.Nundef,term2str t)) |
372 | ModSpec (_,p_, _, gfr, pre, _) => |
372 | ModSpec (_,p_, _, gfr, pre, _) => |
373 Form' (PpcKF (0, EdUndef, 0, Nundef, |
373 Ctree.Form' (Ctree.PpcKF (0, Ctree.EdUndef, 0, Ctree.Nundef, |
374 (case p_ of Pbl => Problem [] | Met => Method [] | _ => error "TESTg_form: uncovered case", |
374 (case p_ of Pbl => Ctree.Problem [] | Met => Ctree.Method [] | _ => error "TESTg_form: uncovered case", |
375 itms2itemppc (assoc_thy"Isac") gfr pre))) |
375 itms2itemppc (assoc_thy"Isac") gfr pre))) |
376 end; |
376 end; |
377 |
377 |
378 (* create a calc-tree; for use within sml: thus "^^^" NOT decoded to "^" etc; |
378 (* create a calc-tree; for use within sml: thus "^^^" NOT decoded to "^" etc; |
379 compare "fun CalcTree" which DOES decode *) |
379 compare "fun CalcTree" which DOES decode *) |
419 in (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *), |
419 in (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *), |
420 (tac2IDstr tac, tac):tac'_, Sundef, pt) |
420 (tac2IDstr tac, tac):tac'_, Sundef, pt) |
421 end |
421 end |
422 |
422 |
423 (* for quick test-print-out, until 'type inout' is removed *) |
423 (* for quick test-print-out, until 'type inout' is removed *) |
424 fun f2str (Form' (FormKF (_, _, _, _, cterm'))) = cterm'; |
424 fun f2str (Ctree.Form' (Ctree.FormKF (_, _, _, _, cterm'))) = cterm'; |
425 |
425 |
426 end |
426 end |