{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LINE 1 "Quipper/Algorithms/BF/BooleanFormula.hs" #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DeriveDataTypeable #-}

-- | This module contains the implementation of the various quantum circuits
-- that make up the boolean formula algorithm. Please see "Quipper.Algorithms.BF.Main"
-- for an overview of the boolean formula algorithm.

module Quipper.Algorithms.BF.BooleanFormula where

import Quipper
import Quipper.Internal
import Quipper.Algorithms.BF.Hex
import Quipper.Libraries.QFT 
import Quipper.Libraries.QuantumIf
import Quipper.Libraries.Simulation
import Quipper.Libraries.Decompose

import Quipper.Utils.Auxiliary (mmap)

import Data.Typeable

-- ----------------------------------------------------------------------
-- * Classical data structures

-- ** Oracle description

-- $ We define a data structure to hold the various parameters that
-- are used to define an oracle.

-- | The input to the BF Algorithm is the description of an oracle to
-- represent a given size of hex board, and a given size for the phase
-- estimation register.
data BooleanFormulaOracle = BFO {
  oracle_x_max :: Int,   -- ^ The /x/-dimension of hex board.
  oracle_y_max :: Int,   -- ^ The /y/-dimension of hex board.
  oracle_t :: Int,       -- ^ Size of phase estimation register.
        
  -- The number of moves remaining can
  -- depend on the starting state of the HexBoard
  oracle_s :: Int,       -- ^ Number of moves remaining.
                         -- This should start as /x/⋅/y/, if no moves have been made.
  oracle_m :: Int,       -- ^ Size of the direction register,
                         -- i.e., size of labels on the BF tree.
                         -- This should be the ceiling of log(/x/⋅/y/).

   
  start_board :: HexBoard, -- ^ A description of the starting state of the
                           -- board, and can be used to calculate /s/.
  oracle_hex :: HexCircuit -- ^ An extra flag that we can use so that different
                           -- HEX circuits can be used instead of the full circuit.

} 

-- | A type to define which Hex circuit to use.
data HexCircuit = Hex      -- ^ The actual Hex circuit.
                | Dummy    -- ^ A Dummy Hex circuit.
                | EmptyHex -- ^ Nothing.

-- | Create an oracle description. This only requires /x/, /y/, and
-- /t/ to be specified, as the remaining values can be calculated. The number of
-- moves remaining, /s/, is calculated as the total number of squares on the board, 
-- and /m/ is calculated as the number of bits required to represent /s/+1.
createOracle :: Int -> Int -> Int -> BooleanFormulaOracle
createOracle x y t = BFO {
        oracle_x_max = x,
        oracle_y_max = y,
        oracle_t = t,
        oracle_s = s,
        oracle_m = m,
        start_board = (empty,empty),
        oracle_hex = Hex
} where s = x * y
        m = ceiling (log (fromIntegral (s+1)) / log 2)
        empty = replicate s False

-- | A function to set the \"Dummy\" flag in the given oracle to the given 
-- 'HexCircuit' value.
update_hex :: BooleanFormulaOracle -> HexCircuit -> BooleanFormulaOracle
update_hex bfo hex = bfo {oracle_hex = hex}

-- | Update the 'start_board' in the given oracle, with the given 'HexBoard'. This
-- also updates the 'oracle_s' field of the oracle to be in line with
-- the new 'start_board'.
update_start_board :: BooleanFormulaOracle -> HexBoard -> BooleanFormulaOracle
update_start_board bfo start = bfo {
  oracle_s = s,
  start_board = start
 } where
    x = oracle_x_max bfo
    y = oracle_y_max bfo
    s = (x*y) - (moves_made start)

-- | An oracle for a 9 by 7 Hex board, with the parameters:
-- /x/=9, /y/=7, /t/=189. The calculated values are: /s/=63, /m/=6.
full_oracle :: BooleanFormulaOracle
full_oracle = createOracle 9 7 189

-- | A smaller oracle for testing purposes. The numbers should be
-- chosen such that /x/⋅/y/ = 2[sup /n/]−1 for some /n/. Here, we set
-- /x/=3 and /y/=5, to give /x/⋅/y/=15. We arbitrarily set the size of
-- the phase estimation register to /t/=4.
test_oracle :: BooleanFormulaOracle
test_oracle = createOracle 5 3 4

-- ** Hex boards

-- | A hex board is specified by a pair of lists of booleans.  For a
-- board of size /x/ by /y/, each list should contain /x/⋅/y/
-- elements.  The first list is the \"blue\" bitmap, and the second is
-- the \"red\" maskmap.
type HexBoard = ([Bool],[Bool])

-- | A function to determine how many moves have been made on a given HexBoard.
-- This function assumes that the given 'HexBoard' is valid, in the sense that
-- no duplicate moves have been made.
moves_made :: HexBoard -> Int
moves_made (blue,red) = moves blue + moves red
  where moves color = length (filter id color)

-- | A function to determine which spaces are still empty in the given HexBoard.
-- This function assumes that the given 'HexBoard' is valid, in the sense that
-- no duplicate moves have been made. This function will return a list of all the 
-- empty spaces remaining, in strictly increasing order.
empty_spaces :: HexBoard -> [Int]
empty_spaces (blue,red) = empty_spaces' blue red 0
  where
   empty_spaces' [] [] _ = []
   empty_spaces' [] _ _ = error "empty_spaces: Red and Blue boards of different length"
   empty_spaces' _ [] _ = error "empty_spaces: Red and Blue boards of different length"
   empty_spaces' (b:bs) (r:rs) n = if (b || r) then rest else (n:rest)
     where rest = empty_spaces' bs rs (n+1)

-- ----------------------------------------------------------------------
-- * Quantum data structures

-- $ Some data structures to help in defining the algorithm.

-- | The phase estimation register is a simple register of qubits. This is kept
-- separate from the rest of the 'BooleanFormulaRegister' as it is this register
-- which will be measured at the end of the algorithm.
type PhaseEstimationRegister = [Qubit]

-- | The direction register is a simple register of qubits, 
--   made explicit here so we can see that a \"position\" is a list of directions.
type GenericDirectionRegister a = [a]

-- | A type synonym defined as the 'Qubit' instance of a
-- 'GenericDirectionRegister'.
type DirectionRegister = GenericDirectionRegister Qubit

-- | The rest of the boolean formula algorithm requires a register which is 
-- split into 3 main parts.
data GenericBooleanFormulaRegister a = BFR {
     -- | The position register is split into two parts:
     -- the leaf and paraleaf \"flags\".
     position_flags :: (a,a),
       -- | The current position, and how we got there, i.e., directions we followed.
       -- Any position can be reached by at most /x/⋅/y/ directions.
     position :: [GenericDirectionRegister a],
     work_leaf :: a,     
     work_paraleaf :: a, 
     work_binary :: a,        
     work_height :: a,   
     work_r :: a,        
     work_rp :: a,       
     work_rpp :: a,       -- ^ Seven flags that make up the work register.  
     direction :: GenericDirectionRegister a  -- ^ The direction register.
}
  deriving (Typeable, Show)

-- | A type synonym defined as the 'Qubit' instantiation of a 
-- 'GenericBooleanFormulaRegister'.
type BooleanFormulaRegister = GenericBooleanFormulaRegister Qubit

-- | A function to add labels to the wires that make up a 'BooleanFormulaRegister'.
-- These labels correspond to the parts of the register. 
labelBFR :: BooleanFormulaRegister -> Circ ()
labelBFR reg = do
  let tuple = toTuple reg
  label tuple (("pos-leaf","pos-paraleaf"),
               "pos",
               ("leaf","paraleaf","binary","height","r","rp","rpp"),
                "dir")

-- | A type synonym defined as the 'Bool' instantiation of a 
-- 'GenericBooleanFormulaRegister'.
type BoolRegister = GenericBooleanFormulaRegister Bool

-- | Helper function to simplify the 'QCData' instance for 'BooleanFormulaRegister'. 
-- Create a tuple from a 'GenericBooleanFormulaRegister'.
toTuple :: GenericBooleanFormulaRegister a -> ((a,a),[[a]],(a,a,a,a,a,a,a),[a])
toTuple r = (position_flags r,position r,(work_leaf r,work_paraleaf r,work_binary r,work_height r,work_r r,work_rp r,work_rpp r),direction r)

-- | Helper function to simplify the 'QCData' instance for 'BooleanFormulaRegister'. 
-- Create a 'GenericBooleanFormulaRegister' from a tuple.
fromTuple :: ((a,a),[[a]],(a,a,a,a,a,a,a),[a]) -> GenericBooleanFormulaRegister a 
fromTuple (pf,p,(wl,wp,wb,wh,wr,wrp,wrpp),d) = BFR {
  position_flags = pf,
  position = p,
  work_leaf = wl,
  work_paraleaf = wp,
  work_binary = wb,
  work_height = wh,
  work_r = wr,
  work_rp = wrp,
  work_rpp = wrpp,
  direction = d
  }

type instance QCType x y (GenericBooleanFormulaRegister a) = GenericBooleanFormulaRegister (QCType x y a)
type instance QTypeB (GenericBooleanFormulaRegister a) = GenericBooleanFormulaRegister (QTypeB a) 
instance QCData a => QCData (GenericBooleanFormulaRegister a) where
  qcdata_mapM s f g xs = mmap fromTuple $ qcdata_mapM (toTuple s) f g (toTuple xs)
  qcdata_zip s q c q' c' xs ys e = fromTuple $ qcdata_zip (toTuple s) q c q' c' (toTuple xs) (toTuple ys) e
  qcdata_promote a x s = fromTuple $ qcdata_promote (toTuple a) (toTuple x) s
instance (Labelable a String) => Labelable (GenericBooleanFormulaRegister a) String where
  label_rec r s = do
    label_rec (position_flags r) s `dotted_indexed` "posflag"
    label_rec (position r) s       `dotted_indexed` "pos"
    label_rec (work_leaf r) s      `dotted_indexed` "leaf"
    label_rec (work_paraleaf r) s  `dotted_indexed` "paraleaf"
    label_rec (work_binary r) s    `dotted_indexed` "binary"
    label_rec (work_height r) s    `dotted_indexed` "height"
    label_rec (work_r r) s         `dotted_indexed` "r"
    label_rec (work_rp r) s        `dotted_indexed` "rp"
    label_rec (work_rpp r) s       `dotted_indexed` "rpp"
    label_rec (direction r) s      `dotted_indexed` "dir"

-- | Create an initial classical 'BooleanFormulaRegister' for a given oracle description.
-- The /position/ register is initialized in the /zero/ state that represents being
-- at label /zero/, or node /rpp/ in the tree. The work qubits are all initialized to
-- /zero/, as the first call to the /oracle/ circuit will set them accordingly for
-- the /position/ we are currently in. The /direction/ register is also set to /zero/
-- as this is the direction in which the node /rp/ is in. The given
-- 'BooleanFormulaOracle' is used to make sure the registers are of the correct
-- size, i.e., number of qubits.
createRegister :: BooleanFormulaOracle -> BoolRegister
createRegister oracle = BFR {
  position_flags = (False,False),
  position = replicate s (replicate m False),
  work_leaf = False,
  work_paraleaf = False,
  work_binary = False,
  work_height = False,
  work_r = False,
  work_rp = False,
  work_rpp = False,
  direction = replicate m False        
  } where
     s = oracle_s oracle
     m = oracle_m oracle

-- | Create a shape parameter for a 'BooleanFormulaRegister' of the
-- correct size.
registerShape :: BooleanFormulaOracle -> BooleanFormulaRegister     
registerShape oracle = qshape (createRegister oracle)

-- | Initialize a 'BooleanFormulaRegister' from a 'BooleanFormulaOracle'. 
initializeRegister :: BooleanFormulaOracle -> Circ BooleanFormulaRegister
initializeRegister oracle = qinit (createRegister oracle)

-- ======================================================================
-- * Oracle implementation

-- $ The functions in this implementation follow a separation of the boolean
-- formula algorithm into two parts. The first part corresponds to the 
-- algorithms defined in this module. The second part consists of the 
-- algorithms defined in "Quipper.Algorithms.BF.Hex". This separation relates to the 
-- first part defining the quantum parts of the algorithm, including the 
-- phase estimation, and the quantum walk, whereas the remaining four define 
-- the classical implementation of the circuit for determining which player 
-- has won a completed game of Hex, which is converted to a quantum circuit 
-- using Quipper's \"build_circuit\" keyword.
--
-- Note that the circuits for the algorithms in this module have been tested
-- for performing a quantum walk on the tree defined for a given oracle (but 
-- with a dummy function taking the place of the call to HEX).

-- | The overall Boolean Formula Algorithm. It initializes the
-- phase estimation register into an equal super-position of all 2[sup t] states,
-- and the other registers as defined previously. It then maps the exponentiated
-- version of the unitary /u/, as per phase estimation, before applying the 
-- inverse QFT, and measuring the result.
qw_bf :: BooleanFormulaOracle -> Circ [Bit]
qw_bf oracle = do
    -- initialize the phase estimation register, 
    -- and put it in an equal super-position
    let t = oracle_t oracle
    a <- qinit (replicate t False)
    label a "a"
    a <- mapUnary hadamard a
    -- initialize the other boolean formula registers
    b <- initializeRegister oracle  
    labelBFR b
    -- we can use a separate recursive function to map the exp_u algorithm over a 
    let t = oracle_t oracle  
    map_exp_u oracle a b (t-1)
    -- qft is defined, so we reverse it to get inverse qft 
    a <- (subroutine_inverse_qft oracle) a 
    -- we're only interested in the result of measuring a, 
    -- so we can discard all the qubits in the rest of the register
    qdiscard b 
    measure a

-- | The inverse quantum Fourier transform as a boxed subroutine.
subroutine_inverse_qft :: BooleanFormulaOracle -> [Qubit] -> Circ [Qubit]
subroutine_inverse_qft o = box "QFT*" (reverse_generic_endo qft_little_endian)  

-- | \"Map\" the application of the exponentiated unitary /u/
-- over the phase estimation register. That is, each qubit in the phase estimation
-- register is used as a control over a call to the unitary /u/, exponentiated to
-- the appropriate power.
map_exp_u :: BooleanFormulaOracle -> [Qubit] -> BooleanFormulaRegister -> Int -> Circ ()
map_exp_u _ [] _ _ = return ()
map_exp_u o (a:as) b l = do
    let x_max = oracle_x_max o
    -- we can move the control out of the exp_u function
    exp_u o (2^(l-(length as))) b `controlled` a 
    map_exp_u o as b l

-- | Exponentiate the unitary /u/. In this implementation, this is
-- achieved by repeated application of /u/.
exp_u :: BooleanFormulaOracle -> Integer -> BooleanFormulaRegister -> Circ ()
exp_u _ 0 _ = return ()
exp_u o n_steps b = do
    (subroutine_u o) b
    exp_u o (n_steps-1) b

-- | The unitary /u/ represents a single step in the walk on the NAND tree. A call
-- to the oracle determines what type of node we are at (so we know which directions
-- are valid to step to), the call to diffuse sets the direction register to be a
-- super-position of all valid directions, the call to walk performs the step, and then
-- the call to undo oracle has to clean up the work registers that were set by the
-- call to the oracle. Note that the undo oracle step is not simply the inverse of the
-- oracle, as we have walked since the oracle was called.
u :: BooleanFormulaOracle -> BooleanFormulaRegister -> Circ ()
u o b = do
    comment "U"
    labelBFR b
    (subroutine_oracle o) b
    (subroutine_diffuse o) b
    (subroutine_walk o) b
    (subroutine_undo_oracle o) b 

-- | The circuit for 'u' as a boxed subroutine.
subroutine_u :: BooleanFormulaOracle -> BooleanFormulaRegister -> Circ ()
subroutine_u o = box "U" (u o)

-- | Call the oracle to determine some extra information about where
-- we are in the tree. Essentially, the special cases are when were are at one of
-- the three \"low height\" nodes, or when we are at a node representing a complete 
-- game of Hex, and we need to determine if this is a leaf, by calling the hex circuit,
-- which determines whether the node represents a completed game of hex in which
-- the red player has won.  
oracle :: BooleanFormulaOracle -> BooleanFormulaRegister -> Circ ()
oracle o register = do
    comment "ORACLE"
    labelBFR register
    let init = start_board o
    let x_max = oracle_x_max o
    let (is_leaf,is_paraleaf) = position_flags register  
    with_controls (is_leaf) 
     ( -- if is_leaf
       -- we are at a leaf node, so set "leaf"
      do
      let leaf = work_leaf register
      qnot_at leaf
     )
    with_controls (is_leaf .==. False .&&. is_paraleaf .==. True)
     ( -- else if is_paraleaf
       -- we are at a paraleaf node, so set "paraleaf"                          
      do
      let paraleaf = work_paraleaf register
      qnot_at paraleaf
      let binary = work_binary register
      qnot_at binary
      let pos = position register
      let hex_subroutine = case oracle_hex o of
                            Hex -> box "HEX" (hex_oracle init (oracle_s o) x_max)
                            Dummy -> hex_oracle_dummy 
                            EmptyHex -> \x -> return x 
      -- hex sets "binary" flag depending on whether the paraleaf is attached to a
      -- a leaf, i.e., whether red has won or lost the game of hex.
      hex_subroutine (pos,binary)
      return ()
     )
    with_controls (is_leaf .==. False .&&. is_paraleaf .==. False)
     ( -- else
       -- we're not at a leaf node, or paraleaf node
      do      
      let pos = position register
      -- are we at a "low height" node?
      with_controls (controls is_paraleaf pos)
       ( -- we're at a "low height" node
        do
        let pos'' = pos !! (length pos - 2)
        let pos_m = last pos''
        with_controls pos_m
         ( -- if pos_m == 1
          do
          let height = work_height register
          qnot_at height
         )
        let pos' = last pos 
        let pos_1 = pos' !! (length pos' - 2)
        with_controls (pos_m .==. False .&&. pos_1 .==. True)
         ( -- else if pos_1 == 1
          do
          let r = work_r register
          qnot_at r
         )
        let pos_0 = last pos'
        with_controls (pos_m .==. False .&&. pos_1 .==. False .&&. pos_0 .==. True)
         ( -- else if pos_0 == 1
          do
          let rp = work_rp register
          qnot_at rp
          let binary = work_binary register
          qnot_at binary
         )
        with_controls (pos_m .==. False .&&. pos_1 .==. False .&&. pos_0 .==. False)
         ( -- else
          do
          let rpp = work_rpp register
          qnot_at rpp
         )  
       )
     )

