Update definition of Replace (and clarify SimpleReplace)

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).