wneuper/isa: src/Tools/isac/BridgeLibisabelle/interface.sml@08296690e7a6

     1 (* the interface between the isac-kernel and the java-frontend;

     2    the isac-kernel holds calc-trees; stdout in XML-format.

     3    This is the only file which does not adhere to Isabelle coding standards,

     4    rather the function names are according to the respective Java methods.

     5    authors: Walther Neuper 2002

     6    (c) due to copyright terms

     8 use"Frontend/interface.sml";

     9 use"interface.sml";

    10 *)

    12 signature KERNEL =

    13   sig

    14     val appendFormula : calcID -> TermC.as_string -> XML.tree (*unit future*)

    15     val autoCalculate : calcID -> Solve.auto -> XML.tree (*unit future*)

    16     val applyTactic : calcID -> Pos.pos' -> Tactic.input -> XML.tree

    17     val CalcTree : Formalise.T list -> XML.tree

    18     val checkContext : calcID -> Pos.pos' -> Check_Unique.id -> XML.tree

    19     val DEconstrCalcTree : calcID -> XML.tree

    20     val fetchApplicableTactics : calcID -> int -> Pos.pos' -> XML.tree

    21     val fetchProposedTactic : calcID -> XML.tree

    22     val findFillpatterns : calcID -> Error_Pattern_Def.id -> XML.tree

    23     val getAccumulatedAsms : calcID -> Pos.pos' -> XML.tree

    24     val getActiveFormula : calcID -> XML.tree

    25     val getAssumptions : calcID -> Pos.pos' -> XML.tree

    26     val getFormulaeFromTo : calcID -> Pos.pos' -> Pos.pos' -> int -> bool -> XML.tree

    27     val getTactic : calcID -> Pos.pos' -> XML.tree

    28     val initContext : calcID -> Ptool.ketype -> Pos.pos' -> XML.tree

    29     val inputFillFormula: calcID -> string -> XML.tree

    30     val interSteps : calcID -> Pos.pos' -> XML.tree

    31     val Iterator : calcID -> XML.tree

    32     val IteratorTEST : calcID -> iterID

    33     val modelProblem : calcID -> XML.tree

    34     val modifyCalcHead : calcID -> P_Spec.icalhd -> XML.tree

    35     val moveActiveCalcHead : calcID -> XML.tree

    36     val moveActiveDown : calcID -> XML.tree

    37     val moveActiveFormula : calcID -> Pos.pos' -> XML.tree

    38     val moveActiveLevelDown : calcID -> XML.tree

    39     val moveActiveLevelUp : calcID -> XML.tree

    40     val moveActiveRoot : calcID -> XML.tree

    41     val moveActiveRootTEST : calcID -> XML.tree

    42     val moveActiveUp : calcID -> XML.tree

    43     val moveCalcHead : calcID -> Pos.pos' -> XML.tree

    44     val moveDown : calcID -> Pos.pos' -> XML.tree

    45     val moveLevelDown : calcID -> Pos.pos' -> XML.tree

    46     val moveLevelUp : calcID -> Pos.pos' -> XML.tree

    47     val moveRoot : calcID -> XML.tree

    48     val moveUp : calcID -> Pos.pos' -> XML.tree

    49     val refFormula : calcID -> Pos.pos' -> XML.tree

    50     val refineProblem : calcID -> Pos.pos' -> Check_Unique.id -> XML.tree

    51     val replaceFormula : calcID -> TermC.as_string -> XML.tree

    52     val requestFillformula : calcID -> Error_Pattern_Def.id * Error_Pattern_Def.fill_in_id -> XML.tree

    53     val resetCalcHead : calcID -> XML.tree

    54     val setContext : calcID -> Pos.pos' -> Check_Unique.id -> XML.tree

    55     val setMethod : calcID -> Method.id -> XML.tree

    56     val setNextTactic : calcID -> Tactic.input -> XML.tree

    57     val setProblem : calcID -> Problem.id -> XML.tree

    58     val setTheory : calcID -> ThyC.id -> XML.tree

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

    60     (* NONE *)

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

    62   end

    64 (**)

    65 structure Kernel(**): KERNEL(**) =

    66 struct

    67 (**)

    68 open Ctree

    69 open Pos

    70 (* encode "Isabelle"-strings as seen by the user to the

    71    format accepted by Isabelle.

    72    encode "^" ---> "^^^"; see Knowledge/Atools.thy;

    73    called for each cterm', icalhd, fmz in this interface;

    74    + see "fun en/decode" in /mathml.sml *)

    75 fun encode_imodel imodel =

    76   let fun enc (P_Spec.Given ifos) = P_Spec.Given (map encode ifos)

    77 	| enc (P_Spec.Find ifos) = P_Spec.Find (map encode ifos)

    78 	| enc (P_Spec.Relate ifos) = P_Spec.Relate (map encode ifos)

    79   in map enc imodel:P_Spec.imodel end;

    80 fun encode_icalhd ((pos', headl, imodel, pos_, spec) : P_Spec.icalhd) =

    81   (pos', encode headl, encode_imodel imodel, pos_, spec) : P_Spec.icalhd;

    82 fun encode_fmz (ifos, spec) = (map encode ifos, spec);

    85 (***. CalcTree .***)

    87 (** add and delete users **)

    89 (*.'Iterator 1' must exist with each CalcTree;

    90    the only for updating the calc-tree

    91    WN.0411: only 'Iterator 1' is stored,

    92    all others are just calculated on the fly

    93    TODO: adapt Iterator, add_user(= add_iterator!),etc. accordingly .*)

    94 fun Iterator cI = (*returned ID unnecessary after WN.0411*)

    95   (adduserOK2xml cI (add_user cI ))

    96   handle _ => sysERROR2xml cI "error in kernel 1";

    97 fun IteratorTEST cI = add_user cI;

    99 (*.create a calc-tree; for calls from java: thus ^^^ decoded to ^;

   100    compare "fun CalcTreeTEST" which does NOT decode.*)

   101 fun CalcTree [(fmz, sp)] (*for several variants lateron*) =

   102   	((let

   103   	    val cs = Step_Specify.nxt_specify_init_calc (encode_fmz (fmz, sp))

   104   	    val cI = add_calc cs (*FIXME.WN.8.03: error-handling missing*)

   105   	   in calctreeOK2xml cI end)

   106   	 handle _ => sysERROR2xml 0 "error in kernel 2")

   107 	| CalcTree [] = error "CalcTree: called with []"

   109 fun DEconstrCalcTree cI = deconstructcalctreeOK2xml (del_calc cI);

   110 fun getActiveFormula cI = iteratorOK2xml cI (get_pos cI 1);

   112 fun moveActiveFormula cI p =

   113   let val ((pt,_),_) = get_calc cI

   114   in

   115     if existpt' p pt

   116     then (upd_ipos cI 1 p; iteratorOK2xml cI p)

   117     else sysERROR2xml cI "frontend sends a non-existing pos"

   118   end

   120 (*. set the next tactic to be applied: dont't change the calc-tree,

   121     but remember the envisaged changes for fun autoCalculate;

   122     compare force NextTactic .*)

   123 fun setNextTactic cI tac =

   124   let

   125     val ((pt, _), _) = get_calc cI                     (* retrieve Calc.state_pre from states *)

   126     val ip = get_pos cI 1                              (* retrieve position from states  *)

   127   in

   128     case Step.by_tactic tac (pt, ip) of

   129       ("ok", (tacis, _, _)) =>                         (* update Calc.state_pre in states     *)

   130         (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "ok")

   131   	| ("unsafe-ok", (tacis, _, _)) =>

   132   	    (upd_calc cI ((pt, ip), tacis); setnexttactic2xml cI "unsafe-ok")

   133   	| ("not-applicable", _) => setnexttactic2xml cI "not-applicable"

   134   	| ("end-of-calculation", _) => setnexttactic2xml cI "end-of-calculation"

   135   	| (msg, _) => sysERROR2xml cI ("setNextTactic: Step.by_tactic returns " ^ msg)

   136   end;

   138 (*. apply a tactic at a position and update the calc-tree if applicable .*)

   139 (*WN080226 java-code is missing, errors smltest/Knowledge/polyminus.sml*)

   140 fun applyTactic cI ip tac =

   141   let

   142     val ((pt, _), _) = get_calc cI

   143 	  val p = get_pos cI 1

   144   in

   145     case Step.by_tactic tac (pt, ip) of

   146 	    ("ok", (_, c, ptp as (_, p'))) =>

   147 	      (upd_calc cI (ptp, []);

   148 	       upd_ipos cI 1 p';

   149 	       autocalculateOK2xml cI p (if null c then p' else last_elem c) p')

   150 	  | ("unsafe-ok", (_, c, ptp as (_, p'))) =>

   151 	      (upd_calc cI (ptp, []);

   152 	       upd_ipos cI 1 p';

   153 	       autocalculateOK2xml cI p (if null c then p' else last_elem c) p')

   154 	  | ("end-of-calculation", (_, c, ptp as (_, p'))) =>

   155 	      (upd_calc cI (ptp, []);

   156 	       upd_ipos cI 1 p';

   157 	       autocalculateOK2xml cI p (if null c then p' else last_elem c) p')

   158 	  | (str, _) => autocalculateERROR2xml cI ("applyTactic: Step.by_tactic returns " ^ str)

   159   end;

   161 fun fetchProposedTactic cI =

   162   (case Step.do_next (get_pos cI 1) (get_calc cI) of

   163 	  ("ok", (tacis, _, _)) =>

   164   	  let

   165   	    val _= upd_tacis cI tacis

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

   167   	  in fetchproposedtacticOK2xml cI tac (Error_Pattern.from_store tac) end

   168 	| ("helpless", _) => fetchproposedtacticERROR2xml cI "helpless"

   169 	| ("no-fmz-spec", _) => fetchproposedtacticERROR2xml cI "no-fmz-spec"

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

   171 	  fetchproposedtacticERROR2xml cI "end-of-calculation")

   172    handle _ => sysERROR2xml cI "error in kernel 3";

   174 fun autoCalculate cI auto = (*Future.fork

   175   (fn () => (( *)let

   176      val pold = get_pos cI 1

   177   in

   178     case Math_Engine.autocalc [] pold (get_calc cI) auto of

   179       ("ok", c, ptp as (_,p)) =>

   180         (upd_calc cI (ptp, []); upd_ipos cI 1 p;

   181          autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)

   182     | ("dummy", c, ptp as (_,p)) => (*prelim. until \<open>Review modelling- + specification-phase\<close>*)

   183         (upd_calc cI (ptp, []); upd_ipos cI 1 p;

   184          autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)

   185     | ("end-of-calculation", c, ptp as (_,p)) =>

   186         (upd_calc cI (ptp, []); upd_ipos cI 1 p;

   187          autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)

   188     | (str, _, _) => autocalculateERROR2xml cI str

   189   end (* ) *)

   190   handle ERROR msg => sysERROR2xml cI ("error in kernel 4: " ^ msg)(* )) *);

   192 fun getTactic cI (p:pos') =

   193   (let

   194     val ((pt, _), _) = get_calc cI

   195     val (_, tac, _) = ME_Misc.pt_extract (pt, p)

   196   in

   197     case tac of

   198  	    SOME ta => gettacticOK2xml cI ta

   199  	  | NONE => gettacticERROR2xml cI ("no tactic at position " ^ pos'2str p)

   200   end)

   201     handle _ => sysERROR2xml cI "syserror in getTactic";

   203 (* Fetch tactics to be applied to a particular step.

   204   Requirements are not yet implemented, see ICalcIterator#fetchApplicableTactics"

   205     @see #TACTICS_ALL

   206     @see #TACTICS_CURRENT_THEORY

   207     @see #TACTICS_CURRENT_METHOD  ..the only impl.WN040307

   208   LItool.specific_from_prog waits to be used here

   209 *)

   210 fun fetchApplicableTactics cI (_(*scope*): int) (p : pos') =

   211   (let val ((pt, _), _) = get_calc cI

   212   in (applicabletacticsOK cI (Fetch_Tacs.from_prog pt p))

   213      handle PTREE str => sysERROR2xml cI str

   214   end)

   215     handle _ => sysERROR2xml cI "error in kernel 5";

   217 fun getAssumptions cI (p:pos') =

   218   (let

   219     val ((pt, _), _) = get_calc cI

   220 	  val (_, _, asms) = ME_Misc.pt_extract (pt, p)

   221   in getasmsOK2xml cI asms end)

   222     handle _ => sysERROR2xml cI "syserror in getAssumptions"

   224 (*WN0502 @see ME/ctree: type asms: illdesigned, thus no positions returned*)

   225 fun getAccumulatedAsms cI (p:pos') =

   226   (let

   227     val ((pt, _), _) = get_calc cI

   228     val ass = Ctree.get_assumptions pt p

   229   in getasmsOK2xml cI ass end)

   230     handle _ => sysERROR2xml cI "syserror in getAccumulatedAsms"

   232 fun refFormula cI (p: pos') = (*WN0501 rename to "fun getElement" !*)

   233   (let

   234     val ((pt, _), _) = get_calc cI

   235 	  val (form, _, _) = ME_Misc.pt_extract (pt, p)

   236   in refformulaOK2xml cI p form end)

   237     handle _ => sysERROR2xml cI ("error in kernel 6: refFormula " ^ int2str cI ^ " " ^ pos'2str p)

   239 (* get formulae "from" "to" w.r.t. ordering in Position#compareTo(Position p);

   240    "level" is adjusted such that an "interval" of formulae is returned;

   241    "from" "to" are designed for use by iterators of calcChangedEvent,

   242    thus "from" is the last unchanged position *)

   243 fun getFormulaeFromTo cI (([], Pbl) : pos') (to as ([], Pbl) : pos') _ false =

   244     ((let

   245         val ((pt,_),_) = get_calc cI

   246         val headline =

   247           case ME_Misc.pt_extract (pt, to) of

   248               (ModSpec (_, _, headline, _, _, _), _, _) => headline

   249           | _ => raise ERROR "getFormulaeFromTo: uncovered case of ME_Misc.pt_extract"

   250     in getintervalOK cI [(to, headline, NONE)] end)

   251       handle _ => sysERROR2xml cI "error in kernel 7")

   252   | getFormulaeFromTo cI ([], Pbl) ([], Met) _ false =

   253       getFormulaeFromTo cI ([], Pbl) ([], Pbl) (~00000) false

   254   (* ^^^ separated cases, because "from" is _before_ the first elements to be returned*)

   255   | getFormulaeFromTo cI from to level false =

   256     (if from = to

   257     then sysERROR2xml cI "getFormulaeFromTo: From = To"

   258     else

   259       (case from of

   260          ([], Res) => sysERROR2xml cI ("getFormulaeFromTo does: moveDown " ^

   261            "from=([],Res) .. goes beyond result")

   262        | _ =>

   263          let

   264            val ((pt,_),_) = get_calc cI

   265            val f = move_dn [] pt from

   266            fun max (a,b) = if a < b then b else a

   267            val lev = max (level, max (lev_of from, lev_of to)) (*... must reach margins *)

   268          in getintervalOK cI (ME_Misc.get_interval f to lev pt) end)

   269     handle _ => sysERROR2xml cI "error in getFormulaeFromTo")

   270   | getFormulaeFromTo cI from to level true =

   271     sysERROR2xml cI ("getFormulaeFromTo impl.for formulae only, " ^

   272       "i.e. last arg only impl. for false, _NOT_ true");

   274 fun interSteps cI ip =

   275   (let val ((pt, p), tacis) = get_calc cI

   276   in

   277     if (not o is_interpos) ip

   278     then interStepsERROR cI ("only formulae with position (_,Res) " ^

   279       "may have intermediate steps above them")

   280     else

   281       let val ip' = lev_pred' pt ip

   282       in case Detail_Step.go pt ip of

   283         ("detailrls", pt, lastpos) =>

   284           (upd_calc cI ((pt, p), tacis); interStepsOK cI ip' ip' lastpos)

   285       | ("no-Rewrite_Set...", _, _) => sysERROR2xml cI "no Rewrite_Set..."

   286       | (_, _, lastpos) => interStepsOK cI ip' ip' lastpos

   287       end

   288   end)

   289     handle _ => sysERROR2xml cI "error in kernel 8";

   291 fun modifyCalcHead cI (ichd as ((p,_),_,_,_,_) : P_Spec.icalhd) =

   292   (let

   293     val ((pt,_),_) = get_calc cI

   294     val (pt, chd as (_,p_,_,_,_,_)) = P_Spec.input_icalhd pt ichd

   295   in (upd_calc cI ((pt, (p,p_)), []); modifycalcheadOK2xml cI chd) end)

   296     handle _ => sysERROR2xml cI "error in kernel 9";

   298 (* at the activeFormula set the Model, the Guard and the Specification to empty

   299    and return a CalcHead; the 'origin' remains (for reconstructing all that) *)

   300 fun resetCalcHead cI =

   301   (let

   302     val (ptp,_) = get_calc cI

   303     val ptp = Specification.reset_calchead ptp

   304   in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Specification.get_ocalhd ptp)) end)

   305     handle _ => sysERROR2xml cI "error in kernel 10";

   307 (* at the activeFormula insert all the Descriptions in the Model and return a CalcHead;

   308    the Descriptions are for user-guidance; the rest of the items are left empty for user-input *)

   309 fun modelProblem cI =

   310   (let val (ptp, _) = get_calc cI

   311   	val ptp = Specification.reset_calchead ptp

   312   	val (_, _, ptp) = Step_Specify.by_tactic_input Tactic.Model_Problem ptp

   313   in (upd_calc cI (ptp, []); modifycalcheadOK2xml cI (Specification.get_ocalhd ptp)) end)

   314     handle _ => sysERROR2xml cI "error in kernel 11";

   316 (* set the UContext determined on a knowledgebrowser to the current calc

   317   WN0825: not implemented in isac-java.

   318   Recalling the state of development after summer-term 2006 (Robert Koenishofer et.al.):

   319   Main success was showing UContext from Worksheet to the Example/Method/Problem/TheoryBrowser,

   320   while the buttons on these browsers <To Worksheet> <Try Refine> have no

   321   code in isac-java (and only partial, untested code in isabisac).

   322 *)

   323 fun setContext cI (ip as (_,p_)) guh =

   324   case (implode o (take_fromto 1 4) o Symbol.explode) guh of

   325     "thy_" =>

   326 	    if member op = [Pbl, Met] p_

   327       then message2xml cI "thy-context not to calchead"

   328       else if ip = ([], Res) then message2xml cI "no thy-context at result"

   329 	    else if Thy_Present.no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")

   330   	  else

   331         ((let

   332           val (ptp as (pt, pold), _) = get_calc cI

   333 		      val is = get_istate_LI pt ip

   334 		      val subs = Thy_Present.subs_from is "dummy" guh

   335 		      val tac = Thy_Present.guh2rewtac guh subs

   336   	    in

   337           case Step.by_tactic tac (pt, ip) of (*='fun setNextTactic'+step*)

   338 		        ("ok", (tacis, c, ptp as (_, p))) =>

   339 		          (upd_calc cI ((pt, p), []);

   340 		           autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)

   341 		      | ("unsafe-ok", (tacis, c, ptp as (_ ,p))) =>

   342   	         (upd_calc cI ((pt, p), []);

   343 	            autocalculateOK2xml cI pold (if null c then pold else last_elem c) p)

   344 		      | ("end-of-calculation", _) => message2xml cI "end-of-calculation"

   345 		      | ("failure", _) => sysERROR2xml cI "failure"

   346 		      | ("not-applicable", _) => (*the rule comes from anywhere..*)

   347 		          (case Step.check tac (pt, ip) of

   348 		            Applicable.No e => message2xml cI ("'" ^ Tactic.input_to_string tac ^ "' not-applicable")

   349 	            | Applicable.Yes m =>

   350 		              let

   351                     val ctxt = get_ctxt pt pold

   352                     val (p, c, _, pt) =

   353                       Step.add m (Istate.Uistate, ctxt) (pt, ip)

   354                   in upd_calc cI ((pt, p), []);

   355 	                  autocalculateOK2xml cI pold (if null c then pold else last_elem c) p

   356 		 	            end)

   357 	      end

   358      ) handle _ => sysERROR2xml cI "setContext: thy_ ???")

   359   | "pbl_" =>

   360 	  ((let

   361         val pI = Ptool.guh2kestoreID guh

   362 	      val ((pt, _), _) = get_calc cI

   363 	    in

   364         if member op = [Pbl, Met] p_

   365 	      then

   366           let val (pt, chd) = Math_Engine.set_problem pI (pt, ip)

   367 		      in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end

   368 	      else sysERROR2xml cI "setContext for pbl requires ActiveFormula on CalcHead"

   369 	   end

   370     ) handle _ => sysERROR2xml cI "setContext: pbl_ ???")

   371   | "met_" =>

   372 	  ((let

   373         val mI = Ptool.guh2kestoreID guh

   374 	      val ((pt, _), _) = get_calc cI

   375 	    in

   376         if member op = [Pbl, Met] p_

   377 	      then

   378           let val (pt, chd) = Math_Engine.set_method mI (pt, ip)

   379 		      in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end

   380 	      else sysERROR2xml cI "setContext for met requires ActiveFormula on CalcHead"

   381 	    end

   382     ) handle _ => sysERROR2xml cI "setContext: met_ ???")

   385 (* specify the Method at the activeFormula and return a CalcHead containing the Guard.

   386    WN0512 impl.incomplete, see "nxt_specif (Specify_Method" *)

   387 fun setMethod cI mI =

   388   (let

   389     val ((pt, _), _) = get_calc cI

   390     val ip as (_, p_) = get_pos cI 1

   391   in

   392     if member op = [Pbl,Met] p_

   393     then

   394       let val (pt, chd) = Math_Engine.set_method mI (pt, ip)

   395       in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end

   396     else sysERROR2xml cI "setMethod requires ActiveFormula on CalcHead"

   397   end

   398   ) handle _ => sysERROR2xml cI "error in kernel 12";

   400 (* specify the Problem at the activeFormula and return a CalcHead containing the Model;

   401    special case of checkContext; WN0512 impl.incomplete, see "nxt_specif (Specify_Problem" *)

   402 fun setProblem cI pI =

   403   (let

   404     val ((pt, _), _) = get_calc cI

   405     val ip as (_, p_) = get_pos cI 1

   406   in

   407     if member op = [Pbl,Met] p_

   408     then

   409       let val (pt, chd) = Math_Engine.set_problem pI (pt, ip)

   410 	    in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end

   411     else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"

   412   end

   413   ) handle _ => sysERROR2xml cI "error in kernel 13";

   415 (* specify the Theory at the activeFormula and return a CalcHead;

   416    special case of checkContext; WN0512 impl.incomplete, see "nxt_specif (Specify_Method" *)

   417 fun setTheory cI tI =

   418   (let

   419     val ((pt, _), _) = get_calc cI

   420     val ip as (_, p_) = get_pos cI 1

   421   in

   422     if member op = [Pbl,Met] p_

   423     then

   424       let val (pt, chd) = Math_Engine.set_theory tI (pt, ip)

   425       in (upd_calc cI ((pt, ip), []); modifycalcheadOK2xml cI chd) end

   426     else sysERROR2xml cI "setProblem requires ActiveFormula on CalcHead"

   427   end

   428   ) handle _ => sysERROR2xml cI "error in kernel 14";

   430 (* refinement for the parent-problem of the position,

   431   Not used in isac-java (see comment WN0825 for setContext) but tryrefine is used within isabisac *)

   432 fun refineProblem cI (p, p_) guh =

   433   (let

   434     val pblID = Ptool.guh2kestoreID guh

   435 	  val ((pt,_),_) = get_calc cI

   436 	  val pp = par_pblobj pt p

   437 	  val chd = Math_Engine.tryrefine pblID pt (pp, p_)

   438   in contextpblOK2xml cI chd end)

   439     handle _ => sysERROR2xml cI "error in kernel 16";

   441 (* append a formula to the calculation *)

   442 fun appendFormula' cI (ifo: TermC.as_string) =

   443   (let

   444     val cs = get_calc cI

   445     val pos = get_pos cI 1

   446   in

   447     case Step.do_next pos cs of

   448 	    ("ok", cs' as (_, _, ptp)) =>

   449 	      (case Step_Solve.by_term ptp (encode ifo) of

   450 	        ("ok", (_(*use in DG !!!*), c, ptp as (_, p))) =>

   451 	          (upd_calc cI (ptp, []); upd_ipos cI 1 p;

   452 	          appendformulaOK2xml cI pos (if null c then pos else last_elem c) p)

   453 	      | ("same-formula", (_, c, ptp as (_, p))) =>

   454 	          (upd_calc cI (ptp, []); upd_ipos cI 1 p;

   455 	          appendformulaOK2xml cI pos (if null c then pos else last_elem c) p)

   456 	      | (msg, _) => appendformulaERROR2xml cI msg)

   457 	  | (msg, _) => appendformulaERROR2xml cI msg

   458   end)

   459   handle ERROR msg => sysERROR2xml cI ("error in kernel 17: " ^ msg);

   461 fun appendFormula cI ifo = (*Future.fork (fn () => *)appendFormula' cI ifo(* ) *);

   463 (* replace a formula with_in_ a calculation; this applies for initial CAS-commands, too *)

   464 fun replaceFormula cI ifo =

   465   (let

   466     val ((pt, _), _) = get_calc cI

   467     val p = get_pos cI 1

   468   in

   469     case Step_Solve.by_term (pt, p) (encode ifo) of

   470 	    ("ok", (_(*tacs used for DG ?*), c, ptp' as (_, p'))) =>

   471 	      let

   472 	        val unc = if null (fst p) then p else move_up [] pt p

   473 	        val _ = upd_calc cI (ptp', [])

   474 	        val _ = upd_ipos cI 1 p'

   475 	      in replaceformulaOK2xml cI unc (if null c then unc else last_elem c) p' end

   476 	  | ("same-formula", _) => replaceformulaERROR2xml cI "formula not changed"

   477 	  | (msg, _) => replaceformulaERROR2xml cI msg

   478   end)

   479     handle _ => sysERROR2xml cI "error in kernel 18";

   481 (*** CalcIterator

   482     moveActive*: set the pos' of the active formula stored with the calctree

   483                  could take pos' as argument for consistency checks

   484     move*:       compute the new iterator from the old one on the fly

   485 ***)

   487 fun moveActiveRoot cI =

   488   (let val _ = upd_ipos cI 1 ([], Pbl)

   489   in iteratorOK2xml cI ([], Pbl) end)

   490   handle _ => sysERROR2xml cI "error in kernel 19"

   491 fun moveRoot cI =

   492   (iteratorOK2xml cI ([], Pbl))

   493   handle _ => sysERROR2xml cI "";

   494 fun moveActiveRootTEST cI =

   495   (let val _ = upd_ipos cI 1 ([], Pbl)

   496   in iteratorOK2xml cI ([], Pbl) end)

   497   handle _ => sysERROR2xml cI "error in kernel 20"

   499 fun moveActiveDown cI =

   500   ((let

   501     val ((pt, _), _) = get_calc cI

   502 	  val ip' = move_dn [] pt (get_pos cI 1)

   503 	  val _ = upd_ipos cI 1 ip'

   504   in iteratorOK2xml cI ip' end)

   505     handle (PTREE _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 21"

   506 fun moveDown cI p =

   507   ((let

   508     val ((pt, _), _) = get_calc cI

   509 	  val ip' = move_dn [] pt p

   510   in iteratorOK2xml cI ip' end)

   511     handle (PTREE _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 22"

   513 fun moveActiveLevelDown cI =

   514   ((let

   515     val ((pt, _) ,_) = get_calc cI

   516 	  val ip' = movelevel_dn [] pt (get_pos cI 1)

   517 	  val _ = upd_ipos cI 1 ip'

   518   in iteratorOK2xml cI ip' end)

   519     handle (PTREE _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 23"

   520 fun moveLevelDown cI p =

   521   ((let

   522     val ((pt, _), _) = get_calc cI

   523     val ip' = movelevel_dn [] pt p

   524   in iteratorOK2xml cI ip' end)

   525     handle (PTREE _) => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 24"

   527 fun moveActiveUp cI =

   528   ((let

   529     val ((pt, _), _) = get_calc cI

   530 	  val ip' = move_up [] pt (get_pos cI 1)

   531 	  val _ = upd_ipos cI 1 ip'

   532   in iteratorOK2xml cI ip' end)

   533     handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 25"

   534 fun moveUp cI p =

   535   ((let

   536     val ((pt, _), _) = get_calc cI

   537 	  val ip' = move_up [] pt p

   538   in iteratorOK2xml cI ip' end)

   539     handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 26"

   541 fun moveActiveLevelUp cI =

   542   ((let

   543     val ((pt, _), _) = get_calc cI

   544     val ip' = movelevel_up [] pt (get_pos cI 1)

   545     val _ = upd_ipos cI 1 ip'

   546   in iteratorOK2xml cI ip' end)

   547     handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 27"

   548 fun moveLevelUp cI p =

   549   ((let

   550     val ((pt, _), _) = get_calc cI

   551 	  val ip' = movelevel_up [] pt p

   552   in iteratorOK2xml cI ip' end)

   553     handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 28"

   555 fun moveActiveCalcHead cI =

   556   ((let

   557     val ((pt, _), _) = get_calc cI

   558 	  val ip' = movecalchd_up pt (get_pos cI 1)

   559 	  val _ = upd_ipos cI 1 ip'

   560   in iteratorOK2xml cI ip' end)

   561     handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 29"

   562 fun moveCalcHead cI p =

   563   ((let

   564     val ((pt, _), _) = get_calc cI

   565 	  val ip' = movecalchd_up pt p

   566   in iteratorOK2xml cI ip' end)

   567     handle PTREE _ => iteratorERROR2xml cI) handle _ => sysERROR2xml cI "error in kernel 30"

   569 (*.initContext Thy_ is conceptually impossible at [Pbl,Met]

   570    and at positions with Check_Postcond and End_Trans;

   571    at possible pos's there can be NO rewrite (returned as a context, too).*)

   572 fun initContext cI Ptool.Thy_ (pos as (p, p_):pos') =

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

   574       then message2xml cI "thy-context not to calchead"

   575       else if pos = ([], Res) then message2xml cI "no thy-context at result"

   576       else

   577         let val cs as (ptp as (pt, _), _) = get_calc cI

   578         in

   579           if exist_lev_on' pt pos

   580           then

   581             let

   582               val pos' = lev_on' pt pos

   583               val tac = Thy_Present.get_tac_checked pt pos'

   584             in

   585               if Tactic.is_rewtac tac

   586               then contextthyOK2xml cI (Thy_Present.context_thy (pt, pos) tac)

   587               else message2xml cI ("no thy-context at tac '" ^ Tactic.input_to_string tac ^ "'")

   588             end

   589           else if is_curr_endof_calc pt pos

   590           then

   591             case Step.do_next pos cs of

   592               ("ok", (tacis, _, (pt, _))) =>

   593                 let val tac = fst3 (last_elem tacis)

   594                 in

   595                   if Tactic.is_rewtac tac

   596                   then contextthyOK2xml cI (Thy_Present.context_thy ptp tac)

   597                   else message2xml cI ("no thy-context at tac '" ^ Tactic.input_to_string tac ^ "'")

   598                 end

   599             | (msg, _) => message2xml cI msg

   600           else message2xml cI "no thy-context at this position"

   601         end)

   602         handle _ => sysERROR2xml cI "error in kernel 31")

   603   | initContext cI Ptool.Pbl_ (p, p_) =

   604     ((let

   605       val ((pt, _), _) = get_calc cI

   606       val pp = par_pblobj pt p

   607       val chd = Math_Engine.initcontext_pbl pt (pp,p_)

   608     in contextpblOK2xml cI chd end)

   609       handle _ => sysERROR2xml cI "error in kernel 32")

   610   | initContext cI Ptool.Met_ (p, p_) =

   611     ((let

   612       val ((pt,_),_) = get_calc cI

   613       val pp = par_pblobj pt p

   614       val chd = Math_Engine.initcontext_met pt (pp,p_)

   615     in contextmetOK2xml cI chd end)

   616       handle _ => sysERROR2xml cI "error in kernel 33");

   618 (* match a theorem, a ruleset (etc., selected in the knowledge-browser)

   619   with the formula in the focus on the worksheet;

   620   string contains the thy, thus it is unique as thmID, rlsID for this thy;

   621   take the substitution from the istate of the formula *)

   622 fun checkContext cI (pos as (p, p_)) guh =

   623   case (implode o (take_fromto 1 4) o Symbol.explode) guh of

   624 	  "thy_" =>

   625 	    if member op = [Pbl, Met] p_

   626       then message2xml cI "thy-context not to calchead"

   627       else if pos = ([],Res) then message2xml cI "no thy-context at result"

   628       else if Thy_Present.no_thycontext guh then message2xml cI ("no thy-context for '" ^ guh ^ "'")

   629       else

   630         ((let

   631           val ((pt,_),_) = get_calc cI

   632     		  val is = get_istate_LI pt pos

   633     		  val subs = Thy_Present.subs_from is "dummy" guh

   634     		  val tac = Thy_Present.guh2rewtac guh subs

   635 	      in contextthyOK2xml cI (Thy_Present.context_thy (pt, pos) tac) end

   636         ) handle _ => sysERROR2xml cI "error in kernel 34")

   637     (*.match the model of a problem at pos p

   638       with the model-pattern of the problem with pblID.*)

   639   | "pbl_" =>

   640 	    ((let

   641 	      val ((pt, _), _) = get_calc cI

   642   	    val pp = par_pblobj pt p

   643   	    val keID = Ptool.guh2kestoreID guh

   644   	    val chd = Math_Engine.context_pbl keID pt pp

   645 	    in contextpblOK2xml cI chd end

   646       ) handle _ => sysERROR2xml cI "error in kernel 35")

   647    | "met_" =>

   648 	     ((let

   649 	       val ((pt, _), _) = get_calc cI

   650 	       val pp = par_pblobj pt p

   651 	       val keID = Ptool.guh2kestoreID guh

   652 	       val chd = Math_Engine.context_met keID pt pp

   653 	     in contextmetOK2xml cI chd end

   654       ) handle _ => sysERROR2xml cI "error in kernel 36")

   655    | str => sysERROR2xml cI ("checkContext: str = " ^ str)

   657 (*

   658   for an Error_Pattern.id find "(fill_in_id * fill_in) list"

   659    which is applicable to the current formula.

   660 *)

   661 fun findFillpatterns cI errpatID =

   662   let

   663     val ((pt, _), _) = get_calc cI

   664 		val pos = get_pos cI 1;

   665 		val fillpats = Error_Pattern.find_fill_patterns (pt, pos) errpatID

   666   in findFillpatterns2xml cI (map #1 fillpats) end

   668 (* given a fillpatID propose a fillform to the learner on the worksheet;

   669   the "ctree" is extended with fillpat and "ostate Inconsistent",

   670   the "istate" is copied and NOT updated;

   671   returns CalcChanged.

   672   arg errpatID: required because there is no dialog-related state in the math-kernel.

   673 *)

   674 fun requestFillformula cI (errpatID, fillpatID) =

   675   let

   676     val ((pt, _), _) = get_calc cI

   677 		val pos = get_pos cI 1

   678     val fillforms = Error_Pattern.find_fill_patterns (pt, pos) errpatID

   679   in

   680     case filter ((curry op = fillpatID) o

   681         (#1: (Error_Pattern_Def.fill_in_id * term * thm * (Subst.input option) -> Error_Pattern_Def.fill_in_id))) fillforms of

   682       (_, fillform, thm, sube_opt) :: _ =>

   683         let

   684           val (pt, pos') = Step.inconsistent (sube_opt, ThmC.of_thm thm)

   685             fillform (get_loc pt pos) pos pt

   686         in

   687           (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)

   688            autocalculateOK2xml cI pos pos' pos')

   689         end

   690     | _ => autocalculateERROR2xml cI "no fillpattern found"

   691   end;

   693 (* input a formula which exactly fills the gaps in a "fillformula"

   694    presented to the learner immediately before by "requestFillformula (errpatID, fillpatID)":

   695    errpatID: lhs of the respective thm = lhs of fillformula with fillpatID.

   696    The respective thm is stored in the ctree. *)

   697 fun inputFillFormula cI ifo =

   698   let

   699     val ((pt, _), _) = get_calc cI

   700     val pos = get_pos cI 1;

   701   in

   702     case Error_Pattern.filled_exactly (pt, pos) ifo of

   703       ("ok", tac) =>

   704         let

   705         in (* cp from applyTactic *)

   706           case Step.by_tactic tac (pt, pos) of

   707             ("ok", (_, c, ptp as (_,p'))) =>

   708               (upd_calc cI (ptp, []);

   709                upd_ipos cI 1 p';

   710                autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')

   711           | ("unsafe-ok", (_, c, ptp as (_,p'))) =>

   712               (upd_calc cI (ptp, []);

   713                upd_ipos cI 1 p';

   714                autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')

   715           | ("end-of-calculation", (_, c, ptp as (_,p'))) =>

   716               (upd_calc cI (ptp, []);

   717                upd_ipos cI 1 p';

   718                autocalculateOK2xml cI pos (if null c then p' else last_elem c) p')

   719           | _ => autocalculateERROR2xml cI "failure"

   720         end

   721     | (msg, _) => message2xml cI msg

   722   end

   724 (**)end(**)

author	Walther Neuper <walther.neuper@jku.at>
	Fri, 15 May 2020 14:22:05 +0200
changeset 59984	08296690e7a6
parent 59983	f1fdb213717b
child 59992	7431c60c4fcc
permissions	-rw-r--r--