theory Isac_Protocol

imports "~~/src/Tools/isac/Knowledge/Build_Thydata" (*"~~/libisabelle-protocol/libisabelle/protocol/Protocol"*) Protocol.Protocol

begin

(* val appendFormula : calcID -> cterm' -> XML.tree *)

operation_setup (sequential, bracket, auto) append_form = 

  \<open>fn intree => 

	 (let 

	   val (calcid, cterm') = case intree of

       XML.Elem (("APPENDFORMULA", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         form]) => (ci |> TermC.int_of_str, form |> xml_to_term_NEW |> Rule.term2str)

     | x => raise ERROR ("append_form: WRONG intree = " ^ xmlstr 0 x)

     val result = Kernel.appendFormula calcid cterm'

	 in result end)

	 handle ERROR msg => appendformulaERROR2xml 4711 msg\<close>

(* val autoCalculate : calcID -> auto -> XML.tree *)

operation_setup autocalculate = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, a) = case intree of

       XML.Elem (("AUTOCALC", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]), a]) => (ci, a)

     | tree => raise ERROR ("autocalculate: WRONG intree = " ^ xmlstr 0 tree)

     val SOME calcid = TermC.int_of_str_opt ci

     val auto = xml_to_auto a

     val result = Kernel.autoCalculate calcid auto

	 in result end)

	 handle ERROR msg => autocalculateERROR2xml 4711 msg)}\<close>

(* val applyTactic : calcID -> pos' -> tac -> XML.tree *)

operation_setup apply_tac = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, pos, tac) = case intree of

       XML.Elem (("AUTOCALC", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         pos, tac]) => (TermC.int_of_str ci, xml_to_pos pos, xml_to_tac tac)

       | tree => raise ERROR ("apply_tac: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.applyTactic ci pos tac

	 in result end)

	 handle ERROR msg => autocalculateERROR2xml 4711 msg)}\<close>

(* val CalcTree : fmz list -> XML.tree *)

operation_setup calctree = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let

	   val fmz = case intree of

	       tree as XML.Elem (("FORMALIZATION", []), vars) => xml_to_fmz tree

       | tree => raise ERROR ("calctree: WRONG intree = " ^ xmlstr 0 tree)

	   val result = Kernel.CalcTree fmz

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val checkContext : calcID -> pos' -> guh -> XML.tree *)

operation_setup check_ctxt = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, pos, guh) = case intree of

       XML.Elem (("CONTEXTTHY", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         pos as XML.Elem (("POSITION", []), _),

         XML.Elem (("GUH", []), [XML.Text guh])])

       => (TermC.int_of_str ci, xml_to_pos pos, guh)

     | tree => raise ERROR ("check_ctxt: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.checkContext ci pos guh

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val DEconstrCalcTree : calcID -> XML.tree *)

operation_setup deconstrcalctree = \<open>

  {from_lib = Codec.int,

   to_lib = Codec.tree,

   action = (fn calcid => 

	 let 

	   val result = Kernel.DEconstrCalcTree calcid

	 in result end)}\<close>

(* val fetchApplicableTactics : calcID -> int -> pos' -> XML.tree *)

operation_setup fetch_applicable_tacs = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, i, pos) = case intree of

       XML.Elem (("APPLICABLETACTICS", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         XML.Elem (("INT", []), [XML.Text i]),

         pos as XML.Elem (("POSITION", []), _)]) 

       => (TermC.int_of_str ci, TermC.int_of_str i, xml_to_pos pos)

     | tree => raise ERROR ("fetch_applicable_tacs: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.fetchApplicableTactics ci i pos

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val fetchProposedTactic : calcID -> XML.tree *)

operation_setup fetch_proposed_tac = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci) = case intree of

       XML.Elem (("NEXTTAC", []), [

         XML.Elem (("CALCID", []), [XML.Text ci])]) => (TermC.int_of_str ci)

       | tree => raise ERROR ("fetch_proposed_tac: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.fetchProposedTactic ci

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val findFillpatterns : calcID -> errpatID -> XML.tree *)