-- | The circuit for the 'oracle' as a boxed subroutine.
subroutine_oracle :: BooleanFormulaOracle -> BooleanFormulaRegister -> Circ ()
subroutine_oracle o = box "Oracle" (oracle o)

-- | The controls to use, to see if we're at a \"low height\" node.
controls :: Qubit -> [DirectionRegister] -> [ControlList]
controls is_paraleaf pos = (is_paraleaf .==. False) : ctrls pos
    where ctrls [] = []
          ctrls [p] = []
          ctrls [p,q] = []
          ctrls (p:ps) = (last p .==. False) : ctrls ps

-- | Diffuse the direction register, to be a super-position of all valid
-- directions from the current node. Note, that this implementation of the boolean
-- formula algorithm does not applying the correct weighting scheme to the NAND graph,
-- which would require this function to diffuse with respect to the weighting scheme.
diffuse :: BooleanFormulaRegister -> Circ ()
diffuse register = do
    comment "DIFFUSE"
    labelBFR register
    let binary = work_binary register
    let dir = direction register
    with_controls binary
     ( -- if binary == 1
      do
      let dir_0 = last dir
      hadamard_at dir_0 
     )
    let leaf = work_leaf register
    let rpp = work_rpp register     
    with_controls (binary .==. False .&&. leaf .==. False .&&. rpp .==. False)
     ( -- else (controlled on binary == 0, leaf == 0, rpp == 0)
      do
      mapUnary hadamard dir
     )
    return ()

