content: -- This file is part of Quipper. Copyright (C) 2011-2014. Please see the
  -- file COPYRIGHT for a list of authors, copyright holders, licensing,
  -- and other details. All rights reserved.
  -- 
  -- ======================================================================
  
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeSynonymInstances #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE FunctionalDependencies #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE UndecidableInstances #-}
  
  -- | This module provides a user-friendly interface to building
  -- quantum circuits out of classical functions on booleans. It is
  -- based on lower-level functionality provided by
  -- "Libraries.Template".
  -- 
  -- Technically, the only functions to be used in this module are
  -- @'decToCircMonad'@, a specialized version of @'decToMonad'@, and
  -- @'unpack'@. The only useful datatype here is @'BoolParam'@.
  -- 
  -- One should not have to directly use the other things: they are only
  -- for the internal use of Template Haskell to build quantum circuits
  -- out of classical computation on booleans.
  -- 
  -- Note: in the following, we write circuits in ASCII form. The
  -- following conventions are used. They are extended in obvious ways
  -- when applicable (e.g. when writing a ternary gate).
  -- 
  -- > ---- : wire
  -- > 
  -- > 0 |-- : initialize an ancilla |0>
  -- > 
  -- > --| 0 : terminate an ancilla, asserting it was |0>
  -- > 
  -- >   +--+
  -- >  -|  |- : a unary gate
  -- >   +--+
  -- > 
  -- >   +--+
  -- >  -|  |- 
  -- >   |  |  : a binary gate
  -- >  -|  |- 
  -- >   +--+
  -- >
  -- >  -- --
  -- >    X   : swap gate
  -- >  -- --
  -- > 
  -- >  --x-- 
  -- >    |   : controlled-not, applying NOT on the bottom wire if the top one is |1>
  -- >  --N-- 
  -- >
  -- >  --o-- 
  -- >    |   : controlled-not, applying NOT on the bottom wire if the top one is |0>
  -- >  --N-- 
  
  -- NOTE: They are only available because Template Haskell requires
  -- them to be in a separate module and exported.
  
  module Quipper.CircLifting (
    -- * Overview
    -- $ROLE 
  
    -- * A type of boolean parameters
    -- $BOOLPARAM 
    BoolParam(PTrue,PFalse),
    newBool,
    template_PFalse,
    template_PTrue,
      
    -- * Lifting classical functions to circuits
    -- $TH
    decToCircMonad,
    
  -- $BUILDTEMPLATE_ANCHOR #build_circuit#
    
    -- * Syntactic sugar
    -- $BUILDTEMPLATE
  
  
    -- * Circuits for specific operations
    -- ** Boolean parameters
    
    template_newBool,
  
    -- ** Boolean constants
    template_False,
    template_True,
    -- ** Unary boolean operations
    template_not,
    -- ** Binary boolean operations
    template_symb_ampersand_symb_ampersand_,
    template_symb_vbar_symb_vbar_,
    template_bool_xor,
    -- ** The if-then-else operation
    -- $IF
    template_if,
    -- ** Equality test
    template_symb_equal_symb_equal_,
  
    -- * Generic unpacking
    CircLiftingUnpack(..)
    
  ) where
  
  import Prelude
  import Language.Haskell.TH as TH
  import Data.Map as Map
  import qualified Data.List
  
  import Quipper.Monad
  import qualified Quipper.Monad
  import Quipper.Circuit
  import Quipper.Generic
  import Quipper.QData
  import Libraries.Auxiliary (list_of_blist,blist_empty)
  import Quipper.Control
  import Quipper.QClasses
  
  import Libraries.Template
  
  
  
  ----------------------------------------------------------------------
  -- * Overview
  
  -- $ROLE Using the tool @'decToMonad'@ designed in "Libraries.Template", we
  -- can easily generate quantum circuits. Indeed, suppose that we are given the classical oracle 
  -- 
  -- > toyOracle :: Bool -> Bool
  -- > toyOracle a = f (g a) (h a)
  -- 
  -- for some @g,h :: Bool -> Bool@ and @f :: Bool -> Bool -> Bool@. If
  -- /g/ and /h/ are given by quantum circuits of the form
  --
  -- >          +-----+
  -- > input ---|     |-- input wire, assumed to be not modified by the box
  -- >          |     |
  -- >      0 |-|     |--- output (was ancilla wire)
  -- >          +-----+
  --
  -- and if /f/ is given by
  --
  -- >          +-----+
  -- > input ---|     |-- was input 1, assumed to be not modified
  -- >          |     | 
  -- > input ---|     |-- was input 2, assumed to be not modified
  -- >          |     |
  -- >     0 |--|     |-- output (was ancilla wire),
  -- >          +-----+
  --
  -- we can compositionally generate a circuit @C@ for /toyOracle/ as follows.
  -- 
  -- >          +---+                    +---+
  -- > input ---|   |-- -----------------|   |-- (output of g)
  -- >          | g |  X  +---+          |   |
  -- >     0 |--|   |-- --|   |--- ------| f |-- (output of h)
  -- >          +---+     | h |   X      |   |                   (I)
  -- >     0 |------------|   |--- - ----|   |-- (output of f)
  -- >                    +---+     X    +---+
  -- >                          0 |- ----------- (input of g)
  -- >
  --
  -- Note that the resulting circuit is a classical, reversible circuit
  -- (more precisely, the circuit defines a one-to-one function). In
  -- order to obtain a reversible quantum circuit, one should then apply
  -- the function @'Quipper.Classical.classical_to_reversible'@ to get the following (we
  -- keep the same convention of wires as in the definition of @C@):
  --
  -- >        +---+     +---+
  -- > input--|   |-----|   |-- still the input
  -- >        |   |     |   |
  -- >   0 |--|   |-----|   |--| 0
  -- >        | C |     | D |                                    (II)
  -- >   0 |--|   |--x--|   |--| 0
  -- >        |   |  |  |   |
  -- >   0 |--|   |--|--|   |--| 0
  -- >        +---+  |  +---+
  -- >               |
  -- > output wire---N--------------.
  --
  -- Here @D@ is the inverse of @C@. We now have a circuit of the
  -- canonical form, computing and then uncomputing its ancillas:
  --
  -- >     +-----------+
  -- > a --|           |- a
  -- >     | toyOracle |
  -- > z --|           |- z + (f (g a) (h a))
  -- >     +-----------+
  --
  ----------------------------------------------------------------------
  -- * A type of boolean parameters
  
  -- $BOOLPARAM During the construction of a quantum circuit from
  -- classical code, the type 'Bool' is mapped to the type
  -- 'Qubit'. However, it is also sometimes useful to specify boolean
  -- parameters to be used during circuit generation (for example, in
  -- the BWT algorithm, the color is a parameter). For this purpose, we
  -- provide a new type 'BoolParam', which is identical to 'Bool' in
  -- most respects, except that it is not mapped to 'Qubit' during
  -- circuit generation.
  
  -- | A custom-design boolean type, not modified by circuit generation.
  data BoolParam = PTrue | PFalse
    deriving (Eq, Show)
  
  -- | Type-cast from BoolParam to Bool
  newBool :: BoolParam -> Bool
  newBool PTrue = True
  newBool PFalse = False
  
  
  -- | Lifted version of PFalse.
  template_PFalse :: Circ BoolParam
  template_PFalse = return PFalse
  
  -- | Lifted version of PTrue.
  template_PTrue :: Circ BoolParam
  template_PTrue = return PTrue
  
  
  ----------------------------------------------------------------------
  -- * Lifting classical functions to circuits
  
  -- $TH The main tool for transforming a classical computation into a
  -- quantum circuit is the function @'decToCircMonad'@. It inputs the
  -- syntax tree of a classical function, and outputs the syntax tree of
  -- a corresponding quantum circuit. The type 'Bool' is mapped to
  -- 'Qubit'; the type 'BoolParam' is unchanged; and each function /f/ :
  -- /a/ → /b/ is mapped to a function /f'/ : /a'/ → 'Circ' /b'/,
  -- where /a'/ and /b'/ are the translations of the types /a/ and /b/,
  -- respectively.
  -- 
  -- Most of the work is done by the lower-level function 
  -- @'decToMonad'@ from the module "Libraries.Template". 
  -- This lower-level function knows how to deal with many usual
  -- constructs of the Haskell language, such as function applications,
  -- lambda-abstractions, let-assignments, case-distinctions, and so
  -- on. However, @'decToMonad'@ does not by default know how to deal
  -- with the base cases, i.e., how to extract quantum circuits from
  -- specific term constants such as @'&&'@, @'||'@, etc.
  -- 
  -- The purpose of the remainder of this module is to do just that. For
  -- every constant or function @XXX@ that one may want to use in a
  -- classical program, we provide an implementation @template_XXX@ as a
  -- quantum circuit.  We refer to @template_XXX@ as the \"lifted\"
  -- version of @XXX@.  The function @'decToCircMonad'@ is a version of
  -- @'decToMonad'@ that knows about these liftings.
  
  
  
  -- | Input the syntax tree of a classical function, and output the
  -- syntax tree of a corresponding quantum function. The type 'Bool' is
  -- mapped to 'Qubit'; the type 'BoolParam' is unchanged; and and each
  -- function /f/ : /a/ → /b/ is mapped to a function /f'/ : /a'/ →
  -- 'Circ' /b'/, where /a'/ and /b'/ are the translations of the types
  -- /a/ and /b/, respectively. The function 'decToCircMonad' knows
  -- about many built-in operations such as @'&&'@ and @'||'@, whose
  -- circuit translations are defined below.
  decToCircMonad :: Q [Dec] -> Q [Dec]
  decToCircMonad x = decToMonad "Circ" x
  
  -- $BUILDTEMPLATE_ANCHOR #build_circuit#
  
  ---------------------------------------------------------------------
  -- * Syntactic sugar
  
  -- $BUILDTEMPLATE Quipper comes equipped with syntactic sugar to ease
  -- the use of the @'decToCircMonad'@ function.
  -- 
  -- Although the code
  -- 
  -- > $( decToCircMonad [d| f x = ... |] )
  -- 
  -- is valid, it is possible to use the special keyword
  -- @build_circuit@, as follows:
  -- 
  -- > build_circuit
  -- > f x = ...
  -- 
  -- This code is equivalent to
  -- 
  -- > f x = ...
  -- > $( decToCircMonad [d| f x = ... |] )
  -- 
  -- In other words, it generates both a function @f@ of type @a -> ...@
  -- and an object @template_f@ of type @Circ (a -> Circ ...)@.
  -- 
  -- The following spellings are recognized:
  --
  -- > build_circuit f x y z = ...
  --
  -- > build_circuit
  -- > f x y z = ...
  --
  -- > build_circuit
  -- > f :: a -> ...
  -- > f x y z = ...
  
  -- ----------------------------------------------------------------------
  -- * Circuits for specific operations
  
  -- ** Boolean parameters
  
  -- | Lifted version of 'newBool':
  -- 
  -- > newBool :: BoolParam -> Bool.
  --
  -- Depending on the boolean parameter, the circuit is either 
  -- 
  -- > 0 |--
  -- 
  -- or
  -- 
  -- > 1 |--
  template_newBool ::  Circ (BoolParam -> Circ Qubit)
  template_newBool =  return $ \b -> case b of 
                               PTrue  -> qinit_qubit True
                               PFalse -> qinit_qubit False
  
  ----------------------------------------------------------------------
  -- ** Boolean constants
  
  -- | Lifted version of 'False':
  -- 
  -- > False :: Bool.
  -- 
  -- The circuit is
  --
  -- > 0 |--   output: quantum bit in state |0>
  template_False :: Circ Qubit
  template_False = qinit_qubit False
  
  -- | Lifted version of 'True':
  -- 
  -- > True :: Bool.
  -- 
  -- The circuit is
  --
  -- > 1 |--   output: quantum bit in state |1>
  template_True :: Circ Qubit
  template_True = qinit_qubit True
  
  
  
  ----------------------------------------------------------------------
  -- ** Unary boolean operations
  
  -- | Lifted version of 'not':
  -- 
  -- > not :: Bool -> Bool.
  -- 
  -- The circuit is 
  -- 
  -- > a -----x--
  -- >        |
  -- >   1 |--N------- output: not a.
  template_not ::  Circ (Qubit -> Circ Qubit)
  template_not  = return $ \b -> do
  	  r <- qinit_qubit True;
            qnot_at r `controlled` b
  	  return r
  
  
  ----------------------------------------------------------------------
  -- ** Binary boolean operations
  
  -- | Lifted version of '&&':
  -- 
  -- > (&&) :: Bool -> Bool -> Bool.
  -- 
  -- The circuit is
  -- 
  -- > a -----x---
  -- >        |
  -- > b -----x---
  -- >        |
  -- >   0 |--N------- output: a and b.
  template_symb_ampersand_symb_ampersand_ ::  Circ (Qubit -> Circ (Qubit -> Circ Qubit))
  template_symb_ampersand_symb_ampersand_ =
    return $ \b1 -> return $ \b2 -> do 
           r <- qinit_qubit False;
           qnot_at r `controlled` [b1,b2];
           return r
  
  -- | Lifted version of '||':
  -- 
  -- > (||) :: Bool -> Bool -> Bool.
  -- 
  -- The circuit is
  -- 
  -- > a -----o---
  -- >        |
  -- > b -----o---
  -- >        |
  -- >   1 |--N------- output: a or b.
  template_symb_vbar_symb_vbar_ ::  Circ (Qubit -> Circ (Qubit -> Circ Qubit))
  template_symb_vbar_symb_vbar_ = return $ \b1 -> return $ \b2 -> do 
           r <- qinit_qubit True; 
           qnot_at r `controlled` b1 .==. 0 .&&. b2 .==. 0;
  	 return r
  
  
  -- | Lifted version of 'bool_xor':
  -- 
  -- > bool_xor :: Bool -> Bool -> Bool.
  -- 
  -- The circuit is
  -- 
  -- > a -----x-------
  -- >        |
  -- > b -----|---x---
  -- >        |   |
  -- >   0 |--N---N------ output: a xor b.
  template_bool_xor ::  Circ (Qubit -> Circ (Qubit -> Circ Qubit))
  template_bool_xor = return $ \b1 -> return $ \b2 -> do 
           r <- qinit_qubit False
  	 qnot_at r `controlled` b1
           qnot_at r `controlled` b2
           return r
  
  
  ----------------------------------------------------------------------
  -- ** The if-then-else operation
  
  -- $IF The last term we need to build is @'template_if'@, a term
  -- describing the if-then-else construct as a circuit.
  
  -- | Lifted version of the @if-then-else@ construction: 
  -- 
  -- > if-then-else :: Bool -> b -> b -> b         
  -- 
  -- We only allow first-order terms in the \"then\" and \"else\"
  -- clauses.  The circuit is:
  --
  -- > q -----x---o---
  -- >        |   |
  -- > a -----x---|---
  -- >        |   |
  -- > b -----|---x---
  -- >        |   |
  -- >   0 |--N---N-------- wire output of the function.
  template_if :: (QData b) => Circ Qubit -> Circ b -> Circ b -> Circ b
  template_if x a b = do
     x' <- x; a' <- a; b' <- b; map2Q (testOnQubit x') (a',b')
     where
     testOnQubit :: Qubit -> (Qubit,Qubit) -> Circ Qubit
     testOnQubit x (a,b) = do
         r <- qinit_qubit False
         qnot_at r `controlled` x .==. 1 .&&. a .==. 1
         qnot_at r `controlled` x .==. 0 .&&. b .==. 1
         return r
  
  -- ----------------------------------------------------------------------
  -- * Operations of the Eq class
         
  -- | Lifted version of the '==' operator:
  -- 
  -- > (==) :: Eq a => a -> a -> Bool
  template_symb_equal_symb_equal_ :: (QEq qa) => Circ (qa -> Circ (qa -> Circ Qubit))
  template_symb_equal_symb_equal_ = return $ \qx -> return $ \qy -> do (qx,qy,test) <- q_is_equal qx qy; return test
  
  -- ----------------------------------------------------------------------
  -- * Generic unpacking
  
  -- $ The 'decToCircMonad' function produces (and also requires)
  -- functions with somewhat unwieldy types. We define generic functions
  -- for unpacking these types into a more useable format, and for
  -- packing them back.
  -- 
  -- For example, @'Circ' (qa -> 'Circ' (qb -> 'Circ' qd))@ unpacks
  -- into the type @qa -> qb -> 'Circ' qd@.
  -- 
  -- The class 'CircLiftingUnpack' keeps track of the unpacked and
  -- packed versions of types; so it will have an instance
  -- 
  -- > @'CircLiftingUnpack' ('Circ' (qa -> 'Circ' (qb -> 'Circ' qd))) (qa -> qb -> 'Circ' qd)@, 
  -- 
  -- and provide functions 'unpack', 'pack' going back and forth between
  -- these.
  -- 
  -- Note that 'pack' and 'unpack' do not in general form an
  -- isomorphism, just a retraction of the packed type onto the unpacked
  -- type.
  -- 
  -- Unfortunately the class cannot (in the current implementation) be
  -- defined in full generality once and for all: whenever a user wishes
  -- to use a new type @QFoo@ in circuit-building functions, she must
  -- define an additional base case @'CircLiftingUnpack' ('Circ' QFoo)
  -- ('Circ' QFoo)@ (with 'pack' and 'unpack' the identity) to use this
  -- class with types involving @QFoo@.
  -- 
  -- The crucial case is 
  -- 
  -- > instance ('CircLiftingUnpack' ('Circ' b) b') => 'CircLiftingUnpack' ('Circ' (a -> 'Circ' b)) (a -> b')@.
  -- 
  -- Unfortunately, this requires @-XUndecidableInstances@, for somewhat
  -- subtle reasons (see
  -- <http://hackage.haskell.org/trac/haskell-prime/wiki/FunctionalDependencies#Restrictionsoninstances>,
  -- <http://hackage.haskell.org/trac/haskell-prime/wiki/FunctionalDependencies#Modifiedcoveragecondition>).
  -- 
  -- The current implementation is fairly restricted, working
  -- essentially only for cases like the examples above.  One can define
  -- the unpacking more generally; but this restriction keeps the
  -- definition much simpler, and suffices for most (all?) of the
  -- circuit-generation functions we use.
  
  -- | The 'decToCircMonad' function produces (and also requires)
  -- functions with somewhat unwieldy types. The 'CircLiftingUnpack'
  -- class defines generic functions for unpacking these types into a
  -- more useable format, and for packing them back.
  -- 
  -- For example, @'Circ' (qa -> 'Circ' (qb -> 'Circ' qd))@ unpacks into
  -- the type @qa -> qb -> 'Circ' qd@.
  -- 
  -- Note that 'pack' and 'unpack' do not in general form an
  -- isomorphism, just a retraction of the packed type onto the unpacked
  -- type.
  class CircLiftingUnpack packed unpacked | packed -> unpacked, unpacked -> packed where
    unpack :: packed -> unpacked
    pack :: unpacked -> packed
  
  instance (CircLiftingUnpack (Circ b) b') => CircLiftingUnpack (Circ (a -> Circ b)) (a -> b') where
    unpack cf x = unpack $ do f <- cf; f x
    pack f = return $ \x -> pack (f x)
  
  instance CircLiftingUnpack (Circ Qubit) (Circ Qubit) where
    pack x = x
    unpack x = x
  
  instance CircLiftingUnpack (Circ [a]) (Circ [a]) where
    pack x = x
    unpack x = x
  
  instance CircLiftingUnpack (Circ ()) (Circ ()) where
    pack x = x
    unpack x = x
  
  instance CircLiftingUnpack (Circ (a,b)) (Circ (a,b)) where
    pack x = x
    unpack x = x
  
  instance CircLiftingUnpack (Circ (a,b,c)) (Circ (a,b,c)) where
    pack x = x
    unpack x = x
  
  instance CircLiftingUnpack (Circ (a,b,c,d)) (Circ (a,b,c,d)) where
    pack x = x
    unpack x = x
  
  instance CircLiftingUnpack (Circ (a,b,c,d,e)) (Circ (a,b,c,d,e)) where
    pack x = x
    unpack x = x
  
  instance CircLiftingUnpack (Circ (a,b,c,d,e,f)) (Circ (a,b,c,d,e,f)) where
    pack x = x
    unpack x = x
  
  instance CircLiftingUnpack (Circ (a,b,c,d,e,f,g)) (Circ (a,b,c,d,e,f,g)) where
    pack x = x
    unpack x = x
  