copilot-libraries (empty) → 0.1
raw patch · 11 files changed
+945/−0 lines, 11 filesdep +arraydep +basedep +containerssetup-changed
Dependencies added: array, base, containers, copilot-language, mtl, parsec
Files
- LICENSE +29/−0
- Setup.hs +2/−0
- copilot-libraries.cabal +49/−0
- src/Copilot/Library/Clocks.hs +73/−0
- src/Copilot/Library/LTL.hs +81/−0
- src/Copilot/Library/PTLTL.hs +39/−0
- src/Copilot/Library/RegExp.hs +402/−0
- src/Copilot/Library/Stacks.hs +71/−0
- src/Copilot/Library/Statistics.hs +37/−0
- src/Copilot/Library/Utils.hs +107/−0
- src/Copilot/Library/Voting.hs +55/−0
+ LICENSE view
@@ -0,0 +1,29 @@+2009+BSD3 License terms++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++Redistributions of source code must retain the above copyright+notice, this list of conditions and the following disclaimer.++Redistributions in binary form must reproduce the above copyright+notice, this list of conditions and the following disclaimer in the+documentation and/or other materials provided with the distribution.++Neither the name of the developers nor the names of its contributors+may be used to endorse or promote products derived from this software+without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ copilot-libraries.cabal view
@@ -0,0 +1,49 @@+cabal-version: >=1.10+name: copilot-libraries+version: 0.1+synopsis: A Haskell-embedded DSL for monitoring hard real-time+ distributed systems.+description: Libraries for the Copilot language+license: BSD3+license-file: LICENSE+author: Lee Pike, Robin Morisset, Alwyn Goodloe, Sebastian Niller,+ Nis Nordby Wegmann+maintainer: niswegmann@gmail.com+stability: Experimental+category: Language, Embedded+build-type: Simple++source-repository head+ type: git+ location: git://github.com/niswegmann/copilot-libraries.git++library+ default-language: Haskell2010++ hs-source-dirs: src++ build-depends:+ array,+ base >= 4.0 && < 5,+ containers,+ copilot-language,+ parsec >= 2.0,+ mtl >= 2.0++ exposed-modules:+ Copilot.Library.Clocks+ Copilot.Library.LTL+ Copilot.Library.PTLTL+ Copilot.Library.Statistics+ Copilot.Library.RegExp+ Copilot.Library.Utils+ Copilot.Library.Voting+ Copilot.Library.Stacks++ other-modules:++ ghc-options:+ -fwarn-tabs+ -auto-all+ -caf-all+ -Wall
+ src/Copilot/Library/Clocks.hs view
@@ -0,0 +1,73 @@+-- | A library that generates new clocks based on a base period.+-- Usage, supposing @v@ is a Copilot variable, then+-- @+-- clk ( period 3 ) ( phase 1 )+-- @+-- is equivalent to a stream of values like:+-- @+-- cycle [False, True, False]+-- @+-- that generates a stream of values+-- @+-- False True False False True False False True False ...+-- 0 1 2 3 4 5 6 7 8+-- @+-- That is true every 3 ticks (the period) starting on the 1st tick (the phase).+-- Constraints:+-- The period must be greater than 0.+-- The phase must be greater than or equal to 0.+-- The phase must be less than the period.+++module Copilot.Library.Clocks+ ( clk, clk1, period, phase ) where++import Prelude ( Integral, fromIntegral, ($))+import qualified Prelude as P+import Copilot.Language+import Data.Bool+import Data.List (replicate)++data ( Integral a ) => Period a = Period a+data ( Integral a ) => Phase a = Phase a++period :: ( Integral a ) => a -> Period a+period = Period++phase :: ( Integral a ) => a -> Phase a+phase = Phase++-- clk generates a clock that counts n ticks by using an array of size n+clk :: ( Integral a ) => Period a -> Phase a -> Stream Bool+clk ( Period period' ) ( Phase phase' ) = clk'+ where clk' = if period' P.< 1 then+ badUsage ( "clk: clock period must be 1 or greater" )+ else if phase' P.< 0 then+ badUsage ( "clk: clock phase must be 0 or greater" )+ else if phase' P.>= period' then+ badUsage ( "clk: clock phase must be less than period")+ else replicate ( fromIntegral phase' ) False+ P.++ True : replicate+ ( fromIntegral+ $ period' P.- phase' P.- 1 ) False+ ++ clk'+++-- clk1 generates a clock that counts n ticks by using a+-- counter variable of integral type a+clk1 :: ( Integral a, Typed a )+ => Period a -> Phase a -> Stream Bool+clk1 ( Period period' ) ( Phase phase' ) =+ if period' P.< 1 then+ badUsage ( "clk1: clock period must be 1 or greater" )+ else if phase' P.< 0 then+ badUsage ( "clk1: clock phase must be 0 or greater" )+ else if phase' P.>= period' then+ badUsage ( "clk1: clock phase must be less than period")+ else+ let counter = [ P.fromInteger 0 ]+ ++ mux ( counter /= ( constant $ + period' P.- 1 ) )+ ( counter P.+ 1 )+ ( 0 )+ in counter == fromIntegral phase'
+ src/Copilot/Library/LTL.hs view
@@ -0,0 +1,81 @@+-- | Bounded Linear Temporal Logic (LTL) operators. For a bound @n@, a property+-- @p@ holds if it holds on the next @n@ transitions (between periods). If+-- @n == 0@, then the trace includes only the current period. For example,+-- @+-- eventually 3 p+-- @+-- holds if @p@ holds at least once every four periods (3 transitions).+--+-- Interface: see Examples/LTLExamples.hs You can embed an LTL specification+-- within a Copilot specification using the form:+-- @+-- operator spec+-- @+--+-- For some properties, stream dependencies may not allow their specification.+-- In particular, you cannot determine the "future" value of an external+-- variable. In general, the ptLTL library is probaby more useful.++{-# LANGUAGE NoImplicitPrelude #-}++module Copilot.Library.LTL+ ( next, eventually, always, until, release ) where++import Copilot.Language+import Copilot.Language.Prelude+import Copilot.Library.Utils+++-- | Property @s@ holds at the next period. For example:+-- @+-- 0 1 2 3 4 5 6 7+-- s => F F F T F F T F ...+-- next s => F F T F F T F ...+-- @+-- Note: s must have sufficient history to drop a value from it.+next :: Stream Bool -> Stream Bool+next = drop ( 1 :: Int )+++-- | Property @s@ holds for the next @n@ periods. We require @n >= 0@. If @n ==+-- 0@, then @s@ holds in the current period. E.g., if @p = always 2 s@, then we+-- have the following relationship between the streams generated:+-- @+-- 0 1 2 3 4 5 6 7+-- s => T T T F T T T T ...+-- p => T F F F T T ...+-- @+always :: ( Integral a ) => a -> Stream Bool -> Stream Bool+always n = nfoldl1 ( fromIntegral n + 1 ) (&&)+++-- | Property @s@ holds at some period in the next @n@ periods. If @n == 0@,+-- then @s@ holds in the current period. We require @n >= 0@. E.g., if @p =+-- eventually 2 s@, then we have the following relationship between the streams+-- generated:+-- @+-- s => F F F T F F F T ...+-- p => F T T T F T T T ...+-- @+eventually :: ( Integral a ) => a -> Stream Bool -> Stream Bool+eventually n = nfoldl1 ( fromIntegral n + 1 ) (||)+++-- | @until n s0 s1@ means that @eventually n s1@, and up until at least the+-- period before @s1@ holds, @s0@ continuously holds.+until :: ( Integral a ) => a -> Stream Bool -> Stream Bool -> Stream Bool+until n s0 s1 = foldl1 (||) v0+ where n' = fromIntegral n+ v0 = [ always ( i :: Int ) s0 && drop ( i + 1 ) s1+ | i <- [ 0 .. n' - 1 ]+ ]+++-- | @release n s0 s1@ means that either @always n s1@, or @s1@ holds up to and+-- including the period at which @s0@ becomes true.+release :: ( Integral a ) => a -> Stream Bool -> Stream Bool -> Stream Bool+release n s0 s1 = always n s1 || foldl1 (||) v0+ where n' = fromIntegral n+ v0 = [ always ( i :: Int ) s1 && drop i s0+ | i <- [ 0 .. n' - 1 ]+ ]
+ src/Copilot/Library/PTLTL.hs view
@@ -0,0 +1,39 @@+-- | Provides past-time linear-temporal logic (ptLTL operators).+--+-- Interface: see Examples/PTLTLExamples.hs.+-- You can embed a ptLTL specification within a Copilot specification using+-- the form:+-- @+-- operator stream+-- @++module Copilot.Library.PTLTL+ ( since, alwaysBeen, eventuallyPrev, previous ) where+++import Prelude ( ($) )+import Copilot.Language+import Data.Bool hiding ( (&&), (||) )+++-- | Did @s@ hold in the previous period?+previous :: Stream Bool -> Stream Bool+previous s = [ False ] ++ s+++-- | Has @s@ always held (up to and including the current state)?+alwaysBeen :: Stream Bool -> Stream Bool+alwaysBeen s = s && tmp+ where tmp = [ True ] ++ s && tmp+++-- | Did @s@ hold at some time in the past (including the current state)?+eventuallyPrev :: Stream Bool -> Stream Bool+eventuallyPrev s = s || tmp+ where tmp = [ False ] ++ s || tmp+++-- | Once @s2@ holds, in the following state (period), does @s1@ continuously hold?+since :: Stream Bool -> Stream Bool -> Stream Bool+since s1 s2 = alwaysBeen ( tmp ==> s1 )+ where tmp = eventuallyPrev $ [ False ] ++ s2
+ src/Copilot/Library/RegExp.hs view
@@ -0,0 +1,402 @@+module Copilot.Library.RegExp ( copilotRegexp, copilotRegexpB ) where+++import Text.ParserCombinators.Parsec+ ( optional, (<|>), string, char, between, GenParser, many, choice, CharParser+ , optionMaybe, chainr1, chainr, many1, digit, letter, eof, parse+ , SourceName )+import Data.Int+import Data.Word+import Data.List+import Data.Char+import Data.Maybe++import Control.Monad.State ( evalState, get, modify )++import qualified Copilot.Language as C++-- The symbols in a regular expression, "Any" is any value of type t+-- (matches any symbol, the "point" character in a regular expression).+data Sym t = Any | Sym t+ deriving ( Eq, Ord, Show )++-- A symbol's value can occur multiple times in a regular expression,+-- e.g. "t(tfft)*". A running number "symbolNum" is used to make all+-- symbols in a regular expression unique.+type NumT = Int+data NumSym t = NumSym { symbolNum :: Maybe NumT+ , symbol :: Sym t+ } deriving ( Eq, Show )++-- The regular expression data type. For our use+-- regular expressions describing a language with+-- no word is not supported since empty languages+-- would not match anything and just yield a+-- copilot stream of constant false values.+data RegExp t = REpsilon+ | RSymbol ( NumSym t )+ | ROr ( RegExp t ) ( RegExp t )+ | RConcat ( RegExp t ) ( RegExp t )+ | RStar ( RegExp t )+ deriving Show+++-- Parsers for single characters.+lquote, rquote, lparen, rparen,+ star, plus, qmark, point, minus,+ nondigit :: CharParser () Char+lquote = char '<'+rquote = char '>'+lparen = char '('+rparen = char ')'+star = char '*'+plus = char '+'+qmark = char '?'+point = char '.'+minus = char '-'++nondigit = char '_' <|> letter++-- A "followedBy" combinator for parsing, parses+-- p, then p' and returns the result of p.+followedBy :: GenParser tok () a+ -> GenParser tok () b+ -> GenParser tok () a+followedBy p p' = p >>= \ r -> p' >> return r+++-- Parsing a string p' with prefix p, returning+-- both in order+cPrefix, optCPrefix :: GenParser tok () Char+ -> GenParser tok () String+ -> GenParser tok () String+cPrefix p p' = p >>= \ c -> fmap ( c : ) p'++-- Parsing a string p' with the character p as an+-- optional prefix, return the result with the+-- optional prefix.+optCPrefix p p' = optionMaybe p+ >>= \ r -> case r of+ Nothing -> p'+ Just c -> fmap ( c : ) p'++-- The ci function ("case insensitive") takes one argument of+-- type string, parses for the string in a case insensitive+-- manner and yields the parsed string (preserving its case).+ci :: String -> GenParser Char () String+ci = mapM ( \ c -> ( char . toLower ) c <|> ( char . toUpper ) c )+++-- the parser for regular expressions+regexp :: ( SymbolParser t ) => GenParser Char () ( RegExp t )+regexp = chainr1 term opOr++term :: ( SymbolParser t ) => GenParser Char () ( RegExp t )+term = chainr factor opConcat REpsilon++factor :: ( SymbolParser t ) => GenParser Char () ( RegExp t )+factor = opSuffix factor'++factor' :: ( SymbolParser t ) => GenParser Char () ( RegExp t )+factor' = between lparen rparen regexp+ <|> anySym+ <|> parseSym++-- Parses the "." - point character used to match any symbol.+anySym :: ( SymbolParser t ) => GenParser Char () ( RegExp t )+anySym = point >> ( return . RSymbol ) ( NumSym Nothing Any )+++class SymbolParser t where+ parseSym :: GenParser Char () ( RegExp t )+++instance SymbolParser Bool where+ parseSym = do { truth <- ( ci "t" >> optional ( ci "rue" )+ >> return True )+ <|> ( ci "f" >> optional ( ci "alse" )+ >> return False )+ <|> ( string "1" >> return True )+ <|> ( string "0" >> return False )+ ; return $ RSymbol ( NumSym Nothing $ Sym truth )+ }+++parseWordSym :: ( Integral t )+ => GenParser Char () ( RegExp t )+parseWordSym = do { num <- between lquote rquote $ many1 digit+ ; return . RSymbol . NumSym Nothing . Sym+ $ fromIntegral ( read num :: Integer )+ }++parseIntSym :: ( Integral t )+ => GenParser Char () ( RegExp t )+parseIntSym = do { num <- between lquote rquote $+ optCPrefix minus ( many1 digit )+ ; return . RSymbol . NumSym Nothing . Sym+ $ fromIntegral ( read num :: Integer )+ }+++type StreamName = String+newtype P = P { getName :: StreamName }+ deriving Eq+++parsePSym :: GenParser Char () ( RegExp P )+parsePSym = do { pStream <- between lquote rquote $+ cPrefix nondigit ( many $ nondigit <|> digit )+ ; return . RSymbol . NumSym Nothing . Sym+ $ P pStream+ }+++instance SymbolParser Word8 where+ parseSym = parseWordSym++instance SymbolParser Word16 where+ parseSym = parseWordSym++instance SymbolParser Word32 where+ parseSym = parseWordSym++instance SymbolParser Word64 where+ parseSym = parseWordSym++instance SymbolParser Int8 where+ parseSym = parseIntSym++instance SymbolParser Int16 where+ parseSym = parseIntSym++instance SymbolParser Int32 where+ parseSym = parseIntSym++instance SymbolParser Int64 where+ parseSym = parseIntSym++instance SymbolParser P where+ parseSym = parsePSym+++opOr :: GenParser Char () ( RegExp t -> RegExp t -> RegExp t )+opOr = char '|' >> return ROr++opConcat :: GenParser Char () ( RegExp t -> RegExp t -> RegExp t )+opConcat = return RConcat++opSuffix :: GenParser Char () ( RegExp t )+ -> GenParser Char () ( RegExp t )+opSuffix r = do + subexp <- r+ suffixes <- many $ choice [ star, plus, qmark ]+ let transform rexp suffix =+ case suffix of+ '*' -> RStar rexp+ '+' -> RConcat rexp ( RStar rexp )+ '?' -> ROr rexp REpsilon+ other -> C.badUsage ("in Regular Expression library: " +++ "unhandled operator: " ++ show other)+ return $ foldl transform subexp suffixes++parser :: ( SymbolParser t )+ => GenParser Char () ( RegExp t )+parser = regexp `followedBy` eof+++hasEpsilon :: RegExp t -> Bool+hasEpsilon REpsilon = True+hasEpsilon ( RSymbol _ ) = False+hasEpsilon ( ROr r1 r2 ) = hasEpsilon r1 || hasEpsilon r2+hasEpsilon ( RConcat r1 r2 ) = hasEpsilon r1 && hasEpsilon r2+hasEpsilon ( RStar _ ) = True+++first :: RegExp t -> [ NumSym t ]+first REpsilon = []+first ( RSymbol s ) = [ s ]+first ( ROr r1 r2 ) = first r1 ++ first r2+first ( RConcat r1 r2 ) = first r1 ++ if hasEpsilon r1 then+ first r2 else []+first ( RStar r ) = first r+++reverse' :: RegExp t -> RegExp t+reverse' ( ROr r1 r2 ) = ROr ( reverse' r1 ) ( reverse' r2 )+reverse' ( RConcat r1 r2 ) = RConcat ( reverse' r2 ) ( reverse' r1 )+reverse' ( RStar r ) = RStar ( reverse' r )+reverse' e = e+++last' :: RegExp t -> [ NumSym t ]+last' = first . reverse'+++follow :: ( Eq t ) =>+ RegExp t -> NumSym t -> [ NumSym t ]+follow REpsilon _ = []+follow ( RSymbol _ ) _ = []+follow ( ROr r1 r2 ) sNr = follow r1 sNr ++ follow r2 sNr+follow ( RConcat r1 r2 ) sNr = follow r1 sNr ++ follow r2 sNr+ ++ if sNr `elem` last' r1 then+ first r2 else []+follow ( RStar r ) sNr = follow r sNr+ `union` if sNr `elem` last' r then+ first r else []+++preceding :: ( Eq t ) => RegExp t -> NumSym t -> [ NumSym t ]+preceding = follow . reverse'+++hasFinitePath :: RegExp t -> Bool+hasFinitePath ( ROr r1 r2 ) = hasFinitePath r1 || hasFinitePath r2+hasFinitePath ( RConcat _ r2 ) = hasFinitePath r2+hasFinitePath ( RStar _ ) = False+hasFinitePath _ = True+++getSymbols :: RegExp t -> [ NumSym t ]+getSymbols ( RSymbol s ) = [ s ]+getSymbols ( ROr r1 r2 ) = getSymbols r1 ++ getSymbols r2+getSymbols ( RConcat r1 r2 ) = getSymbols r1 ++ getSymbols r2+getSymbols ( RStar r ) = getSymbols r+getSymbols _ = []+++-- assign each symbol in the regular expression a+-- unique number, counting up from 0+enumSyms :: RegExp t -> RegExp t+enumSyms rexp = evalState ( enumSyms' rexp ) 0+ where+ enumSyms' ( RSymbol s ) = do+ num <- get+ modify ( + 1 )+ return $ RSymbol s { symbolNum = Just num }+ enumSyms' ( ROr r1 r2 ) = do+ r1' <- enumSyms' r1+ r2' <- enumSyms' r2+ return $ ROr r1' r2'+ enumSyms' ( RConcat r1 r2 ) = do+ r1' <- enumSyms' r1+ r2' <- enumSyms' r2+ return $ RConcat r1' r2'+ enumSyms' ( RStar r ) = do+ r' <- enumSyms' r+ return $ RStar r'+ enumSyms' other =+ return other+++regexp2CopilotNFA :: ( C.Typed t, Eq t )+ => C.Stream t -> RegExp t -> C.Stream Bool -> C.Stream Bool+regexp2CopilotNFA inStream rexp reset =+ let symbols = getSymbols rexp+ first' = first rexp+ start = [ True ] C.++ C.false++ preceding' numSym = let ps = preceding rexp numSym+ s = if numSym `elem` first' then+ [ start ] else []+ in s ++ [ streams !! i+ | i <- map ( fromJust . symbolNum ) ps ]++ matchesInput numSym = case symbol numSym of+ Any -> C.true+ Sym t -> inStream C.== C.constant t++ transitions numSym ps = matchesInput numSym+ C.&& ( foldl ( C.|| ) C.false ps )++ stream numSym = let ps = preceding' numSym+ init_ = C.constant $ numSym `elem` first'+ in C.mux reset+ ( [ False ] C.++ matchesInput numSym C.&& init_ )+ ( [ False ] C.++ transitions numSym ps )++ streams = map stream symbols++ outStream = foldl ( C.|| ) start streams++ in outStream+++copilotRegexp :: ( C.Typed t, SymbolParser t, Eq t )+ => C.Stream t -> SourceName -> C.Stream Bool -> C.Stream Bool+copilotRegexp inStream rexp reset =+ case parse parser rexp rexp of+ Left err -> C.badUsage ("parsing regular exp: " ++ show err)+ Right rexp' -> let nrexp = enumSyms rexp' in+ if hasFinitePath nrexp then+ C.badUsage $+ concat [ "The regular expression contains a finite path "+ , "which is something that will fail to match "+ , "since we do not have a distinct end-of-input "+ , "symbol on infinite streams." ]+ else if hasEpsilon nrexp then+ C.badUsage $+ concat [ "The regular expression matches a language "+ , "that contains epsilon. This cannot be handled "+ , "on infinite streams, since we do not have "+ , "a distinct end-of-input symbol." ]+ else regexp2CopilotNFA inStream nrexp reset+++regexp2CopilotNFAB :: RegExp P -> [ ( StreamName, C.Stream Bool ) ]+ -> C.Stream Bool -> C.Stream Bool+regexp2CopilotNFAB rexp propositions reset =+ let symbols = getSymbols rexp+ first' = first rexp+ start = [ True ] C.++ C.false++ preceding' numSym = let ps = preceding rexp numSym+ s = if numSym `elem` first' then+ [ start ] else []+ in s ++ [ streams !! i+ | i <- map ( fromJust . symbolNum ) ps ]++ lookup' a l = case lookup a l of+ Nothing -> C.badUsage ("boolean stream "+ ++ a+ ++ " is not defined")+ Just s -> s++ matchesInput numSym = case symbol numSym of+ Any -> C.true+ Sym t -> lookup' ( getName t ) propositions++ transitions numSym ps = matchesInput numSym+ C.&& ( foldl ( C.|| ) C.false ps )++ stream numSym = let ps = preceding' numSym+ init_ = C.constant $ numSym `elem` first'+ in C.mux reset+ ( [ False ] C.++ matchesInput numSym C.&& init_ )+ ( [ False ] C.++ transitions numSym ps )++ streams = map stream symbols++ outStream = foldl ( C.|| ) start streams++ in outStream+++copilotRegexpB :: SourceName -> [ ( StreamName, C.Stream Bool ) ]+ -> C.Stream Bool -> C.Stream Bool+copilotRegexpB rexp propositions reset =+ case parse parser rexp rexp of+ Left err -> C.badUsage ("parsing regular exp: " ++ show err)+ Right rexp' -> let nrexp = enumSyms rexp' in+ if hasFinitePath nrexp then+ C.badUsage $+ concat [ "The regular expression contains a finite path "+ , "which is something that will fail to match "+ , "since we do not have a distinct end-of-input "+ , "symbol on infinite streams." ]+ else if hasEpsilon nrexp then+ C.badUsage $+ concat [ "The regular expression matches a language "+ , "that contains epsilon. This cannot be handled "+ , "on infinite streams, since we do not have "+ , "a distinct end-of-input symbol." ]+ else regexp2CopilotNFAB nrexp propositions reset
+ src/Copilot/Library/Stacks.hs view
@@ -0,0 +1,71 @@+{-# LANGUAGE NoImplicitPrelude #-}++module Copilot.Library.Stacks+ ( stack, stack' ) where+++import Copilot.Language+import Copilot.Language.Prelude+++type PushSignal = Stream Bool+type PopSignal = Stream Bool+type PushStream a = Stream a+type StackTop a = Stream a+++-- stack and stack' streams+--+-- for the stack stream, the PopSignal has precedence+-- over the PushSignal in case both are true in the same tick+--+-- for the stack' stream, the PushSignal has precedence+-- over the PopSignal in case both are true in the same tick+stack, stack' :: ( Integral a, Typed b )+ => a -> b+ -> PopSignal+ -> PushSignal+ -> PushStream b+ -> StackTop b+stack depth startValue+ popSignal pushSignal pushValue =+ let depth' = fromIntegral depth+ startValue' = constant startValue+ stackValue pushValue' popValue' =+ let stackValue' = [ startValue ]+ ++ mux popSignal+ popValue'+ ( mux pushSignal+ pushValue'+ stackValue' )+ in stackValue'+ toStack l =+ let toStack' _ [] = startValue'+ toStack' prev ( sv : svs ) =+ let current = sv prev ( toStack' current svs )+ in current+ in toStack' pushValue l++ in toStack $ replicate depth' stackValue+++stack' depth startValue+ popSignal pushSignal pushValue =+ let depth' = fromIntegral depth+ startValue' = constant startValue+ stackValue pushValue' popValue' =+ let stackValue' = [ startValue ]+ ++ mux pushSignal+ pushValue'+ ( mux popSignal+ popValue'+ stackValue' )+ in stackValue'+ toStack l =+ let toStack' _ [] = startValue'+ toStack' prev ( sv : svs ) =+ let current = sv prev ( toStack' current svs )+ in current+ in toStack' pushValue l++ in toStack $ replicate depth' stackValue
+ src/Copilot/Library/Statistics.hs view
@@ -0,0 +1,37 @@+-- | Basic bounded statistics. In the following, a bound @n@ is given stating+-- the number of periods over which to compute the statistic (@n == 1@ computes+-- it only over the current period).++{-# LANGUAGE NoImplicitPrelude #-}++module Copilot.Library.Statistics+ ( max, min, sum, mean, meanNow ) where++import Copilot.Language+import Copilot.Language.Prelude+import Copilot.Library.Utils++-- | Summation.+sum :: ( Typed a, Num a ) => Int -> Stream a -> Stream a+sum n s = nfoldl1 n (+) s++-- | Maximum value.+max :: ( Typed a, Ord a ) => Int -> Stream a -> Stream a+max n s = nfoldl1 n largest s+ where largest = \ x y -> mux ( x >= y ) x y++-- | Minimum value.+min :: ( Typed a, Ord a ) => Int -> Stream a -> Stream a+min n s = nfoldl1 n smallest s+ where smallest = \ x y -> mux ( x <= y ) x y++-- | Mean value. @n@ must not overflow+-- for word size @a@ for streams over which computation is peformed.+mean :: ( Typed a, Fractional a ) => Int -> Stream a -> Stream a+mean n s = ( sum n s ) / ( fromIntegral n )++-- | Mean value over the current set of streams passed in.+meanNow :: ( Typed a, Integral a ) => [ Stream a ] -> Stream a+meanNow [] = + badUsage "list of arguments to meanNow must be nonempty"+meanNow ls = ( foldl1 (+) ls ) `div` ( fromIntegral $ length ls )
+ src/Copilot/Library/Utils.hs view
@@ -0,0 +1,107 @@+module Copilot.Library.Utils+ ( take, tails, nfoldl, nfoldl1, nfoldr, nfoldr1,+ nscanl, nscanr, nscanl1, nscanr1,+ case', (!!), cycle ) +where+++import Copilot.Language+import Copilot.Language.Prelude +import qualified Prelude as P+++-- | functions similar to the Prelude functions on lists++tails :: ( Typed a )+ => Stream a -> [ Stream a ]+tails s = [ drop x s | x <- [ 0 .. ] ]+++take :: ( Integral a, Typed b )+ => a -> Stream b -> [ Stream b ]+take n s = P.take ( fromIntegral n ) $ tails s+++-- Folds++nfoldl :: ( Typed a, Typed b )+ => Int -> ( Stream a -> Stream b -> Stream a )+ -> Stream a -> Stream b -> Stream a+nfoldl n f e s = foldl f e $ take n s++nfoldl1 :: ( Typed a )+ => Int -> ( Stream a -> Stream a -> Stream a )+ -> Stream a -> Stream a+nfoldl1 n f s = foldl1 f $ take n s++nfoldr :: ( Typed a, Typed b )+ => Int -> ( Stream a -> Stream b -> Stream b )+ -> Stream b -> Stream a -> Stream b+nfoldr n f e s = foldr f e $ take n s++nfoldr1 :: ( Typed a )+ => Int -> ( Stream a -> Stream a -> Stream a )+ -> Stream a -> Stream a+nfoldr1 n f s = foldr1 f $ take n s+++-- Scans++nscanl :: ( Typed a, Typed b )+ => Int -> ( Stream a -> Stream b -> Stream a )+ -> Stream a -> Stream b -> [ Stream a ]+nscanl n f e s = scanl f e $ take n s++nscanr :: ( Typed a )+ => Int -> ( Stream a -> Stream b -> Stream b )+ -> Stream b -> Stream a -> [ Stream b ]+nscanr n f e s = scanr f e $ take n s++nscanl1 :: ( Typed a )+ => Int -> ( Stream a -> Stream a -> Stream a )+ -> Stream a -> [ Stream a ]+nscanl1 n f s = scanl1 f $ take n s++nscanr1 :: ( Typed a )+ => Int -> ( Stream a -> Stream a -> Stream a )+ -> Stream a -> [ Stream a ]+nscanr1 n f s = scanr1 f $ take n s+++-- Case-like function, the index of the first predicate that is true+-- in the predicate list selects the stream result, if no predicate+-- is true, the last element is chosen (default element)+case' :: ( Typed a )+ => [ Stream Bool ] -> [ Stream a ] -> Stream a+case' predicates alternatives =+ let case'' [] ( default' : _ ) = default'+ case'' ( p : ps ) ( a : as ) = mux p a ( case'' ps as )+ case'' _ _ =+ badUsage $ "in case' in Utils library: "+ P.++ "length of alternatives list is not "+ P.++ "greater by one than the length of predicates list"+ in case'' predicates alternatives+++-- | Index. WARNING: very expensive! Consider using this only for very short lists.+(!!) :: ( Typed a, Integral a )+ => [ Stream a ] -> Stream a -> Stream a+ls !! n = let indices = map+ ( constant . fromIntegral )+ [ 0 .. P.length ls - 1 ]+ select [] _ = last ls+ select+ ( i : is )+ ( x : xs ) = mux ( i == n ) x ( select is xs )+ -- should not happen+ select _ [] = badUsage ("in (!!) defined in Utils.hs " P.++ + "in copilot-libraries")+ in if null ls then+ badUsage ("in (!!) defined in Utils.hs " P.++ + "indexing the empty list with !! is not defined")+ else+ select indices ls++cycle :: ( Typed a ) => [ a ] -> Stream a+cycle ls = cycle'+ where cycle' = ls ++ cycle'
+ src/Copilot/Library/Voting.hs view
@@ -0,0 +1,55 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | An implementation of the Boyer-Moore Majority Vote Algorithm for Copilot.+--+-- For details of the Boyer-Moore Majority Vote Algorithm see the following+-- papers:+--+-- * Wim H. Hesselink,+-- \"The Boyer-Moore Majority Vote Algorithm\", 2005+--+-- * Robert S. Boyer and J Strother Moore,+-- \"MJRTY - A Fast Majority Vote Algorithm\", 1982++{-# LANGUAGE RebindableSyntax #-}++module Copilot.Library.Voting + ( majority, aMajority ) where++import Copilot.Language+import Copilot.Language.Prelude+import qualified Prelude as P++--------------------------------------------------------------------------------++majority :: (P.Eq a, Typed a) => [Stream a] -> Stream a+majority [] = badUsage "majority: empty list not allowed"+majority (x:xs) = majority' xs x 1++majority' :: (P.Eq a, Typed a)+ => [Stream a] -> Stream a -> Stream Word32 -> Stream a+majority' [] can _ = can+majority' (x:xs) can cnt =+ local (cnt == 0) $ \ zero -> + local (if zero then x else can) $ \ can' ->+ local (if zero || x == can then cnt+1 else cnt-1) $ \ cnt' ->+ majority' xs can' cnt'++--------------------------------------------------------------------------------++aMajority :: (P.Eq a, Typed a) => [Stream a] -> Stream a -> Stream Bool+aMajority [] _ = badUsage "aMajority: empty list not allowed"+aMajority xs can =+ let+ cnt = aMajority' 0 xs can+ in+ (cnt * 2) > fromIntegral (length xs)++aMajority' :: (P.Eq a, Typed a)+ => Stream Word32 -> [Stream a] -> Stream a -> Stream Word32+aMajority' cnt [] _ = cnt+aMajority' cnt (x:xs) can =+ local (if x == can then cnt+1 else cnt) $ \ cnt' ->+ aMajority' cnt' xs can