-- | The circuit for 'diffuse' as a boxed subroutine.
subroutine_diffuse :: BooleanFormulaOracle -> BooleanFormulaRegister -> Circ ()
subroutine_diffuse o = box "Diffuse" diffuse

-- | A datatype to use instead of passing integers to 'toParent' and 'toChild'
-- to define what needs to be shifted. This is used as only three different
-- shift widths are ever used in the algorithm.
data Where = Width -- ^ corresponds to shifting all qubits.
           | M     -- ^ corresponds to shifting only /m/+1 qubits.
           | M2    -- ^ corresponds to shifting only 2/m/+1 qubits.
      deriving Eq

-- | Define a step on the NAND graph, in the direction specified 
-- by the direction register, and updates the direction register to be where
-- we have stepped from.
-- For this algorithm we have developed the 'if_then_elseQ' construct, which
-- gives us a nice way of constructing if/else statements acting on
-- boolean statements over qubits (see "Quipper.Libraries.QuantumIf").
walk :: BooleanFormulaRegister -> Circ ()
walk register = do
    comment "WALK"
    labelBFR register
    let leaf = work_leaf register
    let paraleaf = work_paraleaf register
    let dir = direction register
    let dir_0 = last dir
    let (is_leaf,is_paraleaf) = position_flags register    
    let pos = position register
    let pos_0 = last (last pos)
    let pos_1 = last (init (last pos))
    let height_1 = work_height register
    let rpp = work_rpp register
    let rp = work_rp register
    let r = work_r register
    let dir_all_1 = foldr1 (\x y -> And x y) (map A dir)
    let boolean_statement_in = Or (A leaf) (And (A paraleaf) (Not (A dir_0)))
    let boolean_statement_out = Or (A leaf) (And (A paraleaf) (A is_leaf))
    if_then_elseQinv boolean_statement_in
     ( -- if leaf == 1 or (paraleaf == 1 and dir_0 == 0)
      do
      qnot_at is_leaf
     )
     ( -- else (leaf == 0 and (paraleaf == 0 or dir_0 == 1))
      do
      let boolean_statement_in = And (A paraleaf) (A dir_0)
      let boolean_statement_out = And (A paraleaf) (Not (dir_all_1))
      if_then_elseQinv boolean_statement_in 
       ( -- if paraleaf == 1 and dir_0 == 1
        toParent Width register
        -- now, dir /= 1..1, so dir_0 could be either 0 or 1
       )
       ( -- else (paraleaf == 0 or dir_0 == 0)
        do
        let boolean_statement_in = Or (A rpp) (And (A rp) (A dir_0))
        let boolean_statement_out = Or (A rpp) (And (A rp) (Not (A dir_0)))
        if_then_elseQinv boolean_statement_in
         ( -- if rpp == 1 or (rp == 1 and dir_0 == 1 )
          do
          qnot_at pos_0
          -- dir_0 should be changed,
          -- as we're moving from rp to rpp, and rpp only has a child at 0
          -- or we're moving from rpp to rp, and dir_0 should be set to 1 as
          -- we have come from a parent 
          qnot_at dir_0
         )
         ( -- else (rpp == 0 and (rp == 0 or dir_0 == 0))
          do
          let boolean_statement_in = Or (And (A rp) (Not (A dir_0))) (And (A r) dir_all_1)
          let pos_m = last (last (init pos))         
          let boolean_statement_out = Or (And (A rp) dir_all_1) (And (A r) (And (Not dir_all_1) (Not (A pos_m))))
          if_then_elseQinv boolean_statement_in
           ( -- if (rp == 1 and dir_0 == 0) or (r == 1 and dir == 1..1)
            do
            qnot_at pos_1
            -- we know that pos_m == 0
            -- dir is should be changed
            -- when we move from rp to r, and when we move from r to rp
            mapUnary qnot dir
            return ()
           )
           ( -- else ((rp == 0 or dir_0 == 1) and (r == 0 or dir /= 1..1))
            do
            let boolean_statement = A r
            if_then_elseQ boolean_statement
             ( -- if r == 1
              do
              qnot_at pos_1
              toChild M register
              -- now dir == 1..1
              -- we also know that pos_m == 1
             )
             ( -- else
              do
              let boolean_statement_in = And (A height_1) (dir_all_1)
              let boolean_statement_out = And (A height_1) (Not dir_all_1)
              if_then_elseQinv boolean_statement_in
               ( -- if height_1 == 1 and dir == 1..1
                do
                toParent M register
                qnot_at pos_1
                -- now, dir /= 1..1
               )
               ( -- else height_1 == 0 or dir /= 1..1
                do
                let boolean_statement = A height_1
                if_then_elseQ boolean_statement
                 ( -- if height_1 == 1    (and dir /= 1..1)
                  do
                  toChild M2 register
                  -- now dir == 1..1
                 )
                 ( -- else (if height_1 == 0)
                  do
                  let boolean_statement_in = dir_all_1
                  let boolean_statement_out = Not dir_all_1
                  if_then_elseQinv boolean_statement_in
                   ( -- if dir = 1..1
                     do
                     toParent Width register
                     -- now dir /= 1..1
                   )
                   ( --else (dir /= 1..1)
                     do
                     toChild Width register
                     -- now dir == 1..1
                   ) boolean_statement_out                   
                 )
               ) boolean_statement_out
             )
           ) boolean_statement_out
         ) boolean_statement_out
       ) boolean_statement_out
     ) boolean_statement_out  
    return ()