operation_setup find_fill_patts = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, err_pat_id) = case intree of

       XML.Elem (("FINDFILLPATTERNS", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         XML.Elem (("STRING", []), [XML.Text err_pat_id])]) 

     => (TermC.int_of_str ci, err_pat_id)

     | tree => raise ERROR ("find_fill_patts: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.findFillpatterns ci err_pat_id

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val getAccumulatedAsms : calcID -> pos' -> XML.tree *)

operation_setup get_accumulated_asms = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, pos) = case intree of

       XML.Elem (("GETASSUMPTIONS", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         pos as XML.Elem (("POSITION", []), _)]) 

     => (TermC.int_of_str ci, xml_to_pos pos)

     | tree => raise ERROR ("autocalculate: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.getAccumulatedAsms ci pos

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val getActiveFormula : calcID -> XML.tree *)

operation_setup get_active_form = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci) = case intree of

       XML.Elem (("CALCITERATOR", []), [

         XML.Elem (("CALCID", []), [XML.Text ci])]) 

     => (TermC.int_of_str ci)

     | tree => raise ERROR ("get_active_form: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.getActiveFormula ci

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val getAssumptions : calcID -> pos' -> XML.tree *)

operation_setup get_asms = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, pos) = case intree of

       XML.Elem (("APPLICABLETACTICS", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         pos as XML.Elem (("POSITION", []), _)]) 

     => (TermC.int_of_str ci, xml_to_pos pos)

     | tree => raise ERROR ("get_asms: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.getAssumptions ci pos

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val getFormulaeFromTo : calcID -> pos' -> pos' -> int -> bool -> XML.tree *)

operation_setup getformulaefromto = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let

	   val (calcid, from, to, level, rules) = case intree of

       XML.Elem (("GETFORMULAEFROMTO", []), [

         XML.Elem (("CALCID", []), [XML.Text calcid]),

         from as XML.Elem (("POSITION", []), [

           XML.Elem (("INTLIST", []), _),

           XML.Elem (("POS", []), [XML.Text _])]),

         to as XML.Elem (("POSITION", []), [

           XML.Elem (("INTLIST", []), _),

           XML.Elem (("POS", []), [XML.Text _])]),

         XML.Elem (("INT", []), [XML.Text level]),

         XML.Elem (("BOOL", []), [XML.Text rules])]) 

       => (TermC.int_of_str calcid, xml_to_pos from, xml_to_pos to, TermC.int_of_str level, string_to_bool rules)

     | tree => raise ERROR ("getformulaefromto: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.getFormulaeFromTo calcid from to level rules

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val getTactic : calcID -> pos' -> XML.tree *)

operation_setup get_tac = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, pos) = case intree of

       XML.Elem (("GETTACTIC", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         pos as XML.Elem (("POSITION", []), _)]) 

     => (TermC.int_of_str ci, xml_to_pos pos)

     | tree => raise ERROR ("get_tac: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.getTactic ci pos

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val initContext : calcID -> ketype -> pos' -> XML.tree *)

operation_setup init_ctxt = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 ((let 

	   val (ci, ketype, pos) = case intree of

       XML.Elem (("INITCONTEXT", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         ketype as XML.Elem (("KETYPE", []), _),

         pos as XML.Elem (("POSITION", []), _)]) 

     => (TermC.int_of_str ci, xml_to_ketype ketype, xml_to_pos pos)

     | tree => raise ERROR ("init_ctxt: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.initContext ci ketype pos

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)

	   handle _  => sysERROR2xml 4711 "Protocol.operation_setup init_ctxt UNKNOWN exn")}\<close>

(* val inputFillFormula: calcID -> string -> XML.tree *)

operation_setup input_fill_form = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, str) = case intree of

       XML.Elem (("AUTOCALC", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         XML.Elem (("STRING", []), [XML.Text str])]) 

     => (TermC.int_of_str ci, str)

     | tree => raise ERROR ("input_fill_form: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.inputFillFormula ci str

	 in result end)

	 handle ERROR msg => message2xml 4711 msg)}\<close>

(* val interSteps : calcID -> pos' -> XML.tree *)

operation_setup inter_steps = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, pos) = case intree of

       XML.Elem (("INTERSTEPS", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         pos as XML.Elem (("POSITION", []), _)]) 

     => (TermC.int_of_str ci, xml_to_pos pos)

     | tree => raise ERROR ("inter_steps: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.interSteps ci pos

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val Iterator : calcID -> XML.tree *)

