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

   Input and output are Isabelle's formulae as strings.

   (c) Walther Neuper 2000

   (c) Stefan Rath 2005

use"~/proto2/isac/src/sml/ME/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 get_pblID : ptree * pos' -> pblID Library.option *)

   (* 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_) -> CalcHead.calcstate'

    val step : pos' -> CalcHead.calcstate -> string * CalcHead.calcstate'

    val trymatch : pblID -> ptree -> int list * 'a -> ptform

    val tryrefine : pblID -> ptree -> int list * 'a -> 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;

fun loc_solve_ m (pt,pos) =

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

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

   *)  

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

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

   (writeln 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; (**)

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

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

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

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

   val ptp as (pt, p) = (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 mI mem specsteps

		       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 _ => raise 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 => raise 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*)

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

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

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

   *)

    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 pI') (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 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;

(*WN11.9.03--- was only for hide, detail --> dialog ---------

(*

val nxt_me = fn

  : pblID

    -> (ptree * pos') *             : always the latest ovewriting the others

       (tac * tac_ * istate) list   : new tacs found PREpended to others

                                   -"- calcstate (typeinference doesn get it)

       -> detail * detail -> 

       hid ->                       : handles packages of tacs (eg. modeling)

       nxt_                                        

*)

fun nxt_me _ _ _ Hmodel = raise error "nxt_me: not impl. for Hmodel"

  | nxt_me _ _ _ Hspecify = raise error "nxt_me: not impl. for Hspecify"

  | nxt_me _ _ _ Happly = raise error "nxt_me: not impl. for Happly"

(* val ((ptp as (_,(_,p_)), tacis), (hi, de)) = ((ptp, []), (hide, detail));

   *)

  | nxt_me pI (ptp as (_,([],Res)), tacis) _ _ = Nexts (ptp, tacis)

  | nxt_me pI ((ptp as (_,(_,p_)), tacis):calcstate) (hi, de) _(*Hundef,Htac*)=

(* val ((ptp as (_,(_,p_)), tacis), (hi, de)) = ((ptp, []), (hide, detail));

   val ((ptp as (_,(_,p_)), []   ), (hi, de)) = ((ptp, []), (hide, detail));

   *)

    let val x = (if p_ mem [Pbl,Met]

		 then nxt_specify_ ptp else nxt_solve_ ptp)

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

    in case x of 

	   (_,[]) => HElpless

	 | (cs as (ptp, (tac,_,_)::_)) =>

	   let val (cs as (ptp, tacis' as (tac,_,_)::_)) =

		   if is_detail pI tac de then init_detail ptp else cs

	   in case is_hide pI tac hi of

		  Show => Nexts (ptp, tacis' @ tacis)

		| hid => 

		  nxt_me pI (ptp, tacis' @ tacis) (hi, de) hid

	   end

    end;

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

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

arg ip: 

    calcstate

.*)

fun step ((ip as (_,p_)):pos') ((ptp as (pt,p), tacis):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)) = (ip,cs);

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

   *)

    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 

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

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

	   else (case (if p_ mem [Pbl,Met]

		       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))

	 | _ => (case pIopt of

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

		   | Some pI =>

(* val Some pI = pIopt; 

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

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

       handle _ => ([], ptp);

   *)

		     (case (if p_ mem [Pbl,Met]

			       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)

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

    end;

(* is_complete_mod ptp;

   is_complete_spec ptp;

   get_obj g_form pt [1];

   print_depth 11;pt;print_depth 3;

   val (str, (_, (pt',p'))) = step ip cs;

   get_obj g_form pt [1];

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

   val (c, ip, cs as (ptp as (_,p),tacis)) = ([]:pos' list, pold, get_calc cI);

   val (Step s) = auto;

   *) 

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

    if s <= 1 

    then case tacis of

	     _::_ => (*if ip = p then ("ok", generate tacis ptp)##DONE IN step#

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

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

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

	   | _ => let val (str, (_, c', ptp)) = step ip cs

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

    else (case tacis of

	     _::_ => (*if ip = p then

			 let val ptp as (_, p) = generate tacis ptp

			 in autocalc p (ptp, []) (Step(s-1-(length tacis))) 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

	   | _ => 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 (pos as (_,p_), ((pt,_), _)) = (get_pos cI 1, get_calc cI);

   autocalc (get_pos cI 1) (get_calc cI) 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 p_ mem [Pbl, Met]

	 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) [];

*)    

fun trymatch pI pt (pos as (p,_)) =

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

	val spec = (dI,pI,mI)

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

	val (_, (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 tryrefine pI pt (pos as (p,_)) =

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

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

	   None => (*copy from trymatch*)

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

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

						     probl (ppc,where_,prls) os

	   in ModSpec (ocalhd_complete pbl pre (dI,pI,mI),

		       Pbl, e_term, pbl, pre, (dI,pI,mI)) end

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

	   ModSpec (ocalhd_complete pbl pre (dI,pI,mI),

		    Pbl, e_term, pbl, pre, (dI,pI,mI)) 

    end;

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

   *)

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

    let val nd = get_nd pt p

	val cn = children nd

    in if null cn andalso (is_rewset o (get_obj g_tac nd)) [] (*subnode!*)

       then detailrls pt 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;

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

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

   *)

    let (*val _ = states:= [];   WN050707*)

	val cs as ((pt,p), (tac,_,_)::_) = nxt_specify_init_calc (fmz, sp);

	val f = TESTg_form (pt,p);

(*	val _ = (add_calc cs;  IteratorTEST 1; moveActiveRootTEST 1);WN050707*)

    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) *)

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

(* val (_,tac) = nxt;

   *) let val (pt, p) = 

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

   (writeln o (itms2str thy)) (get_obj g_pbl pt' (fst p'));

   writeln( istate2str (get_istate pt' ([3],Res)));

   term2str (fst (get_obj g_result pt' [3]));

   val (pt,p) = (pt',p');

   *)

	    case locatetac tac (pt,p) of

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

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

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

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

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

	val (_, ts) = 

(* (writeln o (itms2str thy)) (get_obj g_pbl pt (fst p));

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

   (writeln o (itms2str thy)) (get_obj g_pbl pt'' (fst p));

   *)

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

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

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

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

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

	    handle _ => raise error "sys-error";

	val tac = case ts of ((tac,_,_)::_) => tac 

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

				  else Empty_Tac;

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

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

(*

end

open mathengine;

*)

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