{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-} 
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE IncoherentInstances #-}

{-# LANGUAGE NoMonomorphismRestriction #-}



-- Full quantum lambda-calculus with named variables:
-- booleans, qbits, tests and pairing.

-- The class Judg now produce a map in the Kleisli category.

module FullQLCMonad where

import Data.Complex
import qualified Data.IntMap as IntMap
import QRAM

data Z = Z
data S a = S a

data False
data True

data Flag f a = Flag a


-- Make them showable
instance (Show a) => Show (Flag b a) where
  show (Flag a) = show a

instance Show (a -> b) where
  show (f) = "<fn>"


data Dup
data Sim

data Var x a = Var a

data Used a = Used a
data Free a = Free a

data Dummy = Dummy



-- Ordering on flags.

class FlagSubType a b
default (Sim)

instance FlagSubType a a
instance FlagSubType Dup a
instance FlagSubType a Sim
instance (Dup ~ a) => FlagSubType a Dup
instance (Sim ~ a) => FlagSubType Sim a
-- close overlapping cases
instance FlagSubType Dup Sim
instance FlagSubType Dup Dup
instance FlagSubType Sim Sim
instance (Dup ~ Sim) => FlagSubType Sim Dup



-- Ordering on types
-- There are two of them so that one can infer left and right hands.
-- Double functional dependencies do not do the job, for some reason.

class Monad m => TestSubType m a b | a -> b, b -> a where
   subType :: a -> m b

instance Monad m => TestSubType m Bool Bool where subType x = return x
instance Monad m => TestSubType m Qbit Qbit where subType x = return x

instance (Monad m, TestSubType m a b) => TestSubType m (m a) (m b) where
    subType x = x >>= (\y -> return (subType y))

instance (Monad m, TestSubType m a b, FlagSubType f f2) => 
               TestSubType m (Flag f a) (Flag f2 b) where
    subType (Flag x) = (subType x) >>= (\y -> return (Flag y))

instance (Monad m, TestSubType m c a, TestSubType m b d) => 
                  TestSubType m (a -> m b) (c -> m d) where
    subType f = return $ \x -> (subType x) >>= f >>= subType

instance (Monad m, StrongMonad m, TestSubType m a c, TestSubType m b d) => 
                  TestSubType m (a, b) (c, d) where
    subType (a,b) = strength (subType a) (subType b)



class AddVar x a c2 c1 | x a c1 -> c2 where
   add :: x -> a -> c2 -> c1

instance AddVar n a () () where
   add n a () = ()

instance a1 ~ a2 => AddVar Z a1 (Free b,c) (Free a2,c) where
   add Z a (Free b,c) = (Free a, c)

instance a1 ~ a2 => AddVar Z a1 (Free b,c) (Used a2,c) where
   add Z a (Free b,c) = (Used a, c)

instance (AddVar n a c d) => AddVar (S n) a (b,c) (b,d) where
   add (S n) a (b,c) = (b,add n a c)




class IsNotEq a b
instance IsNotEq Z (S n)
instance IsNotEq (S n) Z
instance IsNotEq m n => IsNotEq (S m) (S n)

class Add2Var x a y b c2 c1 | x a y b c1 -> c2 where
   add2 :: x -> a -> y -> b -> c2 -> c1

instance (IsNotEq m n) => Add2Var m a n b () () where
   add2 x a y b () = ()

instance (IsNotEq Z Z) => Add2Var Z a Z b c c where
   add2 x a y b c = c

instance (a1 ~ a2, AddVar m b c2 c1) => Add2Var Z a1 (S m) b (Free y, c2) (Free a2, c1) where
   add2 Z a (S y) b (Free dummy, c2) = (Free a, add y b c2)

instance (a1 ~ a2, AddVar m b c2 c1) => Add2Var (S m) b Z a1 (Free y, c2) (Free a2, c1) where
   add2 (S y) b Z a (Free dummy, c2) = (Free a, add y b c2)

instance (a1 ~ a2, AddVar m b c2 c1) => Add2Var Z a1 (S m) b (Free y, c2) (Used a2, c1) where
   add2 Z a (S y) b (Free dummy, c2) = (Used a, add y b c2)

instance (a1 ~ a2, AddVar m b c2 c1) => Add2Var (S m) b Z a1 (Free y, c2) (Used a2, c1) where
   add2 (S y) b Z a (Free dummy, c2) = (Used a, add y b c2)

instance (Add2Var n a m b c d) => Add2Var (S n) a (S m) b (y,c) (y,d) where
   add2 (S n) a (S m) b (y,c) = (y,add2 n a m b c)





class GetVar m x a c | x a -> c, a -> m  where
  get_var :: c -> x -> m a

instance TestSubType m a b => GetVar m Z b (Used a,()) where
  get_var (Used a,c) Z = subType a

instance GetVar m n a c => GetVar m (S n) a (Free u,c) where
  get_var (u,c) (S n) = get_var c n



class Zip c1 c2 c3 | c1 c2 -> c3 where
   split :: c3 -> (c1,c2)
instance Zip () c c where
   split c = ((),c)
instance Zip c () c where
   split c = (c,())
instance Zip () () () where
   split () = ((),())

instance (Zip c1 c2 c3, c ~ a, c ~ b) => Zip (Free a, c1) (Free b, c2) (Free c, c3) where
   split (Free c,c3) = let (c1,c2) = split c3 in ((Free c,c1),(Free c,c2))

instance (Zip c1 c2 c3, c ~ a, c ~ b) => Zip (Free a, c1) (Used b, c2) (Used c, c3) where
   split (Used c,c3) = let (c1,c2) = split c3 in ((Free c,c1),(Used c,c2))

instance (Zip c1 c2 c3, c ~ a, c ~ b) => Zip (Used a, c1) (Free b, c2) (Used c, c3) where
   split (Used c,c3) = let (c1,c2) = split c3 in ((Used c,c1),(Free c,c2))

instance (Zip c1 c2 c3, (Flag Dup d) ~ c, c ~ a, c ~ b) => Zip (Used a, c1) (Used b, c2) (Used c, c3) where
   split (Used c,c3) = let (c1,c2) = split c3 in ((Used c,c1),(Used c,c2))



class Match c1 c2 c3 | c1 c2 -> c3 where
   match :: c3 -> (c1,c2)
instance Match () c c where
   match c = ((),c)
instance Match c () c where
   match c = (c,())
instance Match () () () where
   match () = ((),())

instance (Match c1 c2 c3, c ~ a, c ~ b) => Match (Free a, c1) (Free b, c2) (Free c, c3) where
   match (Free c,c3) = let (c1,c2) = match c3 in ((Free c,c1),(Free c,c2))
instance (Match c1 c2 c3, c ~ a, c ~ b) => Match (Used a, c1) (Used b, c2) (Used c, c3) where
   match (Used c,c3) = let (c1,c2) = match c3 in ((Used c,c1),(Used c,c2))





-- If the context contains a Sim-flagged type at some ConsYes place,
-- then d is Sim. Otherwise, it is Dup

class TestCont1 cont d | cont -> d
instance TestCont1 () Dup
instance (TestCont1 c f) => TestCont1 (Used (Flag Dup a), c) f
instance                    TestCont1 (Used (Flag Sim a), c) Sim
instance (TestCont1 c f) => TestCont1 (Free a, c) f

-- This relation states that if we have Dup as result, then all the
-- flags are Dup. If we have Sim, we cannot get any other information.

class TestCont2 c f
instance TestCont2 () Dup
instance (TestCont2 c Dup, (Flag Dup a) ~ b) => TestCont2 (Used b, c) Dup
instance (TestCont2 c Dup) => TestCont2 (Free b, c) Dup
instance TestCont2 c Sim

class TestCont c d
instance (TestCont1 c d, TestCont2 c d) => TestCont c d



class Or1 e a x | e a -> x
instance Or1 e Dup Dup
instance Or1 Dup e Dup
instance Or1 Dup Dup Dup
instance Or1 Sim Sim Sim
instance (a ~ b) => Or1 Sim a b
instance (a ~ b) => Or1 a Sim b

class Or2 e a x | x -> e a
instance Or2 Sim Sim Sim
instance Or2 e a Dup

class Or e a x
instance (Or1 e a x, Or2 e a x) => Or e a x 




class Judg j m where
      lamb :: (AddVar x a c2 c1, TestCont c2 f1, FlagSubType f1 f) => 
                 x -> j m w c1 (m (Flag f' b)) -> j m (w,f,f1,f') c2 (m (Flag f (a -> (m (Flag f' b)))))
      appl :: Zip c1 c2 c3 => j m w1 c1 (m (Flag f ((Flag f'' a) -> m (Flag f' b)))) -> j m w2 c2 (m (Flag f'' a)) -> j m (w1,w2,f,f',f'',a) c3 (m (Flag f' b))
      var :: (GetVar m x a c) => x -> j m () c (m a)
      tt :: (TestSubType m (Flag Dup Bool) a) => j m a () (m a)
      ff :: (TestSubType m (Flag Dup Bool) a) => j m a () (m a)
      ifx :: (Match c21 c22 c2, Zip c1 c2 c3) => j m w1 c1 (m (Flag d Bool)) -> j m w2 c21 (m a) -> j m w3 c22 (m a) -> j m (w1,w2,w3,d) c3 (m a)
      new :: j m w c (m (Flag f Bool)) -> j m (w,f) c (m (Flag Sim Qbit))
      meas ::  j m w c (m (Flag f Qbit)) -> j m (w,f) c (m (Flag f' Bool))
      had :: j m w c (m (Flag f Qbit)) -> j m (w,f) c (m (Flag Sim Qbit))
      qnot :: j m w c (m (Flag f Qbit)) -> j m (w,f) c (m (Flag Sim Qbit))
      not2 :: j m w c (m (Flag f Qbit)) -> j m (w,f) c (m (Flag Sim Qbit))
      id2 :: j m w c (m (Flag f Qbit)) -> j m (w,f) c (m (Flag Sim Qbit))
      cnot :: j m w c (m (Flag f1 (Flag f2 Qbit, Flag f3 Qbit))) -> j m (w,f1,f2,f3) c (m (Flag Sim (Flag Sim Qbit, Flag Sim Qbit)))
      tens :: (Zip c1 c2 c3, Or e xa x, Or e yb y) =>
                 j m w1 c1 (m (Flag x a)) -> j m w2 c2 (m (Flag y b)) -> j m (w1,w2,x,y,e,xa,yb) c3 (m (Flag e (Flag xa a, Flag yb b)))


-- separating this one is necessary to expose the types x, a, y and b.

class JudgTens j m x a y b | j -> m where
      lambtens :: (TestCont c3 f1, FlagSubType f1 f, Add2Var n1 (Flag x a) n2 (Flag y b) c3 c1, Or e xa x, Or e yb y) => 
       n1 -> n2 -> j m w c1 (m d)  -> j m (w,f,f1,e,xa,a,yb,b) c3 (m (Flag f ((Flag e (Flag xa a, Flag yb b)) -> (m d))))

lettens x y m n = appl (lambtens x y n) m
letx x m n = appl (lamb x n) m



data J (m :: * -> *) w c a = J (c -> a)

instance (Monad m, StrongMonad m, QC m) => Judg J m where
      lamb x (J f) = J $ \c -> (return (Flag (\a -> f (add x a c))))
      appl (J f) (J g) = J $ \x -> let (x1,x2) = split x in 
                                   let h1 = f x1 in 
                                   let h2 = g x2 in
                                   let h3 = strength h1 h2 in    
                                   h3 >>= (\(Flag a, b) -> a b)
      var x = J $ \z -> get_var z x
      tt = J $ \x -> subType ((Flag True)::Flag Dup Bool)
      ff = J $ \x -> subType ((Flag False)::Flag Dup Bool)
      ifx (J b) (J m) (J n) = J (\x -> let (x1,x2) = split x in
                                       let (x21,x22) = match x2 in
                                       let bb = b x1 in
                                       let mm = m x21 in
                                       let nn = n x22 in
                                       bb >>= (\(Flag a) -> return a) 
                                          >>= (\b -> if b then mm else nn))
      new (J f)  = J $ \x -> f x >>= (\(Flag a) -> qc_new a) >>= (\a -> return (Flag a))
      meas (J f) = J $ \x -> qc_meas (f x >>= (\(Flag a) -> return a)) >>= (\a -> return (Flag a))
      had (J f)  = J $ \x -> qc_had (f x >>= (\(Flag a) -> return a)) >>= (\a -> return (Flag a))
      qnot (J f)  = J $ \x -> qc_NOT (f x >>= (\(Flag a) -> return a)) >>= (\a -> return (Flag a))
      not2 (J f)  = J $ \x -> qc_NOT2 (f x >>= (\(Flag a) -> return a)) >>= (\a -> return (Flag a))
      id2 (J f)  = J $ \x -> qc_Id2 (f x >>= (\(Flag a) -> return a)) >>= (\a -> return (Flag a))
      cnot (J f) = J $ \x -> qc_CNOT (f x >>= (\(Flag (Flag a, Flag b)) -> return (a,b))) >>= (\(a,b) -> return (Flag (Flag a, Flag b)))
      tens (J f) (J g) = J $ \x -> let (x1,x2) = split x in 
                                   strength (f x1) (g x2) >>= (\(Flag a,Flag b) -> return (Flag (Flag a, Flag b)))

instance (StrongMonad m) => JudgTens J m x a y b where
      lambtens n m (J f) = 
          J $ \c -> return $ Flag $ \(Flag (Flag a, Flag b)) -> f (add2 n ((Flag a)::Flag x a)
                                                                        m ((Flag b)::Flag y b) c)
                

data E w a = E a



instance Monad (E w) where
    return x  = E x
    (>>=) x f = f y where (E y) = x

instance Show a => Show (IO (E w a)) where
   show x = show ()

printE :: Show a => E w a -> IO (E w ())
printE (E x) = do
    putStrLn (show x)
    return $ E ()


class Eval m c a where
   eval :: (J m w c a) -> E w a

instance Eval m () a where
   eval (J f) = E (f ())

instance (Eval m c a, (Free Dummy) ~ b) => Eval m (b,c) a where
   eval (J f) = eval ((J (\c -> f (Free Dummy, c)))::(J m w c a))



setType :: E w a -> a -> E w a
setType x y = x

setJudg :: J m w c a -> c -> a -> J m w c a
setJudg x y z = x


-- ----------------------------------------------------------------------------
-- ----------------------------------------------------------------------------
-- Full study of the teleportation algorithm (version [Selinger-Valiron])
--

x = Z
y = S Z
z = S (S Z)
t = S (S (S Z))

epr = lamb x (cnot (tens (had (new ff)) (new ff)))

bellmeasure =
    lamb x (
    lamb y (
    lettens z t 
      (cnot (tens (var x)
                  (var y))) 
      (tens (meas (had (var z)))
            (meas (var t)))))

ucorrection = 
    lamb z (
    lambtens x y (
        ifx (var x) (ifx (var y) (not2 (var z)) (id2 (var z))) 
                    (ifx (var y) (qnot (var z)) (var z))))

telep =
  lettens x y (appl epr ff) (
  letx z (appl bellmeasure (var x)) (
  letx t (appl ucorrection (var y)) (
  (lamb x (appl (var t) (appl (var z) (var x)))))))

{- The type of telep is the same as in FullQLC, modulo the monad m.

:t eval telep
eval telep
  :: (Or2 Sim f f, Or2 f1 xa f8, Or2 f1 yb f7, Or1 f1 xa f8,
      Or1 f1 yb f7, QC m, StrongMonad m) =>
     E ... (m (Flag Sim (Flag f Qbit -> m (Flag Sim Qbit))))
-}


-- The type trace of the derivation of telep, from querying with ghci.

type TelepType m f f1 f2 f3 f4 f5 f6 f7 xa yb = 
    (((((((((),
    ((), (), Sim, f, Sim, Qbit), Sim, Sim, f, (Flag xa Bool, Flag yb Bool)), Sim, Sim, Sim), Sim,
    Sim, Sim), (((((), ((), ((), Sim), ((), Sim), f6), ((), ((), Sim), (), f6), f7), Sim, Sim, f,
    xa, Bool, yb, Bool), f5, Dup, Sim), (), f5, Sim, Sim, Qbit), Sim, Sim,  Sim,
    Flag f (Flag xa Bool, Flag yb Bool) -> m (Flag Sim Qbit)), Sim, Sim, Sim),
    (((((((((), Sim), Sim), ((), Sim), f7, f6, f, xa, yb), f4, Dup, Sim, Sim, Qbit, Sim, Qbit),
    (((), (), Sim, Sim, Sim, Sim, Sim), Sim, Sim, Sim), f4, f, Sim, (Flag Sim Qbit, Flag Sim Qbit)),
    Sim, Sim, f), f3, Dup, Sim), (), f3, Sim, Sim, Qbit), Sim, Sim, Sim,
    Flag Sim Qbit -> m (Flag f (Flag xa Bool, Flag yb Bool))), f1, Dup, Sim, Sim, Qbit, Sim, Qbit),
    ((((((Flag Dup Bool, Dup), Sim), (Flag Dup Bool, Dup), Sim, Sim, Sim, Sim, Sim), Sim, Sim, Sim), f2,
    Dup, Sim), Flag Dup Bool, f2, Sim, Dup, Bool), f1, Sim, Sim, (Flag Sim Qbit, Flag Sim Qbit))


-- ----------------------------------------------------------------------------
-- Using telep with PQM
--

-- first, a auxiliary tool

feedQbit :: (QC m, Monad m) => Bool -> m (Flag Sim (Flag Sim Qbit -> m (Flag Sim Qbit))) -> m (Flag Sim Qbit)
feedQbit b f = do 
     Flag f' <- f
     q <- qc_new b
     f' (Flag q)

type PQM_id_qbit = PQM (Flag Sim (Flag Sim Qbit -> PQM (Flag Sim Qbit))) 


-- The function that uses telep to teleport a quantum bit in a
-- state |False> or |True>

-- We get rid of the constraints by setting the open types to
-- default values, so that the function does not have dangling
-- constraints. 

telepPQM :: (f ~ Sim, yb ~ Sim, f6 ~ Sim, xa ~ Sim, f7 ~ Sim,
         Or2 f yb f6, Or2 f xa f7, Or1 f yb f6, Or1 f xa f7)
        =>
        Bool -> E (TelepType PQM f f1 f2 f3 f4 f5 f6 f7 xa yb) (PQM (Flag Sim Qbit))
telepPQM b = do
   f <- setType (eval telep) (undefined :: PQM_id_qbit)
   return $ feedQbit b f

-- Output the result of the computation.  Note that the absence of
-- dangling constraints is crucial for the execution of the code, if
-- we were to call this function. This should be taken care
-- automatically by the compiler....

printPQM b = printE $ telepPQM b



{- Let's use the map telep. If we feed it |False>:

*> printPQM False

we get

[([0.4999999999999999 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,(-0.0) :+ 0.0],Qbit 2),
  ([0.0 :+ 0.0,0.4999999999999999 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0],Qbit 2),
  ([0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.4999999999999999 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0],Qbit 2),
  ([0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.4999999999999999 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0],Qbit 2)]

The answer is always qbit 2 in the state
prob .25 : |000>
prob .25 : |001>
prob .25 : |100>
prob .25 : |101>
that is, effectively |False>.

Feeding it |True> instead:

*> printPQM False

we get

[([0.0 :+ 0.0,0.0 :+ 0.0,0.4999999999999999 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,(-0.0) :+ 0.0,0.0 :+ 0.0],Qbit 2),
 ([0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.4999999999999999 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0],Qbit 2),
 ([0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.4999999999999999 :+ 0.0,0.0 :+ 0.0],Qbit 2),
 ([0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.0 :+ 0.0,0.4999999999999999 :+ 0.0],Qbit 2)]

Again, the answer is qbit 2 in the state
prob .25 : |010>
prob .25 : |011>
prob .25 : |110>
prob .25 : |111>
that is, effectively |True>.

-}






-- ----------------------------------------------------------------------------
-- Using telep with PQMStrict
--


-- We do the same construction as for PQM.

type PQMS_id_qbit = PQMStrict (Flag Sim (Flag Sim Qbit -> PQMStrict (Flag Sim Qbit))) 

telepPQMS :: (f ~ Sim, yb ~ Sim, f6 ~ Sim, xa ~ Sim, f7 ~ Sim,
         Or2 f yb f6, Or2 f xa f7, Or1 f yb f6, Or1 f xa f7)
        =>
        Bool -> E (TelepType PQMStrict f f1 f2 f3 f4 f5 f6 f7 xa yb) (PQMStrict (Flag Sim Qbit))
telepPQMS b = do
   f <- setType (eval telep) (undefined :: PQMS_id_qbit)
   return $ feedQbit b f

printPQMS b = printE $ telepPQMS b



{-
Let's use telep with this new monad. If we feed it |False>:

*> printPQMS False

since in the state monad PQMStrict measured quantum bits are erased, we get the smaller term

[((3,[0.4999999999999999 :+ 0.0,0.0 :+ 0.0],fromList [(2,1)]),Qbit 2),
 ((3,[0.4999999999999999 :+ 0.0,0.0 :+ 0.0],fromList [(2,1)]),Qbit 2),
 ((3,[0.4999999999999999 :+ 0.0,0.0 :+ 0.0],fromList [(2,1)]),Qbit 2),
 ((3,[0.4999999999999999 :+ 0.0,0.0 :+ 0.0],fromList [(2,1)]),Qbit 2)]

One can easily check that all four possibilities provides the same answer |False>.

Feeding it |True> instead:

*> printPQMS True

we get

[((3,[0.0 :+ 0.0,0.4999999999999999 :+ 0.0],fromList [(2,1)]),Qbit 2),
 ((3,[0.0 :+ 0.0,0.4999999999999999 :+ 0.0],fromList [(2,1)]),Qbit 2),
 ((3,[0.0 :+ 0.0,0.4999999999999999 :+ 0.0],fromList [(2,1)]),Qbit 2),
 ((3,[0.0 :+ 0.0,0.4999999999999999 :+ 0.0],fromList [(2,1)]),Qbit 2)]

and again, the answer is easily read as being |True>

-}




-- ----------------------------------------------------------------------------
-- Using telep with FakeQM
--


-- We do the same construction as for PQM.

type FQM_id_qbit = FakeQM (Flag Sim (Flag Sim Qbit -> FakeQM (Flag Sim Qbit))) 

telepFQM :: (f ~ Sim, yb ~ Sim, f6 ~ Sim, xa ~ Sim, f7 ~ Sim,
         Or2 f yb f6, Or2 f xa f7, Or1 f yb f6, Or1 f xa f7)
        =>
        Bool -> E (TelepType FakeQM f f1 f2 f3 f4 f5 f6 f7 xa yb) (FakeQM (Flag Sim Qbit))
telepFQM b = do
   f <- setType (eval telep) (undefined :: FQM_id_qbit)
   return $ feedQbit b f

printFQM b = printE $ telepFQM b

{- the call to printQPM outputs all the possible execution trace in a
   raw format. We recover four possibilities, i.e. the four possible
   states (Bool,Bool). They are all equal apart from the last command,
   that is, the correction u.

*>  printFQM True
New False
Had
New False
CNOT
New True
CNOT
Had
meas True
meas True
NOT2

New False
Had
New False
CNOT
New True
CNOT
Had
meas True
meas False
Id2

New False
Had
New False
CNOT
New True
CNOT
Had
meas False
meas True
NOT

New False
Had
New False
CNOT
New True
CNOT
Had
meas False
meas False

-}