wneuper/isa: comparison src/Tools/isac/Interpret/mathengine.sml

equal deleted inserted replaced

-:6a2753b8d70c
+:49d7d410b83c
 val locatetac :
 Tac.tac -> Ctree.state -> string * (Generate.taci list * Ctree.pos' list * (Ctree.state))
 val step : Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate'
 val detailstep :
 Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
-val get_pblID : Ctree.state -> pblID option
+val get_pblID : Ctree.state -> Celem.pblID option
-val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * scr * Model.itm list * (bool * term) list
+val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * Celem.scr * Model.itm list * (bool * term) list
 val initcontext_pbl : Ctree.ctree -> Ctree.pos' -> bool * string list * term * Model.itm list * (bool * term) list
-val context_met : metID -> Ctree.ctree -> Ctree.pos -> bool * metID * scr * Model.itm list * (bool * term) list
+val context_met : Celem.metID -> Ctree.ctree -> Ctree.pos -> bool * Celem.metID * Celem.scr * Model.itm list * (bool * term) list
-val context_pbl : pblID -> Ctree.ctree -> Ctree.pos -> bool * pblID * term * Model.itm list * (bool * term) list
+val context_pbl : Celem.pblID -> Ctree.ctree -> Ctree.pos -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
-val set_method : metID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
+val set_method : Celem.metID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
-val set_problem : pblID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
+val set_problem : Celem.pblID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
-val set_theory : thyID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
+val set_theory : Celem.thyID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
-val tryrefine : pblID -> Ctree.ctree -> Ctree.pos' -> bool * pblID * term * Model.itm list * (bool * term) list
+val tryrefine : Celem.pblID -> Ctree.ctree -> Ctree.pos' -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
 val CalcTreeTEST : Selem.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Tac.tac) * Selem.safe * Ctree.ctree
