TestApp shows which formulas are axioms

src/testapp/TestApp.scala

@@ -278,8 +278,8 @@ class TestApp extends JFXApp {
           """Loading the theory from the previous session failed.
           |Start with a fresh theory?
           |(Looses the data from the previous session.)""".stripMargin)
-      if (!newThy) sys.exit(1)
-        for (m <- TestApp.examples) theoryView.theory.addFormula(Formula(m))
+        if (!newThy) sys.exit(1)
+//        for (m <- TestApp.examples) theoryView.theory.addFormula(Formula(m))
     }
   }
 

src/theory/Theory.scala

@@ -117,7 +117,7 @@ final case class Formula private[theory] (id : Int = NO_ID,
   def detach: Formula = copy(id=NO_ID)
   def toXML = {
     val propXML = for {
-      (prop, value) <- properties
+      (prop, value) <- properties // .asInstanceOf[Iterable[(Property[T],T) forSome {type T}]]
       name : String = prop.name
       text : String = prop.asInstanceOf[Property[Any]].toText(value)
     } yield new UnprefixedAttribute(name, text, scala.xml.Null)
@@ -137,12 +137,11 @@ final case class Formula private[theory] (id : Int = NO_ID,
 }
 
 object Formula {
-  sealed abstract class Property[T](val default : T) {
+  sealed abstract class Property[T](val default : T)(implicit val valueType : TypeTag[T]) {
     val name = Utils.lowerFirst(getClass.getSimpleName.stripSuffix("$"))
     @inline protected def toText$(value : Boolean) : String = value.toString
     def toText(value : T) : String
     def fromText(text: String) : T
-    type ValueType = T
   }
   /*private */val properties = mutable.HashMap[String,Property[_]](findProperties : _*)
 

src/ui/TheoryView.scala

@@ -5,7 +5,7 @@ import javafx.scene.input.{MouseButton, MouseEvent}
 import javafx.scene.layout.HBox
 
 import cmathml.CMathML.internal
-import cmathml.Logic
+import cmathml.{CMathML, Logic}
 import misc.Log
 import misc.Utils.ImplicitConversions._
 import theory.{Formula, MutableTheory}
@@ -41,7 +41,7 @@ class TheoryView extends VBox {
     override def formulaUpdated(newFormula: Formula, oldFormula: Formula): Unit = {
       assert(newFormula.id==oldFormula.id)
       val edit = nodes(newFormula.id)
-      edit.mathEdit.setMath(newFormula.math)
+      edit.setFormula(newFormula)
     }
     override def theoryCleared(): Unit = {
       children.clear()
@@ -64,7 +64,7 @@ class TheoryView extends VBox {
     assert(!nodes.contains(id),"formula with id "+id+" added twice")
 //    val mathedit = new MathEdit()
     val formulaBox = new FormulaBox(id)
-    formulaBox.mathEdit.setMath(form.math)
+    formulaBox.setFormula(form)
     formulaBox.mathEdit.focused.onChange { (_, oldVal,newVal) =>
       if (newVal) selectedFormulaId = Some(id) }
     formulaBox.mathEdit.addEventHandler(MouseEvent.MOUSE_CLICKED, { e:MouseEvent =>
@@ -81,8 +81,22 @@ class TheoryView extends VBox {
 object TheoryView {
   private[TheoryView] class FormulaBox(val id:Int) extends HBox {
     val mathEdit = new MathEdit()
+    private val propsLabel = new Label("")
     alignmentProperty.setValue(Pos.CenterLeft)
-    getChildren.addAll(new Label(s"($id) "),mathEdit)
+    getChildren.addAll(new Label(s"($id) "), mathEdit, propsLabel)
+
+    def setFormula(formula: Formula): Unit = {
+      assert(id==formula.id)
+      mathEdit.setMath(formula.math)
+      val props = for {
+        (prop, value) <- formula.properties
+        if value != false
+      } yield if (value==true) prop.name else s"${prop.name}=$value"
+      if (props.isEmpty)
+        propsLabel.setText("")
+      else
+        propsLabel.setText(props.mkString(" (", ", ", ")"))
+    }
   }
   private[TheoryView] class TrafoBox(val trafo: TrafoInstance) extends HBox {
     val mathEdit = new MathView()

src/z3/Z3.scala

@@ -65,8 +65,8 @@ final class Z3(config:Map[String,String]) {
     case e: Expr if e.isConst => CI(e.getFuncDecl.getName.toString)
     case e: ArithExpr if e.isApp =>
       (e.getFuncDecl.getDeclKind,e.getNumArgs) match {
-        case (Z3_OP_ADD,2) => Apply(arith1.plus, e.getArgs map toCMathML: _*)
-        case (Z3_OP_MUL,2) => Apply(arith1.times, e.getArgs map toCMathML: _*)
+        case (Z3_OP_ADD,_) => Apply(arith1.plus, e.getArgs map toCMathML: _*)
+        case (Z3_OP_MUL,_) => Apply(arith1.times, e.getArgs map toCMathML: _*)
         case (Z3_OP_SUB,2) => Apply(arith1.minus, e.getArgs map toCMathML: _*)
         case (Z3_OP_DIV,2) => Apply(arith1.divide, e.getArgs map toCMathML: _*)
         case (Z3_OP_UMINUS,1)=> Apply(arith1.uminus, e.getArgs map toCMathML: _*)