operation_setup iterator = \<open>

  {from_lib = Codec.int,

   to_lib = Codec.tree,

   action = (fn calcid => 

	 let

     val result = Kernel.Iterator calcid

	 in result end)}\<close>

(* val IteratorTEST : calcID -> iterID *)

(* val modelProblem : calcID -> XML.tree *)

operation_setup model_pbl = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci) = case intree of

       XML.Elem (("MODIFYCALCHEAD", []), [

         XML.Elem (("CALCID", []), [XML.Text ci])]) 

     => (TermC.int_of_str ci)

     | tree => raise ERROR ("model_pbl: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.modelProblem ci

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val modifyCalcHead : calcID -> icalhd -> XML.tree *)

operation_setup modify_calchead = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, icalhd) = case intree of

       XML.Elem (("MODIFYCALCHEAD", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         icalhd]) 

     => (TermC.int_of_str ci, xml_to_icalhd icalhd)

     | tree => raise ERROR ("modify_calchead: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.modifyCalcHead ci icalhd

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val moveActiveCalcHead : calcID -> XML.tree *)

operation_setup move_active_calchead = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci) = case intree of

       XML.Elem (("CALCITERATOR", []), [

         XML.Elem (("CALCID", []), [XML.Text ci])]) 

     => (TermC.int_of_str ci)

     | tree => raise ERROR ("move_active_calchead: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.moveActiveCalcHead ci

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val moveActiveDown : calcID -> XML.tree *)

operation_setup move_active_down = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci) = case intree of

       XML.Elem (("CALCITERATOR", []), [

         XML.Elem (("CALCID", []), [XML.Text ci])]) 

     => (TermC.int_of_str ci)

     | tree => raise ERROR ("move_active_down: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.moveActiveDown ci

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val moveActiveFormula : calcID -> pos' -> XML.tree *)

operation_setup move_active_form = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, pos) = case intree of

       XML.Elem (("CALCITERATOR", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         pos as XML.Elem (("POSITION", []), _)]) 

     => (TermC.int_of_str ci, xml_to_pos pos)

     | tree => raise ERROR ("move_active_form: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.moveActiveFormula ci pos

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val moveActiveLevelDown : calcID -> XML.tree *)

operation_setup move_active_levdown = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci) = case intree of

       XML.Elem (("CALCITERATOR", []), [

         XML.Elem (("CALCID", []), [XML.Text ci])]) 

     => (TermC.int_of_str ci)

     | tree => raise ERROR ("move_active_levdown: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.moveActiveLevelDown ci

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val moveActiveLevelUp : calcID -> XML.tree *)

operation_setup move_active_levup = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci) = case intree of

       XML.Elem (("CALCITERATOR", []), [

         XML.Elem (("CALCID", []), [XML.Text ci])]) 

     => (TermC.int_of_str ci)

     | tree => raise ERROR ("move_active_levup: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.moveActiveLevelUp ci

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val moveActiveRoot : calcID -> XML.tree *)

operation_setup moveactiveroot = \<open>

  {from_lib = Codec.int,

   to_lib = Codec.tree,

   action = (fn calcid => 

	 let

	   val result = Kernel.moveActiveRoot calcid

	 in result end)}\<close>

(* val moveActiveRootTEST : calcID -> XML.tree *)

(* val moveActiveUp : calcID -> XML.tree *)

