diff -r 2423f0fbdd08 -r 56dc790071cb src/Tools/isac/Interpret/mathengine.sml --- a/src/Tools/isac/Interpret/mathengine.sml Wed Dec 21 11:27:22 2016 +0100 +++ b/src/Tools/isac/Interpret/mathengine.sml Thu Dec 22 10:25:49 2016 +0100 @@ -9,30 +9,32 @@ signature MATH_ENGINE = sig type NEW (* TODO: refactor "fun me" with calcstate and remove *) - val me : Solve.tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * Generate.mout * Solve.tac'_ * safe * ptree + val me : Solve.tac'_ -> Ctree.pos' -> NEW -> Ctree.ptree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Ctree.safe * Ctree.ptree val autocalc : - pos' list -> pos' -> (ptree * pos') * Generate.taci list -> Solve.auto -> string * pos' list * (ptree * pos') + Ctree.pos' list -> Ctree.pos' -> (Ctree.ptree * Ctree.pos') * Generate.taci list -> Solve.auto -> string * Ctree.pos' list * (Ctree.ptree * Ctree.pos') val locatetac : - tac -> ptree * (posel list * pos_) -> string * (Generate.taci list * pos' list * (ptree * pos')) - val step : pos' -> Chead.calcstate -> string * Chead.calcstate' + Ctree.tac -> Ctree.ptree * Ctree.pos' -> string * (Generate.taci list * Ctree.pos' list * (Ctree.ptree * Ctree.pos')) + val step : Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate' val detailstep : - ptree -> pos' -> string * ptree * pos' val get_pblID : ptree * pos' -> pblID option + Ctree.ptree -> Ctree.pos' -> string * Ctree.ptree * Ctree.pos' + val get_pblID : Ctree.ptree * Ctree.pos' -> pblID option - val initcontext_met : ptree -> pos' -> bool * string list * scr * itm list * (bool * term) list - val initcontext_pbl : ptree -> pos' -> bool * string list * term * itm list * (bool * term) list - val context_met : metID -> ptree -> pos -> bool * metID * scr * itm list * (bool * term) list - val context_pbl : pblID -> ptree -> pos -> bool * pblID * term * itm list * (bool * term) list - val set_method : metID -> ptree * pos' -> ptree * ocalhd - val set_problem : pblID -> ptree * pos' -> ptree * ocalhd - val set_theory : thyID -> ptree * pos' -> ptree * ocalhd - val tryrefine : pblID -> ptree -> pos' -> bool * pblID * term * itm list * (bool * term) list + val initcontext_met : Ctree.ptree -> Ctree.pos' -> bool * string list * scr * itm list * (bool * term) list + val initcontext_pbl : Ctree.ptree -> Ctree.pos' -> bool * string list * term * itm list * (bool * term) list + val context_met : metID -> Ctree.ptree -> Ctree.pos -> bool * metID * scr * itm list * (bool * term) list + val context_pbl : pblID -> Ctree.ptree -> Ctree.pos -> bool * pblID * term * itm list * (bool * term) list + val set_method : metID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd + val set_problem : pblID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd + val set_theory : thyID -> Ctree.ptree * Ctree.pos' -> Ctree.ptree * Ctree.ocalhd + val tryrefine : pblID -> Ctree.ptree -> Ctree.pos' -> bool * pblID * term * itm list * (bool * term) list (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) type nxt_ type lOc_ - val CalcTreeTEST : fmz list -> pos' * NEW * Generate.mout * (string * tac) * safe * ptree + val CalcTreeTEST : Ctree.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Ctree.tac) * Ctree.safe * Ctree.ptree val f2str : Generate.mout -> cterm' - val loc_solve_ : string * tac_ -> ptree * (pos * pos_) -> lOc_ + val loc_solve_ : string * Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> lOc_ + val loc_specify_ : Ctree.tac_ -> Ctree.ptree * Ctree.pos' -> lOc_ ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) end @@ -41,10 +43,10 @@ struct (**) -fun get_pblID (pt, (p, _):pos') = - let val p' = par_pblobj pt p - val (_, pI, _) = get_obj g_spec pt p' - val (_, (_, oI, _), _) = get_obj g_origin pt p' +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 then SOME pI @@ -52,7 +54,7 @@ if oI <> e_pblID then SOME oI else NONE end; (* introduced for test only *) -val e_tac_ = Tac_ (Pure.thy, "", "", ""); +val e_tac_ = Ctree.Tac_ (Pure.thy, "", "", ""); datatype lOc_ = ERror of string (*after loc_specify, loc_solve*) | UNsafe of Chead.calcstate' (*after loc_specify, loc_solve*) @@ -96,7 +98,7 @@ (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*) | UNsafe cs' => ("unsafe-ok", cs') | Updated (cs' as (_, _, (_, p'))) => (*ev.SEVER.tacs like Begin_Trans*) - (if p' = ([],Res) then "end-of-calculation" else "ok", cs') + (if p' = ([], Ctree.Res) then "end-of-calculation" else "ok", cs') (*for SEVER.tacs user to ask ? *) end end @@ -106,16 +108,16 @@ fun nxt_specify_ (ptp as (pt, (p, p_))) = let val (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) = - case get_obj I pt p of - pblobj as (PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _), + case Ctree.get_obj I pt p of + pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _), probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) - | PrfObj _ => error "nxt_specify_: not on PrfObj" + | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj" in - if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin + if Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin then case mI' of - ["no_met"] => Chead.nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl)) - | _ => Chead.nxt_specif Model_Problem (pt, (p,Pbl)) + ["no_met"] => Chead.nxt_specif (Ctree.Refine_Tacitly pI') (pt, (p, Ctree.Pbl)) + | _ => Chead.nxt_specif Ctree.Model_Problem (pt, (p, Ctree.Pbl)) else let val cpI = if pI = e_pblID then pI' else pI; @@ -128,67 +130,67 @@ Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI) in case tac of - Apply_Method mI => - Solve.nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp + Ctree.Apply_Method mI => + Solve.nxt_solv (Ctree.Apply_Method' (mI, NONE, Ctree.e_istate, Ctree.e_ctxt)) (Ctree.e_istate, Ctree.e_ctxt) ptp | _ => Chead.nxt_specif tac ptp end end (* specify a new method; WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' *) -fun set_method (mI:metID) ptp = +fun set_method mI ptp = let val (mits, pt, p) = - case Chead.nxt_specif (Specify_Method mI) ptp of - ([(_, Specify_Method' (_, _, mits), _)], [], (pt, (p,_))) => (mits, pt, p) + case Chead.nxt_specif (Ctree.Specify_Method mI) ptp of + ([(_, Ctree.Specify_Method' (_, _, mits), _)], [], (pt, (p,_))) => (mits, pt, p) | _ => error "set_method: case 1 uncovered" val pre = [] (*...from Specify_Method'*) val complete = true (*...from Specify_Method'*) (*from Specify_Method' ? vvv, vvv ?*) val (hdf, spec) = - case get_obj I pt p of - PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec) - | PrfObj _ => error "set_method: case 2 uncovered" + case Ctree.get_obj I pt p of + Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec) + | Ctree.PrfObj _ => error "set_method: case 2 uncovered" in - (pt, (complete, Met, hdf, mits, pre, spec) : ocalhd) + (pt, (complete, Ctree.Met, hdf, mits, pre, spec) : Ctree.ocalhd) end (* specify a new problem; WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' *) -fun set_problem pI (ptp: ptree * pos') = +fun set_problem pI ptp = let val (complete, pits, pre, pt, p) = - case Chead.nxt_specif (Specify_Problem pI) ptp of - ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)], _, (pt, (p,_))) + case Chead.nxt_specif (Ctree.Specify_Problem pI) ptp of + ([(_, Ctree.Specify_Problem' (_, (complete, (pits, pre))),_)], _, (pt, (p,_))) => (complete, pits, pre, pt, p) | _ => error "set_problem: case 1 uncovered" (*from Specify_Problem' ? vvv, vvv ?*) val (hdf, spec) = - case get_obj I pt p of - PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec) - | PrfObj _ => error "set_problem: case 2 uncovered" + case Ctree.get_obj I pt p of + Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec) + | Ctree.PrfObj _ => error "set_problem: case 2 uncovered" in - (pt, (complete, Pbl, hdf, pits, pre, spec) : ocalhd) + (pt, (complete, Ctree.Pbl, hdf, pits, pre, spec) : Ctree.ocalhd) end -fun set_theory (tI:thyID) (ptp: ptree * pos') = +fun set_theory tI ptp = let val (complete, pits, pre, pt, p) = - case Chead.nxt_specif (Specify_Theory tI) ptp of - ([(_, Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _))) + case Chead.nxt_specif (Ctree.Specify_Theory tI) ptp of + ([(_, Ctree.Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _))) => (complete, pits, pre, pt, p) | _ => error "set_theory: case 1 uncovered" (*from Specify_Theory' ? vvv, vvv ?*) val (hdf, spec) = - case get_obj I pt p of - PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec) - | PrfObj _ => error "set_theory: case 2 uncovered" - in (pt, (complete, Pbl, hdf, pits, pre, spec) : ocalhd) end; + case Ctree.get_obj I pt p of + Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec) + | Ctree.PrfObj _ => error "set_theory: case 2 uncovered" + in (pt, (complete, Ctree.Pbl, hdf, pits, pre, spec) : Ctree.ocalhd) end; (* does a step forward; returns tactic used, ctree updated. TODO.WN0512 redesign after specify-phase became more separated from solve-phase *) -fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis): Chead.calcstate) = +fun step (ip as (_, p_)) (ptp as (pt,p), tacis) = let val pIopt = get_pblID (pt,ip); in - if ip = ([],Res) + if ip = ([], Ctree.Res) then ("end-of-calculation", (tacis, [], ptp): Chead.calcstate') else case tacis of @@ -197,7 +199,7 @@ then let val (pt',c',p') = Generate.generate tacis (pt,[],p) in ("ok", (tacis, c', (pt', p'))) end - else (case (if member op = [Pbl, Met] p_ + else (case (if member op = [Ctree.Pbl, Ctree.Met] p_ then nxt_specify_ (pt, ip) else Solve.nxt_solve_ (pt, ip)) handle ERROR msg => (writeln ("*** " ^ msg); ([], [], ptp)) (*e.g. Add_Given "equality///"*) of @@ -206,7 +208,7 @@ | _ => (case pIopt of NONE => ("no-fmz-spec", ([], [], ptp)) | SOME _ => (*vvvvvv: Apply_Method without init_form*) - (case if member op = [Pbl,Met] p_ andalso is_none (get_obj g_env pt (fst p)) + (case if member op = [Ctree.Pbl, Ctree.Met] p_ andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) then nxt_specify_ (pt, ip) else (Solve.nxt_solve_ (pt,ip)) handle ERROR msg => (writeln ("*** " ^ msg); @@ -234,12 +236,12 @@ else (str, c@c', ptp) end (* handles autoord <= 3, autoord > 3 handled by all_solve, complete_solve *) | autocalc c (pos as (_, p_)) ((pt, _), _(*tacis could help 1x in solve*)) auto = - if Solve.autoord auto > 3 andalso just_created (pt, pos) + if Solve.autoord auto > 3 andalso Ctree.just_created (pt, pos) then let val ptp = Chead.all_modspec (pt, pos); in Solve.all_solve auto c ptp end (*... auto = 4 | 5 | 6 *) else - if member op = [Pbl, Met] p_ + if member op = [Ctree.Pbl, Ctree.Met] p_ then if not (Chead.is_complete_mod (pt, pos)) then @@ -271,10 +273,10 @@ fun initcontext_pbl pt (p, _) = let val (probl, os, pI, hdl, pI') = - case get_obj I pt p of - PblObj {probl, origin = (os, (_, pI, _), hdl), spec=(_, pI', _), ...} + case Ctree.get_obj I pt p of + Ctree.PblObj {probl, origin = (os, (_, pI, _), hdl), spec=(_, pI', _), ...} => (probl, os, pI, hdl, pI') - | PrfObj _ => error "initcontext_pbl: uncovered case" + | Ctree.PrfObj _ => error "initcontext_pbl: uncovered case" val pblID = if pI' = e_pblID then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI) @@ -288,9 +290,9 @@ fun initcontext_met pt (p,_) = let val (meth, os, mI, mI') = - case get_obj I pt p of - PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI') - | PrfObj _ => error "initcontext_met: uncovered case" + 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 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI) else mI' @@ -301,24 +303,24 @@ end (* match the model of a problem at pos p with the model-pattern of the problem with pblID *) -fun context_pbl pI pt (p:pos) = +fun context_pbl pI pt p = let val (probl, os, hdl) = - case get_obj I pt p of - PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl) - | PrfObj _ => error "context_pbl: uncovered case" + 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 in (model_ok, pI, hdl, pbl, pre) end -fun context_met mI pt (p:pos) = +fun context_met mI pt p = let val (meth, os) = - case get_obj I pt p of - PblObj {meth, origin = (os, _, _),...} => (meth, os) - | PrfObj _ => error "context_met: uncovered case" + 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 in @@ -328,9 +330,9 @@ fun tryrefine pI pt (p,_) = let val (probl, os, hdl) = - case get_obj I pt p of - PblObj {probl, origin = (os, _, hdl), ...} => (probl, os, hdl) - | PrfObj _ => error "context_met: uncovered case" + 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 NONE => (*copy from context_pbl*) @@ -343,17 +345,17 @@ | SOME (pI, (pbl, pre)) => (true, pI, hdl, pbl, pre) end -fun detailstep pt (pos as (p, _):pos') = +fun detailstep pt (pos as (p, _)) = let - val nd = get_nd pt p - val cn = children nd + val nd = Ctree.get_nd pt p + val cn = Ctree.children nd in if null cn then - if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)] + if (Ctree.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)] then Solve.detailrls pt pos - else ("no-Rewrite_Set...", EmptyPtree, e_pos') - else ("donesteps", pt, (p @ [length (children (get_nd pt p))], Res)) + else ("no-Rewrite_Set...", Ctree.EmptyPtree, Ctree.e_pos') + else ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Ctree.Res)) end; @@ -368,8 +370,8 @@ val (form, _, _) = Chead.pt_extract ptp in case form of - Form t => Generate.FormKF (term2str t) - | ModSpec (_, p_, _, gfr, pre, _) => + Ctree.Form t => Generate.FormKF (term2str t) + | Ctree.ModSpec (_, p_, _, gfr, pre, _) => Generate.PpcKF ( (case p_ of Pbl => Generate.Problem [] | Met => Generate.Method [] | _ => error "TESTg_form: uncovered case", @@ -381,9 +383,9 @@ fun CalcTreeTEST [(fmz, sp)] = let val ((pt, p), tacis) = Chead.nxt_specify_init_calc (fmz, sp) - val tac = case tacis of [] => Empty_Tac | _ => (#1 o hd) tacis + val tac = case tacis of [] => Ctree.Empty_Tac | _ => (#1 o hd) tacis val f = TESTg_form (pt,p) - in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end + in (p, []:NEW, f, (Ctree.tac2IDstr tac, tac), Ctree.Sundef, pt) end | CalcTreeTEST _ = error "CalcTreeTEST: uncovered case" (*for tests > 15.8.03 after separation setnexttactic / nextTac: @@ -406,7 +408,7 @@ | ("failure", _) => error "sys-error" | _ => error "me: uncovered case" val (_, ts) = - (case step p ((pt, e_pos'),[]) of + (case step p ((pt, Ctree.e_pos'),[]) of ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts) | ("helpless", _) => ("helpless: cannot propose tac", []) | ("no-fmz-spec", _) => error "no-fmz-spec" @@ -416,9 +418,9 @@ val tac = case ts of tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end - | _ => if p = ([], Res) then End_Proof' else Empty_Tac; + | _ => if p = ([], Ctree.Res) then Ctree.End_Proof' else Ctree.Empty_Tac; in (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *), - (tac2IDstr tac, tac): Solve.tac'_, Sundef, pt) + (Ctree.tac2IDstr tac, tac), Ctree.Sundef, pt) end (* for quick test-print-out, until 'type inout' is removed *)