*)

 *)

 signature MATH_ENGINE =

 signature MATH_ENGINE =

 sig

 sig

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

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

   val autocalc :

   val autocalc :

   val locatetac :

   val locatetac :

   val detailstep :

   val detailstep :

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

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

   type nxt_

   type nxt_

   type lOc_

   type lOc_

   val f2str : Generate.mout -> cterm'

   val f2str : Generate.mout -> cterm'

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

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

 end

 end

 (**)

 (**)

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

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

 struct

 struct

 (**)

 (**)

   in

   in

     if pI <> e_pblID

     if pI <> e_pblID

     then SOME pI

     then SOME pI

     else

     else

       if oI <> e_pblID then SOME oI else NONE end;

       if oI <> e_pblID then SOME oI else NONE end;

 (* introduced for test only *)

 (* introduced for test only *)

 datatype lOc_ =

 datatype lOc_ =

   ERror of string              (*after loc_specify, loc_solve*)

   ERror of string              (*after loc_specify, loc_solve*)

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

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

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

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

 	        case x of 

 	        case x of 

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

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

 		        (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)

 		        (*FIXXXXXME: loc_specify_, loc_solve_ TOGETHER with dropping meOLD+detail.sml*)

 		      | UNsafe cs' => ("unsafe-ok", cs')

 		      | UNsafe cs' => ("unsafe-ok", cs')

 		      | Updated (cs' as (_, _, (_, p'))) => (*ev.SEVER.tacs like Begin_Trans*)

 		      | Updated (cs' as (_, _, (_, p'))) => (*ev.SEVER.tacs like Begin_Trans*)

             (*for SEVER.tacs user to ask ? *)

             (*for SEVER.tacs user to ask ? *)

 	      end

 	      end

     end

     end

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

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

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

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

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

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

   let

   let

     val (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) = 

     val (pblobj, meth, origin, oris, dI', pI', mI', probl, dI, pI, mI) = 

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

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

   in 

   in 

     then 

     then 

       case mI' of

       case mI' of

     else 

     else 

       let 

       let 

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

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

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

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

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

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

   	    (*FIXME.WN0308:    ~~~~~: just check true in itms of pbl/met?*)

   	    (*FIXME.WN0308:    ~~~~~: just check true in itms of pbl/met?*)

   	    val (_, tac) =

   	    val (_, tac) =

   	      Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)

   	      Chead.nxt_spec p_ pb oris (dI', pI', mI') (probl, meth) (ppc, (#ppc o Specify.get_met) cmI) (dI, pI, mI)

       in

       in

         case tac of

         case tac of

   	    | _ => Chead.nxt_specif tac ptp

   	    | _ => Chead.nxt_specif tac ptp

   	  end

   	  end

   end

   end

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

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

   let

   let

     val (mits, pt, p) =

     val (mits, pt, p) =

       | _ => error "set_method: case 1 uncovered"

       | _ => error "set_method: case 1 uncovered"

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

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

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

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

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

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

     val (hdf, spec) =

     val (hdf, spec) =

   end

   end

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

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

   let

   let

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

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

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

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

       | _ => error "set_problem: case 1 uncovered"

       | _ => error "set_problem: case 1 uncovered"

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

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

     val (hdf, spec) =

     val (hdf, spec) =

   let

   let

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

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

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

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

       | _ => error "set_theory: case 1 uncovered"

       | _ => error "set_theory: case 1 uncovered"

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

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

     val (hdf, spec) =

     val (hdf, spec) =

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

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

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

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

   let val pIopt = get_pblID (pt,ip);

   let val pIopt = get_pblID (pt,ip);

   in

   in

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

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

     else

     else

       case tacis of

       case tacis of

         (_::_) => 

         (_::_) => 

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

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

           then 

           then 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

       | _ => (case pIopt of

       | _ => (case pIopt of

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

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

   	          | SOME _ =>                         (*vvvvvv: Apply_Method without init_form*)

   	          | SOME _ =>                         (*vvvvvv: Apply_Method without init_form*)

   		                then nxt_specify_ (pt, ip) 

   		                then nxt_specify_ (pt, ip) 

                       else (Solve.nxt_solve_ (pt,ip))

                       else (Solve.nxt_solve_ (pt,ip))

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

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

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

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

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

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

         if str = "ok" 

         if str = "ok" 

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

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

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

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

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

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

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

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

     then

     then

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

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

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

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

     else

     else

       then

       then

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

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

    	    then

    	    then

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

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

    		    in

    		    in

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

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

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

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

 fun initcontext_pbl pt (p, _) =

 fun initcontext_pbl pt (p, _) =

   let

   let

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

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

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

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

   	val pblID =

   	val pblID =

   	  if pI' = e_pblID 

   	  if pI' = e_pblID 

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

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

   		else pI'

   		else pI'

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

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

   end

   end

 fun initcontext_met pt (p,_) =

 fun initcontext_met pt (p,_) =

   let

   let

     val (meth, os, mI, mI') =

     val (meth, os, mI, mI') =

   	val metID = if mI' = e_metID 

   	val metID = if mI' = e_metID 

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

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

   		    else mI'

   		    else mI'

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

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

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

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

   in

   in

     (model_ok, metID, scr, pbl, pre)

     (model_ok, metID, scr, pbl, pre)

   end

   end

 (* match the model of a problem at pos p with the model-pattern of the problem with pblID *)

 (* match the model of a problem at pos p with the model-pattern of the problem with pblID *)

   let

   let

     val (probl, os, hdl) =

     val (probl, os, hdl) =

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

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

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

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

   in

   in

     (model_ok, pI, hdl, pbl, pre)

     (model_ok, pI, hdl, pbl, pre)

   end

   end

   let

   let

     val (meth, os) =

     val (meth, os) =

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

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

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

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

   in

   in

     (model_ok, mI, scr, pbl, pre)

     (model_ok, mI, scr, pbl, pre)

   end

   end

 fun tryrefine pI pt (p,_) =

 fun tryrefine pI pt (p,_) =

   let

   let

     val (probl, os, hdl) =

     val (probl, os, hdl) =

   in

   in

     case Specify.refine_pbl (assoc_thy "Isac") pI probl of

     case Specify.refine_pbl (assoc_thy "Isac") pI probl of

   	  NONE => (*copy from context_pbl*)

   	  NONE => (*copy from context_pbl*)

   	    let

   	    let

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

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

           (false, pI, hdl, pbl, pre)

           (false, pI, hdl, pbl, pre)

         end

         end

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

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

   end

   end

   let 

   let 

   in 

   in 

     if null cn 

     if null cn 

     then

     then

       then Solve.detailrls pt pos

       then Solve.detailrls pt pos

   end;

   end;

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

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

 fun TESTg_form ptp =

 fun TESTg_form ptp =

   let

   let

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

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

   in

   in

     case form of

     case form of

       Generate.PpcKF (

       Generate.PpcKF (

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

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

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

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

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

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

    end

    end

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

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

    compare "fun CalcTree" which DOES decode                        *)

    compare "fun CalcTree" which DOES decode                        *)

 fun CalcTreeTEST [(fmz, sp)] = 

 fun CalcTreeTEST [(fmz, sp)] = 

   let

   let

     val ((pt, p), tacis) = Chead.nxt_specify_init_calc (fmz, sp)

     val ((pt, p), tacis) = Chead.nxt_specify_init_calc (fmz, sp)

 	  val f = TESTg_form (pt,p)

 	  val f = TESTg_form (pt,p)

 | CalcTreeTEST _ = error "CalcTreeTEST: uncovered case"

 | CalcTreeTEST _ = error "CalcTreeTEST: uncovered case"

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

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

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

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

   internal view: loc_specify/solve, nxt_specify/solve used

   internal view: loc_specify/solve, nxt_specify/solve used

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

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

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

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

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

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

 	    | _ => error "me: uncovered case"

 	    | _ => error "me: uncovered case"

 	  val (_, ts) =

 	  val (_, ts) =

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

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

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

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

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

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

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

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

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

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

 	      handle ERROR msg => raise ERROR msg

 	      handle ERROR msg => raise ERROR msg

 	  val tac = 

 	  val tac = 

       case ts of 

       case ts of 

         tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end 

         tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end 

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

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

   end

   end

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

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

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

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