-- | The circuit for 'walk' as a boxed subroutine.
subroutine_walk :: BooleanFormulaOracle -> BooleanFormulaRegister -> Circ ()
subroutine_walk o = box "Walk" walk

-- | Uncompute the various flags that were set by the initial call
-- to the oracle. It has to uncompute the flags depending on where we were before
-- the walk step, so isn't just the inverse of the oracle.
undo_oracle :: BooleanFormulaOracle -> BooleanFormulaRegister -> Circ ()
undo_oracle o register = do
    comment "UNDO_ORACLE"
    labelBFR register
    let initHB = start_board o
    let x_max = oracle_x_max o
    let paraleaf = work_paraleaf register
    let (is_leaf,is_paraleaf) = position_flags register
    with_controls paraleaf
     ( do
       let binary = work_binary register
       let pos = position register
       let dir = direction register
       let hex_subroutine = case oracle_hex o of
                             Hex -> box "HEX" (hex_oracle initHB (oracle_s o) x_max)
                             Dummy -> hex_oracle_dummy 
                             EmptyHex -> \x -> return x 
       hex_subroutine (pos,binary) 
       return ()
     )
    let leaf = work_leaf register
    let dir = direction register
    let dir_0 = last dir
    let boolean_statement = And (Not (A is_leaf)) (And (A is_paraleaf) (Not (A dir_0)))
    if_then_elseQ boolean_statement
     ( -- if is_leaf == 0 and is_paraleaf == 1 and dir_0 == 0
       -- we went from a leaf to a paraleaf, so we can unset leaf
      do
      qnot_at leaf
     )
     ( -- else
      do
      let binary = work_binary register
      let pos = position register
      let pos_w_2_m = last (head pos)
      let dir_all_1 = foldr1 (\x y -> And x y) (map A dir)
      let boolean_statement = Or (A is_leaf) (And (Not (A is_leaf)) (And (Not (A is_paraleaf)) (And (A pos_w_2_m) (Not (dir_all_1)))))
      if_then_elseQ boolean_statement
       ( -- if is_leaf == 1 or (is_leaf == 0 and is_paraleaf == 0 and pos_w_2_m == 1 and dir /= 1..1)
        -- we went from a paraleaf to a leaf, so unset binary and paraleaf
        -- or we went from a paraleaf to its parent...
        do
        qnot_at binary
        qnot_at paraleaf
       )
       ( -- else
        do
        with_controls (init (controls is_paraleaf pos))
         ( -- if pos_sm,pos_(s-1)m,...,3. == 00...0
          do
          let height = work_height register
          let r = work_r register
          let rp = work_rp register
          let pos_0 = last (last pos)
          let pos_1 = last (init (last pos))
          let pos_m = last (last (init pos))
          let pos_2m = last (last (init (init pos)))
          let boolean_statement = dir_all_1
          if_then_elseQ boolean_statement
           ( -- if dir = 1...1
            do
            qnot_at height `controlled` pos_2m
            qnot_at r `controlled` (pos_2m .==. False .&&. pos_m .==. True)
            with_controls (pos_2m .==. False .&&. pos_m .==. False .&&. pos_1 .==. True)
             (
              do
              qnot_at rp
              qnot_at binary
             )
           )
           ( -- else
             with_controls (pos_2m .==. False .&&. pos_m .==. False)
             (
              do
              let rpp = work_rpp register 
              qnot_at height `controlled` pos_1
              qnot_at rpp `controlled` (pos_1 .==. False .&&. dir_0 .==. True)
              qnot_at r `controlled` (pos_1 .==. False .&&. dir_0 .==. False .&&. pos_0 .==. True)
              with_controls (pos_1 .==. False .&&. dir_0 .==. False .&&. pos_0 .==. False)
               (
                do
                qnot_at rp
                qnot_at binary
               )
             )
           )
         ) -- end if
       )
     )
    return ()

