(* The _functional_ mathematics engine, ie. without a state.

    Input and output are Isabelle's formulae as strings.

    authors: Walther Neuper 2000

    (c) due to copyright terms

 use"mathengine.sml";

 *)

 signature MATHENGINE =

   sig

     type nxt_

     (* datatype nxt_ = HElpless | Nexts of CalcHead.calcstate *)

     type NEW

     type lOc_

     (*datatype

       lOc_ =

           ERror of string

         | UNsafe of CalcHead.calcstate'

         | Updated of CalcHead.calcstate' *)

     val CalcTreeTEST :

        fmz list ->

        pos' * NEW * mout * (string * tac) * safe * ptree

     val TESTg_form : ptree * (int list * pos_) -> mout

     val autocalc :

        pos' list ->

        pos' ->

        (ptree * pos') * taci list ->

        auto -> string * pos' list * (ptree * pos')

     val detailstep : ptree -> pos' -> string * ptree * pos'

    (* val e_tac_ : tac_ *)

     val f2str : mout -> cterm'

    (* val get_pblID : ptree * pos' -> pblID option *)

     val initmatch : ptree -> pos' -> ptform

    (* val loc_solve_ :

        string * tac_ -> ptree * (int list * pos_) -> lOc_ *)

    (* val loc_specify_ : tac_ -> ptree * pos' -> lOc_ *)

     val locatetac :     (*tests only*)

        tac ->

        ptree * (posel list * pos_) ->

        string * (taci list * pos' list * (ptree * (posel list * pos_)))

     val me :

        tac'_ ->

        pos' ->

        NEW ->

        ptree -> pos' * NEW * mout * tac'_ * safe * ptree

     val nxt_specify_ : ptree * (int list * pos_) -> calcstate'(*tests only*)

     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 step : pos' -> calcstate -> string * calcstate'

     val trymatch : pblID -> ptree -> pos' -> ptform

     val tryrefine : pblID -> ptree -> pos' -> ptform

   end

 (*------------------------------------------------------------------(**)

 structure MathEngine : MATHENGINE =

 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'

     in if pI <> e_pblID then SOME pI

        else if oI <> e_pblID then SOME oI

        else NONE end;

 (*fun get_pblID (pt, (p,_):pos') =

     ((snd3 o (get_obj g_spec pt)) (par_pblobj pt p));*)

 (*--vvv--dummies for test*)

 val e_tac_ = Tac_ (Pure.thy,"","","");

 datatype lOc_ =

   ERror of string         (*after loc_specify, loc_solve*)

 | UNsafe of calcstate'    (*after loc_specify, loc_solve*)

 | Updated of calcstate';   (*after loc_specify, loc_solve*)

 fun loc_specify_ m (pt,pos) =

 (* val pos = ip;

    *)

     let val (p,_,f,_,s,pt) = specify m pos [] pt;

 (*      val (_,_,_,_,_,pt')= specify m pos [] pt;

    *) 

    in case f of

 	   (Error' (Error_ e)) => ERror e

 	 | _ => Updated ([], [], (pt,p)) end;

 (*. TODO push return-value cs' into solve and rename solve->loc_solve?_? .*)

 (* val (m, pos) = ((mI,m), ip);

    val (m,(pt,pos) ) = ((mI,m), ptp);

    *)  

 fun loc_solve_ m (pt,pos) =

     let val (msg, cs') = solve m (pt, pos);

 (* val (tacis,dels,(pt',p')) = cs';

    (tracing o istate2str) (get_istate pt' p');

    (term2str o fst) (get_obj g_result pt' (fst p'));

    *)

     in case msg of

 	   "ok" => Updated cs' 

 	 | msg => ERror msg 

     end;

 datatype nxt_ =

 	 HElpless  (**)

        | Nexts of calcstate; (**)

 (*. locate a tactic in a script and apply it if possible .*)

 (*report applicability of tac in tacis; pt is dropped in setNextTactic*)

 fun locatetac _ (ptp as (_,([],Res))) = ("end-of-calculation", ([], [], ptp))

 (* val ptp as (pt, p) = (pt, p);

    val ptp as (pt, p) = (pt, ip);

    *)

   | locatetac tac (ptp as (pt, p)) =

     let val (mI,m) = mk_tac'_ tac;

     in case applicable_in p pt m of

 	   Notappl e => ("not-applicable", ([],[],  ptp):calcstate')

 	 | Appl m =>

 (* val Appl m = applicable_in p pt m;

     *) 

 	   let val x = if member op = specsteps mI

 		       then loc_specify_ m ptp else loc_solve_ (mI,m) ptp

 	   in case x of 

 		  ERror e => ("failure", ([], [], ptp))

 		(*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')(*for -"-  user to ask ? *)

 	   end

     end;

 (*------------------------------------------------------------------

 fun init_detail ptp = e_calcstate;(*15.8.03.MISSING-->solve.sml!?*)

 (*----------------------------------------------------from solve.sml*)

   | nxt_solv (Detail_Set'(thy', rls, t)) (pt, p) =

     let (*val rls = the (assoc(!ruleset',rls'))

 	    handle _ => error ("solve: '"^rls'^"' not known");*)

 	val thy = assoc_thy thy';

         val (srls, sc, is) = 

 	    case rls of

 		Rrls {scr=sc as Rfuns {init_state=ii,...},...} => 

 		(e_rls, sc, RrlsState (ii t))

 	      | Rls {srls=srls,scr=sc as Script s,...} => 

 		(srls, sc, ScrState ([(one_scr_arg s,t)], [], 

 			       NONE, e_term, Sundef, true));

 	val pt = update_tac pt (fst p) (Detail_Set (id_rls rls));

 	val (p,cid,_,pt) = generate1 thy (Begin_Trans' t) is p pt;

 	val nx = (tac_2tac o fst3) (next_tac (thy',srls) (pt,p) sc is);

 	val aopt = applicable_in p pt nx;

     in case aopt of

 	   Notappl s => error ("solve Detail_Set: "^s)

 	 (* val Appl m = aopt;

 	    *)

 	 | Appl m => solve ("discardFIXME",m) p pt end

 ------------------------------------------------------------------*)

 (*iterated by nxt_me; there (the resulting) ptp dropped

   may call nxt_solve Apply_Method --- thus evaluated here after solve.sml*)

 (* val (ptp as (pt, pos as (p,p_))) = ptp;

    val (ptp as (pt, pos as (p,p_))) = (pt,ip);

    *)

 fun nxt_specify_ (ptp as (pt, pos as (p,p_))) =

     let val pblobj as (PblObj{meth,origin=origin as (oris,(dI',pI',mI'),_),

 			      probl,spec=(dI,pI,mI),...}) = get_obj I pt p;

     in if just_created_ pblobj (*by Subproblem*) andalso origin <> e_origin

        then case mI' of

 	 ["no_met"] => nxt_specif (Refine_Tacitly pI') (pt, (p, Pbl))

        | _ => nxt_specif Model_Problem (pt, (p,Pbl))

        else let val cpI = if pI = e_pblID then pI' else pI;

 		val cmI = if mI = e_metID then mI' else mI;

 		val {ppc,prls,where_,...} = get_pbt cpI;

 		val pre = 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) =

 		    nxt_spec p_ pb oris (dI',pI',mI') (probl, meth) 

 			     (ppc, (#ppc o get_met) cmI) (dI, pI, mI);

 	    in case tac of

 		   Apply_Method mI => 

 (* val Apply_Method mI = tac;

    *)

 		   nxt_solv (Apply_Method' (mI, NONE, e_istate)) e_istate ptp

 		 | _ => nxt_specif tac ptp end

     end;

 (*.specify a new method;

    WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' .*)

 fun set_method (mI:metID) ptp =

     let val ([(_, Specify_Method' (_, _, mits), _)], [], (pt, pos as (p,_))) = 

 	    nxt_specif (Specify_Method mI) ptp

 	val pre = []        (*...from Specify_Method'*)

 	val complete = true (*...from Specify_Method'*)

 	(*from Specify_Method'  ? vvv,  vvv ?*)

 	val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p

     in (pt, (complete, Met, hdf, mits, pre, spec):ocalhd) end;

 (* val ([(_, Specify_Method' (_, _, mits), _)], [],_) = 

     nxt_specif (Specify_Method mI) ptp;

  *)

 (*.specify a new problem;

    WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' .*)

 (* val (pI, ptp) = (pI, (pt, ip));

    *)

 fun set_problem pI (ptp: ptree * pos') =

     let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)],

 	     _, (pt, pos as (p,_))) = nxt_specif (Specify_Problem pI) ptp

 	(*from Specify_Problem' ? vvv,  vvv ?*)

 	val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p

     in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end;

 fun set_theory (tI:thyID) (ptp: ptree * pos') =

     let val ([(_, Specify_Problem' (_, (complete, (pits, pre))),_)],

 	     _, (pt, pos as (p,_))) = nxt_specif (Specify_Theory tI) ptp

 	(*from Specify_Theory'  ? vvv,  vvv ?*)

 	val PblObj {origin = (_,_,hdf), spec,...} = get_obj I pt p

     in (pt, (complete, Pbl, hdf, pits, pre, spec):ocalhd) end;

 (*.does a step forward; returns tactic used, ctree updated.

 TODO.WN0512 redesign after specify-phase became more separated from solve-phase

 arg ip: 

     calcstate

 .*)

 (* val (ip as (_,p_), (ptp as (pt,p), tacis)) = (get_pos 1 1, get_calc 1);

    val (ip as (_,p_), (ptp as (pt,p), tacis)) = (pos, cs);

    val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'),[]));

    val (ip as (_,p_), (ptp as (pt,p), tacis)) = (ip,cs);

    *)

 fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):calcstate) =

     let val pIopt = get_pblID (pt,ip);

     in if (*p = ([],Res) orelse*) ip = ([],Res)

        then ("end-of-calculation",(tacis, [], ptp):calcstate') else

        case tacis of

 	   (_::_) =>

 (* val((tac,_,_)::_) = tacis;

    *) 

 	   if ip = p (*the request is done where ptp waits for*)

 	   then let val (pt',c',p') = generate tacis (pt,[],p)

 		in ("ok", (tacis, c', (pt', p'))) end

 	   else (case (if member op = [Pbl,Met] p_

 		       then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))

 		      handle _ => ([],[],ptp)(*e.g.by Add_Given "equality///"*)

 		  of cs as ([],_,_) => ("helpless", cs)

 		   | cs => ("ok", cs))

 (* val [] = tacis;

    *) 

 	 | _ => (case pIopt of

 		     NONE => ("no-fmz-spec", ([], [], ptp))

 		   | SOME pI =>

 (* val SOME pI = pIopt; 

    val cs=(if member op = [Pbl,Met] p_ andalso is_none(get_obj g_env pt (fst p))

 	     then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip))

        handle _ => ([], ptp);

    *)

 		     (case (if member op = [Pbl,Met] p_

 			       andalso is_none (get_obj g_env pt (fst p))

 			    (*^^^^^^^^: Apply_Method without init_form*)

 			    then nxt_specify_ (pt,ip) else nxt_solve_ (pt,ip) )

 			   handle _ => ([],[],ptp)(*e.g.by Add_Giv"equality/"*)

 		       of cs as ([],_,_) =>("helpless", cs)(*FIXXMEdel.handle*)

 			| cs => ("ok", cs)))

     end;

 (*  (nxt_solve_ (pt,ip)) handle e => print_exn e ;

    *)

 (*.does several steps within one calculation as given by "type auto";

    the steps may arbitrarily go into and leave different phases, 

    i.e. specify-phase and solve-phase.*)

 (*TODO.WN0512 ? redesign after the phases have been more separated

   at the fron-end in 05: 

   eg. CompleteCalcHead could be done by a separate fun !!!*)

 (* val (ip, cs as (ptp as (pt,p),tacis)) = (get_pos cI 1, get_calc cI);

    val (ip, cs as (ptp as (pt,p),tacis)) = (pold, get_calc cI);

    val (c, ip, cs as (ptp as (_,p),tacis), Step s) = 

        ([]:pos' list, pold, get_calc cI, auto);

    *) 

 fun autocalc c ip (cs as (ptp as (_,p),tacis)) (Step s) =

     if s <= 1

     then let val (str, (_, c', ptp)) = step ip cs;(*1*)

 	 (*at least does 1 step, ev.1 too much*)

 	 in (str, c@c', ptp) end

     else let val (str, (_, c', ptp as (_, p))) = step ip cs;

 	 in if str = "ok" 

 	    then autocalc (c@c') p (ptp,[]) (Step (s-1))

 	    else (str, c@c', ptp) end

 (*handles autoord <= 3, autoord > 3 handled by all_/complete_solve*)

   | autocalc c (pos as (_,p_)) ((pt,_), _(*tacis would help 1x in solve*))auto=

 (* val (c:pos' list, (pos as (_,p_)),((pt,_),_),auto) = 

       ([], pold, get_calc cI, auto);

    *)

      if autoord auto > 3 andalso just_created (pt, pos)

      then let val ptp = all_modspec (pt, pos);

 	  in all_solve auto c ptp end

      else

 	 if member op = [Pbl, Met] p_

  	 then if not (is_complete_mod (pt, pos))

 	      then let val ptp = complete_mod (pt, pos)

 		   in if autoord auto < 3 then ("ok", c, ptp)

 		      else 

 			  if not (is_complete_spec ptp)

 			  then let val ptp = complete_spec ptp

 			       in if autoord auto = 3 then ("ok", c, ptp)

 				  else all_solve auto c ptp

 			       end

 			  else if autoord auto = 3 then ("ok", c, ptp)

 			  else all_solve auto c ptp 

 		   end

 	      else 

 		  if not (is_complete_spec (pt,pos))

 		  then let val ptp = complete_spec (pt, pos)

 		       in if autoord auto = 3 then ("ok", c, ptp)

 			  else all_solve auto c ptp

 		       end

 		  else if autoord auto = 3 then ("ok", c, (pt, pos))

 		  else all_solve auto c (pt, pos)

 	 else complete_solve auto c (pt, pos);

 (* val pbl = get_obj g_pbl (fst ptp) [];

    val (oris,_,_) = get_obj g_origin (fst ptp) [];

 *)    

 (*.initialiye matching; before 'tryMatch' get the pblID to match with:

    if no pbl has been specified, take the init from origin.*)

 (*fun initmatch pt (pos as (p,_):pos') =

     let val PblObj {probl,origin=(os,(_,pI,_),_),spec=(dI',pI',mI'),...} = 

 	    get_obj I pt p

 	val pblID = if pI' = e_pblID 

 		    then (*TODO.WN051125 (#init o get_pbt) pI          <<<*) 

 			takelast (2, pI) (*FIXME.WN051125 a hack, impl.^^^*)

 		    else pI'

 	val spec = (dI',pblID,mI')

 	val {ppc,where_,prls,...} = get_pbt pblID

 	val (model_ok, (pbl, pre)) = 

 	    match_itms_oris (assoc_thy "Isac.thy") probl (ppc,where_,prls) os

     in ModSpec (ocalhd_complete pbl pre spec,

 		Pbl, e_term, pbl, pre, spec) end;*)

 fun initcontext_pbl pt (pos as (p,_):pos') =

     let val PblObj {probl,origin=(os,(_,pI,_),hdl),spec=(dI',pI',mI'),...} = 

 	    get_obj I pt p

 	val pblID = if pI' = e_pblID 

 		    then (*TODO.WN051125 (#init o get_pbt) pI          <<<*) 

 			takelast (2, pI) (*FIXME.WN051125 a hack, impl.^^^*)

 		    else pI'

 	val {ppc,where_,prls,...} = get_pbt pblID

 	val (model_ok, (pbl, pre)) = 

 	    match_itms_oris (assoc_thy "Isac.thy") probl (ppc,where_,prls) os

     in (model_ok, pblID, hdl, pbl, pre) end;

 fun initcontext_met pt (pos as (p,_):pos') =

     let val PblObj {meth,origin=(os,(_,_,mI), _),spec=(_, _, mI'),...} = 

 	    get_obj I pt p

 	val metID = if mI' = e_metID 

 		    then (*TODO.WN051125 (#init o get_pbt) pI          <<<*) 

 			takelast (2, mI) (*FIXME.WN051125 a hack, impl.^^^*)

 		    else mI'

 	val {ppc,pre,prls,scr,...} = get_met metID

 	val (model_ok, (pbl, pre)) = 

 	    match_itms_oris (assoc_thy "Isac.thy") 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*)

 fun context_pbl pI pt (p:pos) =

     let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p

 	val {ppc,where_,prls,...} = get_pbt pI

 	val (model_ok, (pbl, pre)) = 

 	    match_itms_oris (assoc_thy "Isac.thy") probl (ppc,where_,prls) os

     in (model_ok, pI, hdl, pbl, pre) end;

 fun context_met mI pt (p:pos) =

     let val PblObj {meth,origin=(os,_,hdl),...} = get_obj I pt p

 	val {ppc,pre,prls,scr,...} = get_met mI

 	val (model_ok, (pbl, pre)) = 

 	    match_itms_oris (assoc_thy "Isac.thy") meth (ppc,pre,prls) os

     in (model_ok, mI, scr, pbl, pre) end

 (* val (pI, pt, pos as (p,_)) = (pblID, pt, p);

    *)

 fun tryrefine pI pt (pos as (p,_):pos') =

     let val PblObj {probl,origin=(os,_,hdl),...} = get_obj I pt p

     in case refine_pbl (assoc_thy "Isac.thy") pI probl of

 	   NONE => (*copy from context_pbl*)

 	   let val {ppc,where_,prls,...} = get_pbt pI

 	       val (_, (pbl, pre)) = match_itms_oris (assoc_thy "Isac.thy") 

 						     probl (ppc,where_,prls) os

 	   in (false, pI, hdl, pbl, pre) end

 	 | SOME (pI, (pbl, pre)) => 

 	   (true, pI, hdl, pbl, pre) 

     end;

 (* val (pt, (pos as (p,p_):pos')) = (pt, ip);

    *)

 fun detailstep pt (pos as (p,p_):pos') = 

     let val nd = get_nd pt p

 	val cn = children nd

     in if null cn 

        then if (is_rewset o (get_obj g_tac nd)) [(*root of nd*)]

 	    then detailrls pt pos

 	    else ("no-Rewrite_Set...", EmptyPtree, e_pos')

        else ("donesteps", pt(*, get_formress [] ((lev_on o lev_dn) p) cn*),

 	     (p @ [length (children (get_nd pt p))], Res) ) 

     end;

 (***. for mathematics authoring on sml-toplevel; no XML .***)

 type NEW = int list;

 (* val sp = (dI',pI',mI');

    *)

 (*15.8.03 for me with loc_specify/solve, nxt_specify/solve

  delete as soon as TESTg_form -> _mout_ dropped*)

 fun TESTg_form ptp =

 (* val ptp = (pt,p);

    *) 

     let val (form,_,_) = pt_extract ptp

     in case form of

 	   Form t => Form' (FormKF (~1,EdUndef,0,Nundef,term2str t))

 	 | ModSpec (_,p_, head, gfr, pre, _) => 

 	   Form' (PpcKF (0,EdUndef,0,Nundef,

 			 (case p_ of Pbl => Problem[] | Met => Method[],

 			  itms2itemppc (assoc_thy"Isac.thy") gfr pre)))

     end;

 (*.create a calc-tree; for use within sml: thus ^^^ NOT decoded to ^;

    compare "fun CalcTree" which DOES decode.*)

 fun CalcTreeTEST [(fmz, sp):fmz] = 

 (* val [(fmz, sp):fmz] = [(fmz, (dI',pI',mI'))];

    val [(fmz, sp):fmz] = [([], ("e_domID", ["e_pblID"], ["e_metID"]))];

    *)

     let val cs as ((pt,p), tacis) = nxt_specify_init_calc (fmz, sp)

 	val tac = case tacis of [] => Empty_Tac | _ => (#1 o hd) tacis

 	val f = TESTg_form (pt,p)

     in (p, []:NEW, f, (tac2IDstr tac, tac), Sundef, pt) end; 

 (*for tests > 15.8.03 after separation setnexttactic / nextTac:

   external view: me should be used by math-authors as done so far

   internal view: loc_specify/solve, nxt_specify/solve used

                  i.e. same as in setnexttactic / nextTac*)

 (*ENDE TESTPHASE 08/10.03:

   NEW loeschen, eigene Version von locatetac, step

   meNEW, CalcTreeTEST: tac'_ -replace-> tac, remove [](cid) *)

 (* val ((_,tac), p, _, pt) = (nxt, p, c, pt);

    *)

 fun me ((_,tac):tac'_) (p:pos') (_:NEW(*remove*)) (pt:ptree) =

     let val (pt, p) = 

 (* val (msg, (tacis, pos's, (pt',p'))) = locatetac tac (pt,p);

    p = ([1, 9], Res);

    (tracing o istate2str) (get_istate pt p);

    *)

 	      (*locatetac is here for testing by me; step would suffice in me*)

 	    case locatetac tac (pt,p) of

 		("ok", (_, _, ptp))  => ptp

 	      | ("unsafe-ok", (_, _, ptp)) => ptp

 	      | ("not-applicable",_) => (pt, p)

 	      | ("end-of-calculation", (_, _, ptp)) => ptp

 	      | ("failure",_) => error "sys-error";

 	val (_, ts) = 

 (* val (eee, (ts, _, (pt'',_))) = step p ((pt, e_pos'),[]);

    *)

 	    (case step p ((pt, e_pos'),[]) of

 		 ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)

 	       | ("helpless",_) => ("helpless: cannot propose tac", [])

 	       | ("no-fmz-spec",_) => error "no-fmz-spec"

 	       | ("end-of-calculation", (ts, _, _)) => ("",ts))

 	    handle _ => error "sys-error";

 	val tac = case ts of tacis as (_::_) =>

 (* val tacis as (_::_) = ts;

    *)

 			     let val (tac,_,_) = last_elem tacis

 			     in tac end 

 			   | _ => if p = ([],Res) then End_Proof'

 				  else Empty_Tac;

       (*form output comes from locatetac*)

     in(p:pos',[]:NEW, TESTg_form (pt, p), 

 	(tac2IDstr tac, tac):tac'_, Sundef, pt)  end;

 (*for quick test-print-out, until 'type inout' is removed*)

 fun f2str (Form' (FormKF (_, _, _, _, cterm'))) = cterm';

 (*------------------------------------------------------------------(**)

 end

 open MathEngine;

 (**)------------------------------------------------------------------*)