(* 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 MATH_ENGINE =

sig

  type NEW (* TODO: refactor "fun me" with calcstate and remove *)

  val me : tac'_ -> pos' -> NEW -> ptree -> pos' * NEW * Ctree.mout * tac'_ * safe * ptree

  val autocalc :

     pos' list -> pos' -> (ptree * pos') * Ctree.taci list -> auto -> string * pos' list * (ptree * pos')

  val locatetac :

    tac -> ptree * (posel list * pos_) -> string * (Ctree.taci list * pos' list * (ptree * pos'))

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

  val detailstep :

    ptree -> pos' -> string * ptree * pos' val get_pblID : ptree * 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

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

  type nxt_

  type lOc_

  val CalcTreeTEST : fmz list -> pos' * NEW * Ctree.mout * (string * tac) * safe * ptree

  val f2str : Ctree.mout -> cterm'

  val loc_solve_ : string * tac_ -> ptree * (pos * pos_) -> lOc_

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

end

(**)

structure Math_Engine(**): MATH_ENGINE(**) =

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;

(* introduced for test only *)

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

datatype lOc_ =

  ERror of string              (*after loc_specify, loc_solve*)

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

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

fun loc_specify_ m (pt,pos) =

  let

    val (p, _, f, _, _, pt) = Chead.specify m pos [] pt;

  in

    case f of (Ctree.Error' e) => ERror e | _ => Updated ([], [], (pt,p))

  end

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

fun loc_solve_ m (pt, pos) =

  let

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

  in

    case msg of "ok" => Updated cs' | msg => ERror msg 

  end

datatype nxt_ =

	HElpless  (**)

| Nexts of Chead.calcstate (**)

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

   report of tacs' applicability in tacis; pt is dropped in setNextTactic*)

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

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

    let

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

    in

      case applicable_in p pt m of

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

	    | Chead.Appl 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 _ => ("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 SEVER.tacs user to ask ? *)

	      end

    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, (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'), _),

  		  probl, spec = (dI, pI, mI), ...}) => (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI)

      | PrfObj _ => error "nxt_specify_: not on PrfObj"

  in 

    if just_created_ pblobj (*by Subproblem*) andalso origin <> 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))

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

  	      Chead.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 => 

  	        nxt_solv (Apply_Method' (mI, NONE, e_istate, e_ctxt)) (e_istate, 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 =

  let

    val (mits, pt, p) =

      case Chead.nxt_specif (Specify_Method mI) ptp of

        ([(_, 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"

  in

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

  end

(* specify a new problem; WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' *)

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

  let

    val (complete, pits, pre, pt, p) =

      case Chead.nxt_specif (Specify_Problem pI) ptp of

        ([(_, 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"

  in

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

  end

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

  let

    val (complete, pits, pre, pt, p) =

      case Chead.nxt_specif (Specify_Theory tI) ptp of  

        ([(_, 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;

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

  let val pIopt = get_pblID (pt,ip);

  in

    if ip = ([],Res)

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

    else

      case tacis of

        (_::_) => 

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

          then 

            let val (pt',c',p') = Ctree.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 ERROR msg => (writeln ("*** " ^ msg);

  	                    ([], [], ptp)) (*e.g. Add_Given "equality///"*) of

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

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

      | _ => (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))

  		                then nxt_specify_ (pt, ip) 

                      else (nxt_solve_ (pt,ip))

  	                    handle ERROR msg => (writeln ("*** " ^ msg);

  	                      ([],[],ptp)) (*e.g. Add_Given "equality///"*) of

  	               cs as ([],_,_) =>("helpless", cs) (*FIXXME del.handle*)

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

  end

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

fun autocalc c ip cs (Step s) =

    if s <= 1

    then

      let val (str, (_, c', ptp)) = step ip cs;      (* autoord = 1, probably does 1 step 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_solve, complete_solve *)

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

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

    then

      let val ptp = Chead.all_modspec (pt, pos);

      in all_solve auto c ptp end                    (*... auto = 4 | 5 | 6 *)

    else

      if member op = [Pbl, Met] p_

      then

        if not (Chead.is_complete_mod (pt, pos))

   	    then

   	      let val ptp = Chead.complete_mod (pt, pos)      (*... auto = 2 | 3 *)

   		    in

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

   		      else

   		       if not (Chead.is_complete_spec ptp)

   			     then

   			       let val ptp = Chead.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 (Chead.is_complete_spec (pt,pos))

   		    then

   		      let val ptp = Chead.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);

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

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

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', _), ...}

          => (probl, os, pI, hdl, pI')

      | PrfObj _ => error "initcontext_pbl: uncovered case"

  	val pblID =

  	  if pI' = e_pblID 

  		then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)

  		else pI'

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

  	val (model_ok, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") probl (ppc,where_,prls) os

  in

    (model_ok, pblID, hdl, pbl, pre)

  end

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"

  	val metID = if mI' = e_metID 

  		    then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)

  		    else mI'

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

  	val (model_ok, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") 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 (probl, os, hdl) =

      case get_obj I pt p of

        PblObj {probl,origin = (os, _, hdl),...} => (probl, os, hdl)

      | PrfObj _ => error "context_pbl: uncovered case"

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

  	val (model_ok, (pbl, pre)) = 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) =

  let

    val (meth, os) =

      case get_obj I pt p of

        PblObj {meth, origin = (os, _, _),...} => (meth, os)

      | PrfObj _ => error "context_met: uncovered case"

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

  	val (model_ok, (pbl, pre)) = match_itms_oris (assoc_thy "Isac") meth (ppc,pre,prls) os

  in

    (model_ok, mI, scr, pbl, pre)

  end

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"

  in

    case refine_pbl (assoc_thy "Isac") 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") probl (ppc,where_,prls) os

        in

          (false, pI, hdl, pbl, pre)

        end

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

  end

fun detailstep pt (pos as (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, (p @ [length (children (get_nd pt p))], Res)) 

  end;

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

type NEW = int list;

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

   delete as soon as TESTg_form -> _mout_ dropped           *)

fun TESTg_form ptp =

  let

    val (form, _, _) = Chead.pt_extract ptp

  in

    case form of

      Form t => Ctree.FormKF (term2str t)

    | ModSpec (_,p_, _, gfr, pre, _) => Ctree.PpcKF (

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

        | _ => error "TESTg_form: uncovered case",

 			itms2itemppc (assoc_thy"Isac") gfr pre))

   end

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

   compare "fun CalcTree" which DOES decode                        *)

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 f = TESTg_form (pt,p)

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

| CalcTreeTEST _ = error "CalcTreeTEST: uncovered case"

(*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) p _(*NEW remove*) pt =

  let 

    val (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"

	    | _ => error "me: uncovered case"

	  val (_, ts) =

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

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

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

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

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

	    | _ => error "me: uncovered case")

	      handle ERROR msg => raise ERROR msg

	  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;

  in (p, [] : NEW, TESTg_form (pt, p) (* form output comes from locatetac *), 

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

  end

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

fun f2str (Ctree.FormKF cterm') = cterm';

end