-- | The circuit for 'undo_oracle' as a boxed subroutine.
subroutine_undo_oracle :: BooleanFormulaOracle -> BooleanFormulaRegister -> Circ ()
subroutine_undo_oracle o = box "Undo Oracle" (undo_oracle o)

-- | Define the circuit that updates the position register to be the
-- parent node of the current position.
toParent :: Where -> BooleanFormulaRegister -> Circ ()
toParent M2 _ = error "TOPARENT should never be called with 2m+1 as width"
toParent w register = do
    let pos = position register :: [[Qubit]] -- of length x*y
    let pos_firstM = last pos :: [Qubit] -- of length m
    let pos_secondM = last (init pos) :: [Qubit] -- of length m  
    let pos_0 = last pos_firstM :: Qubit
    let pos_m = last pos_secondM :: Qubit
    let dir = direction register :: [Qubit] -- of length m
    let (_,is_paraleaf) = position_flags register :: (Qubit,Qubit)
    mapUnary qnot dir
    mapBinary copy_from_to (reverse pos_firstM) (reverse dir)
    if (w == Width) then
     ( do -- width
       -- we need to shift everything to the right by m 
       shift_right pos
       -- we need to shift is_paraleaf to x*y*m
       copy_from_to is_paraleaf (last (head pos))
       return ()
     ) else return ()
    if (w == M) then
     ( do -- m+1
       -- we need to "shift" pos_m to pos_0
       copy_from_to pos_m pos_0
       return ()      
     ) else return ()

