-- | 
-- 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://github.com/leepike/copilot-discussion/blob/master/tutorial/copilot_tutorial.pdf An Introduction to Copilot> in
-- <https://github.com/leepike/copilot-discussion copilot-discussion> explains
-- 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/VotingExamples.hs@ in the
-- <https://github.com/leepike/Copilot/tree/master/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 :: [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' :: [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'   = 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 :: [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 (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' :: 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