equal
deleted
inserted
replaced
7 |
7 |
8 signature MATH_ENGINE = |
8 signature MATH_ENGINE = |
9 sig |
9 sig |
10 val autocalc : Ctree.pos' list -> Ctree.pos' -> (Calc.T) * Generate.taci list -> |
10 val autocalc : Ctree.pos' list -> Ctree.pos' -> (Calc.T) * Generate.taci list -> |
11 Solve.auto -> string * Ctree.pos' list * (Calc.T) |
11 Solve.auto -> string * Ctree.pos' list * (Calc.T) |
12 val detailstep : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos' |
|
13 |
12 |
14 val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * Program.T * Model.itm list * (bool * term) list |
13 val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * Program.T * Model.itm list * (bool * term) list |
15 val initcontext_pbl : Ctree.ctree -> Ctree.pos' -> bool * string list * term * Model.itm list * (bool * term) list |
14 val initcontext_pbl : Ctree.ctree -> Ctree.pos' -> bool * string list * term * Model.itm list * (bool * term) list |
16 val context_met : Celem.metID -> Ctree.ctree -> Ctree.pos -> bool * Celem.metID * Program.T * Model.itm list * (bool * term) list |
15 val context_met : Celem.metID -> Ctree.ctree -> Ctree.pos -> bool * Celem.metID * Program.T * Model.itm list * (bool * term) list |
17 val context_pbl : Celem.pblID -> Ctree.ctree -> Ctree.pos -> bool * Celem.pblID * term * Model.itm list * (bool * term) list |
16 val context_pbl : Celem.pblID -> Ctree.ctree -> Ctree.pos -> bool * Celem.pblID * term * Model.itm list * (bool * term) list |
210 (false, pI, hdl, pbl, pre) |
209 (false, pI, hdl, pbl, pre) |
211 end |
210 end |
212 | SOME (pI, (pbl, pre)) => (true, pI, hdl, pbl, pre) |
211 | SOME (pI, (pbl, pre)) => (true, pI, hdl, pbl, pre) |
213 end |
212 end |
214 |
213 |
215 fun detailstep pt (pos as (p, _)) = |
|
216 let |
|
217 val nd = Ctree.get_nd pt p |
|
218 val cn = Ctree.children nd |
|
219 in |
|
220 if null cn |
|
221 then |
|
222 if (Tactic.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)] |
|
223 then Solve.detailrls pt pos |
|
224 else ("no-Rewrite_Set...", Ctree.EmptyPtree, Pos.e_pos') |
|
225 else ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Pos.Res)) |
|
226 end; |
|
227 |
|
228 (**)end(**) |
214 (**)end(**) |