-- | @'copy_from_to' a b@: Sets the state of qubit /b/ to be the state of qubit /a/,
--   (and the state of /a/ is lost in the process, so this is not cloning).
--   It falls short of swapping /a/ and /b/, as we're not interested in preserving /a/.
copy_from_to :: Qubit -> Qubit -> Circ (Qubit,Qubit)
copy_from_to from to = do
    qnot_at to `controlled` from
    qnot_at from `controlled` to
    return (from,to)

-- | Define the circuit that updates the position register to be the
-- child node of the current position.
toChild :: Where -> BooleanFormulaRegister -> Circ ()
toChild w register = do
    let pos = position register :: [[Qubit]] -- of length x*y
    let pos_firstM = last pos :: [Qubit] -- of length m
    let pos_secondM = last (init pos) :: [Qubit] -- of length m  
    let pos_thirdM = last (init (init pos)) :: [Qubit] -- of length m
    let pos_0 = last pos_firstM :: Qubit
    let pos_m = last pos_secondM :: Qubit
    let pos_2m = last pos_thirdM :: Qubit
    let dir = direction register :: [Qubit] -- of length m
    let (_,is_paraleaf) = position_flags register :: (Qubit,Qubit)
    if (w == Width) then
     ( do -- width
       -- we need to "shift" x*y*m to is_paraleaf
       copy_from_to (last (head pos)) is_paraleaf
       -- we need to "shift" everything to the left by "m"
       shift_left pos
     ) else return ()
    if (w == M2) then
     ( do -- 2m+1
       -- we need to "shift" pos_m to pos_2m
       copy_from_to pos_m pos_2m
       -- we need to "shift" 0.. to m..  to 
       shift_left [pos_secondM,pos_firstM]
     ) else return ()
    if (w == M) then
     ( do
       -- we need to "shift" pos_0 to pos_m
       copy_from_to pos_0 pos_m
       return ()
     ) else return ()     
    mapBinary copy_from_to dir pos_firstM
    mapUnary qnot dir
    return ()

