--
-- The MoCC of Signal in Haskell (clocked)
-- Jean-Pierre.Talpin@inria.fr 12/3/15
--

Module Signals where

-- an event is (now) present with a value or (determined) absent

data Event a = absent | now a

-- a signal is a (non empty?) lazy list of events 
-- type Signal a = {v: [Event a] | len(v) > 0}

type Signal a = [Event a]

-- the clock of a signal 

measure clk :: a Signal -> Bool
clk (absent : _) = false
clk ((now _) : _) = true

-- the value of a signal 

measure val :: a Signal -> a
val ((now v) : _) = v

-- not defined if absent ... how to say that val v => clk v ?

-- feedback: pre initially returns w and then the stored head of x
-- pre's, y's and w property should be a fixpoint p
--
--      {-@ pre :: forall <p :: Prop>. Signal a<p> -> a<p> -> Signal a<p> @-}
--
-- p should contain clk x = clk pre here just true

pre :: Signal a -> a -> Signal a
pre (x as ((now v) : _) w = (now w) : pre x v
pre (x as (absent  : _) w =  absent : pre x w
infix pre

-- synchronous sample à la Lustre

{-@ sample :: x:Signal a -> y:Signal Bool -> {v:Signal a| clk v = clk x = clk y} @-}

sample :: Signal a -> Signal Bool -> Signal a
sample ((now v) : x) ((now True)  : y) = v : sample x y
sample ((now _) : x) ((now False) : y) = absent : sample x y
sample (absent  : x) (absent      : y) = absent : sample x y

-- synchronous merge à la Lustre

{-@ merge :: x:Signal Bool -> y:Signal a -> z:Signal a -> {v:Signal a| clk v = clk x = clk y = clk z} @-}

merge :: Signal Bool -> Signal a -> Signal a -> Signal a
merge ((now True)  : x) ((now v) : y) ((now _) : z) = v : merge x y z
merge ((now False) : x) ((now _) : y) ((now v) : z) = v : merge x y z
merge (absent      : x) (absent  : y) (absent  : z) = absent : merge x y z

-- sample à la Signal

{-@ when :: x:Signal a -> y:Signal Bool -> {v:Signal a| clk v = clk x and val y} @-}

when :: Signal a -> Signal Bool -> Signal a
when ((now v) : x) ((now True)  : y) = v : when x y
when (_       : x) ((now False) : y) = absent : when x y
when (_       : x) (absent      : y) = absent : when x y

-- merge à la Signal

{-@ combine :: x:Signal Bool -> y:Signal a -> z:Signal a -> {v:Signal a| clk v = clk x or clk y} @-}

combine :: Signal a -> Signal a -> Signal a
combine ((now v) : x) (_ : y) = v : combine x y 
combine (absent  : x) (v : y) = v : combine x y