Merge branch 'varnodes' into integration

core/controller.thy

@@ -10,4 +10,8 @@ ML_file "json_interface/controller.ML";
 ML_file "json_interface/controller_registry.ML";
 ML_file "json_interface/protocol.ML";
 ML_file "json_interface/run.ML";
+
+ML_file "rewriting/simp_util.ML";
+ML_file "theories/red_green/rg_simp_util.ML";
+
 end

core/theories/red_green/data.ML

@@ -7,31 +7,37 @@ struct
   datatype nvdata = Xnd of LinratAngleExpr.T (* Red: defined using H of Z *) 
                   | Znd of LinratAngleExpr.T (* Green *)
                   | Hnd (* Hadamard node *)
+                  | Var of string
   val default_nvdata = Znd LinratAngleExpr.zero
 
   fun default_nvdata_of_typestring s =
     case s of "X" => Xnd LinratAngleExpr.zero
             | "Z" => Znd LinratAngleExpr.zero
             | "hadamard" => Hnd
+            | "var" => Var ""
             | _ => raise unknown_typestring_exp s
 
   fun nvdata_eq (Hnd, Hnd) = true
     | nvdata_eq (Znd a, Znd b) = LinratAngleExpr.eq a b
     | nvdata_eq (Xnd a, Xnd b) = LinratAngleExpr.eq a b
+    | nvdata_eq (Var s, Var t) = (s = t)
     | nvdata_eq _ = false
 
   fun pretty_nvdata (Xnd a) = 
       Pretty.block [Pretty.str "X(", LinratAngleExpr.pretty a, Pretty.str ")"]  
     | pretty_nvdata (Znd a) = 
       Pretty.block [Pretty.str "Z(", LinratAngleExpr.pretty a, Pretty.str ")"]
     | pretty_nvdata Hnd = Pretty.str "H"
+    | pretty_nvdata (Var s) = Pretty.block [Pretty.str "Var(", Pretty.str s, Pretty.str ")"]
 
   fun match_nvdata (Hnd, Hnd) m = SOME m
     | match_nvdata (Znd a1,Znd a2) m = LinratAngleMatcher.match (a1,a2) m
     | match_nvdata (Xnd a1,Xnd a2) m = LinratAngleMatcher.match (a1,a2) m
+    | match_nvdata (Var s, Var t) m = if s = t then SOME m else NONE
     | match_nvdata _ _ = NONE
 
   fun subst_in_nvdata sub Hnd = (sub, Hnd)
+    | subst_in_nvdata sub (Var s) = (sub, Var s)
     | subst_in_nvdata u (Xnd a) =
         let val (sub',a') = LinratAngleMatcher.subst_in_expr u a
         in (sub', Xnd a') end

core/theories/red_green/io.ML

@@ -30,13 +30,17 @@ structure RG_ComponentDataIO : GRAPH_COMPONENT_DATA_IO
               | "h" => RG_Data.Hnd
               | "x" => RG_Data.Xnd LinratAngleExpr.zero
               | "z" => RG_Data.Znd LinratAngleExpr.zero
+              | "var" => RG_Data.Var ""
               | _   => raise bad_input_exp ("Unknown vertex type "^t,""))
       | input (Json.Object obj) =
           (case to_lower (get_string obj "type")
              of "hadamard" => RG_Data.Hnd
               | "h" => RG_Data.Hnd
               | "z" => RG_Data.Znd (get_angle obj)
               | "x" => RG_Data.Xnd (get_angle obj)
+              | "var" => RG_Data.Var (case Json.lookup obj "value"
+                                        of SOME (Json.String s) => s
+                                         | NONE => "")
               | t   => raise bad_input_exp ("Unknown vertex type "^t,"type"))
       | input _ = raise bad_input_exp ("Expected object","")
   end
@@ -61,6 +65,11 @@ structure RG_ComponentDataIO : GRAPH_COMPONENT_DATA_IO
           Json.Object (
             Json.empty_obj |> update ("type",Json.String "hadamard")
           )
+      | output (RG_Data.Var s) =
+          Json.Object (
+            Json.empty_obj |> update ("type", Json.String "var")
+                           |> update ("value", Json.String s)
+          )
   end
   structure EDataInputJSON = InputUnitJSON
   structure EDataOutputJSON = OutputUnitJSON
@@ -72,6 +81,8 @@ structure RG_ComponentDataIO : GRAPH_COMPONENT_DATA_IO
           "[style=filled,fillcolor=green,fontcolor=black,shape=circle]"
       | style_for_ivertex_data (RG_Data.Xnd _) =
           "[style=filled,fillcolor=red,fontcolor=white,shape=circle]"
+      | style_for_ivertex_data (RG_Data.Var _) =
+          "[style=filled,fillcolor=white,fontcolor=black,shape=circle]"
       | style_for_ivertex_data RG_Data.Hnd =
           "[style=filled,fillcolor=yellow,fontcolor=white,shape=square]"
   end

scala/src/main/resources/quanto/data/red_green.qtheory

@@ -64,6 +64,27 @@
         "type" : "hadamard",
         "value" : ""
       }
+    },
+    "var" : {
+      "value" : {
+        "path" : "$.value",
+        "validate_with_core" : false,
+        "latex_constants" : false,
+        "type" : "string"
+      },
+      "style" : {
+        "label" : {
+          "position" : "inside",
+          "fg_color" : [ 0.0, 0.0, 0.0 ]
+        },
+        "stroke_color" : [ 0.0, 0.0, 0.0 ],
+        "fill_color" : [ 0.6, 1.0, 0.8 ],
+        "shape" : "rectangle"
+      },
+      "default_data" : {
+        "type" : "var",
+        "value" : ""
+      }
     }
   },
   "edge_types" : {

scala/src/main/scala/quanto/gui/GraphEditController.scala

@@ -110,11 +110,11 @@ class GraphEditController(view: GraphView, undoStack: UndoStack, val readOnly: B
   // note we need start *and* previous position to do accurate dragging with snapping
   private def shiftVertsNoRegister(vs: TraversableOnce[VName], start: Point, prev: Point, end: Point) {
     val dx =
-      roundCoordIfSnapped(view.trans scaleFromScreen (end.getX - start.getX)) -
-      roundCoordIfSnapped(view.trans scaleFromScreen (prev.getX - start.getX))
+      roundIfSnapped(view.trans scaleFromScreen (end.getX - start.getX)) -
+      roundIfSnapped(view.trans scaleFromScreen (prev.getX - start.getX))
     val dy =
-      roundCoordIfSnapped(view.trans scaleFromScreen (end.getY - start.getY)) -
-      roundCoordIfSnapped(view.trans scaleFromScreen (prev.getY - start.getY))
+      roundIfSnapped(view.trans scaleFromScreen (end.getY - start.getY)) -
+      roundIfSnapped(view.trans scaleFromScreen (prev.getY - start.getY))
     //val (dx,dy) = (view.trans scaleFromScreen (p2.getX - p1.getX), view.trans scaleFromScreen (p2.getY - p1.getY))
     graph = vs.foldLeft(graph) { (g,v) =>
       view.invalidateVertex(v)
@@ -158,7 +158,8 @@ class GraphEditController(view: GraphView, undoStack: UndoStack, val readOnly: B
 
 
   private def addVertex(v: VName, d: VData) {
-    graph = graph.addVertex(v, d)
+    val d1 = d.withCoord(roundCoordIfSnapped(d.coord))
+    graph = graph.addVertex(v, d1)
     undoStack.register("Add Vertex") { deleteVertex(v) }
   }
 
@@ -313,10 +314,12 @@ class GraphEditController(view: GraphView, undoStack: UndoStack, val readOnly: B
     view.repaint()
   }
 
-  private def roundCoordIfSnapped(d : Double) = {
+  private def roundIfSnapped(d : Double) = {
     if (keepSnapped) math.rint(d / 0.25) * 0.25 else d // rounds to .25
   }
 
+  private def roundCoordIfSnapped(d : (Double, Double)) = (roundIfSnapped(d._1), roundIfSnapped(d._2))
+
   def layoutGraph() {
     val lo = new ForceLayout with Ranking with Clusters
     val t0 = System.currentTimeMillis()
@@ -532,7 +535,7 @@ class GraphEditController(view: GraphView, undoStack: UndoStack, val readOnly: B
               case "<wire>" => WireV(theory = theory)
               case typ      =>
                 //              println("adding: " + theory.vertexTypes(typ).defaultData)
-                NodeV(data = theory.vertexTypes(typ).defaultData, theory = theory).withCoord(coord)
+                NodeV(data = theory.vertexTypes(typ).defaultData, theory = theory)
             }
 
             addVertex(graph.verts.freshWithSuggestion(VName("v0")), vertexData.withCoord(coord))

scala/src/main/scala/quanto/gui/graphview/BBoxDisplayData.scala

@@ -14,11 +14,11 @@ case class BBDisplay(rect: Rectangle2D) {
 
   def pointHit(pt: Point2D) = rect.contains(pt)
   def cornerHit(pt : Point2D) = corner.contains(pt)
-  def insideRect(other_rect: Rectangle2D) : Boolean = {
-    other_rect.getMinX <= rect.getMinX &&
-    other_rect.getMinY <= rect.getMinY &&
-    other_rect.getMaxX >= rect.getMaxX &&
-    other_rect.getMaxY >= rect.getMaxY
+  def insideRect(otherRect: Rectangle2D) : Boolean = {
+    otherRect.getMinX <= rect.getMinX &&
+    otherRect.getMinY <= rect.getMinY &&
+    otherRect.getMaxX >= rect.getMaxX &&
+    otherRect.getMaxY >= rect.getMaxY
   }
 }
 

scala/src/main/scala/quanto/gui/graphview/GraphView.scala

@@ -662,8 +662,8 @@ object GraphView {
   final val ArrowheadLength = 0.15
   final val ArrowheadAngle = 0.2 * Pi
   final val EdgeSelectionRadius = 3.0
-  final val VertexLabelFont = new Font("Dialog", AWTFont.PLAIN, 12)
-  final val EdgeLabelFont = new Font("Dialog", AWTFont.PLAIN, 10)
+  final val VertexLabelFont = new Font("Dialog", AWTFont.PLAIN, 8)
+  final val EdgeLabelFont = new Font("Dialog", AWTFont.PLAIN, 8)
 
   final val zoomCutOut = 0.36