isac-java/src/java/isac/bridge/IsacOperationsScala.scala
author Walther Neuper <wneuper@ist.tugraz.at>
Sat, 06 Feb 2016 18:44:57 +0100
changeset 4853 ac0123c9044f
parent 4851 d0e38e353a6a
child 4885 2825d1abb3e9
permissions -rw-r--r--
reduce test term transport to one way, partially

cf. https://intra.ist.tugraz.at/hg/isa/rev/35e792bef15f
Note: error in DataTypes#xml_to_Formula_NEW at
new Formula(str, Codec.term.decode(term))
wneuper@4848
     1
package isac.bridge
wneuper@4848
     2
wneuper@4848
     3
import edu.tum.cs.isabelle._
wneuper@4848
     4
import edu.tum.cs.isabelle.api.XML
wneuper@4848
     5
wneuper@4848
     6
object IsacOperationsScala {
wneuper@4848
     7
  
wneuper@4848
     8
  def implicitly[I : Codec, O : Codec](name: String): Operation[I, O] =
wneuper@4848
     9
    Operation.simple(name, Codec[I], Codec[O])
wneuper@4848
    10
wneuper@4848
    11
  // for Test_PIDE.java
wneuper@4848
    12
  val Hello = implicitly[String, String]("hello")
wneuper@4848
    13
  val Teststr = implicitly[String, String]("teststr")
wneuper@4848
    14
  val Testit = implicitly[scala.math.BigInt, XML.Tree]("testit")
wneuper@4851
    15
  val TestTermTransfer = implicitly[XML.Tree, XML.Tree]("test_term_transfer")
wneuper@4853
    16
  val TestTermOneWay = implicitly[String, XML.Tree]("test_term_one_way")
wneuper@4848
    17
  
wneuper@4848
    18
  // Protoco.thy operation_setup for all isabisac's Math_Engine --------
wneuper@4848
    19
  val appendFormula = implicitly[XML.Tree, XML.Tree]("append_form") 
wneuper@4848
    20
  val autoCalculate = implicitly[XML.Tree, XML.Tree]("autocalculate")  
wneuper@4848
    21
  val applyTactic = implicitly[XML.Tree, XML.Tree]("apply_tac")
wneuper@4848
    22
  val CalcTree = implicitly[XML.Tree, XML.Tree]("calctree")
wneuper@4848
    23
  val checkContext = implicitly[XML.Tree, XML.Tree]("check_ctxt")
wneuper@4848
    24
wneuper@4848
    25
  val DEconstrCalcTree = implicitly[scala.math.BigInt, XML.Tree]("deconstrcalctree")
wneuper@4848
    26
  val fetchApplicableTactics = implicitly[XML.Tree, XML.Tree]("fetch_applicable_tacs")
wneuper@4848
    27
  val fetchProposedTactic = implicitly[XML.Tree, XML.Tree]("fetch_proposed_tac")
wneuper@4848
    28
  val findFillpatterns = implicitly[XML.Tree, XML.Tree]("find_fill_patts")
wneuper@4848
    29
  val getAccumulatedAsms = implicitly[XML.Tree, XML.Tree]("get_accumulated_asms")
wneuper@4848
    30
wneuper@4848
    31
  val getActiveFormula = implicitly[XML.Tree, XML.Tree]("get_active_form")
wneuper@4848
    32
  val getAssumptions = implicitly[XML.Tree, XML.Tree]("get_asms")
wneuper@4848
    33
  val getFormulaeFromTo = implicitly[XML.Tree, XML.Tree]("getformulaefromto")
wneuper@4848
    34
  val getTactic = implicitly[XML.Tree, XML.Tree]("get_tac")
wneuper@4848
    35
  val initContext = implicitly[XML.Tree, XML.Tree]("init_ctxt")
wneuper@4848
    36
wneuper@4848
    37
  val inputFillFormula = implicitly[XML.Tree, XML.Tree]("input_fill_form")
wneuper@4848
    38
  val interSteps = implicitly[XML.Tree, XML.Tree]("inter_steps")
wneuper@4848
    39
  val Iterator = implicitly[scala.math.BigInt, XML.Tree]("iterator")
wneuper@4848
    40
  val modelProblem = implicitly[scala.math.BigInt, XML.Tree]("model_pbl")
wneuper@4848
    41
  val modifyCalcHead = implicitly[XML.Tree, XML.Tree]("modify_calchead")
wneuper@4848
    42
wneuper@4848
    43
  val moveActiveCalcHead = implicitly[XML.Tree, XML.Tree]("move_active_calchead")
wneuper@4848
    44
  val moveActiveDown = implicitly[XML.Tree, XML.Tree]("move_active_down")
wneuper@4848
    45
  val moveActiveFormula = implicitly[XML.Tree, XML.Tree]("move_active_form")
wneuper@4848
    46
  val moveActiveLevelDown = implicitly[XML.Tree, XML.Tree]("move_active_levdown")
wneuper@4848
    47
  val moveActiveLevelUp = implicitly[XML.Tree, XML.Tree]("move_active_levup")
wneuper@4848
    48
wneuper@4848
    49
  val moveActiveRoot = implicitly[scala.math.BigInt, XML.Tree]("moveactiveroot")
wneuper@4848
    50
  val moveActiveUp = implicitly[XML.Tree, XML.Tree]("move_active_up")
wneuper@4848
    51
  val moveCalcHead = implicitly[XML.Tree, XML.Tree]("move_calchead")
wneuper@4848
    52
  val moveDown = implicitly[XML.Tree, XML.Tree]("move_down")
wneuper@4848
    53
  val moveLevelDown = implicitly[XML.Tree, XML.Tree]("move_levdn")
wneuper@4848
    54
wneuper@4848
    55
  val moveLevelUp = implicitly[XML.Tree, XML.Tree]("move_levup")
wneuper@4848
    56
  val moveRoot = implicitly[XML.Tree, XML.Tree]("move_root")
wneuper@4848
    57
  val moveUp = implicitly[XML.Tree, XML.Tree]("move_up")
wneuper@4848
    58
  val refFormula = implicitly[XML.Tree, XML.Tree]("refformula")
wneuper@4848
    59
  val refineProblem = implicitly[XML.Tree, XML.Tree]("refine_pbl")
wneuper@4848
    60
wneuper@4848
    61
  val replaceFormula = implicitly[XML.Tree, XML.Tree]("replace_form")
wneuper@4848
    62
  val requestFillformula = implicitly[XML.Tree, XML.Tree]("request_fill_form")
wneuper@4848
    63
  val resetCalcHead = implicitly[XML.Tree, XML.Tree]("reset_calchead")
wneuper@4848
    64
  val setContext = implicitly[XML.Tree, XML.Tree]("set_ctxt")
wneuper@4848
    65
  val setMethod = implicitly[XML.Tree, XML.Tree]("set_met")
wneuper@4848
    66
wneuper@4848
    67
  val setNextTactic = implicitly[XML.Tree, XML.Tree]("set_next_tac")
wneuper@4848
    68
  val setProblem = implicitly[XML.Tree, XML.Tree]("set_pbl")
wneuper@4848
    69
  val setTheory = implicitly[XML.Tree, XML.Tree]("set_thy")
wneuper@4848
    70
  
wneuper@4848
    71
  //-------------------------------------------------------------------
wneuper@4848
    72
  val UseThys = implicitly[List[String], Unit]("use_thys")
wneuper@4848
    73
  
wneuper@4848
    74
}