lightbulb.tp

-- * Preparation

    -- allNot : Behavior Bool → Behavior Bool
    value allNot = λ b . Behavior (not (head b)) (const not ⊛ tail b)

    -- allXor : Behavior Bool → Behavior Bool
    value allXor = λ b₁ . λ b₂ . Behavior (xor (head b₁) (head b₂)) (const xor ⊛ tail b₁ ⊛ tail b₂)

    type Ticks = ν σ . event σ

    -- dropDummies : EventStream 1 → Ticks
    value dropDummies = unfold [Ticks] (λ s . (const second) ⊙ (unpack [EventStream 1] s))

    type Segments = ν σ . Behavior Bool × event σ

    -- flip : Behavior Bool × event α → event (Behavior Bool × α)
    value flip = λ p . const (onFirst allNot) ⊙ cut (first p) (second p)

    -- step : Behavior Bool × Ticks → Behavior Bool × event (Behavior Bool × Ticks)
    value step = λ p . (first p, flip (onSecond (unpack [Ticks]) p))

    -- alternate : Behavior Bool → Ticks → Segments
    value alternate = curry (unfold [Segments] step)

    type UltraswitchArg = ν σ . behavior Bool × event (Bool × σ)

    -- shiftRecPoints : behavior Bool × event Segments → UltraswitchArg
    value shiftRecPoints = unfold [UltraswitchArg]
                                  (onSecond (λ e . const (λ s . normalize (unpack [Segments] s)) ⊙ e))

    -- ultraswitchArg : Segments → UltraswitchArg
    value ultraswitchArg = λ s . shiftRecPoints (tail (first (unpack [Segments] s)),
                                                 second (unpack [Segments] s))

    -- prepareUltraswitch : Behavior Bool → EventStream 1 → nu s . behavior Bool × event (Bool × s)
    value prepareUltraswitch = λ b . λ s . ultraswitchArg (alternate b (dropDummies s))

-- * Actual example

    -- control : Behavior Bool → EventStream 1 → Behavior Bool
    value control = λ b . λ s . Behavior (head b) (ultraswitch (prepareUltraswitch b s))

    -- init : Bool
    value init = false

    -- one : EventStream 1 → Behavior Bool
    value one = control (Behavior init (const init))

    -- two : EventStream 1 → EventStream 1 → Behavior Bool
    value two = λ s₁ . λ s₂ . allXor (one s₁) (one s₂)

-- * Test cases

    -- s₁ : EventStream 1
    value s₁ = pack [EventStream 1] (event 2 ((),
               pack [EventStream 1] (const ? ⊙ never)))

    -- s₂ : EventStream 1
    value s₂ = pack [EventStream 1] (event 4 ((),
               pack [EventStream 1] (event 1 ((),
               pack [EventStream 1] (const ? ⊙ never)))))

    -- test : Behavior Bool
    value test = two s₁ s₂