{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
{-# LINE 1 "Quipper/Algorithms/CL/RegulatorTemplate.hs" #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}

-- | An experimental adaptation of the code from "Quipper.Algorithms.CL.Types", "Quipper.Algorithms.CL.Math", etc. to build circuits automatically using Template Haskell and "Quipper.Internal.CircLifting".
--
-- Extremely incomplete.

module Quipper.Algorithms.CL.RegulatorTemplate where

import Quipper
import Text.Printf
import Quipper.Libraries.FPReal
import Quipper.Algorithms.CL.Types
import Quipper.Libraries.Arith
import Control.Monad

-- * Auxiliary functions specific to the Class Number algorithm

d_of_ideal :: Ideal -> Integer
d_of_ideal (Ideal bigD m l a b) = d_of_bigD bigD

d_of_idealQ :: IdealQ -> Integer
d_of_idealQ (Ideal bigD m l a b) = d_of_bigD bigD

equal_d_of_ideals :: Ideal -> Ideal -> BoolParam
equal_d_of_ideals i j = if ((d_of_ideal i) == (d_of_ideal j)) then PTrue else PFalse

equal_d_of_idealQs :: IdealQ -> IdealQ -> BoolParam
equal_d_of_idealQs i j = if ((d_of_idealQ i) == (d_of_idealQ j)) then PTrue else PFalse

template_equal_d_of_ideals :: Circ (IdealQ -> Circ (IdealQ -> Circ BoolParam))
template_equal_d_of_ideals = return $ \i -> return $ \j -> return (equal_d_of_idealQs i j)

template_and :: Circ ([Qubit] -> Circ Qubit)
template_and = return $ \qs -> do
  result_qubit <- qinit False
  qnot result_qubit `controlled` qs

m_of_ideal :: Ideal -> IntM
m_of_ideal (Ideal bigD m l a b) = m

l_of_ideal :: Ideal -> IntM
l_of_ideal (Ideal bigD m l a b) = l

a_of_ideal :: Ideal -> IntM
a_of_ideal (Ideal bigD m l a b) = a

b_of_ideal :: Ideal -> IntM
b_of_ideal (Ideal bigD m l a b) = b

template_m_of_ideal :: Circ (IdealQ -> Circ QDInt)
template_m_of_ideal = return $ \(Ideal bigD m l a b) -> return m 

template_l_of_ideal :: Circ (IdealQ -> Circ QDInt)
template_l_of_ideal = return $ \(Ideal bigD m l a b) -> return l 

template_a_of_ideal :: Circ (IdealQ -> Circ QDInt)
template_a_of_ideal = return $ \(Ideal bigD m l a b) -> return a 

template_b_of_ideal :: Circ (IdealQ -> Circ QDInt)
template_b_of_ideal = return $ \(Ideal bigD m l a b) -> return b

one_of_size :: IntM -> IntM
one_of_size n = 
  case intm_length n of
    Just m -> intm m 1
    Nothing -> error "one_of_size: indeterminate size"

template_one_of_size :: Circ (QDInt -> Circ QDInt)
template_one_of_size = return (\qx -> qinit $ one_of_size $ qc_false qx)

-- * Functions from "Quipper.Algorithms.CL.Types"

-- | Return 'True' if the given ideal is reduced.

isReduced :: Ideal -> Bool
isReduced i = (m_of_ideal i == (one_of_size (m_of_ideal i)) && (l_of_ideal i == a_of_ideal i))


{-# LINE 83 "Quipper/Algorithms/CL/RegulatorTemplate.hs" #-}
$( decToCircMonad [d| isReduced :: Ideal -> Bool
                      isReduced i = (m_of_ideal i == (one_of_size (m_of_ideal i)) && (l_of_ideal i == a_of_ideal i))
                      
                      
 |] ) 
{-# LINE 84 "Quipper/Algorithms/CL/RegulatorTemplate.hs" #-}
-- assertReduced can't really be implemented as a quantum circuit. The closest we could
-- define is an asserted termination, that would throw an error at circuit run-time if
-- the assertion doesn't hold.
-- | An assert function will throw an error if the assertion is False.
assert :: Bool -> a -> a
assert True a = a
assert False _ = error "False Assertion"
 
-- | A hand-lifted version of assert, that will produce a circuit run-time error
-- if the assertion doesn't hold. This is done by using an asserted discard.
template_assert :: Circ (Qubit -> Circ (a -> Circ a))
template_assert = return $ \assertion -> return $ \a -> do
  qterm True assertion
  return a

-- | This will throw an error if the given ideal isn't reduced. 
-- The corresponding circuit will use an asserted termination, that will throw an 
-- error at circuit run-time if the assertion doesn't hold.

assertReduced :: Ideal -> a -> a
assertReduced i rest = 
  let assertion = isReduced i in
  assert assertion rest 


{-# LINE 107 "Quipper/Algorithms/CL/RegulatorTemplate.hs" #-}
$( decToCircMonad [d| assertReduced :: Ideal -> a -> a
                      assertReduced i rest = 
                        let assertion = isReduced i in
                        assert assertion rest 
                      
                      
 |] ) 
{-# LINE 108 "Quipper/Algorithms/CL/RegulatorTemplate.hs" #-}
-- | Check if a given ideal equals another ideal.

idealEquals :: Ideal -> Ideal -> Bool
idealEquals i j = case equal_d_of_ideals i j of
  PFalse -> error "Comparing two ideals of different d"
  PTrue -> and [(m_of_ideal i == m_of_ideal j),
                (l_of_ideal i == l_of_ideal j),
                (a_of_ideal i == a_of_ideal j),
                (b_of_ideal i == b_of_ideal j)]


{-# LINE 117 "Quipper/Algorithms/CL/RegulatorTemplate.hs" #-}
$( decToCircMonad [d| idealEquals :: Ideal -> Ideal -> Bool
                      idealEquals i j = case equal_d_of_ideals i j of
                        PFalse -> error "Comparing two ideals of different d"
                        PTrue -> and [(m_of_ideal i == m_of_ideal j),
                                      (l_of_ideal i == l_of_ideal j),
                                      (a_of_ideal i == a_of_ideal j),
                                      (b_of_ideal i == b_of_ideal j)]
                      
                      
 |] ) 
{-# LINE 118 "Quipper/Algorithms/CL/RegulatorTemplate.hs" #-}
-- * Functions from "Quipper.Algorithms.CL.CL"

-- * Some dummy functions for testing

data BoolPair = BoolPair Bool Bool

data QubitPair = QubitPair Qubit Qubit

boolPair = BoolPair
template_boolPair = return $ \x -> return $ \y -> return $ QubitPair x y
template_BoolPair = QubitPair


truePair :: BoolPair
truePair = boolPair True True


{-# LINE 133 "Quipper/Algorithms/CL/RegulatorTemplate.hs" #-}
$( decToCircMonad [d| truePair :: BoolPair
                      truePair = boolPair True True
                      
                      
 |] ) 
{-# LINE 134 "Quipper/Algorithms/CL/RegulatorTemplate.hs" #-}
{-

myAnd :: BoolPair -> Bool
myAnd (BoolPair x y) = x && y

{-# LINE 137 "Quipper/Algorithms/CL/RegulatorTemplate.hs" #-}
$( decToCircMonad [d| myAnd :: BoolPair -> Bool
                      myAnd (BoolPair x y) = x && y
                      
 |] ) 
{-# LINE 138 "Quipper/Algorithms/CL/RegulatorTemplate.hs" #-}
-}


myPlus :: Int -> Int -> Int
myPlus x y = x + y


{-# LINE 143 "Quipper/Algorithms/CL/RegulatorTemplate.hs" #-}
$( decToCircMonad [d| myPlus :: Int -> Int -> Int
                      myPlus x y = x + y
                      
                      
 |] ) 
{-# LINE 144 "Quipper/Algorithms/CL/RegulatorTemplate.hs" #-}
-- * Some test functions
test_is_reduced :: IO ()
test_is_reduced = let zero = qdint_shape 4
                      ideal = Ideal 17 zero zero zero zero
                  in print_generic ASCII (unpack template_isReduced) ideal

-- * A main function
main :: IO ()
main = test_is_reduced

{-
Notes:

- it’s not quite clear to me what assumptions CircLifting makes about lingering arguments, linearity, etc. e.g.: should 'template_m_of_ideal' and the like return copies of the components, not the components themselves?  Or is this kosher as currently written? 

- I guess at the moment, it *does* assume all input arguments are left lingering, and moreover unmodified (in the sense of the computational basis).  A version not assuming this could be written by using the alternate type translation

#(a -> b) = a -> Circ (a,#b)

- linearity is much more of an issue!  if we write something like 


twice x = x + x


{-# LINE 167 "Quipper/Algorithms/CL/RegulatorTemplate.hs" #-}
$( decToCircMonad [d| twice x = x + x
                      
                      
 |] ) 
{-# LINE 168 "Quipper/Algorithms/CL/RegulatorTemplate.hs" #-}
this may well (depending on implementation of 'template_symb_plus_') build to a non-linear circuit (so, runtime error).  With a little more effort we can write examples which will *not* produce runtime errors, but *will* produce incorrect circuit behaviour.

Solution?  One can imagine writing safe circuits like

add_safe qx qy = if (qd_disjoint qx qy) then add qx qy
  else do
    ((qx,qy),qz) <- with_computed_fun (qx,qy)
      (\(qx,qy) -> do
        (qx,qx') <- qc_copy_fun qx
        (qy,qy') <- qc_copy_fun qy
        return (qx,qy,qx',qy'))
      (\(qx,qy,qx',qy') -> 
        (qx',qy',qz) <- add qx' qy'
        return ((qx,qy,qx',qy'),qz))
    return (qx,qy,qz)

One can even imagine doing this generically, so that add_safe = make_safe q_add.  The necessary assumption is just, I think, that q_add leaves qx, qy unmodified.  Given a QData method qd_disjoint, this would not I think be hard.

This may be the wrong solution to the problem, though.  Thoughts?

- It would be really nice if the lifting could deal better with (a) pattern-matching; (b) numeric literals.  (e.g. how to write an algebraic operation like (p x = 17*x + 5)?  Can write this for 'IntM', but can’t translate it correctly.

-}