-val f2str : Generate.mout -> cterm'
+val f2str : Generate.mout -> Celem.cterm'
 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
 type nxt_
 type lOc_
 val loc_solve_ : string * Tac.tac_ -> Ctree.ctree *  Ctree.pos' -> lOc_
 val loc_specify_ : Tac.tac_ -> Ctree.state -> lOc_
 fun get_pblID (pt, (p, _): Ctree.pos') =
 let val p' = Ctree.par_pblobj pt p
 	val (_, pI, _) = Ctree.get_obj Ctree.g_spec pt p'
 	val (_, (_, oI, _), _) = Ctree.get_obj Ctree.g_origin pt p'
 in
-if pI <> e_pblID
+if pI <> Celem.e_pblID
 then SOME pI
 else
-if oI <> e_pblID then SOME oI else NONE end;
+if oI <> Celem.e_pblID then SOME oI else NONE end;
 datatype lOc_ =
 ERror of string              (*after loc_specify, loc_solve*)
 | UNsafe of Chead.calcstate'   (*after loc_specify, loc_solve*)
 | Updated of Chead.calcstate'  (*after loc_specify, loc_solve*)
 case mI' of
 ["no_met"] => Chead.nxt_specif (Tac.Refine_Tacitly pI') (pt, (p, Ctree.Pbl))
 | _ => Chead.nxt_specif Tac.Model_Problem (pt, (p, Ctree.Pbl))
 else
 let
-val cpI = if pI = e_pblID then pI' else pI;
+val cpI = if pI = Celem.e_pblID then pI' else pI;
-	    val cmI = if mI = e_metID then mI' else mI;
+	    val cmI = if mI = Celem.e_metID then mI' else mI;
 	    val {ppc, prls, where_, ...} = Specify.get_pbt cpI;
 	    val pre = Stool.check_preconds "thy 100820" prls where_ probl;
 	    val pb = foldl and_ (true, map fst pre);
 	    (*FIXME.WN0308:    ~~~~~: just check true in itms of pbl/met?*)
 	    val (_, tac) =
 case Ctree.get_obj I pt p of
 Ctree.PblObj {probl, origin = (os, (_, pI, _), hdl), spec=(_, pI', _), ...}
 => (probl, os, pI, hdl, pI')
 | Ctree.PrfObj _ => error "initcontext_pbl: uncovered case"
 	val pblID =
-	  if pI' = e_pblID
+	  if pI' = Celem.e_pblID
 		then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
 		else pI'
 	val {ppc, where_, prls, ...} = Specify.get_pbt pblID
-	val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
+	val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") probl (ppc, where_, prls) os
 in
 (model_ok, pblID, hdl, pbl, pre)
 end
 fun initcontext_met pt (p,_) =
 let
 val (meth, os, mI, mI') =
 case Ctree.get_obj I pt p of
 Ctree.PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI')
 | Ctree.PrfObj _ => error "initcontext_met: uncovered case"
-	val metID = if mI' = e_metID
+	val metID = if mI' = Celem.e_metID
 		    then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
 		    else mI'
 	val {ppc, pre, prls, scr, ...} = Specify.get_met metID
-	val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
+	val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") meth (ppc,pre,prls) os
 in
 (model_ok, metID, scr, pbl, pre)
 end
 (* match the model of a problem at pos p with the model-pattern of the problem with pblID *)
 val (probl, os, hdl) =
 case Ctree.get_obj I pt p of
 Ctree.PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl)
 | Ctree.PrfObj _ => error "context_pbl: uncovered case"
 	val {ppc,where_,prls,...} = Specify.get_pbt pI
-	val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
+	val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") probl (ppc,where_,prls) os
 in
 (model_ok, pI, hdl, pbl, pre)
 end
 fun context_met mI pt p =
 val (meth, os) =
 case Ctree.get_obj I pt p of
 Ctree.PblObj {meth, origin = (os, _, _),...} => (meth, os)
 | Ctree.PrfObj _ => error "context_met: uncovered case"
 	val {ppc,pre,prls,scr,...} = Specify.get_met mI
-	val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
+	val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") meth (ppc,pre,prls) os
 in
 (model_ok, mI, scr, pbl, pre)
 end
 fun tryrefine pI pt (p,_) =
 val (probl, os, hdl) =
 case Ctree.get_obj I pt p of
 Ctree.PblObj {probl, origin = (os, _, hdl), ...} => (probl, os, hdl)
 | Ctree.PrfObj _ => error "context_met: uncovered case"
 in
-case Specify.refine_pbl (assoc_thy "Isac") pI probl of
+case Specify.refine_pbl (Celem.assoc_thy "Isac") pI probl of
 	  NONE => (*copy from context_pbl*)
 	    let
 	      val {ppc,where_,prls,...} = Specify.get_pbt pI
-	      val (_, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
+	      val (_, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") probl (ppc,where_,prls) os
 in
 (false, pI, hdl, pbl, pre)
 end
 	| SOME (pI, (pbl, pre)) => (true, pI, hdl, pbl, pre)
 end
 fun TESTg_form ptp =
 let
 val (form, _, _) = Chead.pt_extract ptp
 in
 case form of
-Ctree.Form t => Generate.FormKF (term2str t)
+Ctree.Form t => Generate.FormKF (Celem.term2str t)
 | Ctree.ModSpec (_, p_, _, gfr, pre, _) =>
 Generate.PpcKF (
 (case p_ of Ctree.Pbl => Generate.Problem []
 | Ctree.Met => Generate.Method []
 | _ => error "TESTg_form: uncovered case",
-			Specify.itms2itemppc (assoc_thy"Isac") gfr pre))
+			Specify.itms2itemppc (Celem.assoc_thy"Isac") gfr pre))
 end
 (* create a calc-tree; for use within sml: thus "^^^" NOT decoded to "^" etc;
 compare "fun CalcTree" which DOES decode                        *)
 fun CalcTreeTEST [(fmz, sp)] =

changeset 59405	49d7d410b83c
parent 59395	862eb17f9e16
child 59411	3e241a6938ce