From 06a18516ba733152530b924af02dbfc8dd687a11 Mon Sep 17 00:00:00 2001 From: Aleks Kissinger Date: Wed, 10 Dec 2014 10:12:01 +0000 Subject: [PATCH 1/3] added data to ZX --- core/theories/red_green/data.ML | 6 ++++++ core/theories/red_green/io.ML | 11 +++++++++++ 2 files changed, 17 insertions(+) diff --git a/core/theories/red_green/data.ML b/core/theories/red_green/data.ML index 65c98eac..4fbada79 100644 --- a/core/theories/red_green/data.ML +++ b/core/theories/red_green/data.ML @@ -7,17 +7,20 @@ 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) = @@ -25,13 +28,16 @@ struct | 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 diff --git a/core/theories/red_green/io.ML b/core/theories/red_green/io.ML index 9d017e60..922bd2f3 100644 --- a/core/theories/red_green/io.ML +++ b/core/theories/red_green/io.ML @@ -30,6 +30,7 @@ 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") @@ -37,6 +38,9 @@ structure RG_ComponentDataIO : GRAPH_COMPONENT_DATA_IO | "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 From d9831419f45ba46f2ca842269d32bc6fd682361a Mon Sep 17 00:00:00 2001 From: Aleks Kissinger Date: Mon, 2 Feb 2015 18:09:05 +0000 Subject: [PATCH 2/3] updated to include varnodes --- .../resources/quanto/data/red_green.qtheory | 21 +++++++++++++++++++ .../quanto/gui/GraphEditController.scala | 17 ++++++++------- .../gui/graphview/BBoxDisplayData.scala | 10 ++++----- .../quanto/gui/graphview/GraphView.scala | 4 ++-- 4 files changed, 38 insertions(+), 14 deletions(-) diff --git a/scala/src/main/resources/quanto/data/red_green.qtheory b/scala/src/main/resources/quanto/data/red_green.qtheory index 5d16ebef..ea42046d 100644 --- a/scala/src/main/resources/quanto/data/red_green.qtheory +++ b/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" : { diff --git a/scala/src/main/scala/quanto/gui/GraphEditController.scala b/scala/src/main/scala/quanto/gui/GraphEditController.scala index 2f20293d..3d609d1f 100644 --- a/scala/src/main/scala/quanto/gui/GraphEditController.scala +++ b/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 "" => 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)) diff --git a/scala/src/main/scala/quanto/gui/graphview/BBoxDisplayData.scala b/scala/src/main/scala/quanto/gui/graphview/BBoxDisplayData.scala index beb66c94..34ec21b4 100644 --- a/scala/src/main/scala/quanto/gui/graphview/BBoxDisplayData.scala +++ b/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 } } diff --git a/scala/src/main/scala/quanto/gui/graphview/GraphView.scala b/scala/src/main/scala/quanto/gui/graphview/GraphView.scala index bb81d394..d06fb44a 100644 --- a/scala/src/main/scala/quanto/gui/graphview/GraphView.scala +++ b/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 From 233065de1d44d20a0f0ab6fc3155ae10e8ff3600 Mon Sep 17 00:00:00 2001 From: Aleks Kissinger Date: Mon, 2 Feb 2015 18:12:41 +0000 Subject: [PATCH 3/3] re-instate simp utils --- core/controller.thy | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/core/controller.thy b/core/controller.thy index f0ffb9d2..68e88c26 100644 --- a/core/controller.thy +++ b/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