neuper@37906: (* The _functional_ mathematics engine, ie. without a state. neuper@37906: Input and output are Isabelle's formulae as strings. neuper@37906: authors: Walther Neuper 2000 neuper@37906: (c) due to copyright terms neuper@37906: neuper@37906: use"mathengine.sml"; neuper@37906: *) neuper@37906: wneuper@59261: signature MATH_ENGINE = wneuper@59261: sig wneuper@59261: type NEW (* TODO: refactor "fun me" with calcstate and remove *) wneuper@59279: val me : Solve.tac'_ -> Ctree.pos' -> NEW -> Ctree.ctree -> Ctree.pos' * NEW * Generate.mout * Solve.tac'_ * Ctree.safe * Ctree.ctree wneuper@59261: val autocalc : wneuper@59279: Ctree.pos' list -> Ctree.pos' -> (Ctree.ctree * Ctree.pos') * Generate.taci list -> Solve.auto -> string * Ctree.pos' list * (Ctree.ctree * Ctree.pos') wneuper@59261: val locatetac : wneuper@59279: Ctree.tac -> Ctree.ctree * Ctree.pos' -> string * (Generate.taci list * Ctree.pos' list * (Ctree.ctree * Ctree.pos')) wneuper@59276: val step : Ctree.pos' -> Chead.calcstate -> string * Chead.calcstate' wneuper@59261: val detailstep : wneuper@59279: Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos' wneuper@59279: val get_pblID : Ctree.ctree * Ctree.pos' -> pblID option neuper@37906: wneuper@59279: val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * scr * itm list * (bool * term) list wneuper@59279: val initcontext_pbl : Ctree.ctree -> Ctree.pos' -> bool * string list * term * itm list * (bool * term) list wneuper@59279: val context_met : metID -> Ctree.ctree -> Ctree.pos -> bool * metID * scr * itm list * (bool * term) list wneuper@59279: val context_pbl : pblID -> Ctree.ctree -> Ctree.pos -> bool * pblID * term * itm list * (bool * term) list wneuper@59279: val set_method : metID -> Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.ocalhd wneuper@59279: val set_problem : pblID -> Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.ocalhd wneuper@59279: val set_theory : thyID -> Ctree.ctree * Ctree.pos' -> Ctree.ctree * Ctree.ocalhd wneuper@59279: val tryrefine : pblID -> Ctree.ctree -> Ctree.pos' -> bool * pblID * term * itm list * (bool * term) list neuper@37906: wneuper@59261: (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) wneuper@59261: type nxt_ wneuper@59261: type lOc_ wneuper@59279: val CalcTreeTEST : Ctree.fmz list -> Ctree.pos' * NEW * Generate.mout * (string * Ctree.tac) * Ctree.safe * Ctree.ctree wneuper@59271: val f2str : Generate.mout -> cterm' wneuper@59279: val loc_solve_ : string * Ctree.tac_ -> Ctree.ctree * Ctree.pos' -> lOc_ wneuper@59279: val loc_specify_ : Ctree.tac_ -> Ctree.ctree * Ctree.pos' -> lOc_ wneuper@59261: ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*) wneuper@59261: end neuper@37906: wneuper@59261: (**) wneuper@59261: structure Math_Engine(**): MATH_ENGINE(**) = wneuper@59261: struct wneuper@59261: (**) neuper@37906: wneuper@59276: fun get_pblID (pt, (p, _): Ctree.pos') = wneuper@59276: let val p' = Ctree.par_pblobj pt p wneuper@59276: val (_, pI, _) = Ctree.get_obj Ctree.g_spec pt p' wneuper@59276: val (_, (_, oI, _), _) = Ctree.get_obj Ctree.g_origin pt p' wneuper@59261: in wneuper@59261: if pI <> e_pblID wneuper@59261: then SOME pI wneuper@59261: else wneuper@59261: if oI <> e_pblID then SOME oI else NONE end; neuper@37906: wneuper@59261: (* introduced for test only *) wneuper@59276: val e_tac_ = Ctree.Tac_ (Pure.thy, "", "", ""); neuper@37906: datatype lOc_ = wneuper@59265: ERror of string (*after loc_specify, loc_solve*) wneuper@59265: | UNsafe of Chead.calcstate' (*after loc_specify, loc_solve*) wneuper@59265: | Updated of Chead.calcstate' (*after loc_specify, loc_solve*) wneuper@59261: neuper@37906: fun loc_specify_ m (pt,pos) = wneuper@59261: let wneuper@59265: val (p, _, f, _, _, pt) = Chead.specify m pos [] pt; wneuper@59261: in wneuper@59271: case f of (Generate.Error' e) => ERror e | _ => Updated ([], [], (pt,p)) wneuper@59261: end neuper@37906: wneuper@59261: (* TODO push return-value cs' into solve and rename solve->loc_solve?_? *) wneuper@59261: fun loc_solve_ m (pt, pos) = wneuper@59261: let wneuper@59273: val (msg, cs') = Solve.solve m (pt, pos); wneuper@59261: in wneuper@59261: case msg of "ok" => Updated cs' | msg => ERror msg wneuper@59261: end neuper@37906: neuper@37906: datatype nxt_ = wneuper@59261: HElpless (**) wneuper@59265: | Nexts of Chead.calcstate (**) neuper@37906: wneuper@59261: (* locate a tactic in a script and apply it if possible; wneuper@59261: report of tacs' applicability in tacis; pt is dropped in setNextTactic*) wneuper@59261: fun locatetac _ (ptp as (_, ([], Res))) = ("end-of-calculation", ([], [], ptp)) neuper@37906: | locatetac tac (ptp as (pt, p)) = wneuper@59261: let wneuper@59273: val (mI, m) = Solve.mk_tac'_ tac; wneuper@59261: in wneuper@59272: case Applicable.applicable_in p pt m of wneuper@59265: Chead.Notappl _ => ("not-applicable", ([],[], ptp): Chead.calcstate') wneuper@59265: | Chead.Appl m => wneuper@59261: let wneuper@59273: val x = if member op = Solve.specsteps mI wneuper@59261: then loc_specify_ m ptp else loc_solve_ (mI,m) ptp wneuper@59261: in wneuper@59261: case x of wneuper@59261: ERror _ => ("failure", ([], [], ptp)) wneuper@59261: (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*) wneuper@59261: | UNsafe cs' => ("unsafe-ok", cs') wneuper@59261: | Updated (cs' as (_, _, (_, p'))) => (*ev.SEVER.tacs like Begin_Trans*) wneuper@59276: (if p' = ([], Ctree.Res) then "end-of-calculation" else "ok", cs') wneuper@59261: (*for SEVER.tacs user to ask ? *) wneuper@59261: end wneuper@59261: end neuper@37906: wneuper@59261: (* iterated by nxt_me; there (the resulting) ptp dropped wneuper@59261: may call nxt_solve Apply_Method --- thus evaluated here after solve.sml *) wneuper@59261: fun nxt_specify_ (ptp as (pt, (p, p_))) = wneuper@59261: let wneuper@59261: val (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) = wneuper@59276: case Ctree.get_obj I pt p of wneuper@59276: pblobj as (Ctree.PblObj {meth, origin = origin as (oris, (dI', pI', mI'), _), wneuper@59261: probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) wneuper@59276: | Ctree.PrfObj _ => error "nxt_specify_: not on PrfObj" neuper@41973: in wneuper@59276: if Ctree.just_created_ pblobj (*by Subproblem*) andalso origin <> Ctree.e_origin neuper@41973: then neuper@41973: case mI' of wneuper@59276: ["no_met"] => Chead.nxt_specif (Ctree.Refine_Tacitly pI') (pt, (p, Ctree.Pbl)) wneuper@59276: | _ => Chead.nxt_specif Ctree.Model_Problem (pt, (p, Ctree.Pbl)) neuper@41973: else neuper@41973: let neuper@41973: val cpI = if pI = e_pblID then pI' else pI; wneuper@59261: val cmI = if mI = e_metID then mI' else mI; wneuper@59269: val {ppc, prls, where_, ...} = Specify.get_pbt cpI; wneuper@59261: val pre = check_preconds "thy 100820" prls where_ probl; wneuper@59261: val pb = foldl and_ (true, map fst pre); wneuper@59261: (*FIXME.WN0308: ~~~~~: just check true in itms of pbl/met?*) wneuper@59261: val (_, tac) = wneuper@59269: Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI) wneuper@59261: in wneuper@59261: case tac of wneuper@59276: Ctree.Apply_Method mI => wneuper@59276: Solve.nxt_solv (Ctree.Apply_Method' (mI, NONE, Ctree.e_istate, Ctree.e_ctxt)) (Ctree.e_istate, Ctree.e_ctxt) ptp wneuper@59265: | _ => Chead.nxt_specif tac ptp wneuper@59261: end wneuper@59261: end neuper@37906: wneuper@59261: (* specify a new method; WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' *) wneuper@59276: fun set_method mI ptp = wneuper@59261: let wneuper@59261: val (mits, pt, p) = wneuper@59276: case Chead.nxt_specif (Ctree.Specify_Method mI) ptp of wneuper@59276: ([(_, Ctree.Specify_Method' (_, _, mits), _)], [], (pt, (p,_))) => (mits, pt, p) wneuper@59261: | _ => error "set_method: case 1 uncovered" wneuper@59261: val pre = [] (*...from Specify_Method'*) wneuper@59261: val complete = true (*...from Specify_Method'*) wneuper@59261: (*from Specify_Method' ? vvv, vvv ?*) wneuper@59261: val (hdf, spec) = wneuper@59276: case Ctree.get_obj I pt p of wneuper@59276: Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec) wneuper@59276: | Ctree.PrfObj _ => error "set_method: case 2 uncovered" wneuper@59261: in wneuper@59276: (pt, (complete, Ctree.Met, hdf, mits, pre, spec) : Ctree.ocalhd) wneuper@59261: end neuper@37906: wneuper@59261: (* specify a new problem; WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' *) wneuper@59276: fun set_problem pI ptp = wneuper@59261: let wneuper@59261: val (complete, pits, pre, pt, p) = wneuper@59276: case Chead.nxt_specif (Ctree.Specify_Problem pI) ptp of wneuper@59276: ([(_, Ctree.Specify_Problem' (_, (complete, (pits, pre))),_)], _, (pt, (p,_))) wneuper@59261: => (complete, pits, pre, pt, p) wneuper@59261: | _ => error "set_problem: case 1 uncovered" wneuper@59261: (*from Specify_Problem' ? vvv, vvv ?*) wneuper@59261: val (hdf, spec) = wneuper@59276: case Ctree.get_obj I pt p of wneuper@59276: Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec) wneuper@59276: | Ctree.PrfObj _ => error "set_problem: case 2 uncovered" wneuper@59261: in wneuper@59276: (pt, (complete, Ctree.Pbl, hdf, pits, pre, spec) : Ctree.ocalhd) wneuper@59261: end neuper@37906: wneuper@59276: fun set_theory tI ptp = wneuper@59261: let wneuper@59261: val (complete, pits, pre, pt, p) = wneuper@59276: case Chead.nxt_specif (Ctree.Specify_Theory tI) ptp of wneuper@59276: ([(_, Ctree.Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _))) wneuper@59261: => (complete, pits, pre, pt, p) wneuper@59261: | _ => error "set_theory: case 1 uncovered" wneuper@59261: (*from Specify_Theory' ? vvv, vvv ?*) wneuper@59261: val (hdf, spec) = wneuper@59276: case Ctree.get_obj I pt p of wneuper@59276: Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec) wneuper@59276: | Ctree.PrfObj _ => error "set_theory: case 2 uncovered" wneuper@59276: in (pt, (complete, Ctree.Pbl, hdf, pits, pre, spec) : Ctree.ocalhd) end; neuper@37906: neuper@41981: (* does a step forward; returns tactic used, ctree updated. wneuper@59261: TODO.WN0512 redesign after specify-phase became more separated from solve-phase *) wneuper@59276: fun step (ip as (_, p_)) (ptp as (pt,p), tacis) = neuper@41972: let val pIopt = get_pblID (pt,ip); neuper@41972: in wneuper@59276: if ip = ([], Ctree.Res) wneuper@59265: then ("end-of-calculation", (tacis, [], ptp): Chead.calcstate') neuper@41972: else neuper@41972: case tacis of wneuper@59261: (_::_) => neuper@41972: if ip = p (*the request is done where ptp waits for*) wneuper@59261: then wneuper@59271: let val (pt',c',p') = Generate.generate tacis (pt,[],p) wneuper@59261: in ("ok", (tacis, c', (pt', p'))) end wneuper@59276: else (case (if member op = [Ctree.Pbl, Ctree.Met] p_ wneuper@59273: then nxt_specify_ (pt, ip) else Solve.nxt_solve_ (pt, ip)) wneuper@59261: handle ERROR msg => (writeln ("*** " ^ msg); wneuper@59261: ([], [], ptp)) (*e.g. Add_Given "equality///"*) of wneuper@59261: cs as ([],_,_) => ("helpless", cs) wneuper@59261: | cs => ("ok", cs)) wneuper@59261: | _ => (case pIopt of wneuper@59261: NONE => ("no-fmz-spec", ([], [], ptp)) wneuper@59261: | SOME _ => (*vvvvvv: Apply_Method without init_form*) wneuper@59276: (case if member op = [Ctree.Pbl, Ctree.Met] p_ andalso is_none (Ctree.get_obj Ctree.g_env pt (fst p)) wneuper@59261: then nxt_specify_ (pt, ip) wneuper@59273: else (Solve.nxt_solve_ (pt,ip)) wneuper@59261: handle ERROR msg => (writeln ("*** " ^ msg); wneuper@59261: ([],[],ptp)) (*e.g. Add_Given "equality///"*) of wneuper@59261: cs as ([],_,_) =>("helpless", cs) (*FIXXME del.handle*) wneuper@59261: | cs => ("ok", cs))) wneuper@59261: end neuper@37906: wneuper@59261: (* does several steps within one calculation as given by "type auto"; neuper@37906: the steps may arbitrarily go into and leave different phases, wneuper@59261: i.e. specify-phase and solve-phase wneuper@59261: TODO.WN0512 ? redesign after the phases have been more separated wneuper@59261: at the fron-end in 05: wneuper@59261: eg. CompleteCalcHead could be done by a separate fun !!!*) wneuper@59273: fun autocalc c ip cs (Solve.Step s) = neuper@37906: if s <= 1 wneuper@59261: then wneuper@59261: let val (str, (_, c', ptp)) = step ip cs; (* autoord = 1, probably does 1 step too much*) wneuper@59261: in (str, c@c', ptp) end wneuper@59261: else wneuper@59261: let val (str, (_, c', ptp as (_, p))) = step ip cs; wneuper@59261: in wneuper@59261: if str = "ok" wneuper@59273: then autocalc (c@c') p (ptp, []) (Solve.Step (s - 1)) wneuper@59261: else (str, c@c', ptp) end wneuper@59261: (* handles autoord <= 3, autoord > 3 handled by all_solve, complete_solve *) wneuper@59261: | autocalc c (pos as (_, p_)) ((pt, _), _(*tacis could help 1x in solve*)) auto = wneuper@59276: if Solve.autoord auto > 3 andalso Ctree.just_created (pt, pos) wneuper@59261: then wneuper@59265: let val ptp = Chead.all_modspec (pt, pos); wneuper@59273: in Solve.all_solve auto c ptp end (*... auto = 4 | 5 | 6 *) wneuper@59261: else wneuper@59276: if member op = [Ctree.Pbl, Ctree.Met] p_ wneuper@59261: then wneuper@59265: if not (Chead.is_complete_mod (pt, pos)) wneuper@59261: then wneuper@59265: let val ptp = Chead.complete_mod (pt, pos) (*... auto = 2 | 3 *) wneuper@59261: in wneuper@59273: if Solve.autoord auto < 3 then ("ok", c, ptp) wneuper@59261: else wneuper@59265: if not (Chead.is_complete_spec ptp) wneuper@59261: then wneuper@59265: let val ptp = Chead.complete_spec ptp wneuper@59261: in wneuper@59273: if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp wneuper@59261: end wneuper@59273: else if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp wneuper@59261: end wneuper@59261: else wneuper@59265: if not (Chead.is_complete_spec (pt,pos)) wneuper@59261: then wneuper@59265: let val ptp = Chead.complete_spec (pt, pos) wneuper@59261: in wneuper@59273: if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp wneuper@59261: end wneuper@59261: else wneuper@59273: if Solve.autoord auto = 3 then ("ok", c, (pt, pos)) else Solve.all_solve auto c (pt, pos) wneuper@59273: else Solve.complete_solve auto c (pt, pos); neuper@37906: neuper@37906: (*.initialiye matching; before 'tryMatch' get the pblID to match with: neuper@37906: if no pbl has been specified, take the init from origin.*) wneuper@59261: fun initcontext_pbl pt (p, _) = wneuper@59261: let wneuper@59261: val (probl, os, pI, hdl, pI') = wneuper@59276: case Ctree.get_obj I pt p of wneuper@59276: Ctree.PblObj {probl, origin = (os, (_, pI, _), hdl), spec=(_, pI', _), ...} wneuper@59261: => (probl, os, pI, hdl, pI') wneuper@59276: | Ctree.PrfObj _ => error "initcontext_pbl: uncovered case" wneuper@59261: val pblID = wneuper@59261: if pI' = e_pblID wneuper@59261: then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI) wneuper@59261: else pI' wneuper@59269: val {ppc, where_, prls, ...} = Specify.get_pbt pblID wneuper@59269: val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os wneuper@59261: in wneuper@59261: (model_ok, pblID, hdl, pbl, pre) wneuper@59261: end neuper@37906: wneuper@59261: fun initcontext_met pt (p,_) = wneuper@59261: let wneuper@59261: val (meth, os, mI, mI') = wneuper@59276: case Ctree.get_obj I pt p of wneuper@59276: Ctree.PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI') wneuper@59276: | Ctree.PrfObj _ => error "initcontext_met: uncovered case" wneuper@59261: val metID = if mI' = e_metID wneuper@59261: then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI) wneuper@59261: else mI' wneuper@59269: val {ppc, pre, prls, scr, ...} = Specify.get_met metID wneuper@59269: val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os wneuper@59261: in wneuper@59261: (model_ok, metID, scr, pbl, pre) wneuper@59261: end neuper@37906: wneuper@59261: (* match the model of a problem at pos p with the model-pattern of the problem with pblID *) wneuper@59276: fun context_pbl pI pt p = wneuper@59261: let wneuper@59261: val (probl, os, hdl) = wneuper@59276: case Ctree.get_obj I pt p of wneuper@59276: Ctree.PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl) wneuper@59276: | Ctree.PrfObj _ => error "context_pbl: uncovered case" wneuper@59269: val {ppc,where_,prls,...} = Specify.get_pbt pI wneuper@59269: val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os wneuper@59261: in wneuper@59261: (model_ok, pI, hdl, pbl, pre) wneuper@59261: end neuper@37906: wneuper@59276: fun context_met mI pt p = wneuper@59261: let wneuper@59261: val (meth, os) = wneuper@59276: case Ctree.get_obj I pt p of wneuper@59276: Ctree.PblObj {meth, origin = (os, _, _),...} => (meth, os) wneuper@59276: | Ctree.PrfObj _ => error "context_met: uncovered case" wneuper@59269: val {ppc,pre,prls,scr,...} = Specify.get_met mI wneuper@59269: val (model_ok, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os wneuper@59261: in wneuper@59261: (model_ok, mI, scr, pbl, pre) wneuper@59261: end neuper@37906: wneuper@59261: fun tryrefine pI pt (p,_) = wneuper@59261: let wneuper@59261: val (probl, os, hdl) = wneuper@59276: case Ctree.get_obj I pt p of wneuper@59276: Ctree.PblObj {probl, origin = (os, _, hdl), ...} => (probl, os, hdl) wneuper@59276: | Ctree.PrfObj _ => error "context_met: uncovered case" wneuper@59261: in wneuper@59269: case Specify.refine_pbl (assoc_thy "Isac") pI probl of wneuper@59261: NONE => (*copy from context_pbl*) wneuper@59261: let wneuper@59269: val {ppc,where_,prls,...} = Specify.get_pbt pI wneuper@59269: val (_, (pbl, pre)) = Specify.match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os wneuper@59261: in wneuper@59261: (false, pI, hdl, pbl, pre) wneuper@59261: end wneuper@59261: | SOME (pI, (pbl, pre)) => (true, pI, hdl, pbl, pre) wneuper@59261: end neuper@37906: wneuper@59276: fun detailstep pt (pos as (p, _)) = neuper@55471: let wneuper@59276: val nd = Ctree.get_nd pt p wneuper@59276: val cn = Ctree.children nd neuper@55471: in neuper@55471: if null cn wneuper@59261: then wneuper@59276: if (Ctree.is_rewset o (Ctree.get_obj Ctree.g_tac nd)) [(*root of nd*)] wneuper@59273: then Solve.detailrls pt pos wneuper@59276: else ("no-Rewrite_Set...", Ctree.EmptyPtree, Ctree.e_pos') wneuper@59276: else ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Ctree.Res)) neuper@55471: end; neuper@37906: neuper@37906: wneuper@59261: (*** for mathematics authoring on sml-toplevel; no XML ***) neuper@37906: neuper@37906: type NEW = int list; neuper@37906: wneuper@59261: (* 15.8.03 for me with loc_specify/solve, nxt_specify/solve wneuper@59261: delete as soon as TESTg_form -> _mout_ dropped *) neuper@37906: fun TESTg_form ptp = wneuper@59261: let wneuper@59265: val (form, _, _) = Chead.pt_extract ptp wneuper@59261: in wneuper@59261: case form of wneuper@59276: Ctree.Form t => Generate.FormKF (term2str t) wneuper@59276: | Ctree.ModSpec (_, p_, _, gfr, pre, _) => wneuper@59271: Generate.PpcKF ( wneuper@59271: (case p_ of Pbl => Generate.Problem [] | Met => Generate.Method [] wneuper@59267: | _ => error "TESTg_form: uncovered case", wneuper@59269: Specify.itms2itemppc (assoc_thy"Isac") gfr pre)) wneuper@59267: end neuper@37906: wneuper@59261: (* create a calc-tree; for use within sml: thus "^^^" NOT decoded to "^" etc; wneuper@59261: compare "fun CalcTree" which DOES decode *) wneuper@59261: fun CalcTreeTEST [(fmz, sp)] = neuper@42011: let wneuper@59265: val ((pt, p), tacis) = Chead.nxt_specify_init_calc (fmz, sp) wneuper@59276: val tac = case tacis of [] => Ctree.Empty_Tac | _ => (#1 o hd) tacis neuper@42011: val f = TESTg_form (pt,p) wneuper@59276: in (p, []:NEW, f, (Ctree.tac2IDstr tac, tac), Ctree.Sundef, pt) end wneuper@59261: | CalcTreeTEST _ = error "CalcTreeTEST: uncovered case" neuper@37906: neuper@37906: (*for tests > 15.8.03 after separation setnexttactic / nextTac: neuper@37906: external view: me should be used by math-authors as done so far neuper@37906: internal view: loc_specify/solve, nxt_specify/solve used neuper@37906: i.e. same as in setnexttactic / nextTac*) neuper@37906: (*ENDE TESTPHASE 08/10.03: neuper@37906: NEW loeschen, eigene Version von locatetac, step neuper@37906: meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *) neuper@37906: wneuper@59261: fun me (_, tac) p _(*NEW remove*) pt = neuper@41972: let neuper@41972: val (pt, p) = neuper@41972: (*locatetac is here for testing by me; step would suffice in me*) neuper@37906: case locatetac tac (pt,p) of neuper@42305: ("ok", (_, _, ptp)) => ptp neuper@41972: | ("unsafe-ok", (_, _, ptp)) => ptp neuper@41972: | ("not-applicable",_) => (pt, p) neuper@41972: | ("end-of-calculation", (_, _, ptp)) => ptp wneuper@59261: | ("failure", _) => error "sys-error" wneuper@59261: | _ => error "me: uncovered case" neuper@42387: val (_, ts) = wneuper@59276: (case step p ((pt, Ctree.e_pos'),[]) of wneuper@59261: ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts) wneuper@59261: | ("helpless", _) => ("helpless: cannot propose tac", []) wneuper@59261: | ("no-fmz-spec", _) => error "no-fmz-spec" wneuper@59261: | ("end-of-calculation", (ts, _, _)) => ("", ts) wneuper@59261: | _ => error "me: uncovered case") wneuper@59261: handle ERROR msg => raise ERROR msg neuper@41972: val tac = neuper@41972: case ts of wneuper@59261: tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end wneuper@59276: | _ => if p = ([], Ctree.Res) then Ctree.End_Proof' else Ctree.Empty_Tac; wneuper@59261: in (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *), wneuper@59276: (Ctree.tac2IDstr tac, tac), Ctree.Sundef, pt) wneuper@59261: end neuper@37906: wneuper@59261: (* for quick test-print-out, until 'type inout' is removed *) wneuper@59271: fun f2str (Generate.FormKF cterm') = cterm'; neuper@37906: neuper@37906: end