copilot-language 2.2.1 → 3.0
raw patch · 11 files changed
+119/−181 lines, 11 filesdep ~arraydep ~basedep ~containersnew-uploaderPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: array, base, containers, copilot-core, copilot-theorem, data-reify, ghc-prim
API changes (from Hackage documentation)
- Copilot.Language.Operators.Extern: externArray :: (Typed a, Typed b, Integral a) => String -> Stream a -> Size -> Maybe [[b]] -> Stream b
- Copilot.Language.Operators.Extern: externArrayB :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Bool]] -> Stream Bool
- Copilot.Language.Operators.Extern: externArrayD :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Double]] -> Stream Double
- Copilot.Language.Operators.Extern: externArrayF :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Float]] -> Stream Float
- Copilot.Language.Operators.Extern: externArrayI16 :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Int16]] -> Stream Int16
- Copilot.Language.Operators.Extern: externArrayI32 :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Int32]] -> Stream Int32
- Copilot.Language.Operators.Extern: externArrayI64 :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Int64]] -> Stream Int64
- Copilot.Language.Operators.Extern: externArrayI8 :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Int8]] -> Stream Int8
- Copilot.Language.Operators.Extern: externArrayW16 :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Word16]] -> Stream Word16
- Copilot.Language.Operators.Extern: externArrayW32 :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Word32]] -> Stream Word32
- Copilot.Language.Operators.Extern: externArrayW64 :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Word64]] -> Stream Word64
- Copilot.Language.Operators.Extern: externArrayW8 :: (Typed a, Integral a) => String -> Stream a -> Size -> Maybe [[Word8]] -> Stream Word8
- Copilot.Language.Operators.Extern: externStruct :: Typed a => String -> [(String, Arg)] -> Stream a
- Copilot.Language.Operators.Temporal: (#) :: (Typed a, Typed b) => Stream a -> String -> Stream b
+ Copilot.Language: class (Show a, Typeable a) => Typed a
+ Copilot.Language: data Int16
+ Copilot.Language: data Int32
+ Copilot.Language: data Int64
+ Copilot.Language: data Int8
+ Copilot.Language: type Name = String
+ Copilot.Language.Operators.Array: (.!!) :: (KnownNat n, t' ~ InnerType t, Flatten t t', Typed t, Typed t') => Stream (Array n t) -> Stream Word32 -> Stream t
+ Copilot.Language.Operators.BitWise: infixl 5 .|.
+ Copilot.Language.Operators.BitWise: infixl 7 .&.
+ Copilot.Language.Operators.Cast: class Cast a b
+ Copilot.Language.Operators.Cast: class UnsafeCast a b
+ Copilot.Language.Operators.Struct: (#) :: (KnownSymbol s, Typed t, Typed a, Struct a) => Stream a -> (a -> Field s t) -> Stream t
+ Copilot.Language.Prelude: ($!) :: () => (a -> b) -> a -> b
+ Copilot.Language.Prelude: ($) :: () => (a -> b) -> a -> b
+ Copilot.Language.Prelude: (*) :: Num a => a -> a -> a
+ Copilot.Language.Prelude: (**) :: Floating a => a -> a -> a
+ Copilot.Language.Prelude: (*>) :: Applicative f => f a -> f b -> f b
+ Copilot.Language.Prelude: (+) :: Num a => a -> a -> a
+ Copilot.Language.Prelude: (-) :: Num a => a -> a -> a
+ Copilot.Language.Prelude: (.) :: () => (b -> c) -> (a -> b) -> a -> c
+ Copilot.Language.Prelude: (/) :: Fractional a => a -> a -> a
+ Copilot.Language.Prelude: (<$) :: Functor f => a -> f b -> f a
+ Copilot.Language.Prelude: (<$>) :: Functor f => (a -> b) -> f a -> f b
+ Copilot.Language.Prelude: (<*) :: Applicative f => f a -> f b -> f a
+ Copilot.Language.Prelude: (<*>) :: Applicative f => f (a -> b) -> f a -> f b
+ Copilot.Language.Prelude: (<>) :: Semigroup a => a -> a -> a
+ Copilot.Language.Prelude: (=<<) :: Monad m => (a -> m b) -> m a -> m b
+ Copilot.Language.Prelude: (>>) :: Monad m => m a -> m b -> m b
+ Copilot.Language.Prelude: (>>=) :: Monad m => m a -> (a -> m b) -> m b
+ Copilot.Language.Prelude: (^^) :: (Fractional a, Integral b) => a -> b -> a
+ Copilot.Language.Prelude: EQ :: Ordering
+ Copilot.Language.Prelude: False :: Bool
+ Copilot.Language.Prelude: GT :: Ordering
+ Copilot.Language.Prelude: Just :: a -> Maybe a
+ Copilot.Language.Prelude: LT :: Ordering
+ Copilot.Language.Prelude: Left :: a -> Either a b
+ Copilot.Language.Prelude: Nothing :: Maybe a
+ Copilot.Language.Prelude: Right :: b -> Either a b
+ Copilot.Language.Prelude: True :: Bool
+ Copilot.Language.Prelude: abs :: Num a => a -> a
+ Copilot.Language.Prelude: acos :: Floating a => a -> a
+ Copilot.Language.Prelude: acosh :: Floating a => a -> a
+ Copilot.Language.Prelude: all :: Foldable t => (a -> Bool) -> t a -> Bool
+ Copilot.Language.Prelude: and :: Foldable t => t Bool -> Bool
+ Copilot.Language.Prelude: any :: Foldable t => (a -> Bool) -> t a -> Bool
+ Copilot.Language.Prelude: appendFile :: FilePath -> String -> IO ()
+ Copilot.Language.Prelude: asTypeOf :: () => a -> a -> a
+ Copilot.Language.Prelude: asin :: Floating a => a -> a
+ Copilot.Language.Prelude: asinh :: Floating a => a -> a
+ Copilot.Language.Prelude: atan :: Floating a => a -> a
+ Copilot.Language.Prelude: atan2 :: RealFloat a => a -> a -> a
+ Copilot.Language.Prelude: atanh :: Floating a => a -> a
+ Copilot.Language.Prelude: break :: () => (a -> Bool) -> [a] -> ([a], [a])
+ Copilot.Language.Prelude: ceiling :: (RealFrac a, Integral b) => a -> b
+ Copilot.Language.Prelude: class Functor f => Applicative (f :: Type -> Type)
+ Copilot.Language.Prelude: class Bounded a
+ Copilot.Language.Prelude: class Enum a
+ Copilot.Language.Prelude: class Eq a
+ Copilot.Language.Prelude: class Fractional a => Floating a
+ Copilot.Language.Prelude: class Foldable (t :: Type -> Type)
+ Copilot.Language.Prelude: class Num a => Fractional a
+ Copilot.Language.Prelude: class Functor (f :: Type -> Type)
+ Copilot.Language.Prelude: class (Real a, Enum a) => Integral a
+ Copilot.Language.Prelude: class Applicative m => Monad (m :: Type -> Type)
+ Copilot.Language.Prelude: class Semigroup a => Monoid a
+ Copilot.Language.Prelude: class Num a
+ Copilot.Language.Prelude: class Eq a => Ord a
+ Copilot.Language.Prelude: class Read a
+ Copilot.Language.Prelude: class (Num a, Ord a) => Real a
+ Copilot.Language.Prelude: class (RealFrac a, Floating a) => RealFloat a
+ Copilot.Language.Prelude: class (Real a, Fractional a) => RealFrac a
+ Copilot.Language.Prelude: class Semigroup a
+ Copilot.Language.Prelude: class Show a
+ Copilot.Language.Prelude: class (Functor t, Foldable t) => Traversable (t :: Type -> Type)
+ Copilot.Language.Prelude: compare :: Ord a => a -> a -> Ordering
+ Copilot.Language.Prelude: concat :: Foldable t => t [a] -> [a]
+ Copilot.Language.Prelude: concatMap :: Foldable t => (a -> [b]) -> t a -> [b]
+ Copilot.Language.Prelude: cos :: Floating a => a -> a
+ Copilot.Language.Prelude: cosh :: Floating a => a -> a
+ Copilot.Language.Prelude: curry :: () => ((a, b) -> c) -> a -> b -> c
+ Copilot.Language.Prelude: data Bool
+ Copilot.Language.Prelude: data Char
+ Copilot.Language.Prelude: data Double
+ Copilot.Language.Prelude: data Either a b
+ Copilot.Language.Prelude: data Float
+ Copilot.Language.Prelude: data IO a
+ Copilot.Language.Prelude: data Int
+ Copilot.Language.Prelude: data Integer
+ Copilot.Language.Prelude: data Maybe a
+ Copilot.Language.Prelude: data Ordering
+ Copilot.Language.Prelude: data Word
+ Copilot.Language.Prelude: decodeFloat :: RealFloat a => a -> (Integer, Int)
+ Copilot.Language.Prelude: divMod :: Integral a => a -> a -> (a, a)
+ Copilot.Language.Prelude: dropWhile :: () => (a -> Bool) -> [a] -> [a]
+ Copilot.Language.Prelude: either :: () => (a -> c) -> (b -> c) -> Either a b -> c
+ Copilot.Language.Prelude: elem :: (Foldable t, Eq a) => a -> t a -> Bool
+ Copilot.Language.Prelude: encodeFloat :: RealFloat a => Integer -> Int -> a
+ Copilot.Language.Prelude: enumFrom :: Enum a => a -> [a]
+ Copilot.Language.Prelude: enumFromThen :: Enum a => a -> a -> [a]
+ Copilot.Language.Prelude: enumFromThenTo :: Enum a => a -> a -> a -> [a]
+ Copilot.Language.Prelude: enumFromTo :: Enum a => a -> a -> [a]
+ Copilot.Language.Prelude: error :: HasCallStack => [Char] -> a
+ Copilot.Language.Prelude: errorWithoutStackTrace :: () => [Char] -> a
+ Copilot.Language.Prelude: even :: Integral a => a -> Bool
+ Copilot.Language.Prelude: exp :: Floating a => a -> a
+ Copilot.Language.Prelude: exponent :: RealFloat a => a -> Int
+ Copilot.Language.Prelude: fail :: Monad m => String -> m a
+ Copilot.Language.Prelude: filter :: () => (a -> Bool) -> [a] -> [a]
+ Copilot.Language.Prelude: flip :: () => (a -> b -> c) -> b -> a -> c
+ Copilot.Language.Prelude: floatDigits :: RealFloat a => a -> Int
+ Copilot.Language.Prelude: floatRadix :: RealFloat a => a -> Integer
+ Copilot.Language.Prelude: floatRange :: RealFloat a => a -> (Int, Int)
+ Copilot.Language.Prelude: floor :: (RealFrac a, Integral b) => a -> b
+ Copilot.Language.Prelude: fmap :: Functor f => (a -> b) -> f a -> f b
+ Copilot.Language.Prelude: foldMap :: (Foldable t, Monoid m) => (a -> m) -> t a -> m
+ Copilot.Language.Prelude: foldl :: Foldable t => (b -> a -> b) -> b -> t a -> b
+ Copilot.Language.Prelude: foldl1 :: Foldable t => (a -> a -> a) -> t a -> a
+ Copilot.Language.Prelude: foldr :: Foldable t => (a -> b -> b) -> b -> t a -> b
+ Copilot.Language.Prelude: foldr1 :: Foldable t => (a -> a -> a) -> t a -> a
+ Copilot.Language.Prelude: fromEnum :: Enum a => a -> Int
+ Copilot.Language.Prelude: fromInteger :: Num a => Integer -> a
+ Copilot.Language.Prelude: fromIntegral :: (Integral a, Num b) => a -> b
+ Copilot.Language.Prelude: fromRational :: Fractional a => Rational -> a
+ Copilot.Language.Prelude: fst :: () => (a, b) -> a
+ Copilot.Language.Prelude: gcd :: Integral a => a -> a -> a
+ Copilot.Language.Prelude: getChar :: IO Char
+ Copilot.Language.Prelude: getContents :: IO String
+ Copilot.Language.Prelude: getLine :: IO String
+ Copilot.Language.Prelude: head :: () => [a] -> a
+ Copilot.Language.Prelude: id :: () => a -> a
+ Copilot.Language.Prelude: infix 4 `notElem`
+ Copilot.Language.Prelude: infixl 1 >>
+ Copilot.Language.Prelude: infixl 4 <$>
+ Copilot.Language.Prelude: infixl 6 -
+ Copilot.Language.Prelude: infixl 7 *
+ Copilot.Language.Prelude: infixr 0 $!
+ Copilot.Language.Prelude: infixr 1 =<<
+ Copilot.Language.Prelude: infixr 6 <>
+ Copilot.Language.Prelude: infixr 8 ^^
+ Copilot.Language.Prelude: infixr 9 .
+ Copilot.Language.Prelude: init :: () => [a] -> [a]
+ Copilot.Language.Prelude: interact :: (String -> String) -> IO ()
+ Copilot.Language.Prelude: ioError :: () => IOError -> IO a
+ Copilot.Language.Prelude: isDenormalized :: RealFloat a => a -> Bool
+ Copilot.Language.Prelude: isIEEE :: RealFloat a => a -> Bool
+ Copilot.Language.Prelude: isInfinite :: RealFloat a => a -> Bool
+ Copilot.Language.Prelude: isNaN :: RealFloat a => a -> Bool
+ Copilot.Language.Prelude: isNegativeZero :: RealFloat a => a -> Bool
+ Copilot.Language.Prelude: iterate :: () => (a -> a) -> a -> [a]
+ Copilot.Language.Prelude: last :: () => [a] -> a
+ Copilot.Language.Prelude: lcm :: Integral a => a -> a -> a
+ Copilot.Language.Prelude: length :: Foldable t => t a -> Int
+ Copilot.Language.Prelude: lex :: ReadS String
+ Copilot.Language.Prelude: lines :: String -> [String]
+ Copilot.Language.Prelude: log :: Floating a => a -> a
+ Copilot.Language.Prelude: logBase :: Floating a => a -> a -> a
+ Copilot.Language.Prelude: lookup :: Eq a => a -> [(a, b)] -> Maybe b
+ Copilot.Language.Prelude: map :: () => (a -> b) -> [a] -> [b]
+ Copilot.Language.Prelude: mapM :: (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b)
+ Copilot.Language.Prelude: mapM_ :: (Foldable t, Monad m) => (a -> m b) -> t a -> m ()
+ Copilot.Language.Prelude: mappend :: Monoid a => a -> a -> a
+ Copilot.Language.Prelude: maxBound :: Bounded a => a
+ Copilot.Language.Prelude: maximum :: (Foldable t, Ord a) => t a -> a
+ Copilot.Language.Prelude: maybe :: () => b -> (a -> b) -> Maybe a -> b
+ Copilot.Language.Prelude: mconcat :: Monoid a => [a] -> a
+ Copilot.Language.Prelude: mempty :: Monoid a => a
+ Copilot.Language.Prelude: minBound :: Bounded a => a
+ Copilot.Language.Prelude: minimum :: (Foldable t, Ord a) => t a -> a
+ Copilot.Language.Prelude: negate :: Num a => a -> a
+ Copilot.Language.Prelude: notElem :: (Foldable t, Eq a) => a -> t a -> Bool
+ Copilot.Language.Prelude: null :: Foldable t => t a -> Bool
+ Copilot.Language.Prelude: odd :: Integral a => a -> Bool
+ Copilot.Language.Prelude: or :: Foldable t => t Bool -> Bool
+ Copilot.Language.Prelude: otherwise :: Bool
+ Copilot.Language.Prelude: pi :: Floating a => a
+ Copilot.Language.Prelude: pred :: Enum a => a -> a
+ Copilot.Language.Prelude: print :: Show a => a -> IO ()
+ Copilot.Language.Prelude: product :: (Foldable t, Num a) => t a -> a
+ Copilot.Language.Prelude: properFraction :: (RealFrac a, Integral b) => a -> (b, a)
+ Copilot.Language.Prelude: pure :: Applicative f => a -> f a
+ Copilot.Language.Prelude: putChar :: Char -> IO ()
+ Copilot.Language.Prelude: putStr :: String -> IO ()
+ Copilot.Language.Prelude: putStrLn :: String -> IO ()
+ Copilot.Language.Prelude: quot :: Integral a => a -> a -> a
+ Copilot.Language.Prelude: quotRem :: Integral a => a -> a -> (a, a)
+ Copilot.Language.Prelude: read :: Read a => String -> a
+ Copilot.Language.Prelude: readFile :: FilePath -> IO String
+ Copilot.Language.Prelude: readIO :: Read a => String -> IO a
+ Copilot.Language.Prelude: readList :: Read a => ReadS [a]
+ Copilot.Language.Prelude: readLn :: Read a => IO a
+ Copilot.Language.Prelude: readParen :: () => Bool -> ReadS a -> ReadS a
+ Copilot.Language.Prelude: reads :: Read a => ReadS a
+ Copilot.Language.Prelude: readsPrec :: Read a => Int -> ReadS a
+ Copilot.Language.Prelude: realToFrac :: (Real a, Fractional b) => a -> b
+ Copilot.Language.Prelude: recip :: Fractional a => a -> a
+ Copilot.Language.Prelude: rem :: Integral a => a -> a -> a
+ Copilot.Language.Prelude: repeat :: () => a -> [a]
+ Copilot.Language.Prelude: replicate :: () => Int -> a -> [a]
+ Copilot.Language.Prelude: return :: Monad m => a -> m a
+ Copilot.Language.Prelude: reverse :: () => [a] -> [a]
+ Copilot.Language.Prelude: round :: (RealFrac a, Integral b) => a -> b
+ Copilot.Language.Prelude: scaleFloat :: RealFloat a => Int -> a -> a
+ Copilot.Language.Prelude: scanl :: () => (b -> a -> b) -> b -> [a] -> [b]
+ Copilot.Language.Prelude: scanl1 :: () => (a -> a -> a) -> [a] -> [a]
+ Copilot.Language.Prelude: scanr :: () => (a -> b -> b) -> b -> [a] -> [b]
+ Copilot.Language.Prelude: scanr1 :: () => (a -> a -> a) -> [a] -> [a]
+ Copilot.Language.Prelude: seq :: () => a -> b -> b
+ Copilot.Language.Prelude: sequence :: (Traversable t, Monad m) => t (m a) -> m (t a)
+ Copilot.Language.Prelude: sequenceA :: (Traversable t, Applicative f) => t (f a) -> f (t a)
+ Copilot.Language.Prelude: sequence_ :: (Foldable t, Monad m) => t (m a) -> m ()
+ Copilot.Language.Prelude: show :: Show a => a -> String
+ Copilot.Language.Prelude: showChar :: Char -> ShowS
+ Copilot.Language.Prelude: showList :: Show a => [a] -> ShowS
+ Copilot.Language.Prelude: showParen :: Bool -> ShowS -> ShowS
+ Copilot.Language.Prelude: showString :: String -> ShowS
+ Copilot.Language.Prelude: shows :: Show a => a -> ShowS
+ Copilot.Language.Prelude: showsPrec :: Show a => Int -> a -> ShowS
+ Copilot.Language.Prelude: significand :: RealFloat a => a -> a
+ Copilot.Language.Prelude: signum :: Num a => a -> a
+ Copilot.Language.Prelude: sin :: Floating a => a -> a
+ Copilot.Language.Prelude: sinh :: Floating a => a -> a
+ Copilot.Language.Prelude: snd :: () => (a, b) -> b
+ Copilot.Language.Prelude: span :: () => (a -> Bool) -> [a] -> ([a], [a])
+ Copilot.Language.Prelude: splitAt :: () => Int -> [a] -> ([a], [a])
+ Copilot.Language.Prelude: sqrt :: Floating a => a -> a
+ Copilot.Language.Prelude: subtract :: Num a => a -> a -> a
+ Copilot.Language.Prelude: succ :: Enum a => a -> a
+ Copilot.Language.Prelude: tail :: () => [a] -> [a]
+ Copilot.Language.Prelude: takeWhile :: () => (a -> Bool) -> [a] -> [a]
+ Copilot.Language.Prelude: tan :: Floating a => a -> a
+ Copilot.Language.Prelude: tanh :: Floating a => a -> a
+ Copilot.Language.Prelude: toEnum :: Enum a => Int -> a
+ Copilot.Language.Prelude: toInteger :: Integral a => a -> Integer
+ Copilot.Language.Prelude: toRational :: Real a => a -> Rational
+ Copilot.Language.Prelude: traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)
+ Copilot.Language.Prelude: truncate :: (RealFrac a, Integral b) => a -> b
+ Copilot.Language.Prelude: type FilePath = String
+ Copilot.Language.Prelude: type IOError = IOException
+ Copilot.Language.Prelude: type Rational = Ratio Integer
+ Copilot.Language.Prelude: type ReadS a = String -> [(a, String)]
+ Copilot.Language.Prelude: type ShowS = String -> String
+ Copilot.Language.Prelude: type String = [Char]
+ Copilot.Language.Prelude: uncurry :: () => (a -> b -> c) -> (a, b) -> c
+ Copilot.Language.Prelude: undefined :: HasCallStack => a
+ Copilot.Language.Prelude: unlines :: [String] -> String
+ Copilot.Language.Prelude: unwords :: [String] -> String
+ Copilot.Language.Prelude: unzip :: () => [(a, b)] -> ([a], [b])
+ Copilot.Language.Prelude: unzip3 :: () => [(a, b, c)] -> ([a], [b], [c])
+ Copilot.Language.Prelude: userError :: String -> IOError
+ Copilot.Language.Prelude: words :: String -> [String]
+ Copilot.Language.Prelude: writeFile :: FilePath -> String -> IO ()
+ Copilot.Language.Prelude: zip :: () => [a] -> [b] -> [(a, b)]
+ Copilot.Language.Prelude: zip3 :: () => [a] -> [b] -> [c] -> [(a, b, c)]
+ Copilot.Language.Prelude: zipWith :: () => (a -> b -> c) -> [a] -> [b] -> [c]
+ Copilot.Language.Prelude: zipWith3 :: () => (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
+ Copilot.Language.Spec: [Exists] :: Stream Bool -> Prop Existential
+ Copilot.Language.Spec: [Forall] :: Stream Bool -> Prop Universal
+ Copilot.Language.Spec: [Observer] :: Typed a => String -> Stream a -> Observer
+ Copilot.Language.Spec: [Property] :: String -> Stream Bool -> Property
+ Copilot.Language.Spec: [Trigger] :: Name -> Stream Bool -> [Arg] -> Trigger
+ Copilot.Language.Spec: arg :: Typed a => Stream a -> Arg
+ Copilot.Language.Spec: data Existential
+ Copilot.Language.Spec: data Observer
+ Copilot.Language.Spec: data Prop a
+ Copilot.Language.Spec: data Property
+ Copilot.Language.Spec: data SpecItem
+ Copilot.Language.Spec: data Trigger
+ Copilot.Language.Spec: data Universal
+ Copilot.Language.Spec: exists :: Stream Bool -> Prop Existential
+ Copilot.Language.Spec: extractProp :: Prop a -> Stream Bool
+ Copilot.Language.Spec: forall :: Stream Bool -> Prop Universal
+ Copilot.Language.Spec: observer :: Typed a => String -> Stream a -> Spec
+ Copilot.Language.Spec: observers :: [SpecItem] -> [Observer]
+ Copilot.Language.Spec: prop :: String -> Prop a -> Writer [SpecItem] (PropRef a)
+ Copilot.Language.Spec: properties :: [SpecItem] -> [Property]
+ Copilot.Language.Spec: runSpec :: Spec' a -> [SpecItem]
+ Copilot.Language.Spec: theorem :: String -> Prop a -> Proof a -> Writer [SpecItem] (PropRef a)
+ Copilot.Language.Spec: theorems :: [SpecItem] -> [(Property, UProof)]
+ Copilot.Language.Spec: trigger :: String -> Stream Bool -> [Arg] -> Spec
+ Copilot.Language.Spec: triggers :: [SpecItem] -> [Trigger]
+ Copilot.Language.Spec: type Spec = Writer [SpecItem] ()
+ Copilot.Language.Spec: type Spec' a = Writer [SpecItem] a
+ Copilot.Language.Stream: StructArg :: String -> Arg -> StructArg
+ Copilot.Language.Stream: [Append] :: Typed a => [a] -> Maybe (Stream Bool) -> Stream a -> Stream a
+ Copilot.Language.Stream: [Arg] :: Typed a => Stream a -> Arg
+ Copilot.Language.Stream: [Const] :: Typed a => a -> Stream a
+ Copilot.Language.Stream: [Drop] :: Typed a => Int -> Stream a -> Stream a
+ Copilot.Language.Stream: [ExternFun] :: Typed a => String -> [Arg] -> Maybe (Stream a) -> Stream a
+ Copilot.Language.Stream: [Extern] :: Typed a => String -> Maybe [a] -> Stream a
+ Copilot.Language.Stream: [Label] :: Typed a => String -> Stream a -> Stream a
+ Copilot.Language.Stream: [Local] :: (Typed a, Typed b) => Stream a -> (Stream a -> Stream b) -> Stream b
+ Copilot.Language.Stream: [Op1] :: (Typed a, Typed b) => Op1 a b -> Stream a -> Stream b
+ Copilot.Language.Stream: [Op2] :: (Typed a, Typed b, Typed c) => Op2 a b c -> Stream a -> Stream b -> Stream c
+ Copilot.Language.Stream: [Op3] :: (Typed a, Typed b, Typed c, Typed d) => Op3 a b c d -> Stream a -> Stream b -> Stream c -> Stream d
+ Copilot.Language.Stream: [Var] :: Typed a => String -> Stream a
+ Copilot.Language.Stream: [arg'] :: StructArg -> Arg
+ Copilot.Language.Stream: [name_] :: StructArg -> String
+ Copilot.Language.Stream: data Arg
+ Copilot.Language.Stream: data Stream :: * -> *
+ Copilot.Language.Stream: data StructArg
+ Copilot.Language.Stream: instance (Copilot.Core.Type.Typed a, GHC.Classes.Eq a, GHC.Float.Floating a) => GHC.Float.Floating (Copilot.Language.Stream.Stream a)
+ Copilot.Language.Stream: instance (Copilot.Core.Type.Typed a, GHC.Classes.Eq a, GHC.Num.Num a) => GHC.Num.Num (Copilot.Language.Stream.Stream a)
+ Copilot.Language.Stream: instance (Copilot.Core.Type.Typed a, GHC.Classes.Eq a, GHC.Real.Fractional a) => GHC.Real.Fractional (Copilot.Language.Stream.Stream a)
+ Copilot.Language.Stream: instance GHC.Classes.Eq (Copilot.Language.Stream.Stream a)
+ Copilot.Language.Stream: instance GHC.Show.Show (Copilot.Language.Stream.Stream a)
- Copilot.Language.Operators.Label: label :: (Typed a) => String -> Stream a -> Stream a
+ Copilot.Language.Operators.Label: label :: Typed a => String -> Stream a -> Stream a
Files
- README.md +37/−0
- copilot-language.cabal +23/−27
- src/Copilot/Language.hs +8/−0
- src/Copilot/Language/Analyze.hs +1/−39
- src/Copilot/Language/Operators/Array.hs +30/−0
- src/Copilot/Language/Operators/Cast.hs +1/−1
- src/Copilot/Language/Operators/Extern.hs +0/−78
- src/Copilot/Language/Operators/Struct.hs +19/−0
- src/Copilot/Language/Operators/Temporal.hs +0/−9
- src/Copilot/Language/Reify.hs +0/−21
- src/Copilot/Language/Stream.hs +0/−6
+ README.md view
@@ -0,0 +1,37 @@+[](https://travis-ci.org/Copilot-Language/copilot-core)++# Copilot: a stream DSL+Copilot-language contains the actual embedded domain specific language that+Copilot provides to its users. It comes with a series of basic operators and+functionality, typically enough for most applications. Extended functionality+is provided by the+[copilot-libraries](https://github.com/Copilot-Language/copilot-libraries)+module.++Copilot is a runtime verification framework written in Haskell. It allows the+user to write programs in a simple but powerful way using a stream-based+approach.++Programs can be interpreted for testing, or translated C99 code to be+incorporated in a project, or as a standalone application. The C99 backend+ensures us that the output is constant in memory and time, making it suitable+for systems with hard realtime requirements.+++## Installation+Copilot-language can be found on+[Hackage](https://hackage.haskell.org/package/copilot-language). It is typically+only installed as part of the complete Copilot distribution. For installation+instructions, please refer to the [Copilot+website](https://copilot-language.github.io).+++## Further information+For further information, install instructions and documentation, please visit+the Copilot website:+[https://copilot-language.github.io](https://copilot-language.github.io)+++## License+Copilot is distributed under the BSD-3-Clause license, which can be found+[here](https://raw.githubusercontent.com/Copilot-Language/copilot-language/master/LICENSE).
copilot-language.cabal view
@@ -1,6 +1,6 @@ cabal-version: >=1.10 name: copilot-language-version: 2.2.1+version: 3.0 synopsis: A Haskell-embedded DSL for monitoring hard real-time distributed systems. description:@@ -10,35 +10,39 @@ Haskell that compiles into embedded C. Copilot contains an interpreter, multiple back-end compilers, and other verification tools. A tutorial, bug reports, and todos are available at- <https://github.com/leepike/copilot-discussion>.+ <https://github.com/Copilot-Language/copilot-discussion>. . Examples are available at- <https://github.com/leepike/Copilot/tree/master/Examples>.+ <https://github.com/Copilot-Language/Copilot/tree/master/Examples>. license: BSD3 license-file: LICENSE-author: Lee Pike, Robin Morisset, Alwyn Goodloe, Sebastian Niller,- Nis Nordby Wegmann-maintainer: leepike@gmail.com+author: Frank Dedden, Lee Pike, Robin Morisset, Alwyn Goodloe,+ Sebastian Niller, Nis Nordby Wegmann+maintainer: Frank Dedden <dev@dedden.net> stability: Experimental category: Language, Embedded build-type: Simple+extra-source-files: README.md source-repository head type: git- location: git://github.com/leepike/copilot-language.git+ location: https://github.com/Copilot-Language/copilot-language.git library default-language: Haskell2010 hs-source-dirs: src- build-depends: array- , base >= 4.0 && < 5- , containers >= 0.4- , data-reify >= 0.6- , mtl >= 2.0 && < 3- , ghc-prim >= 0.2- , copilot-core >= 2.2.1- , copilot-theorem >= 2.1+ build-depends: base >= 4.9 && < 5++ , array >= 0.5 && < 0.6+ , containers >= 0.4 && < 0.7+ , data-reify >= 0.6 && < 0.7+ , mtl >= 2.0 && < 3+ , ghc-prim >= 0.3 && < 0.6++ , copilot-core >= 3.0 && < 3.1+ , copilot-theorem >= 3.0 && < 3.1+ exposed-modules: Copilot , Copilot.Language , Copilot.Language.Operators.BitWise@@ -54,25 +58,17 @@ , Copilot.Language.Operators.Mux , Copilot.Language.Operators.Ord , Copilot.Language.Operators.Temporal+ , Copilot.Language.Operators.Array+ , Copilot.Language.Operators.Struct , Copilot.Language.Prelude , Copilot.Language.Reify- other-modules: Copilot.Language.Analyze- , Copilot.Language.Interpret , Copilot.Language.Stream , Copilot.Language.Spec+ other-modules: Copilot.Language.Analyze+ , Copilot.Language.Interpret , System.Mem.StableName.Dynamic , System.Mem.StableName.Map , Copilot.Language.Error ghc-options: -fwarn-tabs- -auto-all- -caf-all -Wall-- -fpackage-trust- -trust=array- -trust=base- -trust=containers- -trust=copilot-core--
src/Copilot/Language.hs view
@@ -10,6 +10,8 @@ ( module Data.Int , module Data.Word , module Copilot.Core+ , module Copilot.Core.Type+ , module Copilot.Core.Type.Array , module Copilot.Language.Error , module Copilot.Language.Interpret , module Copilot.Language.Operators.Boolean@@ -24,6 +26,8 @@ , module Copilot.Language.Operators.Ord , module Copilot.Language.Operators.Temporal , module Copilot.Language.Operators.BitWise+ , module Copilot.Language.Operators.Array+ , module Copilot.Language.Operators.Struct , module Copilot.Language.Prelude , Spec , Stream@@ -39,6 +43,8 @@ import Data.Int hiding (Int) import Data.Word import Copilot.Core (Name, Typed)+import Copilot.Core.Type+import Copilot.Core.Type.Array import qualified Copilot.Core.PrettyPrint as PP import Copilot.Language.Error import Copilot.Language.Interpret@@ -54,6 +60,8 @@ import Copilot.Language.Operators.Ord import Copilot.Language.Operators.Temporal import Copilot.Language.Operators.BitWise+import Copilot.Language.Operators.Array+import Copilot.Language.Operators.Struct import Copilot.Language.Reify import Copilot.Language.Prelude import Copilot.Language.Spec
src/Copilot/Language/Analyze.hs view
@@ -147,19 +147,6 @@ SeenFun -> throw NestedExternFun SeenArr -> throw NestedArray SeenStruct-> throw InvalidField- ExternArray _ idx _ _ -> case seenExt of- NoExtern -> go SeenArr nodes' idx- SeenFun -> throw NestedExternFun- SeenArr -> throw NestedArray- SeenStruct-> go SeenStruct nodes' idx- ExternStruct _ sargs -> case seenExt of- NoExtern ->- mapM_ (\(_, Arg a) -> go SeenStruct nodes' a) sargs- SeenFun -> throw NestedExternFun- SeenArr -> throw NestedArray- SeenStruct->- mapM_ (\(_, Arg a) -> go SeenStruct nodes' a) sargs- GetField e _ -> analyzeAppend refStreams dstn e () analyzeExpr --Copied from `Append` case Local e f -> go seenExt nodes' e >> go seenExt nodes' (f (Var "dummy")) Var _ -> return ()@@ -359,22 +346,6 @@ , externFunArgs = (name, argTypes) : externFunArgs env'' } - ExternArray name idx _ _ -> do- env' <- go nodes env idx- let arr = ( name, getSimpleType stream )- return env' { externArrEnv = arr : externArrEnv env' }-- ExternStruct name sargs -> do- env' <- foldM (\env' (_, Arg arg_) -> go nodes env' arg_)- env sargs- --let argTypes = map (\(Arg arg_) -> (n, getSimpleType arg_)) sargs- let argTypes = map (\(_, Arg arg_) -> getSimpleType arg_) sargs- let struct = (name, getSimpleType stream)- return env' { externStructEnv = struct : externStructEnv env'- , externStructArgs = (name, argTypes) : externStructArgs env' }-- GetField _ _ -> return env- Local e _ -> go nodes env e Var _ -> return env Op1 _ e -> go nodes env e@@ -386,16 +357,7 @@ Label _ e -> go nodes env e ---------------------------------------------------------------------------------{--getArgName :: forall a. C.Typed a => Stream a -> String-getArgName arg_stream =- case arg_stream of- Extern cs _ -> cs- ExternFun cs _ _ -> cs- ExternArray cs _ _ _ -> cs- ExternStruct cs _ -> cs- _ -> ""--}+ getSimpleType :: forall a. C.Typed a => Stream a -> C.SimpleType getSimpleType _ = C.simpleType (C.typeOf :: C.Type a)
+ src/Copilot/Language/Operators/Array.hs view
@@ -0,0 +1,30 @@+{-# LANGUAGE Safe #-}++{-# LANGUAGE TypeFamilies #-}++module Copilot.Language.Operators.Array+ ( (.!!)+ ) where++import Copilot.Core ( Typed+ , Op2 (Index)+ , typeOf+ , Array+ , InnerType+ , Flatten)+import Copilot.Language.Stream (Stream (..))++import Data.Word (Word32)+import GHC.TypeLits (KnownNat)++--------------------------------------------------------------------------------++(.!!) :: ( KnownNat n+ , t' ~ InnerType t+ , Flatten t t'+ , Typed t+ , Typed t'+ ) => Stream (Array n t) -> Stream Word32 -> Stream t+arr .!! n = Op2 (Index typeOf) arr n++--------------------------------------------------------------------------------
src/Copilot/Language/Operators/Cast.hs view
@@ -8,7 +8,7 @@ {-# LANGUAGE MultiParamTypeClasses #-} module Copilot.Language.Operators.Cast- ( cast, unsafeCast ) where+ ( cast, unsafeCast, Cast, UnsafeCast ) where import qualified Copilot.Core.Operators as C import Copilot.Core.Type
src/Copilot/Language/Operators/Extern.hs view
@@ -20,19 +20,6 @@ , externF , externD , externFun- , externArray- , externArrayB- , externArrayW8- , externArrayW16- , externArrayW32- , externArrayW64- , externArrayI8- , externArrayI16- , externArrayI32- , externArrayI64- , externArrayF- , externArrayD- , externStruct , funArg -- * Deprecated. ) where @@ -51,28 +38,10 @@ externFun :: Typed a => String -> [Arg] -> Maybe (Stream a) -> Stream a externFun = ExternFun -externArray :: (Typed a, Typed b, Integral a)- => String -> Stream a -> Size -> Maybe [[b]] -> Stream b-externArray = ExternArray- -- | Deprecated. funArg :: Typed a => Stream a -> Arg funArg = Arg -externStruct :: Typed a => String -> [(String, Arg)] -> Stream a-externStruct = ExternStruct--{-(#) :: Typed a => Core.StructData -> String -> Stream a-(Core.StructData {Core.structName = x, Core.structInst = y})#z = getField x z- where- getField struct_nm field_nm =- let test = find (\(Core.StructData name _) -> name == struct_nm) structs in- case test of- Nothing -> error "No struct named \"" ++ struct_nm ++ "\" in the spec"- Just element ->- fromMaybe (find (\(Core.SExpr name _) -> name == field_nm) (element Core.structInst))- (error "No field by the name of \"" ++ field_nm ++ "\"") element--} -------------------------------------------------------------------------------- externB :: String -> Maybe [Bool] -> Stream Bool@@ -97,50 +66,3 @@ externF = extern externD :: String -> Maybe [Double] -> Stream Double externD = extern------------------------------------------------------------------------------------externArrayB :: (Typed a, Integral a)- => String -> Stream a -> Size- -> Maybe [[Bool]] -> Stream Bool-externArrayB = externArray-externArrayW8 :: (Typed a, Integral a)- => String -> Stream a -> Size- -> Maybe [[Word8]] -> Stream Word8-externArrayW8 = externArray-externArrayW16 :: (Typed a, Integral a)- => String -> Stream a -> Size- -> Maybe [[Word16]] -> Stream Word16-externArrayW16 = externArray-externArrayW32 :: (Typed a, Integral a)- => String -> Stream a -> Size- -> Maybe [[Word32]] -> Stream Word32-externArrayW32 = externArray-externArrayW64 :: (Typed a, Integral a)- => String -> Stream a -> Size- -> Maybe [[Word64]] -> Stream Word64-externArrayW64 = externArray-externArrayI8 :: (Typed a, Integral a)- => String -> Stream a -> Size- -> Maybe [[Int8]] -> Stream Int8-externArrayI8 = externArray-externArrayI16 :: (Typed a, Integral a)- => String -> Stream a -> Size- -> Maybe [[Int16]] -> Stream Int16-externArrayI16 = externArray-externArrayI32 :: (Typed a, Integral a)- => String -> Stream a -> Size- -> Maybe [[Int32]] -> Stream Int32-externArrayI32 = externArray-externArrayI64 :: (Typed a, Integral a)- => String -> Stream a -> Size- -> Maybe [[Int64]] -> Stream Int64-externArrayI64 = externArray-externArrayF :: (Typed a, Integral a)- => String -> Stream a -> Size- -> Maybe [[Float]] -> Stream Float-externArrayF = externArray-externArrayD :: (Typed a, Integral a)- => String -> Stream a -> Size- -> Maybe [[Double]] -> Stream Double-externArrayD = externArray
+ src/Copilot/Language/Operators/Struct.hs view
@@ -0,0 +1,19 @@+{-# LANGUAGE Safe #-}++module Copilot.Language.Operators.Struct+ ( (#)+ ) where++import Copilot.Core.Type+import Copilot.Core.Operators+import Copilot.Language.Stream (Stream (..))++import GHC.TypeLits (KnownSymbol)++--------------------------------------------------------------------------------++(#) :: (KnownSymbol s, Typed t, Typed a, Struct a)+ => Stream a -> (a -> Field s t) -> Stream t+(#) s f = Op1 (GetField typeOf typeOf (accessorname f)) s++--------------------------------------------------------------------------------
src/Copilot/Language/Operators/Temporal.hs view
@@ -9,7 +9,6 @@ module Copilot.Language.Operators.Temporal ( (++) , drop- , (#) ) where import Copilot.Core (Typed)@@ -29,11 +28,3 @@ drop _ ( Const j ) = Const j drop i ( Drop j s ) = Drop (fromIntegral i + j) s drop i s = Drop (fromIntegral i) s--(#) :: (Typed a, Typed b) => Stream a -> String -> Stream b-(#) = GetField-{-(ExternStruct cs sargs) # (Extern nm i) = Extern nm i-(ExternStruct cs sargs) # (ExternFun nm args i) = ExternFun nm args i-(ExternStruct cs sargs) # (ExternArray nm strm j i) = ExternArray nm strm j i-(ExternStruct cs sargs) # (ExternStruct nm args) = ExternStruct nm args-}---(ExternStruct cs sargs) # name = GetField (ExternStruct cs sargs) name
src/Copilot/Language/Reify.hs view
@@ -208,27 +208,6 @@ ------------------------------------------------------ - ExternArray cs e size mXs -> do- w <- go e- return $ Core.ExternArray typeOf typeOf cs size w mXs Nothing-- -------------------------------------------------------- ExternStruct cs sargs -> do- args' <- mapM (\(name, Arg e) -> mkStrArg (name, Arg e)) sargs- return $ Core.ExternStruct typeOf cs args' Nothing-- -------------------------------------------------------- GetField struct field -> do- s <- go struct- return $ Core.GetField typeOf typeOf s field- {- ISSUE: UNLIKE APPEND, GETFIELD DOES NOT HAVE CONSISTENT RETURN TYPE- --> NEED TO PROPERLY DEFINE GETFIELD IN EXPR- --> IMPLEMENT GETFIELD FROM CORE THROUGH LANGUAGE -}-- ------------------------------------------------------- Op1 op e -> do w <- go e return $ Core.Op1 op w
src/Copilot/Language/Stream.hs view
@@ -33,12 +33,6 @@ => String -> Maybe [a] -> Stream a ExternFun :: Typed a => String -> [Arg] -> Maybe (Stream a) -> Stream a- ExternArray :: (Typed a, Typed b, Integral a)- => String -> Stream a -> Int -> Maybe [[b]] -> Stream b- ExternStruct:: Typed a- => String -> [(String, Arg)] -> Stream a- GetField :: (Typed a, Typed b)- => Stream a -> String -> Stream b Local :: (Typed a, Typed b) => Stream a -> (Stream a -> Stream b) -> Stream b Var :: Typed a