src/Tools/isac/MathEngine/mathengine-stateless.sml
changeset 59903 5037ca1b112b
parent 59898 68883c046963
child 59908 9af7dd257f47
     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