{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE OverloadedLists #-}
{-# OPTIONS -fplugin=WidgetRattus.Plugin #-}
module Main (module Main) where
import WidgetRattus
import WidgetRattus.Signal
import Data.Set as Set
import Data.Text
import qualified Data.String as Str
import qualified GHC.Exts as Exts
boxedInt :: Box Int
boxedInt = box 8
lambdaUnderDelay :: O Int -> O ((Int -> Int -> Int) :* Int)
lambdaUnderDelay d = delay ((\x _ -> x) :* adv d)
sneakyLambdaUnderDelay :: O Int -> O ((Int -> Int -> Int) :* Int)
sneakyLambdaUnderDelay d = delay (let f x _ = x in f :* adv d)
lambdaUnderDelay' :: Int -> O Int -> O ((Int -> Int) :* Int)
lambdaUnderDelay' x d = delay ((\_ -> x) :* adv d)
sneakyLambdaUnderDelay' :: Int -> O Int -> O ((Int -> Int) :* Int)
sneakyLambdaUnderDelay' x d = delay ((let f _ = x in f) :* adv d)
scanBox :: Box(b -> a -> Box b) -> b -> Sig a -> Sig b
scanBox f acc (a ::: as) = unbox acc' ::: delay (scanBox f (unbox acc') (adv as))
where acc' = unbox f acc a
sumBox :: Sig Int -> Sig Int
sumBox = scanBox (box (\x y -> box (x + y))) 0
strMap :: Box (a -> b) -> Sig a -> Sig b
strMap f (x ::: xs) = unbox f x ::: delay (strMap f (adv xs))
strMap' :: Box (a -> b) -> Sig a -> Sig b
strMap' f = run
where run (x ::: xs) = unbox f x ::: delay (run (adv xs))
-- local mutual recursive definition
nestedMutual :: Sig Int -> Sig Int
nestedMutual = lbar1 (box (+1))
where lbar1 :: Box (a -> b) -> Sig a -> Sig b
lbar1 f (x ::: xs) = unbox f x ::: (delay (lbar2 f (adv xs)))
lbar2 :: Box (a -> b) -> Sig a -> Sig b
lbar2 f (x ::: xs) = unbox f x ::: (delay (lbar1 f (adv xs)))
-- mutual recursive definition
bar1 :: Box (a -> b) -> Sig a -> Sig b
bar1 f (x ::: xs) = unbox f x ::: delay (bar2 f (adv xs))
bar2 :: Box (a -> b) -> Sig a -> Sig b
bar2 f (x ::: xs) = unbox f x ::: delay (bar1 f (adv xs))
stableDelay :: Stable a => Box (a -> a -> a) -> a -> O a -> O a
stableDelay f v l = delay (unbox f v (adv l))
patternBinding :: Sig Int -> Sig Int
patternBinding str = (x + 1) ::: (delay (patternBinding (adv xs)))
where (x ::: xs) = sumBox str
data Input a = Input {jump :: !a, move :: !Move}
data Move = StartLeft | EndLeft | StartRight | EndRight | NoMove
-- The compiler plugin should detect that Input is a stable type and
-- thus remains in scope under the delay.
constS :: Stable a => Input a -> O Int -> Sig (Int :* Input a)
constS a l = (0 :* a) ::: delay ((adv l :* a) ::: never)
-- make sure that unit is recognized as stable
constU :: () -> O () -> Sig (() :* ())
constU a l = (() :* a) ::: delay ((adv l :* a) ::: never)
scan1 :: (Stable b) => Box(b -> a -> b) -> b -> Sig a -> Sig b
scan1 f acc (a ::: as) = acc' ::: delay (scan1 f acc' (adv as))
where acc' = unbox f acc a
scan2 :: (Stable b) => Box(b -> a -> b) -> b -> Sig a -> Sig b
scan2 f = run
where run acc (a ::: as) = let acc' = unbox f acc a
in acc' ::: delay (run acc' (adv as))
scanSet :: Sig Int -> Sig (Set Int)
scanSet = scan1 (box (\ s x -> Set.insert x s)) Set.empty
myMap :: Sig Int -> Sig Int
myMap (x ::: xs) = (x + 1) ::: delay (fst' (myMap (adv xs) :* nats never))
nats :: O Int -> Sig Int
nats l = 0 ::: delay (let (n ::: ns) = myMap (nats never) in (adv l + n) ::: ns)
nestedDelay :: Sig a -> Sig a
nestedDelay (a ::: as) = a ::: delay (let x ::: xs = adv as in x ::: delay (nestedDelay (adv xs)))
naiveIf :: Bool -> O a -> O a -> O (Bool :* a)
naiveIf b x y = delay (b :* adv (if b then x else y))
naiveIf' :: Bool -> O a -> O a -> O (Bool :* a)
naiveIf' b x y = delay (b :* adv later)
where
later = case b of
True -> x
False -> y
advUnderLambda :: O Int -> O (a -> Int)
advUnderLambda y = delay (\_ -> adv y)
stableText :: Text -> Sig Text -> Sig Text
stableText = scan (box append)
stableInteger :: Integer -> Sig Integer -> Sig Integer
stableInteger = scan (box (+))
dblAdv :: O (O a) -> O (O a)
dblAdv y = delay (delay (adv (adv y)))
delayAdvUnderLambda :: O () -> O (O Int -> O Int)
delayAdvUnderLambda d = delay (adv d `seq` \x -> delay (adv x))
-- This function is leaky unless the single tick transformation is
-- performed
leaky :: Sig () -> (() -> Bool) -> Sig Bool
leaky (() ::: d) p = p () ::: delay (let d' = adv d in (leaky d' (\ _ -> current (leaky d' (\ _ -> True)))))
unusedAdv :: O () -> O ()
unusedAdv d = delay (adv d `seq` ())
unusedAdv' :: O () -> O ()
unusedAdv' d = delay (let _ = adv d in ())
-- check whether the Stable constraint solver handles GADTs correctly.
data Pull a where
Fun :: Stable s => !s -> !(Box(s -> Int -> (s :* a))) -> Pull a
newtype Beh a = Beh (Sig (Pull a))
funTest :: Pull a -> O () -> O (Pull a)
funTest fun@(Fun x f) d = delay (let _ = adv d in x `seq` fun)
funTest2 :: Pull a -> O () -> O (Pull a)
funTest2 fun d = case fun of (!(Fun x f)) -> delay (let _ = adv d in x `seq` fun)
funTest3 :: C (Pull a) -> O () -> C (O (Pull a))
funTest3 fun d = do Fun x f <- fun
fun' <- fun
return (delay (let _ = adv d in x `seq` fun'))
funTest4 :: Pull a -> O () -> C (O (Pull a))
funTest4 fun@(Fun x f) d = do let (x':* v) = unbox f x 0
return (delay (let _ = adv d in x' `seq` fun))
funTest5 :: Pull a -> O () -> O (Pull a)
funTest5 fun@(Fun x f) d = delay (let _ = adv d in x' `seq` fun)
where (x':* v) = unbox f x 0
funTest6 :: Pull a -> O () -> O (Pull a)
funTest6 fun@(Fun x f) d = let (x':* v) = unbox f x 0 in delay (let _ = adv d in x' `seq` fun)
-- the stable constraint must reach a pattern guard
funTestGuard :: Pull a -> O () -> O (Pull a)
funTestGuard fun d
| Fun x _ <- fun = delay (let _ = adv d in x `seq` fun)
-- ... and a bind statement in do notation
{-# ANN funTestBind AllowLazyData #-}
funTestBind :: Maybe (Pull a) -> O () -> Maybe (O (Pull a))
funTestBind fun d = do Fun x _ <- fun
fun' <- fun
return (delay (let _ = adv d in x `seq` fun'))
-- ... and a match on a constructor of a data family instance, which
-- the type checker wraps in a coercion pattern
data family Fam a
data instance Fam Int where
MkFam :: Stable s => !s -> Fam Int
funTestFamily :: Fam Int -> O () -> O ()
funTestFamily (MkFam x) d = delay (let _ = adv d in x `seq` ())
funTestWorkaround :: Pull a -> O () -> O (Pull a)
funTestWorkaround fun@(Fun x f) d = foo x fun
where foo :: Stable s => s -> (Pull a) -> O (Pull a)
foo x fun = delay (let _ = adv d in x `seq` fun)
zipFun :: Box (a -> b -> c) -> Pull a -> Pull b -> Pull c
zipFun f (Fun sa fa) (Fun sb fb) = Fun (sa :* sb)
(box (\ (sa' :* sb') t ->
let (sa'' :* a) = unbox fa sa' t
(sb'' :* b) = unbox fb sb' t
in ((sa'' :* sb'') :* unbox f a b) ))
zipWithBeh :: (Stable a, Stable b) => Box (a -> b -> c) -> Beh a -> Beh b -> Beh c
zipWithBeh f (Beh as) (Beh bs) = Beh (run as bs) where
run (a ::: as) (b ::: bs) = zipFun f a b ::: delay
(case select as bs of
Fst as' lbs -> run as' (b ::: lbs)
Snd las bs' -> run (a ::: las) bs'
Both as' bs' -> run as' bs')
-- check that newtypes over stable types are recognised as stable
newtype Count = Count Int
newtypeStable :: Count -> O () -> O Count
newtypeStable x d = delay (let _ = adv d in x)
-- check the strict sum type
strictSum :: Int :+ Bool -> Int
strictSum (Left' n) = n
strictSum (Right' b) = if b then 1 else 0
strictSumStable :: Int :+ Bool -> O () -> O (Int :+ Bool)
strictSumStable x d = delay (let _ = adv d in x)
-- check the Functor instance of Maybe'
incMaybe' :: Maybe' Int -> Maybe' Int
incMaybe' = fmap (+1)
-- The definitions below must not produce a "may lead to memory leaks"
-- warning: the lazy arguments of fromString, fromList/fromListN and
-- Data.Text.pack are consumed immediately and are not retained. Note
-- that the arguments must not be literals, since those are already
-- exempt from the check.
-- fromListN, as inserted by OverloadedLists
intSet :: Set Int
intSet = [1,2,3]
-- fromList, the method of the IsList class
setFromList :: [Int] -> Set Int
setFromList xs = Exts.fromList xs
-- fromString, the method of the IsString class
textFromString :: String -> Text
textFromString s = Str.fromString s
-- Data.Text.pack
packedText :: String -> Text
packedText s = pack s
-- 'Item l' must be recognised as strict whenever 'l' is.
itemStrict :: IsList l => l -> Item l -> List (Item l)
itemStrict _ x = x :! Nil
main = putStrLn "This file should just type check"