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 : Solve.tac'_ -> Ctree.pos' -> NEW -> Ctree.ptree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Ctree.safe * Ctree.ptree |
12 val me : Solve.tac'_ -> Ctree.pos' -> NEW -> Ctree.ctree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Ctree.safe * Ctree.ctree |
13 val autocalc : |
13 val autocalc : |
14 Ctree.pos' list -> Ctree.pos' -> (Ctree.ptree * Ctree.pos') * Generate.taci list -> Solve.auto -> string * Ctree.pos' list * (Ctree.ptree * Ctree.pos') |
14 Ctree.pos' list -> Ctree.pos' -> (Ctree.ctree * Ctree.pos') * Generate.taci list -> Solve.auto -> string * Ctree.pos' list * (Ctree.ctree * Ctree.pos') |
15 val locatetac : |
15 val locatetac : |
16 Ctree.tac -> Ctree.ptree * Ctree.pos' -> string * (Generate.taci list * Ctree.pos' list * (Ctree.ptree * Ctree.pos')) |
16 Ctree.tac -> Ctree.ctree * Ctree.pos' -> string * (Generate.taci list * Ctree.pos' list * (Ctree.ctree * Ctree.pos')) |
17 val step : Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate' |
17 val step : Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate' |
18 val detailstep : |
18 val detailstep : |
19 Ctree.ptree -> Ctree.pos' -> string * Ctree.ptree * Ctree.pos' |
19 Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos' |
20 val get_pblID : Ctree.ptree * Ctree.pos' -> pblID option |
20 val get_pblID : Ctree.ctree * Ctree.pos' -> pblID option |
21 |
21 |
22 val initcontext_met : Ctree.ptree -> Ctree.pos' -> bool * string list * scr * itm list * (bool * term) list |
22 val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * scr * itm list * (bool * term) list |
23 val initcontext_pbl : Ctree.ptree -> Ctree.pos' -> bool * string list * term * itm list * (bool * term) list |
23 val initcontext_pbl : Ctree.ctree -> Ctree.pos' -> bool * string list * term * itm list * (bool * term) list |
24 val context_met : metID -> Ctree.ptree -> Ctree.pos -> bool * metID * scr * itm list * (bool * term) list |
24 val context_met : metID -> Ctree.ctree -> Ctree.pos -> bool * metID * scr * itm list * (bool * term) list |
25 val context_pbl : pblID -> Ctree.ptree -> Ctree.pos -> bool * pblID * term * itm list * (bool * term) list |
25 val context_pbl : pblID -> Ctree.ctree -> Ctree.pos -> bool * pblID * term * itm list * (bool * term) list |
26 val set_method : metID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd |
26 val set_method : metID -> Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.ocalhd |
27 val set_problem : pblID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd |
27 val set_problem : pblID -> Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.ocalhd |
28 val set_theory : thyID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd |
28 val set_theory : thyID -> Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.ocalhd |
29 val tryrefine : pblID -> Ctree.ptree -> Ctree.pos' -> bool * pblID * term * itm list * (bool * term) list |
29 val tryrefine : pblID -> Ctree.ctree -> Ctree.pos' -> bool * pblID * term * itm list * (bool * term) list |
30 |
30 |
31 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
31 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
32 type nxt_ |
32 type nxt_ |
33 type lOc_ |
33 type lOc_ |
34 val CalcTreeTEST : Ctree.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Ctree.tac) * Ctree.safe * Ctree.ptree |
34 val CalcTreeTEST : Ctree.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Ctree.tac) * Ctree.safe * Ctree.ctree |
35 val f2str : Generate.mout -> cterm' |
35 val f2str : Generate.mout -> cterm' |
36 val loc_solve_ : string * Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> lOc_ |
36 val loc_solve_ : string * Ctree.tac_ -> Ctree.ctree * Ctree.pos' -> lOc_ |
37 val loc_specify_ : Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> lOc_ |
37 val loc_specify_ : Ctree.tac_ -> Ctree.ctree * Ctree.pos' -> lOc_ |
38 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
38 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) |
39 end |
39 end |
40 |
40 |
41 (**) |
41 (**) |
42 structure Math_Engine(**): MATH_ENGINE(**) = |
42 structure Math_Engine(**): MATH_ENGINE(**) = |