copilot-libraries 3.8 → 3.9
raw patch · 11 files changed
+65/−89 lines, 11 filesdep ~copilot-languagePVP ok
version bump matches the API change (PVP)
Dependency ranges changed: copilot-language
API changes (from Hackage documentation)
Files
- CHANGELOG +5/−1
- copilot-libraries.cabal +2/−2
- src/Copilot/Library/Clocks.hs +14/−14
- src/Copilot/Library/LTL.hs +11/−14
- src/Copilot/Library/Libraries.hs +0/−1
- src/Copilot/Library/PTLTL.hs +7/−7
- src/Copilot/Library/RegExp.hs +0/−25
- src/Copilot/Library/Stacks.hs +13/−13
- src/Copilot/Library/Statistics.hs +6/−4
- src/Copilot/Library/Utils.hs +2/−3
- src/Copilot/Library/Voting.hs +5/−5
CHANGELOG view
@@ -1,4 +1,8 @@-2022-01-07+2022-05-06+ * Version bump (3.9). (#320)+ * Compliance with style guide (partial). (#316)++2022-03-07 * Version bump (3.8). (#298) * Mark package as uncurated to avoid modification. (#288)
copilot-libraries.cabal view
@@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-libraries-version: 3.8+version: 3.9 synopsis: Libraries for the Copilot language. description: Libraries for the Copilot language.@@ -43,7 +43,7 @@ , data-reify >= 0.6 && < 0.7 , mtl >= 2.0 && < 2.3 , parsec >= 2.0 && < 3.2- , copilot-language >= 3.8 && < 3.9+ , copilot-language >= 3.9 && < 3.10 exposed-modules: Copilot.Library.Libraries
src/Copilot/Library/Clocks.hs view
@@ -1,4 +1,4 @@--- | +-- | -- Module: Clocks -- Description: Clocks based on a base period and phase -- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.@@ -57,18 +57,18 @@ -> Phase a -- ^ Phase @m@ of clock -> Stream Bool -- ^ Clock signal - 'True' on clock ticks, 'False' otherwise 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'-+ 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' -- | This follows the same convention as 'clk', but uses a counter variable of -- integral type /a/ rather than an array.@@ -85,7 +85,7 @@ badUsage ( "clk1: clock phase must be less than period") else let counter = [ P.fromInteger 0 ]- ++ mux ( counter /= ( constant $ + ++ mux ( counter /= ( constant $ period' P.- 1 ) ) ( counter P.+ 1 ) ( 0 )
src/Copilot/Library/LTL.hs view
@@ -1,4 +1,4 @@--- | +-- | -- Module: LTL -- Description: Bounded Linear Temporal Logic (LTL) operators -- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.@@ -45,7 +45,6 @@ import Copilot.Language import Copilot.Library.Utils - -- | Property @s@ holds at the next period. For example: -- -- @@@ -57,7 +56,6 @@ 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:@@ -72,7 +70,6 @@ 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@@ -90,7 +87,6 @@ -> 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. --@@ -99,11 +95,11 @@ until :: ( Integral a ) => a -> Stream Bool -> Stream Bool -> Stream Bool until 0 _ s1 = s1 until n s0 s1 = foldl (||) s1 v0- where n' = fromIntegral n- v0 = [ always ( i :: Int ) s0 && drop ( i + 1 ) s1- | i <- [ 0 .. n' - 1 ]- ]-+ 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.@@ -113,7 +109,8 @@ release :: ( Integral a ) => a -> Stream Bool -> Stream Bool -> Stream Bool release 0 _ s1 = s1 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 ]- ]+ where+ n' = fromIntegral n+ v0 = [ always ( i :: Int ) s1 && drop i s0+ | i <- [ 0 .. n' - 1 ]+ ]
src/Copilot/Library/Libraries.hs view
@@ -26,4 +26,3 @@ import Copilot.Library.Utils import Copilot.Library.Voting import Copilot.Library.Stacks-
src/Copilot/Library/PTLTL.hs view
@@ -1,4 +1,4 @@--- | +-- | -- Module: PTLTL -- Description: Past-Time Linear-Temporal Logic -- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.@@ -27,20 +27,20 @@ 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-+ 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-+ 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+ where+ tmp = eventuallyPrev $ [ False ] ++ s2
src/Copilot/Library/RegExp.hs view
@@ -9,8 +9,6 @@ -- For an example, see -- <https://github.com/Copilot-Language/examplesForACSL/blob/master/example15/main.hs> -{-# LANGUAGE FlexibleContexts #-}- module Copilot.Library.RegExp ( copilotRegexp, copilotRegexpB ) where import Text.ParserCombinators.Parsec@@ -54,7 +52,6 @@ | RStar ( RegExp t ) deriving Show - -- | Parsers for single characters. lquote, rquote, lparen, rparen, star, plus, qmark, point, minus,@@ -78,7 +75,6 @@ -> 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@@ -98,7 +94,6 @@ ci :: String -> GenParser Char () String ci = mapM ( \ c -> ( char . toLower ) c <|> ( char . toUpper ) c ) - -- | Parser for regular expressions regexp :: ( SymbolParser t ) => GenParser Char () ( RegExp t ) regexp = chainr1 term opOr@@ -118,11 +113,9 @@ 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 )@@ -133,7 +126,6 @@ ; return $ RSymbol ( NumSym Nothing $ Sym truth ) } - parseWordSym :: ( Integral t ) => GenParser Char () ( RegExp t ) parseWordSym = do { num <- between lquote rquote $ many1 digit@@ -149,12 +141,10 @@ $ 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 )@@ -162,7 +152,6 @@ $ P pStream } - instance SymbolParser Word8 where parseSym = parseWordSym @@ -190,7 +179,6 @@ instance SymbolParser P where parseSym = parsePSym - opOr :: GenParser Char () ( RegExp t -> RegExp t -> RegExp t ) opOr = char '|' >> return ROr @@ -215,7 +203,6 @@ => GenParser Char () ( RegExp t ) parser = regexp `followedBy` eof - hasEpsilon :: RegExp t -> Bool hasEpsilon REpsilon = True hasEpsilon ( RSymbol _ ) = False@@ -223,7 +210,6 @@ hasEpsilon ( RConcat r1 r2 ) = hasEpsilon r1 && hasEpsilon r2 hasEpsilon ( RStar _ ) = True - first :: RegExp t -> [ NumSym t ] first REpsilon = [] first ( RSymbol s ) = [ s ]@@ -232,18 +218,15 @@ 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 _ = []@@ -256,18 +239,15 @@ `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@@ -275,7 +255,6 @@ 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@@ -299,7 +278,6 @@ 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 =@@ -332,7 +310,6 @@ in outStream - -- | Regular expression matching over an arbitrary stream copilotRegexp :: ( C.Typed t, SymbolParser t, Eq t ) => C.Stream t -- ^ The stream to monitor.@@ -358,7 +335,6 @@ , "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 =@@ -396,7 +372,6 @@ outStream = foldl ( C.|| ) start streams in outStream- -- | Regular expression matching over a collection of boolean streams. --
src/Copilot/Library/Stacks.hs view
@@ -1,8 +1,8 @@--- | +-- | -- Module: Stacks -- Description: Stream for a stack machine -- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.--- +-- -- This is a stream for a stack machine. -- -- The stack is created from a specified depth, a specified start value, and@@ -15,21 +15,21 @@ -- -- In 'stack' the push signal takes priority over the pop signal in the event -- that both are true in the same tick. This priority is reversed in 'stack''.--- +-- -- Here is an example sequence with one stack of each type, both depth 3 and -- starting value 0: ----- @ --- popSignal: pushSignal: pushValue: stack: stack': --- false true 100 0 0 --- false true 101 100 100 --- true true 102 101 101 --- true false 103 100 102 --- true false 104 0 101 --- true false 105 0 100 --- true false 106 0 0 -- @--- +-- popSignal: pushSignal: pushValue: stack: stack':+-- false true 100 0 0+-- false true 101 100 100+-- true true 102 101 101+-- true false 103 100 102+-- true false 104 0 101+-- true false 105 0 100+-- true false 106 0 0+-- @+-- -- Note the difference at the 4th tick after /popSignal/ and /pushSignal/ were -- both true. Note also that one cannot pop the start value off the stack - -- that is, the stack is never empty.
src/Copilot/Library/Statistics.hs view
@@ -1,4 +1,4 @@--- | +-- | -- Module: Statistics -- Description: Basic bounded statistics -- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.@@ -22,12 +22,14 @@ -- | 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+ 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+ 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.@@ -36,6 +38,6 @@ -- | Mean value over the current set of streams passed in. meanNow :: ( Typed a, Integral a ) => [ Stream a ] -> Stream a-meanNow [] = +meanNow [] = badUsage "list of arguments to meanNow must be nonempty" meanNow ls = ( foldl1 (+) ls ) `div` ( fromIntegral $ length ls )
src/Copilot/Library/Utils.hs view
@@ -27,7 +27,6 @@ => Stream a -> [ Stream a ] tails s = [ drop x s | x <- [ 0 .. ] ] - -- | Given a stream and a number, produce a finite list of streams dropping an -- increasing number of elements of the given stream, up to that number. For -- example, for a given stream @s@, the expression @take 2 s@ is equal to@@ -118,7 +117,6 @@ -> 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)@@ -156,4 +154,5 @@ -- | Cycle a list to form an infinite stream. cycle :: ( Typed a ) => [ a ] -> Stream a cycle ls = cycle'- where cycle' = ls ++ cycle'+ where+ cycle' = ls ++ cycle'
src/Copilot/Library/Voting.hs view
@@ -1,4 +1,4 @@--- | +-- | -- Module: Voting -- Description: Implementation of the Boyer-Moore Majority Vote Algorithm -- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.@@ -34,7 +34,7 @@ {-# LANGUAGE RebindableSyntax #-} -module Copilot.Library.Voting +module Copilot.Library.Voting ( majority, aMajority ) where import Copilot.Language@@ -53,11 +53,11 @@ majority' [] can _ = can majority' (x:xs) can cnt = local (cnt == 0) inZero- where + where inZero zero = local (if zero then x else can) inCan- where + where inCan can' = local (if zero || x == can then cnt+1 else cnt-1) inCnt- where + where inCnt cnt' = majority' xs can' cnt' -- | Majority vote second pass: checking that a candidate indeed has more than