{-# LANGUAGE NoImplicitPrelude #-}
module Copilot.Library.LTL
( next, eventually, always, until, release ) where
import Copilot.Language
import Copilot.Library.Utils
next :: Stream Bool -> Stream Bool
next :: Stream Bool -> Stream Bool
next = Int -> Stream Bool -> Stream Bool
forall a. Typed a => Int -> Stream a -> Stream a
drop ( Int
1 :: Int )
always :: ( Integral a ) => a -> Stream Bool -> Stream Bool
always :: a -> Stream Bool -> Stream Bool
always a
n = Int
-> (Stream Bool -> Stream Bool -> Stream Bool)
-> Stream Bool
-> Stream Bool
forall a.
Typed a =>
Int -> (Stream a -> Stream a -> Stream a) -> Stream a -> Stream a
nfoldl1 ( a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 ) Stream Bool -> Stream Bool -> Stream Bool
(&&)
eventually :: ( Integral a ) =>
a
-> Stream Bool
-> Stream Bool
eventually :: a -> Stream Bool -> Stream Bool
eventually a
n = Int
-> (Stream Bool -> Stream Bool -> Stream Bool)
-> Stream Bool
-> Stream Bool
forall a.
Typed a =>
Int -> (Stream a -> Stream a -> Stream a) -> Stream a -> Stream a
nfoldl1 ( a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 ) Stream Bool -> Stream Bool -> Stream Bool
(||)
until :: ( Integral a ) => a -> Stream Bool -> Stream Bool -> Stream Bool
until :: a -> Stream Bool -> Stream Bool -> Stream Bool
until a
0 Stream Bool
_ Stream Bool
s1 = Stream Bool
s1
until a
n Stream Bool
s0 Stream Bool
s1 = (Stream Bool -> Stream Bool -> Stream Bool)
-> Stream Bool -> [Stream Bool] -> Stream Bool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Stream Bool -> Stream Bool -> Stream Bool
(||) Stream Bool
s1 [Stream Bool]
v0
where n' :: Int
n' = a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n
v0 :: [Stream Bool]
v0 = [ Int -> Stream Bool -> Stream Bool
forall a. Integral a => a -> Stream Bool -> Stream Bool
always ( Int
i :: Int ) Stream Bool
s0 Stream Bool -> Stream Bool -> Stream Bool
&& Int -> Stream Bool -> Stream Bool
forall a. Typed a => Int -> Stream a -> Stream a
drop ( Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 ) Stream Bool
s1
| Int
i <- [ Int
0 .. Int
n' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 ]
]
release :: ( Integral a ) => a -> Stream Bool -> Stream Bool -> Stream Bool
release :: a -> Stream Bool -> Stream Bool -> Stream Bool
release a
0 Stream Bool
_ Stream Bool
s1 = Stream Bool
s1
release a
n Stream Bool
s0 Stream Bool
s1 = a -> Stream Bool -> Stream Bool
forall a. Integral a => a -> Stream Bool -> Stream Bool
always a
n Stream Bool
s1 Stream Bool -> Stream Bool -> Stream Bool
|| (Stream Bool -> Stream Bool -> Stream Bool)
-> [Stream Bool] -> Stream Bool
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Stream Bool -> Stream Bool -> Stream Bool
(||) [Stream Bool]
v0
where n' :: Int
n' = a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n
v0 :: [Stream Bool]
v0 = [ Int -> Stream Bool -> Stream Bool
forall a. Integral a => a -> Stream Bool -> Stream Bool
always ( Int
i :: Int ) Stream Bool
s1 Stream Bool -> Stream Bool -> Stream Bool
&& Int -> Stream Bool -> Stream Bool
forall a. Typed a => Int -> Stream a -> Stream a
drop Int
i Stream Bool
s0
| Int
i <- [ Int
0 .. Int
n' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 ]
]