package Bug308 where

import ListN

type BaseData = Bit 5


getLarger :: (Add 1 a aa) =>
             Tuple2 (Bit a) BaseData ->
             Tuple2 (Bit a) BaseData ->
             Tuple2 (Bit aa) BaseData
getLarger in1 in2 =
    let theResult' =
            if tpl_2 in1 > tpl_2 in2 then
                let theResult' =
                        let outdata' :: BaseData
                            outdata' =  tpl_2 in1
                        in  let outdata :: BaseData
                                outdata =  outdata'
                            in  let currentIndex' :: Bit a
                                    currentIndex' =  tpl_1 in1
                                in  let currentIndex :: Bit a
                                        currentIndex =  currentIndex'
                                    in  let nextIndex' :: Bit aa
                                            nextIndex' =
                                                primConcat
                                                  (unpack (0b0::(Bit 1)))
                                                  currentIndex
                                        in  let nextIndex :: Bit aa
                                                nextIndex =  nextIndex'
                                            in  (currentIndex ,
                                                 (nextIndex , outdata))
                in  let (currentIndex , (nextIndex, outdata)) =  theResult'
                    in  (currentIndex , (nextIndex , outdata))
            else
                let theResult' =
                        let outdata' :: BaseData
                            outdata' =  tpl_2 in2
                        in  let outdata :: BaseData
                                outdata =  outdata'
                            in  let currentIndex' :: Bit a
                                    currentIndex' =  tpl_1 in2
                                in  let currentIndex :: Bit a
                                        currentIndex =  currentIndex'
                                    in  let nextIndex' :: Bit aa
                                            nextIndex' =
                                                Prelude.primConcat
                                                  (unpack (0b1::(Bit 1)))
                                                  currentIndex
                                        in  let nextIndex :: Bit aa
                                                nextIndex =  nextIndex'
                                            in  (currentIndex ,
                                                 (nextIndex , outdata))
                in  let (currentIndex, (nextIndex, outdata)) =  theResult'
                    in  (currentIndex , (nextIndex , outdata))
    in  let (currentIndex , (nextIndex, outdata)) =  theResult'
        in  tuple2 nextIndex outdata

getLarger1 :: (Add 1 a aa) => Tuple2 (Bit a) BaseData ->
                              Tuple2 (Bit aa) BaseData
getLarger1 in1 =  error "getLarger1 has been called"

maxpair :: (Div n 2 nn, Add 1 a aa) =>
           ListN n (Tuple2 (Bit a) BaseData) ->
           ListN nn (Tuple2 (Bit aa) BaseData)
maxpair in1 =  mapPairs getLarger getLarger1 in1