    -- |
    -- Module: Voting
    -- Description: Implementation of the Boyer-Moore Majority Vote Algorithm
    -- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.
    --
    -- This is an implementation of the Boyer-Moore Majority Vote Algorithm for
    -- Copilot, which solves the majority vote problem in linear time and constant
    -- memory in two passes. 'majority' implements the first pass, and 'aMajority'
    -- the second pass. For details of the Boyer-Moore Majority Vote Algorithm see
    -- the following papers:
    --
    -- * <http://www.cs.rug.nl/~wim/pub/whh348.pdf Wim H. Hesselink, \"The Boyer-Moore Majority Vote Algorithm\", 2005>
    --
    -- * <ftp://net9.cs.utexas.edu/pub/techreports/tr81-32.pdf Robert S. Boyer and J Strother Moore, \"MJRTY - A Fast Majority Vote Algorithm\", 1981>
    --
    -- In addition, <https://copilot-language.github.io/downloads/copilot_tutorial.pdf An Introduction to Copilot> and
    -- <https://github.com/Copilot-Language/copilot-discussion copilot-discussion> explain
    -- a form of this code in section 4.
    --
    -- For instance, with four streams passed to 'majority', and the candidate stream
    -- then passed to 'aMajority':
    --
    -- @
    -- vote1:       vote2:       vote3:       vote4:       majority:    aMajority:
    -- 0            0            0            0            0            true
    -- 1            0            0            0            0            true
    -- 1            1            0            0            1            false
    -- 1            1            1            0            1            true
    -- 1            1            1            1            1            true
    -- @
    --
    -- For other examples, see @examples/Voting.hs@ in the
    -- <https://github.com/Copilot-Language/copilot/blob/master/copilot/examples/ Copilot repository>.

    {-# LANGUAGE RebindableSyntax #-}

    module Copilot.Library.Voting
      ( majority, aMajority ) where

    import Copilot.Language
    import qualified Prelude as P

    -- | Majority vote first pass: choosing a candidate.
    majority :: (P.Eq a, Typed a) =>
                [Stream a] -- ^ Vote streams
                -> Stream a -- ^ Candidate stream
    majority :: forall a. (Eq a, Typed a) => [Stream a] -> Stream a
    majority []     = String -> Stream a
    forall a. String -> a
    badUsage String
    "majority: empty list not allowed"
    majority (Stream a
    x:[Stream a]
    xs) = [Stream a] -> Stream a -> Stream Word32 -> Stream a
    forall a.
    (Eq a, Typed a) =>
    [Stream a] -> Stream a -> Stream Word32 -> Stream a
    majority' [Stream a]
    xs Stream a
    x Stream Word32
    1

    -- Alternate syntax of local bindings.
    majority' :: (P.Eq a, Typed a)
       => [Stream a] -> Stream a -> Stream Word32 -> Stream a
    majority' :: forall a.
    (Eq a, Typed a) =>
    [Stream a] -> Stream a -> Stream Word32 -> Stream a
    majority' []     Stream a
    can Stream Word32
    _   = Stream a
    can
    majority' (Stream a
    x:[Stream a]
    xs) Stream a
    can Stream Word32
    cnt =
      Stream Bool -> (Stream Bool -> Stream a) -> Stream a
    forall a b.
    (Typed a, Typed b) =>
    Stream a -> (Stream a -> Stream b) -> Stream b
    local (Stream Word32
    cnt Stream Word32 -> Stream Word32 -> Stream Bool
    forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
    == Stream Word32
    0) Stream Bool -> Stream a
    inZero
      where
      inZero :: Stream Bool -> Stream a
    inZero Stream Bool
    zero    = Stream a -> (Stream a -> Stream a) -> Stream a
    forall a b.
    (Typed a, Typed b) =>
    Stream a -> (Stream a -> Stream b) -> Stream b
    local (if Stream Bool
    zero then Stream a
    x else Stream a
    can) Stream a -> Stream a
    inCan
        where
        inCan :: Stream a -> Stream a
    inCan Stream a
    can' =
            -- We include a special case for when `xs` is empty that immediately
            -- returns `can'`. We could omit this special case without changing the
            -- final result, but this has the downside that `local` would bind a
            -- local variable that would go unused in `inCnt`. (Note that `inCnt`
            -- recursively invokes `majority'`, which doesn't use its last argument
            -- if the list of vote streams is empty.) These unused local variables
            -- would result in C code that triggers compiler warnings.
            case [Stream a]
    xs of
              [] -> Stream a
    can'
              [Stream a]
    _  -> Stream Word32 -> (Stream Word32 -> Stream a) -> Stream a
    forall a b.
    (Typed a, Typed b) =>
    Stream a -> (Stream a -> Stream b) -> Stream b
    local (if Stream Bool
    zero Stream Bool -> Stream Bool -> Stream Bool
    || Stream a
    x Stream a -> Stream a -> Stream Bool
    forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
    == Stream a
    can then Stream Word32
    cntStream Word32 -> Stream Word32 -> Stream Word32
    forall a. Num a => a -> a -> a
    +Stream Word32
    1 else Stream Word32
    cntStream Word32 -> Stream Word32 -> Stream Word32
    forall a. Num a => a -> a -> a
    -Stream Word32
    1) Stream Word32 -> Stream a
    inCnt
          where
          inCnt :: Stream Word32 -> Stream a
    inCnt Stream Word32
    cnt' = [Stream a] -> Stream a -> Stream Word32 -> Stream a
    forall a.
    (Eq a, Typed a) =>
    [Stream a] -> Stream a -> Stream Word32 -> Stream a
    majority' [Stream a]
    xs Stream a
    can' Stream Word32
    cnt'

    -- | Majority vote second pass: checking that a candidate indeed has more than
    -- half the votes.
    aMajority :: (P.Eq a, Typed a) =>
                 [Stream a] -- ^ Vote streams
                 -> Stream a -- ^ Candidate stream
                 -> Stream Bool -- ^ True if candidate holds majority
    aMajority :: forall a. (Eq a, Typed a) => [Stream a] -> Stream a -> Stream Bool
    aMajority [] Stream a
    _ = String -> Stream Bool
    forall a. String -> a
    badUsage String
    "aMajority: empty list not allowed"
    aMajority [Stream a]
    xs Stream a
    can =
      let
        cnt :: Stream Word32
    cnt = Stream Word32 -> [Stream a] -> Stream a -> Stream Word32
    forall a.
    (Eq a, Typed a) =>
    Stream Word32 -> [Stream a] -> Stream a -> Stream Word32
    aMajority' Stream Word32
    0 [Stream a]
    xs Stream a
    can
      in
        (Stream Word32
    cnt Stream Word32 -> Stream Word32 -> Stream Word32
    forall a. Num a => a -> a -> a
    * Stream Word32
    2) Stream Word32 -> Stream Word32 -> Stream Bool
    forall a. (Ord a, Typed a) => Stream a -> Stream a -> Stream Bool
    > Int -> Stream Word32
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral ([Stream a] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Stream a]
    xs)

    aMajority' :: (P.Eq a, Typed a)
      => Stream Word32 -> [Stream a] -> Stream a -> Stream Word32
    aMajority' :: forall a.
    (Eq a, Typed a) =>
    Stream Word32 -> [Stream a] -> Stream a -> Stream Word32
    aMajority' Stream Word32
    cnt []     Stream a
    _   = Stream Word32
    cnt
    aMajority' Stream Word32
    cnt (Stream a
    x:[Stream a]
    xs) Stream a
    can =
      Stream Word32 -> (Stream Word32 -> Stream Word32) -> Stream Word32
    forall a b.
    (Typed a, Typed b) =>
    Stream a -> (Stream a -> Stream b) -> Stream b
    local (if Stream a
    x Stream a -> Stream a -> Stream Bool
    forall a. (Eq a, Typed a) => Stream a -> Stream a -> Stream Bool
    == Stream a
    can then Stream Word32
    cntStream Word32 -> Stream Word32 -> Stream Word32
    forall a. Num a => a -> a -> a
    +Stream Word32
    1 else Stream Word32
    cnt) ((Stream Word32 -> Stream Word32) -> Stream Word32)
    -> (Stream Word32 -> Stream Word32) -> Stream Word32
    forall a b. (a -> b) -> a -> b
    $ \ Stream Word32
    cnt' ->
        Stream Word32 -> [Stream a] -> Stream a -> Stream Word32
    forall a.
    (Eq a, Typed a) =>
    Stream Word32 -> [Stream a] -> Stream a -> Stream Word32
    aMajority' Stream Word32
    cnt' [Stream a]
    xs Stream a
    can