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: 
neuper@37906: signature MATHENGINE =
neuper@37906:   sig
neuper@37906:     type nxt_
neuper@37906:     (* datatype nxt_ = HElpless | Nexts of CalcHead.calcstate *)
neuper@37906:     type NEW
neuper@37906:     type lOc_
neuper@37906:     (*datatype
neuper@37906:       lOc_ =
neuper@37906:           ERror of string
neuper@37906:         | UNsafe of CalcHead.calcstate'
neuper@37906:         | Updated of CalcHead.calcstate' *)
neuper@37906: 
neuper@37906:     val CalcTreeTEST :
neuper@37906:        fmz list ->
neuper@37906:        pos' * NEW * mout * (string * tac) * safe * ptree
neuper@37906: 
neuper@37906:     val TESTg_form : ptree * (int list * pos_) -> mout
neuper@37906:     val autocalc :
neuper@37906:        pos' list ->
neuper@37906:        pos' ->
neuper@37906:        (ptree * pos') * taci list ->
neuper@37906:        auto -> string * pos' list * (ptree * pos')
neuper@37906:     val detailstep : ptree -> pos' -> string * ptree * pos'
neuper@37906:    (* val e_tac_ : tac_ *)
neuper@37906:     val f2str : mout -> cterm'
neuper@37931:    (* val get_pblID : ptree * pos' -> pblID option *)
neuper@37906:     val initmatch : ptree -> pos' -> ptform
neuper@37906:    (* val loc_solve_ :
neuper@37906:        string * tac_ -> ptree * (int list * pos_) -> lOc_ *)
neuper@37906:    (* val loc_specify_ : tac_ -> ptree * pos' -> lOc_ *)
neuper@37906:     val locatetac :     (*tests only*)
neuper@37906:        tac ->
neuper@37906:        ptree * (posel list * pos_) ->
neuper@37906:        string * (taci list * pos' list * (ptree * (posel list * pos_)))
neuper@37906:     val me :
neuper@37906:        tac'_ ->
neuper@37906:        pos' ->
neuper@37906:        NEW ->
neuper@37906:        ptree -> pos' * NEW * mout * tac'_ * safe * ptree
neuper@37906: 
neuper@37906:     val nxt_specify_ : ptree * (int list * pos_) -> calcstate'(*tests only*)
neuper@37906:     val set_method : metID -> ptree * pos' -> ptree * ocalhd
neuper@37906:     val set_problem : pblID -> ptree * pos' -> ptree * ocalhd
neuper@37906:     val set_theory : thyID -> ptree * pos' -> ptree * ocalhd
neuper@37906:     val step : pos' -> calcstate -> string * calcstate'
neuper@37906:     val trymatch : pblID -> ptree -> pos' -> ptform
neuper@37906:     val tryrefine : pblID -> ptree -> pos' -> ptform
neuper@37906:   end
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (*------------------------------------------------------------------(**)
neuper@37906: structure MathEngine : MATHENGINE =
neuper@37906: struct
neuper@37906: (**)------------------------------------------------------------------*)
neuper@37906: 
neuper@37906: fun get_pblID (pt, (p,_):pos') =
neuper@37906:     let val p' = par_pblobj pt p
neuper@37906: 	val (_,pI,_) = get_obj g_spec pt p'
neuper@37906: 	val (_,(_,oI,_),_) = get_obj g_origin pt p'
neuper@37926:     in if pI <> e_pblID then SOME pI
neuper@37926:        else if oI <> e_pblID then SOME oI
neuper@37926:        else NONE end;
neuper@37906: (*fun get_pblID (pt, (p,_):pos') =
neuper@37906:     ((snd3 o (get_obj g_spec pt)) (par_pblobj pt p));*)
neuper@37906: 
neuper@37906: 
neuper@37906: (*--vvv--dummies for test*)
neuper@37906: val e_tac_ = Tac_ (Pure.thy,"","","");
neuper@37906: datatype lOc_ =
neuper@37906:   ERror of string         (*after loc_specify, loc_solve*)
neuper@37906: | UNsafe of calcstate'    (*after loc_specify, loc_solve*)
neuper@37906: | Updated of calcstate';   (*after loc_specify, loc_solve*)
neuper@37906: fun loc_specify_ m (pt,pos) =
neuper@37906: (* val pos = ip;
neuper@37906:    *)
neuper@37906:     let val (p,_,f,_,s,pt) = specify m pos [] pt;
neuper@37906: (*      val (_,_,_,_,_,pt')= specify m pos [] pt;
neuper@37906:    *) 
neuper@37906:    in case f of
neuper@37906: 	   (Error' (Error_ e)) => ERror e
neuper@37906: 	 | _ => Updated ([], [], (pt,p)) end;
neuper@37906: 
neuper@37906: (*. TODO push return-value cs' into solve and rename solve->loc_solve?_? .*)
neuper@37906: (* val (m, pos) = ((mI,m), ip);
neuper@37906:    val (m,(pt,pos) ) = ((mI,m), ptp);
neuper@37906:    *)  
neuper@37906: fun loc_solve_ m (pt,pos) =
neuper@37906:     let val (msg, cs') = solve m (pt, pos);
neuper@37906: (* val (tacis,dels,(pt',p')) = cs';
neuper@38015:    (tracing o istate2str) (get_istate pt' p');
neuper@37906:    (term2str o fst) (get_obj g_result pt' (fst p'));
neuper@37906:    *)
neuper@37906:     in case msg of
neuper@37906: 	   "ok" => Updated cs' 
neuper@37906: 	 | msg => ERror msg 
neuper@37906:     end;
neuper@37906: 
neuper@37906: datatype nxt_ =
neuper@37906: 	 HElpless  (**)
neuper@37906:        | Nexts of calcstate; (**)
neuper@37906: 
neuper@37906: (*. locate a tactic in a script and apply it if possible .*)
neuper@37906: (*report applicability of tac in tacis; pt is dropped in setNextTactic*)
neuper@37906: fun locatetac _ (ptp as (_,([],Res))) = ("end-of-calculation", ([], [], ptp))
neuper@37906:   | locatetac tac (ptp as (pt, p)) =
neuper@41975:       let val (mI,m) = mk_tac'_ tac;
neuper@41975:       in case applicable_in p pt m of
neuper@41975: 	         Notappl e => ("not-applicable", ([],[],  ptp):calcstate')
neuper@41975: 	       | Appl m =>
neuper@41975: 	           let 
neuper@41975:                val x = if member op = specsteps mI
neuper@41975: 		             then loc_specify_ m ptp else loc_solve_ (mI,m) ptp
neuper@41975: 	           in case x of 
neuper@41975: 		              ERror e => ("failure", ([], [], ptp))
neuper@41975: 		              (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)
neuper@41975: 		            | UNsafe cs' => ("unsafe-ok", cs')
neuper@41975: 		            | Updated (cs' as (_,_,(_,p'))) => (*ev.SEVER.tacs like Begin_Trans*)
neuper@41975: 		                (if p' = ([],Res) then "end-of-calculation" else "ok", cs')
neuper@41975:                     (*for SEVER.tacs  user to ask ? *)
neuper@41975: 	           end
neuper@41975:       end;
neuper@37906: 
neuper@37906: (*iterated by nxt_me; there (the resulting) ptp dropped
neuper@37906:   may call nxt_solve Apply_Method --- thus evaluated here after solve.sml*)
neuper@37906: fun nxt_specify_ (ptp as (pt, pos as (p,p_))) =
neuper@41973:   let val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),
neuper@41973: 			  probl,spec=(dI,pI,mI),...}) = get_obj I pt p;
neuper@41973:   in 
neuper@41973:     if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin
neuper@41973:     then 
neuper@41973:       case mI' of
neuper@41973: 	      ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))
neuper@41973:       | _ => nxt_specif Model_Problem (pt, (p,Pbl))
neuper@41973:     else 
neuper@41973:       let 
neuper@41973:         val cpI = if pI = e_pblID then pI' else pI;
neuper@41973: 		    val cmI = if mI = e_metID then mI' else mI;
neuper@41973: 		    val {ppc, prls, where_, ...} = get_pbt cpI;
neuper@41973: 		    val pre = check_preconds "thy 100820" prls where_ probl;
neuper@41973: 		    val pb = foldl and_ (true, map fst pre);
neuper@41973: 		    (*FIXME.WN0308:    ~~~~~: just check true in itms of pbl/met?*)
neuper@41973: 		    val (_,tac) = nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) 
neuper@41973: 			    (ppc, (#ppc o get_met) cmI) (dI, pI, mI);
neuper@37906: 	    in case tac of
neuper@41973: 		       Apply_Method mI => 
neuper@41973: 		         nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, e_ctxt) ptp
neuper@41973: 		     | _ => nxt_specif tac ptp end
neuper@41973:    end;
neuper@37906: 
neuper@37906: (*.specify a new method;
neuper@37906:    WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' .*)
neuper@37906: fun set_method (mI:metID) ptp =
neuper@37906:     let val ([(_, Specify_Method' (_, _, mits), _)], [], (pt, pos as (p,_))) = 
neuper@37906: 	    nxt_specif (Specify_Method mI) ptp
neuper@37906: 	val pre = []        (*...from Specify_Method'*)
neuper@37906: 	val complete = true (*...from Specify_Method'*)
neuper@37906: 	(*from Specify_Method'  ? vvv,  vvv ?*)
neuper@37906: 	val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
neuper@37906:     in (pt, (complete, Met, hdf, mits, pre, spec):ocalhd) end;
neuper@37906: 
neuper@37906: (*.specify a new problem;
neuper@37906:    WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' .*)
neuper@37906: fun set_problem pI (ptp: ptree * pos') =
neuper@37906:     let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)],
neuper@37906: 	     _, (pt, pos as (p,_))) = nxt_specif (Specify_Problem pI) ptp
neuper@37906: 	(*from Specify_Problem' ? vvv,  vvv ?*)
neuper@37906: 	val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
neuper@37906:     in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end;
neuper@37906: 
neuper@37906: fun set_theory (tI:thyID) (ptp: ptree * pos') =
neuper@37906:     let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)],
neuper@37906: 	     _, (pt, pos as (p,_))) = nxt_specif (Specify_Theory tI) ptp
neuper@37906: 	(*from Specify_Theory'  ? vvv,  vvv ?*)
neuper@37906: 	val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p
neuper@37906:     in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end;
neuper@37906: 
neuper@41981: (* does a step forward; returns tactic used, ctree updated.
neuper@41981: TODO.WN0512 redesign after specify-phase became more separated from solve-phase *)
neuper@37906: fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =
neuper@41972:   let val pIopt = get_pblID (pt,ip);
neuper@41972:   in
neuper@41972:     if (*p = ([],Res) orelse*) ip = ([],Res)
neuper@41972:     then ("end-of-calculation",(tacis, [], ptp):calcstate') 
neuper@41972:     else
neuper@41972:       case tacis of
neuper@41972: 	      (_::_) => 
neuper@41972:           if ip = p (*the request is done where ptp waits for*)
neuper@41972: 	        then 
neuper@41972:             let val (pt',c',p') = generate tacis (pt,[],p)
neuper@41972: 		        in ("ok", (tacis, c', (pt', p'))) end
neuper@41972: 	        else (case (if member op = [Pbl,Met] p_
neuper@41972: 		                  then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))
neuper@41972: 		                  handle _ => ([],[],ptp)(*e.g. Add_Given "equality///"*) of
neuper@41972: 		              cs as ([],_,_) => ("helpless", cs)
neuper@41972: 		            | cs => ("ok", cs))
neuper@41972: 	    | _ => (case pIopt of
neuper@41972: 		            NONE => ("no-fmz-spec", ([], [], ptp))
neuper@41972: 		          | SOME pI =>
neuper@41972: 		            (case (if member op = [Pbl,Met] p_
neuper@41972: 			                   andalso is_none (get_obj g_env pt (fst p))
neuper@41972: 			                        (*^^^^^^^^: Apply_Method without init_form*)
neuper@41982: 			                 then nxt_specify_ (pt, ip) 
neuper@41972:                        else nxt_solve_ (pt,ip) )
neuper@41972: 			                handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality///"*) of
neuper@41972: 		               cs as ([],_,_) =>("helpless", cs)(*FIXXMEdel.handle*)
neuper@41972: 			           | cs => ("ok", cs)))
neuper@41972:   end;
neuper@37906: 
neuper@37906: (*.does several steps within one calculation as given by "type auto";
neuper@37906:    the steps may arbitrarily go into and leave different phases, 
neuper@37906:    i.e. specify-phase and solve-phase.*)
neuper@37906: (*TODO.WN0512 ? redesign after the phases have been more separated
neuper@37906:   at the fron-end in 05: 
neuper@37906:   eg. CompleteCalcHead could be done by a separate fun !!!*)
neuper@37906: fun autocalc c ip (cs as (ptp as (_,p),tacis)) (Step s) =
neuper@37906:     if s <= 1
neuper@37906:     then let val (str, (_, c', ptp)) = step ip cs;(*1*)
neuper@37906: 	 (*at least does 1 step, ev.1 too much*)
neuper@37906: 	 in (str, c@c', ptp) end
neuper@37906:     else let val (str, (_, c', ptp as (_, p))) = step ip cs;
neuper@37906: 	 in if str = "ok" 
neuper@37906: 	    then autocalc (c@c') p (ptp,[]) (Step (s-1))
neuper@37906: 	    else (str, c@c', ptp) end
neuper@37906: (*handles autoord <= 3, autoord > 3 handled by all_/complete_solve*)
neuper@37906:   | autocalc c (pos as (_,p_)) ((pt,_), _(*tacis would help 1x in solve*))auto=
neuper@37906: (* val (c:pos' list, (pos as (_,p_)),((pt,_),_),auto) = 
neuper@37906:       ([], pold, get_calc cI, auto);
neuper@37906:    *)
neuper@37906:      if autoord auto > 3 andalso just_created (pt, pos)
neuper@37906:      then let val ptp = all_modspec (pt, pos);
neuper@37906: 	  in all_solve auto c ptp end
neuper@37906:      else
neuper@37939: 	 if member op = [Pbl, Met] p_
neuper@37939:  	 then if not (is_complete_mod (pt, pos))
neuper@37906: 	      then let val ptp = complete_mod (pt, pos)
neuper@37906: 		   in if autoord auto < 3 then ("ok", c, ptp)
neuper@37906: 		      else 
neuper@37906: 			  if not (is_complete_spec ptp)
neuper@37906: 			  then let val ptp = complete_spec ptp
neuper@37906: 			       in if autoord auto = 3 then ("ok", c, ptp)
neuper@37906: 				  else all_solve auto c ptp
neuper@37906: 			       end
neuper@37906: 			  else if autoord auto = 3 then ("ok", c, ptp)
neuper@37906: 			  else all_solve auto c ptp 
neuper@37906: 		   end
neuper@37906: 	      else 
neuper@37906: 		  if not (is_complete_spec (pt,pos))
neuper@37906: 		  then let val ptp = complete_spec (pt, pos)
neuper@37906: 		       in if autoord auto = 3 then ("ok", c, ptp)
neuper@37906: 			  else all_solve auto c ptp
neuper@37906: 		       end
neuper@37906: 		  else if autoord auto = 3 then ("ok", c, (pt, pos))
neuper@37906: 		  else all_solve auto c (pt, pos)
neuper@37906: 	 else complete_solve auto c (pt, pos);
neuper@37906: (* val pbl = get_obj g_pbl (fst ptp) [];
neuper@37906:    val (oris,_,_) = get_obj g_origin (fst ptp) [];
neuper@37906: *)    
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
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.*)
neuper@37906: (*fun initmatch pt (pos as (p,_):pos') =
neuper@37906:     let val PblObj {probl,origin=(os,(_,pI,_),_),spec=(dI',pI',mI'),...} = 
neuper@37906: 	    get_obj I pt p
neuper@37906: 	val pblID = if pI' = e_pblID 
neuper@37906: 		    then (*TODO.WN051125 (#init o get_pbt) pI          <<<*) 
neuper@37906: 			takelast (2, pI) (*FIXME.WN051125 a hack, impl.^^^*)
neuper@37906: 		    else pI'
neuper@37906: 	val spec = (dI',pblID,mI')
neuper@37906: 	val {ppc,where_,prls,...} = get_pbt pblID
neuper@37906: 	val (model_ok, (pbl, pre)) = 
neuper@38050: 	    match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
neuper@37906:     in ModSpec (ocalhd_complete pbl pre spec,
neuper@37906: 		Pbl, e_term, pbl, pre, spec) end;*)
neuper@37906: fun initcontext_pbl pt (pos as (p,_):pos') =
neuper@37906:     let val PblObj {probl,origin=(os,(_,pI,_),hdl),spec=(dI',pI',mI'),...} = 
neuper@37906: 	    get_obj I pt p
neuper@37906: 	val pblID = if pI' = e_pblID 
neuper@37906: 		    then (*TODO.WN051125 (#init o get_pbt) pI          <<<*) 
neuper@37906: 			takelast (2, pI) (*FIXME.WN051125 a hack, impl.^^^*)
neuper@37906: 		    else pI'
neuper@37906: 	val {ppc,where_,prls,...} = get_pbt pblID
neuper@37906: 	val (model_ok, (pbl, pre)) = 
neuper@38050: 	    match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
neuper@37906:     in (model_ok, pblID, hdl, pbl, pre) end;
neuper@37906: 
neuper@37906: fun initcontext_met pt (pos as (p,_):pos') =
neuper@37906:     let val PblObj {meth,origin=(os,(_,_,mI), _),spec=(_, _, mI'),...} = 
neuper@37906: 	    get_obj I pt p
neuper@37906: 	val metID = if mI' = e_metID 
neuper@37906: 		    then (*TODO.WN051125 (#init o get_pbt) pI          <<<*) 
neuper@37906: 			takelast (2, mI) (*FIXME.WN051125 a hack, impl.^^^*)
neuper@37906: 		    else mI'
neuper@37906: 	val {ppc,pre,prls,scr,...} = get_met metID
neuper@37906: 	val (model_ok, (pbl, pre)) = 
neuper@38050: 	    match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
neuper@37906:     in (model_ok, metID, scr, pbl, pre) end;
neuper@37906: 
neuper@37906: (*.match the model of a problem at pos p 
neuper@37906:    with the model-pattern of the problem with pblID*)
neuper@37906: fun context_pbl pI pt (p:pos) =
neuper@37906:     let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p
neuper@37906: 	val {ppc,where_,prls,...} = get_pbt pI
neuper@37906: 	val (model_ok, (pbl, pre)) = 
neuper@38050: 	    match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os
neuper@37906:     in (model_ok, pI, hdl, pbl, pre) end;
neuper@37906: 
neuper@37906: fun context_met mI pt (p:pos) =
neuper@37906:     let val PblObj {meth,origin=(os,_,hdl),...} = get_obj I pt p
neuper@37906: 	val {ppc,pre,prls,scr,...} = get_met mI
neuper@37906: 	val (model_ok, (pbl, pre)) = 
neuper@38050: 	    match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os
neuper@37906:     in (model_ok, mI, scr, pbl, pre) end
neuper@37906: 
neuper@37906: 
neuper@37906: (* val (pI, pt, pos as (p,_)) = (pblID, pt, p);
neuper@37906:    *)
neuper@37906: fun tryrefine pI pt (pos as (p,_):pos') =
neuper@37906:     let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p
neuper@38050:     in case refine_pbl (assoc_thy "Isac") pI probl of
neuper@37926: 	   NONE => (*copy from context_pbl*)
neuper@37906: 	   let val {ppc,where_,prls,...} = get_pbt pI
neuper@38050: 	       val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") 
neuper@37906: 						     probl (ppc,where_,prls) os
neuper@37906: 	   in (false, pI, hdl, pbl, pre) end
neuper@37926: 	 | SOME (pI, (pbl, pre)) => 
neuper@37906: 	   (true, pI, hdl, pbl, pre) 
neuper@37906:     end;
neuper@37906: 
neuper@37906: (* val (pt, (pos as (p,p_):pos')) = (pt, ip);
neuper@37906:    *)
neuper@37906: fun detailstep pt (pos as (p,p_):pos') = 
neuper@37906:     let val nd = get_nd pt p
neuper@37906: 	val cn = children nd
neuper@37906:     in if null cn 
neuper@37906:        then if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)]
neuper@37906: 	    then detailrls pt pos
neuper@37906: 	    else ("no-Rewrite_Set...", EmptyPtree, e_pos')
neuper@37906:        else ("donesteps", pt(*, get_formress [] ((lev_on o lev_dn) p) cn*),
neuper@37906: 	     (p @ [length (children (get_nd pt p))], Res) ) 
neuper@37906:     end;
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (***. for mathematics authoring on sml-toplevel; no XML .***)
neuper@37906: 
neuper@37906: type NEW = int list;
neuper@37906: (* val sp = (dI',pI',mI');
neuper@37906:    *)
neuper@37906: 
neuper@37906: (*15.8.03 for me with loc_specify/solve, nxt_specify/solve
neuper@37906:  delete as soon as TESTg_form -> _mout_ dropped*)
neuper@37906: fun TESTg_form ptp =
neuper@37906: (* val ptp = (pt,p);
neuper@37906:    *) 
neuper@37906:     let val (form,_,_) = pt_extract ptp
neuper@37906:     in case form of
neuper@37906: 	   Form t => Form' (FormKF (~1,EdUndef,0,Nundef,term2str t))
neuper@37906: 	 | ModSpec (_,p_, head, gfr, pre, _) => 
neuper@37906: 	   Form' (PpcKF (0,EdUndef,0,Nundef,
neuper@37906: 			 (case p_ of Pbl => Problem[] | Met => Method[],
neuper@38050: 			  itms2itemppc (assoc_thy"Isac") gfr pre)))
neuper@37906:     end;
neuper@37906: 
neuper@37906: (*.create a calc-tree; for use within sml: thus ^^^ NOT decoded to ^;
neuper@37906:    compare "fun CalcTree" which DOES decode.*)
neuper@37906: fun CalcTreeTEST [(fmz, sp):fmz] = 
neuper@37906: (* val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))];
neuper@37906:    val [(fmz, sp):fmz] = [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
neuper@37906:    *)
neuper@37906:     let val cs as ((pt,p), tacis) = nxt_specify_init_calc (fmz, sp)
neuper@37906: 	val tac = case tacis of [] => Empty_Tac | _ => (#1 o hd) tacis
neuper@37906: 	val f = TESTg_form (pt,p)
neuper@37906:     in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end; 
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: 
neuper@37906: fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) =
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@41972: 		    ("ok", (_, _, ptp))  => ptp
neuper@41972: 	    | ("unsafe-ok", (_, _, ptp)) => ptp
neuper@41972: 	    | ("not-applicable",_) => (pt, p)
neuper@41972: 	    | ("end-of-calculation", (_, _, ptp)) => ptp
neuper@41972: 	    | ("failure",_) => error "sys-error";
neuper@41972: 	  val (_, ts) = (*WN101102 NOT tested, if step would create _same_ ptp*)
neuper@37906: 	    (case step p ((pt, e_pos'),[]) of
neuper@41972: 		    ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)
neuper@41972: 	    | ("helpless",_) => ("helpless: cannot propose tac", [])
neuper@41972: 	    | ("no-fmz-spec",_) => error "no-fmz-spec"
neuper@41972: 	    | ("end-of-calculation", (ts, _, _)) => ("",ts))
neuper@38031: 	    handle _ => error "sys-error";
neuper@41972: 	  val tac = 
neuper@41972:       case ts of 
neuper@41972:         tacis as (_::_) => let val (tac,_,_) = last_elem tacis in tac end 
neuper@41972: 		  | _ => if p = ([],Res) then End_Proof' else Empty_Tac;
neuper@37906:       (*form output comes from locatetac*)
neuper@41972:   in (p:pos', []:NEW, TESTg_form (pt, p), 
neuper@41972: 	   (tac2IDstr tac, tac):tac'_, Sundef, pt) end;
neuper@37906: 
neuper@37906: (*for quick test-print-out, until 'type inout' is removed*)
neuper@37906: fun f2str (Form' (FormKF (_, _, _, _, cterm'))) = cterm';
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (*------------------------------------------------------------------(**)
neuper@37906: end
neuper@37906: open MathEngine;
neuper@37906: (**)------------------------------------------------------------------*)
neuper@37906: