From d63d454682ac7c0aa3f54f882aaffc7872319b00 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Mon, 9 Oct 2023 11:15:51 +0100 Subject: [PATCH 01/18] Remove unused (wider-scoped) duplicate definitions of separated and S(^)\* --- specification/hugr.md | 6 ------ 1 file changed, 6 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 4134da96b..47608ac30 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1143,12 +1143,6 @@ is itself in S. The meaning of “convex” is: if A and B are nodes in the convex set S, then any sibling node on a path from A to B is also in S. -Given a set S of nodes in a hugr, let S\* be the set of all nodes -descended from nodes in S, including S itself. - -Call two nodes a, b in Γ *separated* if a is not in {b}\* and b is not -in {a}\* (i.e. there is no hierarchy relation between them). - #### API methods There are the following primitive operations. From ca1af212b84fee95c13bcd13f7f043cf0de73b31 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Mon, 9 Oct 2023 12:35:13 +0100 Subject: [PATCH 02/18] Add note separated is hierarchy equivalent of dataflow convexity --- specification/hugr.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/specification/hugr.md b/specification/hugr.md index 47608ac30..77414304d 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1206,7 +1206,9 @@ descended from nodes in $S$ (i.e. reachable from $S$ by following hierarchy edge including $S$ itself. Call two nodes $a, b \in \Gamma$ _separated_ if $a \notin \\{b\\}^\*$ and -$b \notin \\{a\\}^\*$ (i.e. there is no hierarchy relation between them). +$b \notin \\{a\\}^\*$ (i.e. there is no hierarchy relation between them). Note +that this is much the same requirement as convexity, but following the hierarchy +edges rather than dataflow edges. A `NewEdgeSpec` specifies an edge inserted between an existing node and a new node. It contains the following fields: From f04f42ba6991a23b64f9855ba9033a53eff59e6c Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Mon, 9 Oct 2023 13:20:45 +0100 Subject: [PATCH 03/18] Reuse previous idea of "mutually-separated" --- specification/hugr.md | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 77414304d..6608f7249 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1229,9 +1229,8 @@ The `Replace` method takes as input: - a set $S$ of mutually-separated nodes in $\Gamma$; - a partial hugr $G$; - a map $T : \top(G) \to \Gamma \setminus S^*$ whose image consists of container nodes; - - a map $B : \bot(G) \to S^\*$ whose image consists of container nodes, such that $B(x)$ - is separated from $B(y)$ unless $x = y$. Let $X$ be the set of children - of nodes in the image of $B$, and $R = S^\* \setminus X^\*$. + - a map $B : \bot(G) \to S^\*$ whose image consists of mutually-separated container nodes. + Let $X$ be the set of children of nodes in the image of $B$, and $R = S^\* \setminus X^\*$. - a list $\mu\_\textrm{inp}$ of `NewEdgeSpec` which all have their `TgtNode`in $G$ and `SrcNode` in $\Gamma \setminus S^*$; - a list $\mu\_\textrm{out}$ of `NewEdgeSpec` which all have their `SrcNode`in From 3b08d839509ba7805d38f49b0c8fb2d00dbc8820 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Mon, 9 Oct 2023 13:25:12 +0100 Subject: [PATCH 04/18] p* only for _copied_ ports p of R --- specification/hugr.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 6608f7249..a237e879b 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1178,8 +1178,8 @@ The new hugr is then derived as follows: 1. Make a copy in $\Gamma$ of all children of $R$, excluding Input and Output, and all edges between them. Make all the newly added nodes children of $P$. - Notation: if $p$ is a port of a node in $R$, write $p^*$ for the copy of - the port in $\Gamma$. + Notation: for each port $p$ of a node in $R$ of which a copy is made, write + $p^*$ for the copy of the port in $\Gamma$. 2. For each $(q, p = \nu_\textrm{inp}(q))$ such that $q \notin \texttt{Output}$, add an edge from $p^-$ to $q^*$. 3. For each $(p, q = \nu_\textrm{out}(p))$ such that $q^- \notin \texttt{Input}$, From e089df701c327ef8042e89cfb3817b11e44398c6 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Mon, 9 Oct 2023 13:28:42 +0100 Subject: [PATCH 05/18] SimpleReplace: avoid defining T....ok, quite complex, probably revert --- specification/hugr.md | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index a237e879b..a63251307 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1143,6 +1143,10 @@ is itself in S. The meaning of “convex” is: if A and B are nodes in the convex set S, then any sibling node on a path from A to B is also in S. +Given a set $S$ of nodes in a hugr, let $S^\*$ be the set of all nodes +descended from nodes in $S$ (i.e. reachable from $S$ by following hierarchy edges), +including $S$ itself. + #### API methods There are the following primitive operations. @@ -1169,10 +1173,9 @@ The method takes as input: - a DFG-convex set $S$ of IDs of leaf nodes that are children of $P$ (not including the Input and Output nodes), and that have no incoming or outgoing Ext edges; - - a hugr $H$ whose root is a DFG node $R$ with only leaf nodes as children -- - let $T$ be the set of children of $R$; - - a map $\nu\_\textrm{inp}: \textrm{inp}\_H(T \setminus \\{\texttt{Input}\\}) \to \textrm{inp}\_{\Gamma}(S)$; - - a map $\nu_\textrm{out}: \textrm{out}_{\Gamma}(S) \to \textrm{out}_H(T \setminus \\{\texttt{Output}\\})$. + - a hugr $H$ whose root is a DFG node $R$ with only leaf nodes as children + - a map $\nu\_\textrm{inp}: \textrm{inp}\_H(R^\* \setminus \\{\texttt{R, Input}\\}) \to \textrm{inp}\_{\Gamma}(S)$; + - a map $\nu_\textrm{out}: \textrm{out}_{\Gamma}(S) \to \textrm{out}_H(R^\* \setminus \\{\texttt{R, Output}\\})$. The new hugr is then derived as follows: @@ -1201,10 +1204,6 @@ Given a partial hugr $G$, let - $\top(G)$ be the set of nodes in $G$ without an incoming hierarchy edge; - $\bot(G)$ be the set of container nodes in $G$ without an outgoing hierarchy edge. -Given a set $S$ of nodes in a hugr, let $S^\*$ be the set of all nodes -descended from nodes in $S$ (i.e. reachable from $S$ by following hierarchy edges), -including $S$ itself. - Call two nodes $a, b \in \Gamma$ _separated_ if $a \notin \\{b\\}^\*$ and $b \notin \\{a\\}^\*$ (i.e. there is no hierarchy relation between them). Note that this is much the same requirement as convexity, but following the hierarchy From 65e4d04813065f1bc6520255447b87f97f6c06ab Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Mon, 9 Oct 2023 13:49:53 +0100 Subject: [PATCH 06/18] Revert "SimpleReplace: avoid defining T....ok, quite complex, probably revert" This reverts commit f3e0150a5d5ec889bff68e93844255fb1a8f7c68. --- specification/hugr.md | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index a63251307..a237e879b 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1143,10 +1143,6 @@ is itself in S. The meaning of “convex” is: if A and B are nodes in the convex set S, then any sibling node on a path from A to B is also in S. -Given a set $S$ of nodes in a hugr, let $S^\*$ be the set of all nodes -descended from nodes in $S$ (i.e. reachable from $S$ by following hierarchy edges), -including $S$ itself. - #### API methods There are the following primitive operations. @@ -1173,9 +1169,10 @@ The method takes as input: - a DFG-convex set $S$ of IDs of leaf nodes that are children of $P$ (not including the Input and Output nodes), and that have no incoming or outgoing Ext edges; - - a hugr $H$ whose root is a DFG node $R$ with only leaf nodes as children - - a map $\nu\_\textrm{inp}: \textrm{inp}\_H(R^\* \setminus \\{\texttt{R, Input}\\}) \to \textrm{inp}\_{\Gamma}(S)$; - - a map $\nu_\textrm{out}: \textrm{out}_{\Gamma}(S) \to \textrm{out}_H(R^\* \setminus \\{\texttt{R, Output}\\})$. + - a hugr $H$ whose root is a DFG node $R$ with only leaf nodes as children -- + let $T$ be the set of children of $R$; + - a map $\nu\_\textrm{inp}: \textrm{inp}\_H(T \setminus \\{\texttt{Input}\\}) \to \textrm{inp}\_{\Gamma}(S)$; + - a map $\nu_\textrm{out}: \textrm{out}_{\Gamma}(S) \to \textrm{out}_H(T \setminus \\{\texttt{Output}\\})$. The new hugr is then derived as follows: @@ -1204,6 +1201,10 @@ Given a partial hugr $G$, let - $\top(G)$ be the set of nodes in $G$ without an incoming hierarchy edge; - $\bot(G)$ be the set of container nodes in $G$ without an outgoing hierarchy edge. +Given a set $S$ of nodes in a hugr, let $S^\*$ be the set of all nodes +descended from nodes in $S$ (i.e. reachable from $S$ by following hierarchy edges), +including $S$ itself. + Call two nodes $a, b \in \Gamma$ _separated_ if $a \notin \\{b\\}^\*$ and $b \notin \\{a\\}^\*$ (i.e. there is no hierarchy relation between them). Note that this is much the same requirement as convexity, but following the hierarchy From b1a86502676b78b51a0afaca7c4bac686c7c492e Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Mon, 9 Oct 2023 14:01:50 +0100 Subject: [PATCH 07/18] SimpleReplace: note about inputs/outputs --- specification/hugr.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index a237e879b..bd6654468 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1171,8 +1171,8 @@ The method takes as input: Ext edges; - a hugr $H$ whose root is a DFG node $R$ with only leaf nodes as children -- let $T$ be the set of children of $R$; - - a map $\nu\_\textrm{inp}: \textrm{inp}\_H(T \setminus \\{\texttt{Input}\\}) \to \textrm{inp}\_{\Gamma}(S)$; - - a map $\nu_\textrm{out}: \textrm{out}_{\Gamma}(S) \to \textrm{out}_H(T \setminus \\{\texttt{Output}\\})$. + - a map $\nu\_\textrm{inp}: \textrm{inp}\_H(T \setminus \\{\texttt{Input}\\}) \to \textrm{inp}\_{\Gamma}(S)$ (*note* in order to produce a valid Hugr, all keys must be present; and all possible values must be present exactly once unless Copyable); + - a map $\nu_\textrm{out}: \textrm{out}_{\Gamma}(S) \to \textrm{out}_H(T \setminus \\{\texttt{Output}\\})$ (*note* (similarly) in order to produce a valid hugr, all keys $\textrm{out}_{\Gamma}(S)$ must be present; and each possible value must be either Copyable and/or present exactly once. Any possible value not present could just be omitted from $H$...). The new hugr is then derived as follows: From f010e49079e1e788c84cd231118801d3b361b606 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Mon, 9 Oct 2023 16:14:11 +0100 Subject: [PATCH 08/18] Update InsertConst/RemoveConst: any region, no Order edge --- specification/hugr.md | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index bd6654468..1080b61dc 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1346,13 +1346,12 @@ it (and its incoming value and Order edges) from the hugr. ###### `InsertConst` -Given a `Const` node `c` and a DSG `P`, add `c` as a child of `P`, -inserting an Order edge from the Input under `P` to `c`. +Given a `Const` node `c` and a container node `P` (either a `Module`, + a `CFG` node or a dataflow container), add `c` as a child of `P`. ###### `RemoveConst` -Given a `Const` node `c` having no outgoing edges, remove `c` -together with its incoming `Order` edge. +Given a `Const` node `c` having no outgoing edges, remove `c`. #### Usage From 22ed6d0180d23b264d916c4e71f08d72114da746 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Tue, 10 Oct 2023 11:25:34 +0100 Subject: [PATCH 09/18] Attempt to update Replace with single parent --- specification/hugr.md | 48 ++++++++++++++++++++++++------------------- 1 file changed, 27 insertions(+), 21 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 1080b61dc..8cb0be493 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1171,8 +1171,13 @@ The method takes as input: Ext edges; - a hugr $H$ whose root is a DFG node $R$ with only leaf nodes as children -- let $T$ be the set of children of $R$; - - a map $\nu\_\textrm{inp}: \textrm{inp}\_H(T \setminus \\{\texttt{Input}\\}) \to \textrm{inp}\_{\Gamma}(S)$ (*note* in order to produce a valid Hugr, all keys must be present; and all possible values must be present exactly once unless Copyable); - - a map $\nu_\textrm{out}: \textrm{out}_{\Gamma}(S) \to \textrm{out}_H(T \setminus \\{\texttt{Output}\\})$ (*note* (similarly) in order to produce a valid hugr, all keys $\textrm{out}_{\Gamma}(S)$ must be present; and each possible value must be either Copyable and/or present exactly once. Any possible value not present could just be omitted from $H$...). + - a map $\nu\_\textrm{inp}: \textrm{inp}\_H(T \setminus \\{\texttt{Input}\\}) \to \textrm{inp}\_{\Gamma}(S)$; note that + * $\nu\_\textrm{inp}: \textrm{inp}\_H(T \setminus \\{\texttt{Input}\\})$ is just "the successors of $\texttt{Input}$", so could be expressed as outputs of the $\texttt{Input}$ node + * in order to produce a valid Hugr, all possible keys must be present; and all possible values must be present exactly once unless Copyable); + - a map $\nu_\textrm{out}: \textrm{out}_{\Gamma}(S) \to \textrm{out}_H(T \setminus \\{\texttt{Output}\\})$; again note that + * $\textrm{out}_H(T \setminus \\{\texttt{Output}\\})$ is just the input ports to the $\texttt{Output}$ node (their source must all be in $H$) + * in order to produce a valid hugr, all keys $\textrm{out}_{\Gamma}(S)$ must be present + * ...and each possible value must be either Copyable and/or present exactly once. Any that is absent could just be omitted from $H$.... The new hugr is then derived as follows: @@ -1193,22 +1198,21 @@ The new hugr is then derived as follows: This is the general subgraph-replacement method. -A _partial hugr_ is a graph formed by a subset of nodes of a valid hugr together -with a subset of their adjoining edges. It must not include a `Module` node. +# A _partial hugr_ is a graph formed by a subset of nodes of a valid hugr together +# with a subset of their adjoining edges. -Given a partial hugr $G$, let +# Given a partial hugr $G$, let - - $\top(G)$ be the set of nodes in $G$ without an incoming hierarchy edge; - - $\bot(G)$ be the set of container nodes in $G$ without an outgoing hierarchy edge. +# - $\bot(G)$ be the set of container nodes in $G$ without an outgoing hierarchy edge. Given a set $S$ of nodes in a hugr, let $S^\*$ be the set of all nodes descended from nodes in $S$ (i.e. reachable from $S$ by following hierarchy edges), including $S$ itself. -Call two nodes $a, b \in \Gamma$ _separated_ if $a \notin \\{b\\}^\*$ and -$b \notin \\{a\\}^\*$ (i.e. there is no hierarchy relation between them). Note -that this is much the same requirement as convexity, but following the hierarchy -edges rather than dataflow edges. +# Call two nodes $a, b \in \Gamma$ _separated_ if $a \notin \\{b\\}^\*$ and +# $b \notin \\{a\\}^\*$ (i.e. there is no hierarchy relation between them). Note +# that this is much the same requirement as convexity, but following the hierarchy +# edges rather than dataflow edges. A `NewEdgeSpec` specifies an edge inserted between an existing node and a new node. It contains the following fields: @@ -1225,11 +1229,14 @@ Note that in a `NewEdgeSpec` one of `SrcNode` and `TgtNode` is an existing node in the hugr and the other is a new node. The `Replace` method takes as input: - - - a set $S$ of mutually-separated nodes in $\Gamma$; - - a partial hugr $G$; - - a map $T : \top(G) \to \Gamma \setminus S^*$ whose image consists of container nodes; - - a map $B : \bot(G) \to S^\*$ whose image consists of mutually-separated container nodes. + - the ID of a DFG node $P$ in $\Gamma$; + - a set $S$ of IDs of nodes that are children of $P$ + - a Hugr $H$ whose root is a node of the same type as $P$. Note this Hugr need not be valid, in that it may be missing: + * edges to/from some ports (i.e. it may have unconnected ports)---not just Copyable dataflow outputs, which may occur even in valid Hugrs, but also incoming and/or non-Copyable dataflow ports, and ControlFlow ports, + * children for some container nodes (i.e. it may have container nodes with no outgoing hierarchy edges) + * $\mathtt{Input}$ and/or $\mathtt{Output}$ children of $P$ (if $P$ is a dataflow container node) + * A basic block exit node as a child of $P$ (if $P$ is a CFG node) + - a map $B$ *from* container nodes in $H$ that have no children *to* container nodes in $S^\*$ none of which is an ancestor of another. Let $X$ be the set of children of nodes in the image of $B$, and $R = S^\* \setminus X^\*$. - a list $\mu\_\textrm{inp}$ of `NewEdgeSpec` which all have their `TgtNode`in $G$ and `SrcNode` in $\Gamma \setminus S^*$; @@ -1239,17 +1246,16 @@ The `Replace` method takes as input: The new hugr is then derived as follows: -1. Make a copy in $\Gamma$ of all the nodes in $G$, and all edges between them. -2. For each $\sigma\_\mathrm{inp} \in \mu\_\textrm{inp}$, insert a new edge going into the new +1. Make a copy in $\Gamma$ of all the nodes in $H$ *except the root*, and all edges where both source and target are copied. +2. For each child of the root of $H$, make the corresponding copy in $\Gamma$ be a child of $P$. +3. For each $\sigma\_\mathrm{inp} \in \mu\_\textrm{inp}$, insert a new edge going into the new copy of the `TgtNode` of $\sigma\_\mathrm{inp}$ according to the specification $\sigma\_\mathrm{inp}$. Where these edges are from ports that currently have edges to nodes in $R$, the existing edges are replaced. -3. For each $\sigma\_\mathrm{out} \in \mu\_\textrm{out}$, insert a new edge going out of the new +4. For each $\sigma\_\mathrm{out} \in \mu\_\textrm{out}$, insert a new edge going out of the new copy of the `SrcNode` of $\sigma\_\mathrm{out}$ according to the specification $\sigma\_\mathrm{out}$. The target port must have an existing edge whose source is in $R$; this edge is removed. -4. For each $(n, t = T(n))$, append the copy of $n$ to the list - of children of $t$ (adding a hierachy edge from $t$ to $n$). 5. For each node $(n, b = B(n))$ and for each child $m$ of $b$, replace the hierarchy edge from $b$ to $m$ with a hierarchy edge from the new copy of $n$ to $m$ (preserving the order). From 3eb300f26028def0cb7b401ae053e79e88a134e1 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Tue, 10 Oct 2023 16:14:04 +0100 Subject: [PATCH 10/18] Ooops, comments are --- specification/hugr.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 8cb0be493..656841331 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1198,22 +1198,22 @@ The new hugr is then derived as follows: This is the general subgraph-replacement method. -# A _partial hugr_ is a graph formed by a subset of nodes of a valid hugr together + Given a set $S$ of nodes in a hugr, let $S^\*$ be the set of all nodes descended from nodes in $S$ (i.e. reachable from $S$ by following hierarchy edges), including $S$ itself. -# Call two nodes $a, b \in \Gamma$ _separated_ if $a \notin \\{b\\}^\*$ and -# $b \notin \\{a\\}^\*$ (i.e. there is no hierarchy relation between them). Note -# that this is much the same requirement as convexity, but following the hierarchy -# edges rather than dataflow edges. - + A `NewEdgeSpec` specifies an edge inserted between an existing node and a new node. It contains the following fields: From 8862f3c1d214e34353a5cabddc3a903dbde9047c Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Tue, 10 Oct 2023 16:30:43 +0100 Subject: [PATCH 11/18] mu_inp/out - use gamma \ R not \ S* --- specification/hugr.md | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 656841331..9ffdb4b4b 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1233,20 +1233,21 @@ The `Replace` method takes as input: - a set $S$ of IDs of nodes that are children of $P$ - a Hugr $H$ whose root is a node of the same type as $P$. Note this Hugr need not be valid, in that it may be missing: * edges to/from some ports (i.e. it may have unconnected ports)---not just Copyable dataflow outputs, which may occur even in valid Hugrs, but also incoming and/or non-Copyable dataflow ports, and ControlFlow ports, - * children for some container nodes (i.e. it may have container nodes with no outgoing hierarchy edges) + * all children for some container nodes strictly beneath the root (i.e. it may have container nodes with no outgoing hierarchy edges) * $\mathtt{Input}$ and/or $\mathtt{Output}$ children of $P$ (if $P$ is a dataflow container node) * A basic block exit node as a child of $P$ (if $P$ is a CFG node) - a map $B$ *from* container nodes in $H$ that have no children *to* container nodes in $S^\*$ none of which is an ancestor of another. Let $X$ be the set of children of nodes in the image of $B$, and $R = S^\* \setminus X^\*$. - a list $\mu\_\textrm{inp}$ of `NewEdgeSpec` which all have their `TgtNode`in - $G$ and `SrcNode` in $\Gamma \setminus S^*$; + $G$ and `SrcNode` in $\Gamma \setminus R$; - a list $\mu\_\textrm{out}$ of `NewEdgeSpec` which all have their `SrcNode`in - $G$ and `TgtNode` in $\Gamma \setminus S^*$ (and `TgtNode` has an existing + $G$ and `TgtNode` in $\Gamma \setminus R$ (and `TgtNode` has an existing incoming edge from a node in $R$). The new hugr is then derived as follows: -1. Make a copy in $\Gamma$ of all the nodes in $H$ *except the root*, and all edges where both source and target are copied. +1. Make a copy in $\Gamma$ of all the nodes in $H$ *except the root*, and all edges except + hierarchy edges from the root. 2. For each child of the root of $H$, make the corresponding copy in $\Gamma$ be a child of $P$. 3. For each $\sigma\_\mathrm{inp} \in \mu\_\textrm{inp}$, insert a new edge going into the new copy of the `TgtNode` of $\sigma\_\mathrm{inp}$ according to the specification $\sigma\_\mathrm{inp}$. From 78f8567edf9a6b20c300ae4b922b2c502a90e1aa Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Tue, 10 Oct 2023 16:31:29 +0100 Subject: [PATCH 12/18] New children replace existing children in hierarchy order --- specification/hugr.md | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 9ffdb4b4b..bf225847a 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1248,15 +1248,18 @@ The new hugr is then derived as follows: 1. Make a copy in $\Gamma$ of all the nodes in $H$ *except the root*, and all edges except hierarchy edges from the root. -2. For each child of the root of $H$, make the corresponding copy in $\Gamma$ be a child of $P$. -3. For each $\sigma\_\mathrm{inp} \in \mu\_\textrm{inp}$, insert a new edge going into the new +2. For each $\sigma\_\mathrm{inp} \in \mu\_\textrm{inp}$, insert a new edge going into the new copy of the `TgtNode` of $\sigma\_\mathrm{inp}$ according to the specification $\sigma\_\mathrm{inp}$. Where these edges are from ports that currently have edges to nodes in $R$, the existing edges are replaced. -4. For each $\sigma\_\mathrm{out} \in \mu\_\textrm{out}$, insert a new edge going out of the new +3. For each $\sigma\_\mathrm{out} \in \mu\_\textrm{out}$, insert a new edge going out of the new copy of the `SrcNode` of $\sigma\_\mathrm{out}$ according to the specification $\sigma\_\mathrm{out}$. The target port must have an existing edge whose source is in $R$; this edge is removed. +4. Let $N$ be the ordered list of the copies made in $\Gamma$ of the children of the root node of $H$. + For each child $C$ of $P$ (in order), if $C \in S$, redirect the hierarchy edge $P \rightarrow C$ to + target the next node in $N$. Stop if there are no more nodes in $N$. + Add any remaining nodes in $N$ to the end of $P$'s list of children. 5. For each node $(n, b = B(n))$ and for each child $m$ of $b$, replace the hierarchy edge from $b$ to $m$ with a hierarchy edge from the new copy of $n$ to $m$ (preserving the order). From 80b8e2725aa0edc384ac46ccee421e204835c5cb Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Tue, 10 Oct 2023 16:34:51 +0100 Subject: [PATCH 13/18] node type of P --- specification/hugr.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index bf225847a..c0f2ad6e4 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1229,13 +1229,14 @@ Note that in a `NewEdgeSpec` one of `SrcNode` and `TgtNode` is an existing node in the hugr and the other is a new node. The `Replace` method takes as input: - - the ID of a DFG node $P$ in $\Gamma$; + - the ID of a container node $P$ in $\Gamma$; - a set $S$ of IDs of nodes that are children of $P$ - a Hugr $H$ whose root is a node of the same type as $P$. Note this Hugr need not be valid, in that it may be missing: * edges to/from some ports (i.e. it may have unconnected ports)---not just Copyable dataflow outputs, which may occur even in valid Hugrs, but also incoming and/or non-Copyable dataflow ports, and ControlFlow ports, * all children for some container nodes strictly beneath the root (i.e. it may have container nodes with no outgoing hierarchy edges) - * $\mathtt{Input}$ and/or $\mathtt{Output}$ children of $P$ (if $P$ is a dataflow container node) - * A basic block exit node as a child of $P$ (if $P$ is a CFG node) + * some children of the root, for container nodes that require particular children (e.g. + $\mathtt{Input}$ and/or $\mathtt{Output}$ if $P$ is a dataflow container, the exit node + of a CFG, the required number of children of a conditional) - a map $B$ *from* container nodes in $H$ that have no children *to* container nodes in $S^\*$ none of which is an ancestor of another. Let $X$ be the set of children of nodes in the image of $B$, and $R = S^\* \setminus X^\*$. - a list $\mu\_\textrm{inp}$ of `NewEdgeSpec` which all have their `TgtNode`in From 18bdd0ed9cb2bce6399c478b300ca1406febf3b8 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Tue, 10 Oct 2023 16:42:27 +0100 Subject: [PATCH 14/18] Replacement Hugr is $G$ not $H$ --- specification/hugr.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index c0f2ad6e4..73cdddf28 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1231,13 +1231,13 @@ in the hugr and the other is a new node. The `Replace` method takes as input: - the ID of a container node $P$ in $\Gamma$; - a set $S$ of IDs of nodes that are children of $P$ - - a Hugr $H$ whose root is a node of the same type as $P$. Note this Hugr need not be valid, in that it may be missing: + - a Hugr $G$ whose root is a node of the same type as $P$. Note this Hugr need not be valid, in that it may be missing: * edges to/from some ports (i.e. it may have unconnected ports)---not just Copyable dataflow outputs, which may occur even in valid Hugrs, but also incoming and/or non-Copyable dataflow ports, and ControlFlow ports, * all children for some container nodes strictly beneath the root (i.e. it may have container nodes with no outgoing hierarchy edges) * some children of the root, for container nodes that require particular children (e.g. $\mathtt{Input}$ and/or $\mathtt{Output}$ if $P$ is a dataflow container, the exit node of a CFG, the required number of children of a conditional) - - a map $B$ *from* container nodes in $H$ that have no children *to* container nodes in $S^\*$ none of which is an ancestor of another. + - a map $B$ *from* container nodes in $G$ that have no children *to* container nodes in $S^\*$ none of which is an ancestor of another. Let $X$ be the set of children of nodes in the image of $B$, and $R = S^\* \setminus X^\*$. - a list $\mu\_\textrm{inp}$ of `NewEdgeSpec` which all have their `TgtNode`in $G$ and `SrcNode` in $\Gamma \setminus R$; @@ -1247,7 +1247,7 @@ The `Replace` method takes as input: The new hugr is then derived as follows: -1. Make a copy in $\Gamma$ of all the nodes in $H$ *except the root*, and all edges except +1. Make a copy in $\Gamma$ of all the nodes in $G$ *except the root*, and all edges except hierarchy edges from the root. 2. For each $\sigma\_\mathrm{inp} \in \mu\_\textrm{inp}$, insert a new edge going into the new copy of the `TgtNode` of $\sigma\_\mathrm{inp}$ according to the specification $\sigma\_\mathrm{inp}$. @@ -1257,7 +1257,7 @@ The new hugr is then derived as follows: copy of the `SrcNode` of $\sigma\_\mathrm{out}$ according to the specification $\sigma\_\mathrm{out}$. The target port must have an existing edge whose source is in $R$; this edge is removed. -4. Let $N$ be the ordered list of the copies made in $\Gamma$ of the children of the root node of $H$. +4. Let $N$ be the ordered list of the copies made in $\Gamma$ of the children of the root node of $G$. For each child $C$ of $P$ (in order), if $C \in S$, redirect the hierarchy edge $P \rightarrow C$ to target the next node in $N$. Stop if there are no more nodes in $N$. Add any remaining nodes in $N$ to the end of $P$'s list of children. From 67fae3419dcb1b3c8ddb3b6a105235dd3e83a207 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Wed, 11 Oct 2023 09:17:51 +0100 Subject: [PATCH 15/18] Reindent --- specification/hugr.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 73cdddf28..5e3cf14d9 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1231,13 +1231,15 @@ in the hugr and the other is a new node. The `Replace` method takes as input: - the ID of a container node $P$ in $\Gamma$; - a set $S$ of IDs of nodes that are children of $P$ - - a Hugr $G$ whose root is a node of the same type as $P$. Note this Hugr need not be valid, in that it may be missing: + - a Hugr $G$ whose root is a node of the same type as $P$. + Note this Hugr need not be valid, in that it may be missing: * edges to/from some ports (i.e. it may have unconnected ports)---not just Copyable dataflow outputs, which may occur even in valid Hugrs, but also incoming and/or non-Copyable dataflow ports, and ControlFlow ports, * all children for some container nodes strictly beneath the root (i.e. it may have container nodes with no outgoing hierarchy edges) * some children of the root, for container nodes that require particular children (e.g. $\mathtt{Input}$ and/or $\mathtt{Output}$ if $P$ is a dataflow container, the exit node of a CFG, the required number of children of a conditional) - - a map $B$ *from* container nodes in $G$ that have no children *to* container nodes in $S^\*$ none of which is an ancestor of another. + - a map $B$ *from* container nodes in $G$ that have no children *to* container nodes in $S^\*$ + none of which is an ancestor of another. Let $X$ be the set of children of nodes in the image of $B$, and $R = S^\* \setminus X^\*$. - a list $\mu\_\textrm{inp}$ of `NewEdgeSpec` which all have their `TgtNode`in $G$ and `SrcNode` in $\Gamma \setminus R$; From 2a4cf295a54b41182de5086c9a7f41edb010593e Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Wed, 11 Oct 2023 09:18:09 +0100 Subject: [PATCH 16/18] Clarify new edges and restrictions on Order/ControlFlow --- specification/hugr.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 5e3cf14d9..06bba28d7 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1244,8 +1244,10 @@ The `Replace` method takes as input: - a list $\mu\_\textrm{inp}$ of `NewEdgeSpec` which all have their `TgtNode`in $G$ and `SrcNode` in $\Gamma \setminus R$; - a list $\mu\_\textrm{out}$ of `NewEdgeSpec` which all have their `SrcNode`in - $G$ and `TgtNode` in $\Gamma \setminus R$ (and `TgtNode` has an existing - incoming edge from a node in $R$). + $G$ and `TgtNode` in $\Gamma \setminus R$ (where `TgtNode` and `TgtPos` describe + an existing incoming edge of that kind from a node in $R$). + +Note that the well-formedness requirements of Hugr imply that $\mu\_\textrm{inp}$ and $\mu\_\textrm{out}$ only contain Order edges if $P$ is a dataflow container, and only contain ControlFlow edges if $P$ is a CFG-node; and that any such Order or ControlFlow edges will (more precisely) be between nodes $S$ and children of the root of $G$. The new hugr is then derived as follows: From 9a54300549a71a782e5ea98401dd19e027160d00 Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Wed, 11 Oct 2023 13:14:20 +0100 Subject: [PATCH 17/18] Clarify well-formedness requirements of type of $ on allowable EdgeKinds --- specification/hugr.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/specification/hugr.md b/specification/hugr.md index 06bba28d7..4e0619268 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1247,7 +1247,11 @@ The `Replace` method takes as input: $G$ and `TgtNode` in $\Gamma \setminus R$ (where `TgtNode` and `TgtPos` describe an existing incoming edge of that kind from a node in $R$). -Note that the well-formedness requirements of Hugr imply that $\mu\_\textrm{inp}$ and $\mu\_\textrm{out}$ only contain Order edges if $P$ is a dataflow container, and only contain ControlFlow edges if $P$ is a CFG-node; and that any such Order or ControlFlow edges will (more precisely) be between nodes $S$ and children of the root of $G$. +The well-formedness requirements of Hugr imply that $\mu\_\textrm{inp}$ and $\mu\_\textrm{out}$ may only contain `NewEdgeSpec`s with certain `EdgeKind`s, depending on $P$: + - if $P$ is a dataflow container, `EdgeKind`s may be `Order`, `Value` or `Static` only (no `ControlFlow`) + - if $P$ is a CFG node, `EdgeKind`s may be `ControlFlow`, `Value`, or `Static` only (no `Order`) + - if $P$ is a Module node, there may be `Value` or `Static` only (no `Order`). +(in the case of $P$ being a CFG or Module node, any `Value` edges will be nonlocal, like Static edges.) The new hugr is then derived as follows: From cf9b729be74b177e497ef3f2c19df1c6746778db Mon Sep 17 00:00:00 2001 From: Alan Lawrence Date: Wed, 11 Oct 2023 15:03:56 +0100 Subject: [PATCH 18/18] remove comments --- specification/hugr.md | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/specification/hugr.md b/specification/hugr.md index 4e0619268..4d7d4ef7f 100644 --- a/specification/hugr.md +++ b/specification/hugr.md @@ -1198,22 +1198,10 @@ The new hugr is then derived as follows: This is the general subgraph-replacement method. - Given a set $S$ of nodes in a hugr, let $S^\*$ be the set of all nodes descended from nodes in $S$ (i.e. reachable from $S$ by following hierarchy edges), including $S$ itself. - A `NewEdgeSpec` specifies an edge inserted between an existing node and a new node. It contains the following fields: