{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE MultiParamTypeClasses #-}

-- | This module provides functions for defining general-purpose
-- transformations on low-level circuits. The uses of this include:
-- 
-- * gate transformations, where a whole circuit is transformed by
-- replacing each kind of gate with another gate or circuit;
-- 
-- * error correcting codes, where a whole circuit is transformed
-- replacing each qubit by some fixed number of qubits, and each gate
-- by a circuit; and
-- 
-- * simulations, where a whole circuit is mapped to a semantic
-- function by specifying a semantic function for each gate.
-- 
-- The interface is designed to allow the programmer to specify new
-- transformers easily. To define a specific transformation, the
-- programmer has to specify only four pieces of information:
-- 
-- * A type /a/=⟦Qubit⟧, to serve as a semantic domain for qubits.
-- 
-- * A type /b/=⟦Bit⟧, to serve as a semantic domain for bits.
-- 
-- * A monad /m/. This is to allow translations to have side effects
-- if desired; one can use the identity monad otherwise.
-- 
-- * For every gate /G/, a corresponding semantic function ⟦/G/⟧.  The
-- type of this function depends on what kind of gate /G/ is. For example:
-- 
-- @
-- If /G/ :: Qubit -> Circ Qubit, then ⟦/G/⟧ :: /a/ -> /m/ /a/. 
-- If /G/ :: (Qubit, Bit) -> Circ (Bit, Bit), then ⟦/G/⟧ :: (/a/, /b/) -> /m/ (/b/, /b/).
-- @ 
-- 
-- The programmer provides this information by defining a function of
-- type 'Transformer' /m/ /a/ /b/. See <#Transformers> below.  Once a
-- particular transformer has been defined, it can then be applied to
-- entire circuits. For example, for a circuit with 1 inputs and 2
-- outputs:
-- 
-- @
-- If /C/ :: Qubit -> (Bit, Qubit), then ⟦/C/⟧ :: /a/ -> /m/ (/b/, /a/).
-- @

-- ----------------------------------------------------------------------
-- Grammar note for developers: a "transformer" does a
-- "transformation" by "transforming" gates. We use "transform" as a
-- verb, "transformation" to describe the process of transforming, and
-- "transformer" for the code that describes or does the transformation. 
-- 
-- I had initially used the words "iteration", "translation",
-- "transform", "transformation", "interpretation", and "semantics"
-- interchangeably, which was a huge linguistic mess.

module Quipper.Internal.Transformer where

-- import other Quipper stuff
import Quipper.Internal.Circuit
import Quipper.Utils.Auxiliary

-- import other stuff
import Control.Monad
import Control.Monad.State
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap
import Data.Typeable

-- ======================================================================
-- * An example transformer
-- 
-- $EXAMPLE
-- 
-- The following is a short but complete example of how to write and
-- use a simple transformer. As usual, we start by importing Quipper:
-- 
-- > import Quipper
-- 
-- We will write a transformer called @sample_transformer@, which maps
-- every swap gate to a sequence of three controlled-not gates, and
-- leaves all other gates unchanged. For convenience, Quipper
-- pre-defines an 'Quipper.identity_transformer', which can be used as
-- a catch-all clause to take care of all the gates that don't need to
-- be rewritten.
-- 
-- > mytransformer :: Transformer Circ Qubit Bit
-- > mytransformer (T_QGate "swap" 2 0 _ ncf f) = f $
-- >   \[q0, q1] [] ctrls -> do
-- >     without_controls_if ncf $ do
-- >       with_controls ctrls $ do
-- >         qnot_at q0 `controlled` q1
-- >         qnot_at q1 `controlled` q0
-- >         qnot_at q0 `controlled` q1
-- >         return ([q0, q1], [], ctrls)
-- > mytransformer g = identity_transformer g
-- 
-- Note how Quipper syntax has been used to define the replacement
-- circuit, consisting of three controlled-not gates. Also, since the
-- original swap gate may have been controlled, we have added the
-- additional controls with a 'Quipper.with_controls' operator.
-- 
-- To try this out, we define some random circuit using swap gates:
-- 
-- > mycirc a b c d = do
-- >   swap_at a b
-- >   hadamard_at b
-- >   swap_at b c `controlled` [a, d]
-- >   hadamard_at c
-- >   swap_at c d
-- 
-- To apply the transformer to this circuit, we use the generic
-- operator 'Quipper.transform_generic':
-- 
-- > mycirc2 = transform_generic mytransformer mycirc
-- 
-- Finally, we use a @main@ function to display the original circuit
-- and then the transformed one:
-- 
-- > main = do
-- >   print_simple Preview mycirc
-- >   print_simple Preview mycirc2

-- ======================================================================
-- * Bindings

-- $bindings
-- 
-- We introduce the notion of a /binding/ as a low-level way to
-- describe functions of varying arities. A binding assigns a value to
-- a wire in a circuit (much like a \"valuation\" in logic or semantics
-- assigns values to variables). 
-- 
-- To iterate through a circuit, one will typically specify initial
-- bindings for the input wires. This encodes the input of the function
-- ⟦/C/⟧ mentioned in the introduction. The bindings are updated as
-- one passes through each gate. When the iteration is finished, the
-- final bindings assign a value to each output wire of the
-- circuit. This encodes the output of the function ⟦/C/⟧. Therefore,
-- the interpretation of a circuit is representable as a function from
-- bindings (of input wires) to bindings (of output wires), i.e., it
-- has the type ⟦/C/⟧ :: 'Bindings' /a/ /b/ -> 'Bindings' /a/ /b/.

-- | An /endpoint/ is either a /qubit/ or a /bit/. In a transformer,
-- we have ⟦B_Endpoint Qubit Bit⟧ = ⟦Qubit⟧ + ⟦Bit⟧. The type 'B_Endpoint'
-- /a/ /b/ is the same as 'Either' /a/ /b/, but we use more suggestive
-- field names.
data B_Endpoint a b =
  Endpoint_Qubit a
  | Endpoint_Bit b
    deriving (Eq, Ord, Typeable, Show)

-- | A binding is a map from a set of wires to the disjoint union of
-- /a/ and /b/.
type Bindings a b = Map Wire (B_Endpoint a b)

-- | Return the list of bound wires from a binding.
wires_of_bindings :: Bindings a b -> [Wire]
wires_of_bindings = Map.keys

-- | The empty binding.
bindings_empty :: Bindings a b
bindings_empty = Map.empty

-- | Bind a wire to a value, and add it to the given bindings.
bind :: Wire -> B_Endpoint a b -> Bindings a b -> Bindings a b
bind r x bindings = Map.insert r x bindings

-- | Bind a qubit wire to a value, and add it to the given bindings.
bind_qubit_wire :: Wire -> a -> Bindings a b -> Bindings a b
bind_qubit_wire r x bindings = bind r (Endpoint_Qubit x) bindings

-- | Bind a bit wire to a value, and add it to the given bindings.
bind_bit_wire :: Wire -> b -> Bindings a b -> Bindings a b
bind_bit_wire r x bindings = bind r (Endpoint_Bit x) bindings

-- | Retrieve the value of a wire from the given bindings. 
unbind :: Bindings a b -> Wire -> B_Endpoint a b
unbind bindings w = case Map.lookup w bindings of
       Nothing -> error ("unbind: wire (" ++ show w ++ ") not in bindings: " ++ show (wires_of_bindings bindings))
       Just a -> a

-- | Retrieve the value of a qubit wire from the given bindings.
-- Throws an error if the wire was bound to a classical bit.
unbind_qubit_wire :: Bindings a b -> Wire -> a
unbind_qubit_wire bindings w = 
  case unbind bindings w of
    Endpoint_Qubit x -> x
    Endpoint_Bit x -> error "Transformer error: expected a qubit, got a bit"

-- | Retrieve the value of a bit wire from the given bindings.
-- Throws an error if the wire was bound to a qubit.
unbind_bit_wire :: Bindings a b -> Wire -> b
unbind_bit_wire bindings w = 
  case unbind bindings w of
    Endpoint_Bit x -> x
    Endpoint_Qubit x -> error "Transformer error: expected a bit, got a qubit"

-- | Delete a wire from the given bindings.
bind_delete :: Wire -> Bindings a b -> Bindings a b
bind_delete r bindings = Map.delete r bindings

-- | Like 'bind', except bind a list of wires to a list of values. The
-- lists must be of the same length.
bind_list :: [Wire] -> [B_Endpoint a b] -> Bindings a b -> Bindings a b
bind_list ws xs bindings =
  foldr (\ (w, x) -> bind w x) bindings (zip ws xs)
    
-- | Like 'bind_qubit_wire', except bind a list of qubit wires to a list of
-- values. The lists must be of the same length.
bind_qubit_wire_list :: [Wire] -> [a] -> Bindings a b -> Bindings a b
bind_qubit_wire_list ws xs bindings =
  foldr (\ (w, x) -> bind_qubit_wire w x) bindings (zip ws xs)
    
-- | Like 'bind_bit_wire', except bind a list of bit wires to a list of
-- values. The lists must be of the same length.
bind_bit_wire_list :: [Wire] -> [b] -> Bindings a b -> Bindings a b
bind_bit_wire_list ws xs bindings =
  foldr (\ (w, x) -> bind_bit_wire w x) bindings (zip ws xs)
    
-- | Like 'unbind', except retrieve a list of values.
unbind_list :: Bindings a b -> [Wire] -> [B_Endpoint a b]
unbind_list bindings ws =
  map (unbind bindings) ws

-- | Like 'unbind_qubit_wire', except retrieve a list of values.
unbind_qubit_wire_list :: Bindings a b -> [Wire] -> [a]
unbind_qubit_wire_list bindings ws =
  map (unbind_qubit_wire bindings) ws
    
-- | Like 'unbind_bit_wire', except retrieve a list of values.
unbind_bit_wire_list :: Bindings a b -> [Wire] -> [b]
unbind_bit_wire_list bindings ws =
  map (unbind_bit_wire bindings) ws
    
-- | A list of signed values of type ⟦B_Endpoint⟧. This type is an
-- abbreviation defined for convenience.
type Ctrls a b = [Signed (B_Endpoint a b)]

-- | Given a list of signed wires (controls), and a list of signed
-- values, make a bindings from the wires to the values. Ignore the signs.
bind_controls :: Controls -> Ctrls a b -> Bindings a b -> Bindings a b
bind_controls controls xs bindings =
  bind_list (map from_signed controls) (map from_signed xs) bindings

-- | Like 'unbind', but retrieve binding for all wires in a list of
-- controls.
unbind_controls :: Bindings a b -> Controls -> Ctrls a b
unbind_controls bindings c =
  [Signed (unbind bindings w) b | Signed w b <- c ]

-- $transformers_anchor #Transformers#

-- ----------------------------------------------------------------------
-- * Transformers

-- $transformers
-- 
-- The types 'T_Gate' and 'Transformer' are at the heart of the
-- circuit transformer functionality. Their purpose is to give a
-- concise syntax in which to express semantic functions for gates. As
-- mentioned in the introduction, the programmer needs to specify two
-- type /a/ and /b/, a monad /m/, and a semantic function for each
-- gate.  With the T_Gate' and 'Transformer' types, the definition
-- takes the following form:
-- 
-- > my_transformer :: Transformer m a b
-- > my_transformer (T_Gate1 <parameters> f) = f $ <semantic function for gate 1>
-- > my_transformer (T_Gate2 <parameters> f) = f $ <semantic function for gate 2>
-- > my_transformer (T_Gate3 <parameters> f) = f $ <semantic function for gate 3>
-- > ...
-- 
-- The type 'T_Gate' is very higher-order, involving a function /f/
-- that consumes the semantic function for each gate. The reason for
-- this higher-orderness is that the semantic functions for different
-- gates may have different types. 
-- 
-- This higher-orderness makes the 'T_Gate' mechanism hard to read,
-- but easy to use. Effectively we only have to write lengthy and
-- messy code once and for all, rather than once for each transformer.
-- In particular, all the required low-level bindings and unbindings
-- can be handled by general-purpose code, and do not need to clutter
-- each transformer. 

-- | The type 'T_Gate' is used to define case distinctions over gates
-- in the definition of transformers. For each kind of gate /X/, it
-- contains a constructor of the form @(T_X f)@. Here, /X/ identifies
-- the gate, and /f/ is a higher-order function to pass the
-- translation of /X/ to.

-- Implementation note: in the future, perhaps we can also add two
-- variants of this type: one that is specialized to the "simple"
-- case, where the semantics functions are assumed not to modify the
-- controls; another that is specialized to m = Id. This would make
-- the definition of most circuit transformers look less cluttered. 

data T_Gate m a b x =
  T_QGate      String Int Int InverseFlag NoControlFlag (([a] -> [a] -> Ctrls a b -> m ([a], [a], Ctrls a b)) -> x)
  | T_QRot       String Int Int InverseFlag Timestep NoControlFlag (([a] -> [a] -> Ctrls a b -> m ([a], [a], Ctrls a b)) -> x)
  | T_GPhase     Double NoControlFlag (([B_Endpoint a b] -> Ctrls a b -> m (Ctrls a b)) -> x)
  | T_CNot       NoControlFlag ((b -> Ctrls a b -> m (b, Ctrls a b)) -> x)
  | T_CGate      String NoControlFlag (([b] -> m (b, [b])) -> x)
  | T_CGateInv   String NoControlFlag ((b -> [b] -> m [b]) -> x)
  | T_CSwap      NoControlFlag ((b -> b -> Ctrls a b -> m (b, b, Ctrls a b)) -> x)
  | T_QPrep      NoControlFlag ((b -> m a) -> x)
  | T_QUnprep    NoControlFlag ((a -> m b) -> x)
  | T_QInit      Bool NoControlFlag (m a -> x)
  | T_CInit      Bool NoControlFlag (m b -> x)
  | T_QTerm      Bool NoControlFlag ((a -> m ()) -> x)
  | T_CTerm      Bool NoControlFlag ((b -> m ()) -> x)
  | T_QMeas      ((a -> m b) -> x)
  | T_QDiscard   ((a -> m ()) -> x)
  | T_CDiscard   ((b -> m ()) -> x)
  | T_DTerm      Bool ((b -> m ()) -> x)
  | T_Subroutine BoxId InverseFlag NoControlFlag ControllableFlag [Wire] Arity [Wire] Arity RepeatFlag ((Namespace -> [B_Endpoint a b] -> Ctrls a b -> m ([B_Endpoint a b], Ctrls a b)) -> x)
  | T_Comment String InverseFlag (([(B_Endpoint a b, String)] -> m ()) -> x)

-- Make 'T_Gate' an instance of 'Show', to enable transformers to
-- produce better error messages about unimplemented gates etc.
instance Show (T_Gate m a b x) where
  show (T_QGate name n m inv ncf f) = "QGate[" ++ name ++ "," ++ show n ++ "," ++ show m ++ "]" ++ optional inv "*"
  show (T_QRot name n m inv t ncf f) = "QRot[" ++ name ++ "," ++ show t ++ "," ++ show n ++ "," ++ show m ++ "]" ++ optional inv "*"
  show (T_GPhase t ncf f) = "GPhase[" ++ show t ++ "]"
  show (T_CNot ncf f) = "CNot"
  show (T_CGate n ncf f) = "CGate[" ++ n ++ "]"
  show (T_CGateInv n ncf f) = "CGate[" ++ n ++ "]*"
  show (T_CSwap ncf f) = "CSwap"
  show (T_QPrep ncf f) = "QPrep"
  show (T_QUnprep ncf f) = "QUnprep"
  show (T_QInit b ncf f) = "QInit" ++ if b then "1" else "0"
  show (T_CInit b ncf f) = "CInit" ++ if b then "1" else "0"
  show (T_QTerm b ncf f) = "QTerm" ++ if b then "1" else "0"
  show (T_CTerm b ncf f) = "CTerm" ++ if b then "1" else "0"
  show (T_QMeas f) = "QMeas"
  show (T_QDiscard f) = "QDiscard"
  show (T_CDiscard f) = "CDiscard"
  show (T_DTerm b f) = "DTerm" ++ if b then "1" else "0"
  show (T_Subroutine n inv ncf scf ws a1 vs a2 rep f) = "Subroutine(x" ++ (show rep) ++ ")[" ++ show n ++ "]" ++ optional inv "*"
  show (T_Comment n inv f) = "Comment[" ++ n ++ "]" ++ optional inv "*"

-- | A circuit transformer is specified by defining a function of type
-- 'Transformer' /m/ /a/ /b/. This involves specifying a monad /m/,
-- semantic domains /a/=⟦Qubit⟧ and /b/=⟦Bit⟧, and a semantic function
-- for each gate, like this:
-- 
-- > my_transformer :: Transformer m a b
-- > my_transformer (T_Gate1 <parameters> f) = f $ <semantic function for gate 1>
-- > my_transformer (T_Gate2 <parameters> f) = f $ <semantic function for gate 2>
-- > my_transformer (T_Gate3 <parameters> f) = f $ <semantic function for gate 3>
-- > ...

-- Implementation note: the use of \"forall\" in this type is to allow
-- some freedom in the return type of the continuation 'f' in the
-- definition of 'T_Gate'. This makes it easier, for example, to
-- compose transformers with other transformers. The use of \"forall\"
-- implies that any module that uses the 'Transformer' type may have
-- to declare the @Rank2Types@ language extension. This was not
-- required in GHC 7.4, but seems to be required in GHC 7.6.
type Transformer m a b = forall x . T_Gate m a b x -> x

-- | A \"binding transformer\" is a function from bindings to
-- bindings. The semantics of any gate or circuit is ultimately a
-- binding transformer, for some types /a/, /b/ and some monad /m/. We
-- introduce an abbreviation for this type primarily as a convenience
-- for the definition of 'bind_gate', but also because this type can
-- be completely hidden from user code.
type BT m a b = Bindings a b -> m (Bindings a b)

-- | Turn a 'Gate' into a 'T_Gate'. This is the function that actually
-- handles the explicit bindings/unbindings required for the inputs
-- and outputs of each gate. Effectively it gives a way, for each
-- gate, of turning a semantic function into a binding transformer.
-- Additionally, this function is passed a Namespace, so that the
-- semantic function for T_Subroutine can use it.
bind_gate :: Monad m => Namespace -> Gate -> T_Gate m a b (BT m a b)
bind_gate namespace gate = case gate of
  QGate name inv ws vs c ncf -> T_QGate name n m inv ncf (list_binary ws vs c)
    where
      n = length ws
      m = length vs
  QRot name inv t ws vs c ncf -> T_QRot name n m inv t ncf (list_binary ws vs c)
    where
      n = length ws
      m = length vs
  GPhase t w c ncf         -> T_GPhase t ncf (phase_ary w c)
  CNot w c ncf             -> T_CNot ncf (cunary w c)  
  CGate n w vs ncf         -> T_CGate n ncf (cgate_ary w vs)
  CGateInv n w vs ncf      -> T_CGateInv n ncf (cgateinv_ary w vs)
  CSwap w v c ncf          -> T_CSwap ncf (binary_c w v c)
  QPrep w ncf              -> T_QPrep ncf (qprep_ary w)
  QUnprep w ncf            -> T_QUnprep ncf (qunprep_ary w)
  QInit b w ncf            -> T_QInit b ncf (qinit_ary w)
  CInit b w ncf            -> T_CInit b ncf (cinit_ary w)
  QTerm b w ncf            -> T_QTerm b ncf (qterm_ary w)
  CTerm b w ncf            -> T_CTerm b ncf (cterm_ary w)
  QMeas w                  -> T_QMeas (qunprep_ary w)
  QDiscard w               -> T_QDiscard (qterm_ary w)
  CDiscard w               -> T_CDiscard (cterm_ary w)
  DTerm b w                -> T_DTerm b (cterm_ary w)
  Subroutine n inv ws a1 vs a2 c ncf scf rep
    -> T_Subroutine n inv ncf scf ws a1 vs a2 rep
         (\f -> subroutine_ary ws vs c (f namespace))
  Comment s inv ws         -> T_Comment s inv (comment_ary ws)
  where
    unary :: Monad m => Wire -> Controls -> (a -> Ctrls a b -> m (a, Ctrls a b)) -> BT m a b
    unary w c f bindings = do
      let w' = unbind_qubit_wire bindings w
      let c' = unbind_controls bindings c
      (w'', c'') <- f w' c'
      let bindings1 = bind_qubit_wire w w'' bindings
      let bindings2 = bind_controls c c'' bindings1
      return bindings2
    
    binary :: Monad m => Wire -> Wire -> Controls -> (a -> a -> Ctrls a b -> m (a, a, Ctrls a b)) -> BT m a b
    binary w v c f bindings = do
      let w' = unbind_qubit_wire bindings w
      let v' = unbind_qubit_wire bindings v
      let c' = unbind_controls bindings c
      (w'', v'', c'') <- f w' v' c'
      let bindings1 = bind_qubit_wire w w'' bindings
      let bindings2 = bind_qubit_wire v v'' bindings1
      let bindings3 = bind_controls c c'' bindings2
      return bindings3
    
    binary_c :: Monad m => Wire -> Wire -> Controls -> (b -> b -> Ctrls a b -> m (b, b, Ctrls a b)) -> BT m a b
    binary_c w v c f bindings = do
      let w' = unbind_bit_wire bindings w
      let v' = unbind_bit_wire bindings v
      let c' = unbind_controls bindings c
      (w'', v'', c'') <- f w' v' c'
      let bindings1 = bind_bit_wire w w'' bindings
      let bindings2 = bind_bit_wire v v'' bindings1
      let bindings3 = bind_controls c c'' bindings2
      return bindings3
    
    list_unary :: Monad m => [Wire] -> Controls -> ([a] -> Ctrls a b -> m ([a], Ctrls a b)) -> BT m a b
    list_unary ws c f bindings = do
      let ws' = unbind_qubit_wire_list bindings ws
      let c' = unbind_controls bindings c
      (ws'', c'') <- f ws' c'
      let bindings1 = bind_qubit_wire_list ws ws'' bindings
      let bindings2 = bind_controls c c'' bindings1
      return bindings2

    list_binary :: Monad m => [Wire] -> [Wire] -> Controls -> ([a] -> [a] -> Ctrls a b -> m ([a], [a], Ctrls a b)) -> BT m a b
    list_binary ws vs c f bindings = do
      let ws' = unbind_qubit_wire_list bindings ws
      let vs' = unbind_qubit_wire_list bindings vs
      let c' = unbind_controls bindings c
      (ws'', vs'', c'') <- f ws' vs' c'
      let bindings1 = bind_qubit_wire_list ws ws'' bindings
      let bindings2 = bind_qubit_wire_list vs vs'' bindings1
      let bindings3 = bind_controls c c'' bindings2
      return bindings3

    qprep_ary :: Monad m => Wire -> (b -> m a) -> BT m a b
    qprep_ary w f bindings = do
      let w' = unbind_bit_wire bindings w
      w'' <- f w'
      let bindings1 = bind_qubit_wire w w'' bindings
      return bindings1
    
    qunprep_ary :: Monad m => Wire -> (a -> m b) -> BT m a b
    qunprep_ary w f bindings = do
      let w' = unbind_qubit_wire bindings w
      w'' <- f w'
      let bindings1 = bind_bit_wire w w'' bindings
      return bindings1
    
    cunary :: Monad m => Wire -> Controls -> (b -> Ctrls a b -> m (b, Ctrls a b)) -> BT m a b
    cunary w c f bindings = do
      let w' = unbind_bit_wire bindings w
      let c' = unbind_controls bindings c
      (w'', c'') <- f w' c'
      let bindings1 = bind_bit_wire w w'' bindings
      let bindings2 = bind_controls c c'' bindings1
      return bindings2
    
    qinit_ary :: Monad m => Wire -> m a -> BT m a b
    qinit_ary w f bindings = do
      w'' <- f
      let bindings1 = bind_qubit_wire w w'' bindings
      return bindings1
    
    cinit_ary :: Monad m => Wire -> m b -> BT m a b
    cinit_ary w f bindings = do
      w'' <- f
      let bindings1 = bind_bit_wire w w'' bindings
      return bindings1
    
    qterm_ary :: Monad m => Wire -> (a -> m ()) -> BT m a b
    qterm_ary w f bindings = do
      let w' = unbind_qubit_wire bindings w
      () <- f w'
      let bindings1 = bind_delete w bindings
      return bindings1
    
    cterm_ary :: Monad m => Wire -> (b -> m ()) -> BT m a b
    cterm_ary w f bindings = do
      let w' = unbind_bit_wire bindings w
      () <- f w'
      let bindings1 = bind_delete w bindings
      return bindings1
    
    cgate_ary :: Monad m => Wire -> [Wire] -> ([b] -> m (b, [b])) -> BT m a b
    cgate_ary w vs f bindings = do
      let vs' = unbind_bit_wire_list bindings vs
      (w'', vs'') <- f vs'
      let bindings1 = bind_bit_wire w w'' bindings
      let bindings2 = bind_bit_wire_list vs vs'' bindings1 
      return bindings2

    cgateinv_ary :: Monad m => Wire -> [Wire] -> (b -> [b] -> m [b]) -> BT m a b
    cgateinv_ary w vs f bindings = do
      let vs' = unbind_bit_wire_list bindings vs
      let w' = unbind_bit_wire bindings w
      vs'' <- f w' vs'
      let bindings1 = bind_bit_wire_list vs vs'' bindings
      return bindings1

    subroutine_ary :: Monad m => [Wire] -> [Wire] -> Controls
                   -> ([B_Endpoint a b] -> Ctrls a b -> m ([B_Endpoint a b], Ctrls a b))
                   -> BT m a b
    subroutine_ary ws vs c f bindings = do
      let c' = unbind_controls bindings c
      let ws' = unbind_list bindings ws
      (vs'',c'') <- f ws' c'
      let bindings1 = bind_list vs vs'' bindings 
      let bindings2 = bind_controls c c'' bindings1
      return bindings2
      
    phase_ary :: Monad m => [Wire] -> Controls -> ([B_Endpoint a b] -> Ctrls a b -> m (Ctrls a b)) -> BT m a b
    phase_ary w c f bindings = do
      let w' = map (unbind bindings) w
      let c' = unbind_controls bindings c
      c'' <- f w' c'
      let bindings1 = bind_controls c c'' bindings
      return bindings1

    comment_ary :: Monad m => [(Wire, String)] -> (([(B_Endpoint a b, String)] -> m ()) -> BT m a b)
    comment_ary ws f bindings = do
      let ws' = zip (unbind_list bindings $ map fst ws) (map snd ws)
      f ws'
      return bindings

-- ----------------------------------------------------------------------
-- * Applying transformers to circuits

-- | Apply a 'Transformer' ⟦-⟧ to a 'Circuit' /C/, and output the
-- semantic function ⟦/C/⟧ :: bindings -> bindings.
transform_circuit :: Monad m => Transformer m a b -> Circuit -> Bindings a b -> m (Bindings a b)
transform_circuit transformer c bindings =
  foldM apply bindings gs
  where
    (_,gs,_,_) = c
    apply bindings g = transformer (bind_gate namespace_empty g) bindings

-- | Like 'transform_circuit', but for boxed circuits.
--
-- The handling of subroutines will depend on the transformer. 
-- For \"gate transformation\" types of applications, one typically
-- would like to leave the boxed structure intact.
-- For \"simulation\" types of applications, one would generally
-- recurse through the boxed structure.
--
-- The difference is specified in the definition of the transformer
-- within the semantic function of the Subroutine gate, whether to
-- create another boxed gate or open the box.
transform_bcircuit_rec :: Monad m => Transformer m a b -> BCircuit -> Bindings a b -> m (Bindings a b)
transform_bcircuit_rec transformer (c,namespace) bindings = 
  foldM apply bindings gs
  where
    (_,gs,_,_) = c
    apply bindings g = transformer (bind_gate namespace g) bindings

-- | Same as 'transform_bcircuit_rec', but specialized to when /m/ is
-- the identity operation.
transform_bcircuit_id :: Transformer Id a b -> BCircuit -> Bindings a b -> Bindings a b
transform_bcircuit_id t c b = getId (transform_bcircuit_rec t c b)

-- | To transform Dynamic Boxed circuits, we require a Transformer to define the
-- behavior on static gates, but we also require functions for what to do when
-- a subroutine is defined, and for when a dynamic_lift operation occurs. This is
-- all wrapped in the DynamicTransformer data type.
data DynamicTransformer m a b = DT {
     transformer :: Transformer m a b,
     define_subroutine :: BoxId -> TypedSubroutine -> m (),     
     lifting_function :: b -> m Bool
  }     

-- | Like 'transform_bcircuit_rec', but for dynamic-boxed circuits.
--
-- \"Write\" operations can be thought of as gates, and so they are passed to 
-- the given transformer. The handling of \"Read\" operations is taken care of 
-- by the \"lifting_function\" of the DynamicTransformer. \"Subroutine\" operations 
-- call the 'define_subroutine' function of the DynamicTransformer.
transform_dbcircuit :: Monad m => DynamicTransformer m a b -> DBCircuit x -> Bindings a b -> m (x,Bindings a b)
transform_dbcircuit dt (a0,rw) bindings = evalStateT (inner_transform dt (a0,rw) bindings) namespace_empty where
  inner_transform :: Monad m => DynamicTransformer m a b -> DBCircuit x -> Bindings a b -> (StateT Namespace m) (x,Bindings a b)
  inner_transform dt (a0,rw) bindings = 
    case rw of
      (RW_Return (_,_,x)) -> return (x,bindings)
      (RW_Write gate rw') -> do
        namespace <- get
        bindings' <- lift $ (transformer dt) (bind_gate namespace gate) bindings
        inner_transform dt (a0,rw')  bindings'
      (RW_Read wire rw_cont) -> do
        let bit = unbind_bit_wire bindings wire
        bool <- lift $ (lifting_function dt) bit
        let rw' = rw_cont bool
        inner_transform dt (a0,rw') bindings
      (RW_Subroutine name subroutine rw') -> do
        lift $ (define_subroutine dt) name subroutine
        namespace <- get
        let namespace' = map_provide name subroutine namespace
        put namespace'
        inner_transform dt (a0,rw') bindings