operation_setup move_active_up = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci) = case intree of

       XML.Elem (("CALCITERATOR", []), [

         XML.Elem (("CALCID", []), [XML.Text ci])]) 

     => (TermC.int_of_str ci)

     | tree => raise ERROR ("move_active_up: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.moveActiveUp ci

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val moveCalcHead : calcID -> pos' -> XML.tree *)

operation_setup move_calchead = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, pos) = case intree of

       XML.Elem (("CALCITERATOR", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         pos as XML.Elem (("POSITION", []), _)]) 

     => (TermC.int_of_str ci, xml_to_pos pos)

     | tree => raise ERROR ("move_active_calchead: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.moveCalcHead ci pos

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val moveDown : calcID -> pos' -> XML.tree *)

operation_setup move_down = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, pos) = case intree of

       XML.Elem (("CALCITERATOR", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         pos as XML.Elem (("POSITION", []), _)]) 

     => (TermC.int_of_str ci, xml_to_pos pos)

     | tree => raise ERROR ("move_down: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.moveDown ci pos

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val moveLevelDown : calcID -> pos' -> XML.tree *)

operation_setup move_levdn = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, pos) = case intree of

       XML.Elem (("CALCITERATOR", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         pos as XML.Elem (("POSITION", []), _)]) 

     => (TermC.int_of_str ci, xml_to_pos pos)

     | tree => raise ERROR ("move_levdn: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.moveLevelDown ci pos

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val moveLevelUp : calcID -> pos' -> XML.tree *)

operation_setup move_levup = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, pos) = case intree of

       XML.Elem (("CALCITERATOR", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         pos as XML.Elem (("POSITION", []), _)]) 

     => (TermC.int_of_str ci, xml_to_pos pos)

     | tree => raise ERROR ("move_levup: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.moveLevelUp ci pos

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val moveRoot : calcID -> XML.tree *)

operation_setup move_root = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci) = case intree of

       XML.Elem (("CALCITERATOR", []), [

         XML.Elem (("CALCID", []), [XML.Text ci])]) 

     => (TermC.int_of_str ci)

     | tree => raise ERROR ("move_root: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.moveRoot ci

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val moveUp : calcID -> pos' -> XML.tree *)

operation_setup move_up = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, pos) = case intree of

       XML.Elem (("CALCITERATOR", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         pos as XML.Elem (("POSITION", []), _)]) 

     => (TermC.int_of_str ci, xml_to_pos pos)

     | tree => raise ERROR ("move_up: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.moveUp ci pos

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val refFormula : calcID -> pos' -> XML.tree *)

operation_setup refformula = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, p) = case intree of

       XML.Elem (("REFFORMULA", []), [

           XML.Elem (("CALCID", []), [XML.Text ci]), p]) 

     => (ci, p)

     | tree => raise ERROR ("refformula: WRONG intree = " ^ xmlstr 0 tree)

     val SOME calcid = TermC.int_of_str_opt ci

     val pos = xml_to_pos p

     val result = Kernel.refFormula calcid pos

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val refineProblem : calcID -> pos' -> guh -> XML.tree *)

operation_setup refine_pbl = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, pos, guh) = case intree of

       XML.Elem (("CONTEXTPBL", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         pos as XML.Elem (("POSITION", []), _),

         XML.Elem (("GUH", []), [XML.Text guh])])

       => (TermC.int_of_str ci, xml_to_pos pos, guh)

     | tree => raise ERROR ("refine_pbl: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.refineProblem ci pos guh

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val replaceFormula : calcID -> cterm' -> XML.tree *)

operation_setup replace_form = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (calcid, cterm') = case intree of

       XML.Elem (("REPLACEFORMULA", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]), form]) 

       => (ci |> TermC.int_of_str, form |> xml_to_term_NEW |> Rule.term2str)

     | tree => raise ERROR ("replace_form: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.replaceFormula calcid cterm'

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val requestFillformula : calcID -> errpatID * fillpatID -> XML.tree NOT IMPL. IN isac-java *)

operation_setup request_fill_form = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, errpat_id, fillpat_id) = case intree of

       XML.Elem (("AUTOCALC", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         XML.Elem (("ERRPATTID", []), [XML.Text errpat_id]),

         XML.Elem (("FILLPATTID", []), [XML.Text fillpat_id])]) 

       => (TermC.int_of_str ci, errpat_id, fillpat_id)

     | tree => raise ERROR ("request_fill_form: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.requestFillformula ci (errpat_id, fillpat_id)

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val resetCalcHead : calcID -> XML.tree *)

operation_setup reset_calchead = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci) = case intree of

       XML.Elem (("MODIFYCALCHEAD", []), [

         XML.Elem (("CALCID", []), [XML.Text ci])]) 

     => (TermC.int_of_str ci)

     | tree => raise ERROR ("reset_calchead: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.resetCalcHead ci

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val setContext : calcID -> pos' -> guh -> XML.tree *)

operation_setup set_ctxt = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, pos, guh) = case intree of

       XML.Elem (("CONTEXT", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         pos as XML.Elem (("POSITION", []), _),

         XML.Elem (("GUH", []), [XML.Text guh])])

       => (TermC.int_of_str ci, xml_to_pos pos, guh)

     | tree => raise ERROR ("set_ctxt: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.setContext ci pos guh

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(*//===vvv TODO ================================================================\\\\\\\\\\\\\\\\*)

(* val setMethod : calcID -> metID -> XML.tree *)

operation_setup set_met = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, met_id) = case intree of

       XML.Elem (("MODIFYCALCHEAD", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         XML.Elem (("METHODID", []), [met_id])]) 

     => (TermC.int_of_str ci, xml_to_strs met_id)

     | tree => raise ERROR ("set_met: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.setMethod ci met_id

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val setNextTactic : calcID -> tac -> XML.tree *)

operation_setup set_next_tac = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, tac) = case intree of

       XML.Elem (("SETNEXTTACTIC", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         tac])

     => (TermC.int_of_str ci, xml_to_tac tac)

     | tree => raise ERROR ("set_next_tac: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.setNextTactic ci tac

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(*\\===^^^ TODO ================================================================///////////////*)

(* val setProblem : calcID -> pblID -> XML.tree *)

operation_setup set_pbl = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, pbl_id) = case intree of

       XML.Elem (("MODIFYCALCHEAD", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         XML.Elem (("PROBLEMID", []), [pbl_id])]) 

     => (TermC.int_of_str ci, xml_to_strs pbl_id)

     | tree => raise ERROR ("set_pbl: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.setProblem ci pbl_id

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* val setTheory : calcID -> thyID -> XML.tree *)

operation_setup set_thy = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val (ci, thy_id) = case intree of

       XML.Elem (("MODIFYCALCHEAD", []), [

         XML.Elem (("CALCID", []), [XML.Text ci]),

         XML.Elem (("THEORYID", []), [XML.Text thy_id])])

     => (TermC.int_of_str ci, thy_id)

     | tree => raise ERROR ("set_thy: WRONG intree = " ^ xmlstr 0 tree)

     val result = Kernel.setTheory ci thy_id

	 in result end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* for inital java-tests/isac/bridge/TestTerm.scala *)

operation_setup make_int = \<open>

  {from_lib = Codec.unit,

   to_lib = Codec.term,

   action = (fn _ => HOLogic.mk_number @{typ int} 3)}

\<close>

(* passes libisabelle term in both directions;

  the use of direction isac-java \<longrightarrow> Isabelle/Isac is a future design question *)

operation_setup test_term_transfer = \<open>

  {from_lib = Codec.tree,

   to_lib = Codec.tree,

   action = (fn intree => 

	 (let 

	   val t = case intree of

       XML.Elem (("MATHML", []), [

         XML.Elem (("ISA", []), [XML.Text _]),

         XML.Elem (("TERM", []), [xt])])

     => xt |> Codec.decode Codec.term |> Codec.the_success

     | tree => raise ERROR ("test_term_transfer: WRONG intree = " ^ xmlstr 0 tree)

     val test_out = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))

	 in  xml_of_term_NEW test_out end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

operation_setup test_term_one_way = \<open>

  {from_lib = Codec.string,

   to_lib = Codec.tree,

   action = (fn instr => 

	 (let 

	   val t = instr |> TermC.parse @{theory} |> the |> Thm.term_of

     val test_out = HOLogic.mk_eq (t, Const ("processed_by_Isabelle_Isac", type_of t))

	 in  xml_of_term_NEW test_out end)

	 handle ERROR msg => sysERROR2xml 4711 msg)}\<close>

(* tool for creating libisabelle's terms *)

operation_setup scalaterm_of_string = \<open>

  {from_lib = Codec.string,

   to_lib = Codec.tree,

   action = (fn instr => 

	 (let 

	   val termopt = TermC.parseNEW (Proof_Context.init_global @{theory}) instr

	 in

     case TermC.parseNEW (Proof_Context.init_global @{theory}) instr of

       SOME term => xml_of_term_NEW term

     | NONE => sysERROR2xml 4711 ("*** syntax ERROR in: " ^ instr)

   end))}\<close>

end