-- | Shift every qubit in a register to the left by one. 
shift_left :: [DirectionRegister] -> Circ ()
shift_left [] = return ()
shift_left [d] = return ()
shift_left (d:d':ds) = do
    mapBinary copy_from_to d' d
    shift_left (d':ds)

-- | Shift every qubit in a register to the right by one.
shift_right :: [DirectionRegister] -> Circ ()
shift_right [] = return ()
shift_right [d] = return ()
shift_right (d:d':ds) = do
    shift_right (d':ds)
    mapBinary copy_from_to (reverse d) (reverse d')
    -- the arguments are reversed to give a nice symmetry to the circuits
    -- and should be equivalent to if they're not reversed
    return ()

-- ----------------------------------------------------------------------
-- * Possible main functions

-- $ The following functions define various \main\ functions that can be called
-- from an overall \main\ function to display various parts of the
-- overall Boolean Formula Algorithm. The Boolean 
-- Formula Algorithm is split into 13 sub-algorithms, each of which can be
-- displayed separately, or in various combinations.

-- | Displays the overall Boolean Formula circuit for a given oracle description.
main_circuit :: Format -> GateBase -> BooleanFormulaOracle -> IO ()
main_circuit f g oracle = print_simple f (decompose_generic g (qw_bf oracle))

-- | Display just 1 time-step of the given oracle,
--   i.e., one iteration of the 'u' from 'exp_u', with no controls.
main_u :: Format -> GateBase -> BooleanFormulaOracle -> IO ()
main_u f g o = print_generic f (decompose_generic g (u o)) (registerShape o)

-- | Display just 1 time-step of the 'walk' algorithm for the given oracle,
--   i.e., one iteration of /walk/, with no controls.
main_walk :: Format -> GateBase -> BooleanFormulaOracle -> IO ()
main_walk f g o = print_generic f (decompose_generic g walk) (registerShape o)

-- | Display just 1 time-step of the 'diffuse' algorithm for the given oracle,
--   i.e., one iteration of /diffuse/, with no controls.
main_diffuse :: Format -> GateBase -> BooleanFormulaOracle -> IO ()
main_diffuse f g o = print_generic f (decompose_generic g diffuse) (registerShape o)

-- | Display just 1 time-step of the 'oracle' algorithm for the given oracle,
--   i.e., one iteration of /oracle/, with no controls.
main_oracle :: Format -> GateBase -> BooleanFormulaOracle -> IO ()
main_oracle f g o = print_generic f (decompose_generic g (oracle o)) (registerShape o)

-- | Display just 1 time-step of the 'undo_oracle' algorithm for the given oracle,
--   i.e., one iteration of /undo_oracle/, with no controls.
main_undo_oracle :: Format -> GateBase -> BooleanFormulaOracle -> IO ()
main_undo_oracle f g o = print_generic f (decompose_generic g (undo_oracle o)) (registerShape o)

-- | Display the circuit for the Hex algorithm, for the given oracle,
-- i.e., one iteration of 'hex_oracle', with no controls.
main_hex :: Format -> GateBase -> BooleanFormulaOracle -> IO ()
main_hex f g o = print_generic f (decompose_generic g (hex_oracle init s x_max)) (pos,binary)
  where
    init = start_board o
    s = oracle_s o
    x_max = oracle_x_max o
    reg = registerShape o
    pos = position reg
    binary = work_binary reg

-- | Display the circuit for the Checkwin_red algorithm, for the given oracle,
-- i.e., one iteration of 'checkwin_red_circuit', with no controls.
main_checkwin_red :: Format -> GateBase -> BooleanFormulaOracle -> IO ()
main_checkwin_red f g o = print_generic f (decompose_generic g (checkwin_red_circuit x_max)) (qshape redboard,qubit)
  where
    (redboard,_) = start_board o
    x_max = oracle_x_max o  

-- ----------------------------------------------------------------------
-- * Running the Boolean Formula Algorithm

-- $ The following functions define the way that the Boolean Formula Algorithm
-- would be run, if we had access to a quantum computer. Indeed, the functions
-- here interface with the "QuantumSimulation" quantum simulator so that they
-- can be built.

-- | Approximation of how the algorithm would be run if we had a quantum computer:
--   uses QuantumSimulation run_generic_io function. The output of the algorithm will
-- be all False only in the instance that the Blue player wins the game.
main_bf :: BooleanFormulaOracle -> IO Bool
main_bf oracle = do
        output <- run_generic_io (undefined :: Double) (qw_bf oracle)
        let result = if (or output) then True  -- a /= 0 (Red Wins) 
                                    else False -- a == 0 (Blue Wins)
        return result

-- | Display the result of 'main_bf',
--   i.e., either \"Red Wins\", or \"Blue Wins\" is the output.
whoWins :: BooleanFormulaOracle -> IO ()
whoWins oracle = do
        result <- main_bf oracle
        if result then putStrLn "Red Wins"
                  else putStrLn "Blue Wins"

-- | Run 'whoWins' for the given oracle, and its \"initial\" board.
main_whoWins :: BooleanFormulaOracle -> IO ()
main_whoWins o = whoWins o