1.1 --- a/src/Tools/isac/Interpret/mathengine.sml Tue Mar 13 15:04:27 2018 +0100
1.2 +++ b/src/Tools/isac/Interpret/mathengine.sml Thu Mar 15 10:17:44 2018 +0100
1.3 @@ -17,19 +17,19 @@
1.4 val step : Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate'
1.5 val detailstep :
1.6 Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
1.7 - val get_pblID : Ctree.state -> pblID option
1.8 + val get_pblID : Ctree.state -> Celem.pblID option
1.9
1.10 - val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * scr * Model.itm list * (bool * term) list
1.11 + val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * Celem.scr * Model.itm list * (bool * term) list
1.12 val initcontext_pbl : Ctree.ctree -> Ctree.pos' -> bool * string list * term * Model.itm list * (bool * term) list
1.13 - val context_met : metID -> Ctree.ctree -> Ctree.pos -> bool * metID * scr * Model.itm list * (bool * term) list
1.14 - val context_pbl : pblID -> Ctree.ctree -> Ctree.pos -> bool * pblID * term * Model.itm list * (bool * term) list
1.15 - val set_method : metID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
1.16 - val set_problem : pblID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
1.17 - val set_theory : thyID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
1.18 - val tryrefine : pblID -> Ctree.ctree -> Ctree.pos' -> bool * pblID * term * Model.itm list * (bool * term) list
1.19 + val context_met : Celem.metID -> Ctree.ctree -> Ctree.pos -> bool * Celem.metID * Celem.scr * Model.itm list * (bool * term) list
1.20 + val context_pbl : Celem.pblID -> Ctree.ctree -> Ctree.pos -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
1.21 + val set_method : Celem.metID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
1.22 + val set_problem : Celem.pblID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
1.23 + val set_theory : Celem.thyID -> Ctree.state -> Ctree.ctree * Ctree.ocalhd
1.24 + val tryrefine : Celem.pblID -> Ctree.ctree -> Ctree.pos' -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
1.25 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
1.26 val CalcTreeTEST : Selem.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Tac.tac) * Selem.safe * Ctree.ctree
1.27 - val f2str : Generate.mout -> cterm'
1.28 + val f2str : Generate.mout -> Celem.cterm'
1.29 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
1.30 type nxt_
1.31 type lOc_
1.32 @@ -53,10 +53,10 @@
1.33 val (_, pI, _) = Ctree.get_obj Ctree.g_spec pt p'
1.34 val (_, (_, oI, _), _) = Ctree.get_obj Ctree.g_origin pt p'
1.35 in
1.36 - if pI <> e_pblID
1.37 + if pI <> Celem.e_pblID
1.38 then SOME pI
1.39 else
1.40 - if oI <> e_pblID then SOME oI else NONE end;
1.41 + if oI <> Celem.e_pblID then SOME oI else NONE end;
1.42
1.43 datatype lOc_ =
1.44 ERror of string (*after loc_specify, loc_solve*)
1.45 @@ -123,8 +123,8 @@
1.46 | _ => Chead.nxt_specif Tac.Model_Problem (pt, (p, Ctree.Pbl))
1.47 else
1.48 let
1.49 - val cpI = if pI = e_pblID then pI' else pI;
1.50 - val cmI = if mI = e_metID then mI' else mI;
1.51 + val cpI = if pI = Celem.e_pblID then pI' else pI;
1.52 + val cmI = if mI = Celem.e_metID then mI' else mI;
1.53 val {ppc, prls, where_, ...} = Specify.get_pbt cpI;
1.54 val pre = Stool.check_preconds "thy 100820" prls where_ probl;
1.55 val pb = foldl and_ (true, map fst pre);
1.56 @@ -282,11 +282,11 @@
1.57 => (probl, os, pI, hdl, pI')
1.58 | Ctree.PrfObj _ => error "initcontext_pbl: uncovered case"
1.59 val pblID =
1.60 - if pI' = e_pblID
1.61 + if pI' = Celem.e_pblID
1.62 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
1.63 else pI'
1.64 val {ppc, where_, prls, ...} = Specify.get_pbt pblID
1.65 - val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
1.66 + val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") probl (ppc, where_, prls) os
1.67 in
1.68 (model_ok, pblID, hdl, pbl, pre)
1.69 end
1.70 @@ -297,11 +297,11 @@
1.71 case Ctree.get_obj I pt p of
1.72 Ctree.PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI')
1.73 | Ctree.PrfObj _ => error "initcontext_met: uncovered case"
1.74 - val metID = if mI' = e_metID
1.75 + val metID = if mI' = Celem.e_metID
1.76 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
1.77 else mI'
1.78 val {ppc, pre, prls, scr, ...} = Specify.get_met metID
1.79 - val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
1.80 + val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") meth (ppc,pre,prls) os
1.81 in
1.82 (model_ok, metID, scr, pbl, pre)
1.83 end
1.84 @@ -314,7 +314,7 @@
1.85 Ctree.PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl)
1.86 | Ctree.PrfObj _ => error "context_pbl: uncovered case"
1.87 val {ppc,where_,prls,...} = Specify.get_pbt pI
1.88 - val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
1.89 + val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") probl (ppc,where_,prls) os
1.90 in
1.91 (model_ok, pI, hdl, pbl, pre)
1.92 end
1.93 @@ -326,7 +326,7 @@
1.94 Ctree.PblObj {meth, origin = (os, _, _),...} => (meth, os)
1.95 | Ctree.PrfObj _ => error "context_met: uncovered case"
1.96 val {ppc,pre,prls,scr,...} = Specify.get_met mI
1.97 - val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
1.98 + val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") meth (ppc,pre,prls) os
1.99 in
1.100 (model_ok, mI, scr, pbl, pre)
1.101 end
1.102 @@ -338,11 +338,11 @@
1.103 Ctree.PblObj {probl, origin = (os, _, hdl), ...} => (probl, os, hdl)
1.104 | Ctree.PrfObj _ => error "context_met: uncovered case"
1.105 in
1.106 - case Specify.refine_pbl (assoc_thy "Isac") pI probl of
1.107 + case Specify.refine_pbl (Celem.assoc_thy "Isac") pI probl of
1.108 NONE => (*copy from context_pbl*)
1.109 let
1.110 val {ppc,where_,prls,...} = Specify.get_pbt pI
1.111 - val (_, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
1.112 + val (_, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac") probl (ppc,where_,prls) os
1.113 in
1.114 (false, pI, hdl, pbl, pre)
1.115 end
1.116 @@ -374,13 +374,13 @@
1.117 val (form, _, _) = Chead.pt_extract ptp
1.118 in
1.119 case form of
1.120 - Ctree.Form t => Generate.FormKF (term2str t)
1.121 + Ctree.Form t => Generate.FormKF (Celem.term2str t)
1.122 | Ctree.ModSpec (_, p_, _, gfr, pre, _) =>
1.123 Generate.PpcKF (
1.124 (case p_ of Ctree.Pbl => Generate.Problem []
1.125 | Ctree.Met => Generate.Method []
1.126 | _ => error "TESTg_form: uncovered case",
1.127 - Specify.itms2itemppc (assoc_thy"Isac") gfr pre))
1.128 + Specify.itms2itemppc (Celem.assoc_thy"Isac") gfr pre))
1.129 end
1.130
1.131 (* create a calc-tree; for use within sml: thus "^^^" NOT decoded to "^" etc;