1.1 --- a/src/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 22 11:23:30 2020 +0200
1.2 +++ b/src/Tools/isac/MathEngine/mathengine-stateless.sml Wed Apr 22 14:36:27 2020 +0200
1.3 @@ -12,12 +12,12 @@
1.4
1.5 val initcontext_met : Ctree.ctree -> Pos.pos' -> bool * string list * Program.T * Model.itm list * (bool * term) list
1.6 val initcontext_pbl : Ctree.ctree -> Pos.pos' -> bool * string list * term * Model.itm list * (bool * term) list
1.7 - val context_met : Spec.metID -> Ctree.ctree -> Pos.pos -> bool * Spec.metID * Program.T * Model.itm list * (bool * term) list
1.8 - val context_pbl : Spec.pblID -> Ctree.ctree -> Pos.pos -> bool * Spec.pblID * term * Model.itm list * (bool * term) list
1.9 - val set_method : Spec.metID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
1.10 - val set_problem : Spec.pblID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
1.11 + val context_met : Method.id -> Ctree.ctree -> Pos.pos -> bool * Method.id * Program.T * Model.itm list * (bool * term) list
1.12 + val context_pbl : Problem.id -> Ctree.ctree -> Pos.pos -> bool * Problem.id * term * Model.itm list * (bool * term) list
1.13 + val set_method : Method.id -> Calc.T -> Ctree.ctree * Ctree.ocalhd
1.14 + val set_problem : Problem.id -> Calc.T -> Ctree.ctree * Ctree.ocalhd
1.15 val set_theory : ThyC.id -> Calc.T -> Ctree.ctree * Ctree.ocalhd
1.16 - val tryrefine : Spec.pblID -> Ctree.ctree -> Pos.pos' -> bool * Spec.pblID * term * Model.itm list * (bool * term) list
1.17 + val tryrefine : Problem.id -> Ctree.ctree -> Pos.pos' -> bool * Problem.id * term * Model.itm list * (bool * term) list
1.18 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.19 (*NONE*)
1.20 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.21 @@ -144,7 +144,7 @@
1.22 => (probl, os, pI, hdl, pI')
1.23 | Ctree.PrfObj _ => error "initcontext_pbl: uncovered case"
1.24 val pblID =
1.25 - if pI' = Spec.e_pblID
1.26 + if pI' = Problem.id_empty
1.27 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
1.28 else pI'
1.29 val {ppc, where_, prls, ...} = Specify.get_pbt pblID
1.30 @@ -159,7 +159,7 @@
1.31 case Ctree.get_obj I pt p of
1.32 Ctree.PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI')
1.33 | Ctree.PrfObj _ => error "initcontext_met: uncovered case"
1.34 - val metID = if mI' = Spec.e_metID
1.35 + val metID = if mI' = Method.id_empty
1.36 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
1.37 else mI'
1.38 val {ppc, pre, prls, scr, ...} = Specify.get_met metID