(* MathEngine/mathengine-stateless.sml

   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

*)

signature MATH_ENGINE =

sig

  val autocalc : Pos.pos' list -> Pos.pos' -> Calc.T * State_Steps.T ->

    Solve.auto -> string * Pos.pos' list * Calc.T

  val initcontext_met : Ctree.ctree -> Pos.pos' -> bool * string list * Program.T * I_Model.T * Pre_Conds.T

  val initcontext_pbl : Ctree.ctree -> Pos.pos' -> bool * string list * term * I_Model.T * Pre_Conds.T

  val context_met : MethodC.id -> Ctree.ctree -> Pos.pos -> bool * MethodC.id * Program.T * I_Model.T * Pre_Conds.T

  val context_pbl : Problem.id -> Ctree.ctree -> Pos.pos -> bool * Problem.id * term * I_Model.T * Pre_Conds.T

  val set_method : MethodC.id -> Calc.T -> Ctree.ctree * SpecificationC.T

  val set_problem : Problem.id -> Calc.T -> Ctree.ctree * SpecificationC.T

  val set_theory : ThyC.id -> Calc.T -> Ctree.ctree * SpecificationC.T

  val tryrefine : Problem.id -> Ctree.ctree -> Pos.pos' -> bool * Problem.id * term * I_Model.T * Pre_Conds.T

(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

  (*NONE*)

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

  (*NONE*)

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

(*----- unused code, kept as hints to design ideas ---------------------------------------------*)

  (* NONE *)

end

(**)

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

struct

(**)

datatype nxt_ =

	HElpless  (**)

| Nexts of Calc.T * State_Steps.T (**)

(* specify a new method; WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' *)

fun set_method mI ptp =

  let

    val (mits, pt, p) =

      case Step_Specify.by_tactic_input (Tactic.Specify_Method mI) ptp of

        (_, ([(_, Tactic.Specify_Method' (_, _, mits), _)], [], (pt, (p, _)))) => (mits, pt, p)

      | _ => raise 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 Ctree.get_obj I pt p of

        Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)

      | Ctree.PrfObj _ => raise ERROR "set_method: case 2 uncovered"

  in

    (pt, (complete, Pos.Met, hdf, mits, pre, spec) : SpecificationC.T)

  end

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

fun set_problem pI ptp =

  let

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

      case Step_Specify.by_tactic_input (Tactic.Specify_Problem pI) ptp of

        (_, ([(_, Tactic.Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _))))

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

      | _ => raise ERROR "set_problem: case 1 uncovered"

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

    val (hdf, spec) =

      case Ctree.get_obj I pt p of

        Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)

      | Ctree.PrfObj _ => raise ERROR "set_problem: case 2 uncovered"

  in

    (pt, (complete, Pos.Pbl, hdf, pits, pre, spec) : SpecificationC.T)

  end

fun set_theory tI ptp =

  let

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

      case Step_Specify.by_tactic_input (Tactic.Specify_Theory tI) ptp of  

        (_, ([(_, Tactic.Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _))))

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

      | _ => raise ERROR "set_theory: case 1 uncovered"

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

    val (hdf, spec) =

      case Ctree.get_obj I pt p of

        Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)

      | Ctree.PrfObj _ => raise ERROR "set_theory: case 2 uncovered"

  in (pt, (complete, Pos.Pbl, hdf, pits, pre, spec) : SpecificationC.T) 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 *)

fun autocalc c ip cs (Solve.Steps s) =

    if s <= 1

    then

      let val (str, (_, c', ptp)) = Step.do_next ip cs;      (* autoord = 1, probably does 1 do_next too much*)

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

    else

      let val (str, (_, c', ptp as (_, p))) = Step.do_next ip cs;

      in

        if str = "ok" 

        then autocalc (c@c') p (ptp, []) (Solve.Steps (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 Solve.autoord auto > 3 andalso Ctree.just_created (pt, pos)

    then

      let val ptp = Specify.do_all (pt, pos);

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

    else

      if member op = [Pos.Pbl, Pos.Met] p_

      then

        if not (SpecificationC.is_complete (pt, pos))

   	    then

   	      let val ptp = Specify.finish_phase (pt, pos)      (*... auto = 2 | 3 *)

   		    in

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

   		      else

   		       if not (References.are_complete ptp)

   			     then

   			       let val ptp = References.complete ptp

   			       in

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

   			       end

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

   		    end

   	    else 

   		    if not (References.are_complete (pt,pos))

   		    then

   		      let val ptp = References.complete (pt, pos)

   		      in

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

   		      end

   		    else

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

   	  else Solve.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 Ctree.get_obj I pt p of

        Ctree.PblObj {probl, origin = (os, (_, pI, _), hdl), spec=(_, pI', _), ...}

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

      | Ctree.PrfObj _ => raise ERROR "initcontext_pbl: uncovered case"

  	val pblID =

  	  if pI' = Problem.id_empty 

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

  		else pI'

  	val {ppc, where_, prls, ...} = Problem.from_store pblID

  	val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") 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 Ctree.get_obj I pt p of

        Ctree.PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI')

      | Ctree.PrfObj _ => raise ERROR "initcontext_met: uncovered case"

  	val metID = if mI' = MethodC.id_empty 

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

  		    else mI'

  	val {ppc, pre, prls, scr, ...} = MethodC.from_store metID

  	val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") 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 pI *)

fun context_pbl pI pt p =

  let

    val (probl, os, hdl) =

      case Ctree.get_obj I pt p of

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

      | Ctree.PrfObj _ => raise ERROR "context_pbl: uncovered case"

  	val {ppc, where_, prls, ...} = Problem.from_store pI

  	val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os

  in

    (model_ok, pI, hdl, pbl, pre)

  end

fun context_met mI pt p =

  let

    val (meth, os) =

      case Ctree.get_obj I pt p of

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

      | Ctree.PrfObj _ => raise ERROR "context_met: uncovered case"

  	val {ppc,pre,prls,scr,...} = MethodC.from_store mI

  	val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os

  in

    (model_ok, mI, scr, pbl, pre)

  end

fun tryrefine pI pt (p,_) =

  let

    val (probl, os, hdl) =

      case Ctree.get_obj I pt p of

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

      | Ctree.PrfObj _ => raise ERROR "context_met: uncovered case"

  in

    case Refine.problem (ThyC.get_theory "Isac_Knowledge") pI probl of

  	  NONE => (*copy from context_pbl*)

  	    let

  	      val {ppc,where_,prls,...} = Problem.from_store pI

  	      val (_, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os

        in

          (false, pI, hdl, pbl, pre)

        end

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

  end

(**)end(**)